Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Program.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_PROGRAM_H_
2#define STORM_STORAGE_PRISM_PROGRAM_H_
3
4#include <boost/optional.hpp>
5#include <map>
6#include <memory>
7#include <set>
8#include <vector>
9
23
24namespace storm {
25namespace jani {
26class Model;
27class Property;
28} // namespace jani
29
30namespace prism {
32 public:
36 enum class ModelType { UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA, SMG };
37
38 enum class ValidityCheckLevel : unsigned { VALIDINPUT = 0, READYFORPROCESSING = 1 };
39
62 Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants,
63 std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables,
64 std::vector<Formula> const& formulas, std::vector<Player> const& players, std::vector<Module> const& modules,
65 std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels,
66 std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct,
67 boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "",
68 uint_fast64_t lineNumber = 0, bool finalModel = true);
69
70 // Provide default implementations for constructors and assignments.
71 Program() = default;
72 Program(Program const& other) = default;
73 Program& operator=(Program const& other) = default;
74 Program(Program&& other) = default;
75 Program& operator=(Program&& other) = default;
76
82 ModelType getModelType() const;
83
89 bool isDiscreteTimeModel() const;
90
94 bool isDeterministicModel() const;
95
99 bool isPartiallyObservable() const;
100
104 bool hasUnboundedVariables() const;
105
111 bool hasUndefinedConstants() const;
112
121
127 std::vector<std::reference_wrapper<Constant const>> getUndefinedConstants() const;
128
134 std::string getUndefinedConstantsAsString() const;
135
142 bool hasConstant(std::string const& constantName) const;
143
150 Constant const& getConstant(std::string const& constantName) const;
151
157 std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
158
164 std::map<storm::expressions::Variable, storm::expressions::Expression> getFormulasSubstitution() const;
165
171 std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsFormulasSubstitution(bool getConstantsSubstitution = true,
172 bool getFormulasSubstitution = true) const;
173
177 std::map<storm::expressions::Variable, storm::expressions::Expression> getSubstitutionForRenamedModule(
178 Module const& renamedModule, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
179
184 std::map<std::string, std::string> getFinalRenamingOfModule(Module const& renamedModule) const;
185
191 std::vector<Constant> const& getConstants() const;
192
198 std::size_t getNumberOfConstants() const;
199
204 std::vector<Constant> usedConstants() const;
205
209 size_t getNumberOfCommands() const;
210
217 bool globalBooleanVariableExists(std::string const& variableName) const;
218
225 bool globalIntegerVariableExists(std::string const& variableName) const;
226
232 std::vector<BooleanVariable> const& getGlobalBooleanVariables() const;
233
240 BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
241
247 std::vector<IntegerVariable> const& getGlobalIntegerVariables() const;
248
255 IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
256
263 std::set<storm::expressions::Variable> getAllExpressionVariables(bool includeConstants = true) const;
264
270 std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
271
277 std::size_t getNumberOfGlobalBooleanVariables() const;
278
284 std::size_t getNumberOfGlobalIntegerVariables() const;
285
291 std::vector<Formula> const& getFormulas() const;
292
298 std::size_t getNumberOfFormulas() const;
299
305 std::size_t getNumberOfModules() const;
306
313 Module const& getModule(uint_fast64_t index) const;
314
320 bool hasModule(std::string const& moduleName) const;
321
328 Module const& getModule(std::string const& moduleName) const;
329
335 std::vector<Module> const& getModules() const;
336
342 std::vector<Player> const& getPlayers() const;
343
349 std::size_t getNumberOfPlayers() const;
350
356 storm::storage::PlayerIndex const& getIndexOfPlayer(std::string const& playerName) const;
357
361 std::map<std::string, storm::storage::PlayerIndex> const& getPlayerNameToIndexMapping() const;
362
367 std::vector<storm::storage::PlayerIndex> buildModuleIndexToPlayerIndexMap() const;
368
373 std::map<uint_fast64_t, storm::storage::PlayerIndex> buildActionIndexToPlayerIndexMap() const;
374
380 std::map<std::string, uint_fast64_t> const& getActionNameToIndexMapping() const;
381
387
391 bool hasInitialConstruct() const;
392
399
403 bool hasIntervalUpdates() const;
404
411 bool specifiesSystemComposition() const;
412
419
425 boost::optional<SystemCompositionConstruct> getOptionalSystemCompositionConstruct() const;
426
432 std::shared_ptr<Composition> getDefaultSystemComposition() const;
433
439 std::set<std::string> const& getActions() const;
440
446 std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
447
454 std::string const& getActionName(uint_fast64_t actionIndex) const;
455
462 uint_fast64_t getActionIndex(std::string const& actionName) const;
463
469 bool hasAction(std::string const& actionName) const;
470
476 bool hasAction(uint_fast64_t const& actionIndex) const;
477
485 std::set<uint_fast64_t> const& getModuleIndicesByAction(std::string const& action) const;
486
494 std::set<uint_fast64_t> const& getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const;
495
502 uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
503
515 std::pair<uint_fast64_t, uint_fast64_t> getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const;
516
517 /*
518 * Get total number of unlabeled commands
519 */
520 uint64_t getNumberOfUnlabeledCommands() const;
521
527 bool hasRewardModel() const;
528
535 bool hasRewardModel(std::string const& name) const;
536
542 std::vector<RewardModel> const& getRewardModels() const;
543
549 std::size_t getNumberOfRewardModels() const;
550
557 RewardModel const& getRewardModel(std::string const& rewardModelName) const;
558
565 RewardModel const& getRewardModel(uint_fast64_t index) const;
566
573 bool hasLabel(std::string const& labelName) const;
574
580 std::vector<Label> const& getLabels() const;
581
588 std::vector<storm::expressions::Expression> getAllGuards(bool negated = false) const;
589
595 storm::expressions::Expression const& getLabelExpression(std::string const& label) const;
596
602 std::map<std::string, storm::expressions::Expression> getLabelToExpressionMapping() const;
603
609 std::size_t getNumberOfLabels() const;
610
617 void addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression);
618
624 void removeLabel(std::string const& name);
625
632 void filterLabels(std::set<std::string> const& labelSet);
633
634 void removeRewardModels();
635
641 std::vector<ObservationLabel> const& getObservationLabels() const;
642
648 std::size_t getNumberOfObservationLabels() const;
649
656
665 Program defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
666
674
682
687
695
702
712 bool observable = true) const;
713
719
725
732 Program flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory =
733 std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
734
742 Program labelUnlabelledCommands(std::map<uint64_t, std::string> const& nameSuggestions = {}) const;
743
744 friend std::ostream& operator<<(std::ostream& stream, Program const& program);
745
752
753 std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
754
755 std::unordered_map<uint_fast64_t, uint_fast64_t> buildCommandIndexToActionIndex() const;
756
757 std::unordered_map<uint_fast64_t, std::string> buildActionIndexToActionNameMap() const;
758
762 storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "") const;
763
769 std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties,
770 bool allVariablesGlobal = true, std::string suffix = "") const;
771
777
778 private:
784 InitialConstruct const& getInitialConstruct() const;
785
791 boost::optional<InitialConstruct> const& getOptionalInitialConstruct() const;
792
803 Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName,
804 std::vector<std::reference_wrapper<Command const>> const& commands) const;
805
809 void createMissingInitialValues();
810
811 // The manager responsible for the variables/expressions of the program.
812 std::shared_ptr<storm::expressions::ExpressionManager> manager;
813
814 // Creates the internal mappings.
815 void createMappings();
816
817 uint64_t getHighestCommandIndex() const;
818
819 // The type of the model.
820 ModelType modelType;
821
822 // The constants of the program.
823 std::vector<Constant> constants;
824
825 // A mapping from constant names to their corresponding indices.
826 std::map<std::string, uint_fast64_t> constantToIndexMap;
827
828 // The global boolean variables.
829 std::vector<BooleanVariable> globalBooleanVariables;
830
831 // A mapping from global boolean variable names to their corresponding indices.
832 std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
833
834 // The global integer variables.
835 std::vector<IntegerVariable> globalIntegerVariables;
836
837 // A mapping from global integer variable names to their corresponding indices.
838 std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
839
840 // The formulas defined in the program.
841 std::vector<Formula> formulas;
842
843 // A mapping of formula names to their corresponding indices.
844 std::map<std::string, uint_fast64_t> formulaToIndexMap;
845
846 // The players associated with the program.
847 std::vector<Player> players;
848
849 // A mapping of player names to their indices.
850 std::map<std::string, storm::storage::PlayerIndex> playerToIndexMap;
851
852 // The modules associated with the program.
853 std::vector<Module> modules;
854
855 // A mapping of module names to their indices.
856 std::map<std::string, uint_fast64_t> moduleToIndexMap;
857
858 // The reward models associated with the program.
859 std::vector<RewardModel> rewardModels;
860
861 // A mapping of reward models to their indices.
862 std::map<std::string, uint_fast64_t> rewardModelToIndexMap;
863
864 // The initial construct of the program.
865 boost::optional<InitialConstruct> initialConstruct;
866
867 // If set, this specifies the way the modules are composed to obtain the full system.
868 boost::optional<SystemCompositionConstruct> systemCompositionConstruct;
869
870 // The labels that are defined for this model.
871 std::vector<Label> labels;
872
873 // A mapping from labels to their indices.
874 std::map<std::string, uint_fast64_t> labelToIndexMap;
875
876 // Observation labels
877 std::vector<ObservationLabel> observationLabels;
878
879 // A mapping from action names to their indices.
880 std::map<std::string, uint_fast64_t> actionToIndexMap;
881
882 // A mapping from action indices to their names.
883 std::map<uint_fast64_t, std::string> indexToActionMap;
884
885 // The set of actions present in this program.
886 std::set<std::string> actions;
887
888 // The set of synchronizing actions present in this program.
889 std::set<uint_fast64_t> synchronizingActionIndices;
890
891 // A map of actions to the set of modules containing commands labelled with this action.
892 std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToModuleIndexMap;
893
894 // A mapping from variable names to the modules in which they were declared.
895 std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
896
897 storage::BitVector possiblySynchronizingCommands;
898
899 bool prismCompatibility;
900};
901
902std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
903
904} // namespace prism
905} // namespace storm
906
907#endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */
This class is responsible for managing a set of typed variables and all expressions using these varia...
Program replaceConstantByVariable(Constant const &c, expressions::Expression const &lowerBound, expressions::Expression const &upperBound, bool observable=true) const
Substitutes the given constant by a fresh global variable that is bound between lowerBound and upperB...
Definition Program.cpp:1218
std::set< uint_fast64_t > const & getSynchronizingActionIndices() const
Retrieves the set of synchronizing action indices present in the program.
Definition Program.cpp:751
Program & operator=(Program &&other)=default
void checkValidity(Program::ValidityCheckLevel lvl=Program::ValidityCheckLevel::READYFORPROCESSING) const
Checks the validity of the program.
Definition Program.cpp:1239
std::map< std::string, std::string > getFinalRenamingOfModule(Module const &renamedModule) const
Gets the renaming of a module after flattening all renamings.
Definition Program.cpp:450
bool hasIntervalUpdates() const
Retrieves whether the program considers at least one update with an interval probability/rate.
Definition Program.cpp:710
ModelType getModelType() const
Retrieves the model type of the model.
Definition Program.cpp:247
Program defineUndefinedConstants(std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
Defines the undefined constants according to the given map and returns the resulting program.
Definition Program.cpp:997
std::vector< storm::expressions::Expression > getAllRangeExpressions() const
Retrieves a list of expressions that characterize the legal ranges of all variables.
Definition Program.cpp:512
std::vector< RewardModel > const & getRewardModels() const
Retrieves the reward models of the program.
Definition Program.cpp:821
std::vector< Player > const & getPlayers() const
Retrieves the players of the program.
Definition Program.cpp:562
RewardModel const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name.
Definition Program.cpp:829
std::vector< BooleanVariable > const & getGlobalBooleanVariables() const
Retrieves the global boolean variables of the program.
Definition Program.cpp:482
ModelType
An enum for the different model types.
Definition Program.h:36
std::set< std::string > const & getActions() const
Retrieves the set of actions present in the program.
Definition Program.cpp:747
std::set< uint_fast64_t > const & getModuleIndicesByAction(std::string const &action) const
Retrieves the indices of all modules within this program that contain commands that are labelled with...
Definition Program.cpp:775
std::vector< std::reference_wrapper< Constant const > > getUndefinedConstants() const
Retrieves the undefined constants in the program.
Definition Program.cpp:368
storm::storage::PlayerIndex const & getIndexOfPlayer(std::string const &playerName) const
Retrieves the index of the player in the program.
Definition Program.cpp:570
bool isPartiallyObservable() const
Retrieves whether the model has restricted observability.
Definition Program.cpp:259
std::pair< uint_fast64_t, uint_fast64_t > getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const
Retrieves the index of the module and the (local) index of the command with the given global command ...
Definition Program.cpp:795
bool hasAction(std::string const &actionName) const
Retrieves whether the program has an action with the given name.
Definition Program.cpp:767
std::size_t getNumberOfLabels() const
Retrieves the number of labels in the program.
Definition Program.cpp:875
boost::optional< SystemCompositionConstruct > getOptionalSystemCompositionConstruct() const
Retrieves the system composition construct (if any) and none otherwise.
Definition Program.cpp:731
std::map< storm::expressions::Variable, storm::expressions::Expression > getConstantsSubstitution() const
Retrieves a mapping of all defined constants to their defining expressions.
Definition Program.cpp:406
std::string const & getActionName(uint_fast64_t actionIndex) const
Retrieves the action name of the given action index.
Definition Program.cpp:755
std::vector< Module > const & getModules() const
Retrieves all modules of the program.
Definition Program.cpp:629
bool isDiscreteTimeModel() const
Retrieves whether the model is a discrete-time model, i.e.
Definition Program.cpp:251
storm::expressions::Expression const & getLabelExpression(std::string const &label) const
Retrieves the expression associated with the given label, if it exists.
Definition Program.cpp:860
std::unordered_map< uint_fast64_t, std::string > buildCommandIndexToActionNameMap() const
Definition Program.cpp:2254
Program substituteNonStandardPredicates() const
Substitutes all nonstandard predicates in expressions of the program by their defining expressions.
Definition Program.cpp:1047
Program & operator=(Program const &other)=default
std::vector< ObservationLabel > const & getObservationLabels() const
Retrieves all observation labels that are defined by this program.
Definition Program.cpp:913
Module const & getModule(uint_fast64_t index) const
Retrieves the module with the given index.
Definition Program.cpp:615
uint_fast64_t getActionIndex(std::string const &actionName) const
Retrieves the index of the action with the given name.
Definition Program.cpp:761
IntegerVariable const & getGlobalIntegerVariable(std::string const &variableName) const
Retrieves a the global integer variable with the given name.
Definition Program.cpp:543
std::set< uint_fast64_t > const & getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const
Retrieves the indices of all modules within this program that contain commands that are labelled with...
Definition Program.cpp:781
std::map< uint_fast64_t, storm::storage::PlayerIndex > buildActionIndexToPlayerIndexMap() const
Retrieves a vector whose i'th entry corresponds to the player controlling action with index i.
Definition Program.cpp:590
bool isDeterministicModel() const
Retrieves whether the model is one without nondeterministic choices, i.e.
Definition Program.cpp:255
std::map< storm::expressions::Variable, storm::expressions::Expression > getConstantsFormulasSubstitution(bool getConstantsSubstitution=true, bool getFormulasSubstitution=true) const
Retrieves a mapping of all defined constants and formula variables to their defining expressions.
Definition Program.cpp:414
std::vector< storm::expressions::Expression > getAllGuards(bool negated=false) const
Retrieves all guards appearing in the program.
Definition Program.cpp:850
void removeLabel(std::string const &name)
Removes the label with the given name from the program.
Definition Program.cpp:886
bool undefinedConstantsAreGraphPreserving() const
Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
Definition Program.cpp:294
std::size_t getNumberOfRewardModels() const
Retrieves the number of reward models in the program.
Definition Program.cpp:825
std::size_t getNumberOfPlayers() const
Retrieves the number of players in the program.
Definition Program.cpp:566
void updateInitialStatesExpression(expressions::Expression const &newExpression)
Sets a new initial states expression.
Definition Program.cpp:657
Constant const & getConstant(std::string const &constantName) const
Retrieves the constant with the given name if it exists.
Definition Program.cpp:397
std::map< std::string, uint_fast64_t > const & getActionNameToIndexMapping() const
Retrieves the mapping of action names to their indices.
Definition Program.cpp:633
size_t getNumberOfCommands() const
The total number of commands in the prism file.
Definition Program.cpp:263
Program labelUnlabelledCommands(std::map< uint64_t, std::string > const &nameSuggestions={}) const
Give commands that do not have an action name an action, which can be helpful for debugging and under...
Definition Program.cpp:1165
Program(Program const &other)=default
SystemCompositionConstruct const & getSystemCompositionConstruct() const
If the program specifies a system composition construct, this method retrieves it.
Definition Program.cpp:727
Program substituteConstants() const
Substitutes all constants appearing in the expressions of the program by their defining expressions.
Definition Program.cpp:1039
Program substituteFormulas() const
Substitutes all formulas appearing in the expressions of the program by their defining expressions.
Definition Program.cpp:1043
std::size_t getNumberOfObservationLabels() const
Retrieves the number of observation labels in the program.
Definition Program.cpp:917
std::map< std::string, storm::storage::PlayerIndex > const & getPlayerNameToIndexMapping() const
Definition Program.cpp:574
std::size_t getNumberOfConstants() const
Retrieves the number of all constants defined in the program.
Definition Program.cpp:478
std::set< storm::expressions::Variable > getAllExpressionVariables(bool includeConstants=true) const
Retrieves all expression variables used by this program.
Definition Program.cpp:490
Program(Program &&other)=default
bool globalIntegerVariableExists(std::string const &variableName) const
Retrieves whether a global Integer variable with the given name exists.
Definition Program.cpp:532
std::unordered_map< uint_fast64_t, std::string > buildActionIndexToActionNameMap() const
Definition Program.cpp:2264
BooleanVariable const & getGlobalBooleanVariable(std::string const &variableName) const
Retrieves a the global boolean variable with the given name.
Definition Program.cpp:536
void filterLabels(std::set< std::string > const &labelSet)
Removes all labels that are not contained in the given set from the program.
Definition Program.cpp:897
bool hasModule(std::string const &moduleName) const
Retrieves whether the program has a module with the given name.
Definition Program.cpp:619
Program substituteConstantsFormulas(bool substituteConstants=true, bool substituteFormulas=true) const
Substitutes all constants and/or formulas appearing in the expressions of the program by their defini...
Definition Program.cpp:1091
bool globalBooleanVariableExists(std::string const &variableName) const
Retrieves whether a global Boolean variable with the given name exists.
Definition Program.cpp:528
std::unordered_map< uint_fast64_t, uint_fast64_t > buildCommandIndexToActionIndex() const
Definition Program.cpp:2272
std::vector< Constant > const & getConstants() const
Retrieves all constants defined in the program.
Definition Program.cpp:402
std::map< storm::expressions::Variable, storm::expressions::Expression > getFormulasSubstitution() const
Retrieves a mapping of all formula variables to their defining expressions.
Definition Program.cpp:410
friend std::ostream & operator<<(std::ostream &stream, Program const &program)
Definition Program.cpp:2424
bool hasUnboundedVariables() const
Definition Program.cpp:271
storm::expressions::ExpressionManager & getManager() const
Retrieves the manager responsible for the expressions of this program.
Definition Program.cpp:2378
Program replaceVariableInitializationByInitExpression() const
Replace the initialization in variables by an init-expression.
Definition Program.cpp:1197
std::vector< Constant > usedConstants() const
Retrieves the constants that are actually used in the program.
Definition Program.cpp:2184
bool hasLabel(std::string const &labelName) const
Checks whether the program has a label with the given name.
Definition Program.cpp:841
std::vector< storm::storage::PlayerIndex > buildModuleIndexToPlayerIndexMap() const
Retrieves a vector whose i'th entry corresponds to the player controlling module i.
Definition Program.cpp:578
std::vector< IntegerVariable > const & getGlobalIntegerVariables() const
Retrieves the global integer variables of the program.
Definition Program.cpp:486
std::size_t getNumberOfGlobalIntegerVariables() const
Retrieves the number of global integer variables of the program.
Definition Program.cpp:554
std::string getUndefinedConstantsAsString() const
Retrieves the undefined constants in the program as a comma-separated string.
Definition Program.cpp:378
std::size_t getNumberOfFormulas() const
Retrieves the number of formulas in the program.
Definition Program.cpp:607
bool hasConstant(std::string const &constantName) const
Retrieves whether the given constant exists in the program.
Definition Program.cpp:393
storm::expressions::Expression getInitialStatesExpression() const
Retrieves an expression characterizing the initial states.
Definition Program.cpp:662
void addLabel(std::string const &name, storm::expressions::Expression const &statePredicateExpression)
Adds a label with the given name and defining expression to the program.
Definition Program.cpp:879
std::size_t getNumberOfModules() const
Retrieves the number of modules in the program.
Definition Program.cpp:611
bool hasInitialConstruct() const
Retrieves whether the program specifies an initial construct.
Definition Program.cpp:645
Program restrictCommands(storm::storage::FlatSet< uint_fast64_t > const &indexSet) const
Creates a new program that drops all commands whose indices are not in the given set.
Definition Program.cpp:925
Program flattenModules(std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::shared_ptr< storm::utility::solver::SmtSolverFactory >(new storm::utility::solver::SmtSolverFactory())) const
Creates an equivalent program that contains exactly one module.
Definition Program.cpp:1970
bool hasUndefinedConstants() const
Retrieves whether there are undefined constants of any type in the program.
Definition Program.cpp:285
bool specifiesSystemComposition() const
Retrieves whether the program specifies a system composition in terms of process algebra operations o...
Definition Program.cpp:723
std::shared_ptr< Composition > getDefaultSystemComposition() const
Retrieves the default system composition for this program.
Definition Program.cpp:735
std::vector< Label > const & getLabels() const
Retrieves all labels that are defined by the probabilitic program.
Definition Program.cpp:846
uint64_t getNumberOfUnlabeledCommands() const
Definition Program.cpp:637
storm::storage::BitVector const & getPossiblySynchronizingCommands() const
Compute the (labelled) commands in the program that may be synchronizing.
Definition Program.cpp:921
uint_fast64_t getModuleIndexByVariable(std::string const &variableName) const
Retrieves the index of the module in which the given variable name was declared.
Definition Program.cpp:788
bool hasRewardModel() const
Retrieves whether the program has reward models.
Definition Program.cpp:812
std::map< std::string, storm::expressions::Expression > getLabelToExpressionMapping() const
Retrieves a mapping from all labels in the program to their defining expressions.
Definition Program.cpp:867
Program simplify()
Entry point for static analysis for simplify.
Definition Program.cpp:1822
std::map< storm::expressions::Variable, storm::expressions::Expression > getSubstitutionForRenamedModule(Module const &renamedModule, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Applies the renaming of a renamed module to the given substitution.
Definition Program.cpp:432
std::size_t getNumberOfGlobalBooleanVariables() const
Retrieves the number of global boolean variables of the program.
Definition Program.cpp:550
storm::jani::Model toJani(bool allVariablesGlobal=true, std::string suffix="") const
Converts the PRISM model into an equivalent JANI model.
Definition Program.cpp:2340
std::vector< Formula > const & getFormulas() const
Retrieves the formulas defined in the program.
Definition Program.cpp:558
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
uint64_t PlayerIndex
Definition PlayerIndex.h:7
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
LabParser.cpp.