From f83c0fa606a1516fc2a690abac0f09668faf00a7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Jul 2019 16:29:01 +0200 Subject: [PATCH] MultiObjectivePreprocesso: Fix for new preprocessing in case of multi-dimensional bounded until formulas. --- .../SparseMultiObjectivePreprocessor.cpp | 29 +++++++++++++++---- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 5252d380c..a27025cf4 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -119,13 +119,30 @@ namespace storm { absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs); absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs); } 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 { - 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()){ auto phi = mc.check(pathFormula.asGloballyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();