Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcInstantiationModelChecker.cpp
Go to the documentation of this file.
2
11
12namespace storm {
13namespace modelchecker {
14
15template<typename SparseModelType, typename ConstantType>
17 : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
18 // Intentionally left empty
19}
20
21template<typename SparseModelType, typename ConstantType>
24 STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
25 auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
26 STORM_LOG_THROW(instantiatedModel.getTransitionMatrix().isProbabilistic(), storm::exceptions::InvalidArgumentException,
27 "Instantiation point is invalid as the transition matrix becomes non-stochastic.");
29
30 // Check if there are some optimizations implemented for the specified property
31 if (this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
32 return checkReachabilityProbabilityFormula(env, modelChecker);
33 } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional()
38 return checkReachabilityRewardFormula(env, modelChecker);
39 } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional()
46 return checkBoundedUntilFormula(env, modelChecker);
47 } else {
48 return modelChecker.check(env, *this->currentCheckTask);
49 }
50}
51
52template<typename SparseModelType, typename ConstantType>
55 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
56 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
57 }
58 ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
59
60 if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
61 // Perform purely qualitative analysis once
62 std::vector<ConstantType> qualitativeResult;
63 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
64 auto newCheckTask = *this->currentCheckTask;
65 newCheckTask.setQualitative(true);
66 newCheckTask.setOnlyInitialStatesRelevant(false);
67 qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
68 } else {
69 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
70 newCheckTask.setQualitative(true);
71 newCheckTask.setOnlyInitialStatesRelevant(false);
72 qualitativeResult =
73 modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
74 }
75 storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult, [](ConstantType const& value) -> bool {
76 return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value));
77 });
78 hint.setMaybeStates(std::move(maybeStates));
79 hint.setResultHint(std::move(qualitativeResult));
81 }
82
83 std::unique_ptr<CheckResult> result;
84 // Check the formula and store the result as a hint for the next call.
85 // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
86 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
87 result = modelChecker.check(env, *this->currentCheckTask);
88 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
89 } else {
90 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
91 .setOnlyInitialStatesRelevant(false);
92 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
93 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
94 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
95 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
96 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
97 }
98
99 return result;
100}
101
102template<typename SparseModelType, typename ConstantType>
105 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
106 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
107 }
108 ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
109
110 if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
111 // Perform purely qualitative analysis once
112 std::vector<ConstantType> qualitativeResult;
113 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
114 auto newCheckTask = *this->currentCheckTask;
115 newCheckTask.setQualitative(true);
116 newCheckTask.setOnlyInitialStatesRelevant(false);
117 qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
118 } else {
119 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
120 newCheckTask.setQualitative(true);
121 newCheckTask.setOnlyInitialStatesRelevant(false);
122 qualitativeResult = modelChecker.computeRewards(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
123 }
124 storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult, [](ConstantType const& value) -> bool {
125 return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value));
126 });
127 hint.setMaybeStates(std::move(maybeStates));
128 hint.setResultHint(std::move(qualitativeResult));
129 hint.setComputeOnlyMaybeStates(true);
130 }
131
132 std::unique_ptr<CheckResult> result;
133
134 // Check the formula and store the result as a hint for the next call.
135 // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
136 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
137 result = modelChecker.check(env, *this->currentCheckTask);
138 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(
139 result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
140 } else {
141 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
142 .setOnlyInitialStatesRelevant(false);
143 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(env, newCheckTask);
144 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
145 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
146 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
147 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(
148 std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
149 }
150
151 return result;
152}
153
154template<typename SparseModelType, typename ConstantType>
157 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
158 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
159 }
160 std::unique_ptr<CheckResult> result;
161 ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
162
163 if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
164 // We extract the maybestates from the quantitative result
165 // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
166 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
167 result = modelChecker.check(env, *this->currentCheckTask);
168 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
169 } else {
170 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
171 .setOnlyInitialStatesRelevant(false);
172 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
173 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
174 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
175 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
176 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
177 }
178
180 // We need to exclude the target states from the maybe states.
181 // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
182 std::unique_ptr<CheckResult> subFormulaResult =
183 modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
184 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
185 hint.setMaybeStates(std::move(maybeStates));
186 hint.setComputeOnlyMaybeStates(true);
187 } else {
188 result = modelChecker.check(env, *this->currentCheckTask);
189 }
190
191 return result;
192}
193
196
197} // namespace modelchecker
198} // namespace storm
FragmentSpecification & setStepBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setOperatorAtTopLevelRequired(bool newValue)
FragmentSpecification & setTimeBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setReachabilityRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardOperatorsAllowed(bool newValue)
FragmentSpecification & setBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setNestedOperatorsAllowed(bool newValue)
FragmentSpecification & setProbabilityOperatorsAllowed(bool newValue)
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
This class contains information that might accelerate the model checking process.
void setResultHint(boost::optional< std::vector< ValueType > > const &resultHint)
void setMaybeStates(storm::storage::BitVector const &maybeStates)
std::vector< ValueType > const & getResultHint() const
Class to efficiently check a formula on a parametric model with different parameter instantiations.
std::unique_ptr< CheckResult > checkReachabilityRewardFormula(Environment const &env, storm::modelchecker::SparseDtmcPrctlModelChecker< storm::models::sparse::Dtmc< ConstantType > > &modelChecker)
virtual std::unique_ptr< CheckResult > check(Environment const &env, storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &valuation) override
std::unique_ptr< CheckResult > checkBoundedUntilFormula(Environment const &env, storm::modelchecker::SparseDtmcPrctlModelChecker< storm::models::sparse::Dtmc< ConstantType > > &modelChecker)
std::unique_ptr< CheckResult > checkReachabilityProbabilityFormula(Environment const &env, storm::modelchecker::SparseDtmcPrctlModelChecker< storm::models::sparse::Dtmc< ConstantType > > &modelChecker)
Class to efficiently check a formula on a parametric model with different parameter instantiations.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
FragmentSpecification propositional()
FragmentSpecification reachability()
std::map< typename VariableType< FunctionType >::type, typename CoefficientType< FunctionType >::type > Valuation
Definition parametric.h:41
storm::storage::BitVector filterGreaterZero(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is greater tha...
Definition vector.h:552
LabParser.cpp.
Definition cli.cpp:18