diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 86841f63f..12b51dcf4 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -227,7 +227,7 @@ namespace storm { storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); storm::storage::BitVector soiProduct(product->getStatesOfInterest()); - // Create goal for computeUntilProbabilities, compute maximizing probabilties for DA product with MDP + // Create goal for computeUntilProbabilities, compute maximizing probabilities for DA product with MDP storm::solver::SolveGoal solveGoalProduct; if (this->isValueThresholdSet()) { solveGoalProduct = storm::solver::SolveGoal(OptimizationDirection::Maximize, this->getValueThresholdComparisonType(), this->getValueThresholdValue(), std::move(soiProduct)); @@ -263,17 +263,23 @@ namespace storm { return numericResult; } - - //todo remove goal? template - std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { - // TODO optDir: helper.getOptimizationDirection for MDP - // negate formula etc ~ap? + std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets) { + std::shared_ptr ltlFormula; + STORM_LOG_THROW((!Nondeterministic) || this->isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + if (Nondeterministic && this->getOptimizationDirection() == OptimizationDirection::Minimize) { + // negate formula in order to compute 1-Pmax[!formula] + ltlFormula = std::make_shared(storm::logic::UnaryBooleanOperatorType::Not, formula.asSharedPointer()); + STORM_LOG_INFO("Computing Pmin, proceeding with negated LTL formula."); + } else { + ltlFormula = formula.asSharedPointer(); + } - STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula); - STORM_LOG_INFO(" in prefix format: " << ltlFormula.toPrefixString()); - std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(ltlFormula); + STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula->toString()); + STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); + + std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula); STORM_LOG_INFO("Deterministic automaton for LTL formula has " << da->getNumberOfStates() << " states, " @@ -281,18 +287,16 @@ namespace storm { << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - //todo remove goal here? send dir instead? + // compute Pmax for MDP std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet()); - // TODO optDir: helper.getOptimizationDirection for MDP - /* //for any path formula ψ: pmin(s, ψ) = 1- pmax(s, ¬ψ) if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { - // compute 1-Pmax[!ltl] + // compute 1-Pmax[!fomula] for (auto& value : numericResult) { value = storm::utility::one() - value; } } - */ + return numericResult; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 3e69b6f8d..b8944446c 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -45,7 +45,7 @@ namespace storm { * Computes the ltl probabilities ...todo * @return a value for each state */ - std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& f, std::map& apSatSets); //todo was brauchen wir hier aps und ..? + std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); //todo was brauchen wir hier aps und ..? private: diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 85f89bf18..1623477f1 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -202,22 +202,7 @@ namespace storm { apSets[p.first] = std::move(sat); } - bool minimize = false; - CheckTask subTask(checkTask); - - if (checkTask.getOptimizationDirection() == OptimizationDirection::Minimize) { - minimize = true; - // negate - ltlFormula = std::make_shared(storm::logic::UnaryBooleanOperatorType::Not, ltlFormula); - STORM_LOG_INFO("Computing Pmin, proceeding with negated LTL formula."); - - subTask = checkTask.negate().substituteFormula(*ltlFormula); - } else { - subTask = checkTask.substituteFormula(*ltlFormula); - } - const SparseMdpModelType& mdp = this->getModel(); - storm::solver::SolveGoal goal(mdp, subTask); //todo remove, infos now in helper, see below // TODO if (storm::settings::getModule().isTraceSet()) { @@ -228,16 +213,9 @@ namespace storm { } storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); - storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp); std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); - if(minimize) { - // compute 1-Pmax[!ltl] - for (auto& value : numericResult) { - value = storm::utility::one() - value; - } - } - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); }