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

MultiObjectivePreprocesso: Fix for new preprocessing in case of multi-dimensional bounded until formulas.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
9e510560c9
commit
f83c0fa606
1 changed files with 23 additions and 6 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. 29
      src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp

29
src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
View File

@ -119,13 +119,30 @@ namespace storm {
absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs); absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs);
absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs); absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs);
} else if (pathFormula.isBoundedUntilFormula()) { } else if (pathFormula.isBoundedUntilFormula()) {
auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs);
if (pathFormula.asBoundedUntilFormula().hasLowerBound()) {
absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs);
if (pathFormula.asBoundedUntilFormula().hasMultiDimensionalSubformulas()) {
absorbingStatesForSubformula = storm::storage::BitVector(model->getNumberOfStates(), true);
storm::storage::BitVector absorbingStatesForSubSubformula;
for (uint64_t i = 0; i < pathFormula.asBoundedUntilFormula().getDimension(); ++i) {
auto subPathFormula = pathFormula.asBoundedUntilFormula().restrictToDimension(i);
auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector();
auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector();
absorbingStatesForSubSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs);
if (pathFormula.asBoundedUntilFormula().hasLowerBound(i)) {
absorbingStatesForSubSubformula |= getOnlyReachableViaPhi(*model, ~lhs);
} else {
absorbingStatesForSubSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs);
}
absorbingStatesForSubformula &= absorbingStatesForSubSubformula;
}
} else { } else {
absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs);
auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs);
if (pathFormula.asBoundedUntilFormula().hasLowerBound()) {
absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs);
} else {
absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs);
}
} }
} else if (pathFormula.isGloballyFormula()){ } else if (pathFormula.isGloballyFormula()){
auto phi = mc.check(pathFormula.asGloballyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); auto phi = mc.check(pathFormula.asGloballyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();

Write Preview
Loading…
Cancel
Save