diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ce88522eb..6cc9b37ce 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -61,7 +61,22 @@ namespace storm { std::map constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); - STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants."); + + if (preparedProgram.hasUndefinedConstants()) { + std::vector> undefinedConstants = preparedProgram.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + } // Now that we have defined all the constants in the program, we need to substitute their appearances in // all expressions in the program so we can then evaluate them without having to store the values of the diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 9c5d25808..352534d8e 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1,19 +1,16 @@ -/* - * MILPMinimalLabelSetGenerator.h - * - * Created on: 15.09.2013 - * Author: Christian Dehnert - */ - #ifndef STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ #define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ #include #include "src/models/Mdp.h" +#include "src/logic/Formulas.h" #include "src/storage/prism/Program.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" #include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidStateException.h" @@ -922,7 +919,7 @@ namespace storm { public: - static boost::container::flat_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + static boost::container::flat_set getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; @@ -931,14 +928,13 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + std::unique_ptr result = modelchecker.check(pathFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult = result->asExplicitQuantitativeCheckResult(); for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } - if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; + maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]); } + STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } @@ -978,49 +974,48 @@ namespace storm { * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested * formula can be either an unbounded until formula or an eventually formula. */ - static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const& formula) { - std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl; - // First, we need to check whether the current formula is an Until-Formula. - std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formula); - if (probBoundFormula.get() == nullptr) { - LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."); - throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."; - } + static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr const& formula) { + std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; - // Check whether we were given an upper bound, because counterexample generation is limited to this case. - if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) { - LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); - throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; - } - bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; + STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); + storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); + STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); + storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); + STORM_LOG_THROW(comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual, storm::exceptions::InvalidPropertyException, "Counterexample generation only supports formulas with an upper probability bound."); + STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); + + bool strictBound = comparisonType == storm::logic::ComparisonType::Less; + double bound = probabilityOperator.getBound(); - // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. - double bound = probBoundFormula->getBound(); - std::shared_ptr> pathFormula = probBoundFormula->getChild(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); - if(untilFormula.get() != nullptr) { - phiStates = untilFormula->getLeft()->check(modelchecker); - psiStates = untilFormula->getRight()->check(modelchecker); + if (probabilityOperator.getSubformula().isUntilFormula()) { + storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); - } if (std::dynamic_pointer_cast>(pathFormula).get() != nullptr) { - // If the nested formula was not an until formula, it remains to check whether it's an eventually formula. - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); + std::unique_ptr leftResult = modelchecker.check(untilFormula.getLeftSubformula()); + std::unique_ptr rightResult = modelchecker.check(untilFormula.getRightSubformula()); - phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = eventuallyFormula->getChild()->check(modelchecker); + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); - } else { - // If the nested formula is neither an until nor a finally formula, we throw an exception. - throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; + phiStates = leftQualitativeResult.getTruthValues(); + psiStates = rightQualitativeResult.getTruthValues(); + } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); + + std::unique_ptr subResult = modelchecker.check(eventuallyFormula.getSubformula()); + + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + + phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); + psiStates = subQualitativeResult.getTruthValues(); } // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); + boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; @@ -1028,8 +1023,6 @@ namespace storm { storm::prism::Program restrictedProgram = program.restrictCommands(usedLabelSet); std::cout << restrictedProgram << std::endl; std::cout << std::endl << "-------------------------------------------" << std::endl; - - // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set. } }; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index d0793c781..8b161d372 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -9,6 +9,7 @@ #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/utility/counterexamples.h" @@ -1594,7 +1595,7 @@ namespace storm { * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalCommandSet(storm::logic::Formula const& pathFormula, storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1625,15 +1626,14 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + std::unique_ptr result = modelchecker.check(pathFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult = result->asExplicitQuantitativeCheckResult(); for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); + maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]); } - if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; - } - std::cout << std::endl << "Maximal reachability in model determined is " << maximalReachabilityProbability << "." << std::endl; + STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); + std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. @@ -1752,50 +1752,49 @@ namespace storm { #endif } - static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr> const& formula) { + static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl; - // First, we need to check whether the current formula is an Until-Formula. - std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formula); - if (probBoundFormula.get() == nullptr) { - LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."); - throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."; - } + std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; - // Check whether we were given an upper bound, because counterexample generation is limited to this case. - if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) { - LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); - throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; - } - bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; + STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); + storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); + STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); + storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); + STORM_LOG_THROW(comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual, storm::exceptions::InvalidPropertyException, "Counterexample generation only supports formulas with an upper probability bound."); + STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); + + bool strictBound = comparisonType == storm::logic::ComparisonType::Less; + double bound = probabilityOperator.getBound(); - // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. - double bound = probBoundFormula->getBound(); - std::shared_ptr> pathFormula = probBoundFormula->getChild(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); - if(untilFormula.get() != nullptr) { - phiStates = untilFormula->getLeft()->check(modelchecker); - psiStates = untilFormula->getRight()->check(modelchecker); - - } if (std::dynamic_pointer_cast>(pathFormula).get() != nullptr) { - // If the nested formula was not an until formula, it remains to check whether it's an eventually formula. - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); - - phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = eventuallyFormula->getChild()->check(modelchecker); - - } else { - // If the nested formula is neither an until nor a finally formula, we throw an exception. - throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + + if (probabilityOperator.getSubformula().isUntilFormula()) { + storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); + + std::unique_ptr leftResult = modelchecker.check(untilFormula.getLeftSubformula()); + std::unique_ptr rightResult = modelchecker.check(untilFormula.getRightSubformula()); + + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult.asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult.asExplicitQualitativeCheckResult(); + + phiStates = leftQualitativeResult.getTruthValues(); + psiStates = rightQualitativeResult.getTruthValues(); + } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); + + std::unique_ptr subResult = modelchecker.check(untilFormula.getSubformula()); + + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult(); + + phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); + psiStates = subResult.getTruthValues(); } // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); + auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp index a2b3d733a..70f2e9287 100644 --- a/src/logic/BinaryBooleanStateFormula.cpp +++ b/src/logic/BinaryBooleanStateFormula.cpp @@ -14,6 +14,18 @@ namespace storm { return this->getLeftSubformula().isPropositionalFormula() && this->getRightSubformula().isPropositionalFormula(); } + BinaryBooleanStateFormula::OperatorType BinaryBooleanStateFormula::getOperator() const { + return operatorType; + } + + bool BinaryBooleanStateFormula::isAnd() const { + return this->getOperator() == OperatorType::And; + } + + bool BinaryBooleanStateFormula::isOr() const { + return this->getOperator() == OperatorType::Or; + } + std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const { out << "("; this->getLeftSubformula().writeToStream(out); diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h index 2d6ca37c7..5e77bbf88 100644 --- a/src/logic/BinaryBooleanStateFormula.h +++ b/src/logic/BinaryBooleanStateFormula.h @@ -19,6 +19,11 @@ namespace storm { virtual bool isPropositionalFormula() const override; + OperatorType getOperator() const; + + virtual bool isAnd() const; + virtual bool isOr() const; + virtual std::ostream& writeToStream(std::ostream& out) const override; private: diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp index 09ee894e0..926b56037 100644 --- a/src/logic/UnaryBooleanStateFormula.cpp +++ b/src/logic/UnaryBooleanStateFormula.cpp @@ -10,6 +10,14 @@ namespace storm { return true; } + UnaryBooleanStateFormula::OperatorType UnaryBooleanStateFormula::getOperator() const { + return operatorType; + } + + bool UnaryBooleanStateFormula::isNot() const { + return this->getOperator() == OperatorType::Not; + } + std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const { switch (operatorType) { case OperatorType::Not: out << "!("; break; diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h index 37d6a82ae..317e89af7 100644 --- a/src/logic/UnaryBooleanStateFormula.h +++ b/src/logic/UnaryBooleanStateFormula.h @@ -17,6 +17,10 @@ namespace storm { virtual bool isUnaryBooleanStateFormula() const override; + OperatorType getOperator() const; + + virtual bool isNot() const; + virtual std::ostream& writeToStream(std::ostream& out) const override; private: diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 9d3c21c8f..bb70df149 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -15,7 +15,7 @@ namespace storm { } else if (formula.isRewardPathFormula()) { return this->computeRewards(formula.asRewardPathFormula()); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } std::unique_ptr AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { @@ -30,7 +30,7 @@ namespace storm { } else if (pathFormula.isUntilFormula()) { return this->computeUntilProbabilities(pathFormula.asUntilFormula(), qualitative, optimalityType); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid."); } std::unique_ptr AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { @@ -66,7 +66,7 @@ namespace storm { } else if (rewardPathFormula.isReachabilityRewardFormula()) { return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), qualitative, optimalityType); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); } std::unique_ptr AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { @@ -84,6 +84,8 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) { if (stateFormula.isBinaryBooleanStateFormula()) { return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula()); + } else if (stateFormula.isUnaryBooleanStateFormula()) { + return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula()); } else if (stateFormula.isBooleanLiteralFormula()) { return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); } else if (stateFormula.isProbabilityOperatorFormula()) { @@ -116,7 +118,14 @@ namespace storm { std::unique_ptr leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula()); std::unique_ptr rightResult = this->check(stateFormula.getRightSubformula().asStateFormula()); - *leftResult &= *rightResult; + if (stateFormula.isAnd()) { + *leftResult &= *rightResult; + } else if (stateFormula.isOr()) { + *leftResult |= *rightResult; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); + } + return leftResult; } @@ -172,7 +181,11 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) { std::unique_ptr subResult = this->check(stateFormula.getSubformula()); - subResult->complement(); + if (stateFormula.isNot()) { + subResult->complement(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); + } return subResult; } } diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/CheckResult.h index 485fd03b8..9e7c061e7 100644 --- a/src/modelchecker/CheckResult.h +++ b/src/modelchecker/CheckResult.h @@ -4,6 +4,7 @@ #include #include +#include "src/storage/BitVector.h" #include "src/logic/ComparisonType.h" namespace storm { @@ -23,8 +24,6 @@ namespace storm { virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; - friend std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); - virtual bool isExplicit() const; virtual bool isQuantitative() const; virtual bool isQualitative() const; @@ -42,8 +41,8 @@ namespace storm { template ExplicitQuantitativeCheckResult const& asExplicitQuantitativeCheckResult() const; - protected: virtual std::ostream& writeToStream(std::ostream& out) const = 0; + virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const = 0; }; std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp index f69744fc4..e41ea1945 100644 --- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp @@ -47,5 +47,27 @@ namespace storm { out << truthValues; return out; } + + std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const { + std::ios::fmtflags oldflags(std::cout.flags()); + + out << "["; + storm::storage::BitVector::const_iterator it = filter.begin(); + storm::storage::BitVector::const_iterator itPlusOne = filter.begin(); + ++itPlusOne; + storm::storage::BitVector::const_iterator ite = filter.end(); + + out << std::boolalpha; + for (; it != ite; ++itPlusOne, ++it) { + out << truthValues[*it]; + if (itPlusOne != ite) { + out << ", "; + } + } + out << "]"; + + std::cout.flags(oldflags); + return out; + } } } \ No newline at end of file diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.h b/src/modelchecker/ExplicitQualitativeCheckResult.h index c45f29577..5b3903a35 100644 --- a/src/modelchecker/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/ExplicitQualitativeCheckResult.h @@ -47,9 +47,9 @@ namespace storm { storm::storage::BitVector const& getTruthValues() const; - protected: virtual std::ostream& writeToStream(std::ostream& out) const override; - + virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override; + private: // The values of the quantitative check result. storm::storage::BitVector truthValues; diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp index 1718a46fd..06719223e 100644 --- a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp @@ -12,6 +12,24 @@ namespace storm { return values; } + template + std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const { + out << "["; + storm::storage::BitVector::const_iterator it = filter.begin(); + storm::storage::BitVector::const_iterator itPlusOne = filter.begin(); + ++itPlusOne; + storm::storage::BitVector::const_iterator ite = filter.end(); + + for (; it != ite; ++itPlusOne, ++it) { + out << values[*it]; + if (itPlusOne != ite) { + out << ", "; + } + } + out << "]"; + return out; + } + template std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out) const { out << "["; diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.h b/src/modelchecker/ExplicitQuantitativeCheckResult.h index 41511a6d4..ba933459e 100644 --- a/src/modelchecker/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.h @@ -47,8 +47,8 @@ namespace storm { std::vector const& getValues() const; - protected: virtual std::ostream& writeToStream(std::ostream& out) const override; + virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override; private: // The values of the quantitative check result. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index c34aa8b01..1d6a26367 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -13,6 +13,7 @@ #include "src/solver/LpSolver.h" +#include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" namespace storm { @@ -210,7 +211,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslModelChecker::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const { - + // FIXME } template @@ -232,6 +233,7 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index b6ab4d230..3759fd1d5 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -308,6 +308,7 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 0d7b9d5fc..5f73e5b9f 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -319,6 +319,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); } diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index ece0d9a00..d361c4de5 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -23,12 +23,8 @@ namespace storm { const std::string GeneralSettings::explicitOptionShortName = "e"; const std::string GeneralSettings::symbolicOptionName = "symbolic"; const std::string GeneralSettings::symbolicOptionShortName = "s"; - const std::string GeneralSettings::pctlOptionName = "pctl"; - const std::string GeneralSettings::pctlFileOptionName = "pctlfile"; - const std::string GeneralSettings::cslOptionName = "csl"; - const std::string GeneralSettings::cslFileOptionName = "cslfile"; - const std::string GeneralSettings::ltlOptionName = "ltl"; - const std::string GeneralSettings::ltlFileOptionName = "ltlfile"; + const std::string GeneralSettings::propertyOptionName = "prop"; + const std::string GeneralSettings::propertyFileOptionName = "propfile"; const std::string GeneralSettings::transitionRewardsOptionName = "transrew"; const std::string GeneralSettings::stateRewardsOptionName = "staterew"; const std::string GeneralSettings::counterexampleOptionName = "counterexample"; @@ -63,18 +59,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.") + this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies a PCTL formula that is to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") + this->addOption(storm::settings::OptionBuilder(moduleName, propertyFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, cslOptionName, false, "Specifies a CSL formula that is to be checked on the model.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, cslFileOptionName, false, "Specifies the CSL formulas that are to be checked on the model.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, ltlOptionName, false, "Specifies an LTL formula that is to be checked on the model.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, ltlFileOptionName, false, "Specifies the LTL formulas that are to be checked on the model.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build()); @@ -163,52 +151,20 @@ namespace storm { return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString(); } - bool GeneralSettings::isPctlPropertySet() const { - return this->getOption(pctlOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getPctlProperty() const { - return this->getOption(pctlOptionName).getArgumentByName("formula").getValueAsString(); - } - - bool GeneralSettings::isPctlFileSet() const { - return this->getOption(pctlFileOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getPctlPropertiesFilename() const { - return this->getOption(pctlFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool GeneralSettings::isCslPropertySet() const { - return this->getOption(cslOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getCslProperty() const { - return this->getOption(cslOptionName).getArgumentByName("formula").getValueAsString(); - } - - bool GeneralSettings::isCslFileSet() const { - return this->getOption(cslFileOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getCslPropertiesFilename() const { - return this->getOption(cslOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool GeneralSettings::isLtlPropertySet() const { - return this->getOption(ltlOptionName).getHasOptionBeenSet(); + bool GeneralSettings::isPropertySet() const { + return this->getOption(propertyOptionName).getHasOptionBeenSet(); } - std::string GeneralSettings::getLtlProperty() const { - return this->getOption(ltlOptionName).getArgumentByName("formula").getValueAsString(); + std::string GeneralSettings::getProperty() const { + return this->getOption(propertyOptionName).getArgumentByName("formula").getValueAsString(); } - bool GeneralSettings::isLtlFileSet() const { - return this->getOption(ltlFileOptionName).getHasOptionBeenSet(); + bool GeneralSettings::isPropertyFileSet() const { + return this->getOption(propertyFileOptionName).getHasOptionBeenSet(); } - std::string GeneralSettings::getLtlPropertiesFilename() const { - return this->getOption(ltlOptionName).getArgumentByName("filename").getValueAsString(); + std::string GeneralSettings::getPropertiesFilename() const { + return this->getOption(propertyFileOptionName).getArgumentByName("filename").getValueAsString(); } bool GeneralSettings::isTransitionRewardsSet() const { @@ -288,8 +244,8 @@ namespace storm { STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both."); // Make sure that one "source" for properties is given. - uint_fast64_t propertySources = 0 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0); - STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties."); + uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0); + STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both."); return true; } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 22f8fe58f..583bf7e3b 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -142,88 +142,32 @@ namespace storm { std::string getSymbolicRewardModelName() const; /*! - * Retrieves whether the pctl option was set. + * Retrieves whether the property option was set. * - * @return True if the pctl option was set. + * @return True if the property option was set. */ - bool isPctlPropertySet() const; + bool isPropertySet() const; /*! - * Retrieves the property specified with the pctl option. + * Retrieves the property specified with the property option. * - * @return The property specified with the pctl option. + * @return The property specified with the property option. */ - std::string getPctlProperty() const; + std::string getProperty() const; /*! - * Retrieves whether the pctl-file option was set. + * Retrieves whether a property file was set. * - * @return True iff the pctl-file option was set. + * @return True iff a property was set. */ - bool isPctlFileSet() const; + bool isPropertyFileSet() const; /*! - * Retrieves the name of the file that contains the PCTL properties to be checked on the model. + * Retrieves the name of the file that contains the properties to be checked on the model. * - * @return The name of the file that contains the PCTL properties to be checked on the model. + * @return The name of the file that contains the properties to be checked on the model. */ - std::string getPctlPropertiesFilename() const; - - /*! - * Retrieves whether the csl option was set. - * - * @return True if the csl option was set. - */ - bool isCslPropertySet() const; - - /*! - * Retrieves the property specified with the csl option. - * - * @return The property specified with the csl option. - */ - std::string getCslProperty() const; - - /*! - * Retrieves whether the csl-file option was set. - * - * @return True iff the csl-file option was set. - */ - bool isCslFileSet() const; - - /*! - * Retrieves the name of the file that contains the CSL properties to be checked on the model. - * - * @return The name of the file that contains the CSL properties to be checked on the model. - */ - std::string getCslPropertiesFilename() const; - - /*! - * Retrieves whether the ltl option was set. - * - * @return True if the ltl option was set. - */ - bool isLtlPropertySet() const; - - /*! - * Retrieves the property specified with the ltl option. - * - * @return The property specified with the ltl option. - */ - std::string getLtlProperty() const; - - /*! - * Retrieves whether the ltl-file option was set. - * - * @return True iff the ltl-file option was set. - */ - bool isLtlFileSet() const; - - /*! - * Retrieves the name of the file that contains the LTL properties to be checked on the model. - * - * @return The name of the file that contains the LTL properties to be checked on the model. - */ - std::string getLtlPropertiesFilename() const; + std::string getPropertiesFilename() const; /*! * Retrieves whether the transition reward option was set. @@ -363,12 +307,8 @@ namespace storm { static const std::string explicitOptionShortName; static const std::string symbolicOptionName; static const std::string symbolicOptionShortName; - static const std::string pctlOptionName; - static const std::string pctlFileOptionName; - static const std::string cslOptionName; - static const std::string cslFileOptionName; - static const std::string ltlOptionName; - static const std::string ltlFileOptionName; + static const std::string propertyOptionName; + static const std::string propertyFileOptionName; static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; static const std::string counterexampleOptionName; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 013d3d77d..e89ff8a3c 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -53,6 +53,16 @@ namespace storm { return false; } + std::vector> Program::getUndefinedConstants() const { + std::vector> result; + for (auto const& constant : this->getConstants()) { + if (!constant.isDefined()) { + result.push_back(constant); + } + } + return result; + } + bool Program::hasConstant(std::string const& constantName) const { return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end(); } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 5e37f5095..5d108ea65 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -72,6 +72,13 @@ namespace storm { */ bool hasUndefinedConstants() const; + /*! + * Retrieves the undefined constants in the program. + * + * @return The undefined constants in the program. + */ + std::vector> getUndefinedConstants() const; + /*! * Retrieves whether the given constant exists in the program. * diff --git a/src/utility/cli.h b/src/utility/cli.h index 2f559277a..71067daf9 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -40,7 +40,10 @@ log4cplus::Logger logger; // Headers related to parsing. #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" -#include "src/parser/PrctlParser.h" +#include "src/parser/FormulaParser.h" + +// Formula headers. +#include "src/logic/Formulas.h" // Model headers. #include "src/models/AbstractModel.h" @@ -61,6 +64,7 @@ log4cplus::Logger logger; #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" // Headers related to exception handling. +#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidTypeException.h" @@ -290,7 +294,7 @@ namespace storm { return result; } - void generateCounterexample(std::shared_ptr> model, std::shared_ptr> const& formula) { + void generateCounterexample(std::shared_ptr> model, std::shared_ptr const& formula) { if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); @@ -324,21 +328,32 @@ namespace storm { // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { - STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); - std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty()); - generateCounterexample(model, filterFormula->getChild()); - } else if (settings.isPctlPropertySet()) { - std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - + STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseFromString(settings.getProperty()); + generateCounterexample(model, formula); + } else if (settings.isPropertySet()) { + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseFromString(storm::settings::generalSettings().getProperty()); + + std::cout << "Model checking property: " << *formula << " ..."; + std::unique_ptr result; if (model->getType() == storm::models::DTMC) { std::shared_ptr> dtmc = model->as>(); - modelchecker::prctl::SparseDtmcPrctlModelChecker modelchecker(*dtmc); - filterFormula->check(modelchecker); - } - if (model->getType() == storm::models::MDP) { + storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); + result = modelchecker.check(*formula); + } else if (model->getType() == storm::models::MDP) { std::shared_ptr> mdp = model->as>(); - modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(*mdp); - filterFormula->check(modelchecker); + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); + result = modelchecker.check(*formula); + } + if (result) { + std::cout << " done." << std::endl; + std::cout << "Result (initial states): "; + result->writeToStream(std::cout, model->getInitialStates()); + std::cout << std::endl << std::endl; + } else { + std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } } } diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 403e61db1..df2c40732 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/parser/AutoParser.h" @@ -16,34 +17,31 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - auto apFormula = std::make_shared>("observe0Greater1"); - auto eventuallyFormula = std::make_shared>(apFormula); + auto labelFormula = std::make_shared("observe0Greater1"); + auto eventuallyFormula = std::make_shared(labelFormula); - LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5..."); - std::vector result = eventuallyFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[0] - 0.2296800237), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - apFormula = std::make_shared>("observeIGreater1"); - eventuallyFormula = std::make_shared>(apFormula); + labelFormula = std::make_shared("observeIGreater1"); + eventuallyFormula = std::make_shared(labelFormula); - LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5..."); - result = eventuallyFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[0] - 0.05073232193), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - apFormula = std::make_shared>("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared>(apFormula); + labelFormula = std::make_shared("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared(labelFormula); - LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); - result = eventuallyFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); - - ASSERT_LT(std::abs(result[0] - 0.22742171078), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); } @@ -57,32 +55,30 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); - - LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8..."); - std::vector result = eventuallyFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); - ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); - apFormula = std::make_shared>("elected"); - auto boundedUntilFormula = std::make_shared>(std::make_shared>("true"), apFormula, 20); - - LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8..."); - result = boundedUntilFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[0] - 0.9993949793), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + result = checker.check(*boundedUntilFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8..."); - result = reachabilityRewardFormula->check(mc, false); - LOG4CPLUS_WARN(logger, "Done."); + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); - ASSERT_LT(std::abs(result[0] - 1.025106273), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + result = checker.check(*reachabilityRewardFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); } diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index a1e5dddf0..402eae502 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -3,6 +3,7 @@ #include "src/settings/SettingsManager.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/ExplicitQuantitativeCheckResult.h" #include "src/solver/NativeNondeterministicLinearEquationSolver.h" #include "src/parser/AutoParser.h" @@ -16,46 +17,59 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - auto apFormula = std::make_shared>("elected"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); - - ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision()); - - result = mc.checkOptimizingOperator(*eventuallyFormula, false); - - ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - apFormula = std::make_shared>("elected"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 25); + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); + EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false); + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - apFormula = std::make_shared>("elected"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[0] - 6.172433512), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[0] - 6.1724344), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); } TEST(SparseMdpPrctlModelCheckerTest, Consensus) { - // Increase the maximal number of iterations, because the solver does not converge otherwise. - // This is done in the main cpp unit - std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(abstractModel->getType(), storm::models::MDP); @@ -65,62 +79,81 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - - auto apFormula = std::make_shared>("finished"); - auto eventuallyFormula = std::make_shared>(apFormula); - - std::vector result = mc.checkOptimizingOperator(*eventuallyFormula, true); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); - ASSERT_LT(std::abs(result[31168] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + auto labelFormula = std::make_shared("finished"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - apFormula = std::make_shared>("finished"); - auto apFormula2 = std::make_shared>("all_coins_equal_0"); - auto andFormula = std::make_shared>(apFormula, apFormula2); - eventuallyFormula = std::make_shared>(andFormula); + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*eventuallyFormula, true); + EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[31168] - 0.4374282832), storm::settings::nativeEquationSolverSettings().getPrecision()); + labelFormula = std::make_shared("finished"); + auto labelFormula2 = std::make_shared("all_coins_equal_0"); + auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); + eventuallyFormula = std::make_shared(andFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - apFormula = std::make_shared>("finished"); - apFormula2 = std::make_shared>("all_coins_equal_1"); - andFormula = std::make_shared>(apFormula, apFormula2); - eventuallyFormula = std::make_shared>(andFormula); + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*eventuallyFormula, false); + EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[31168] - 0.5293286369), storm::settings::nativeEquationSolverSettings().getPrecision()); - - apFormula = std::make_shared>("finished"); - apFormula2 = std::make_shared>("agree"); - auto notFormula = std::make_shared>(apFormula2); - andFormula = std::make_shared>(apFormula, notFormula); - eventuallyFormula = std::make_shared>(andFormula); + labelFormula = std::make_shared("finished"); + labelFormula2 = std::make_shared("all_coins_equal_1"); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); + eventuallyFormula = std::make_shared(andFormula); + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - result = mc.checkOptimizingOperator(*eventuallyFormula, false); + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[31168] - 0.10414097), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + labelFormula2 = std::make_shared("agree"); + auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula); + eventuallyFormula = std::make_shared(andFormula); + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - apFormula = std::make_shared>("finished"); - auto boundedEventuallyFormula = std::make_shared>(apFormula, 50ull); + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true); + EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 50); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); - ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false); + EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision()); + labelFormula = std::make_shared("finished"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); - apFormula = std::make_shared>("finished"); - auto reachabilityRewardFormula = std::make_shared>(apFormula); + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true); - - ASSERT_LT(std::abs(result[31168] - 1725.593313), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false); + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - ASSERT_LT(std::abs(result[31168] - 2183.142422), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); }