Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BisimulationDecomposition.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
2#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
3
12
14
17
18namespace storm {
19namespace logic {
20class Formula;
21}
22
23namespace storage {
24
26 switch (c) {
32 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
34 } else {
36 }
37 }
39}
40
44template<typename ModelType, typename BlockDataType>
45class BisimulationDecomposition : public Decomposition<StateBlock> {
46 public:
47 typedef typename ModelType::ValueType ValueType;
48 typedef typename ModelType::RewardModelType RewardModelType;
49
50 // A class that offers the possibility to customize the bisimulation.
51 struct Options {
52 // Creates an object representing the default values for all options.
53 Options();
54
63 Options(ModelType const& model, storm::logic::Formula const& formula);
64
73 Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
74
80 void preserveFormula(storm::logic::Formula const& formula);
81
88 if (t == BisimulationType::Weak) {
89 STORM_LOG_WARN_COND(!bounded, "Weak bisimulation does not preserve bounded properties.");
90 STORM_LOG_WARN_COND(!discounted, "Weak bisimulation does not preserve discounted properties.");
91 bounded = false;
92 discounted = false;
93 }
94 type = t;
95 }
96
98 return this->type;
99 }
100
101 bool getBounded() const {
102 return this->bounded;
103 }
104
105 bool getDiscounted() const {
106 return this->discounted;
107 }
108
109 bool getKeepRewards() const {
110 return this->keepRewards;
111 }
112
113 void setKeepRewards(bool keepRewards) {
114 this->keepRewards = keepRewards;
115 }
116
118 return static_cast<bool>(optimalityType);
119 }
120
122 STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
123 return optimalityType.get();
124 }
125
126 // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
127 // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
128 // measure driven initial partition wrt. to the states phi and psi is taken.
130 boost::optional<storm::storage::BitVector> phiStates;
131 boost::optional<storm::storage::BitVector> psiStates;
132
135 boost::optional<std::set<std::string>> respectedAtomicPropositions;
136
139
140 private:
141 boost::optional<OptimizationDirection> optimalityType;
142
145 bool keepRewards;
146
148 BisimulationType type;
149
152 bool bounded;
153
156 bool discounted;
157
164 void preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula);
165
172 void addToRespectedAtomicPropositions(std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions,
173 std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels);
174
175 /*
176 * Checks whether a measure driven partition is possible with the given formula and sets the necessary
177 * data if this is the case.
178 *
179 * @param model The model for which to derive the data.
180 * @param formula The formula for which to derive the data for the measure driven initial partition (if
181 * applicable).
182 */
183 void checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula);
184 };
185
192 BisimulationDecomposition(ModelType const& model, Options const& options);
193
194 virtual ~BisimulationDecomposition() = default;
195
201 std::shared_ptr<ModelType> getQuotient() const;
202
208
209 protected:
218
225
234 std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0;
235
240 virtual void buildQuotient() = 0;
241
245 virtual void initializeLabelBasedPartition();
246
251
255 virtual void initialize();
256
263 virtual std::pair<storm::storage::BitVector, storm::storage::BitVector> getStatesWithProbability01() = 0;
264
269
273 virtual void splitInitialPartitionBasedOnRewards(std::vector<ValueType> const& rewardVector);
274
278 virtual void splitInitialPartitionBasedOnActionRewards(std::vector<std::set<ValueType>> const& rewardVector);
279
284
285 // The model to decompose.
286 ModelType const& model;
287
288 // The backward transitions of the model.
290
291 // The options used during construction.
293
294 // The current partition (used by partition refinement).
296
297 // A comparator used for comparing the distances of constants.
299
300 // The quotient, if it was build. Otherwhise a null pointer.
301 std::shared_ptr<ModelType> quotient;
302};
303} // namespace storage
304} // namespace storm
305
306#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */
This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
storm::storage::SparseMatrix< ValueType > backwardTransitions
virtual void buildQuotient()=0
Builds the quotient model based on the previously computed equivalence classes (stored in the blocks ...
virtual void refinePartitionBasedOnSplitter(bisimulation::Block< BlockDataType > &splitter, std::vector< bisimulation::Block< BlockDataType > * > &splitterQueue)=0
Refines the partition by considering the given splitter.
storm::utility::ConstantsComparator< ValueType > comparator
std::shared_ptr< ModelType > getQuotient() const
Retrieves the quotient of the model under the computed bisimulation.
void performPartitionRefinement()
Performs the partition refinement on the model and thereby computes the equivalence classes under str...
virtual void splitInitialPartitionBasedOnRewards()
Splits the initial partition based on the (unique) reward model of the current model.
virtual void splitInitialPartitionBasedOnActionRewards(std::vector< std::set< ValueType > > const &rewardVector)
Splits the initial partition based on the given vector of action rewards.
storm::storage::bisimulation::Partition< BlockDataType > partition
void computeBisimulationDecomposition()
Computes the decomposition of the model into bisimulation equivalence classes.
void extractDecompositionBlocks()
Constructs the blocks of the decomposition object based on the current partition.
virtual std::pair< storm::storage::BitVector, storm::storage::BitVector > getStatesWithProbability01()=0
Computes the set of states with probability 0/1 for satisfying phi until psi.
virtual void initializeMeasureDrivenPartition()
Creates the measure-driven initial partition for reaching psi states from phi states.
virtual void initializeLabelBasedPartition()
Initializes the initial partition based on all respected labels.
virtual void initialize()
A function that can initialize auxiliary data structures.
This class represents the decomposition of a model into blocks which are of the template type.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
BisimulationType resolveBisimulationTypeChoice(BisimulationTypeChoice c)
LabParser.cpp.
void preserveFormula(storm::logic::Formula const &formula)
Changes the options in a way that the given formula is preserved.
boost::optional< storm::storage::BitVector > psiStates
boost::optional< storm::storage::BitVector > phiStates
void setType(BisimulationType t)
Sets the bisimulation type.
boost::optional< std::set< std::string > > respectedAtomicPropositions
An optional set of strings that indicate which of the atomic propositions of the model are to be resp...
bool buildQuotient
A flag that governs whether the quotient model is actually built or only the decomposition is compute...