Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BisimulationDecomposition.cpp
Go to the documentation of this file.
2
3#include <chrono>
4
9
12
17
20
23
25
28
29namespace storm {
30namespace storage {
31
32using namespace bisimulation;
33
34template<typename ModelType, typename BlockDataType>
36 this->preserveSingleFormula(model, formula);
37}
38
39template<typename ModelType, typename BlockDataType>
41 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas)
42 : Options() {
43 if (formulas.empty()) {
44 this->respectedAtomicPropositions = model.getStateLabeling().getLabels();
45 this->keepRewards = true;
46 }
47 if (formulas.size() == 1) {
48 this->preserveSingleFormula(model, *formulas.front());
49 } else {
50 for (auto const& formula : formulas) {
51 preserveFormula(*formula);
52 }
53 }
54}
55
56template<typename ModelType, typename BlockDataType>
58 : measureDrivenInitialPartition(false),
59 phiStates(),
60 psiStates(),
61 respectedAtomicPropositions(),
62 buildQuotient(true),
63 keepRewards(false),
65 bounded(false),
66 discounted(false) {
67 // Intentionally left empty.
68}
69
70template<typename ModelType, typename BlockDataType>
72 // Disable the measure driven initial partition.
73 measureDrivenInitialPartition = false;
74 phiStates = boost::none;
75 psiStates = boost::none;
76
77 // Retrieve information about formula.
79
80 // Preserve rewards if necessary.
81 keepRewards = keepRewards || info.containsRewardOperator() || info.containsRewardBoundedFormula();
82
83 // Preserve bounded properties if necessary.
84 bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula() || info.containsCumulativeRewardFormula());
85
86 // Preserve discounted properties if necessary.
87 discounted = discounted || info.containsDiscountFormula();
88
89 // Compute the relevant labels and expressions.
90 this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
91}
92
93template<typename ModelType, typename BlockDataType>
95 // Retrieve information about formula.
97
98 keepRewards = info.containsRewardOperator() || info.containsRewardBoundedFormula();
99
100 // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
102
103 // We need to preserve discounting iff the formula contains a discounted subformula
104 discounted = info.containsDiscountFormula();
105
106 // Compute the relevant labels and expressions.
107 this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
108
109 // Check whether measure driven initial partition is possible and, if so, set it.
110 this->checkAndSetMeasureDrivenInitialPartition(model, formula);
111}
112
113template<typename ModelType, typename BlockDataType>
115 storm::logic::Formula const& formula) {
116 std::shared_ptr<storm::logic::Formula const> newFormula = formula.asSharedPointer();
117
118 if (formula.isProbabilityOperatorFormula()) {
120 optimalityType = formula.asProbabilityOperatorFormula().getOptimalityType();
121 } else if (formula.asProbabilityOperatorFormula().hasBound()) {
123 if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
124 optimalityType = OptimizationDirection::Maximize;
125 } else {
126 optimalityType = OptimizationDirection::Minimize;
127 }
128 }
130 } else if (formula.isRewardOperatorFormula()) {
132 optimalityType = formula.asRewardOperatorFormula().getOptimalityType();
133 } else if (formula.asRewardOperatorFormula().hasBound()) {
135 if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
136 optimalityType = OptimizationDirection::Maximize;
137 } else {
138 optimalityType = OptimizationDirection::Minimize;
139 }
140 }
141 newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer();
142 }
143
144 std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
145 std::shared_ptr<storm::logic::Formula const> rightSubformula;
146 if (newFormula->isUntilFormula()) {
147 leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
148 rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
149 if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) {
150 measureDrivenInitialPartition = true;
151 }
152 } else if (newFormula->isEventuallyFormula()) {
153 rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
154 if (rightSubformula->isInFragment(storm::logic::propositional())) {
155 measureDrivenInitialPartition = true;
156 }
157 }
158
159 if (measureDrivenInitialPartition) {
161 std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
162 std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
163 phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
164 psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
165 } else {
166 optimalityType = boost::none;
167 }
168}
169
170template<typename ModelType, typename BlockDataType>
171void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespectedAtomicPropositions(
172 std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions,
173 std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels) {
174 std::set<std::string> labelsToRespect;
175 for (auto const& labelFormula : labels) {
176 labelsToRespect.insert(labelFormula->getLabel());
177 }
178 for (auto const& expressionFormula : expressions) {
179 labelsToRespect.insert(expressionFormula->toString());
180 }
181 if (!respectedAtomicPropositions) {
182 respectedAtomicPropositions = labelsToRespect;
183 } else {
184 respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
185 }
186}
187
188template<typename ModelType, typename BlockDataType>
190 : BisimulationDecomposition(model, model.getBackwardTransitions(), options) {
191 // Intentionally left empty.
193
194template<typename ModelType, typename BlockDataType>
196 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
197 Options const& options)
198 : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
199 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException,
200 "Bisimulation currently only supports models with at most one reward model.");
201 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || !model.getUniqueRewardModel().hasTransitionRewards(),
202 storm::exceptions::IllegalFunctionCallException,
203 "Bisimulation is currently supported for models with state or action rewards only. Consider converting the transition rewards to state "
204 "rewards (via suitable function calls).");
205 STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException,
206 "Weak bisimulation cannot preserve bounded properties.");
207 STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getDiscounted(), storm::exceptions::IllegalFunctionCallException,
208 "Weak bisimulation cannot preserve discounted properties.");
209
210 // Fix the respected atomic propositions if they were not explicitly given.
211 if (!this->options.respectedAtomicPropositions) {
212 this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels();
213 }
214}
215
216template<typename ModelType, typename BlockDataType>
218 std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
219
220 std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now();
221 // initialize the initial partition.
222 if (options.measureDrivenInitialPartition) {
223 STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states.");
224 STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states.");
225 this->initializeMeasureDrivenPartition();
226 } else {
227 this->initializeLabelBasedPartition();
228 }
229 STORM_LOG_WARN_COND(partition.size() > 1, "Initial partition consists only of a single block.");
230 std::chrono::high_resolution_clock::duration initialPartitionTime = std::chrono::high_resolution_clock::now() - initialPartitionStart;
231
232 this->initialize();
233
234 std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
235 this->performPartitionRefinement();
236 std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
237
238 std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
239 this->extractDecompositionBlocks();
240 std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
241
242 std::chrono::high_resolution_clock::time_point quotientBuildStart = std::chrono::high_resolution_clock::now();
243 if (options.buildQuotient) {
244 this->buildQuotient();
246 std::chrono::high_resolution_clock::duration quotientBuildTime = std::chrono::high_resolution_clock::now() - quotientBuildStart;
247
248 std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
249
250 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
251 std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime);
252 std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime);
253 std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime);
254 std::chrono::milliseconds quotientBuildTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(quotientBuildTime);
255 std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
256 std::cout << "\nTime breakdown:\n";
257 std::cout << " * time for initial partition: " << initialPartitionTimeInMilliseconds.count() << "ms\n";
258 std::cout << " * time for partitioning: " << refinementTimeInMilliseconds.count() << "ms\n";
259 std::cout << " * time for extraction: " << extractionTimeInMilliseconds.count() << "ms\n";
260 std::cout << " * time for building quotient: " << quotientBuildTimeInMilliseconds.count() << "ms\n";
261 std::cout << "------------------------------------------\n";
262 std::cout << " * total time: " << totalTimeInMilliseconds.count() << "ms\n\n";
263 }
264}
265
266template<typename ModelType, typename BlockDataType>
268 // Insert all blocks into the splitter queue as a (potential) splitter.
269 std::vector<Block<BlockDataType>*> splitterQueue;
270 std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&](std::unique_ptr<Block<BlockDataType>> const& block) {
271 block->data().setSplitter();
272 splitterQueue.push_back(block.get());
273 });
274
275 // Then perform the actual splitting until there are no more splitters.
276 uint_fast64_t iterations = 0;
277 while (!splitterQueue.empty()) {
278 ++iterations;
279
280 // Get and prepare the next splitter.
281 // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but
282 // tends to work well.
283 std::sort(splitterQueue.begin(), splitterQueue.end(),
284 [](Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); });
285 Block<BlockDataType>* splitter = splitterQueue.back();
286 splitterQueue.pop_back();
287 splitter->data().setSplitter(false);
288
289 // Now refine the partition using the current splitter.
290 refinePartitionBasedOnSplitter(*splitter, splitterQueue);
291
293 std::cout << "Performed " << iterations << " iterations of partition refinement before abort.\n";
294 STORM_LOG_THROW(false, storm::exceptions::AbortException, "Aborted in bisimulation computation.");
295 break;
296 }
297 }
298}
299
300template<typename ModelType, typename BlockDataType>
302 STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException,
303 "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
304 return this->quotient;
305}
306
307template<typename ModelType, typename BlockDataType>
309 auto const& rewardModel = model.getUniqueRewardModel();
310 if (rewardModel.hasStateRewards()) {
311 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateRewardVector());
312 }
313 if (rewardModel.hasStateActionRewards()) {
314 if (model.isNondeterministicModel()) {
315 std::vector<std::set<ValueType>> actionRewards;
316 actionRewards.reserve(model.getNumberOfStates());
317 for (storm::storage::sparse::state_type state = 0; state < model.getNumberOfStates(); ++state) {
318 std::set<ValueType> rewardsAtState;
319 for (auto choice = model.getTransitionMatrix().getRowGroupIndices()[state];
320 choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
321 rewardsAtState.insert(rewardModel.getStateActionReward(choice));
322 }
323 actionRewards.push_back(std::move(rewardsAtState));
324 }
325 this->splitInitialPartitionBasedOnActionRewards(actionRewards);
326 } else {
327 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateActionRewardVector());
328 }
329 }
330}
331
332template<typename ModelType, typename BlockDataType>
334 partition.split([&rewardVector](storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) {
335 return rewardVector[a] < rewardVector[b];
336 });
337}
338
339template<typename ModelType, typename BlockDataType>
341 partition.split([&actionRewards](storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) {
342 return actionRewards[a] < actionRewards[b];
343 });
344}
345
346template<typename ModelType, typename BlockDataType>
348 partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates());
349
350 for (auto const& label : options.respectedAtomicPropositions.get()) {
351 if (label == "init") {
352 continue;
353 }
354 partition.splitStates(model.getStates(label));
355 }
356
357 // If the model has state rewards, we need to consider them, because otherwise reward properties are not
358 // preserved.
359 if (options.getKeepRewards() && model.hasRewardModel()) {
360 this->splitInitialPartitionBasedOnRewards();
361 }
362}
363
364template<typename ModelType, typename BlockDataType>
366 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
367
368 boost::optional<storm::storage::sparse::state_type> representativePsiState;
369 if (!options.psiStates.get().empty()) {
370 representativePsiState = *options.psiStates.get().begin();
371 }
372
374 model.getNumberOfStates(), statesWithProbability01.first,
375 options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
376
377 // If the model has state rewards, we need to consider them, because otherwise reward properties are not
378 // preserved.
379 if (options.getKeepRewards() && model.hasRewardModel()) {
380 this->splitInitialPartitionBasedOnRewards();
381 }
382}
383
384template<typename ModelType, typename BlockDataType>
386 // Intentionally left empty.
387}
388
389template<typename ModelType, typename BlockDataType>
391 // Now move the states from the internal partition into their final place in the decomposition. We do so in
392 // a way that maintains the block IDs as indices.
393 this->blocks.resize(partition.size());
394 for (auto const& blockPtr : partition.getBlocks()) {
395 // We need to sort the states to allow for rapid construction of the blocks.
396 partition.sortBlock(*blockPtr);
397
398 // Convert the state-value-pairs to states only.
399 this->blocks[blockPtr->getId()] = block_type(partition.begin(*blockPtr), partition.end(*blockPtr), true);
400 }
401}
402
406
407#ifdef STORM_HAVE_CARL
411
415#endif
416} // namespace storage
417} // namespace storm
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:484
std::vector< std::shared_ptr< AtomicExpressionFormula const > > getAtomicExpressionFormulas() const
Definition Formula.cpp:500
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:180
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
std::vector< std::shared_ptr< AtomicLabelFormula const > > getAtomicLabelFormulas() const
Definition Formula.cpp:506
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:184
std::shared_ptr< Formula const > asSharedPointer()
Definition Formula.cpp:571
FormulaInformation info(bool recurseIntoOperators=true) const
Definition Formula.cpp:209
ComparisonType getComparisonType() const
storm::solver::OptimizationDirection const & getOptimalityType() const
Formula const & getSubformula() const
This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
virtual void buildQuotient()=0
Builds the quotient model based on the previously computed equivalence classes (stored in the blocks ...
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.
BisimulationDecomposition(ModelType const &model, Options const &options)
Decomposes the given model into equivalance classes of a bisimulation.
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 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.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
FragmentSpecification propositional()
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
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
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...