Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicModelPartitionRefiner.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace dd {
8namespace bisimulation {
9
10template<storm::dd::DdType DdType, typename ValueType>
13 : PartitionRefiner<DdType, ValueType>(model, initialStatePartition),
14 model(model),
15 choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(model, initialStatePartition.getBlockVariables())),
16 stateSignatureRefiner(model.getManager(), this->statePartition.getBlockVariable(), model.getRowVariables(), model.getColumnVariables(), true),
17 statePartitonHasBeenRefinedOnce(false) {
18 // For Markov automata, we refine the state partition wrt. to their exit rates.
20 STORM_LOG_TRACE("Refining with respect to exit rates.");
21 auto exitRateVector = this->model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getExitRateVector();
22 this->statePartition = stateSignatureRefiner.refine(this->statePartition, Signature<DdType, ValueType>(exitRateVector));
23 }
24}
25
26template<storm::dd::DdType DdType, typename ValueType>
28 // In this procedure, we will
29 // (1) refine the partition of nondeterministic choices based on the state partition. For this, we use
30 // the signature computer/refiner of the superclass. These objects use the full transition matrix.
31 // (2) if the choice partition was in fact split, the state partition also needs to be refined.
32 // For this, we use the signature computer/refiner of this class.
33
34 STORM_LOG_TRACE("Refining choice partition.");
35 Partition<DdType, ValueType> newChoicePartition =
36 this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode);
37
38 // If the choice partition has become stable in an iteration that is not the starting one, we have
39 // reached a fixed point and can return.
40 if (newChoicePartition.getNumberOfBlocks() == choicePartition.getNumberOfBlocks() && statePartitonHasBeenRefinedOnce) {
41 this->status = Status::FixedPoint;
42 return false;
43 } else {
44 this->choicePartition = newChoicePartition;
45
46 // Compute state signatures.
47 storm::dd::Bdd<DdType> choicePartitionAsBdd;
48 if (this->choicePartition.storedAsBdd()) {
49 choicePartitionAsBdd = this->choicePartition.asBdd();
50 } else {
51 choicePartitionAsBdd = this->choicePartition.asAdd().notZero();
52 }
53
54 auto signatureStart = std::chrono::high_resolution_clock::now();
55 Signature<DdType, ValueType> stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd<ValueType>());
56 auto signatureEnd = std::chrono::high_resolution_clock::now();
57 this->totalSignatureTime += (signatureEnd - signatureStart);
58
59 // If the choice partition changed, refine the state partition.
60 STORM_LOG_TRACE("Refining state partition.");
61 auto refinementStart = std::chrono::high_resolution_clock::now();
62 Partition<DdType, ValueType> newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition);
63 statePartitonHasBeenRefinedOnce = true;
64 auto refinementEnd = std::chrono::high_resolution_clock::now();
65
66 auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
67 auto refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
68 STORM_LOG_INFO("Refinement " << (this->refinements - 1) << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in "
69 << (signatureTime + refinementTime) << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime
70 << "ms).");
71
72 if (newStatePartition == this->statePartition) {
73 this->status = Status::FixedPoint;
74 return false;
75 } else {
76 this->statePartition = newStatePartition;
77 return true;
78 }
79 }
80}
81
82template<storm::dd::DdType DdType, typename ValueType>
86
87template<storm::dd::DdType DdType, typename ValueType>
89 STORM_LOG_TRACE("Refining with respect to state rewards.");
90 Partition<DdType, ValueType> newStatePartition = this->stateSignatureRefiner.refine(this->statePartition, Signature<DdType, ValueType>(stateRewards));
91 if (newStatePartition == this->statePartition) {
92 return false;
93 } else {
94 this->statePartition = newStatePartition;
95 return true;
96 }
97}
98
99template<storm::dd::DdType DdType, typename ValueType>
100bool NondeterministicModelPartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
101 STORM_LOG_TRACE("Refining with respect to state-action rewards.");
102 Partition<DdType, ValueType> newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature<DdType, ValueType>(stateActionRewards));
103 if (newChoicePartition == this->choicePartition) {
104 return false;
105 } else {
106 this->choicePartition = newChoicePartition;
107 return true;
108 }
109}
110
111template class NondeterministicModelPartitionRefiner<storm::dd::DdType::CUDD, double>;
112
113template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, double>;
114template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalNumber>;
115template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction>;
116
117} // namespace bisimulation
118} // namespace dd
119} // namespace storm
Bdd< LibraryType > existsAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Existentially abstracts from the given meta variables.
Definition Bdd.cpp:178
virtual bool refine(bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager) override
Refines the partition.
NondeterministicModelPartitionRefiner(storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, Partition< DdType, ValueType > const &initialStatePartition)
Partition< DdType, ValueType > const & getChoicePartition() const
Retrieves the current choice partition in the refinement process.
Partition< DdType, ValueType > statePartition
bool isOfType(storm::models::ModelType const &modelType) const
Checks whether the model is of the given type.
Definition ModelBase.cpp:19
Base class for all nondeterministic symbolic models.
#define STORM_LOG_INFO(message)
Definition logging.h:29
#define STORM_LOG_TRACE(message)
Definition logging.h:17
LabParser.cpp.
Definition cli.cpp:18