CompositionInformationVisitor.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <map>
#include <set>
 
#include <boost/optional.hpp>
 
#include "storm/storage/jani/visitor/CompositionVisitor.h"
 
namespace storm {
namespace jani {
 
class Model;
 
class CompositionInformation {
   public:
    CompositionInformation();
 
    void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);
    std::map<std::string, uint64_t> const& getAutomatonToMultiplicityMap() const;
    static std::map<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
    void addMultiplicityMap(std::map<std::string, uint64_t> const& multiplicityMap);
 
    void setContainsNonStandardParallelComposition(bool value);
    bool containsNonStandardParallelComposition() const;
 
    void setContainsNestedParallelComposition(bool value);
    bool containsNestedParallelComposition() const;
 
    void setContainsParallelComposition(bool value);
    bool containsParallelComposition() const;
 
    std::string const& getActionName(uint64_t index) const;
    uint64_t getActionIndex(std::string const& name) const;
 
    void addNonSilentActionIndex(uint64_t index);
    void addNonSilentActionIndices(std::set<uint64_t> const& indices);
    bool hasNonSilentActionIndex(uint64_t index);
    void addInputEnabledActionIndex(uint64_t index);
 
    std::set<uint64_t> const& getNonSilentActionIndices() const;
    std::set<uint64_t> const& getInputEnabledActionIndices() const;
 
    void setMappings(std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap);
 
   private:
    std::set<uint64_t> nonSilentActionIndices;

    std::set<uint64_t> inputEnabledActionIndices;

    std::map<uint64_t, std::string> indexToNameMap;

    std::map<std::string, uint64_t> nameToIndexMap;

    std::map<std::string, uint64_t> automatonNameToMultiplicity;

    bool nonStandardParallelComposition;

    bool nestedParallelComposition;

    bool parallelComposition;
};
 
class CompositionInformationVisitor : public CompositionVisitor {
   public:
    CompositionInformationVisitor(Model const& model, Composition const& composition);
    CompositionInformation getInformation();
 
    virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
    virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
 
   private:
    uint64_t addOrGetActionIndex(std::string const& name);
 
    storm::jani::Model const& model;
    Composition const& composition;
    uint64_t nextFreeActionIndex;
    std::map<std::string, uint64_t> nameToIndexMap;
    std::map<uint64_t, std::string> indexToNameMap;
};
 
}  // namespace jani
}  // namespace storm