Program.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_PRISM_PROGRAM_H_
#define STORM_STORAGE_PRISM_PROGRAM_H_
 
#include <boost/optional.hpp>
#include <map>
#include <memory>
#include <set>
#include <vector>
 
#include "storm/storage/BitVector.h"
#include "storm/storage/BoostTypes.h"
#include "storm/storage/PlayerIndex.h"
#include "storm/storage/prism/Composition.h"
#include "storm/storage/prism/Constant.h"
#include "storm/storage/prism/Formula.h"
#include "storm/storage/prism/InitialConstruct.h"
#include "storm/storage/prism/Label.h"
#include "storm/storage/prism/Module.h"
#include "storm/storage/prism/Player.h"
#include "storm/storage/prism/RewardModel.h"
#include "storm/storage/prism/SystemCompositionConstruct.h"
#include "storm/utility/OsDetection.h"
#include "storm/utility/solver.h"
 
namespace storm {
namespace jani {
class Model;
class Property;
}  // namespace jani
 
namespace prism {
class Program : public LocatedInformation {
   public:
    enum class ModelType { UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA, SMG };
 
    enum class ValidityCheckLevel : unsigned { VALIDINPUT = 0, READYFORPROCESSING = 1 };
 
    Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants,
            std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables,
            std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules,
            std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels,
            std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct,
            boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "",
            uint_fast64_t lineNumber = 0, bool finalModel = true);
 
    // Provide default implementations for constructors and assignments.
    Program() = default;
    Program(Program const& other) = default;
    Program& operator=(Program const& other) = default;
    Program(Program&& other) = default;
    Program& operator=(Program&& other) = default;
 
    ModelType getModelType() const;
 
    bool isDiscreteTimeModel() const;
 
    bool isDeterministicModel() const;
 
    bool isPartiallyObservable() const;
 
    bool hasUnboundedVariables() const;
 
    bool hasUndefinedConstants() const;
 
    bool undefinedConstantsAreGraphPreserving() const;
 
    std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
 
    std::string getUndefinedConstantsAsString() const;
 
    bool hasConstant(std::string const& constantName) const;
 
    Constant const& getConstant(std::string const& constantName) const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> getFormulasSubstitution() const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsFormulasSubstitution(bool getConstantsSubstitution = true,
                                                                                                            bool getFormulasSubstitution = true) const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> getSubstitutionForRenamedModule(
        Module const& renamedModule, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
 
    std::map<std::string, std::string> getFinalRenamingOfModule(Module const& renamedModule) const;
 
    std::vector<Constant> const& getConstants() const;
 
    std::size_t getNumberOfConstants() const;
 
    std::vector<Constant> usedConstants() const;
 
    size_t getNumberOfCommands() const;
 
    bool globalBooleanVariableExists(std::string const& variableName) const;
 
    bool globalIntegerVariableExists(std::string const& variableName) const;
 
    std::vector<BooleanVariable> const& getGlobalBooleanVariables() const;
 
    BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
 
    std::vector<IntegerVariable> const& getGlobalIntegerVariables() const;
 
    IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
 
    std::set<storm::expressions::Variable> getAllExpressionVariables(bool includeConstants = true) const;
 
    std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
 
    std::size_t getNumberOfGlobalBooleanVariables() const;
 
    std::size_t getNumberOfGlobalIntegerVariables() const;
 
    std::vector<Formula> const& getFormulas() const;
 
    std::size_t getNumberOfFormulas() const;
 
    std::size_t getNumberOfModules() const;
 
    Module const& getModule(uint_fast64_t index) const;
 
    bool hasModule(std::string const& moduleName) const;
 
    Module const& getModule(std::string const& moduleName) const;
 
    std::vector<Module> const& getModules() const;
 
    std::vector<Player> const& getPlayers() const;
 
    std::size_t getNumberOfPlayers() const;
 
    storm::storage::PlayerIndex const& getIndexOfPlayer(std::string const& playerName) const;
 
    std::map<std::string, storm::storage::PlayerIndex> const& getPlayerNameToIndexMapping() const;
 
    std::vector<storm::storage::PlayerIndex> buildModuleIndexToPlayerIndexMap() const;
 
    std::map<uint_fast64_t, storm::storage::PlayerIndex> buildActionIndexToPlayerIndexMap() const;
 
    std::map<std::string, uint_fast64_t> const& getActionNameToIndexMapping() const;
 
    void updateInitialStatesExpression(expressions::Expression const& newExpression);
 
    bool hasInitialConstruct() const;
 
    storm::expressions::Expression getInitialStatesExpression() const;
 
    bool specifiesSystemComposition() const;
 
    SystemCompositionConstruct const& getSystemCompositionConstruct() const;
 
    boost::optional<SystemCompositionConstruct> getOptionalSystemCompositionConstruct() const;
 
    std::shared_ptr<Composition> getDefaultSystemComposition() const;
 
    std::set<std::string> const& getActions() const;
 
    std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
 
    std::string const& getActionName(uint_fast64_t actionIndex) const;
 
    uint_fast64_t getActionIndex(std::string const& actionName) const;
 
    bool hasAction(std::string const& actionName) const;
 
    bool hasAction(uint_fast64_t const& actionIndex) const;
 
    std::set<uint_fast64_t> const& getModuleIndicesByAction(std::string const& action) const;
 
    std::set<uint_fast64_t> const& getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const;
 
    uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
 
    std::pair<uint_fast64_t, uint_fast64_t> getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const;
 
    /*
     * Get total number of unlabeled commands
     */
    uint64_t getNumberOfUnlabeledCommands() const;
 
    bool hasRewardModel() const;
 
    bool hasRewardModel(std::string const& name) const;
 
    std::vector<RewardModel> const& getRewardModels() const;
 
    std::size_t getNumberOfRewardModels() const;
 
    RewardModel const& getRewardModel(std::string const& rewardModelName) const;
 
    RewardModel const& getRewardModel(uint_fast64_t index) const;
 
    bool hasLabel(std::string const& labelName) const;
 
    std::vector<Label> const& getLabels() const;
 
    std::vector<storm::expressions::Expression> getAllGuards(bool negated = false) const;
 
    storm::expressions::Expression const& getLabelExpression(std::string const& label) const;
 
    std::map<std::string, storm::expressions::Expression> getLabelToExpressionMapping() const;
 
    std::size_t getNumberOfLabels() const;
 
    void addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression);
 
    void removeLabel(std::string const& name);
 
    void filterLabels(std::set<std::string> const& labelSet);
 
    void removeRewardModels();
 
    std::vector<ObservationLabel> const& getObservationLabels() const;
 
    std::size_t getNumberOfObservationLabels() const;
 
    Program restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const;
 
    Program defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
 
    Program substituteConstants() const;
 
    Program substituteFormulas() const;
 
    Program substituteNonStandardPredicates() const;
 
    Program substituteConstantsFormulas(bool substituteConstants = true, bool substituteFormulas = true) const;
 
    Program replaceVariableInitializationByInitExpression() const;
 
    Program replaceConstantByVariable(Constant const& c, expressions::Expression const& lowerBound, expressions::Expression const& upperBound,
                                      bool observable = true) const;
 
    Program simplify();
 
    void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) const;
 
    Program flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory =
                               std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
 
    Program labelUnlabelledCommands(std::map<uint64_t, std::string> const& nameSuggestions = {}) const;
 
    friend std::ostream& operator<<(std::ostream& stream, Program const& program);
 
    storm::expressions::ExpressionManager& getManager() const;
 
    std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
 
    std::unordered_map<uint_fast64_t, uint_fast64_t> buildCommandIndexToActionIndex() const;
 
    std::unordered_map<uint_fast64_t, std::string> buildActionIndexToActionNameMap() const;
 
    storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "") const;
 
    std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties,
                                                                             bool allVariablesGlobal = true, std::string suffix = "") const;
 
    storm::storage::BitVector const& getPossiblySynchronizingCommands() const;
 
   private:
    InitialConstruct const& getInitialConstruct() const;
 
    boost::optional<InitialConstruct> const& getOptionalInitialConstruct() const;
 
    Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName,
                                std::vector<std::reference_wrapper<Command const>> const& commands) const;
 
    void createMissingInitialValues();
 
    // The manager responsible for the variables/expressions of the program.
    std::shared_ptr<storm::expressions::ExpressionManager> manager;
 
    // Creates the internal mappings.
    void createMappings();
 
    uint64_t getHighestCommandIndex() const;
 
    // The type of the model.
    ModelType modelType;
 
    // The constants of the program.
    std::vector<Constant> constants;
 
    // A mapping from constant names to their corresponding indices.
    std::map<std::string, uint_fast64_t> constantToIndexMap;
 
    // The global boolean variables.
    std::vector<BooleanVariable> globalBooleanVariables;
 
    // A mapping from global boolean variable names to their corresponding indices.
    std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
 
    // The global integer variables.
    std::vector<IntegerVariable> globalIntegerVariables;
 
    // A mapping from global integer variable names to their corresponding indices.
    std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
 
    // The formulas defined in the program.
    std::vector<Formula> formulas;
 
    // A mapping of formula names to their corresponding indices.
    std::map<std::string, uint_fast64_t> formulaToIndexMap;
 
    // The players associated with the program.
    std::vector<Player> players;
 
    // A mapping of player names to their indices.
    std::map<std::string, storm::storage::PlayerIndex> playerToIndexMap;
 
    // The modules associated with the program.
    std::vector<Module> modules;
 
    // A mapping of module names to their indices.
    std::map<std::string, uint_fast64_t> moduleToIndexMap;
 
    // The reward models associated with the program.
    std::vector<RewardModel> rewardModels;
 
    // A mapping of reward models to their indices.
    std::map<std::string, uint_fast64_t> rewardModelToIndexMap;
 
    // The initial construct of the program.
    boost::optional<InitialConstruct> initialConstruct;
 
    // If set, this specifies the way the modules are composed to obtain the full system.
    boost::optional<SystemCompositionConstruct> systemCompositionConstruct;
 
    // The labels that are defined for this model.
    std::vector<Label> labels;
 
    // A mapping from labels to their indices.
    std::map<std::string, uint_fast64_t> labelToIndexMap;
 
    // Observation labels
    std::vector<ObservationLabel> observationLabels;
 
    // A mapping from action names to their indices.
    std::map<std::string, uint_fast64_t> actionToIndexMap;
 
    // A mapping from action indices to their names.
    std::map<uint_fast64_t, std::string> indexToActionMap;
 
    // The set of actions present in this program.
    std::set<std::string> actions;
 
    // The set of synchronizing actions present in this program.
    std::set<uint_fast64_t> synchronizingActionIndices;
 
    // A map of actions to the set of modules containing commands labelled with this action.
    std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToModuleIndexMap;
 
    // A mapping from variable names to the modules in which they were declared.
    std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
 
    storage::BitVector possiblySynchronizingCommands;
 
    bool prismCompatibility;
};
 
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
 
}  // namespace prism
}  // namespace storm
 
#endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */