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

Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas).

tempestpy_adaptions
TimQu 8 years ago
parent
c5c14f3178
commit
48d5025bd9
2 changed files with 38 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/modelchecker/AbstractModelChecker.cpp
  2. 62
      src/storm/modelchecker/CheckTask.h

4
src/storm/modelchecker/AbstractModelChecker.cpp
View File

@ -219,9 +219,9 @@ namespace storm {
storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula()));
if (stateFormula.hasBound()) {
if (checkTask.isBoundSet()) {
STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
return result->asQuantitativeCheckResult<ValueType>().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThresholdAs<ValueType>());
return result->asQuantitativeCheckResult<ValueType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
} else {
return result;
}

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

@ -40,8 +40,27 @@ namespace storm {
this->produceSchedulers = false;
this->qualitative = false;
if (formula.isOperatorFormula()) {
storm::logic::OperatorFormula const& operatorFormula = formula.asOperatorFormula();
updateOperatorInformation();
}
/*!
* Copies the check task from the source while replacing the formula with the new one. In particular, this
* changes the formula type of the check task object.
*/
template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint);
result.updateOperatorInformation();
return result;
}
/*!
* If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula.
* Calling this method has no effect if the provided formula is not an operator formula.
*/
void updateOperatorInformation() {
if (formula.get().isOperatorFormula()) {
storm::logic::OperatorFormula const& operatorFormula = formula.get().asOperatorFormula();
if (operatorFormula.hasOptimalityType()) {
this->optimizationDirection = operatorFormula.getOptimalityType();
}
@ -55,37 +74,28 @@ namespace storm {
this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
}
}
}
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
if (probabilityOperatorFormula.hasBound()) {
if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
if (formula.get().isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.get().asProbabilityOperatorFormula();
if (probabilityOperatorFormula.hasBound()) {
if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
}
}
}
} else if (formula.isRewardOperatorFormula()) {
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
if (rewardOperatorFormula.hasBound()) {
if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
} else if (formula.get().isRewardOperatorFormula()) {
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.get().asRewardOperatorFormula();
this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
if (rewardOperatorFormula.hasBound()) {
if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
this->qualitative = true;
}
}
}
}
}
/*!
* Copies the check task from the source while replacing the formula with the new one. In particular, this
* changes the formula type of the check task object.
*/
template<typename NewFormulaType>
CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint);
}
/*!
* Retrieves the formula from this task.
*/

Write Preview
Loading…
Cancel
Save