Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
CounterexampleGeneratorSettings.h
Go to the documentation of this file.
1#ifndef STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_
2#define STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_
3
5
6namespace storm {
7namespace settings {
8namespace modules {
9
14 public:
19
25 bool isCounterexampleSet() const;
26
32 bool isCounterexampleTypeSet() const;
33
40
46 bool isShortestPathGenerationSet() const;
47
53 size_t getShortestPathMaxK() const;
54
62
70
77 bool isEncodeReachabilitySet() const;
78
85 bool isUseSchedulerCutsSet() const;
86
92 bool isUseDynamicConstraintsSet() const;
93
94 bool check() const override;
95
96 // The name of the module.
97 static const std::string moduleName;
98
99 private:
100 // Define the string names of the options as constants.
101 static const std::string counterexampleOptionName;
102 static const std::string counterexampleOptionShortName;
103 static const std::string counterexampleTypeOptionName;
104 static const std::string shortestPathMaxKOptionName;
105 static const std::string minimalCommandMethodOptionName;
106 static const std::string encodeReachabilityOptionName;
107 static const std::string schedulerCutsOptionName;
108 static const std::string noDynamicConstraintsOptionName;
109};
110
111} // namespace modules
112} // namespace settings
113} // namespace storm
114
115#endif /* STORM_SETTINGS_MODULES_COUNTEREXAMPLEGENERATORSETTINGS_H_ */
This class represents the settings for counterexample generation.
bool isCounterexampleSet() const
Retrieves whether the counterexample option was set.
CounterexampleGeneratorSettings()
Creates a new set of counterexample settings.
bool isShortestPathGenerationSet() const
Retrieves whether the option to generate a shortest path counterexample was set.
bool isUseMaxSatBasedMinimalCommandSetGenerationSet() const
Retrieves whether the MAXSAT-based technique is to be used to generate a minimal command set countere...
bool check() const override
Checks whether the settings are consistent.
size_t getShortestPathMaxK() const
Retrieves the maximal number K of shortest paths which should be generated.
bool isUseDynamicConstraintsSet() const
Retrieves whether to use the dynamic constraints in the MAXSAT-based technique.
bool isUseSchedulerCutsSet() const
Retrieves whether scheduler cuts are to be used if the MAXSAT-based technique is used to generate a m...
bool isEncodeReachabilitySet() const
Retrieves whether reachability of a target state is to be encoded if the MAXSAT-based technique is us...
bool isCounterexampleTypeSet() const
Retrieves whether the type of counterexample was set.
bool isMinimalCommandSetGenerationSet() const
Retrieves whether the option to generate a minimal command set counterexample was set.
bool isUseMilpBasedMinimalCommandSetGenerationSet() const
Retrieves whether the MILP-based technique is to be used to generate a minimal command set counterexa...
This is the base class of the settings for a particular module.
LabParser.cpp.
Definition cli.cpp:18