diff --git a/CHANGELOG.md b/CHANGELOG.md index fc6acc2cd..4453f0ed1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,9 +12,12 @@ Version 1.3.x - Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the --qvbs option. - Added script resources/examples/download_qvbs.sh to download the QVBS. - If an option is unknown, Storm now prints a hint to similar option names. -- Allow bounded types for constants in JANI. +- JANI: Allow bounded types for constants +- JANI: Support for non-trivial reward accumulations. +- JANI: Fixed support for reward expressions over non-transient variables. - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial) - Fixed linking with Mathsat on macOS +- Fixed compilation for macOS mojave ### Version 1.3.0 (2018/12) - Slightly improved scheduler extraction diff --git a/resources/3rdparty/cpptemplate/cpptempl.h b/resources/3rdparty/cpptemplate/cpptempl.h index b6a19d293..28c289a10 100755 --- a/resources/3rdparty/cpptemplate/cpptempl.h +++ b/resources/3rdparty/cpptemplate/cpptempl.h @@ -126,6 +126,7 @@ namespace cpptempl class Data { public: + virtual ~Data() {} virtual bool empty() = 0 ; virtual std::string getvalue(); virtual data_list& getlist(); @@ -192,6 +193,7 @@ namespace cpptempl class Token { public: + virtual ~Token() {}; virtual TokenType gettype() = 0 ; virtual void gettext(std::ostream &stream, data_map &data) = 0 ; virtual void set_children(token_vector &children); diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index 3030f44b3..9aafb98b4 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -28,13 +28,19 @@ if (NOT STORM_PORTABLE) set(STORM_CUDD_FLAGS "${STORM_CUDD_FLAGS} -march=native") endif() +# Set sysroot to circumvent problems in macOS "Mojave" where the header files are no longer in /usr/include +set(CUDD_INCLUDE_FLAGS "") +if (CMAKE_OSX_SYSROOT) + set(CUDD_INCLUDE_FLAGS "CPPFLAGS=--sysroot=${CMAKE_OSX_SYSROOT}") +endif() + ExternalProject_Add( cudd3 DOWNLOAD_COMMAND "" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0 PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 PATCH_COMMAND ${AUTORECONF} - CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} + CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} ${CUDD_INCLUDE_FLAGS} BUILD_COMMAND make ${STORM_CUDD_FLAGS} INSTALL_COMMAND make install BUILD_IN_SOURCE 0 diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index ae69cc1e2..1d71c3639 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -633,7 +633,12 @@ namespace storm { for (auto const& property : properties) { printModelCheckingProperty(property); storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); + std::unique_ptr result; + try { + result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); + } catch (storm::exceptions::BaseException const& ex) { + STORM_LOG_WARN("Cannot handle property: " << ex.what()); + } watch.stop(); postprocessingCallback(result); printResult(result, property, &watch); diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index e8218cc4e..2a467a27a 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -89,6 +89,7 @@ namespace storm { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); + STORM_LOG_WARN_COND(version >= 1 && version <=1, "JANI Version " << version << " is not supported. Results may be wrong."); //name STORM_LOG_THROW(parsedStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "A model must have a (single) name"); std::string name = getString(parsedStructure.at("name"), "model name"); @@ -205,11 +206,7 @@ namespace storm { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { try { - nonTrivialRewardModelExpressions.clear(); - auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); - for (auto const& nonTrivRewExpr : nonTrivialRewardModelExpressions) { - model.addNonTrivialRewardExpression(nonTrivRewExpr.first, nonTrivRewExpr.second); - } + auto prop = this->parseProperty(model, propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); // Eliminate reward accumulations as much as possible rewAccEliminator.eliminateRewardAccumulations(prop); properties.push_back(prop); @@ -222,18 +219,16 @@ namespace storm { } return {model, properties}; } - - std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { + std::vector> JaniParser::parseUnaryFormulaArgument(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description); - return { parseFormula(propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) }; + return { parseFormula(model, propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - - std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { + std::vector> JaniParser::parseBinaryFormulaArguments(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description); STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description); - return { parseFormula(propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) }; + return { parseFormula(model, propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(model, propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure, Scope const& scope) { @@ -277,7 +272,20 @@ namespace storm { return storm::logic::RewardAccumulation(accSteps, accTime, accExit); } - std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound) { + void insertLowerUpperTimeBounds(std::vector>& lowerBounds, std::vector>& upperBounds, storm::jani::PropertyInterval const& pi) { + if (pi.hasLowerBound()) { + lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); + } else { + lowerBounds.push_back(boost::none); + } + if (pi.hasUpperBound()) { + upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); + } else { + upperBounds.push_back(boost::none); + } + } + + std::shared_ptr JaniParser::parseFormula(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound) { if (propertyStructure.is_boolean()) { return std::make_shared(propertyStructure.get()); } @@ -305,7 +313,7 @@ namespace storm { std::string opString = getString(propertyStructure.at("op"), "Operation description"); if(opString == "Pmin" || opString == "Pmax") { - std::vector> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); + std::vector> args = parseUnaryFormulaArgument(model, propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; @@ -314,8 +322,9 @@ namespace storm { } else if (opString == "∀" || opString == "∃") { assert(bound == boost::none); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description); } else if (opString == "Emin" || opString == "Emax") { + STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Model not compliant: Contains Emin/Emax property in " << scope.description << "."); STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description); storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), scope.refine("Reward expression")); STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description); @@ -337,7 +346,7 @@ namespace storm { storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant")); if (!rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + model.addNonTrivialRewardExpression(rewardName, rewExpr); } if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo); @@ -348,7 +357,7 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description); storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant")); if (!rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + model.addNonTrivialRewardExpression(rewardName, rewExpr); } if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo); @@ -361,17 +370,23 @@ namespace storm { for (auto const& rewInst : propertyStructure.at("reward-instants")) { storm::expressions::Expression rewInstRewardModelExpression = parseExpression(rewInst.at("exp"), scope.refine("Reward expression at reward instant")); STORM_LOG_THROW(rewInstRewardModelExpression.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewInstRewardModelExpression << "' does not have numerical type in " << scope.description); - std::string rewInstRewardModelName = rewInstRewardModelExpression.toString(); - if (!rewInstRewardModelExpression.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewInstRewardModelName, rewInstRewardModelExpression); - } storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rewInst.at("accumulate"), scope.description); - boundReferences.emplace_back(rewInstRewardModelName, boundRewardAccumulation); + bool steps = (boundRewardAccumulation.isStepsSet() || boundRewardAccumulation.isExitSet()) && boundRewardAccumulation.size() == 1; + bool time = boundRewardAccumulation.isTimeSet() && boundRewardAccumulation.size() == 1 && !model.isDiscreteTimeModel(); + if ((steps || time) && !rewInstRewardModelExpression.containsVariables() && storm::utility::isOne(rewInstRewardModelExpression.evaluateAsRational())) { + boundReferences.emplace_back(steps ? storm::logic::TimeBoundType::Steps : storm::logic::TimeBoundType::Time); + } else { + std::string rewInstRewardModelName = rewInstRewardModelExpression.toString(); + if (!rewInstRewardModelExpression.isVariable()) { + model.addNonTrivialRewardExpression(rewInstRewardModelName, rewInstRewardModelExpression); + } + boundReferences.emplace_back(rewInstRewardModelName, boundRewardAccumulation); + } storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant")); bounds.emplace_back(false, rewInstantExpr); } if (!rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + model.addNonTrivialRewardExpression(rewardName, rewExpr); } return std::make_shared(std::make_shared(bounds, boundReferences, rewardAccumulation), rewardName, opInfo); } else { @@ -379,7 +394,7 @@ namespace storm { std::shared_ptr subformula; if (propertyStructure.count("reach") > 0) { auto formulaContext = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward; - subformula = std::make_shared(parseFormula(propertyStructure.at("reach"), formulaContext, scope.refine("Reach-expression of operator " + opString)), formulaContext, rewardAccumulation); + subformula = std::make_shared(parseFormula(model, propertyStructure.at("reach"), formulaContext, scope.refine("Reach-expression of operator " + opString)), formulaContext, rewardAccumulation); } else { subformula = std::make_shared(rewardAccumulation); } @@ -388,7 +403,7 @@ namespace storm { return std::make_shared(subformula, opInfo); } else { if (!rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + model.addNonTrivialRewardExpression(rewardName, rewExpr); } return std::make_shared(subformula, rewardName, opInfo); } @@ -397,29 +412,35 @@ namespace storm { storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Smin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; - + // Reward accumulation is optional as it was not available in the early days... + boost::optional rewardAccumulation; + if (propertyStructure.count("accumulate") > 0) { + STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Unexpected accumulate field in " << scope.description << "."); + rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); + } STORM_LOG_THROW(propertyStructure.count("exp") > 0, storm::exceptions::InvalidJaniException, "Expected an expression at steady state property at " << scope.description); - auto rewExpr = parseExpression(propertyStructure["exp"], scope.refine("steady-state operator"), true); - if (!rewExpr.isInitialized() || rewExpr.hasBooleanType()) { - std::shared_ptr subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; + auto exp = parseExpression(propertyStructure["exp"], scope.refine("steady-state operator"), true); + if (!exp.isInitialized() || exp.hasBooleanType()) { + STORM_LOG_THROW(!rewardAccumulation.is_initialized(), storm::exceptions::InvalidJaniException, "Long-run average probabilities are not allowed to have a reward accumulation at" << scope.description); + std::shared_ptr subformula = parseUnaryFormulaArgument(model, propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; return std::make_shared(subformula, opInfo); } - STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description); - std::string rewardName = rewExpr.toString(); - if (!rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + STORM_LOG_THROW(exp.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << exp << "' does not have numerical type in " << scope.description); + std::string rewardName = exp.toString(); + if (!exp.isVariable()) { + model.addNonTrivialRewardExpression(rewardName, exp); } - auto subformula = std::make_shared(); + auto subformula = std::make_shared(rewardAccumulation); return std::make_shared(subformula, rewardName, opInfo); } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector> args; if (opString == "U") { - args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); + args = parseBinaryFormulaArguments(model, propertyStructure, formulaContext, opString, scope); } else { assert(opString == "F"); - args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope); + args = parseUnaryFormulaArgument(model, propertyStructure, formulaContext, opString, scope); args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } @@ -427,56 +448,35 @@ namespace storm { std::vector> lowerBounds, upperBounds; std::vector tbReferences; if (propertyStructure.count("step-bounds") > 0) { + STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Jani model not compliant: Contains step-bounds in " << scope.description << "."); storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"), scope.refine("step-bounded until").clearVariables()); - boost::optional lowerBound, upperBound; - if (pi.hasLowerBound()) { - lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); - } else { - lowerBounds.push_back(boost::none); - } - if (pi.hasUpperBound()) { - upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); - } else { - upperBounds.push_back(boost::none); - } + insertLowerUpperTimeBounds(lowerBounds, upperBounds, pi); tbReferences.emplace_back(storm::logic::TimeBoundType::Steps); } if (propertyStructure.count("time-bounds") > 0) { + STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Jani model not compliant: Contains time-bounds in " << scope.description << "."); storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"), scope.refine("time-bounded until").clearVariables()); - boost::optional lowerBound, upperBound; - if (pi.hasLowerBound()) { - lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); - } else { - lowerBounds.push_back(boost::none); - } - if (pi.hasUpperBound()) { - upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); - } else { - upperBounds.push_back(boost::none); - } + insertLowerUpperTimeBounds(lowerBounds, upperBounds, pi); tbReferences.emplace_back(storm::logic::TimeBoundType::Time); } if (propertyStructure.count("reward-bounds") > 0 ) { for (auto const& rbStructure : propertyStructure.at("reward-bounds")) { storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"), scope.refine("reward-bounded until").clearVariables()); + insertLowerUpperTimeBounds(lowerBounds, upperBounds, pi); STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description); storm::expressions::Expression rewInstRewardModelExpression = parseExpression(rbStructure.at("exp"), scope.refine("Reward expression at reward-bounds")); STORM_LOG_THROW(rewInstRewardModelExpression.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewInstRewardModelExpression << "' does not have numerical type in " << scope.description); - std::string rewInstRewardModelName = rewInstRewardModelExpression.toString(); - if (!rewInstRewardModelExpression.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewInstRewardModelName, rewInstRewardModelExpression); - } storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), scope.description); - tbReferences.emplace_back(rewInstRewardModelName, boundRewardAccumulation); - if (pi.hasLowerBound()) { - lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); + bool steps = (boundRewardAccumulation.isStepsSet() || boundRewardAccumulation.isExitSet()) && boundRewardAccumulation.size() == 1; + bool time = boundRewardAccumulation.isTimeSet() && boundRewardAccumulation.size() == 1 && !model.isDiscreteTimeModel(); + if ((steps || time) && !rewInstRewardModelExpression.containsVariables() && storm::utility::isOne(rewInstRewardModelExpression.evaluateAsRational())) { + tbReferences.emplace_back(steps ? storm::logic::TimeBoundType::Steps : storm::logic::TimeBoundType::Time); } else { - lowerBounds.push_back(boost::none); - } - if (pi.hasUpperBound()) { - upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); - } else { - upperBounds.push_back(boost::none); + std::string rewInstRewardModelName = rewInstRewardModelExpression.toString(); + if (!rewInstRewardModelExpression.isVariable()) { + model.addNonTrivialRewardExpression(rewInstRewardModelName, rewInstRewardModelExpression); + } + tbReferences.emplace_back(rewInstRewardModelName, boundRewardAccumulation); } } } @@ -489,15 +489,15 @@ namespace storm { } } else if (opString == "G") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Subformula of globally operator ")); + std::vector> args = parseUnaryFormulaArgument(model, propertyStructure, formulaContext, opString, scope.refine("Subformula of globally operator ")); if (propertyStructure.count("step-bounds") > 0) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported."); } else if (propertyStructure.count("time-bounds") > 0) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by storm"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported."); } else if (propertyStructure.count("reward-bounds") > 0 ) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and reward bounded properties are not supported."); } - return std::make_shared(args[1]); + return std::make_shared(args[0]); } else if (opString == "W") { assert(bound == boost::none); @@ -507,19 +507,19 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); } else if (opString == "∧" || opString == "∨") { assert(bound == boost::none); - std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); + std::vector> args = parseBinaryFormulaArguments(model, propertyStructure, formulaContext, opString, scope); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared(oper, args[0], args[1]); } else if (opString == "⇒") { assert(bound == boost::none); - std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); + std::vector> args = parseBinaryFormulaArguments(model, propertyStructure, formulaContext, opString, scope); assert(args.size() == 2); std::shared_ptr tmp = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); return std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, tmp, args[1]); } else if (opString == "¬") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope); + std::vector> args = parseUnaryFormulaArgument(model, propertyStructure, formulaContext, opString, scope); assert(args.size() == 1); return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); } else if (!expr.isInitialized() && (opString == "≥" || opString == "≤" || opString == "<" || opString == ">" || opString == "=" || opString == "≠")) { @@ -558,10 +558,10 @@ namespace storm { ct = storm::logic::ComparisonType::Less; } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported in " << scope.description << "."); } } - return parseFormula(propertyStructure.at(leftRight[i]), formulaContext, scope, storm::logic::Bound(ct, boundExpr)); + return parseFormula(model, propertyStructure.at(leftRight[i]), formulaContext, scope, storm::logic::Bound(ct, boundExpr)); } } } @@ -576,7 +576,7 @@ namespace storm { } } - storm::jani::Property JaniParser::parseProperty(json const& propertyStructure, Scope const& scope) { + storm::jani::Property JaniParser::parseProperty(storm::jani::Model& model, json const& propertyStructure, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name std::string name = getString(propertyStructure.at("name"), "property-name"); @@ -629,7 +629,7 @@ namespace storm { if (!statesFormula) { try { // Try to parse the states as formula. - statesFormula = parseFormula(expressionStructure.at("states"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); + statesFormula = parseFormula(model, expressionStructure.at("states"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); } catch (storm::exceptions::NotSupportedException const& ex) { throw ex; } catch (storm::exceptions::NotImplementedException const& ex) { @@ -638,7 +638,7 @@ namespace storm { } STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); - auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); + auto formula = parseFormula(model, expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, comment); } diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 93e1a5790..aacd90cc4 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -75,7 +75,7 @@ namespace storm { }; std::pair> parseModel(bool parseProperties = true); - storm::jani::Property parseProperty(json const& propertyStructure, Scope const& scope); + storm::jani::Property parseProperty(storm::jani::Model& model, json const& propertyStructure, Scope const& scope); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, Scope const& scope); struct ParsedType { enum class BasicType {Bool, Int, Real}; @@ -97,13 +97,13 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound = boost::none); + std::shared_ptr parseFormula(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound = boost::none); std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); - std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); - std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); + std::vector> parseUnaryFormulaArgument(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); + std::vector> parseBinaryFormulaArguments(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, Scope const& scope); storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context); @@ -122,7 +122,6 @@ namespace storm { std::shared_ptr expressionManager; std::set labels = {}; - std::unordered_map nonTrivialRewardModelExpressions; bool allowRecursion = true; diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 7f074a3d4..699787ee8 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1452,7 +1452,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of type " << modelType << "."); } } else { - return ActionDd(this->variables.manager->template getBddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); + return ActionDd(this->variables.manager->getBddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); } } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 7b12a4f96..185ebfa44 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -43,7 +43,7 @@ namespace storm { JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false) { STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); - auto features = model.getModelFeatures(); + auto features = this->model.getModelFeatures(); features.remove(storm::jani::ModelFeature::DerivedOperators); features.remove(storm::jani::ModelFeature::StateExitRewards); // Eliminate arrays if necessary. @@ -72,15 +72,15 @@ namespace storm { this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData); // Create a proper evalator. - this->evaluator = std::make_unique>(model.getManager()); + this->evaluator = std::make_unique>(this->model.getManager()); this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); if (this->options.isBuildAllRewardModelsSet()) { - rewardExpressions = model.getAllRewardModelExpressions(); + rewardExpressions = this->model.getAllRewardModelExpressions(); } else { // Extract the reward models from the model based on the names we were given. for (auto const& rewardModelName : this->options.getRewardModelNames()) { - rewardExpressions.emplace_back(rewardModelName, model.getRewardModelExpression(rewardModelName)); + rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName)); } } @@ -96,9 +96,9 @@ namespace storm { // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression // for the label so we can cut off the exploration there. if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") { - STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); + STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); - storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel()); + storm::jani::Variable const& variable = this->model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel()); STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 4bda466c4..b669e75bd 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -206,9 +206,10 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(LongRunAverageRewardFormula const&, boost::any const& data) const { + boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); + bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); + return result && inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); } boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/LongRunAverageRewardFormula.cpp b/src/storm/logic/LongRunAverageRewardFormula.cpp index fc7edd7fe..c36dab8a9 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.cpp +++ b/src/storm/logic/LongRunAverageRewardFormula.cpp @@ -4,7 +4,7 @@ namespace storm { namespace logic { - LongRunAverageRewardFormula::LongRunAverageRewardFormula() { + LongRunAverageRewardFormula::LongRunAverageRewardFormula(boost::optional rewardAccumulation) : rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } @@ -16,12 +16,25 @@ namespace storm { return true; } + bool LongRunAverageRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& LongRunAverageRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out) const { - return out << "LRA"; + out << "LRA"; + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } + return out; } + } } diff --git a/src/storm/logic/LongRunAverageRewardFormula.h b/src/storm/logic/LongRunAverageRewardFormula.h index 545dd0b57..03f1c3684 100644 --- a/src/storm/logic/LongRunAverageRewardFormula.h +++ b/src/storm/logic/LongRunAverageRewardFormula.h @@ -1,13 +1,15 @@ #ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ #define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_ +#include #include "storm/logic/PathFormula.h" +#include "storm/logic/RewardAccumulation.h" namespace storm { namespace logic { class LongRunAverageRewardFormula : public PathFormula { public: - LongRunAverageRewardFormula(); + LongRunAverageRewardFormula(boost::optional rewardAccumulation = boost::none); virtual ~LongRunAverageRewardFormula() { // Intentionally left empty. @@ -15,11 +17,15 @@ namespace storm { virtual bool isLongRunAverageRewardFormula() const override; virtual bool isRewardPathFormula() const override; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - + + private: + boost::optional rewardAccumulation; }; } } diff --git a/src/storm/logic/RewardAccumulation.cpp b/src/storm/logic/RewardAccumulation.cpp index 4a4ba4366..8cdbce70f 100644 --- a/src/storm/logic/RewardAccumulation.cpp +++ b/src/storm/logic/RewardAccumulation.cpp @@ -23,6 +23,10 @@ namespace storm { return !isStepsSet() && !isTimeSet() && !isExitSet(); } + uint64_t RewardAccumulation::size() const { + return (isStepsSet() ? 1 : 0) + (isTimeSet() ? 1 : 0) + (isExitSet() ? 1 : 0); + } + std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) { bool hasEntry = false; if (acc.isStepsSet()) { diff --git a/src/storm/logic/RewardAccumulation.h b/src/storm/logic/RewardAccumulation.h index 4f8a50b29..673694ba3 100644 --- a/src/storm/logic/RewardAccumulation.h +++ b/src/storm/logic/RewardAccumulation.h @@ -16,6 +16,9 @@ namespace storm { // Returns true iff accumulation for all types of reward is disabled. bool isEmpty() const; + // Returns the number of types of rewards that are enabled. + uint64_t size() const; + private: bool time, steps, exit; }; diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 374e49f94..9169b89f4 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -91,6 +91,16 @@ namespace storm { return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); } + boost::any RewardAccumulationEliminationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); + auto rewName = boost::any_cast>(data); + if (!f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) { + return std::static_pointer_cast(std::make_shared()); + } else { + return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); + } + } + boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h index 59dbc330d..e5e78c04e 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.h +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h @@ -26,6 +26,7 @@ namespace storm { virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp index 6136581a3..4d1df7e0d 100644 --- a/src/storm/logic/TotalRewardFormula.cpp +++ b/src/storm/logic/TotalRewardFormula.cpp @@ -30,6 +30,9 @@ namespace storm { std::ostream& TotalRewardFormula::writeToStream(std::ostream& out) const { out << "C"; + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } return out; } } diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 6e41f2782..b6d65edf0 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -10,6 +10,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/logic/FragmentSpecification.h" @@ -31,7 +32,7 @@ namespace storm { template::SupportsExponential, int>::type> bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTimeOperatorsAllowed(true).setRewardAccumulationAllowed(true)); } template @@ -66,8 +67,8 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - - return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } template @@ -117,7 +118,8 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on CTMCs are not supported."); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); } template @@ -131,7 +133,8 @@ namespace storm { template std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel("")); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get()); } // Explicitly instantiate the model checker. diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index cf2aa5bcb..d084a42e4 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/utility/graph.h" #include "storm/utility/solver.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -37,7 +38,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true).setRewardAccumulationAllowed(true)); } template @@ -103,7 +104,8 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on CTMCs are not supported."); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -112,14 +114,15 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModel.get(), checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -137,7 +140,8 @@ namespace storm { template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), probabilityMatrix, checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), &this->getModel().getExitRateVector()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), probabilityMatrix, rewardModel.get(), &this->getModel().getExitRateVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 3a21d36db..7da489e01 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -6,6 +6,7 @@ #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/utility/macros.h" #include "storm/settings/SettingsManager.h" @@ -35,7 +36,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseMarkovAutomatonCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { + if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -105,8 +106,9 @@ namespace storm { STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector()); + + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModel.get(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -115,7 +117,8 @@ namespace storm { std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTotalRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel("")); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTotalRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModel.get()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -136,7 +139,8 @@ namespace storm { std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long run average rewards in non-closed Markov automaton."); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getUniqueRewardModel()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModel.get()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 476c3cf2c..a6bee0577 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -413,7 +413,7 @@ namespace storm { uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); // Start by decomposing the CTMC into its BSCCs. - storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs."); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index b2fcad350..f813564c2 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -244,8 +244,7 @@ namespace storm { storm::storage::BitVector probabilisticStates = ~markovianStates; // Searching for SCCs in probabilistic fragment to decide which algorithm is applied. - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, probabilisticStates, true, false); - bool cycleFree = sccDecomposition.empty(); + bool cycleFree = !storm::utility::graph::hasCycle(transitionMatrix, probabilisticStates); // Vectors to store computed vectors. UnifPlusVectors unifVectors; diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 0654a9788..ecd57182f 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -8,6 +8,7 @@ #include "storm/utility/macros.h" #include "storm/utility/graph.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -33,7 +34,7 @@ namespace storm { template bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } template @@ -78,7 +79,8 @@ namespace storm { std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); } template @@ -93,7 +95,8 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } template @@ -117,7 +120,8 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel("")); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get()); } template class HybridDtmcPrctlModelChecker>; diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 9af47c767..270e99c47 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -19,6 +19,7 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/settings/modules/GeneralSettings.h" @@ -39,7 +40,7 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -98,7 +99,8 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); } template @@ -115,7 +117,8 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 7c11c31b8..9896f8ce4 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -4,6 +4,7 @@ #include #include "storm/utility/macros.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -33,7 +34,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else if (formula.isInFragment(storm::logic::quantiles())) { if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; @@ -101,6 +102,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); storm::logic::OperatorInformation opInfo; if (checkTask.isBoundSet()) { opInfo.bound = checkTask.getBound(); @@ -110,7 +112,8 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } @@ -128,7 +131,8 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -143,7 +147,8 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.getHint()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -158,7 +163,8 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), nullptr); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), nullptr); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index bd2dfd326..79e0a433b 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -40,7 +41,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else if (formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { // Check whether we consider a multi-objective formula @@ -140,6 +141,7 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model."); + STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given."); STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries"); storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); if (checkTask.isBoundSet()) { @@ -151,7 +153,8 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } @@ -171,7 +174,8 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); @@ -196,7 +200,8 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); @@ -217,7 +222,8 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - std::vector result = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getUniqueRewardModel()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + std::vector result = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModel.get()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index a6a099833..8b0040b2f 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -5,6 +5,7 @@ #include "storm/storage/dd/Add.h" #include "storm/utility/macros.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -30,7 +31,7 @@ namespace storm { template bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } template @@ -79,7 +80,8 @@ namespace storm { std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } @@ -96,7 +98,8 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(env, this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); return std::make_unique>(this->getModel().getReachableStates(), numericResult); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 713ce3295..a08546669 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -11,6 +11,7 @@ #include "storm/utility/macros.h" #include "storm/utility/graph.h" +#include "storm/utility/FilteredRewardModel.h" #include "storm/settings/modules/GeneralSettings.h" @@ -30,7 +31,7 @@ namespace storm { template bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true)); } template @@ -80,7 +81,8 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), rewardPathFormula.getNonStrictBound()); } template @@ -97,7 +99,8 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector()); + auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(env, checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModel.get(), subResult.getTruthValuesVector()); } template diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2798d9c74..38af2e3ac 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -179,7 +179,7 @@ namespace storm { // Start by decomposing the DTMC into its BSCCs. std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now(); - storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); auto sccDecompositionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); @@ -896,7 +896,8 @@ namespace storm { STORM_LOG_TRACE("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); // Here, we further decompose the SCC into sub-SCCs. - storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, false, false); + storm::storage::BitVector nonEntrySccStates = scc & ~entryStates; + storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, storm::storage::StronglyConnectedComponentDecompositionOptions().subsystem(&nonEntrySccStates)); STORM_LOG_TRACE("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which diff --git a/src/storm/models/ModelBase.cpp b/src/storm/models/ModelBase.cpp index f73ba1bce..7bf753ab8 100644 --- a/src/storm/models/ModelBase.cpp +++ b/src/storm/models/ModelBase.cpp @@ -19,7 +19,21 @@ namespace storm { } bool ModelBase::isNondeterministicModel() const { - return this->isOfType(storm::models::ModelType::Mdp) || this->isOfType(storm::models::ModelType::MarkovAutomaton); + for (auto const& type : {storm::models::ModelType::Mdp, storm::models::ModelType::Pomdp, storm::models::ModelType::S2pg, storm::models::ModelType::MarkovAutomaton}) { + if (this->isOfType(type)) { + return true; + } + } + return false; + } + + bool ModelBase::isDiscreteTimeModel() const { + for (auto const& type : {storm::models::ModelType::Dtmc, storm::models::ModelType::Mdp, storm::models::ModelType::Pomdp, storm::models::ModelType::S2pg}) { + if (this->isOfType(type)) { + return true; + } + } + return false; } bool ModelBase::supportsParameters() const { diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index 77fa5b60d..ca275ed92 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -115,6 +115,11 @@ namespace storm { */ bool isNondeterministicModel() const; + /*! + * Returns true if the model is a descrete-time model. + */ + bool isDiscreteTimeModel() const; + /*! * Checks whether the model supports parameters. * diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index f96bd8714..5167ea1ce 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -117,11 +117,6 @@ namespace storm { } bool NativeEquationSolverSettings::check() const { - // This list does not include the precision, because this option is shared with other modules. - bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); - - STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Native || !optionSet, "Native is not selected as the preferred equation solver, so setting options for native might have no effect."); - return true; } diff --git a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp index f31d1cde3..17acb643d 100644 --- a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp @@ -136,8 +136,7 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!"; #endif } else { - storm::storage::BitVector fullSystem(this->A->getRowGroupCount(), true); - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*this->A, fullSystem, false, false); + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*this->A); STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs."); diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 5b31509fa..649843521 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -105,12 +105,9 @@ namespace storm { template void TopologicalLinearEquationSolver::createSortedSccDecomposition(bool needLongestChainSize) const { // Obtain the scc decomposition - this->sortedSccDecomposition = std::make_unique>(*this->A); + this->sortedSccDecomposition = std::make_unique>(*this->A, storm::storage::StronglyConnectedComponentDecompositionOptions().forceTobologicalSort().computeSccDepths(needLongestChainSize)); if (needLongestChainSize) { - this->longestSccChainSize = 0; - this->sortedSccDecomposition->sortTopologically(*this->A, &(this->longestSccChainSize.get())); - } else { - this->sortedSccDecomposition->sortTopologically(*this->A); + this->longestSccChainSize = this->sortedSccDecomposition->getMaxSccDepth() + 1; } } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 1f517fc10..7afb90bb6 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -113,12 +113,9 @@ namespace storm { template void TopologicalMinMaxLinearEquationSolver::createSortedSccDecomposition(bool needLongestChainSize) const { // Obtain the scc decomposition - this->sortedSccDecomposition = std::make_unique>(*this->A); + this->sortedSccDecomposition = std::make_unique>(*this->A, storm::storage::StronglyConnectedComponentDecompositionOptions().forceTobologicalSort().computeSccDepths(needLongestChainSize)); if (needLongestChainSize) { - this->longestSccChainSize = 0; - this->sortedSccDecomposition->sortTopologically(*this->A, &(this->longestSccChainSize.get())); - } else { - this->sortedSccDecomposition->sortTopologically(*this->A); + this->longestSccChainSize = this->sortedSccDecomposition->getMaxSccDepth() + 1; } } diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index ec5484912..f3401e09b 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -93,15 +93,18 @@ namespace storm { } else { includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true); } + storm::storage::BitVector currMecAsBitVector(transitionMatrix.getRowGroupCount()); for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; - + currMecAsBitVector.clear(); + currMecAsBitVector.set(mec.begin(), mec.end(), true); // Keep track of whether the MEC changed during this iteration. bool mecChanged = false; // Get an SCC decomposition of the current MEC candidate. - StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, includedChoices, true); + + StronglyConnectedComponentDecomposition sccs(transitionMatrix, StronglyConnectedComponentDecompositionOptions().subsystem(&currMecAsBitVector).choices(&includedChoices).dropNaiveSccs()); // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than // the MEC canditate itself. diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index 509eb196c..16d4fbfb6 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,3 +1,4 @@ +#include #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -14,49 +15,8 @@ namespace storm { } template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { - performSccDecomposition(model, dropNaiveSccs, onlyBottomSccs); - } - - template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { - storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end()); - performSccDecomposition(model.getTransitionMatrix(), &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model.getTransitionMatrix(), &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { - storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); - performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { - storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); - performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options) { + performSccDecomposition(transitionMatrix, options); } template @@ -80,142 +40,31 @@ namespace storm { this->blocks = std::move(other.blocks); return *this; } - - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs) { - - STORM_LOG_ASSERT(!choices || subsystem, "Expecting subsystem if choices are given."); - - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - - // Set up the environment of the algorithm. - // Start with the two stacks it maintains. - std::vector s; - s.reserve(numberOfStates); - std::vector p; - p.reserve(numberOfStates); - - // We also need to store the preorder numbers of states and which states have been assigned to which SCC. - std::vector preorderNumbers(numberOfStates); - storm::storage::BitVector hasPreorderNumber(numberOfStates); - storm::storage::BitVector stateHasScc(numberOfStates); - std::vector stateToSccMapping(numberOfStates); - uint_fast64_t sccCount = 0; - - // Finally, we need to keep track of the states with a self-loop to identify naive SCCs. - storm::storage::BitVector statesWithSelfLoop(numberOfStates); - - // Start the search for SCCs from every state in the block. - uint_fast64_t currentIndex = 0; - if (subsystem) { - for (auto state : *subsystem) { - if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); - } - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); - } - } - } - - // After we obtained the state-to-SCC mapping, we build the actual blocks. - this->blocks.resize(sccCount); - if (subsystem) { - for (auto state : *subsystem) { - this->blocks[stateToSccMapping[state]].insert(state); - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - this->blocks[stateToSccMapping[state]].insert(state); - } - } - - // Now flag all trivial SCCs as such. - for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { - if (this->blocks[sccIndex].size() == 1) { - uint_fast64_t onlyState = *this->blocks[sccIndex].begin(); - - if (!statesWithSelfLoop.get(onlyState)) { - this->blocks[sccIndex].setIsTrivial(true); - } - } - } - - // If requested, we need to drop some SCCs. - if (onlyBottomSccs || dropNaiveSccs) { - storm::storage::BitVector blocksToDrop(sccCount); - - // If requested, we need to delete all naive SCCs. - if (dropNaiveSccs) { - for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { - if (this->blocks[sccIndex].isTrivial()) { - blocksToDrop.set(sccIndex); - } - } - } - - // If requested, we need to drop all non-bottom SCCs. - if (onlyBottomSccs) { - if (subsystem) { - for (uint64_t state : *subsystem) { - // If the block of the state is already known to be dropped, we don't need to check the transitions. - if (!blocksToDrop.get(stateToSccMapping[state])) { - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { - if (choices && !choices->get(row)) { - continue; - } - for (auto const& entry : transitionMatrix.getRow(row)) { - if (subsystem->get(entry.getColumn()) && stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { - blocksToDrop.set(stateToSccMapping[state]); - break; - } - } - } - } - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - // If the block of the state is already known to be dropped, we don't need to check the transitions. - if (!blocksToDrop.get(stateToSccMapping[state])) { - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { - for (auto const& entry : transitionMatrix.getRow(row)) { - if (stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { - blocksToDrop.set(stateToSccMapping[state]); - break; - } - } - } - } - } - } - } - - // Create the new set of blocks by moving all the blocks we need to keep into it. - std::vector newBlocks((~blocksToDrop).getNumberOfSetBits()); - uint_fast64_t currentBlock = 0; - for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { - if (!blocksToDrop.get(blockIndex)) { - newBlocks[currentBlock] = std::move(this->blocks[blockIndex]); - ++currentBlock; - } - } - - // Now set this new set of blocks as the result of the decomposition. - this->blocks = std::move(newBlocks); - } - } - - template - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model.getTransitionMatrix(), nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); - } + /*! + * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to + * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by + * the function as a side-effect. + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param startState The starting state for the search of Tarjan's algorithm. + * @param nonTrivialStates A bit vector where entries for non-trivial states (states that either have a selfloop or whose SCC is not a singleton) will be set to true + * @param subsystem An optional bit vector indicating which subsystem to consider. + * @param choices An optional bit vector indicating which choices belong to the subsystem. + * @param currentIndex The next free index that can be assigned to states. + * @param hasPreorderNumber A bit that is used to keep track of the states that already have a preorder number. + * @param preorderNumbers A vector storing the preorder number for each state. + * @param s The stack S used by the algorithm. + * @param p The stack S used by the algorithm. + * @param stateHasScc A bit vector containing all states that have already been assigned to an SCC. + * @param stateToSccMapping A mapping from states to the SCC indices they belong to. As a side effect of this + * function this mapping is filled (for all states reachable from the starting state). + * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count + * is increased. + */ template - void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { + void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& nonTrivialStates, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount, bool /*forceTopologicalSort*/, std::vector* sccDepths) { + // The forceTopologicalSort flag can be ignored as this method always generates a topological sort. // Prepare the stack used for turning the recursive procedure into an iterative one. std::vector recursionStateStack; @@ -242,7 +91,7 @@ namespace storm { for (auto const& successor : transitionMatrix.getRow(row)) { if ((!subsystem || subsystem->get(successor.getColumn())) && successor.getValue() != storm::utility::zero()) { if (currentState == successor.getColumn()) { - statesWithSelfLoop.set(currentState); + nonTrivialStates.set(currentState, true); } if (!hasPreorderNumber.get(successor.getColumn())) { @@ -264,12 +113,35 @@ namespace storm { // on the current state. if (currentState == p.back()) { p.pop_back(); + if (sccDepths) { + uint_fast64_t sccDepth = 0; + // Find the largest depth over successor SCCs. + auto stateIt = s.end(); + do { + --stateIt; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[*stateIt], rowEnd = transitionMatrix.getRowGroupIndices()[*stateIt + 1]; row != rowEnd; ++row) { + if (choices && !choices->get(row)) { + continue; + } + for (auto const& successor : transitionMatrix.getRow(row)) { + if ((!subsystem || subsystem->get(successor.getColumn())) && successor.getValue() != storm::utility::zero() && stateHasScc.get(successor.getColumn())) { + sccDepth = std::max(sccDepth, (*sccDepths)[stateToSccMapping[successor.getColumn()]] + 1); + } + } + } + } while (*stateIt != currentState); + sccDepths->push_back(sccDepth); + } + bool nonSingletonScc = s.back() != currentState; uint_fast64_t poppedState = 0; do { poppedState = s.back(); s.pop_back(); stateToSccMapping[poppedState] = sccCount; stateHasScc.set(poppedState); + if (nonSingletonScc) { + nonTrivialStates.set(poppedState, true); + } } while (poppedState != currentState); ++sccCount; } @@ -278,117 +150,107 @@ namespace storm { } } } - + template - void StronglyConnectedComponentDecomposition::sortTopologically(storm::storage::SparseMatrix const& transitions, uint64_t* longestChainSize) { + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options) { - // Get a mapping from state to the corresponding scc - STORM_LOG_THROW(this->size() < std::numeric_limits::max(), storm::exceptions::UnexpectedException, "The number of SCCs is too large."); - std::vector sccIndices(transitions.getRowGroupCount(), std::numeric_limits::max()); - uint32_t sccIndex = 0; - for (auto const& scc : *this) { - for (auto const& state : scc) { - sccIndices[state] = sccIndex; - } - ++sccIndex; + STORM_LOG_ASSERT(!options.choicesPtr || options.subsystemPtr, "Expecting subsystem if choices are given."); + + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + + // Set up the environment of the algorithm. + // Start with the two stacks it maintains. + std::vector s; + s.reserve(numberOfStates); + std::vector p; + p.reserve(numberOfStates); + + // We also need to store the preorder numbers of states and which states have been assigned to which SCC. + std::vector preorderNumbers(numberOfStates); + storm::storage::BitVector hasPreorderNumber(numberOfStates); + storm::storage::BitVector stateHasScc(numberOfStates); + std::vector stateToSccMapping(numberOfStates); + uint_fast64_t sccCount = 0; + + // Store scc depths if requested + std::vector* sccDepthsPtr = nullptr; + sccDepths = boost::none; + if (options.isComputeSccDepthsSet || options.areOnlyBottomSccsConsidered) { + sccDepths = std::vector(); + sccDepthsPtr = &sccDepths.get(); } - // Prepare the resulting set of sorted sccs - std::vector sortedSCCs; - sortedSCCs.reserve(this->size()); + // Finally, we need to keep of trivial states (singleton SCCs without selfloop). + storm::storage::BitVector nonTrivialStates(numberOfStates, false); - // Find a topological sort via DFS. - storm::storage::BitVector unsortedSCCs(this->size(), true); - std::vector sccStack, chainSizes; - if (longestChainSize != nullptr) { - chainSizes.resize(this->size(), 1u); - *longestChainSize = 0; + // Start the search for SCCs from every state in the block. + uint_fast64_t currentIndex = 0; + if (options.subsystemPtr) { + for (auto state : *options.subsystemPtr) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, nonTrivialStates, options.subsystemPtr, options.choicesPtr, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount, options.isTopologicalSortForced, sccDepthsPtr); + } + } + } else { + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, nonTrivialStates, options.subsystemPtr, options.choicesPtr, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount, options.isTopologicalSortForced, sccDepthsPtr); + } + } } - uint32_t const token = std::numeric_limits::max(); - std::set successorSCCs; - - for (uint32_t firstUnsortedScc = 0; firstUnsortedScc < unsortedSCCs.size(); firstUnsortedScc = unsortedSCCs.getNextSetIndex(firstUnsortedScc + 1)) { - - sccStack.push_back(firstUnsortedScc); - while (!sccStack.empty()) { - uint32_t currentSccIndex = sccStack.back(); - if (currentSccIndex != token) { - // Check whether the SCC is still unprocessed - if (unsortedSCCs.get(currentSccIndex)) { - // Explore the successors of the scc. - storm::storage::StronglyConnectedComponent const& currentScc = this->getBlock(currentSccIndex); - // We first push a token on the stack in order to recognize later when all successors of this SCC have been explored already. - sccStack.push_back(token); - // Now add all successors that are not already sorted. - // Successors should only be added once, so we first prepare a set of them and add them afterwards. - successorSCCs.clear(); - for (auto const& state : currentScc) { - for (auto const& entry : transitions.getRowGroup(state)) { - if (!storm::utility::isZero(entry.getValue())) { - auto const& successorSCC = sccIndices[entry.getColumn()]; - if (successorSCC != currentSccIndex && unsortedSCCs.get(successorSCC)) { - successorSCCs.insert(successorSCC); - } - } - } - } - sccStack.insert(sccStack.end(), successorSCCs.begin(), successorSCCs.end()); - - } - } else { - // all successors of the current scc have already been explored. - sccStack.pop_back(); // pop the token - - currentSccIndex = sccStack.back(); - storm::storage::StronglyConnectedComponent& scc = this->getBlock(currentSccIndex); - - // Compute the longest chain size for this scc - if (longestChainSize != nullptr) { - uint32_t& currentChainSize = chainSizes[currentSccIndex]; - for (auto const& state : scc) { - for (auto const& entry : transitions.getRowGroup(state)) { - if (!storm::utility::isZero(entry.getValue())) { - auto const& successorSCC = sccIndices[entry.getColumn()]; - if (successorSCC != currentSccIndex) { - currentChainSize = std::max(currentChainSize, chainSizes[successorSCC] + 1); - } - } - } + + // After we obtained the state-to-SCC mapping, we build the actual blocks. + this->blocks.resize(sccCount); + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + // Check if this state (and is SCC) should be considered in this decomposition. + if ((!options.subsystemPtr || options.subsystemPtr->get(state))) { + if (!options.areNaiveSccsDropped || nonTrivialStates.get(state)) { + uint_fast64_t sccIndex = stateToSccMapping[state]; + if (!options.areOnlyBottomSccsConsidered || sccDepths.get()[sccIndex] == 0) { + this->blocks[sccIndex].insert(state); + if (!nonTrivialStates.get(state)) { + this->blocks[sccIndex].setIsTrivial(true); + STORM_LOG_ASSERT(this->blocks[sccIndex].size() == 1, "Unexpected number of states in a trivial SCC."); } - *longestChainSize = std::max(*longestChainSize, currentChainSize); } - - unsortedSCCs.set(currentSccIndex, false); - sccStack.pop_back(); // pop the current scc index - sortedSCCs.push_back(std::move(scc)); } } } - this->blocks = std::move(sortedSCCs); + + // If requested, we need to delete all naive SCCs. + if (options.areOnlyBottomSccsConsidered || options.areNaiveSccsDropped) { + storm::storage::BitVector blocksToDrop(sccCount); + for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { + if (this->blocks[sccIndex].empty()) { + blocksToDrop.set(sccIndex, true); + } + } + // Create the new set of blocks by moving all the blocks we need to keep into it. + storm::utility::vector::filterVectorInPlace(this->blocks, ~blocksToDrop); + if (this->sccDepths) { + storm::utility::vector::filterVectorInPlace(this->sccDepths.get(), ~blocksToDrop); + } + } } - - // Explicitly instantiate the SCC decomposition. - template class StronglyConnectedComponentDecomposition; - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + template + uint_fast64_t StronglyConnectedComponentDecomposition::getSccDepth(uint_fast64_t const& sccIndex) const { + STORM_LOG_THROW(sccDepths.is_initialized(), storm::exceptions::InvalidOperationException, "Tried to get the SCC depth but SCC depths were not computed upon construction."); + STORM_LOG_ASSERT(sccIndex < sccDepths->size(), "SCC index " << sccIndex << " is out of range (" << sccDepths->size() << ")"); + return sccDepths.get()[sccIndex]; + } + + template + uint_fast64_t StronglyConnectedComponentDecomposition::getMaxSccDepth() const { + STORM_LOG_THROW(sccDepths.is_initialized(), storm::exceptions::InvalidOperationException, "Tried to get the maximum SCC depth but SCC depths were not computed upon construction."); + STORM_LOG_THROW(!sccDepths->empty(), storm::exceptions::InvalidOperationException, "Tried to get the maximum SCC depth but this SCC decomposition seems to be empty."); + return *std::max_element(sccDepths->begin(), sccDepths->end()); + } + // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); - -#ifdef STORM_HAVE_CARL + template class StronglyConnectedComponentDecomposition; template class StronglyConnectedComponentDecomposition; - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); - template class StronglyConnectedComponentDecomposition; - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); -#endif } // namespace storage } // namespace storm diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.h b/src/storm/storage/StronglyConnectedComponentDecomposition.h index 7d244b914..da8b1dc25 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.h @@ -1,12 +1,12 @@ #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ +#include #include "storm/storage/SparseMatrix.h" #include "storm/storage/Decomposition.h" #include "storm/storage/StronglyConnectedComponent.h" #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" - namespace storm { namespace models { namespace sparse { @@ -17,119 +17,51 @@ namespace storm { namespace storage { + + struct StronglyConnectedComponentDecompositionOptions { + /// Sets a bit vector indicating which subsystem to consider for the decomposition into SCCs. + StronglyConnectedComponentDecompositionOptions& subsystem(storm::storage::BitVector const* subsystem) { subsystemPtr = subsystem; return *this; } + /// Sets a bit vector indicating which choices of the states are contained in the subsystem. + StronglyConnectedComponentDecompositionOptions& choices(storm::storage::BitVector const* choices) { choicesPtr = choices; return *this; } + /// Sets if trivial SCCs (i.e. SCCs consisting of just one state without a self-loop) are to be kept in the decomposition. + StronglyConnectedComponentDecompositionOptions& dropNaiveSccs(bool value = true) { areNaiveSccsDropped = value; return *this; } + /// Sets if only bottom SCCs, i.e. SCCs in which all states have no way of leaving the SCC), are kept. + StronglyConnectedComponentDecompositionOptions& onlyBottomSccs(bool value = true) { areOnlyBottomSccsConsidered = value; return *this; } + /// Enforces that the returned SCCs are sorted in a topological order. + StronglyConnectedComponentDecompositionOptions& forceTobologicalSort(bool value = true) { isTopologicalSortForced = value; return *this; } + /// Sets if scc depths can be retrieved. + StronglyConnectedComponentDecompositionOptions& computeSccDepths(bool value = true) { isComputeSccDepthsSet = value; return *this; } + + storm::storage::BitVector const* subsystemPtr = nullptr; + storm::storage::BitVector const* choicesPtr = nullptr; + bool areNaiveSccsDropped = false; + bool areOnlyBottomSccsConsidered = false; + bool isTopologicalSortForced = false; + bool isComputeSccDepthsSet = false; + + }; + /*! * This class represents the decomposition of a graph-like structure into its strongly connected components. */ template class StronglyConnectedComponentDecomposition : public Decomposition { - public: + public: + /* * Creates an empty SCC decomposition. */ StronglyConnectedComponentDecomposition(); - /* - * Creates an SCC decomposition of the given model. - * - * @param model The model to decompose into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - template > - StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given block in the given model. - * - * @param model The model whose block to decompose. - * @param block The block to decompose into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - template > - StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given model. - * - * @param model The model that contains the block. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - template > - StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param block The block to decompose into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - /* * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is * given by a sparse matrix). * * @param transitionMatrix The transition matrix of the system to decompose. - * @param block The block to decompose into SCCs. - * @param choices A bit vector indicating which choices of the states are contained in the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + * @param options options for the decomposition - /* - * Creates an SCC decomposition of the given system (whose transition relation is given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. - */ - StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param choices A bit vector indicating which choices of the states are contained in the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. */ - StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options = StronglyConnectedComponentDecompositionOptions()); /*! * Creates an SCC decomposition by copying the given SCC decomposition. @@ -159,65 +91,30 @@ namespace storm { */ StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other); - /*! - * Sorts the SCCs topologically: The ith block can only reach states in block j const& transitions, uint64_t* longestChainSize = nullptr); + uint_fast64_t getSccDepth(uint_fast64_t const& sccIndex) const; - private: /*! - * Performs the SCC decomposition of the given model. As a side-effect this fills the vector of - * blocks of the decomposition. - * - * @param model The model to decompose into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. + * Gets the maximum depth of an SCC. */ - template > - void performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + uint_fast64_t getMaxSccDepth() const; + private: /* * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills * the vector of blocks of the decomposition. * * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem An optional bit vector indicating which subsystem to consider. - * @param choices An optional bit vector indicating which choices belong to the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of - * leaving the SCC), are kept. */ - void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options); - /*! - * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to - * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by - * the function as a side-effect. - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param startState The starting state for the search of Tarjan's algorithm. - * @param statesWithSelfLoop A bit vector that is to be filled with all states that have a self-loop. This - * is later needed for identification of the naive SCCs. - * @param subsystem An optional bit vector indicating which subsystem to consider. - * @param choices An optional bit vector indicating which choices belong to the subsystem. - * @param currentIndex The next free index that can be assigned to states. - * @param hasPreorderNumber A bit that is used to keep track of the states that already have a preorder number. - * @param preorderNumbers A vector storing the preorder number for each state. - * @param s The stack S used by the algorithm. - * @param p The stack S used by the algorithm. - * @param stateHasScc A bit vector containing all states that have already been assigned to an SCC. - * @param stateToSccMapping A mapping from states to the SCC indices they belong to. As a side effect of this - * function this mapping is filled (for all states reachable from the starting state). - * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count - * is increased. - */ - void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount); + + boost::optional> sccDepths; }; } } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 947bf128d..be2c98e9f 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -342,8 +342,11 @@ namespace storm { return opDecl; } - boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const&, boost::any const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae"); + boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "G"; + opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const { @@ -495,61 +498,46 @@ namespace storm { } else { opString += "min"; } + + opDecl["op"] = opString; + + if (f.getSubformula().isEventuallyFormula()) { + opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); + if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { + opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName); + } else { + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); + } + } else if (f.getSubformula().isCumulativeRewardFormula()) { + // TODO: support for reward bounded formulas + STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for cumulative reward formulas with reward instant currently unsupported."); + opDecl[instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); + if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) { + opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName); + } else { + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); + } + } else if (f.getSubformula().isInstantaneousRewardFormula()) { + opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); + } else if (f.getSubformula().isLongRunAverageRewardFormula()) { + if (f.getSubformula().asLongRunAverageRewardFormula().hasRewardAccumulation()) { + opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asLongRunAverageRewardFormula().getRewardAccumulation(), rewardModelName); + } else { + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); + } + } + opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); if(f.hasBound()) { + modernjson::json compDecl; auto bound = f.getBound(); - opDecl["op"] = comparisonTypeToJani(bound.comparisonType); - opDecl["left"]["op"] = opString; - if (f.getSubformula().isEventuallyFormula()) { - opDecl["left"]["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); - if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { - opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName); - } else { - opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName); - } - } else if (f.getSubformula().isCumulativeRewardFormula()) { - // TODO: support for reward bounded formulas - STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported."); - opDecl["left"][instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); - if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) { - opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName); - } else { - opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName); - } - } else if (f.getSubformula().isInstantaneousRewardFormula()) { - opDecl["left"][instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); - } else if (f.getSubformula().isLongRunAverageRewardFormula()) { - // Nothing to do in this case - } - opDecl["left"]["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); - opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); + compDecl["op"] = comparisonTypeToJani(bound.comparisonType); + compDecl["left"] = std::move(opDecl); + compDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); + return compDecl; } else { - opDecl["op"] = opString; - - if (f.getSubformula().isEventuallyFormula()) { - opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); - if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { - opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName); - } else { - opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); - } - } else if (f.getSubformula().isCumulativeRewardFormula()) { - // TODO: support for reward bounded formulas - STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported."); - opDecl[instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); - if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) { - opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName); - } else { - opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); - } - } else if (f.getSubformula().isInstantaneousRewardFormula()) { - opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); - } else if (f.getSubformula().isLongRunAverageRewardFormula()) { - // Nothing to do in this case - } - opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); + return opDecl; } - return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const { diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 249920f36..213c2e273 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -23,11 +23,11 @@ namespace storm { storm::expressions::Expression upperBound; bool upperBoundStrict = false; - bool hasLowerBound() { + bool hasLowerBound() const { return lowerBound.isInitialized(); } - bool hasUpperBound() { + bool hasUpperBound() const { return upperBound.isInitialized(); } }; diff --git a/src/storm/storage/jani/traverser/RewardModelInformation.cpp b/src/storm/storage/jani/traverser/RewardModelInformation.cpp index 908802742..d3c63aeeb 100644 --- a/src/storm/storage/jani/traverser/RewardModelInformation.cpp +++ b/src/storm/storage/jani/traverser/RewardModelInformation.cpp @@ -19,15 +19,19 @@ namespace storm { RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false) { auto variablesInRewardExpression = rewardModelExpression.getVariables(); std::map initialSubstitution; + bool containsNonTransientVariable = false; for (auto const& v : variablesInRewardExpression) { STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); auto const& janiVar = model.getGlobalVariable(v.getName()); if (janiVar.hasInitExpression()) { initialSubstitution.emplace(v, janiVar.getInitExpression()); } + if (!janiVar.isTransient()) { + containsNonTransientVariable = true; + } } auto initExpr = storm::jani::substituteJaniExpression(rewardModelExpression, initialSubstitution); - if (initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) { + if (containsNonTransientVariable || initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) { stateRewards = true; actionRewards = true; transitionRewards = true; diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index a0b32175a..1a22f87dc 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1843,7 +1843,7 @@ namespace storm { storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - auto janiModel = converter.convert(*this, allVariablesGlobal, suffix); + auto janiModel = converter.convert(*this, allVariablesGlobal, {}, suffix); STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored."); STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored."); return janiModel; @@ -1851,7 +1851,14 @@ namespace storm { std::pair> Program::toJani(std::vector const& properties, bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - auto janiModel = converter.convert(*this, allVariablesGlobal, suffix); + std::set variablesToMakeGlobal; + if (!allVariablesGlobal) { + for (auto const& prop : properties) { + auto vars = prop.getUsedVariablesAndConstants(); + variablesToMakeGlobal.insert(vars.begin(), vars.end()); + } + } + auto janiModel = converter.convert(*this, allVariablesGlobal, variablesToMakeGlobal, suffix); std::vector newProperties; if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) { newProperties = converter.applyRenaming(properties); diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index bc6476e5b..8c9f624ed 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -18,7 +18,7 @@ namespace storm { namespace prism { - storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) { + storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::set const& givenVariablesToMakeGlobal, std::string suffix) { labelRenaming.clear(); rewardModelRenaming.clear(); formulaToFunctionCallMap.clear(); @@ -53,6 +53,9 @@ namespace storm { // Maintain a mapping of each variable to a flag that is true if the variable will be made global. std::map variablesToMakeGlobal; + for (auto const& var : givenVariablesToMakeGlobal) { + variablesToMakeGlobal.emplace(var, true); + } // Get the set of variables that appeare in a renaimng of a renamed module if (program.getNumberOfFormulas() > 0) { diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index 38d5f331e..a86f6dea0 100644 --- a/src/storm/storage/prism/ToJaniConverter.h +++ b/src/storm/storage/prism/ToJaniConverter.h @@ -18,7 +18,7 @@ namespace storm { class ToJaniConverter { public: - storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = ""); + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::set const& variablesToMakeGlobal = {}, std::string suffix = ""); bool labelsWereRenamed() const; bool rewardModelsWereRenamed() const; diff --git a/src/storm/utility/FilteredRewardModel.h b/src/storm/utility/FilteredRewardModel.h new file mode 100644 index 000000000..32dc13521 --- /dev/null +++ b/src/storm/utility/FilteredRewardModel.h @@ -0,0 +1,64 @@ +#pragma once + +#include + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace utility { + + + /* + * This class wraps around a + */ + template + class FilteredRewardModel { + public: + FilteredRewardModel(RewardModelType const& baseRewardModel, bool enableStateRewards, bool enableStateActionRewards, bool enableTransitionRewards) { + if ((baseRewardModel.hasStateRewards() && !enableStateRewards) || (baseRewardModel.hasStateActionRewards() && !enableStateActionRewards) || (baseRewardModel.hasTransitionRewards() && !enableTransitionRewards)) { + // One of the available reward types need to be deleted. + typename std::remove_const::type>::type stateRewards; + if (enableStateRewards) { + stateRewards = baseRewardModel.getOptionalStateRewardVector(); + } + typename std::remove_const::type>::type stateActionRewards; + if (enableStateActionRewards) { + stateActionRewards = baseRewardModel.getOptionalStateActionRewardVector(); + } + typename std::remove_const::type>::type transitionRewards; + if (enableTransitionRewards) { + transitionRewards = baseRewardModel.getOptionalTransitionRewardMatrix(); + } + localRewardModel = std::unique_ptr(new RewardModelType(stateRewards, stateActionRewards, transitionRewards)); + rewardModel = localRewardModel.get(); + } else { + rewardModel = &baseRewardModel; + } + } + + RewardModelType const& get() const { + return *rewardModel; + } + private: + std::unique_ptr localRewardModel; + RewardModelType const* rewardModel; + }; + + template + FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { + auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); + if (checkTask.getFormula().hasRewardAccumulation()) { + auto const& acc = checkTask.getFormula().getRewardAccumulation(); + STORM_LOG_THROW(model.isDiscreteTimeModel() || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); + // Check which of the available reward types are allowed. + bool hasStateRewards = model.isDiscreteTimeModel() ? acc.isExitSet() : acc.isTimeSet(); + bool hasStateActionRewards = acc.isStepsSet(); + bool hasTransitionRewards = acc.isStepsSet(); + return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); + } else { + return FilteredRewardModel(baseRewardModel, true, true, true); + } + } + } +} \ No newline at end of file diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 1515a31f7..c1f1216ad 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -106,7 +106,7 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::BitVector result(transitionMatrix.getRowGroupCount()); - storm::storage::StronglyConnectedComponentDecomposition decomposition(transitionMatrix, false, true); + storm::storage::StronglyConnectedComponentDecomposition decomposition(transitionMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); // Take the first state out of each BSCC. for (auto const& scc : decomposition) { diff --git a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp index 821b721a7..429f7de2a 100644 --- a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -21,17 +21,19 @@ TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) { storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build()); - storm::storage::BitVector allBits(6, true); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + storm::storage::StronglyConnectedComponentDecompositionOptions options; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, false, false)); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(4ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, false)); + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(3ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(1ul, sccDecomposition.size()); } @@ -41,14 +43,17 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem1) { std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + storm::storage::StronglyConnectedComponentDecompositionOptions options; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton)); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(5ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true)); + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); markovAutomaton = nullptr; @@ -60,8 +65,10 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) { std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, false)); - + storm::storage::StronglyConnectedComponentDecompositionOptions options; + + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way. @@ -73,7 +80,8 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) { ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end())); ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end())); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(1ul, sccDecomposition.size()); markovAutomaton = nullptr;