Storm 1.10.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 // Intentionally left empty.
67}
68
69template<typename ModelType, typename BlockDataType>
71 // Disable the measure driven initial partition.
72 measureDrivenInitialPartition = false;
73 phiStates = boost::none;
74 psiStates = boost::none;
75
76 // Retrieve information about formula.
78
79 // Preserve rewards if necessary.
80 keepRewards = keepRewards || info.containsRewardOperator() || info.containsRewardBoundedFormula();
81
82 // Preserve bounded properties if necessary.
83 bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula() || info.containsCumulativeRewardFormula());
84
85 // Compute the relevant labels and expressions.
86 this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
87}
88
89template<typename ModelType, typename BlockDataType>
91 // Retrieve information about formula.
93
94 keepRewards = info.containsRewardOperator() || info.containsRewardBoundedFormula();
95
96 // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
98
99 // Compute the relevant labels and expressions.
100 this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
101
102 // Check whether measure driven initial partition is possible and, if so, set it.
103 this->checkAndSetMeasureDrivenInitialPartition(model, formula);
104}
105
106template<typename ModelType, typename BlockDataType>
108 storm::logic::Formula const& formula) {
109 std::shared_ptr<storm::logic::Formula const> newFormula = formula.asSharedPointer();
110
111 if (formula.isProbabilityOperatorFormula()) {
113 optimalityType = formula.asProbabilityOperatorFormula().getOptimalityType();
114 } else if (formula.asProbabilityOperatorFormula().hasBound()) {
116 if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
117 optimalityType = OptimizationDirection::Maximize;
118 } else {
119 optimalityType = OptimizationDirection::Minimize;
120 }
121 }
123 } else if (formula.isRewardOperatorFormula()) {
125 optimalityType = formula.asRewardOperatorFormula().getOptimalityType();
126 } else if (formula.asRewardOperatorFormula().hasBound()) {
128 if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
129 optimalityType = OptimizationDirection::Maximize;
130 } else {
131 optimalityType = OptimizationDirection::Minimize;
132 }
133 }
134 newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer();
135 }
136
137 std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
138 std::shared_ptr<storm::logic::Formula const> rightSubformula;
139 if (newFormula->isUntilFormula()) {
140 leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
141 rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
142 if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) {
143 measureDrivenInitialPartition = true;
144 }
145 } else if (newFormula->isEventuallyFormula()) {
146 rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
147 if (rightSubformula->isInFragment(storm::logic::propositional())) {
148 measureDrivenInitialPartition = true;
149 }
150 }
151
152 if (measureDrivenInitialPartition) {
154 std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
155 std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
156 phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
157 psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
158 } else {
159 optimalityType = boost::none;
160 }
161}
162
163template<typename ModelType, typename BlockDataType>
164void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespectedAtomicPropositions(
165 std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions,
166 std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels) {
167 std::set<std::string> labelsToRespect;
168 for (auto const& labelFormula : labels) {
169 labelsToRespect.insert(labelFormula->getLabel());
170 }
171 for (auto const& expressionFormula : expressions) {
172 labelsToRespect.insert(expressionFormula->toString());
173 }
174 if (!respectedAtomicPropositions) {
175 respectedAtomicPropositions = labelsToRespect;
176 } else {
177 respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
178 }
179}
180
181template<typename ModelType, typename BlockDataType>
183 : BisimulationDecomposition(model, model.getBackwardTransitions(), options) {
184 // Intentionally left empty.
185}
186
187template<typename ModelType, typename BlockDataType>
189 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
190 Options const& options)
191 : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
192 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException,
193 "Bisimulation currently only supports models with at most one reward model.");
194 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || !model.getUniqueRewardModel().hasTransitionRewards(),
195 storm::exceptions::IllegalFunctionCallException,
196 "Bisimulation is currently supported for models with state or action rewards only. Consider converting the transition rewards to state "
197 "rewards (via suitable function calls).");
198 STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException,
199 "Weak bisimulation cannot preserve bounded properties.");
200
201 // Fix the respected atomic propositions if they were not explicitly given.
202 if (!this->options.respectedAtomicPropositions) {
203 this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels();
204 }
205}
207template<typename ModelType, typename BlockDataType>
209 std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
210
211 std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now();
212 // initialize the initial partition.
213 if (options.measureDrivenInitialPartition) {
214 STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi states.");
215 STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without psi states.");
216 this->initializeMeasureDrivenPartition();
217 } else {
218 this->initializeLabelBasedPartition();
219 }
220 STORM_LOG_WARN_COND(partition.size() > 1, "Initial partition consists only of a single block.");
221 std::chrono::high_resolution_clock::duration initialPartitionTime = std::chrono::high_resolution_clock::now() - initialPartitionStart;
222
223 this->initialize();
224
225 std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
226 this->performPartitionRefinement();
227 std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
228
229 std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
230 this->extractDecompositionBlocks();
231 std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
232
233 std::chrono::high_resolution_clock::time_point quotientBuildStart = std::chrono::high_resolution_clock::now();
234 if (options.buildQuotient) {
235 this->buildQuotient();
236 }
237 std::chrono::high_resolution_clock::duration quotientBuildTime = std::chrono::high_resolution_clock::now() - quotientBuildStart;
238
239 std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
240
242 std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime);
243 std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime);
244 std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime);
245 std::chrono::milliseconds quotientBuildTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(quotientBuildTime);
246 std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
247 std::cout << "\nTime breakdown:\n";
248 std::cout << " * time for initial partition: " << initialPartitionTimeInMilliseconds.count() << "ms\n";
249 std::cout << " * time for partitioning: " << refinementTimeInMilliseconds.count() << "ms\n";
250 std::cout << " * time for extraction: " << extractionTimeInMilliseconds.count() << "ms\n";
251 std::cout << " * time for building quotient: " << quotientBuildTimeInMilliseconds.count() << "ms\n";
252 std::cout << "------------------------------------------\n";
253 std::cout << " * total time: " << totalTimeInMilliseconds.count() << "ms\n\n";
254 }
255}
256
257template<typename ModelType, typename BlockDataType>
259 // Insert all blocks into the splitter queue as a (potential) splitter.
260 std::vector<Block<BlockDataType>*> splitterQueue;
261 std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&](std::unique_ptr<Block<BlockDataType>> const& block) {
262 block->data().setSplitter();
263 splitterQueue.push_back(block.get());
264 });
265
266 // Then perform the actual splitting until there are no more splitters.
267 uint_fast64_t iterations = 0;
268 while (!splitterQueue.empty()) {
269 ++iterations;
270
271 // Get and prepare the next splitter.
272 // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but
273 // tends to work well.
274 std::sort(splitterQueue.begin(), splitterQueue.end(),
275 [](Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); });
276 Block<BlockDataType>* splitter = splitterQueue.back();
277 splitterQueue.pop_back();
278 splitter->data().setSplitter(false);
279
280 // Now refine the partition using the current splitter.
281 refinePartitionBasedOnSplitter(*splitter, splitterQueue);
282
284 std::cout << "Performed " << iterations << " iterations of partition refinement before abort.\n";
285 STORM_LOG_THROW(false, storm::exceptions::AbortException, "Aborted in bisimulation computation.");
286 break;
287 }
288 }
289}
290
291template<typename ModelType, typename BlockDataType>
293 STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException,
294 "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
295 return this->quotient;
296}
297
298template<typename ModelType, typename BlockDataType>
300 auto const& rewardModel = model.getUniqueRewardModel();
301 if (rewardModel.hasStateRewards()) {
302 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateRewardVector());
303 }
304 if (rewardModel.hasStateActionRewards()) {
305 if (model.isNondeterministicModel()) {
306 std::vector<std::set<ValueType>> actionRewards;
307 actionRewards.reserve(model.getNumberOfStates());
308 for (storm::storage::sparse::state_type state = 0; state < model.getNumberOfStates(); ++state) {
309 std::set<ValueType> rewardsAtState;
310 for (auto choice = model.getTransitionMatrix().getRowGroupIndices()[state];
311 choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
312 rewardsAtState.insert(rewardModel.getStateActionReward(choice));
313 }
314 actionRewards.push_back(std::move(rewardsAtState));
315 }
316 this->splitInitialPartitionBasedOnActionRewards(actionRewards);
317 } else {
318 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateActionRewardVector());
319 }
320 }
321}
322
323template<typename ModelType, typename BlockDataType>
325 partition.split([&rewardVector](storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) {
326 return rewardVector[a] < rewardVector[b];
327 });
328}
329
330template<typename ModelType, typename BlockDataType>
332 partition.split([&actionRewards](storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) {
333 return actionRewards[a] < actionRewards[b];
334 });
335}
336
337template<typename ModelType, typename BlockDataType>
339 partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates());
340
341 for (auto const& label : options.respectedAtomicPropositions.get()) {
342 if (label == "init") {
343 continue;
344 }
345 partition.splitStates(model.getStates(label));
346 }
347
348 // If the model has state rewards, we need to consider them, because otherwise reward properties are not
349 // preserved.
350 if (options.getKeepRewards() && model.hasRewardModel()) {
351 this->splitInitialPartitionBasedOnRewards();
352 }
353}
354
355template<typename ModelType, typename BlockDataType>
357 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
358
359 boost::optional<storm::storage::sparse::state_type> representativePsiState;
360 if (!options.psiStates.get().empty()) {
361 representativePsiState = *options.psiStates.get().begin();
362 }
363
365 model.getNumberOfStates(), statesWithProbability01.first,
366 options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
367
368 // If the model has state rewards, we need to consider them, because otherwise reward properties are not
369 // preserved.
370 if (options.getKeepRewards() && model.hasRewardModel()) {
371 this->splitInitialPartitionBasedOnRewards();
372 }
373}
374
375template<typename ModelType, typename BlockDataType>
377 // Intentionally left empty.
378}
379
380template<typename ModelType, typename BlockDataType>
382 // Now move the states from the internal partition into their final place in the decomposition. We do so in
383 // a way that maintains the block IDs as indices.
384 this->blocks.resize(partition.size());
385 for (auto const& blockPtr : partition.getBlocks()) {
386 // We need to sort the states to allow for rapid construction of the blocks.
387 partition.sortBlock(*blockPtr);
388
389 // Convert the state-value-pairs to states only.
390 this->blocks[blockPtr->getId()] = block_type(partition.begin(*blockPtr), partition.end(*blockPtr), true);
391 }
392}
393
397
398#ifdef STORM_HAVE_CARL
402
406#endif
407} // namespace storage
408} // namespace storm
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:461
std::vector< std::shared_ptr< AtomicExpressionFormula const > > getAtomicExpressionFormulas() const
Definition Formula.cpp:477
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:172
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:453
std::vector< std::shared_ptr< AtomicLabelFormula const > > getAtomicLabelFormulas() const
Definition Formula.cpp:483
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:176
std::shared_ptr< Formula const > asSharedPointer()
Definition Formula.cpp:548
FormulaInformation info(bool recurseIntoOperators=true) const
Definition Formula.cpp:201
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 ...
BisimulationDecomposition(ModelType const &model, Options const &options)
Decomposes the given model into equivalance classes of a bisimulation.
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()
SettingsType const & getModule()
Get module.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
LabParser.cpp.
Definition cli.cpp:18
void preserveFormula(storm::logic::Formula const &formula)
Changes the options in a way that the given formula is preserved.
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...