Module.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <memory>
#include <set>
#include <string>
#include <vector>
 
#include "storm/storage/BoostTypes.h"
#include "storm/storage/prism/BooleanVariable.h"
#include "storm/storage/prism/ClockVariable.h"
#include "storm/storage/prism/Command.h"
#include "storm/storage/prism/IntegerVariable.h"
#include "storm/storage/prism/ModuleRenaming.h"
 
namespace storm {
namespace prism {
class Module : public LocatedInformation {
   public:
    Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
           std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
           storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename = "",
           uint_fast64_t lineNumber = 0);

    Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables,
           std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables,
           storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule,
           storm::prism::ModuleRenaming const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    // Create default implementations of constructors/assignment.
    Module() = default;
    Module(Module const& other) = default;
    Module& operator=(Module const& other) = default;
    Module(Module&& other) = default;
    Module& operator=(Module&& other) = default;

    bool hasUnboundedVariables() const;

    std::size_t getNumberOfBooleanVariables() const;

    std::size_t getNumberOfIntegerVariables() const;

    storm::prism::BooleanVariable const& getBooleanVariable(std::string const& variableName) const;

    std::vector<storm::prism::BooleanVariable> const& getBooleanVariables() const;

    storm::prism::IntegerVariable const& getIntegerVariable(std::string const& variableName) const;

    std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;

    std::size_t getNumberOfClockVariables() const;

    storm::prism::ClockVariable const& getClockVariable(std::string const& variableName) const;

    std::vector<storm::prism::ClockVariable> const& getClockVariables() const;

    std::set<storm::expressions::Variable> getAllExpressionVariables() const;

    std::vector<storm::expressions::Expression> getAllRangeExpressions() const;

    std::size_t getNumberOfCommands() const;

    std::size_t getNumberOfUpdates() const;

    storm::prism::Command const& getCommand(uint_fast64_t index) const;

    std::vector<storm::prism::Command> const& getCommands() const;

    std::vector<storm::prism::Command>& getCommands();

    std::string const& getName() const;

    std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;

    bool hasActionIndex(uint_fast64_t actionIndex) const;

    bool isRenamedFromModule() const;

    std::string const& getBaseModule() const;

    std::map<std::string, std::string> const& getRenaming() const;

    std::set<uint_fast64_t> const& getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const;

    Module restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const;

    Module restrictActionIndices(storm::storage::FlatSet<uint_fast64_t> const& actionIndices) const;

    Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;

    Module substituteNonStandardPredicates() const;

    Module labelUnlabelledCommands(std::map<uint64_t, std::string> const& suggestions, uint64_t& newId, std::map<std::string, uint64_t>& nameToIdMapping) const;

    bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;

    void createMissingInitialValues();

    void removeVariableInitialization();
 
    /*
     * Gets the number of commands without a label
     */
    uint64_t getNumberOfUnlabeledCommands() const;

    bool hasInvariant() const;

    storm::expressions::Expression const& getInvariant() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
   private:
    void createMappings();
 
    // The name of the module.
    std::string moduleName;
 
    // A list of boolean variables.
    std::vector<storm::prism::BooleanVariable> booleanVariables;
 
    // A mapping from boolean variables to the corresponding indices in the vector.
    std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
 
    // A list of integer variables.
    std::vector<storm::prism::IntegerVariable> integerVariables;
 
    // A mapping from integer variables to the corresponding indices in the vector.
    std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
 
    // A list of clock variables.
    std::vector<storm::prism::ClockVariable> clockVariables;
 
    // A mapping from clock variables to the corresponding indices in the vector.
    std::map<std::string, uint_fast64_t> clockVariableToIndexMap;
 
    // An invariant (only for PTA models)
    storm::expressions::Expression invariant;
 
    // The commands associated with the module.
    std::vector<storm::prism::Command> commands;
 
    // The set of action indices present in this module.
    std::set<uint_fast64_t> synchronizingActionIndices;
 
    // A map of actions to the set of commands labeled with this action.
    std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;
 
    // This string indicates whether and from what module this module was created via renaming.
    std::string renamedFromModule;
 
    // If the module was created by renaming, this mapping contains the provided renaming of identifiers.
    storm::prism::ModuleRenaming renaming;
};
 
}  // namespace prism
}  // namespace storm