sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

storm-pars: Fixed an issue in the instantiation model checkers where maybestates were cached incorrectly.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
d135bc8ecb
commit
45803c547e
3 changed files with 100 additions and 56 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 68
      src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
  2. 80
      src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
  3. 8
      src/storm/modelchecker/CheckTask.h

68
src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
View File

@ -42,8 +42,31 @@ namespace storm {
this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>()); this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
} }
ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>(); ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
std::unique_ptr<CheckResult> result;
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Perform purely qualitative analysis once
std::vector<ConstantType> qualitativeResult;
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
auto newCheckTask = *this->currentCheckTask;
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
} else {
auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl;
storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
[] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value)); });
std::cout <<maybeStates << std::endl;
hint.setMaybeStates(std::move(maybeStates));
hint.setResultHint(std::move(qualitativeResult));
hint.setComputeOnlyMaybeStates(true);
}
std::unique_ptr<CheckResult> result;
// Check the formula and store the result as a hint for the next call. // Check the formula and store the result as a hint for the next call.
// For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@ -56,15 +79,6 @@ namespace storm {
hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector())); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
} }
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Extract the maybe states from the current result.
assert(hint.hasResultHint());
storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
[] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
}
return result; return result;
} }
@ -75,6 +89,28 @@ namespace storm {
this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>()); this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
} }
ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>(); ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Perform purely qualitative analysis once
std::vector<ConstantType> qualitativeResult;
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
auto newCheckTask = *this->currentCheckTask;
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
} else {
auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
[] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value)); });
hint.setMaybeStates(std::move(maybeStates));
hint.setResultHint(std::move(qualitativeResult));
hint.setComputeOnlyMaybeStates(true);
}
std::unique_ptr<CheckResult> result; std::unique_ptr<CheckResult> result;
// Check the formula and store the result as a hint for the next call. // Check the formula and store the result as a hint for the next call.
@ -89,18 +125,6 @@ namespace storm {
this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector())); this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
} }
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Extract the maybe states from the current result.
assert(hint.hasResultHint());
storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
// We need to exclude the target states from the maybe states.
// Note that we can not consider the states with reward zero since a valuation might set a reward to zero
std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
}
return result; return result;
} }

80
src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
View File

@ -47,8 +47,31 @@ namespace storm {
this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>()); this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
} }
ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>(); ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
std::unique_ptr<CheckResult> result;
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Perform purely qualitative analysis once
std::vector<ConstantType> qualitativeResult;
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
auto newCheckTask = *this->currentCheckTask;
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
} else {
auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl;
storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
[] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value)); });
std::cout <<maybeStates << std::endl;
hint.setMaybeStates(std::move(maybeStates));
hint.setResultHint(std::move(qualitativeResult));
hint.setComputeOnlyMaybeStates(true);
}
std::unique_ptr<CheckResult> result;
// Check the formula and store the result as a hint for the next call. // Check the formula and store the result as a hint for the next call.
// For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@ -65,21 +88,6 @@ namespace storm {
hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler))); hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
} }
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Extract the maybe states from the current result.
assert(hint.hasResultHint());
storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
[] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
// Check if there can be end components within the maybestates
if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) ||
storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
hint.setNoEndComponentsInMaybeStates(true);
}
}
return result; return result;
} }
@ -92,8 +100,29 @@ namespace storm {
this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>()); this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
} }
ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>(); ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
std::unique_ptr<CheckResult> result;
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Perform purely qualitative analysis once
std::vector<ConstantType> qualitativeResult;
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
auto newCheckTask = *this->currentCheckTask;
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
} else {
auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
newCheckTask.setQualitative(true);
newCheckTask.setOnlyInitialStatesRelevant(false);
qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
}
storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
[] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value)); });
hint.setMaybeStates(std::move(maybeStates));
hint.setResultHint(std::move(qualitativeResult));
hint.setComputeOnlyMaybeStates(true);
}
std::unique_ptr<CheckResult> result;
// Check the formula and store the result as a hint for the next call. // Check the formula and store the result as a hint for the next call.
// For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@ -110,23 +139,6 @@ namespace storm {
hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler))); hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
} }
if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
// Extract the maybe states from the current result.
assert(hint.hasResultHint());
storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
// We need to exclude the target states from the maybe states.
// Note that we can not consider the states with reward zero since a valuation might set a reward to zero
std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
// Check if there can be end components within the maybestates
if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) ||
storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
hint.setNoEndComponentsInMaybeStates(true);
}
}
return result; return result;
} }

8
src/storm/modelchecker/CheckTask.h
View File

@ -207,6 +207,14 @@ namespace storm {
bool isQualitativeSet() const { bool isQualitativeSet() const {
return qualitative; return qualitative;
} }
/*!
* sets whether the computation only needs to be performed qualitatively, because the values will only
* be compared to 0/1.
*/
void setQualitative(bool value) {
qualitative = value;
}
/*! /*!
* Sets whether to produce schedulers (if supported). * Sets whether to produce schedulers (if supported).

Write Preview
Loading…
Cancel
Save