diff --git a/examples/pdtmc/die/die.pm b/examples/pdtmc/die/die.pm index 84e466a18..032323827 100644 --- a/examples/pdtmc/die/die.pm +++ b/examples/pdtmc/die/die.pm @@ -26,8 +26,8 @@ rewards "coin_flips" endrewards label "one" = s=7&d=1; -//label "two" = s=7&d=2; -//label "three" = s=7&d=3; -//label "four" = s=7&d=4; -//label "five" = s=7&d=5; -//label "six" = s=7&d=6; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "four" = s=7&d=4; +label "five" = s=7&d=5; +label "six" = s=7&d=6; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 501fc097c..250083ea7 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1691,7 +1691,7 @@ namespace storm { modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp); + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); @@ -1776,20 +1776,20 @@ namespace storm { 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(); + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); - std::unique_ptr subResult = modelchecker.check(untilFormula.getSubformula()); + std::unique_ptr subResult = modelchecker.check(eventuallyFormula.getSubformula()); storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult(); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = subResult.getTruthValuesVector(); + psiStates = subResult->getTruthValuesVector(); } // Delegate the actual computation work to the function of equal name. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 17ddff695..621712f10 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -166,7 +166,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantativeResult<>().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -192,7 +192,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantativeResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -218,7 +218,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantativeResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } diff --git a/src/modelchecker/CheckResult.cpp b/src/modelchecker/CheckResult.cpp index 78fcf7d12..e646d4633 100644 --- a/src/modelchecker/CheckResult.cpp +++ b/src/modelchecker/CheckResult.cpp @@ -22,7 +22,11 @@ namespace storm { void CheckResult::complement() { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result."); } - + + std::unique_ptr CheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); + } + bool CheckResult::isExplicit() const { return false; } diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/CheckResult.h index 82baf0fa7..a4c4847db 100644 --- a/src/modelchecker/CheckResult.h +++ b/src/modelchecker/CheckResult.h @@ -21,7 +21,8 @@ namespace storm { virtual CheckResult& operator&=(CheckResult const& other); virtual CheckResult& operator|=(CheckResult const& other); virtual void complement(); - + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; + virtual bool isExplicit() const; virtual bool isQuantitative() const; virtual bool isQualitative() const; diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp index b688bb1d8..114819af6 100644 --- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp @@ -111,10 +111,18 @@ namespace storm { out << std::boolalpha; map_type const& map = boost::get(truthValues); + +#ifndef WINDOWS typename map_type::const_iterator it = map.begin(); typename map_type::const_iterator itPlusOne = map.begin(); ++itPlusOne; typename map_type::const_iterator ite = map.end(); +#else + map_type::const_iterator it = map.begin(); + map_type::const_iterator itPlusOne = map.begin(); + ++itPlusOne; + map_type::const_iterator ite = map.end(); +#endif for (; it != ite; ++itPlusOne, ++it) { out << it->second; diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp index 4b4a5d67d..f6d79429c 100644 --- a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp @@ -123,7 +123,7 @@ namespace storm { } template - std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { + std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { if (this->isResultForAllStates()) { vector_type const& valuesAsVector = boost::get(values); storm::storage::BitVector result(valuesAsVector.size()); @@ -188,9 +188,9 @@ namespace storm { } template<> - std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, storm::RationalFunction const& bound) const { + std::unique_ptr ExplicitQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { // Since it is not possible to compare rational functions against bounds, we simply call the base class method. - QuantitativeCheckResult::compareAgainstBound(comparisonType, bound); + return QuantitativeCheckResult::compareAgainstBound(comparisonType, bound); } template diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.h b/src/modelchecker/ExplicitQuantitativeCheckResult.h index ff9c95bae..699840c05 100644 --- a/src/modelchecker/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/ExplicitQuantitativeCheckResult.h @@ -34,7 +34,7 @@ namespace storm { ValueType& operator[](storm::storage::sparse::state_type state); ValueType const& operator[](storm::storage::sparse::state_type state) const; - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override; + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; virtual bool isExplicit() const override; virtual bool isResultForAllStates() const override; diff --git a/src/modelchecker/QuantitativeCheckResult.cpp b/src/modelchecker/QuantitativeCheckResult.cpp index c6db27a49..df03db786 100644 --- a/src/modelchecker/QuantitativeCheckResult.cpp +++ b/src/modelchecker/QuantitativeCheckResult.cpp @@ -8,11 +8,6 @@ namespace storm { namespace modelchecker { - template - std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); - } - template bool QuantitativeCheckResult::isQuantitative() const { return true; diff --git a/src/modelchecker/QuantitativeCheckResult.h b/src/modelchecker/QuantitativeCheckResult.h index 7cd9d2e73..73eda6c6a 100644 --- a/src/modelchecker/QuantitativeCheckResult.h +++ b/src/modelchecker/QuantitativeCheckResult.h @@ -8,8 +8,6 @@ namespace storm { template class QuantitativeCheckResult : public CheckResult { public: - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const; - virtual bool isQuantitative() const override; }; } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 14cc4c0d9..dbc50eb74 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include +#include #ifdef PARAMETRIC_SYSTEMS #include "src/storage/parameters.h" diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index 6cc8aaeb2..f2480e029 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -7,24 +7,11 @@ namespace storm { namespace modules { const std::string ParametricSettings::moduleName = "parametric"; - const std::string ParametricSettings::eliminationMethodOptionName = "method"; - const std::string ParametricSettings::eliminationOrderOptionName = "order"; - const std::string ParametricSettings::entryStatesLastOptionName = "entrylast"; - const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize"; const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy"; const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path"; const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile"; ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { - std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("bw").build()).build()); - - std::vector methods = {"state", "hybrid"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build()); - - this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.") @@ -33,42 +20,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); } - ParametricSettings::EliminationMethod ParametricSettings::getEliminationMethod() const { - std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString(); - if (eliminationMethodAsString == "state") { - return EliminationMethod::State; - } else if (eliminationMethodAsString == "hybrid") { - return EliminationMethod::Hybrid; - } else { - STORM_LOG_ASSERT(false, "Illegal elimination method selected."); - } - } - - ParametricSettings::EliminationOrder ParametricSettings::getEliminationOrder() const { - std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString(); - if (eliminationOrderAsString == "fw") { - return EliminationOrder::Forward; - } else if (eliminationOrderAsString == "fwrev") { - return EliminationOrder::ForwardReversed; - } else if (eliminationOrderAsString == "bw") { - return EliminationOrder::Backward; - } else if (eliminationOrderAsString == "bwrev") { - return EliminationOrder::BackwardReversed; - } else if (eliminationOrderAsString == "rand") { - return EliminationOrder::Random; - } else { - STORM_LOG_ASSERT(false, "Illegal elimination order selected."); - } - } - - bool ParametricSettings::isEliminateEntryStatesLastSet() const { - return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet(); - } - - uint_fast64_t ParametricSettings::getMaximalSccSize() const { - return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger(); - } - bool ParametricSettings::exportResultToFile() const { return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h index bb137cdeb..3586e2d5f 100644 --- a/src/settings/modules/ParametricSettings.h +++ b/src/settings/modules/ParametricSettings.h @@ -21,16 +21,6 @@ namespace storm { * RATIONAL_FUNCTION: The smt file should contain only the rational function. */ enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION}; - - /*! - * An enum that contains all available state elimination orders. - */ - enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random }; - - /*! - * An enum that contains all available techniques to solve parametric systems. - */ - enum class EliminationMethod { State, Scc, Hybrid}; /*! * Creates a new set of parametric model checking settings that is managed by the given manager. @@ -38,34 +28,6 @@ namespace storm { * @param settingsManager The responsible manager. */ ParametricSettings(storm::settings::SettingsManager& settingsManager); - - /*! - * Retrieves the selected elimination method. - * - * @return The selected elimination method. - */ - EliminationMethod getEliminationMethod() const; - - /*! - * Retrieves the selected elimination order. - * - * @return The selected elimination order. - */ - EliminationOrder getEliminationOrder() const; - - /*! - * Retrieves whether the option to eliminate entry states in the very end is set. - * - * @return True iff the option is set. - */ - bool isEliminateEntryStatesLastSet() const; - - /*! - * Retrieves the maximal size of an SCC on which state elimination is to be directly applied. - * - * @return The maximal size of an SCC on which state elimination is to be directly applied. - */ - uint_fast64_t getMaximalSccSize() const; /** * Retrieves whether the model checking result should be exported to a file. @@ -100,10 +62,6 @@ namespace storm { const static std::string moduleName; private: - const static std::string eliminationMethodOptionName; - const static std::string eliminationOrderOptionName; - const static std::string entryStatesLastOptionName; - const static std::string maximalSccSizeOptionName; const static std::string encodeSmt2StrategyOptionName; const static std::string exportSmt2DestinationPathOptionName; const static std::string exportResultDestinationPathOptionName; diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 9627c8dea..16610f4ad 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -191,6 +191,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_MSAT @@ -218,6 +219,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } +#endif storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index badca77a8..a1ec0810b 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -79,7 +79,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 7425e8187..475c3ee95 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -70,9 +70,15 @@ namespace storm { virtual ~SmtSolver(); SmtSolver(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver(SmtSolver&& other) = default; +#endif SmtSolver& operator=(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver& operator=(SmtSolver&& other) = default; +#endif /*! * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those @@ -146,8 +152,10 @@ namespace storm { * @param assumptions The assumptions to add to the call. * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. - */ + */ +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) = 0; +#endif /*! * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 0e89d1d6c..b8b93431a 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -155,6 +155,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_Z3 @@ -181,7 +182,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - +#endif storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_Z3 @@ -229,7 +230,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); + this->allSat(important, static_cast>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; })); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 1e0fd2a43..1873cb4df 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -51,7 +51,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index b928907e6..205012331 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -325,4 +325,14 @@ namespace storm { } } +//specialize +namespace std { + template<> + struct less < storm::expressions::Expression > { + bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const { + return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer(); + } + }; +} + #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index 3b675a60d..b48c53d09 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -18,8 +18,10 @@ namespace storm { VariableCoefficients(VariableCoefficients const& other) = default; VariableCoefficients& operator=(VariableCoefficients const& other) = default; +#ifndef WINDOWS VariableCoefficients(VariableCoefficients&& other) = default; VariableCoefficients& operator=(VariableCoefficients&& other) = default; +#endif VariableCoefficients& operator+=(VariableCoefficients&& other); VariableCoefficients& operator-=(VariableCoefficients&& other); diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index a3940e8c5..a38311344 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include +#include // Include other headers. #include "src/exceptions/BaseException.h" @@ -12,10 +13,9 @@ //#include "src/modelchecker/reachability/DirectEncoding.h" #include "src/storage/DeterministicModelBisimulationDecomposition.h" -#include "src/modelchecker/reachability/SparseSccModelChecker.h" +#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/storage/parameters.h" #include "src/models/Dtmc.h" -#include "src/properties/prctl/PrctlFilter.h" //std::tuple>, boost::optional>, boost::optional, boost::optional, boost::optional> computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula) { // // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract @@ -145,7 +145,14 @@ void check() { std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename(); std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, true, false, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants); + + STORM_LOG_THROW(storm::settings::generalSettings().isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); + std::shared_ptr formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); + + typename storm::builder::ExplicitPrismModelBuilder::Options options(*formula); + options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); model->printModelInformationToStream(std::cout); @@ -155,47 +162,57 @@ void check() { std::shared_ptr> dtmc = model->template as>(); - STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); - std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - std::cout << "Checking formula " << *filterFormula << std::endl; + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + STORM_LOG_THROW(modelchecker.canHandle(*formula), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula << "'."); - bool checkRewards = false; - std::shared_ptr> phiStateFormulaApFormula = nullptr; - std::shared_ptr> psiStateFormulaApFormula = nullptr; + std::cout << "Checking formula " << *formula << std::endl; - // The first thing we need to do is to make sure the formula is of the correct form. - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - std::shared_ptr> phiStateFormula; - std::shared_ptr> psiStateFormula; - if (untilFormula) { - phiStateFormula = untilFormula->getLeft(); - psiStateFormula = untilFormula->getRight(); - } else { - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - if (eventuallyFormula) { - - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = eventuallyFormula->getChild(); - } else { - std::shared_ptr> reachabilityRewardFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - - STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted."); - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = reachabilityRewardFormula->getChild(); - checkRewards = true; + bool checkRewards = formula->isRewardOperatorFormula(); + + std::string phiLabel; + std::string psiLabel; + + bool measureDrivenBisimulation = false; + if (formula->isProbabilityOperatorFormula()) { + storm::logic::Formula const& subformula = formula->asProbabilityOperatorFormula().getSubformula(); + + if (subformula.isEventuallyFormula()) { + phiLabel = "true"; + std::stringstream stream; + stream << subformula.asEventuallyFormula().getSubformula(); + psiLabel = stream.str(); + measureDrivenBisimulation = true; + } else if (subformula.isUntilFormula()) { + std::stringstream stream; + stream << subformula.asUntilFormula().getLeftSubformula(); + phiLabel = stream.str(); + + std::stringstream stream2; + stream2 << subformula.asUntilFormula().getRightSubformula(); + psiLabel = stream2.str(); + measureDrivenBisimulation = true; + } + } else if (formula->isRewardOperatorFormula()) { + storm::logic::Formula const& subformula = formula->asRewardOperatorFormula().getSubformula(); + + if (subformula.isReachabilityRewardFormula()) { + phiLabel = "true"; + std::stringstream stream; + stream << subformula.asReachabilityRewardFormula().getSubformula(); + psiLabel = stream.str(); + measureDrivenBisimulation = true; } } - // Now we need to make sure the formulas defining the phi and psi states are just labels. - phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); - psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); - STORM_LOG_THROW(phiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - STORM_LOG_THROW(psiStateFormulaApFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - // Perform bisimulation minimization if requested. if (storm::settings::generalSettings().isBisimulationSet()) { - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); - dtmc = bisimulationDecomposition.getQuotient()->template as>(); + if (measureDrivenBisimulation) { + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiLabel, psiLabel, checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); + dtmc = bisimulationDecomposition.getQuotient()->template as>(); + } else { + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + dtmc = bisimulationDecomposition.getQuotient()->template as>(); + } dtmc->printModelInformationToStream(std::cout); } @@ -205,15 +222,14 @@ void check() { // storm::modelchecker::reachability::CollectConstraints constraintCollector; // constraintCollector(*dtmc); - storm::modelchecker::reachability::SparseSccModelChecker modelchecker; - - ValueType valueFunction = modelchecker.computeConditionalProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); - // storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); - - STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl); + std::unique_ptr result = modelchecker.check(*formula); + + // Report the result. + STORM_PRINT_AND_LOG(std::endl << "Result: " << std::endl); + result->writeToStream(std::cout, model->getInitialStates()); if (std::is_same::value) { - printApproximateResult(valueFunction); + printApproximateResult(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]); } }