diff --git a/CMakeLists.txt b/CMakeLists.txt index 1b3bee076..86847d6fd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -325,6 +325,11 @@ if (STORM_DEVELOPER) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-float-equal") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-local-typedef") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-variable-declarations") + elseif (GCC) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wunused") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unknown-pragmas") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-local-typedefs") endif () else () set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra") diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 87fe8edc9..0fb923dc0 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -3,7 +3,7 @@ namespace storm { namespace parser { - + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true), propertyCount(0) { initialize(); } @@ -16,72 +16,72 @@ namespace storm { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *constManager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); - } + } // Set the identifier mapping to actually generate expressions. expressionParser.setIdentifierMapping(&identifiers_); - + longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") | qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; longRunAverageRewardFormula.name("long run average reward formula"); - + instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); - + cumulativeRewardFormula = (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - + totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; totalRewardFormula.name("total reward formula"); - + rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | totalRewardFormula; rewardPathFormula.name("reward path formula"); - + expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; expressionFormula.name("expression formula"); - + label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]; label.name("label"); - + labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; labelFormula.name("label formula"); - + booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); - + operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator; operatorFormula.name("operator formulas"); - + atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula"); - + atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula without expression"); - + notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1]; notStateFormula.name("negation formula"); - + eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); - + globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; globallyFormula.name("globally formula"); - + nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - + pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula; pathFormulaWithoutUntil.name("path formula"); - + untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); - + conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); - + timeBoundReference = (-qi::lit("rew") >> rewardModelName)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Reward, qi::_1)] | (qi::lit("steps"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Steps, boost::none)] | (-qi::lit("time"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Time, boost::none)]; timeBoundReference.name("time bound reference"); - + timeBound = ((timeBoundReference >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")) [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] | ( timeBoundReference >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser) @@ -89,46 +89,46 @@ namespace storm { | ( timeBoundReference >> qi::lit("=") >> expressionParser) [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_2, qi::_1)]; timeBound.name("time bound"); - + timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}")); timeBounds.name("time bounds"); - + pathFormula = conditionalFormula(qi::_r1); pathFormula.name("path formula"); - + rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]"); rewardMeasureType.name("reward measure type"); - + operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); - + longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; longRunAverageOperator.name("long-run average operator"); - + rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); rewardModelName.name("reward model name"); - + rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)]; rewardOperator.name("reward operator"); - + timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; timeOperator.name("time operator"); - + probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; probabilityOperator.name("probability operator"); - + andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; andStateFormula.name("and state formula"); - + orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula.name("or state formula"); - + multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)]; multiFormula.name("Multi formula"); identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; identifier.name("identifier"); - + quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a, qi::_1)]; quantileBoundVariable.name("quantile bound variable"); quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -140,18 +140,30 @@ namespace storm { gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); + + coalitionOperator = (qi::lit("<<") + > *( (identifier[phoenix::push_back(qi::_a, qi::_1)] + | qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ',' + ) + > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)]; + coalitionOperator.name("coalition operator"); + + gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + gameFormula.name("game formula"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula.name("state formula"); - + formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); - + constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); - + #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); @@ -162,7 +174,7 @@ namespace storm { | qi::eps) % +(qi::char_("\n;")) >> qi::skip(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); - + // Enable the following lines to print debug output for most the rules. // debug(start); // debug(constantDefinition); @@ -188,7 +200,7 @@ namespace storm { // debug(totalRewardFormula); // debug(instantaneousRewardFormula); // debug(multiFormula); - + // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -216,16 +228,16 @@ namespace storm { qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(multiFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } - + void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { this->identifiers_.add(identifier, expression); } - + void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants."); storm::expressions::Variable newVariable; STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException, "Invalid constant definition '" << name << "' in property: variable already exists."); - + if (type == ConstantDataType::Bool) { newVariable = manager->declareBooleanVariable(name); } else if (type == ConstantDataType::Integer) { @@ -233,7 +245,7 @@ namespace storm { } else { newVariable = manager->declareRationalVariable(name); } - + if (expression) { addIdentifierExpression(name, expression.get()); } else { @@ -241,11 +253,11 @@ namespace storm { addIdentifierExpression(name, newVariable); } } - + bool FormulaParserGrammar::areConstantDefinitionsAllowed() const { return static_cast(manager); } - + std::shared_ptr FormulaParserGrammar::createTimeBoundReference(storm::logic::TimeBoundType const& type, boost::optional const& rewardModelName) const { if (type == storm::logic::TimeBoundType::Reward) { STORM_LOG_THROW(rewardModelName, storm::exceptions::WrongFormatException, "Reward bound does not specify a reward model name."); @@ -254,7 +266,7 @@ namespace storm { return std::make_shared(type); } } - + std::tuple, boost::optional, std::shared_ptr> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, std::shared_ptr const& timeBoundReference) const { // As soon as it somehow does not break everything anymore, I will change return types here. @@ -262,7 +274,7 @@ namespace storm { storm::logic::TimeBound upper(false, upperBound); return std::make_tuple(lower, upper, timeBoundReference); } - + std::tuple, boost::optional, std::shared_ptr> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, std::shared_ptr const& timeBoundReference) const { // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { @@ -271,11 +283,11 @@ namespace storm { return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, timeBoundReference); } } - + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const { return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBound)); } - + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(std::vector, boost::optional, std::shared_ptr>> const& timeBounds) const { std::vector bounds; std::vector timeBoundReferences; @@ -287,28 +299,28 @@ namespace storm { } return std::shared_ptr(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences)); } - + std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { return std::shared_ptr(new storm::logic::TotalRewardFormula()); } - + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); } - + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); } - + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); } - + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -323,15 +335,15 @@ namespace storm { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } } - + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } - + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula) { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -346,11 +358,11 @@ namespace storm { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } } - + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); } - + storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { storm::expressions::ExpressionEvaluator evaluator(*constManager); @@ -359,11 +371,11 @@ namespace storm { return storm::logic::OperatorInformation(optimizationDirection, boost::none); } } - + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); } - + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { @@ -371,7 +383,7 @@ namespace storm { } return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); } - + std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { @@ -379,15 +391,15 @@ namespace storm { } return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); } - + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); } - + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } - + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (operatorType) { return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); @@ -395,7 +407,7 @@ namespace storm { return subformula; } } - + std::shared_ptr FormulaParserGrammar::createMultiFormula(std::vector> const& subformulas) { bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty(); for (auto const& subformula : subformulas) { @@ -404,7 +416,7 @@ namespace storm { break; } } - + if (isMultiDimensionalBoundedUntilFormula) { std::vector> leftSubformulas, rightSubformulas; std::vector> lowerBounds, upperBounds; @@ -431,7 +443,7 @@ namespace storm { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } } - + storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define quantile bound variable."); storm::expressions::Variable var; @@ -450,17 +462,17 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::QuantileFormula(boundVariables, subformula)); } - + std::set FormulaParserGrammar::getUndefinedConstants(std::shared_ptr const& formula) const { std::set result; std::set usedVariables = formula->getUsedVariables(); std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(), std::inserter(result, result.begin())); return result; } - + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { storm::jani::FilterExpression filterExpression(formula, filterType, states); - + ++propertyCount; if (propertyName) { return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula)); @@ -468,7 +480,7 @@ namespace storm { return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula)); } } - + storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula) { ++propertyCount; if (propertyName) { diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index e709366cd..ad76aa87f 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -19,17 +19,17 @@ namespace storm { namespace logic { class Formula; } - + namespace parser { - + class FormulaParserGrammar : public qi::grammar(), Skipper> { public: FormulaParserGrammar(std::shared_ptr const& manager); FormulaParserGrammar(std::shared_ptr const& manager); - + FormulaParserGrammar(FormulaParserGrammar const& other) = delete; FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = delete; - + /*! * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used * to substitute special identifiers in the formula by expressions. @@ -38,10 +38,10 @@ namespace storm { * @param expression The expression it is to be substituted with. */ void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); - + private: void initialize(); - + struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -56,10 +56,10 @@ namespace storm { ("quantile", 9); } }; - + // A parser used for recognizing the keywords. keywordsStruct keywords_; - + struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add @@ -69,10 +69,10 @@ namespace storm { ("<", storm::logic::ComparisonType::Less); } }; - + // A parser used for recognizing the operators at the "relational" precedence level. relationalOperatorStruct relationalOperator_; - + struct binaryBooleanOperatorStruct : qi::symbols { binaryBooleanOperatorStruct() { add @@ -80,20 +80,20 @@ namespace storm { ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); } }; - + // A parser used for recognizing the operators at the "binary" precedence level. binaryBooleanOperatorStruct binaryBooleanOperator_; - + struct unaryBooleanOperatorStruct : qi::symbols { unaryBooleanOperatorStruct() { add ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not); } }; - + // A parser used for recognizing the operators at the "unary" precedence level. unaryBooleanOperatorStruct unaryBooleanOperator_; - + struct optimalityOperatorStruct : qi::symbols { optimalityOperatorStruct() { add @@ -101,10 +101,10 @@ namespace storm { ("max", storm::OptimizationDirection::Maximize); } }; - + // A parser used for recognizing the optimality operators. optimalityOperatorStruct optimalityOperator_; - + struct rewardMeasureTypeStruct : qi::symbols { rewardMeasureTypeStruct() { add @@ -112,10 +112,10 @@ namespace storm { ("var", storm::logic::RewardMeasureType::Variance); } }; - + // A parser used for recognizing the reward measure types. rewardMeasureTypeStruct rewardMeasureType_; - + struct filterTypeStruct : qi::symbols { filterTypeStruct() { add @@ -134,28 +134,28 @@ namespace storm { // A parser used for recognizing the filter type. filterTypeStruct filterType_; - + // The manager used to parse expressions. std::shared_ptr constManager; std::shared_ptr manager; - + // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; - + // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions // they are to be replaced with. qi::symbols identifiers_; - + qi::rule(), Skipper> start; - + enum class ConstantDataType { Bool, Integer, Rational }; - + qi::rule, Skipper> constantDefinition; qi::rule identifier; qi::rule formulaName; - + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule rewardMeasureType; qi::rule(), Skipper> probabilityOperator; @@ -176,30 +176,30 @@ namespace storm { qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; - + qi::rule(), Skipper> andStateFormula; qi::rule(), Skipper> orStateFormula; qi::rule(), Skipper> notStateFormula; qi::rule(), Skipper> labelFormula; qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - + qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - + qi::rule, Skipper> timeBoundReference; qi::rule, boost::optional, std::shared_ptr>(), qi::locals, Skipper> timeBound; qi::rule, boost::optional, std::shared_ptr>>(), qi::locals, Skipper> timeBounds; - + qi::rule(), Skipper> rewardPathFormula; qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; qi::rule(), Skipper> totalRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; - + qi::rule(), Skipper> multiFormula; qi::rule>, Skipper> quantileBoundVariable; qi::rule(), Skipper> quantileFormula; @@ -242,16 +242,16 @@ namespace storm { std::shared_ptr createMultiFormula(std::vector> const& subformulas); storm::expressions::Variable createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName); std::shared_ptr createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula); - + std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); - + // An error handler function. phoenix::function handler; - + uint64_t propertyCount; - + std::set undefinedConstants; std::set quantileFormulaVariables; }; diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 1fa1a38c7..73c1ad9c1 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -869,7 +869,7 @@ namespace storm { if (!this->secondRun) { // Add a mapping from the new module name to its (future) index. globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size(); - + // Register all (renamed) variables for later use. // We already checked before, whether the renaiming is valid. for (auto const& variable : moduleToRename.getBooleanVariables()) { @@ -921,7 +921,7 @@ namespace storm { // Assert that the module name is already known and has the expected index. STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap.count(newModuleName) > 0, "Module name '" << newModuleName << "' was not found."); STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap[newModuleName] == globalProgramInformation.modules.size(), "The index for module " << newModuleName << " does not match the index from the first parsing run."); - + // Create a mapping from identifiers to the expressions they need to be replaced with. std::map expressionRenaming; for (auto const& namePair : renaming) { diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 9ac504d7c..d6d4969d4 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -39,7 +39,7 @@ namespace storm { namespace api { - + template storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); @@ -53,7 +53,7 @@ namespace storm { AbstractionRefinementOptions(std::vector&& constraints, std::vector>&& injectedRefinementPredicates) : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { // Intentionally left empty. } - + std::vector constraints; std::vector> injectedRefinementPredicates; }; @@ -228,13 +228,13 @@ namespace storm { template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; - + // Close the MA, if it is not already closed. if (!ma->isClosed()) { STORM_LOG_WARN("Closing Markov automaton. Consider closing the MA before verification."); ma->close(); } - + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); if (modelchecker.canHandle(task)) { result = modelchecker.check(env, task); @@ -299,7 +299,7 @@ namespace storm { Environment env; return verifyWithSparseEngine(env, model, task); } - + template std::unique_ptr computeSteadyStateDistributionWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& dtmc) { std::unique_ptr result; @@ -326,7 +326,7 @@ namespace storm { } return result; } - + // // Verifying with Hybrid engine // @@ -485,6 +485,6 @@ namespace storm { Environment env; return verifyWithDdEngine(env, model, task); } - + } } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index b80825d1d..3df2f42b7 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -154,6 +154,7 @@ namespace storm { while (!statesToExplore.empty()) { // Get the first state in the queue. CompressedState currentState = statesToExplore.front().first; + STORM_LOG_DEBUG("Exploring (" << currentRowGroup << ") : " << toString(currentState, this->generator->getVariableInformation())); StateType currentIndex = statesToExplore.front().second; statesToExplore.pop_front(); @@ -196,7 +197,7 @@ namespace storm { rewardModelBuilder.addStateActionReward(storm::utility::zero()); } } - + // This state shall be Markovian (to not introduce Zeno behavior) if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) { stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup); @@ -340,7 +341,7 @@ namespace storm { stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet()); buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder); - + // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel()); diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index f33b37ba3..6538c72c1 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -35,12 +35,12 @@ namespace storm { namespace utility { template class ConstantsComparator; } - + namespace builder { - + using namespace storm::utility::prism; using namespace storm::generator; - + // Forward-declare classes. template class RewardModelBuilder; class StateAndChoiceInformationBuilder; @@ -59,21 +59,21 @@ namespace storm { VariableInformation varInfo; storm::storage::BitVectorHashMap stateToId; }; - + template, typename StateType = uint32_t> class ExplicitModelBuilder { public: - + struct Options { /*! * Creates an object representing the default building options. */ Options(); - + // The order in which to explore the model. ExplorationOrder explorationOrder; }; - + /*! * Creates an explicit model builder that uses the provided generator. * @@ -94,7 +94,7 @@ namespace storm { * @param model The JANI model for which to build the model. */ ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options()); - + /*! * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. @@ -121,7 +121,7 @@ namespace storm { * @return A pair indicating whether the state was already discovered before and the state id of the state. */ StateType getOrAddStateIndex(CompressedState const& state); - + /*! * Builds the transition matrix and the transition reward matrix based for the given program. * diff --git a/src/storm/environment/solver/MultiplierEnvironment.cpp b/src/storm/environment/solver/MultiplierEnvironment.cpp index 85e3bac77..0dd7f031a 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.cpp +++ b/src/storm/environment/solver/MultiplierEnvironment.cpp @@ -6,28 +6,36 @@ #include "storm/utility/macros.h" namespace storm { - + MultiplierEnvironment::MultiplierEnvironment() { auto const& multiplierSettings = storm::settings::getModule(); type = multiplierSettings.getMultiplierType(); typeSetFromDefault = multiplierSettings.isMultiplierTypeSetFromDefaultValue(); } - + MultiplierEnvironment::~MultiplierEnvironment() { // Intentionally left empty } - + storm::solver::MultiplierType const& MultiplierEnvironment::getType() const { return type; } - + bool const& MultiplierEnvironment::isTypeSetFromDefault() const { return typeSetFromDefault; } - + void MultiplierEnvironment::setType(storm::solver::MultiplierType value, bool isSetFromDefault) { type = value; typeSetFromDefault = isSetFromDefault; } - + + void MultiplierEnvironment::setOptimizationDirectionOverride(storm::storage::BitVector optDirOverride) { + optimizationDirectionOverride = optDirOverride; + } + + boost::optional const& MultiplierEnvironment::getOptimizationDirectionOverride() const { + return optimizationDirectionOverride; + } + } diff --git a/src/storm/environment/solver/MultiplierEnvironment.h b/src/storm/environment/solver/MultiplierEnvironment.h index d9e35f5fb..945b62602 100644 --- a/src/storm/environment/solver/MultiplierEnvironment.h +++ b/src/storm/environment/solver/MultiplierEnvironment.h @@ -1,23 +1,31 @@ #pragma once +#include + #include "storm/environment/solver/SolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/storage/BitVector.h" + namespace storm { - + class MultiplierEnvironment { public: - + MultiplierEnvironment(); ~MultiplierEnvironment(); - + storm::solver::MultiplierType const& getType() const; bool const& isTypeSetFromDefault() const; void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false); - + + void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride); + boost::optional const& getOptimizationDirectionOverride() const; + private: storm::solver::MultiplierType type; bool typeSetFromDefault; + + boost::optional optimizationDirectionOverride = boost::none; }; } - diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index a0efb04f9..ef5d0ab4a 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -11,30 +11,30 @@ namespace storm { namespace generator { - + template Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), rewards(), labels() { // Intentionally left empty. } - + template void Choice::add(Choice const& other) { STORM_LOG_THROW(this->markovian == other.markovian, storm::exceptions::InvalidOperationException, "Type of choices do not match."); STORM_LOG_THROW(this->actionIndex == other.actionIndex, storm::exceptions::InvalidOperationException, "Action index of choices do not match."); STORM_LOG_THROW(this->rewards.size() == other.rewards.size(), storm::exceptions::InvalidOperationException, "Reward value sizes of choices do not match."); - + // Add the elements to the distribution. this->distribution.add(other.distribution); - + // Update the total mass of the choice. this->totalMass += other.totalMass; - + // Add all reward values. auto otherRewIt = other.rewards.begin(); for (auto& rewardValue : this->rewards) { rewardValue += *otherRewIt; } - + // Join label sets and origin data if given. if (other.labels) { this->addLabels(other.labels.get()); @@ -43,27 +43,27 @@ namespace storm { this->addOriginData(other.originData.get()); } } - + template typename storm::storage::Distribution::iterator Choice::begin() { return distribution.begin(); } - + template typename storm::storage::Distribution::const_iterator Choice::begin() const { return distribution.cbegin(); } - + template typename storm::storage::Distribution::iterator Choice::end() { return distribution.end(); } - + template typename storm::storage::Distribution::const_iterator Choice::end() const { return distribution.cend(); } - + template void Choice::addLabel(std::string const& newLabel) { if (!labels) { @@ -71,7 +71,7 @@ namespace storm { } labels->insert(newLabel); } - + template void Choice::addLabels(std::set const& newLabels) { if (labels) { @@ -113,7 +113,7 @@ namespace storm { } else { if (!data.empty()) { // Reaching this point means that the both the existing and the given data are non-empty - + auto existingDataAsIndexSet = boost::any_cast>(&this->originData.get()); if (existingDataAsIndexSet != nullptr) { auto givenDataAsIndexSet = boost::any_cast>(&data); @@ -125,63 +125,63 @@ namespace storm { } } } - + template bool Choice::hasOriginData() const { return originData.is_initialized(); } - + template boost::any const& Choice::getOriginData() const { return originData.get(); } - + template uint_fast64_t Choice::getActionIndex() const { return actionIndex; } - + template ValueType Choice::getTotalMass() const { return totalMass; } - + template void Choice::addProbability(StateType const& state, ValueType const& value) { totalMass += value; distribution.addProbability(state, value); } - + template void Choice::addReward(ValueType const& value) { rewards.push_back(value); } - + template void Choice::addRewards(std::vector&& values) { this->rewards = std::move(values); } - + template std::vector const& Choice::getRewards() const { return rewards; } - + template bool Choice::isMarkovian() const { return markovian; } - + template std::size_t Choice::size() const { return distribution.size(); } - + template void Choice::reserve(std::size_t const& size) { distribution.reserve(size); } - + template std::ostream& operator<<(std::ostream& out, Choice const& choice) { out << "<"; @@ -191,7 +191,7 @@ namespace storm { out << ">"; return out; } - + template struct Choice; #ifdef STORM_HAVE_CARL diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 31842ddee..acd6f29b4 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -13,51 +13,51 @@ namespace storm { namespace generator { - + // A structure holding information about a particular choice. template struct Choice { public: Choice(uint_fast64_t actionIndex = 0, bool markovian = false); - + Choice(Choice const& other) = default; Choice& operator=(Choice const& other) = default; Choice(Choice&& other) = default; Choice& operator=(Choice&& other) = default; - + /*! * Adds the given choice to the current one. */ void add(Choice const& other); - + /*! * Returns an iterator to the distribution associated with this choice. * * @return An iterator to the first element of the distribution. */ typename storm::storage::Distribution::iterator begin(); - + /*! * Returns an iterator to the distribution associated with this choice. * * @return An iterator to the first element of the distribution. */ typename storm::storage::Distribution::const_iterator begin() const; - + /*! * Returns an iterator past the end of the distribution associated with this choice. * * @return An iterator past the end of the distribution. */ typename storm::storage::Distribution::iterator end(); - + /*! * Returns an iterator past the end of the distribution associated with this choice. * * @return An iterator past the end of the distribution. */ typename storm::storage::Distribution::const_iterator end() const; - + /*! * Inserts the contents of this object to the given output stream. * diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 1d751bb2e..103c47fc0 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -4,30 +4,30 @@ namespace storm { namespace logic { - + std::shared_ptr CloneVisitor::clone(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } - + boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getOperator(), left, right)); } - + boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; @@ -57,17 +57,17 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); } } - + boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); std::shared_ptr conditionFormula = boost::any_cast>(f.getConditionFormula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, conditionFormula, f.getContext())); } - + boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { @@ -112,41 +112,41 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(subformulas)); } - + boost::any CloneVisitor::visit(QuantileFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getBoundVariables(), subformula)); } - + boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula)); } - + boost::any CloneVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, f.getOperatorInformation())); } - + boost::any CloneVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - + boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getOperator(), subformula)); } - + boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(left, right)); } - + } } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 94da18e87..06772b6ba 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -9,7 +9,7 @@ namespace storm { InheritedInformation(FragmentSpecification const& fragmentSpecification) : fragmentSpecification(fragmentSpecification) { // Intentionally left empty. } - + FragmentSpecification const& getSpecification() const { return fragmentSpecification; } @@ -17,10 +17,10 @@ namespace storm { private: FragmentSpecification const& fragmentSpecification; }; - + bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const { bool result = boost::any_cast(f.accept(*this, InheritedInformation(specification))); - + if (specification.isOperatorAtTopLevelRequired()) { result &= f.isOperatorFormula(); } @@ -30,20 +30,20 @@ namespace storm { if (specification.isQuantileFormulaAtTopLevelRequired()) { result &= f.isQuantileFormula(); } - + return result; } - + boost::any FragmentChecker::visit(AtomicExpressionFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areAtomicExpressionFormulasAllowed(); } - + boost::any FragmentChecker::visit(AtomicLabelFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areAtomicLabelFormulasAllowed(); } - + boost::any FragmentChecker::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBinaryBooleanStateFormulasAllowed(); @@ -51,12 +51,12 @@ namespace storm { result = result && boost::any_cast(f.getRightSubformula().accept(*this, data)); return result; } - + boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areBooleanLiteralFormulasAllowed(); } - + boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed(); @@ -78,7 +78,7 @@ namespace storm { } } } - + if (f.hasMultiDimensionalSubformulas()) { for (uint64_t i = 0; i < f.getDimension(); ++i) { if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { @@ -98,7 +98,7 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(ConditionalFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = true; @@ -118,10 +118,10 @@ namespace storm { result = result && boost::any_cast(f.getConditionFormula().accept(*this, data)); return result; } - + boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - + bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed(); result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed()); result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); @@ -141,7 +141,7 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = true; @@ -163,7 +163,7 @@ namespace storm { result = result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; } - + boost::any FragmentChecker::visit(TimeOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areTimeOperatorsAllowed(); @@ -178,7 +178,7 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areGloballyFormulasAllowed(); @@ -211,16 +211,16 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); return result && inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); } - + boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - + FragmentSpecification subFormulaFragment(inherited.getSpecification()); if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){ subFormulaFragment.setMultiObjectiveFormulasAllowed(false); @@ -228,7 +228,7 @@ namespace storm { if(!inherited.getSpecification().areNestedOperatorsInsideMultiObjectiveFormulasAllowed()){ subFormulaFragment.setNestedOperatorsAllowed(false); } - + bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); for(auto const& subF : f.getSubformulas()){ if(inherited.getSpecification().areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()){ @@ -238,7 +238,7 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(QuantileFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); if (!inherited.getSpecification().areQuantileFormulasAllowed()) { @@ -246,7 +246,7 @@ namespace storm { } return f.getSubformula().accept(*this, data); } - + boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areNextFormulasAllowed(); @@ -256,7 +256,7 @@ namespace storm { result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; } - + boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); @@ -270,7 +270,7 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areRewardOperatorsAllowed(); @@ -278,7 +278,7 @@ namespace storm { result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation); - + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { @@ -286,21 +286,21 @@ namespace storm { } return result; } - + boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); result = result && inherited.getSpecification().areTotalRewardFormulasAllowed(); return result; } - + boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed(); result = result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; } - + boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areUntilFormulasAllowed(); diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9fd7353b9..96cbaf181 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -5,34 +5,34 @@ namespace storm { namespace logic { - + FragmentSpecification propositional() { FragmentSpecification propositional; - + propositional.setBooleanLiteralFormulasAllowed(true); propositional.setBinaryBooleanStateFormulasAllowed(true); propositional.setUnaryBooleanStateFormulasAllowed(true); propositional.setAtomicExpressionFormulasAllowed(true); propositional.setAtomicLabelFormulasAllowed(true); - + return propositional; } - + FragmentSpecification reachability() { FragmentSpecification reachability = propositional(); - + reachability.setProbabilityOperatorsAllowed(true); reachability.setUntilFormulasAllowed(true); reachability.setReachabilityProbabilityFormulasAllowed(true); reachability.setOperatorAtTopLevelRequired(true); reachability.setNestedOperatorsAllowed(false); - + return reachability; } - + FragmentSpecification pctl() { FragmentSpecification pctl = propositional(); - + pctl.setProbabilityOperatorsAllowed(true); pctl.setGloballyFormulasAllowed(true); pctl.setReachabilityProbabilityFormulasAllowed(true); @@ -76,34 +76,34 @@ namespace storm { prctl.setLongRunAverageOperatorsAllowed(true); prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); - + return prctl; } - + FragmentSpecification csl() { FragmentSpecification csl = pctl(); - + csl.setTimeBoundedUntilFormulasAllowed(true); - + return csl; } - + FragmentSpecification csrl() { FragmentSpecification csrl = csl(); - + csrl.setRewardOperatorsAllowed(true); csrl.setCumulativeRewardFormulasAllowed(true); csrl.setInstantaneousFormulasAllowed(true); csrl.setReachabilityRewardFormulasAllowed(true); csrl.setLongRunAverageOperatorsAllowed(true); csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true); - + return csrl; } - + FragmentSpecification multiObjective() { FragmentSpecification multiObjective = propositional(); - + multiObjective.setMultiObjectiveFormulasAllowed(true); multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true); multiObjective.setNestedMultiObjectiveFormulasAllowed(false); @@ -125,10 +125,10 @@ namespace storm { return multiObjective; } - + FragmentSpecification quantiles() { FragmentSpecification quantiles = propositional(); - + quantiles.setQuantileFormulasAllowed(true); quantiles.setQuantileFormulaAtTopLevelRequired(true); quantiles.setProbabilityOperatorsAllowed(true); @@ -143,44 +143,44 @@ namespace storm { quantiles.setCumulativeRewardFormulasAllowed(true); quantiles.setMultiDimensionalBoundedUntilFormulasAllowed(true); quantiles.setMultiDimensionalCumulativeRewardFormulasAllowed(true); - + return quantiles; } - + FragmentSpecification::FragmentSpecification() { probabilityOperator = false; rewardOperator = false; expectedTimeOperator = false; longRunAverageOperator = false; - + multiObjectiveFormula = false; quantileFormula = false; - + globallyFormula = false; reachabilityProbabilityFormula = false; nextFormula = false; untilFormula = false; boundedUntilFormula = false; - + atomicExpressionFormula = false; atomicLabelFormula = false; booleanLiteralFormula = false; unaryBooleanStateFormula = false; binaryBooleanStateFormula = false; - + cumulativeRewardFormula = false; instantaneousRewardFormula = false; reachabilityRewardFormula = false; longRunAverageRewardFormula = false; totalRewardFormula = false; - + conditionalProbabilityFormula = false; conditionalRewardFormula = false; - + reachabilityTimeFormula = false; - + gameFormula = false; - + nestedOperators = true; nestedPathFormulas = false; nestedMultiObjectiveFormulas = false; @@ -195,296 +195,296 @@ namespace storm { rewardBoundedCumulativeRewardFormulas = false; multiDimensionalCumulativeRewardFormulas = false; varianceAsMeasureType = false; - + qualitativeOperatorResults = true; quantitativeOperatorResults = true; - + operatorAtTopLevelRequired = false; multiObjectiveFormulaAtTopLevelRequired = false; operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false; quantileFormulaAtTopLevelRequired = false; - + rewardAccumulation = false; } - + FragmentSpecification FragmentSpecification::copy() const { return FragmentSpecification(*this); } - + bool FragmentSpecification::areProbabilityOperatorsAllowed() const { return probabilityOperator; } - + FragmentSpecification& FragmentSpecification::setProbabilityOperatorsAllowed(bool newValue) { this->probabilityOperator = newValue; return *this; } - + bool FragmentSpecification::areRewardOperatorsAllowed() const { return rewardOperator; } - + FragmentSpecification& FragmentSpecification::setRewardOperatorsAllowed(bool newValue) { this->rewardOperator = newValue; return *this; } - + bool FragmentSpecification::areTimeOperatorsAllowed() const { return expectedTimeOperator; } - + FragmentSpecification& FragmentSpecification::setTimeOperatorsAllowed(bool newValue) { this->expectedTimeOperator = newValue; return *this; } - + bool FragmentSpecification::areLongRunAverageOperatorsAllowed() const { return longRunAverageOperator; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageOperatorsAllowed(bool newValue) { this->longRunAverageOperator = newValue; return *this; } - + bool FragmentSpecification::areMultiObjectiveFormulasAllowed() const { return multiObjectiveFormula; } - + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulasAllowed( bool newValue) { this->multiObjectiveFormula = newValue; return *this; } - + bool FragmentSpecification::areQuantileFormulasAllowed() const { return quantileFormula; } - + FragmentSpecification& FragmentSpecification::setQuantileFormulasAllowed( bool newValue) { this->quantileFormula = newValue; return *this; } - + bool FragmentSpecification::areGloballyFormulasAllowed() const { return globallyFormula; } - + FragmentSpecification& FragmentSpecification::setGloballyFormulasAllowed(bool newValue) { this->globallyFormula = newValue; return *this; } - + bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const { return reachabilityProbabilityFormula; } - + FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) { this->reachabilityProbabilityFormula = newValue; return *this; } - + bool FragmentSpecification::areNextFormulasAllowed() const { return nextFormula; } - + FragmentSpecification& FragmentSpecification::setNextFormulasAllowed(bool newValue) { this->nextFormula = newValue; return *this; } - + bool FragmentSpecification::areUntilFormulasAllowed() const { return untilFormula; } - + FragmentSpecification& FragmentSpecification::setUntilFormulasAllowed(bool newValue) { this->untilFormula = newValue; return *this; } - + bool FragmentSpecification::areBoundedUntilFormulasAllowed() const { return boundedUntilFormula; } - + FragmentSpecification& FragmentSpecification::setBoundedUntilFormulasAllowed(bool newValue) { this->boundedUntilFormula = newValue; return *this; } - + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { return atomicExpressionFormula; } - + FragmentSpecification& FragmentSpecification::setAtomicExpressionFormulasAllowed(bool newValue) { this->atomicExpressionFormula = newValue; return *this; } - + bool FragmentSpecification::areAtomicLabelFormulasAllowed() const { return atomicLabelFormula; } - + FragmentSpecification& FragmentSpecification::setAtomicLabelFormulasAllowed(bool newValue) { this->atomicLabelFormula = newValue; return *this; } - + bool FragmentSpecification::areBooleanLiteralFormulasAllowed() const { return booleanLiteralFormula; } - + FragmentSpecification& FragmentSpecification::setBooleanLiteralFormulasAllowed(bool newValue) { this->booleanLiteralFormula = newValue; return *this; } - + bool FragmentSpecification::areUnaryBooleanStateFormulasAllowed() const { return unaryBooleanStateFormula; } - + FragmentSpecification& FragmentSpecification::setUnaryBooleanStateFormulasAllowed(bool newValue) { this->unaryBooleanStateFormula = newValue; return *this; } - + bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const { return binaryBooleanStateFormula; } - + FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) { this->binaryBooleanStateFormula = newValue; return *this; } - + bool FragmentSpecification::areCumulativeRewardFormulasAllowed() const { return cumulativeRewardFormula; } - + FragmentSpecification& FragmentSpecification::setCumulativeRewardFormulasAllowed(bool newValue) { this->cumulativeRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areInstantaneousRewardFormulasAllowed() const { return instantaneousRewardFormula; } - + FragmentSpecification& FragmentSpecification::setInstantaneousFormulasAllowed(bool newValue) { this->instantaneousRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areReachabilityRewardFormulasAllowed() const { return reachabilityRewardFormula; } - + FragmentSpecification& FragmentSpecification::setReachabilityRewardFormulasAllowed(bool newValue) { this->reachabilityRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areLongRunAverageRewardFormulasAllowed() const { return longRunAverageRewardFormula; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageRewardFormulasAllowed(bool newValue) { this->longRunAverageRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areTotalRewardFormulasAllowed() const { return totalRewardFormula; } - + FragmentSpecification& FragmentSpecification::setTotalRewardFormulasAllowed(bool newValue) { this->totalRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const { return conditionalProbabilityFormula; } - + FragmentSpecification& FragmentSpecification::setConditionalProbabilityFormulasAllowed(bool newValue) { this->conditionalProbabilityFormula = newValue; return *this; } - + bool FragmentSpecification::areConditionalRewardFormulasFormulasAllowed() const { return conditionalRewardFormula; } - + FragmentSpecification& FragmentSpecification::setConditionalRewardFormulasAllowed(bool newValue) { this->conditionalRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areReachbilityTimeFormulasAllowed() const { return reachabilityTimeFormula; } - + FragmentSpecification& FragmentSpecification::setReachbilityTimeFormulasAllowed(bool newValue) { this->reachabilityTimeFormula = newValue; return *this; } - + bool FragmentSpecification::areNestedOperatorsAllowed() const { return this->nestedOperators; } - + FragmentSpecification& FragmentSpecification::setNestedOperatorsAllowed(bool newValue) { this->nestedOperators = newValue; return *this; } - + bool FragmentSpecification::areNestedPathFormulasAllowed() const { return this->nestedPathFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedPathFormulasAllowed(bool newValue) { this->nestedPathFormulas = newValue; return *this; } - + bool FragmentSpecification::areNestedMultiObjectiveFormulasAllowed() const { return this->nestedMultiObjectiveFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedMultiObjectiveFormulasAllowed(bool newValue) { this->nestedMultiObjectiveFormulas = newValue; return *this; } - + bool FragmentSpecification::areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const { return this->nestedOperatorsInsideMultiObjectiveFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue) { this->nestedOperatorsInsideMultiObjectiveFormulas = newValue; return *this; } - + bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const { return this->onlyEventuallyFormuluasInConditionalFormulas; } - + FragmentSpecification& FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue) { this->onlyEventuallyFormuluasInConditionalFormulas = newValue; return *this; } - + bool FragmentSpecification::areStepBoundedUntilFormulasAllowed() const { return this->stepBoundedUntilFormulas; } - + FragmentSpecification& FragmentSpecification::setStepBoundedUntilFormulasAllowed(bool newValue) { this->stepBoundedUntilFormulas = newValue; return *this; } - + bool FragmentSpecification::areTimeBoundedUntilFormulasAllowed() const { return this->timeBoundedUntilFormulas; } - + FragmentSpecification& FragmentSpecification::setTimeBoundedUntilFormulasAllowed(bool newValue) { this->timeBoundedUntilFormulas = newValue; return *this; @@ -498,7 +498,7 @@ namespace storm { this->rewardBoundedUntilFormulas = newValue; return *this; } - + bool FragmentSpecification::areMultiDimensionalBoundedUntilFormulasAllowed() const { return this->multiDimensionalBoundedUntilFormulas; } @@ -511,16 +511,16 @@ namespace storm { bool FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed() const { return this->stepBoundedCumulativeRewardFormulas; } - + FragmentSpecification& FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed(bool newValue) { this->stepBoundedCumulativeRewardFormulas = newValue; return *this; } - + bool FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed() const { return this->timeBoundedCumulativeRewardFormulas; } - + FragmentSpecification& FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue) { this->timeBoundedCumulativeRewardFormulas = newValue; return *this; @@ -534,7 +534,7 @@ namespace storm { this->rewardBoundedCumulativeRewardFormulas = newValue; return *this; } - + bool FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed() const { return this->multiDimensionalCumulativeRewardFormulas; } @@ -543,7 +543,7 @@ namespace storm { this->multiDimensionalCumulativeRewardFormulas = newValue; return *this; } - + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); @@ -551,40 +551,40 @@ namespace storm { this->setTimeOperatorsAllowed(newValue); return *this; } - + FragmentSpecification& FragmentSpecification::setTimeAllowed(bool newValue) { this->setTimeOperatorsAllowed(newValue); this->setReachbilityTimeFormulasAllowed(newValue); return *this; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageProbabilitiesAllowed(bool newValue) { this->setLongRunAverageOperatorsAllowed(newValue); return *this; } - + bool FragmentSpecification::isVarianceMeasureTypeAllowed() const { return varianceAsMeasureType; } - + FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) { this->varianceAsMeasureType = newValue; return *this; } - + bool FragmentSpecification::areQuantitativeOperatorResultsAllowed() const { return this->quantitativeOperatorResults; } - + FragmentSpecification& FragmentSpecification::setQuantitativeOperatorResultsAllowed(bool newValue) { this->quantitativeOperatorResults = newValue; return *this; } - + bool FragmentSpecification::areQualitativeOperatorResultsAllowed() const { return this->qualitativeOperatorResults; } - + FragmentSpecification& FragmentSpecification::setQualitativeOperatorResultsAllowed(bool newValue) { this->qualitativeOperatorResults = newValue; return *this; @@ -593,7 +593,7 @@ namespace storm { bool FragmentSpecification::isOperatorAtTopLevelRequired() const { return operatorAtTopLevelRequired; } - + FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) { operatorAtTopLevelRequired = newValue; return *this; @@ -602,7 +602,7 @@ namespace storm { bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const { return multiObjectiveFormulaAtTopLevelRequired; } - + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) { multiObjectiveFormulaAtTopLevelRequired = newValue; return *this; @@ -611,7 +611,7 @@ namespace storm { bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const { return operatorsAtTopLevelOfMultiObjectiveFormulasRequired; } - + FragmentSpecification& FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue) { operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue; return *this; diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 19cf232ed..8ac56b885 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -6,9 +6,9 @@ namespace storm { namespace logic { - + class RewardAccumulation; - + class FragmentSpecification { public: FragmentSpecification(); @@ -16,24 +16,24 @@ namespace storm { FragmentSpecification(FragmentSpecification&& other) = default; FragmentSpecification& operator=(FragmentSpecification const& other) = default; FragmentSpecification& operator=(FragmentSpecification&& other) = default; - + FragmentSpecification copy() const; - + bool areProbabilityOperatorsAllowed() const; FragmentSpecification& setProbabilityOperatorsAllowed(bool newValue); - + bool areRewardOperatorsAllowed() const; FragmentSpecification& setRewardOperatorsAllowed(bool newValue); - + bool areTimeOperatorsAllowed() const; FragmentSpecification& setTimeOperatorsAllowed(bool newValue); bool areLongRunAverageOperatorsAllowed() const; FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue); - + bool areMultiObjectiveFormulasAllowed() const; FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue); - + bool areQuantileFormulasAllowed() const; FragmentSpecification& setQuantileFormulasAllowed( bool newValue); @@ -75,10 +75,10 @@ namespace storm { bool areReachabilityRewardFormulasAllowed() const; FragmentSpecification& setReachabilityRewardFormulasAllowed(bool newValue); - + bool areLongRunAverageRewardFormulasAllowed() const; FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue); - + bool areTotalRewardFormulasAllowed() const; FragmentSpecification& setTotalRewardFormulasAllowed(bool newValue); @@ -156,7 +156,7 @@ namespace storm { bool areGameFormulasAllowed() const; FragmentSpecification& setGameFormulasAllowed(bool newValue); - + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -217,16 +217,16 @@ namespace storm { bool multiObjectiveFormulaAtTopLevelRequired; bool quantileFormulaAtTopLevelRequired; bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired; - + bool rewardAccumulation; }; - + // Propositional. FragmentSpecification propositional(); - + // Just reachability properties. FragmentSpecification reachability(); - + // Regular PCTL. FragmentSpecification pctl(); @@ -238,16 +238,16 @@ namespace storm { // PCTL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctl(); - + // Regular CSL. FragmentSpecification csl(); - + // CSL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification csrl(); - + // Multi-Objective formulas. FragmentSpecification multiObjective(); - + // Quantile formulas. FragmentSpecification quantiles(); diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp index 64fdc60b8..8387e38fd 100644 --- a/src/storm/logic/GameFormula.cpp +++ b/src/storm/logic/GameFormula.cpp @@ -23,7 +23,11 @@ namespace storm { PlayerCoalition const& GameFormula::getCoalition() const { return coalition; } - + + void GameFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + } + boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h index bc57583eb..4ccb2de03 100644 --- a/src/storm/logic/GameFormula.h +++ b/src/storm/logic/GameFormula.h @@ -19,7 +19,7 @@ namespace storm { virtual bool isGameFormula() const override; virtual bool hasQualitativeResult() const override; virtual bool hasQuantitativeResult() const override; - + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index 22ff54cdd..ce17bb60e 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -5,38 +5,38 @@ namespace storm { namespace logic { - + LiftableTransitionRewardsVisitor::LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription) : symbolicModelDescription(symbolicModelDescription) { // Intentionally left empty. } - + bool LiftableTransitionRewardsVisitor::areTransitionRewardsLiftable(Formula const& f) const { return boost::any_cast(f.accept(*this, boost::any())); } - + boost::any LiftableTransitionRewardsVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(AtomicLabelFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { for (unsigned i = 0; i < f.getDimension(); ++i) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { return false; } } - + bool result = true; if (f.hasMultiDimensionalSubformulas()) { for (unsigned i = 0; i < f.getDimension(); ++i) { @@ -49,11 +49,11 @@ namespace storm { } return result; } - + boost::any LiftableTransitionRewardsVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { return !f.isConditionalRewardFormula() && boost::any_cast(f.getSubformula().accept(*this, data)) && boost::any_cast(f.getConditionFormula().accept(*this, data)); } - + boost::any LiftableTransitionRewardsVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { for (unsigned i = 0; i < f.getDimension(); ++i) { if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) { @@ -100,35 +100,35 @@ namespace storm { } return result; } - + boost::any LiftableTransitionRewardsVisitor::visit(QuantileFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const { return boost::any_cast(f.getSubformula().accept(*this, data)); } - + boost::any LiftableTransitionRewardsVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { return boost::any_cast(f.getSubformula().accept(*this, data)); } - + boost::any LiftableTransitionRewardsVisitor::visit(TotalRewardFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const { return boost::any_cast(f.getLeftSubformula().accept(*this, data)) && boost::any_cast(f.getRightSubformula().accept(*this)); } - + bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const { if (symbolicModelDescription.hasModel()) { if (symbolicModelDescription.isJaniModel()) { diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 3704215d4..be7b14ae6 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -54,6 +54,8 @@ namespace storm { return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(formula.asMultiObjectiveFormula())); } else if (formula.isQuantileFormula()){ return this->checkQuantileFormula(env, checkTask.substituteFormula(formula.asQuantileFormula())); + } else if(formula.isGameFormula()){ + return this->checkGameFormula(env, checkTask.substituteFormula(formula.asGameFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h index 6630dd5ad..5b8ed6419 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h @@ -93,8 +93,8 @@ namespace storm { * @param actionValuesGetter a function returning a value for a given (global) choice index * @return a value for each state */ - std::vector computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter); - + virtual std::vector computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter); + /*! * @param stateValuesGetter a function returning a value for a given state index * @param actionValuesGetter a function returning a value for a given (global) choice index diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp new file mode 100644 index 000000000..34a1a8d93 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -0,0 +1,135 @@ +#include "SparseNondeterministicGameInfiniteHorizonHelper.h" + +#include "storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h" + +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/GameMaximalEndComponentDecomposition.h" +#include "storm/storage/Scheduler.h" + +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" + +#include "storm/utility/solver.h" +#include "storm/utility/vector.h" + +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +#include "storm/exceptions/UnmetRequirementException.h" +#include "storm/exceptions/InternalException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player) : SparseInfiniteHorizonHelper(transitionMatrix), player(player) { + // Intentionally left empty. + } + + template + std::vector const& SparseNondeterministicGameInfiniteHorizonHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + std::vector& SparseNondeterministicGameInfiniteHorizonHelper::getProducedOptimalChoices() { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); + } + + template + storm::storage::Scheduler SparseNondeterministicGameInfiniteHorizonHelper::extractScheduler() const { + auto const& optimalChoices = getProducedOptimalChoices(); + storm::storage::Scheduler scheduler(optimalChoices.size()); + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { + scheduler.setChoice(optimalChoices[state], state); + } + return scheduler; + } + + + template + void SparseNondeterministicGameInfiniteHorizonHelper::createDecomposition() { + // TODO This needs to be changed to return the whole model as one component as long as there is no overwritten version of MaximalEndComponentDecomposition for SMGs. + if (this->_longRunComponentDecomposition == nullptr) { + // The decomposition has not been provided or computed, yet. + if (this->_backwardTransitions == nullptr) { + this->_computedBackwardTransitions = std::make_unique>(this->_transitionMatrix.transpose(true)); + this->_backwardTransitions = this->_computedBackwardTransitions.get(); + } + this->_computedLongRunComponentDecomposition = std::make_unique>(this->_transitionMatrix, *this->_backwardTransitions); + + this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get(); + //STORM_LOG_DEBUG("\n" << this->_transitionMatrix); + STORM_LOG_DEBUG("GMEC: " << *(this->_longRunComponentDecomposition)); + } + } + + template + std::vector SparseNondeterministicGameInfiniteHorizonHelper::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) { + auto underlyingSolverEnvironment = env; + std::vector componentLraValues; + createDecomposition(); + componentLraValues.reserve(this->_longRunComponentDecomposition->size()); + for (auto const& c : *(this->_longRunComponentDecomposition)) { + componentLraValues.push_back(computeLraForComponent(underlyingSolverEnvironment, stateValuesGetter, actionValuesGetter, c)); + } + return componentLraValues; + } + + template + ValueType SparseNondeterministicGameInfiniteHorizonHelper::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) { + // Allocate memory for the nondeterministic choices. + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); + if (method == storm::solver::LraMethod::LinearProgramming) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); + } else if (method == storm::solver::LraMethod::ValueIteration) { + return computeLraVi(env, stateRewardsGetter, actionRewardsGetter, component); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); + } + } + + template + ValueType SparseNondeterministicGameInfiniteHorizonHelper::computeLraVi(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) { + + // Collect some parameters of the computation + ValueType aperiodicFactor = storm::utility::convertNumber(env.solver().lra().getAperiodicFactor()); + std::vector* optimalChoices = nullptr; + if (this->isProduceSchedulerSet()) { + optimalChoices = &this->_producedOptimalChoices.get(); + } + + // Now create a helper and perform the algorithm + if (this->isContinuousTime()) { + STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games."); + } else { + storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor); + return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); + } + } + + template + std::vector SparseNondeterministicGameInfiniteHorizonHelper::buildAndSolveSsp(Environment const& env, std::vector const& componentLraValues) { + STORM_LOG_THROW(false, storm::exceptions::InternalException, "We do not create compositions for LRA for SMGs, solving a stochastic shortest path problem is not available."); + } + + + template class SparseNondeterministicGameInfiniteHorizonHelper; + template class SparseNondeterministicGameInfiniteHorizonHelper; + + } + } +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h new file mode 100644 index 000000000..f6075dc57 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h @@ -0,0 +1,73 @@ +#pragma once + +#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h" + +namespace storm { + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + + /*! + * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system with different players choices. + * @tparam ValueType the type a value can have + */ + template + class SparseNondeterministicGameInfiniteHorizonHelper : public SparseInfiniteHorizonHelper { + + public: + + /*! + * Function mapping from indices to values + */ + typedef typename SparseInfiniteHorizonHelper::ValueGetter ValueGetter; + + /*! + * Initializes the helper for a discrete time model with different players (i.e. SMG) + */ + SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player); + + /*! TODO + * Computes the long run average value given the provided state and action based rewards + * @param stateValuesGetter a function returning a value for a given state index + * @param actionValuesGetter a function returning a value for a given (global) choice index + * @return a value for each state + */ + std::vector computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) override; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector const& getProducedOptimalChoices() const; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + std::vector& getProducedOptimalChoices(); + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call. + */ + storm::storage::Scheduler extractScheduler() const; + + ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component); + + ValueType computeLraVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); + + void createDecomposition(); + std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues); + + private: + std::vector> player; + }; + + + } + } +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 2a4f6950a..e5aeecdd3 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -14,6 +14,7 @@ #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" #include "storm/exceptions/UnmetRequirementException.h" @@ -23,11 +24,11 @@ namespace storm { namespace modelchecker { namespace helper { namespace internal { - + template LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) { setComponent(component); - + // Run through the component and collect some data: // We create two submodels, one consisting of the timed states of the component and one consisting of the instant states of the component. // For this, we create a state index map that point from state indices of the input model to indices of the corresponding submodel of that state. @@ -140,8 +141,9 @@ namespace storm { _IsTransitions = isTransitionsBuilder.build(); _IsToTsTransitions = isToTsTransitionsBuilder.build(); } + STORM_LOG_DEBUG(uniformizationFactor << " - " << _uniformizationRate); } - + template void LraViHelper::setComponent(ComponentType component) { _component.clear(); @@ -155,7 +157,7 @@ namespace storm { } } - + template ValueType LraViHelper::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector* choices) { initializeNewValues(stateValueGetter, actionValueGetter, exitRates); @@ -165,26 +167,43 @@ namespace storm { if (env.solver().lra().isMaximalIterationCountSet()) { maxIter = env.solver().lra().getMaximalIterationCount(); } - + // start the iterations ValueType result = storm::utility::zero(); uint64_t iter = 0; while (!maxIter.is_initialized() || iter < maxIter.get()) { ++iter; performIterationStep(env, dir); - + + std::vector xOldTemp = xOld(); + std::vector xNewTemp = xNew(); + if(gameNondetTs() && iter > 1) { + // Weight values with current iteration step + storm::utility::vector::applyPointwise(xOld(), xOld(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)(iter - 1); }); + storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); + } // Check if we are done auto convergenceCheckResult = checkConvergence(relative, precision); result = convergenceCheckResult.currentValue; + + if(gameNondetTs() && iter > 1) { + xOld() = xOldTemp; + xNew() = xNewTemp; + } + if (convergenceCheckResult.isPrecisionAchieved) { break; } if (storm::utility::resources::isTerminate()) { break; } + + // If there will be a next iteration, we have to prepare it. - prepareNextIteration(env); - + if(!gameNondetTs()) { + prepareNextIteration(env); + } + } if (maxIter.is_initialized() && iter == maxIter.get()) { STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations."); @@ -193,15 +212,24 @@ namespace storm { } else { STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations."); } - + if (choices) { // We will be doing one more iteration step and track scheduler choices this time. - prepareNextIteration(env); + if(!gameNondetTs()) { + prepareNextIteration(env); + } performIterationStep(env, dir, choices); } + std::cout << "result (" << iter << " steps):" << std::endl; + storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); + for(int i = 0; i < xNew().size() ; i++ ) { + std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl; + //if(i == 50) {std::cout << "only showing top 50 lines"; break; } + } + if(gameNondetTs()) result = xOld().at(0) * _uniformizationRate; // TODO is "init" always going to be .at(0) ? return result; } - + template void LraViHelper::initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates) { // clear potential old values and reserve enough space for new values @@ -211,7 +239,7 @@ namespace storm { _IsChoiceValues.clear(); _IsChoiceValues.reserve(_IsTransitions.getRowCount()); } - + // Set the new choice-based values ValueType actionRewardScalingFactor = storm::utility::one() / _uniformizationRate; for (auto const& element : _component) { @@ -236,14 +264,14 @@ namespace storm { // Set-up new iteration vectors for timed states _Tsx1.assign(_TsTransitions.getRowGroupCount(), storm::utility::zero()); _Tsx2 = _Tsx1; - + if (_hasInstantStates) { // Set-up vectors for storing intermediate results for instant states. _Isx.resize(_IsTransitions.getRowGroupCount(), storm::utility::zero()); _Isb = _IsChoiceValues; } } - + template void LraViHelper::prepareSolversAndMultipliers(const Environment& env, storm::solver::OptimizationDirection const* dir) { _TsMultiplier = storm::solver::MultiplierFactory().create(env, _TsTransitions); @@ -301,13 +329,16 @@ namespace storm { STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been cleared."); } } - + // Set up multipliers for transitions connecting timed and instant states _TsToIsMultiplier = storm::solver::MultiplierFactory().create(env, _TsToIsTransitions); _IsToTsMultiplier = storm::solver::MultiplierFactory().create(env, _IsToTsTransitions); } + if(env.solver().multiplier().getOptimizationDirectionOverride().is_initialized()) { + _TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get()); + } } - + template void LraViHelper::setInputModelChoices(std::vector& choices, std::vector const& localMecChoices, bool setChoiceZeroToTimedStates, bool setChoiceZeroToInstantStates) const { // Transform the local choices (within this mec) to choice indices for the input model @@ -330,7 +361,7 @@ namespace storm { } STORM_LOG_ASSERT(localState == localMecChoices.size(), "Did not traverse all component states."); } - + template void LraViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector* choices) { STORM_LOG_ASSERT(!((nondetTs() || nondetIs()) && dir == nullptr), "No optimization direction provided for model with nondeterminism"); @@ -338,15 +369,15 @@ namespace storm { if (!_TsMultiplier) { prepareSolversAndMultipliers(env, dir); } - + // Compute new x values for the timed states // Flip what is new and what is old _Tsx1IsCurrent = !_Tsx1IsCurrent; // At this point, xOld() points to what has been computed in the most recent call of performIterationStep (initially, this is the 0-vector). // The result of this ongoing computation will be stored in xNew() - + // Compute the values obtained by a single uniformization step between timed states only - if (nondetTs()) { + if (nondetTs() && !gameNondetTs()) { if (choices == nullptr) { _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew()); } else { @@ -358,6 +389,14 @@ namespace storm { STORM_LOG_ASSERT(!_hasInstantStates, "Nondeterministic timed states are only supported if there are no instant states."); setInputModelChoices(*choices, tsChoices); } + } else if(gameNondetTs()) { // TODO DRYness? exact same behaviour as case above? + if (choices == nullptr) { + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew()); + } else { + std::vector tsChoices(_TsTransitions.getRowGroupCount()); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); + setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? + } } else { _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, xNew()); } @@ -400,7 +439,7 @@ namespace storm { _TsToIsMultiplier->multiply(env, _Isx, &xNew(), xNew()); } } - + template typename LraViHelper::ConvergenceCheckResult LraViHelper::checkConvergence(bool relative, ValueType precision) const { STORM_LOG_ASSERT(_TsMultiplier, "tried to check for convergence without doing an iteration first."); @@ -408,7 +447,7 @@ namespace storm { // We need to 'revert' this scaling when computing the absolute precision. // However, for relative precision, the scaling cancels out. ValueType threshold = relative ? precision : ValueType(precision / _uniformizationRate); - + ConvergenceCheckResult res = { true, storm::utility::one() }; // Now check whether the currently produced results are precise enough STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); @@ -435,15 +474,15 @@ namespace storm { break; } } - + // Compute the average of the maximal and the minimal difference. ValueType avgDiff = (maxDiff + minDiff) / (storm::utility::convertNumber(2.0)); - + // "Undo" the scaling of the values res.currentValue = avgDiff * _uniformizationRate; return res; } - + template void LraViHelper::prepareNextIteration(Environment const& env) { // To avoid large (and numerically unstable) x-values, we substract a reference value. @@ -455,53 +494,60 @@ namespace storm { _IsToTsMultiplier->multiply(env, xNew(), &_IsChoiceValues, _Isb); } } - + template bool LraViHelper::isTimedState(uint64_t const& inputModelStateIndex) const { STORM_LOG_ASSERT(!_hasInstantStates || _timedStates != nullptr, "Model has instant states but no partition into timed and instant states is given."); STORM_LOG_ASSERT(!_hasInstantStates || inputModelStateIndex < _timedStates->size(), "Unable to determine whether state " << inputModelStateIndex << " is timed."); return !_hasInstantStates || _timedStates->get(inputModelStateIndex); } - + template std::vector& LraViHelper::xNew() { return _Tsx1IsCurrent ? _Tsx1 : _Tsx2; } - + template std::vector const& LraViHelper::xNew() const { return _Tsx1IsCurrent ? _Tsx1 : _Tsx2; } - + template std::vector& LraViHelper::xOld() { return _Tsx1IsCurrent ? _Tsx2 : _Tsx1; } - + template std::vector const& LraViHelper::xOld() const { return _Tsx1IsCurrent ? _Tsx2 : _Tsx1; } - + template bool LraViHelper::nondetTs() const { - return TransitionsType == LraViTransitionsType::NondetTsNoIs; + return TransitionsType == LraViTransitionsType::NondetTsNoIs || gameNondetTs(); } - + template bool LraViHelper::nondetIs() const { return TransitionsType == LraViTransitionsType::DetTsNondetIs; } - + + template + bool LraViHelper::gameNondetTs() const { + return TransitionsType == LraViTransitionsType::GameNondetTsNoIs; + } + template class LraViHelper; template class LraViHelper; + template class LraViHelper; + template class LraViHelper; template class LraViHelper; template class LraViHelper; - + template class LraViHelper; template class LraViHelper; - + } } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index bbf9207a4..c800a9976 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -25,9 +25,10 @@ namespace storm { DetTsNoIs, /// deterministic choice at timed states, no instant states (as in DTMCs and CTMCs) DetTsNondetIs, /// deterministic choice at timed states, nondeterministic choice at instant states (as in Markov Automata) DetTsDetIs, /// deterministic choice at timed states, deterministic choice at instant states (as in Markov Automata without any nondeterminisim) - NondetTsNoIs /// nondeterministic choice at timed states, no instant states (as in MDPs) + NondetTsNoIs, /// nondeterministic choice at timed states, no instant states (as in MDPs) + GameNondetTsNoIs // nondeterministic choices of different players at timed states, no instant states (as in SMGs) }; - + /*! * Helper class that performs iterations of the value iteration method. * The purpose of the template parameters ComponentType and TransitionsType are used to make this work for various model types. @@ -127,7 +128,9 @@ namespace storm { /// @return true iff there potentially is a nondeterministic choice at instant states. Returns false if there are no instant states. bool nondetIs() const; - + /// @return true iff there potentially are nondeterministic choices for different players at timed states + bool gameNondetTs() const; + void setComponent(ComponentType component); // We need to make sure that states/choices will be processed in ascending order diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6c42b3e30..fbfcd796f 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -2,6 +2,8 @@ #include #include +#include +#include #include "storm/utility/macros.h" #include "storm/utility/FilteredRewardModel.h" @@ -12,6 +14,10 @@ #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/logic/Coalition.h" + +#include "storm/storage/BitVector.h" +#include "storm/environment/solver/MultiplierEnvironment.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -27,6 +33,8 @@ namespace storm { // Intentionally left empty. } + + template bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); @@ -44,14 +52,46 @@ namespace storm { } } + + template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula(); - if (subFormula.isOperatorFormula()) { - return this->checkStateFormula(env, checkTask.substituteFormula(subFormula.asStateFormula()).setPlayerCoalition(gameFormula.getCoalition())); + + if (subFormula.isRewardOperatorFormula()) { + return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula())); + } else if (subFormula.isLongRunAverageOperatorFormula()) { + return this->checkLongRunAverageOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asLongRunAverageOperatorFormula())); + } + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Cannot check this property (yet)."); + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); + std::unique_ptr result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); + + return result; + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) { + storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula(); + std::unique_ptr result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula())); + + return result; + } + + + + template + std::unique_ptr SparseSmgRpatlModelChecker::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + storm::logic::Formula const& rewardFormula = checkTask.getFormula(); + if (rewardFormula.isLongRunAverageRewardFormula()) { + return this->computeLongRunAverageRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); } - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Only game formulas with Operatorformulas as subformula are supported."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' cannot (yet) be handled."); } template @@ -62,10 +102,15 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set."); - auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition()); - std::cout << "Found " << coalitionStates.getNumberOfSetBits() << " states in coalition." << std::endl; - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented."); + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getPlayerActionIndices()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; } template class SparseSmgRpatlModelChecker>; diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index 40481ee06..af9846f19 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -37,7 +37,6 @@ namespace storm { storm::storage::PlayerIndex Smg::getPlayerOfState(uint64_t stateIndex) const { STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << "."); return statePlayerIndications[stateIndex]; - } template storm::storage::PlayerIndex Smg::getPlayerIndex(std::string const& playerName) const { @@ -62,7 +61,7 @@ namespace storm { for (auto const& pi : coalitionAsIndexSet) { coalitionAsBitVector.set(pi); } - + // Now create the actual result storm::storage::BitVector result(this->getNumberOfStates(), false); for (uint64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -71,7 +70,7 @@ namespace storm { result.set(state, true); } } - + return result; } diff --git a/src/storm/models/sparse/Smg.h b/src/storm/models/sparse/Smg.h index b16475c18..46e8699a8 100644 --- a/src/storm/models/sparse/Smg.h +++ b/src/storm/models/sparse/Smg.h @@ -34,7 +34,7 @@ namespace storm { storm::storage::PlayerIndex getPlayerOfState(uint64_t stateIndex) const; storm::storage::PlayerIndex getPlayerIndex(std::string const& playerName) const; storm::storage::BitVector computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const; - + private: // Assigns the controlling player to each state. // If a state has storm::storage::INVALID_PLAYER_INDEX, it shall be the case that the choice at that state is unique diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 6e0f727b0..a75ab623f 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -1,5 +1,7 @@ #include "storm/solver/GmmxxMultiplier.h" +#include + #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/IntelTbbAdapter.h" @@ -14,25 +16,26 @@ namespace storm { namespace solver { - + template GmmxxMultiplier::GmmxxMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { // Intentionally left empty. + //STORM_LOG_DEBUG("\n" << matrix); } - + template void GmmxxMultiplier::initialize() const { if (gmmMatrix.nrows() == 0) { gmmMatrix = std::move(*storm::adapters::GmmxxAdapter().toGmmxxSparseMatrix(this->matrix)); } } - + template void GmmxxMultiplier::clearCache() const { gmmMatrix = gmm::csr_matrix(); Multiplier::clearCache(); } - + template bool GmmxxMultiplier::parallelize(Environment const& env) const { #ifdef STORM_HAVE_INTELTBB @@ -41,7 +44,7 @@ namespace storm { return false; #endif } - + template void GmmxxMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { initialize(); @@ -63,7 +66,7 @@ namespace storm { std::swap(result, *this->cachedVector); } } - + template void GmmxxMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards) const { initialize(); @@ -82,7 +85,7 @@ namespace storm { } } } - + template void GmmxxMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { initialize(); @@ -104,13 +107,13 @@ namespace storm { std::swap(result, *this->cachedVector); } } - + template void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { initialize(); multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards); } - + template void GmmxxMultiplier::multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const { initialize(); @@ -146,14 +149,14 @@ namespace storm { } } } - + template template void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; - + typename gmm::linalg_traits::const_iterator add_it, add_ite; if (b) { add_it = backwards ? gmm::vect_end(*b) - 1 : gmm::vect_begin(*b); @@ -166,23 +169,30 @@ namespace storm { choice_it = backwards ? choices->end() - 1 : choices->begin(); } + boost::optional optimizationDirectionOverride; + if(this->getOptimizationDirectionOverride().is_initialized()) { + optimizationDirectionOverride = this->getOptimizationDirectionOverride(); + } + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; uint64_t currentRow = backwards ? gmmMatrix.nrows() - 1 : 0; + uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 1 : 0; auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin(); auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1; + //if(choices) STORM_LOG_DEBUG(" "); while (row_group_it != row_group_ite) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if the row group is not empty. if (*row_group_it != *(row_group_it + 1)) { // Process the (backwards ? last : first) row of the current row group if (b) { currentValue = *add_it; } - + currentValue += vect_sp(gmm::linalg_traits::row(itr), x); if (choices) { @@ -191,7 +201,7 @@ namespace storm { oldSelectedChoiceValue = currentValue; } } - + // move row-based iterators to the next row if (backwards) { --itr; @@ -202,22 +212,28 @@ namespace storm { ++currentRow; ++add_it; } - + // Process the (rowGroupSize-1) remaining rows within the current row Group uint64_t rowGroupSize = *(row_group_it + 1) - *row_group_it; + uint choiceforprintout = 0; + //std::cout << currentRowGroup << ": " << currentValue << ", "; + //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); + //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); for (uint64_t i = 1; i < rowGroupSize; ++i) { ValueType newValue = b ? *add_it : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); - + if (choices && currentRow == *choice_it + *row_group_it) { oldSelectedChoiceValue = newValue; } - - if (compare(newValue, currentValue)) { + //std::cout << newValue << ", "; + //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); + if(this->isOverridden(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *row_group_it; } + choiceforprintout = currentRow - *row_group_it; } // move row-based iterators to the next row if (backwards) { @@ -230,33 +246,39 @@ namespace storm { ++add_it; } } - + //STORM_LOG_DEBUG("\t= " << currentValue << "\tchoice: " << choiceforprintout); + //std::cout << std::fixed << std::setprecision(2) << " | v(" << currentRowGroup << ")=" << currentValue << " c: " << choiceforprintout << " |\n" ; // Finally write value to target vector. *target_it = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choice_it = selectedChoice; + if(choices) { + if(this->isOverridden(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) { + *choice_it = selectedChoice; + } } } - + // move rowGroup-based iterators to the next row group if (backwards) { --row_group_it; --choice_it; --target_it; + --currentRowGroup; } else { ++row_group_it; ++choice_it; ++target_it; + ++currentRowGroup; } } + //std::cout << std::endl; } - + template<> template void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } - + template void GmmxxMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB @@ -274,7 +296,7 @@ namespace storm { multAdd(x, b, result); #endif } - + #ifdef STORM_HAVE_INTELTBB template class TbbMultAddReduceFunctor { @@ -282,14 +304,14 @@ namespace storm { TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { // Intentionally left empty. } - + void operator()(tbb::blocked_range const& range) const { typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; auto groupIt = rowGroupIndices.begin() + range.begin(); auto groupIte = rowGroupIndices.begin() + range.end(); - + auto itr = mat_row_const_begin(matrix) + *groupIt; typename std::vector::const_iterator bIt; if (b) { @@ -299,40 +321,40 @@ namespace storm { if (choices) { choiceIt = choices->begin() + range.begin(); } - + auto resultIt = result.begin() + range.begin(); - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; - + uint64_t currentRow = *groupIt; for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if the row group is not empty. if (*groupIt != *(groupIt + 1)) { if (b) { currentValue = *bIt; ++bIt; } - + currentValue += vect_sp(gmm::linalg_traits::row(itr), x); - + if (choices) { selectedChoice = currentRow - *groupIt; if (*choiceIt == selectedChoice) { oldSelectedChoiceValue = currentValue; } } - + ++itr; ++currentRow; - + for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr, ++bIt, ++currentRow) { ValueType newValue = b ? *bIt : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); - + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { @@ -341,7 +363,7 @@ namespace storm { } } } - + // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { @@ -349,7 +371,7 @@ namespace storm { } } } - + private: Compare compare; std::vector const& rowGroupIndices; @@ -360,7 +382,7 @@ namespace storm { std::vector* choices; }; #endif - + template void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { #ifdef STORM_HAVE_INTELTBB @@ -374,18 +396,18 @@ namespace storm { multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices); #endif } - + template<> void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } - + template class GmmxxMultiplier; - + #ifdef STORM_HAVE_CARL template class GmmxxMultiplier; template class GmmxxMultiplier; #endif - + } } diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 4049b56ca..556a4dfa9 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -18,17 +18,17 @@ namespace storm { namespace solver { - + template Multiplier::Multiplier(storm::storage::SparseMatrix const& matrix) : matrix(matrix) { // Intentionally left empty. } - + template void Multiplier::clearCache() const { cachedVector.reset(); } - + template void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices); @@ -38,7 +38,7 @@ namespace storm { void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards); } - + template void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const { storm::utility::ProgressMeasurement progress("multiplications"); @@ -53,7 +53,7 @@ namespace storm { } } } - + template void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const { storm::utility::ProgressMeasurement progress("multiplications"); @@ -67,17 +67,33 @@ namespace storm { } } } - + template void Multiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const { multiplyRow(rowIndex, x1, val1); multiplyRow(rowIndex, x2, val2); } - + + template + void Multiplier::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) { + optimizationDirectionOverride = optDirOverride; + } + + template + boost::optional Multiplier::getOptimizationDirectionOverride() const { + return optimizationDirectionOverride; + } + + template + bool Multiplier::isOverridden(uint_fast64_t const index) const { + if(!optimizationDirectionOverride.is_initialized()) return false; + return optimizationDirectionOverride.get().get(index); + } + template std::unique_ptr> MultiplierFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) { auto type = env.solver().multiplier().getType(); - + // Adjust the multiplier type if an eqsolver was specified but not a multiplier if (!env.solver().isLinearEquationSolverTypeSetFromDefaultValue() && env.solver().multiplier().isTypeSetFromDefault()) { bool changed = false; @@ -90,7 +106,7 @@ namespace storm { } STORM_LOG_INFO_COND(!changed, "Selecting '" + toString(type) + "' as the multiplier type to match the selected equation solver. If you want to override this, please explicitly specify a different multiplier type."); } - + switch (type) { case MultiplierType::Gmmxx: return std::make_unique>(matrix); @@ -99,16 +115,16 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType"); } - + template class Multiplier; template class MultiplierFactory; - + #ifdef STORM_HAVE_CARL template class Multiplier; template class MultiplierFactory; template class Multiplier; template class MultiplierFactory; #endif - + } } diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index 58aeb4e38..acf754e94 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -2,34 +2,37 @@ #include #include +#include + +#include "storm/storage/BitVector.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/MultiplicationStyle.h" namespace storm { - + class Environment; - + namespace storage { template class SparseMatrix; } - + namespace solver { - + template class Multiplier { public: - + Multiplier(storm::storage::SparseMatrix const& matrix); - + virtual ~Multiplier() = default; - + /* * Clears the currently cached data of this multiplier in order to free some memory. */ virtual void clearCache() const; - + /*! * Performs a matrix-vector multiplication x' = A*x + b. * @@ -41,7 +44,7 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. */ virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const = 0; - + /*! * Performs a matrix-vector multiplication in gauss-seidel style. * @@ -52,7 +55,7 @@ namespace storm { * @param backwards if true, the iterations will be performed beginning from the last row and ending at the first row. */ virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const = 0; - + /*! * Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups * so that the resulting vector has the size of number of row groups of A. @@ -69,7 +72,7 @@ namespace storm { */ void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const = 0; - + /*! * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups * so that the resulting vector has the size of number of row groups of A. @@ -87,7 +90,7 @@ namespace storm { */ void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const = 0; - + /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After * performing the necessary multiplications, the result is written to the input vector x. Note that the @@ -100,7 +103,7 @@ namespace storm { * @param n The number of times to perform the multiplication. */ void repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const; - + /*! * Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups * so that the resulting vector has the size of number of row groups of A. @@ -115,7 +118,7 @@ namespace storm { * @param n The number of times to perform the multiplication. */ void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const; - + /*! * Multiplies the row with the given index with x and adds the result to the provided value * @param rowIndex The index of the considered row @@ -123,7 +126,7 @@ namespace storm { * @param value The multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix. */ virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const = 0; - + /*! * Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively * @param rowIndex The index of the considered row @@ -133,12 +136,29 @@ namespace storm { * @param val2 The second multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix. */ virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const; - + + /* + * TODO + */ + void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride); + + /* + * TODO + */ + boost::optional getOptimizationDirectionOverride() const; + + /* + * TODO + */ + bool isOverridden(uint_fast64_t const index) const; + protected: mutable std::unique_ptr> cachedVector; storm::storage::SparseMatrix const& matrix; + + boost::optional optimizationDirectionOverride = boost::none; }; - + template class MultiplierFactory { public: @@ -147,6 +167,6 @@ namespace storm { std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& matrix); }; - + } } diff --git a/src/storm/storage/Decomposition.cpp b/src/storm/storage/Decomposition.cpp index efe850083..a45987d69 100644 --- a/src/storm/storage/Decomposition.cpp +++ b/src/storm/storage/Decomposition.cpp @@ -8,84 +8,84 @@ namespace storm { namespace storage { - + template Decomposition::Decomposition() : blocks() { // Intentionally left empty. } - + template Decomposition::Decomposition(Decomposition const& other) : blocks(other.blocks) { // Intentionally left empty. } - + template Decomposition& Decomposition::operator=(Decomposition const& other) { this->blocks = other.blocks; return *this; } - + template Decomposition::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) { // Intentionally left empty. } - + template Decomposition& Decomposition::operator=(Decomposition&& other) { this->blocks = std::move(other.blocks); return *this; } - + template std::size_t Decomposition::size() const { return blocks.size(); } - + template bool Decomposition::empty() const { return blocks.empty(); } - + template typename Decomposition::iterator Decomposition::begin() { return blocks.begin(); } - + template typename Decomposition::iterator Decomposition::end() { return blocks.end(); } - + template typename Decomposition::const_iterator Decomposition::begin() const { return blocks.begin(); } - + template typename Decomposition::const_iterator Decomposition::end() const { return blocks.end(); } - + template BlockType const& Decomposition::getBlock(uint_fast64_t index) const { return blocks.at(index); } - + template BlockType& Decomposition::getBlock(uint_fast64_t index) { return blocks.at(index); } - + template BlockType const& Decomposition::operator[](uint_fast64_t index) const { return blocks[index]; } - + template BlockType& Decomposition::operator[](uint_fast64_t index) { return blocks[index]; } - + template template storm::storage::SparseMatrix Decomposition::extractPartitionDependencyGraph(storm::storage::SparseMatrix const& matrix) const { @@ -97,49 +97,49 @@ namespace storm { stateToBlockMap[state] = i; } } - + // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. storm::storage::SparseMatrixBuilder dependencyGraphBuilder(this->size(), this->size()); - + for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < this->size(); ++currentBlockIndex) { // Get the next block. block_type const& block = this->getBlock(currentBlockIndex); - + // Now, we determine the blocks which are reachable (in one step) from the current block. storm::storage::FlatSet allTargetBlocks; for (auto state : block) { for (auto const& transitionEntry : matrix.getRowGroup(state)) { uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()]; - + // We only need to consider transitions that are actually leaving the SCC. if (targetBlock != currentBlockIndex) { allTargetBlocks.insert(targetBlock); } } } - + // Now we can just enumerate all the target blocks and insert the corresponding transitions. for (auto const& targetBlock : allTargetBlocks) { dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::one()); } } - + return dependencyGraphBuilder.build(); } - + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition) { - out << "["; + out << "[ "; if (decomposition.size() > 0) { for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) { - out << decomposition.blocks[blockIndex] << ", "; + out << decomposition.blocks[blockIndex] << ", " << std::endl; } out << decomposition.blocks.back(); } - out << "]"; + out << " ]"; return out; } - + template storm::storage::SparseMatrix Decomposition::extractPartitionDependencyGraph(storm::storage::SparseMatrix const& matrix) const; template storm::storage::SparseMatrix Decomposition::extractPartitionDependencyGraph(storm::storage::SparseMatrix const& matrix) const; template class Decomposition; @@ -149,7 +149,7 @@ namespace storm { template storm::storage::SparseMatrix Decomposition::extractPartitionDependencyGraph(storm::storage::SparseMatrix const& matrix) const; template class Decomposition; template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); - + template class Decomposition; template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); } // namespace storage diff --git a/src/storm/storage/GameMaximalEndComponentDecomposition.cpp b/src/storm/storage/GameMaximalEndComponentDecomposition.cpp new file mode 100644 index 000000000..f82933b6e --- /dev/null +++ b/src/storm/storage/GameMaximalEndComponentDecomposition.cpp @@ -0,0 +1,281 @@ +#include +#include +#include + +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/storage/GameMaximalEndComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" + +namespace storm { + namespace storage { + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition() : Decomposition() { + // Intentionally left empty. + } + + template + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model) { + singleMEC(model.getTransitionMatrix(), model.getBackwardTransitions()); + //performGameMaximalEndComponentDecomposition(model.getTransitionMatrix(), model.getBackwardTransitions()); + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { + singleMEC(transitionMatrix, backwardTransitions); + //performGameMaximalEndComponentDecomposition(transitionMatrix, backwardTransitions); + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states, storm::storage::BitVector const& choices) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& states) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition const& other) : Decomposition(other) { + // Intentionally left empty. + } + + template + GameMaximalEndComponentDecomposition& GameMaximalEndComponentDecomposition::operator=(GameMaximalEndComponentDecomposition const& other) { + Decomposition::operator=(other); + return *this; + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition&& other) : Decomposition(std::move(other)) { + // Intentionally left empty. + } + + template + GameMaximalEndComponentDecomposition& GameMaximalEndComponentDecomposition::operator=(GameMaximalEndComponentDecomposition&& other) { + Decomposition::operator=(std::move(other)); + return *this; + } + + template + void GameMaximalEndComponentDecomposition::performGameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states, storm::storage::BitVector const* choices) { + // Get some data for convenient access. + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + + // Initialize the maximal end component list to be the full state space. + std::list endComponentStateSets; + if (states) { + endComponentStateSets.emplace_back(states->begin(), states->end(), true); + } else { + std::vector allStates; + allStates.resize(transitionMatrix.getRowGroupCount()); + std::iota(allStates.begin(), allStates.end(), 0); + endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true); + } + storm::storage::BitVector statesToCheck(numberOfStates); + storm::storage::BitVector includedChoices; + if (choices) { + includedChoices = *choices; + } else if (states) { + includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount()); + for (auto state : *states) { + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + includedChoices.set(choice, true); + } + } + } 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, StronglyConnectedComponentDecompositionOptions().subsystem(&currMecAsBitVector).choices(&includedChoices).dropNaiveSccs()); + for(auto const& sc: sccs) { + STORM_LOG_DEBUG("SCC size: " << sc.size()); + } + + // 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. + mecChanged |= sccs.size() != 1 || (sccs.size() > 0 && sccs[0].size() < mec.size()); + + // Check for each of the SCCs whether all actions for each state do not leave the SCC. // TODO there is certainly a better way to do that... + for (auto& scc : sccs) { + statesToCheck.set(scc.begin(), scc.end()); + + while (!statesToCheck.empty()) { + storm::storage::BitVector statesToRemove(numberOfStates); + + for (auto state : statesToCheck) { + bool keepStateInMEC = true; + + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + + // If the choice is not part of our subsystem, skip it. + if (choices && !choices->get(choice)) { + continue; + } + + // If the choice is not included any more, skip it. + //if (!includedChoices.get(choice)) { + // continue; + //} + + bool choiceContainedInMEC = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (storm::utility::isZero(entry.getValue())) { + continue; + } + + if (!scc.containsState(entry.getColumn())) { + //includedChoices.set(choice, false); + choiceContainedInMEC = false; + break; + } + } + + //TODO If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. + if (!choiceContainedInMEC) { + keepStateInMEC = false; + break; + } + } + if (!keepStateInMEC) { + statesToRemove.set(state, true); + } + + } + + // Now erase the states that have no option to stay inside the MEC with all successors. + mecChanged |= !statesToRemove.empty(); + for (uint_fast64_t state : statesToRemove) { + scc.erase(state); + } + + // Now check which states should be reconsidered, because successors of them were removed. + statesToCheck.clear(); + for (auto state : statesToRemove) { + for (auto const& entry : backwardTransitions.getRow(state)) { + if (scc.containsState(entry.getColumn())) { + statesToCheck.set(entry.getColumn()); + } + } + } + } + } + + // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to + // the list instead. + if (mecChanged) { + for (StronglyConnectedComponent& scc : sccs) { + if (!scc.empty()) { + endComponentStateSets.push_back(std::move(scc)); + } + } + + std::list::const_iterator eraseIterator(mecIterator); + ++mecIterator; + endComponentStateSets.erase(eraseIterator); + } else { + // Otherwise, we proceed with the next MEC candidate. + ++mecIterator; + } + + } // End of loop over all MEC candidates. + + // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices + // contained in the MEC and store them as actual MECs. + this->blocks.reserve(endComponentStateSets.size()); + for (auto const& mecStateSet : endComponentStateSets) { + MaximalEndComponent newMec; + + for (auto state : mecStateSet) { + MaximalEndComponent::set_type containedChoices; + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + // Skip the choice if it is not part of our subsystem. + if (choices && !choices->get(choice)) { + continue; + } + + if (includedChoices.get(choice)) { + containedChoices.insert(choice); + } + } + + STORM_LOG_ASSERT(!containedChoices.empty(), "The contained choices of any state in an MEC must be non-empty."); + newMec.addState(state, std::move(containedChoices)); + } + + this->blocks.emplace_back(std::move(newMec)); + } + + STORM_LOG_DEBUG("MEC decomposition found " << this->size() << " GMEC(s)."); + } + + template + void GameMaximalEndComponentDecomposition::singleMEC(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states, storm::storage::BitVector const* choices) { + MaximalEndComponent singleMec; + + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + + std::list endComponentStateSets; + std::vector allStates; + allStates.resize(transitionMatrix.getRowGroupCount()); + std::iota(allStates.begin(), allStates.end(), 0); + endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true); + + storm::storage::BitVector includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + this->blocks.reserve(endComponentStateSets.size()); + for (auto const& mecStateSet : endComponentStateSets) { + MaximalEndComponent newMec; + + for (auto state : mecStateSet) { + MaximalEndComponent::set_type containedChoices; + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + // Skip the choice if it is not part of our subsystem. + if (choices && !choices->get(choice)) { + continue; + } + + if (includedChoices.get(choice)) { + containedChoices.insert(choice); + } + } + + STORM_LOG_ASSERT(!containedChoices.empty(), "The contained choices of any state in an MEC must be non-empty."); + newMec.addState(state, std::move(containedChoices)); + } + + this->blocks.emplace_back(std::move(newMec)); + } + + STORM_LOG_DEBUG("Whole state space is one single MEC"); + + } + + // Explicitly instantiate the MEC decomposition. + template class GameMaximalEndComponentDecomposition; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + +#ifdef STORM_HAVE_CARL + template class GameMaximalEndComponentDecomposition; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + + template class GameMaximalEndComponentDecomposition; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); +#endif + } +} diff --git a/src/storm/storage/GameMaximalEndComponentDecomposition.h b/src/storm/storage/GameMaximalEndComponentDecomposition.h new file mode 100644 index 000000000..36c590426 --- /dev/null +++ b/src/storm/storage/GameMaximalEndComponentDecomposition.h @@ -0,0 +1,109 @@ +#ifndef STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_ +#define STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_ + +#include "storm/storage/Decomposition.h" +#include "storm/storage/MaximalEndComponent.h" +#include "storm/models/sparse/NondeterministicModel.h" + +namespace storm { + namespace storage { + + /*! + * This class represents the decomposition of a stochastic multiplayer game into its (irreducible) maximal end components. + */ + template + class GameMaximalEndComponentDecomposition : public Decomposition { + public: + /* + * Creates an empty MEC decomposition. + */ + GameMaximalEndComponentDecomposition(); + + /* + * Creates an MEC decomposition of the given model. + * + * @param model The model to decompose into MECs. + */ + template > + GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + + /* + * Creates an MEC decomposition of the given model (represented by a row-grouped matrix). + * + * @param transitionMatrix The transition relation of model to decompose into MECs. + * @param backwardTransition The reversed transition relation. + */ + GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + + /* + * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix). + * + * @param transitionMatrix The transition relation of model to decompose into MECs. + * @param backwardTransition The reversed transition relation. + * @param states The states of the subsystem to decompose. + */ + GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states); + + /* + * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix). + * + * @param transitionMatrix The transition relation of model to decompose into MECs. + * @param backwardTransition The reversed transition relation. + * @param states The states of the subsystem to decompose. + * @param choices The choices of the subsystem to decompose. + */ + GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states, storm::storage::BitVector const& choices); + + /*! + * Creates an MEC decomposition of the given subsystem in the given model. + * + * @param model The model whose subsystem to decompose into MECs. + * @param states The states of the subsystem to decompose. + */ + GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& states); + + /*! + * Creates an MEC decomposition by copying the contents of the given MEC decomposition. + * + * @param other The MEC decomposition to copy. + */ + GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition const& other); + + /*! + * Assigns the contents of the given MEC decomposition to the current one by copying its contents. + * + * @param other The MEC decomposition from which to copy-assign. + */ + GameMaximalEndComponentDecomposition& operator=(GameMaximalEndComponentDecomposition const& other); + + /*! + * Creates an MEC decomposition by moving the contents of the given MEC decomposition. + * + * @param other The MEC decomposition to move. + */ + GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition&& other); + + /*! + * Assigns the contents of the given MEC decomposition to the current one by moving its contents. + * + * @param other The MEC decomposition from which to move-assign. + */ + GameMaximalEndComponentDecomposition& operator=(GameMaximalEndComponentDecomposition&& other); + + private: + /*! + * Performs the actual decomposition of the given subsystem in the given model into MECs. As a side-effect + * this stores the MECs found in the current decomposition. + * + * @param transitionMatrix The transition matrix representing the system whose subsystem to decompose into MECs. + * @param backwardTransitions The reversed transition relation. + * @param states The states of the subsystem to decompose. + * @param choices The choices of the subsystem to decompose. + */ + void performGameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr); + void singleMEC(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr); + }; + } +} + +#endif /* STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_ */ diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp index 68e8eda99..58683a3df 100644 --- a/src/storm/storage/MaximalEndComponent.cpp +++ b/src/storm/storage/MaximalEndComponent.cpp @@ -3,125 +3,125 @@ namespace storm { namespace storage { - + std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet const& block); - + MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { // Intentionally left empty. } - + MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) { // Intentionally left empty. } - + MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) { stateToChoicesMapping = other.stateToChoicesMapping; return *this; } - + MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) { // Intentionally left empty. } - + MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) { stateToChoicesMapping = std::move(other.stateToChoicesMapping); return *this; } - + void MaximalEndComponent::addState(uint_fast64_t state, set_type const& choices) { stateToChoicesMapping[state] = choices; } - + void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) { stateToChoicesMapping.emplace(state, std::move(choices)); } - + std::size_t MaximalEndComponent::size() const { return stateToChoicesMapping.size(); } - + MaximalEndComponent::set_type const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { auto stateChoicePair = stateToChoicesMapping.find(state); - + if (stateChoicePair == stateToChoicesMapping.end()) { throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC."; } - + return stateChoicePair->second; } - + MaximalEndComponent::set_type& MaximalEndComponent::getChoicesForState(uint_fast64_t state) { auto stateChoicePair = stateToChoicesMapping.find(state); - + if (stateChoicePair == stateToChoicesMapping.end()) { throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC."; } - + return stateChoicePair->second; } - + bool MaximalEndComponent::containsState(uint_fast64_t state) const { auto stateChoicePair = stateToChoicesMapping.find(state); - + if (stateChoicePair == stateToChoicesMapping.end()) { return false; } return true; } - + void MaximalEndComponent::removeState(uint_fast64_t state) { auto stateChoicePair = stateToChoicesMapping.find(state); - + if (stateChoicePair == stateToChoicesMapping.end()) { throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::removeState: cannot remove state not contained in MEC."; } - + stateToChoicesMapping.erase(stateChoicePair); } - + bool MaximalEndComponent::containsChoice(uint_fast64_t state, uint_fast64_t choice) const { auto stateChoicePair = stateToChoicesMapping.find(state); - + if (stateChoicePair == stateToChoicesMapping.end()) { throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::containsChoice: cannot obtain choices for state not contained in MEC."; } - + return stateChoicePair->second.find(choice) != stateChoicePair->second.end(); } - + MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const { set_type states; states.reserve(stateToChoicesMapping.size()); - + for (auto const& stateChoicesPair : stateToChoicesMapping) { states.insert(stateChoicesPair.first); } - + return states; } - + std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) { out << "{"; for (auto const& stateChoicesPair : component.stateToChoicesMapping) { - out << "{" << stateChoicesPair.first << ", " << stateChoicesPair.second << "}"; + out << "(" << stateChoicesPair.first << ", " << stateChoicesPair.second << ")"; } out << "}"; - + return out; } - + MaximalEndComponent::iterator MaximalEndComponent::begin() { return stateToChoicesMapping.begin(); } - + MaximalEndComponent::iterator MaximalEndComponent::end() { return stateToChoicesMapping.end(); } - + MaximalEndComponent::const_iterator MaximalEndComponent::begin() const { return stateToChoicesMapping.begin(); } - + MaximalEndComponent::const_iterator MaximalEndComponent::end() const { return stateToChoicesMapping.end(); } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 05a526702..d89f7a568 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -21,64 +21,64 @@ namespace storm { namespace storage { - + template MatrixEntry::MatrixEntry(IndexType column, ValueType value) : entry(column, value) { // Intentionally left empty. } - + template MatrixEntry::MatrixEntry(std::pair&& pair) : entry(std::move(pair)) { // Intentionally left empty. } - + template IndexType const& MatrixEntry::getColumn() const { return this->entry.first; } - + template void MatrixEntry::setColumn(IndexType const& column) { this->entry.first = column; } - + template ValueType const& MatrixEntry::getValue() const { return this->entry.second; } - + template void MatrixEntry::setValue(ValueType const& value) { this->entry.second = value; } - + template std::pair const& MatrixEntry::getColumnValuePair() const { return this->entry; } - + template MatrixEntry MatrixEntry::operator*(value_type factor) const { return MatrixEntry(this->getColumn(), this->getValue() * factor); } - - + + template bool MatrixEntry::operator==(MatrixEntry const& other) const { return this->entry.first == other.entry.first && this->entry.second == other.entry.second; } - + template bool MatrixEntry::operator!=(MatrixEntry const& other) const { return !(*this == other); } - + template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry) { out << "(" << entry.getColumn() << ", " << entry.getValue() << ")"; return out; } - + template SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroupCount(0) { // Prepare the internal storage. @@ -96,14 +96,14 @@ namespace storm { } rowIndications.push_back(0); } - + template SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), currentRowGroupCount() { - + lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1; lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); highestColumn = matrix.getColumnCount() == 0 ? 0 : matrix.getColumnCount() - 1; - + // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again. if (hasCustomRowGrouping) { rowGroupIndices = std::move(matrix.rowGroupIndices); @@ -112,19 +112,19 @@ namespace storm { } currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; } - + // Likewise, we need to 'open' the row indications again. if (!rowIndications.empty()) { rowIndications.pop_back(); } } - + template void SparseMatrixBuilder::addNextValue(index_type row, index_type column, ValueType const& value) { // Check that we did not move backwards wrt. the row. STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException, "Adding an element in row " << row << ", but an element in row " << lastRow << " has already been added."); STORM_LOG_ASSERT(columnsAndValues.size() == currentEntryCount, "Unexpected size of columnsAndValues vector."); - + // Check if a diagonal entry shall be inserted before if (pendingDiagonalEntry) { index_type diagColumn = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow; @@ -143,7 +143,7 @@ namespace storm { } } } - + // If the element is in the same row, but was not inserted in the correct order, we need to fix the row after // the insertion. bool fixCurrentRow = row == lastRow && column < lastColumn; @@ -159,26 +159,26 @@ namespace storm { rowIndications.resize(row + 1, currentEntryCount); lastRow = row; } - + lastColumn = column; - + // Finally, set the element and increase the current size. columnsAndValues.emplace_back(column, value); highestColumn = std::max(highestColumn, column); ++currentEntryCount; - + // If we need to fix the row, do so now. if (fixCurrentRow) { // First, we sort according to columns. std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }); - + // Then, we eliminate possible duplicate entries. auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { return a.getColumn() == b.getColumn(); }); - + // Finally, remove the superfluous elements. std::size_t elementsToRemove = std::distance(it, columnsAndValues.end()); if (elementsToRemove > 0) { @@ -188,7 +188,7 @@ namespace storm { } } } - + // In case we did not expect this value, we throw an exception. if (forceInitialDimensions) { STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << "."); @@ -196,12 +196,12 @@ namespace storm { STORM_LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << "."); } } - + template void SparseMatrixBuilder::newRowGroup(index_type startingRow) { STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size."); - + // If there still is a pending diagonal entry, we need to add it now (otherwise, the correct diagonal column will be unclear) if (pendingDiagonalEntry) { STORM_LOG_ASSERT(currentRowGroupCount > 0, "Diagonal entry was set before opening the first row group."); @@ -210,10 +210,10 @@ namespace storm { pendingDiagonalEntry = boost::none; // clear now, so addNextValue works properly addNextValue(lastRow, diagColumn, diagValue); } - + rowGroupIndices.get().push_back(startingRow); ++currentRowGroupCount; - + // Handle the case where the previous row group ends with one or more empty rows if (lastRow + 1 < startingRow) { // Close all rows from the most recent one to the starting row. @@ -224,10 +224,10 @@ namespace storm { lastColumn = 0; } } - + template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { - + // If there still is a pending diagonal entry, we need to add it now if (pendingDiagonalEntry) { index_type diagColumn = hasCustomRowGrouping ? currentRowGroupCount - 1 : lastRow; @@ -235,30 +235,30 @@ namespace storm { pendingDiagonalEntry = boost::none; // clear now, so addNextValue works properly addNextValue(lastRow, diagColumn, diagValue); } - + bool hasEntries = currentEntryCount != 0; - + uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0; - + // If the last row group was empty, we need to add one more to the row count, because otherwise this empty row is not counted. if (hasCustomRowGrouping) { if (lastRow < rowGroupIndices->back()) { ++rowCount; } } - + if (initialRowCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); rowCount = std::max(rowCount, initialRowCount); } - + rowCount = std::max(rowCount, overriddenRowCount); - + // If the current row count was overridden, we may need to add empty rows. for (index_type i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); } - + // We put a sentinel element at the last position of the row indices array. This eases iteration work, // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. @@ -272,12 +272,12 @@ namespace storm { columnCount = std::max(columnCount, initialColumnCount); } columnCount = std::max(columnCount, overriddenColumnCount); - + uint_fast64_t entryCount = currentEntryCount; if (initialEntryCountSet && forceInitialDimensions) { STORM_LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << "."); } - + // Check whether row groups are missing some entries. if (hasCustomRowGrouping) { uint_fast64_t rowGroupCount = currentRowGroupCount; @@ -286,15 +286,15 @@ namespace storm { rowGroupCount = std::max(rowGroupCount, initialRowGroupCount); } rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount); - + for (index_type i = currentRowGroupCount; i <= rowGroupCount; ++i) { rowGroupIndices.get().push_back(rowCount); } } - + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } - + template typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastRow() const { return lastRow; @@ -313,7 +313,7 @@ namespace storm { typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastColumn() const { return lastColumn; } - + // Debug method for printing the current matrix template void print(std::vector::index_type> const& rowGroupIndices, std::vector::index_type, typename SparseMatrix::value_type>> const& columnsAndValues, std::vector::index_type> const& rowIndications) { @@ -335,11 +335,11 @@ namespace storm { } } } - + template void SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { index_type maxColumn = 0; - + for (index_type row = 0; row < rowIndications.size(); ++row) { bool changed = false; auto startRow = std::next(columnsAndValues.begin(), rowIndications[row]); @@ -365,11 +365,11 @@ namespace storm { }), "Columns not sorted."); } } - + highestColumn = maxColumn; lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); } - + template void SparseMatrixBuilder::addDiagonalEntry(index_type row, ValueType const& value) { STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException, "Adding a diagonal element in row " << row << ", but an element in row " << lastRow << " has already been added."); @@ -399,59 +399,59 @@ namespace storm { SparseMatrix::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } - + template typename SparseMatrix::iterator SparseMatrix::rows::begin() { return beginIterator; } - + template typename SparseMatrix::iterator SparseMatrix::rows::end() { return beginIterator + entryCount; } - + template typename SparseMatrix::index_type SparseMatrix::rows::getNumberOfEntries() const { return this->entryCount; } - + template SparseMatrix::const_rows::const_rows(const_iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } - + template typename SparseMatrix::const_iterator SparseMatrix::const_rows::begin() const { return beginIterator; } - + template typename SparseMatrix::const_iterator SparseMatrix::const_rows::end() const { return beginIterator + entryCount; } - + template typename SparseMatrix::index_type SparseMatrix::const_rows::getNumberOfEntries() const { return this->entryCount; } - + template SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { // Intentionally left empty. } - + template SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } - + template SparseMatrix::SparseMatrix(SparseMatrix const& other, bool insertDiagonalElements) { storm::storage::BitVector rowConstraint(other.getRowCount(), true); storm::storage::BitVector columnConstraint(other.getColumnCount(), true); *this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements); } - + template SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix @@ -459,12 +459,12 @@ namespace storm { other.columnCount = 0; other.entryCount = 0; } - + template SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, boost::optional> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(rowGroupIndices) { this->updateNonzeroEntryCount(); } - + template SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, boost::optional>&& rowGroupIndices) : columnCount(columnCount), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { // Initialize some variables here which depend on other variables @@ -474,7 +474,7 @@ namespace storm { this->trivialRowGrouping = !this->rowGroupIndices; this->updateNonzeroEntryCount(); } - + template SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. @@ -483,7 +483,7 @@ namespace storm { columnCount = other.columnCount; entryCount = other.entryCount; nonzeroEntryCount = other.nonzeroEntryCount; - + columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; rowGroupIndices = other.rowGroupIndices; @@ -491,7 +491,7 @@ namespace storm { } return *this; } - + template SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { // Only perform assignment if source and target are not the same. @@ -500,7 +500,7 @@ namespace storm { columnCount = other.columnCount; entryCount = other.entryCount; nonzeroEntryCount = other.nonzeroEntryCount; - + columnsAndValues = std::move(other.columnsAndValues); rowIndications = std::move(other.rowIndications); rowGroupIndices = std::move(other.rowGroupIndices); @@ -508,15 +508,15 @@ namespace storm { } return *this; } - + template bool SparseMatrix::operator==(SparseMatrix const& other) const { if (this == &other) { return true; } - + bool equalityResult = true; - + equalityResult &= this->getRowCount() == other.getRowCount(); if (!equalityResult) { return false; @@ -533,7 +533,7 @@ namespace storm { if (!equalityResult) { return false; } - + // For the actual contents, we need to do a little bit more work, because we want to ignore elements that // are set to zero, please they may be represented implicitly in the other matrix. for (index_type row = 0; row < this->getRowCount(); ++row) { @@ -559,25 +559,25 @@ namespace storm { return false; } } - + return equalityResult; } - + template typename SparseMatrix::index_type SparseMatrix::getRowCount() const { return rowCount; } - + template typename SparseMatrix::index_type SparseMatrix::getColumnCount() const { return columnCount; } - + template typename SparseMatrix::index_type SparseMatrix::getEntryCount() const { return entryCount; } - + template uint_fast64_t SparseMatrix::getRowGroupEntryCount(uint_fast64_t const group) const { uint_fast64_t result = 0; @@ -590,12 +590,12 @@ namespace storm { } return result; } - + template typename SparseMatrix::index_type SparseMatrix::getNonzeroEntryCount() const { return nonzeroEntryCount; } - + template void SparseMatrix::updateNonzeroEntryCount() const { this->nonzeroEntryCount = 0; @@ -605,12 +605,12 @@ namespace storm { } } } - + template void SparseMatrix::updateNonzeroEntryCount(std::make_signed::type difference) { this->nonzeroEntryCount += difference; } - + template void SparseMatrix::updateDimensions() const { this->nonzeroEntryCount = 0; @@ -622,7 +622,7 @@ namespace storm { } } } - + template typename SparseMatrix::index_type SparseMatrix::getRowGroupCount() const { if (!this->hasTrivialRowGrouping()) { @@ -631,12 +631,12 @@ namespace storm { return rowCount; } } - + template typename SparseMatrix::index_type SparseMatrix::getRowGroupSize(index_type group) const { return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group]; } - + template typename SparseMatrix::index_type SparseMatrix::getSizeOfLargestRowGroup() const { if (this->hasTrivialRowGrouping()) { @@ -650,7 +650,7 @@ namespace storm { } return res; } - + template typename SparseMatrix::index_type SparseMatrix::getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const { if (this->hasTrivialRowGrouping()) { @@ -669,7 +669,7 @@ namespace storm { return numRows; } - + template std::vector::index_type> const& SparseMatrix::getRowGroupIndices() const { // If there is no current row grouping, we need to create it. @@ -679,7 +679,7 @@ namespace storm { } return rowGroupIndices.get(); } - + template std::vector::index_type> SparseMatrix::swapRowGroupIndices(std::vector&& newRowGrouping) { std::vector result; @@ -689,7 +689,7 @@ namespace storm { } return result; } - + template void SparseMatrix::setRowGroupIndices(std::vector const& newRowGroupIndices) { trivialRowGrouping = false; @@ -700,7 +700,7 @@ namespace storm { bool SparseMatrix::hasTrivialRowGrouping() const { return trivialRowGrouping; } - + template void SparseMatrix::makeRowGroupingTrivial() { if (trivialRowGrouping) { @@ -710,7 +710,7 @@ namespace storm { rowGroupIndices = boost::none; } } - + template storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint) const { storm::storage::BitVector res(this->getRowCount(), false); @@ -722,7 +722,7 @@ namespace storm { } return res; } - + template storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraint) const { storm::storage::BitVector result(this->getRowCount(), false); @@ -743,7 +743,7 @@ namespace storm { } return result; } - + template storm::storage::BitVector SparseMatrix::getRowGroupFilter(storm::storage::BitVector const& rowConstraint, bool setIfForAllRowsInGroup) const { STORM_LOG_ASSERT(!this->hasTrivialRowGrouping(), "Tried to get a row group filter but this matrix does not have row groups"); @@ -766,14 +766,14 @@ namespace storm { } return result; } - + template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { for (auto row : rows) { makeRowDirac(row, row); } } - + template void SparseMatrix::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) { if (!this->hasTrivialRowGrouping()) { @@ -788,19 +788,19 @@ namespace storm { } } } - + template void SparseMatrix::makeRowDirac(index_type row, index_type column) { iterator columnValuePtr = this->begin(row); iterator columnValuePtrEnd = this->end(row); - + // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements // in the vector of nonzeros otherwise. if (columnValuePtr >= columnValuePtrEnd) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, because there is no entry in this row."; } iterator lastColumnValuePtr = this->end(row) - 1; - + // If there is at least one entry in this row, we can set it to one, modify its column value to the // one given by the parameter and set all subsequent elements of this row to zero. // However, we want to preserve that column indices within a row are ascending, so we pick an entry that is close to the desired column index @@ -824,7 +824,7 @@ namespace storm { columnValuePtr->setValue(storm::utility::zero()); } } - + template bool SparseMatrix::compareRows(index_type i1, index_type i2) const { const_iterator end1 = this->end(i1); @@ -841,7 +841,7 @@ namespace storm { } return false; } - + template BitVector SparseMatrix::duplicateRowsInRowgroups() const { BitVector bv(this->getRowCount()); @@ -856,31 +856,31 @@ namespace storm { } return bv; } - + template void SparseMatrix::swapRows(index_type const& row1, index_type const& row2) { if (row1 == row2) { return; } - + // Get the index of the row that has more / less entries than the other. index_type largerRow = getRow(row1).getNumberOfEntries() > getRow(row2).getNumberOfEntries() ? row1 : row2; index_type smallerRow = largerRow == row1 ? row2 : row1; index_type rowSizeDifference = getRow(largerRow).getNumberOfEntries() - getRow(smallerRow).getNumberOfEntries(); - + // Save contents of larger row. auto copyRow = getRow(largerRow); std::vector> largerRowContents(copyRow.begin(), copyRow.end()); - + if (largerRow < smallerRow) { auto writeIt = getRows(largerRow, smallerRow + 1).begin(); - + // Write smaller row to its new position. for (auto& smallerRowEntry : getRow(smallerRow)) { *writeIt = std::move(smallerRowEntry); ++writeIt; } - + // Write the intermediate rows into their correct position. if (!storm::utility::isZero(rowSizeDifference)) { for (auto& intermediateRowEntry : getRows(largerRow + 1, smallerRow)) { @@ -891,15 +891,15 @@ namespace storm { // skip the intermediate rows writeIt = getRow(smallerRow).begin(); } - + // Write the larger row to its new position. for (auto& largerRowEntry : largerRowContents) { *writeIt = std::move(largerRowEntry); ++writeIt; } - + STORM_LOG_ASSERT(writeIt == getRow(smallerRow).end(), "Unexpected position of write iterator."); - + // Update the row indications to account for the shift of indices at where the rows now start. if (!storm::utility::isZero(rowSizeDifference)) { for (index_type row = largerRow + 1; row <= smallerRow; ++row) { @@ -908,14 +908,14 @@ namespace storm { } } else { auto writeIt = getRows(smallerRow, largerRow + 1).end() - 1; - + // Write smaller row to its new position auto copyRow = getRow(smallerRow); for (auto smallerRowEntryIt = copyRow.end() - 1; smallerRowEntryIt != copyRow.begin() - 1; --smallerRowEntryIt) { *writeIt = std::move(*smallerRowEntryIt); --writeIt; } - + // Write the intermediate rows into their correct position. if (!storm::utility::isZero(rowSizeDifference)) { for (auto intermediateRowEntryIt = getRows(smallerRow + 1, largerRow).end() - 1; intermediateRowEntryIt != getRows(smallerRow + 1, largerRow).begin() - 1; --intermediateRowEntryIt) { @@ -926,15 +926,15 @@ namespace storm { // skip the intermediate rows writeIt = getRow(smallerRow).end() - 1; } - + // Write the larger row to its new position. for (auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) { *writeIt = std::move(*largerRowEntryIt); --writeIt; } - + STORM_LOG_ASSERT(writeIt == getRow(smallerRow).begin() - 1, "Unexpected position of write iterator."); - + // Update row indications. // Update the row indications to account for the shift of indices at where the rows now start. if (!storm::utility::isZero(rowSizeDifference)) { @@ -944,11 +944,11 @@ namespace storm { } } } - + template std::vector SparseMatrix::getRowSumVector() const { std::vector result(this->getRowCount()); - + index_type row = 0; for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++row) { *resultIt = getRowSum(row); @@ -956,7 +956,7 @@ namespace storm { return result; } - + template ValueType SparseMatrix::getConstrainedRowSum(index_type row, storm::storage::BitVector const& constraint) const { ValueType result = storm::utility::zero(); @@ -967,7 +967,7 @@ namespace storm { } return result; } - + template std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const { std::vector result(rowConstraint.getNumberOfSetBits()); @@ -977,7 +977,7 @@ namespace storm { } return result; } - + template std::vector SparseMatrix::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const { std::vector result; @@ -995,7 +995,7 @@ namespace storm { } return result; } - + template SparseMatrix SparseMatrix::getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalElements, storm::storage::BitVector const& makeZeroColumns) const { if (useGroups) { @@ -1008,14 +1008,14 @@ namespace storm { *it = i; } auto res = getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements, makeZeroColumns); - + // Create a new row grouping that reflects the new sizes of the row groups if the current matrix has a // non trivial row-grouping. if (!this->hasTrivialRowGrouping()) { std::vector newRowGroupIndices; newRowGroupIndices.push_back(0); auto selectedRowIt = rowConstraint.begin(); - + // For this, we need to count how many rows were preserved in every group. for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { uint_fast64_t newRowCount = 0; @@ -1027,20 +1027,20 @@ namespace storm { newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount); } } - + res.trivialRowGrouping = false; res.rowGroupIndices = newRowGroupIndices; } - + return res; } } - + template SparseMatrix SparseMatrix::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries, storm::storage::BitVector const& makeZeroColumns) const { STORM_LOG_THROW(!rowGroupConstraint.empty() && !columnConstraint.empty(), storm::exceptions::InvalidArgumentException, "Cannot build empty submatrix."); uint_fast64_t submatrixColumnCount = columnConstraint.getNumberOfSetBits(); - + // Start by creating a temporary vector that stores for each index whose bit is set to true the number of // bits that were set before that particular index. std::vector columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices(); @@ -1049,7 +1049,7 @@ namespace storm { tmp = std::make_unique>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); } std::vector const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex; - + // Then, we need to determine the number of entries and the number of rows of the submatrix. index_type subEntries = 0; index_type subRows = 0; @@ -1058,17 +1058,17 @@ namespace storm { subRows += rowGroupIndices[index + 1] - rowGroupIndices[index]; for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { bool foundDiagonalElement = false; - + for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { if (columnConstraint.get(it->getColumn()) && (makeZeroColumns.size() == 0 || !makeZeroColumns.get(it->getColumn())) ) { ++subEntries; - + if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { foundDiagonalElement = true; } } } - + // If requested, we need to reserve one entry more for inserting the diagonal zero entry. if (insertDiagonalEntries && !foundDiagonalElement && rowGroupCount < submatrixColumnCount) { ++subEntries; @@ -1076,10 +1076,10 @@ namespace storm { } ++rowGroupCount; } - + // Create and initialize resulting matrix. SparseMatrixBuilder matrixBuilder(subRows, submatrixColumnCount, subEntries, true, !this->hasTrivialRowGrouping()); - + // Copy over selected entries. rowGroupCount = 0; index_type rowCount = 0; @@ -1090,7 +1090,7 @@ namespace storm { } for (index_type i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { bool insertedDiagonalElement = false; - + for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { if (columnConstraint.get(it->getColumn()) && (makeZeroColumns.size() == 0 || !makeZeroColumns.get(it->getColumn()))) { if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { @@ -1110,20 +1110,20 @@ namespace storm { } ++rowGroupCount; } - + return matrixBuilder.build(); } - + template SparseMatrix SparseMatrix::restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups) const { STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch."); - + // Count the number of entries of the resulting matrix uint_fast64_t entryCount = 0; for (auto const& row : rowsToKeep) { entryCount += this->getRow(row).getNumberOfEntries(); } - + // Get the smallest row group index such that all row groups with at least this index are empty. uint_fast64_t firstTrailingEmptyRowGroup = this->getRowGroupCount(); for (auto groupIndexIt = this->getRowGroupIndices().rbegin() + 1; groupIndexIt != this->getRowGroupIndices().rend(); ++groupIndexIt) { @@ -1133,7 +1133,7 @@ namespace storm { --firstTrailingEmptyRowGroup; } STORM_LOG_THROW(allowEmptyRowGroups || firstTrailingEmptyRowGroup == this->getRowGroupCount(), storm::exceptions::InvalidArgumentException, "Empty rows are not allowed, but row group " << firstTrailingEmptyRowGroup << " is empty."); - + // build the matrix. The row grouping will always be considered as nontrivial. SparseMatrixBuilder builder(rowsToKeep.getNumberOfSetBits(), this->getColumnCount(), entryCount, true, true, this->getRowGroupCount()); uint_fast64_t newRow = 0; @@ -1150,12 +1150,12 @@ namespace storm { } STORM_LOG_THROW(allowEmptyRowGroups || !rowGroupEmpty, storm::exceptions::InvalidArgumentException, "Empty rows are not allowed, but row group " << rowGroup << " is empty."); } - + // The all remaining row groups will be empty. Note that it is not allowed to call builder.addNewGroup(...) if there are no more rows afterwards. SparseMatrix res = builder.build(); return res; } - + template SparseMatrix SparseMatrix::filterEntries(storm::storage::BitVector const& rowFilter) const { // Count the number of entries in the resulting matrix. @@ -1163,7 +1163,7 @@ namespace storm { for (auto const& row : rowFilter) { entryCount += getRow(row).getNumberOfEntries(); } - + // Build the resulting matrix. SparseMatrixBuilder builder(getRowCount(), getColumnCount(), entryCount); for (auto const& row : rowFilter) { @@ -1172,14 +1172,14 @@ namespace storm { } } SparseMatrix result = builder.build(); - + // Add a row grouping if necessary. if (!hasTrivialRowGrouping()) { result.setRowGroupIndices(getRowGroupIndices()); } return result; } - + template void SparseMatrix::dropZeroEntries() { updateNonzeroEntryCount(); @@ -1200,7 +1200,7 @@ namespace storm { *this = std::move(result); } } - + template SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for @@ -1209,7 +1209,7 @@ namespace storm { for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; - + // Iterate through that row and count the number of slots we have to reserve for copying. bool foundDiagonalElement = false; for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) { @@ -1222,15 +1222,15 @@ namespace storm { ++subEntries; } } - + // Now create the matrix to be returned with the appropriate size. SparseMatrixBuilder matrixBuilder(rowGroupIndices.get().size() - 1, columnCount, subEntries); - + // Copy over the selected lines from the source matrix. for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; - + // Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if // there is no entry yet. bool insertedDiagonalElement = false; @@ -1247,7 +1247,7 @@ namespace storm { matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero()); } } - + // Finalize created matrix and return result. return matrixBuilder.build(); } @@ -1317,7 +1317,7 @@ namespace storm { } return result; } - + template SparseMatrix SparseMatrix::transpose(bool joinGroups, bool keepZeros) const { index_type rowCount = this->getColumnCount(); @@ -1329,10 +1329,10 @@ namespace storm { this->updateNonzeroEntryCount(); entryCount = this->getNonzeroEntryCount(); } - + std::vector rowIndications(rowCount + 1); std::vector> columnsAndValues(entryCount); - + // First, we need to count how many entries each column has. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { @@ -1341,17 +1341,17 @@ namespace storm { } } } - + // Now compute the accumulated offsets. for (index_type i = 1; i < rowCount + 1; ++i) { rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; } - + // Create an array that stores the index for the next value to be added for // each row in the transposed matrix. Initially this corresponds to the previously // computed accumulated offsets. std::vector nextIndices = rowIndications; - + // Now we are ready to actually fill in the values of the transposed matrix. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { @@ -1361,17 +1361,17 @@ namespace storm { } } } - + storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), boost::none); - + return transposedMatrix; } - + template SparseMatrix SparseMatrix::transposeSelectedRowsFromRowGroups(std::vector const& rowGroupChoices, bool keepZeros) const { index_type rowCount = this->getColumnCount(); index_type columnCount = this->getRowGroupCount(); - + // Get the overall entry count as well as the number of entries of each column index_type entryCount = 0; std::vector rowIndications(columnCount + 1); @@ -1384,19 +1384,19 @@ namespace storm { } } } - + // Now compute the accumulated offsets. for (index_type i = 1; i < rowCount + 1; ++i) { rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; } - + std::vector> columnsAndValues(entryCount); - + // Create an array that stores the index for the next value to be added for // each row in the transposed matrix. Initially this corresponds to the previously // computed accumulated offsets. std::vector nextIndices = rowIndications; - + // Now we are ready to actually fill in the values of the transposed matrix. rowGroupChoiceIt = rowGroupChoices.begin(); for (index_type rowGroup = 0; rowGroup < columnCount; ++rowGroup, ++rowGroupChoiceIt) { @@ -1407,16 +1407,16 @@ namespace storm { } } } - + return storm::storage::SparseMatrix(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none); } - + template void SparseMatrix::convertToEquationSystem() { invertDiagonal(); negateAllNonDiagonalEntries(); } - + template void SparseMatrix::invertDiagonal() { // Now iterate over all row groups and set the diagonal elements to the inverted value. @@ -1439,14 +1439,14 @@ namespace storm { foundDiagonalElement = true; } } - + // Throw an exception if a row did not have an element on the diagonal. if (!foundDiagonalElement) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is missing diagonal entries."; } } } - + template void SparseMatrix::negateAllNonDiagonalEntries() { // Iterate over all row groups and negate all the elements that are not on the diagonal. @@ -1458,7 +1458,7 @@ namespace storm { } } } - + template void SparseMatrix::deleteDiagonalEntries() { // Iterate over all rows and negate all the elements that are not on the diagonal. @@ -1471,15 +1471,15 @@ namespace storm { } } } - + template typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(this->getRowCount() == this->getColumnCount(), storm::exceptions::InvalidArgumentException, "Canno compute Jacobi decomposition of non-square matrix."); - + // Prepare the resulting data structures. SparseMatrixBuilder luBuilder(this->getRowCount(), this->getColumnCount()); std::vector invertedDiagonal(rowCount); - + // Copy entries to the appropriate matrices. for (index_type rowNumber = 0; rowNumber < rowCount; ++rowNumber) { for (const_iterator it = this->begin(rowNumber), ite = this->end(rowNumber); it != ite; ++it) { @@ -1490,22 +1490,22 @@ namespace storm { } } } - + return std::make_pair(luBuilder.build(), std::move(invertedDiagonal)); } - + #ifdef STORM_HAVE_CARL template<> typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } - + template<> typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } #endif - + template template ResultValueType SparseMatrix::getPointwiseProductRowSum(storm::storage::SparseMatrix const& otherMatrix, index_type const& row) const { @@ -1513,7 +1513,7 @@ namespace storm { typename storm::storage::SparseMatrix::const_iterator ite1 = this->end(row); typename storm::storage::SparseMatrix::const_iterator it2 = otherMatrix.begin(row); typename storm::storage::SparseMatrix::const_iterator ite2 = otherMatrix.end(row); - + ResultValueType result = storm::utility::zero(); for (;it1 != ite1 && it2 != ite2; ++it1) { if (it1->getColumn() < it2->getColumn()) { @@ -1529,7 +1529,7 @@ namespace storm { } return result; } - + template template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { @@ -1540,7 +1540,7 @@ namespace storm { } return result; } - + template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result, std::vector const* summand) const { // If the vector and the result are aliases and this is not set to be allowed, we need and temporary vector. @@ -1553,14 +1553,14 @@ namespace storm { } else { target = &result; } - + this->multiplyWithVectorForward(vector, *target, summand); - + if (target == &temporary) { std::swap(result, *target); } } - + template void SparseMatrix::multiplyWithVectorForward(std::vector const& vector, std::vector& result, std::vector const* summand) const { const_iterator it = this->begin(); @@ -1572,7 +1572,7 @@ namespace storm { if (summand) { summandIterator = summand->begin(); } - + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator, ++summandIterator) { ValueType newValue; if (summand) { @@ -1580,15 +1580,15 @@ namespace storm { } else { newValue = storm::utility::zero(); } - + for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { newValue += it->getValue() * vector[it->getColumn()]; } - + *resultIterator = newValue; } } - + template void SparseMatrix::multiplyWithVectorBackward(std::vector const& vector, std::vector& result, std::vector const* summand) const { const_iterator it = this->end() - 1; @@ -1600,7 +1600,7 @@ namespace storm { if (summand) { summandIterator = summand->end() - 1; } - + for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --summandIterator) { ValueType newValue; if (summand) { @@ -1608,15 +1608,15 @@ namespace storm { } else { newValue = storm::utility::zero(); } - + for (ite = this->begin() + *rowIterator - 1; it != ite; --it) { newValue += (it->getValue() * vector[it->getColumn()]); } - + *resultIterator = newValue; } } - + #ifdef STORM_HAVE_INTELTBB template class TbbMultAddFunctor { @@ -1624,11 +1624,11 @@ namespace storm { typedef typename storm::storage::SparseMatrix::index_type index_type; typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - + TbbMultAddFunctor(std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand) : columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand) { // Intentionally left empty. } - + void operator()(tbb::blocked_range const& range) const { index_type startRow = range.begin(); index_type endRow = range.end(); @@ -1641,18 +1641,18 @@ namespace storm { if (summand) { summandIterator = summand->begin() + startRow; } - + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator, ++summandIterator) { ValueType newValue = summand ? *summandIterator : storm::utility::zero(); - + for (ite = columnsAndEntries.begin() + *(rowIterator + 1); it != ite; ++it) { newValue += it->getValue() * x[it->getColumn()]; } - + *resultIterator = newValue; } } - + private: std::vector> const& columnsAndEntries; std::vector const& rowIndications; @@ -1660,7 +1660,7 @@ namespace storm { std::vector& result; std::vector const* summand; }; - + template void SparseMatrix::multiplyWithVectorParallel(std::vector const& vector, std::vector& result, std::vector const* summand) const { if (&vector == &result) { @@ -1673,7 +1673,7 @@ namespace storm { } } #endif - + template ValueType SparseMatrix::multiplyRowWithVector(index_type row, std::vector const& vector) const { ValueType result = storm::utility::zero(); @@ -1683,7 +1683,7 @@ namespace storm { } return result; } - + template void SparseMatrix::performSuccessiveOverRelaxationStep(ValueType omega, std::vector& x, std::vector const& b) const { const_iterator it = this->end() - 1; @@ -1692,13 +1692,13 @@ namespace storm { typename std::vector::const_iterator bIt = b.end() - 1; typename std::vector::iterator resultIterator = x.end() - 1; typename std::vector::iterator resultIteratorEnd = x.begin() - 1; - + index_type currentRow = getRowCount(); for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --bIt) { --currentRow; ValueType tmpValue = storm::utility::zero(); ValueType diagonalElement = storm::utility::zero(); - + for (ite = this->begin() + *rowIterator - 1; it != ite; --it) { if (it->getColumn() != currentRow) { tmpValue += it->getValue() * x[it->getColumn()]; @@ -1710,14 +1710,14 @@ namespace storm { *resultIterator = ((storm::utility::one() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue); } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::performSuccessiveOverRelaxationStep(Interval, std::vector&, std::vector const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif - + template void SparseMatrix::performWalkerChaeStep(std::vector const& x, std::vector const& columnSums, std::vector const& b, std::vector const& ax, std::vector& result) const { const_iterator it = this->begin(); @@ -1735,7 +1735,7 @@ namespace storm { result[it->getColumn()] += it->getValue() * (b[row] / ax[row]); } } - + auto xIterator = x.begin(); auto sumsIterator = columnSums.begin(); for (auto& entry : result) { @@ -1751,7 +1751,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif - + template void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { if (dir == OptimizationDirection::Minimize) { @@ -1776,36 +1776,36 @@ namespace storm { if (choices) { choiceIt = choices->begin(); } - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; - + uint64_t currentRow = 0; for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if there is at least one row in the group. if (*rowGroupIt < *(rowGroupIt + 1)) { if (summand) { currentValue = *summandIt; ++summandIt; } - + for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } - + if (choices) { selectedChoice = 0; if (*choiceIt == 0) { oldSelectedChoiceValue = currentValue; } } - + ++rowIt; ++currentRow; - + for (; currentRow < *(rowGroupIt + 1); ++rowIt, ++currentRow) { ValueType newValue = summand ? *summandIt : storm::utility::zero(); for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { @@ -1815,7 +1815,7 @@ namespace storm { if (choices && currentRow == *choiceIt + *rowGroupIt) { oldSelectedChoiceValue = newValue; } - + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { @@ -1826,7 +1826,7 @@ namespace storm { ++summandIt; } } - + // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { @@ -1835,14 +1835,14 @@ namespace storm { } } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif - + template void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { if (dir == storm::OptimizationDirection::Minimize) { @@ -1851,7 +1851,7 @@ namespace storm { multiplyAndReduceBackward>(rowGroupIndices, vector, summand, result, choices); } } - + template template void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { @@ -1867,22 +1867,22 @@ namespace storm { if (choices) { choiceIt = choices->end() - 1; } - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; - + uint64_t currentRow = this->getRowCount() - 1; for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if there is at least one row in the group. if (*rowGroupIt < *(rowGroupIt + 1)) { if (summand) { currentValue = *summandIt; --summandIt; } - + for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } @@ -1894,17 +1894,17 @@ namespace storm { } --rowIt; --currentRow; - + for (uint64_t i = *rowGroupIt + 1, end = *(rowGroupIt + 1); i < end; --rowIt, --currentRow, ++i, --summandIt) { ValueType newValue = summand ? *summandIt : storm::utility::zero(); for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) { newValue += elementIt->getValue() * vector[elementIt->getColumn()]; } - + if (choices && currentRow == *choiceIt + *rowGroupIt) { oldSelectedChoiceValue = newValue; } - + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { @@ -1912,7 +1912,7 @@ namespace storm { } } } - + // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { @@ -1921,14 +1921,14 @@ namespace storm { } } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif - + #ifdef STORM_HAVE_INTELTBB template class TbbMultAddReduceFunctor { @@ -1936,16 +1936,16 @@ namespace storm { typedef typename storm::storage::SparseMatrix::index_type index_type; typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices) { // Intentionally left empty. } - + void operator()(tbb::blocked_range const& range) const { auto groupIt = rowGroupIndices.begin() + range.begin(); auto groupIte = rowGroupIndices.begin() + range.end(); - + auto rowIt = rowIndications.begin() + *groupIt; auto elementIt = columnsAndEntries.begin() + *rowIt; typename std::vector::const_iterator summandIt; @@ -1956,9 +1956,9 @@ namespace storm { if (choices) { choiceIt = choices->begin() + range.begin(); } - + auto resultIt = result.begin() + range.begin(); - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; @@ -1966,7 +1966,7 @@ namespace storm { uint64_t currentRow = *groupIt; for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if there is at least one row in the group. if (*groupIt < *(groupIt + 1)) { if (summand) { @@ -1977,23 +1977,23 @@ namespace storm { for (auto elementIte = columnsAndEntries.begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { currentValue += elementIt->getValue() * x[elementIt->getColumn()]; } - + if (choices) { selectedChoice = 0; if (*choiceIt == 0) { oldSelectedChoiceValue = currentValue; } } - + ++rowIt; ++currentRow; - + for (; currentRow < *(groupIt + 1); ++rowIt, ++currentRow, ++summandIt) { ValueType newValue = summand ? *summandIt : storm::utility::zero(); for (auto elementIte = columnsAndEntries.begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { newValue += elementIt->getValue() * x[elementIt->getColumn()]; } - + if (choices && currentRow == *choiceIt + *groupIt) { oldSelectedChoiceValue = newValue; } @@ -2005,7 +2005,7 @@ namespace storm { } } } - + // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { @@ -2014,7 +2014,7 @@ namespace storm { } } } - + private: Compare compare; std::vector const& rowGroupIndices; @@ -2025,7 +2025,7 @@ namespace storm { std::vector const* summand; std::vector* choices; }; - + template void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { if (dir == storm::OptimizationDirection::Minimize) { @@ -2034,7 +2034,7 @@ namespace storm { tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { @@ -2042,10 +2042,10 @@ namespace storm { } #endif #endif - + template void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - + // If the vector and the result are aliases, we need and temporary vector. std::vector* target; std::vector temporary; @@ -2056,21 +2056,21 @@ namespace storm { } else { target = &result; } - + this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices); if (target == &temporary) { std::swap(temporary, result); } } - + template void SparseMatrix::multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const { const_iterator it = this->begin(); const_iterator ite; std::vector::const_iterator rowIterator = rowIndications.begin(); std::vector::const_iterator rowIteratorEnd = rowIndications.end(); - + uint_fast64_t currentRow = 0; for (; rowIterator != rowIteratorEnd - 1; ++rowIterator) { for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { @@ -2079,7 +2079,7 @@ namespace storm { ++currentRow; } } - + template void SparseMatrix::scaleRowsInPlace(std::vector const& factors) { STORM_LOG_ASSERT(factors.size() == this->getRowCount(), "Can not scale rows: Number of rows and number of scaling factors do not match."); @@ -2091,7 +2091,7 @@ namespace storm { ++row; } } - + template void SparseMatrix::divideRowsInPlace(std::vector const& divisors) { STORM_LOG_ASSERT(divisors.size() == this->getRowCount(), "Can not divide rows: Number of rows and number of divisors do not match."); @@ -2104,34 +2104,34 @@ namespace storm { ++row; } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::divideRowsInPlace(std::vector const&) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } #endif - + template typename SparseMatrix::const_rows SparseMatrix::getRows(index_type startRow, index_type endRow) const { return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]); } - + template typename SparseMatrix::rows SparseMatrix::getRows(index_type startRow, index_type endRow) { return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]); } - + template typename SparseMatrix::const_rows SparseMatrix::getRow(index_type row) const { return getRows(row, row + 1); } - + template typename SparseMatrix::rows SparseMatrix::getRow(index_type row) { return getRows(row, row + 1); } - + template typename SparseMatrix::const_rows SparseMatrix::getRow(index_type rowGroup, index_type offset) const { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); @@ -2142,7 +2142,7 @@ namespace storm { return getRow(this->getRowGroupIndices()[rowGroup] + offset); } } - + template typename SparseMatrix::rows SparseMatrix::getRow(index_type rowGroup, index_type offset) { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); @@ -2154,8 +2154,8 @@ namespace storm { return getRow(rowGroup + offset); } } - - + + template typename SparseMatrix::const_rows SparseMatrix::getRowGroup(index_type rowGroup) const { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); @@ -2165,7 +2165,7 @@ namespace storm { return getRows(rowGroup, rowGroup + 1); } } - + template typename SparseMatrix::rows SparseMatrix::getRowGroup(index_type rowGroup) { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); @@ -2175,32 +2175,32 @@ namespace storm { return getRows(rowGroup, rowGroup + 1); } } - + template typename SparseMatrix::const_iterator SparseMatrix::begin(index_type row) const { return this->columnsAndValues.begin() + this->rowIndications[row]; } - + template typename SparseMatrix::iterator SparseMatrix::begin(index_type row) { return this->columnsAndValues.begin() + this->rowIndications[row]; } - + template typename SparseMatrix::const_iterator SparseMatrix::end(index_type row) const { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } - + template typename SparseMatrix::iterator SparseMatrix::end(index_type row) { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } - + template typename SparseMatrix::const_iterator SparseMatrix::end() const { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } - + template typename SparseMatrix::iterator SparseMatrix::end() { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; @@ -2214,7 +2214,7 @@ namespace storm { } return sum; } - + template typename SparseMatrix::index_type SparseMatrix::getNonconstantEntryCount() const { index_type nonConstEntries = 0; @@ -2225,7 +2225,7 @@ namespace storm { } return nonConstEntries; } - + template typename SparseMatrix::index_type SparseMatrix::getNonconstantRowGroupCount() const { index_type nonConstRowGroups = 0; @@ -2239,7 +2239,7 @@ namespace storm { } return nonConstRowGroups; } - + template bool SparseMatrix::isProbabilistic() const { storm::utility::ConstantsComparator comparator; @@ -2258,7 +2258,7 @@ namespace storm { } return true; } - + template template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { @@ -2269,7 +2269,7 @@ namespace storm { if (!this->hasTrivialRowGrouping() && matrix.hasTrivialRowGrouping()) return false; if (!this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping() && this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; - + // Check the subset property for all rows individually. for (index_type row = 0; row < this->getRowCount(); ++row) { auto it2 = matrix.begin(row); @@ -2286,7 +2286,7 @@ namespace storm { } return true; } - + template bool SparseMatrix::isIdentityMatrix() const { if (this->getRowCount() != this->getColumnCount()) { @@ -2326,7 +2326,7 @@ namespace storm { return result; } - + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. @@ -2335,22 +2335,22 @@ namespace storm { out << i << "\t"; } out << std::endl; - + // Iterate over all row groups. for (typename SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; typename SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; typename SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; - + for (typename SparseMatrix::index_type i = start; i < end; ++i) { typename SparseMatrix::index_type nextIndex = matrix.rowIndications[i]; - + // Print the actual row. out << i << "\t(\t"; typename SparseMatrix::index_type currentRealIndex = 0; while (currentRealIndex < matrix.columnCount) { if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) { - out << matrix.columnsAndValues[nextIndex].getValue() << "\t"; + out << std::setprecision(3) << matrix.columnsAndValues[nextIndex].getValue() << "\t"; ++nextIndex; } else { out << "0\t"; @@ -2360,17 +2360,17 @@ namespace storm { out << "\t)\t" << i << std::endl; } } - + // Print column numbers in footer. out << "\t\t"; for (typename SparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; - + return out; } - + template void SparseMatrix::printAsMatlabMatrix(std::ostream& out) const { // Iterate over all row groups. @@ -2378,7 +2378,7 @@ namespace storm { STORM_LOG_ASSERT(this->getRowGroupSize(group) == 1, "Incorrect row group size."); for (typename SparseMatrix::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) { typename SparseMatrix::index_type nextIndex = this->rowIndications[i]; - + // Print the actual row. out << i << "\t("; typename SparseMatrix::index_type currentRealIndex = 0; @@ -2395,11 +2395,11 @@ namespace storm { } } } - + template std::size_t SparseMatrix::hash() const { std::size_t result = 0; - + boost::hash_combine(result, this->getRowCount()); boost::hash_combine(result, this->getColumnCount()); boost::hash_combine(result, this->getEntryCount()); @@ -2408,11 +2408,11 @@ namespace storm { if (!this->hasTrivialRowGrouping()) { boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end())); } - + return result; } - - + + #ifdef STORM_HAVE_CARL std::set getVariables(SparseMatrix const& matrix) { @@ -2422,9 +2422,9 @@ namespace storm { } return result; } - + #endif - + // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; @@ -2435,10 +2435,10 @@ namespace storm { template double SparseMatrix::getPointwiseProductRowSum(storm::storage::SparseMatrix const& otherMatrix, typename SparseMatrix::index_type const& row) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + template class MatrixEntry; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); - + // float template class MatrixEntry::index_type, float>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, float> const& entry); @@ -2448,7 +2448,7 @@ namespace storm { template float SparseMatrix::getPointwiseProductRowSum(storm::storage::SparseMatrix const& otherMatrix, typename SparseMatrix::index_type const& row) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + // int template class MatrixEntry::index_type, int>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, int> const& entry); @@ -2456,7 +2456,7 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + // state_type template class MatrixEntry::index_type, storm::storage::sparse::state_type>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, storm::storage::sparse::state_type> const& entry); @@ -2464,10 +2464,10 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + #ifdef STORM_HAVE_CARL // Rational Numbers - + #if defined(STORM_HAVE_CLN) template class MatrixEntry::index_type, ClnRationalNumber>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); @@ -2478,7 +2478,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #endif - + #if defined(STORM_HAVE_GMP) template class MatrixEntry::index_type, GmpRationalNumber>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); @@ -2489,7 +2489,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #endif - + // Rational Function template class MatrixEntry::index_type, RationalFunction>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); @@ -2505,7 +2505,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + // Intervals template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template class MatrixEntry::index_type, Interval>; @@ -2515,13 +2515,10 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #endif - - - } // namespace storage -} // namespace storm - + } // namespace storage +} // namespace storm diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index ee2487002..586c81051 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -44,7 +44,7 @@ namespace storm { ExportJsonType res = std::move(*boost::any_cast(&tmp)); return res; } - + ExportJsonType buildExpression(storm::expressions::Expression const& exp, std::vector const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set const& auxiliaryVariables = {}) { STORM_LOG_TRACE("Exporting " << exp); return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables); @@ -53,14 +53,14 @@ namespace storm { class CompositionJsonExporter : public CompositionVisitor { public: CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){ - + } - + static ExportJsonType translate(storm::jani::Composition const& comp, bool allowRecursion = true) { CompositionJsonExporter visitor(allowRecursion); return anyToJson(comp.accept(visitor, boost::none)); } - + virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) { ExportJsonType compDecl; ExportJsonType autDecl; @@ -70,10 +70,10 @@ namespace storm { compDecl["elements"] = elements; return compDecl; } - + virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) { ExportJsonType compDecl; - + std::vector elems; for (auto const& subcomp : composition.getSubcompositions()) { ExportJsonType elemDecl; @@ -103,14 +103,14 @@ namespace storm { if (!synElems.empty()) { compDecl["syncs"] = synElems; } - + return compDecl; } - + private: bool allowRecursion; }; - + std::string comparisonTypeToJani(storm::logic::ComparisonType ct) { switch(ct) { case storm::logic::ComparisonType::Less: @@ -124,12 +124,12 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); } - + ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional const& lower, boost::optional const& lowerExclusive, boost::optional const& upper, boost::optional const& upperExclusive) const { STORM_LOG_THROW((lower.is_initialized() || upper.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval needs either a lower or an upper bound, but none was given."); STORM_LOG_THROW((lower.is_initialized() || !lowerExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the lower bound is exclusive but no lower bound is given."); STORM_LOG_THROW((upper.is_initialized() || !upperExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the upper bound is exclusive but no upper bound is given."); - + ExportJsonType iDecl; if (lower) { iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables()); @@ -145,17 +145,17 @@ namespace storm { } return iDecl; } - + ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const { storm::jani::RewardModelInformation info(model, rewardModelName); - + bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards()); bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && info.hasStateRewards(); bool exit = rewardAccumulation.isExitSet() && info.hasStateRewards(); - + return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); } - + ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const { std::vector res; if (rewardAccumulation.isStepsSet()) { @@ -178,7 +178,7 @@ namespace storm { return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName); } } - + ExportJsonType FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { FormulaToJaniJson translator(model); auto result = anyToJson(formula.accept(translator)); @@ -187,15 +187,15 @@ namespace storm { } return result; } - + bool FormulaToJaniJson::containsStateExitRewards() const { return stateExitRewards; } - + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const { return buildExpression(f.getExpression(), model.getConstants(), model.getGlobalVariables()); } - + boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const { ExportJsonType opDecl(f.getLabel()); return opDecl; @@ -218,10 +218,10 @@ namespace storm { opDecl["op"] = "U"; opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data)); opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); - + bool hasStepBounds(false), hasTimeBounds(false); std::vector rewardBounds; - + for (uint64_t i = 0; i < f.getDimension(); ++i) { boost::optional lower, upper; boost::optional lowerExclusive, upperExclusive; @@ -234,7 +234,7 @@ namespace storm { upperExclusive = f.isUpperBoundStrict(i); } ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive); - + auto tbr = f.getTimeBoundReference(i); if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { STORM_LOG_THROW(!hasStepBounds, storm::exceptions::NotSupportedException, "Jani export of until formulas with multiple step bounds is not supported."); @@ -262,15 +262,15 @@ namespace storm { return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); } - + boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cumulative reward formulae"); } - + boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { ExportJsonType opDecl; opDecl["op"] = "U"; @@ -278,10 +278,10 @@ namespace storm { opDecl["right"] = anyToJson(f.getSubformula().accept(*this, data)); return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { ExportJsonType opDecl; - + // Create standard reward accumulation for time operator formulas. storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false); if (f.getSubformula().isEventuallyFormula() && f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { @@ -357,7 +357,7 @@ namespace storm { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); - + } else { // TODO add checks opDecl["op"] = "Smin"; @@ -366,7 +366,7 @@ namespace storm { } return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const { // ExportJsonType opDecl; // if(f.()) { @@ -384,7 +384,7 @@ namespace storm { // if(f.hasOptimalityType()) { // opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; // opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, boost::none)); -// +// // } else { // // TODO add checks // opDecl["op"] = "Pmin"; @@ -392,19 +392,19 @@ namespace storm { // } // } // return opDecl; - + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an LRA reward formula"); } - - + + boost::any FormulaToJaniJson::visit(storm::logic::MultiObjectiveFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a multi-objective formula"); } - + boost::any FormulaToJaniJson::visit(storm::logic::QuantileFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a Quantile formula"); } - + boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { ExportJsonType opDecl; opDecl["op"] = "U"; @@ -414,13 +414,13 @@ namespace storm { opDecl["step-bounds"] = constructPropertyInterval(intervalExpressionManager->integer(1), false, intervalExpressionManager->integer(1), false); return opDecl; } - - - - + + + + boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const { ExportJsonType opDecl; - + if(f.hasBound()) { auto bound = f.getBound(); opDecl["op"] = comparisonTypeToJani(bound.comparisonType); @@ -436,7 +436,7 @@ namespace storm { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); - + } else { // TODO add checks opDecl["op"] = "Pmin"; @@ -445,10 +445,10 @@ namespace storm { } return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { ExportJsonType opDecl; - + std::string instantName; if (model.isDiscreteTimeModel()) { instantName = "step-instant"; @@ -514,7 +514,7 @@ namespace storm { } } opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); - + if(f.hasBound()) { ExportJsonType compDecl; auto bound = f.getBound(); @@ -526,11 +526,11 @@ namespace storm { return opDecl; } } - + boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support a total reward formula"); } - + boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { ExportJsonType opDecl; storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); @@ -539,7 +539,7 @@ namespace storm { opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { ExportJsonType opDecl; opDecl["op"] = "U"; @@ -547,9 +547,9 @@ namespace storm { opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); return opDecl; } - + std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { - + using OpType = storm::expressions::OperatorType; switch(optype) { case OpType::And: @@ -602,16 +602,16 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Operator not supported by Jani"); } } - + ExportJsonType ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set const& auxiliaryVariables) { - + // Simplify the expression first and reduce the nesting auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify()); - + ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables); return anyToJson(simplifiedExpr.accept(visitor, boost::none)); } - + boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = "ite"; @@ -679,7 +679,7 @@ namespace storm { boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { return ExportJsonType(expression.getValue()); } - + boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = "av"; @@ -691,7 +691,7 @@ namespace storm { opDecl["elements"] = std::move(elements); return opDecl; } - + boost::any ExpressionToJson::visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = "ac"; @@ -704,7 +704,7 @@ namespace storm { } return opDecl; } - + boost::any ExpressionToJson::visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = "aa"; @@ -712,7 +712,7 @@ namespace storm { opDecl["index"] = anyToJson(expression.getOperand(1)->accept(*this, data)); return opDecl; } - + boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) { ExportJsonType opDecl; opDecl["op"] = "call"; @@ -724,14 +724,14 @@ namespace storm { opDecl["args"] = std::move(arguments); return opDecl; } - + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid, bool compact) { std::ofstream stream; storm::utility::openFile(filepath, stream, false, true); toStream(janiModel, formulas, stream, checkValid, compact); storm::utility::closeFile(stream); } - + void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& os, bool checkValid, bool compact) { if(checkValid) { janiModel.checkValid(); @@ -752,7 +752,7 @@ namespace storm { } STORM_LOG_INFO("Conversion completed " << janiModel.getName() << "."); } - + ExportJsonType buildActionArray(std::vector const& actions) { std::vector actionReprs; uint64_t actIndex = 0; @@ -766,11 +766,11 @@ namespace storm { actEntry["name"] = act.getName(); actionReprs.push_back(actEntry); } - + return ExportJsonType(actionReprs); - + } - + ExportJsonType buildTypeDescription(storm::expressions::Type const& type) { ExportJsonType typeDescr; if (type.isIntegerType()) { @@ -787,7 +787,7 @@ namespace storm { } return typeDescr; } - + void getBoundsFromConstraints(ExportJsonType& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector const& constants) { if (constraint.getBaseExpression().isBinaryBooleanFunctionExpression() && constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::And) { getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(0), constants); @@ -811,7 +811,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani Export for constant constraint " << constraint << " is not supported."); } } - + ExportJsonType buildConstantsArray(std::vector const& constants) { std::vector constantDeclarations; for(auto const& constant : constants) { @@ -833,8 +833,8 @@ namespace storm { } return ExportJsonType(constantDeclarations); } - - + + ExportJsonType buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) { ExportJsonType variableDeclarations = std::vector(); for(auto const& variable : varSet) { @@ -916,7 +916,7 @@ namespace storm { } return functionDeclarations; } - + ExportJsonType buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType assignmentDeclarations = std::vector(); bool addIndex = orderedAssignments.hasMultipleLevels(); @@ -943,7 +943,7 @@ namespace storm { } return assignmentDeclarations; } - + ExportJsonType buildLocationsArray(std::vector const& locations, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType locationDeclarations = std::vector(); for(auto const& location : locations) { @@ -964,7 +964,7 @@ namespace storm { } return locationDeclarations; } - + ExportJsonType buildInitialLocations(storm::jani::Automaton const& automaton) { std::vector names; for(auto const& initLocIndex : automaton.getInitialLocationIndices()) { @@ -972,7 +972,7 @@ namespace storm { } return ExportJsonType(names); } - + ExportJsonType buildDestinations(std::vector const& destinations, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { assert(destinations.size() > 0); ExportJsonType destDeclarations = std::vector(); @@ -998,7 +998,7 @@ namespace storm { } return destDeclarations; } - + ExportJsonType buildEdge(Edge const& edge , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed."); ExportJsonType edgeEntry; @@ -1024,7 +1024,7 @@ namespace storm { } return edgeEntry; } - + ExportJsonType buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType edgeDeclarations = std::vector(); for(auto const& edge : edges) { @@ -1035,7 +1035,7 @@ namespace storm { } return edgeDeclarations; } - + ExportJsonType buildAutomataArray(std::vector const& automata, std::map const& actionNames, std::vector const& constants, VariableSet const& globalVariables, bool commentExpressions) { ExportJsonType automataDeclarations = std::vector(); for(auto const& automaton : automata) { @@ -1055,7 +1055,7 @@ namespace storm { } return automataDeclarations; } - + void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) { modelFeatures = janiModel.getModelFeatures(); jsonStruct["jani-version"] = janiModel.getJaniVersion(); @@ -1071,12 +1071,12 @@ namespace storm { jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); } - + ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) { auto const& automaton = janiModel.getAutomaton(automatonIndex); return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions); } - + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: @@ -1102,7 +1102,7 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); } - + ExportJsonType convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) { ExportJsonType propDecl; propDecl["states"]["op"] = "initial"; @@ -1111,11 +1111,11 @@ namespace storm { propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model, modelFeatures); return propDecl; } - - + + void JsonExporter::convertProperties( std::vector const& formulas, storm::jani::Model const& model) { ExportJsonType properties; - + // Unset model-features that only relate to properties. These are only set if such properties actually exist. modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards); if (formulas.empty()) { @@ -1133,7 +1133,7 @@ namespace storm { } jsonStruct["properties"] = std::move(properties); } - + ExportJsonType JsonExporter::finalize() { jsonStruct["features"] = ExportJsonType::parse(modelFeatures.toString()); return jsonStruct; diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 496ac7bf8..7e4b7e766 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -345,19 +345,19 @@ namespace storm { * @return Retrieves the mapping of player names to their indices. */ std::map const& getPlayerNameToIndexMapping() const; - + /*! * Retrieves a vector whose i'th entry corresponds to the player controlling module i. * Modules that are not controlled by any player will get assigned INVALID_PLAYER_INDEX */ std::vector buildModuleIndexToPlayerIndexMap() const; - + /*! * Retrieves a vector whose i'th entry corresponds to the player controlling action with index i. * Actions that are not controlled by any player (in particular the silent action) will get assigned INVALID_PLAYER_INDEX. */ std::map buildActionIndexToPlayerIndexMap() const; - + /*! * Retrieves the mapping of action names to their indices. * diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 19554875c..e98ccfea2 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -179,10 +179,10 @@ namespace storm { return storm::modelchecker::SparseDtmcPrctlModelChecker>::canHandleStatic(checkTask); case ModelType::CTMC: return storm::modelchecker::SparseCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::SMG: case ModelType::MDP: case ModelType::MA: case ModelType::POMDP: - case ModelType::SMG: return false; } break;