diff --git a/CHANGELOG.md b/CHANGELOG.md index ed86c3df0..3c8aeb2d8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ Version 1.6.x ## Version 1.6.4 (20xx/xx) - Added an export of check results to json. Use `--exportresult` in the command line interface. - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface. +- Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now. ## Version 1.6.3 (2020/11) - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives. diff --git a/README.md b/README.md index 4b2dd59e2..99265f6f0 100644 --- a/README.md +++ b/README.md @@ -57,5 +57,6 @@ Storm has been developed at RWTH Aachen University. * Jan Karuc * Gereon Kremer * Sascha Vincent Kurowski +* Stefan Pranger * Manuel Sascha Weiand * Lukas Westhofen diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 139c3e226..87fe8edc9 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -133,8 +133,14 @@ namespace storm { 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)]; quantileFormula.name("Quantile formula"); - - stateFormula = (orStateFormula | multiFormula | quantileFormula); + + playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)]; + playerCoalition.name("player coalition"); + + 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); stateFormula.name("state formula"); formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); @@ -472,5 +478,12 @@ namespace storm { } } + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { + return storm::logic::PlayerCoalition(playerIds); + } + + std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); + } } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index b60ef27f0..e709366cd 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -3,6 +3,8 @@ #include #include +#include + #include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/jani/Property.h" @@ -160,7 +162,9 @@ namespace storm { qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; - + + qi::rule>>, Skipper> playerCoalition; + qi::rule filterProperty; qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; @@ -199,10 +203,14 @@ namespace storm { qi::rule(), Skipper> multiFormula; qi::rule>, Skipper> quantileBoundVariable; qi::rule(), Skipper> quantileFormula; - + qi::rule(), Skipper> gameFormula; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; + storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; + std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index c95c42af2..1fa1a38c7 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -1,5 +1,6 @@ #include "storm-parsers/parser/PrismParser.h" +#include #include "storm/storage/prism/Compositions.h" @@ -23,7 +24,7 @@ namespace storm { std::ifstream inputFileStream; storm::utility::openFile(filename, inputFileStream); storm::prism::Program result; - + // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); @@ -37,15 +38,15 @@ namespace storm { storm::utility::closeFile(inputFileStream); throw e; } - + // Close the stream in case everything went smoothly and return result. storm::utility::closeFile(inputFileStream); return result; } - + storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) { bool hasByteOrderMark = input.size() >= 3 && input[0] == '\xEF' && input[1] == '\xBB' && input[2] == '\xBF'; - + PositionIteratorType first(hasByteOrderMark ? input.begin() + 3 : input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); @@ -53,7 +54,7 @@ namespace storm { // Create empty result; storm::prism::Program result; - + // Create grammar. storm::parser::PrismParser grammar(filename, first, prismCompatibility); try { @@ -62,7 +63,7 @@ namespace storm { bool succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass."); STORM_LOG_DEBUG("First pass of parsing PRISM input finished."); - + // Start second run. first = PositionIteratorType(input.begin()); iter = first; @@ -73,98 +74,98 @@ namespace storm { } catch (qi::expectation_failure const& e) { // If the parser expected content different than the one provided, display information about the location of the error. std::size_t lineNumber = boost::spirit::get_line(e.first); - + // Now propagate exception. STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << "."); } - + STORM_LOG_TRACE("Parsed PRISM input: " << result); - + return result; } - + PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { - + ExpressionParser& expression_ = *expressionParser; boolExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfBoolType, phoenix::ref(*this), qi::_val)]; boolExpression.name("boolean expression"); - + intExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfIntType, phoenix::ref(*this), qi::_val)]; intExpression.name("integer expression"); - + numericalExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfNumericalType, phoenix::ref(*this), qi::_val)]; numericalExpression.name("numerical expression"); - + // Parse simple identifier. identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); - + // Fail if the identifier has been used before freshIdentifier = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshIdentifier, phoenix::ref(*this), qi::_1)]; freshIdentifier.name("fresh identifier"); - + modelTypeDefinition %= modelType_; modelTypeDefinition.name("model type"); - + // Defined constants. Will be checked before undefined constants. // ">>" before literal '=' because we can still parse an undefined constant afterwards. definedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) >> (qi::lit("=") > boolExpression > qi::lit(";")) )[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); - + definedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) >> freshIdentifier) >> (qi::lit("=") > intExpression > qi::lit(";")) )[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; // '>>' before freshIdentifier because of the optional 'int'. Otherwise, undefined constant 'const bool b;' would not parse. definedIntegerConstantDefinition.name("defined integer constant declaration"); - + definedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) >> (qi::lit("=") > numericalExpression > qi::lit(";")) )[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedDoubleConstantDefinition.name("defined double constant declaration"); - + definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition); definedConstantDefinition.name("defined constant definition"); - + // Undefined constants. At this point we already checked for a defined constant, therefore a ";" is required after the identifier; undefinedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - + undefinedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - + undefinedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant definition"); - + undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedDoubleConstantDefinition | undefinedIntegerConstantDefinition); // Due to the 'const N;' syntax, it is important to have integer constants last undefinedConstantDefinition.name("undefined constant definition"); - + // formula definitions. This will be changed for the second run. formulaDefinitionRhs = (qi::lit("=") > qi::as_string[(+(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))))][qi::_val = qi::_1] > qi::lit(";")); formulaDefinitionRhs.name("formula defining expression"); - + formulaDefinition = (qi::lit("formula") > freshIdentifier > formulaDefinitionRhs )[qi::_val = phoenix::bind(&PrismParser::createFormulaFirstRun, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition.name("formula definition"); - + booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - + integerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; integerVariableDefinition.name("integer variable definition"); - + clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)]; clockVariableDefinition.name("clock variable definition"); - + variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]); variableDefinition.name("variable declaration"); - + globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)])); globalVariableDefinition.name("global variable declaration list"); - + stateRewardDefinition = (boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - + stateActionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)]; stateActionRewardDefinition.name("state action reward definition"); @@ -181,28 +182,28 @@ namespace storm { ) > qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)]; rewardModelDefinition.name("reward model definition"); - + initialStatesConstruct = (qi::lit("init") > boolExpression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; initialStatesConstruct.name("initial construct"); observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)]; observablesConstruct.name("observables construct"); - + invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1]; invariantConstruct.name("invariant construct"); - knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1)]; + knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1, false)]; knownModuleName.name("existing module name"); - + freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshModuleName, phoenix::ref(*this), qi::_1)]; freshModuleName.name("fresh module name"); systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; systemCompositionConstruct.name("system composition construct"); - + actionNameList %= identifier[phoenix::insert(qi::_val, qi::_1)] >> *("," >> identifier[phoenix::insert(qi::_val, qi::_1)]); actionNameList.name("action list"); - + parallelComposition = hidingOrRenamingComposition[qi::_val = qi::_1] >> *((interleavingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createInterleavingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] | (synchronizingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createSynchronizingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] | (restrictedParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createRestrictedParallelComposition, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)] @@ -211,31 +212,31 @@ namespace storm { synchronizingParallelComposition = qi::lit("||"); synchronizingParallelComposition.name("synchronizing parallel composition"); - + interleavingParallelComposition = qi::lit("|||"); interleavingParallelComposition.name("interleaving parallel composition"); restrictedParallelComposition = qi::lit("|[") > actionNameList > qi::lit("]|"); restrictedParallelComposition.name("restricted parallel composition"); - + hidingOrRenamingComposition = hidingComposition | renamingComposition | atomicComposition; hidingOrRenamingComposition.name("hiding/renaming composition"); - + hidingComposition = (atomicComposition >> (qi::lit("/") > (qi::lit("{") > actionNameList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)]; hidingComposition.name("hiding composition"); - + actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct>(qi::_1, qi::_2))]; actionRenamingList.name("action renaming list"); - + renamingComposition = (atomicComposition >> (qi::lit("{") > (actionRenamingList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)]; renamingComposition.name("renaming composition"); - + atomicComposition = (qi::lit("(") > parallelComposition > qi::lit(")")) | moduleComposition; atomicComposition.name("atomic composition"); - + moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)]; moduleComposition.name("module composition"); - + freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)]; freshLabelName.name("fresh label name"); @@ -247,20 +248,20 @@ namespace storm { observableDefinition = (qi::lit("observable") > -qi::lit("\"") > freshObservationLabelName > -qi::lit("\"") > qi::lit("=") > (intExpression | boolExpression) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createObservationLabel, phoenix::ref(*this), qi::_1, qi::_2)]; observableDefinition.name("observable definition"); - + assignmentDefinition = ((qi::lit("(") >> identifier >> qi::lit("'")) > qi::lit("=") > expression_ > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); - + assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); - + updateDefinition = (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), manager->rational(1), qi::_1, qi::_r1)] | ((numericalExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)])); updateDefinition.name("update"); - + updateListDefinition %= +updateDefinition(qi::_r1) % "+"; updateListDefinition.name("update list"); - + // This is a dummy command-definition (it ignores the actual contents of the command) that is overwritten when the parser is moved to the second run. commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | @@ -272,16 +273,32 @@ namespace storm { // We first check for a module renaming, i.e., for this rule we certainly have to see a module definition moduleDefinition = ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)]; moduleDefinition.name("module definition"); - + + freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshPlayerName, phoenix::ref(*this), qi::_1)]; + freshPlayerName.name("fresh player name"); + + playerControlledActionName = ((qi::lit("[") > identifier > qi::lit("]"))[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownActionName, phoenix::ref(*this), qi::_1, true)]; + playerControlledActionName.name("player controlled action name"); + + playerControlledModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1, true)]; + playerControlledModuleName.name("player controlled module name"); + + playerConstruct = (qi::lit("player") > freshPlayerName[qi::_a = qi::_1] + > +( (playerControlledActionName[phoenix::push_back(qi::_c, qi::_1)] + | playerControlledModuleName[phoenix::push_back(qi::_b, qi::_1)]) % ',' + ) + > qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParser::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; + playerConstruct.name("player construct"); + moduleRenaming = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = phoenix::bind(&PrismParser::createModuleRenaming, phoenix::ref(*this), qi::_a)]; moduleRenaming.name("Module renaming list"); - + renamedModule = (((qi::lit("module") > freshModuleName) >> qi::lit("=")) > knownModuleName[qi::_a = qi::_1] > (moduleRenaming[qi::_b = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isValidModuleRenaming, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)] > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)]; renamedModule.name("module definition via renaming"); - + start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] > -observablesConstruct @@ -293,12 +310,13 @@ namespace storm { | initialStatesConstruct(phoenix::ref(globalProgramInformation)) | rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] - | observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)), qi::_1)] - | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] + | observableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::observationLabels, phoenix::ref(globalProgramInformation)), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] + | playerConstruct(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)] ) > -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]; start.name("probabilistic program"); - + // Enable location tracking for important entities. auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3); qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction); @@ -320,16 +338,16 @@ namespace storm { qi::on_success(commandDefinition, setLocationInfoFunction); qi::on_success(updateDefinition, setLocationInfoFunction); qi::on_success(assignmentDefinition, setLocationInfoFunction); - + // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } - + void PrismParser::moveToSecondRun() { // In the second run, we actually need to parse the commands instead of just skipping them, // so we adapt the rule for parsing commands. STORM_LOG_THROW(observables.empty(), storm::exceptions::WrongFormatException, "Some variables marked as observable, but never declared, e.g. " << *observables.begin()); - + commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) @@ -350,10 +368,10 @@ namespace storm { // * in the first run, the type of the formula (int, bool, clock) is not known // * in the second run, formulas might be used before they are declared createFormulaIdentifiers(this->globalProgramInformation.formulas); - + this->globalProgramInformation.moveToSecondRun(); } - + void PrismParser::createFormulaIdentifiers(std::vector const& formulas) { STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException, "Unexpected number of formulas and formula expressions"); this->formulaOrder.clear(); @@ -397,30 +415,30 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "'."); } } - + void PrismParser::allowDoubleLiterals(bool flag) { this->expressionParser->setAcceptDoubleLiterals(flag); } - + std::string const& PrismParser::getFilename() const { return this->filename; } - + bool PrismParser::isValidIdentifier(std::string const& identifier) { if (this->keywords_.find(identifier) != nullptr) { return false; } return true; } - - bool PrismParser::isKnownModuleName(std::string const& moduleName) { - if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) { + + bool PrismParser::isKnownModuleName(std::string const& moduleName, bool inSecondRun) { + if ((this->secondRun == inSecondRun) && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) { STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'."); return false; } return true; } - + bool PrismParser::isFreshModuleName(std::string const& moduleName) { if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) != 0) { STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate module name '" << moduleName << "'."); @@ -428,7 +446,15 @@ namespace storm { } return true; } - + + bool PrismParser::isKnownActionName(std::string const& actionName, bool inSecondRun) { + if ((this->secondRun == inSecondRun) && this->globalProgramInformation.actionIndices.count(actionName) == 0) { + STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown action label '" << actionName << "'."); + return false; + } + return true; + }; + bool PrismParser::isFreshIdentifier(std::string const& identifier) { if (!this->secondRun && this->manager->hasVariable(identifier)) { STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'."); @@ -436,7 +462,7 @@ namespace storm { } return true; } - + bool PrismParser::isFreshLabelName(std::string const& labelName) { if (!this->secondRun) { for (auto const& existingLabel : this->globalProgramInformation.labels) { @@ -460,7 +486,7 @@ namespace storm { } return true; } - + bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) { if (!this->secondRun) { for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) { @@ -472,19 +498,23 @@ namespace storm { } return true; } - + + bool PrismParser::isFreshPlayerName(std::string const& playerName) { + return true; + } + bool PrismParser::isOfBoolType(storm::expressions::Expression const& expression) { return !this->secondRun || expression.hasBooleanType(); } - + bool PrismParser::isOfIntType(storm::expressions::Expression const& expression) { return !this->secondRun || expression.hasIntegerType(); } - + bool PrismParser::isOfNumericalType(storm::expressions::Expression const& expression) { return !this->secondRun || expression.hasNumericalType(); } - + bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not define two initial constructs."); if (globalProgramInformation.hasInitialConstruct) { @@ -494,12 +524,12 @@ namespace storm { globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3)); return true; } - + bool PrismParser::addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation) { globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3)); return true; } - + void PrismParser::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) { STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not set model type multiple times."); globalProgramInformation.modelType = modelType; @@ -508,27 +538,27 @@ namespace storm { std::shared_ptr PrismParser::createModuleComposition(std::string const& moduleName) const { return std::make_shared(moduleName); } - + std::shared_ptr PrismParser::createRenamingComposition(std::shared_ptr const& subcomposition, std::map const& renaming) const { return std::make_shared(subcomposition, renaming); } - + std::shared_ptr PrismParser::createHidingComposition(std::shared_ptr const& subcomposition, std::set const& actionsToHide) const { return std::make_shared(subcomposition, actionsToHide); } - + std::shared_ptr PrismParser::createSynchronizingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const { return std::make_shared(left, right); } - + std::shared_ptr PrismParser::createInterleavingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right) const { return std::make_shared(left, right); } - + std::shared_ptr PrismParser::createRestrictedParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr const& right) const { return std::make_shared(left, synchronizingActions, right); } - + storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { if (!this->secondRun) { try { @@ -540,7 +570,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } - + storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { if (!this->secondRun) { try { @@ -552,7 +582,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } - + storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { if (!this->secondRun) { try { @@ -564,7 +594,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } - + storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { @@ -576,7 +606,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } - + storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { @@ -588,7 +618,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } - + storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { @@ -600,7 +630,7 @@ namespace storm { } return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } - + storm::prism::Formula PrismParser::createFormulaFirstRun(std::string const& formulaName, std::string const& expression) { // Only store the expression as a string. It will be parsed between first and second run // This is necessary because the resulting type of the formula is only known after the first run. @@ -608,14 +638,14 @@ namespace storm { formulaExpressions.push_back(expression); return storm::prism::Formula(formulaName, this->getFilename()); } - + storm::prism::Formula PrismParser::createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression) { // This is necessary because the resulting type of the formula is only known after the first run. STORM_LOG_ASSERT(this->secondRun, "This constructor should have only been called during the second run."); storm::expressions::Expression lhsExpression = *this->identifiers_.find(formulaName); return storm::prism::Formula(lhsExpression.getBaseExpression().asVariableExpression().getVariable(), expression, this->getFilename()); } - + storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const { return storm::prism::Label(labelName, expression, this->getFilename()); } @@ -623,11 +653,11 @@ namespace storm { storm::prism::ObservationLabel PrismParser::createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const { return storm::prism::ObservationLabel(labelName, expression, this->getFilename()); } - + storm::prism::RewardModel PrismParser::createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards) const { return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename()); } - + storm::prism::StateReward PrismParser::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const { if (this->secondRun) { return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); @@ -635,11 +665,11 @@ namespace storm { return storm::prism::StateReward(); } } - + storm::prism::StateActionReward PrismParser::createStateActionReward(boost::optional const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { if (this->secondRun) { std::string realActionName = actionName ? actionName.get() : ""; - + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Action reward refers to illegal action '" << realActionName << "'."); return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename()); @@ -647,11 +677,11 @@ namespace storm { return storm::prism::StateActionReward(); } } - + storm::prism::TransitionReward PrismParser::createTransitionReward(boost::optional const& actionName, storm::expressions::Expression sourceStatePredicateExpression, storm::expressions::Expression targetStatePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { if (this->secondRun) { std::string realActionName = actionName ? actionName.get() : ""; - + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'."); return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); @@ -659,22 +689,22 @@ namespace storm { return storm::prism::TransitionReward(); } } - + storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const { return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename()); } - + storm::prism::Update PrismParser::createUpdate(storm::expressions::Expression likelihoodExpression, std::vector const& assignments, GlobalProgramInformation& globalProgramInformation) const { ++globalProgramInformation.currentUpdateIndex; return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpression, assignments, this->getFilename()); } - + storm::prism::Command PrismParser::createCommand(bool markovian, boost::optional const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const { ++globalProgramInformation.currentCommandIndex; std::string realActionName = actionName ? actionName.get() : ""; uint_fast64_t actionIndex = 0; - + // If the action name was not yet seen, record it. auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); if (nameIndexPair == globalProgramInformation.actionIndices.end()) { @@ -686,7 +716,7 @@ namespace storm { } return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, markovian, actionIndex, realActionName, guardExpression, updates, this->getFilename()); } - + storm::prism::Command PrismParser::createDummyCommand(boost::optional const& actionName, GlobalProgramInformation& globalProgramInformation) const { STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run."); std::string realActionName = actionName ? actionName.get() : ""; @@ -697,10 +727,10 @@ namespace storm { std::size_t nextIndex = globalProgramInformation.actionIndices.size(); globalProgramInformation.actionIndices.emplace(realActionName, nextIndex); } - + return storm::prism::Command(); } - + storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { try { @@ -716,7 +746,7 @@ namespace storm { } return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename()); } - + storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { try { @@ -733,7 +763,7 @@ namespace storm { return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename()); } - + storm::prism::ClockVariable PrismParser::createClockVariable(std::string const& variableName) const { if (!this->secondRun) { try { @@ -755,12 +785,41 @@ namespace storm { this->observables.insert(observables.begin(), observables.end()); // We need this list to be filled in both runs. } - + + storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & actionNames) { + if (this->secondRun) { + std::unordered_set controlledModules; + std::unordered_set controlledActions; + for(auto const& moduleName : moduleNames) { + auto moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName); + STORM_LOG_ASSERT(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present."); + controlledModules.insert(moduleIndexPair->first); + bool moduleNotYetControlled = globalProgramInformation.playerControlledModules.insert(moduleIndexPair->second).second; + STORM_LOG_THROW(moduleNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName << "' already controlled by another player."); + } + for(std::string actionName : actionNames) { + auto actionIndexPair = globalProgramInformation.actionIndices.find(actionName); + STORM_LOG_ASSERT(actionIndexPair != globalProgramInformation.actionIndices.end(), "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present."); + controlledActions.insert(actionIndexPair->first); + bool actionNotYetControlled = globalProgramInformation.playerControlledActions.insert(actionIndexPair->second).second; + STORM_LOG_THROW(actionNotYetControlled, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName << "' already controlled by another player."); + } + return storm::prism::Player(playerName, controlledModules, controlledActions); + } else { + return storm::prism::Player(); + } + } + storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { - globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); + if (!this->secondRun) { + globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); + } + // Assert that the module name is already known and has the expected index. + STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap.count(moduleName) > 0, "Module name '" << moduleName << "' was not found."); + STORM_LOG_ASSERT(!this->secondRun || globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), "The index for module '" << moduleName << "' does not match the index from the first parsing run."); return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename()); } - + bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const { if (!this->secondRun) { auto const& renaming = moduleRenaming.getRenaming(); @@ -795,19 +854,22 @@ namespace storm { } return true; } - + storm::prism::ModuleRenaming PrismParser::createModuleRenaming(std::map const& renaming) const { return storm::prism::ModuleRenaming(renaming); } - + storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation& globalProgramInformation) const { // Check whether the module to rename actually exists. auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename."); storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second]; + STORM_LOG_THROW(!moduleToRename.isRenamedFromModule(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": The module '" << newModuleName << "' can not be created from module '" << oldModuleName << "' through module renaming because '" << oldModuleName << "' is also a renamed module. Create '" << newModuleName << "' via a renaming from base module '" << moduleToRename.getBaseModule() << "' instead."); auto const& renaming = moduleRenaming.getRenaming(); - 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()) { @@ -837,7 +899,7 @@ namespace storm { this->observables.erase(renamingPair->second); } } - + for (auto const& command : moduleToRename.getCommands()) { std::string newActionName = command.getActionName(); auto const& renamingPair = renaming.find(command.getActionName()); @@ -852,12 +914,13 @@ namespace storm { globalProgramInformation.actionIndices.emplace(newActionName, nextIndex); } } - + // Return a dummy module in the first pass. return storm::prism::Module(); } else { - // Add a mapping from the new module name to its (future) index. - globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size(); + // 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; @@ -868,7 +931,7 @@ namespace storm { expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression); } } - + // Rename the boolean variables. std::vector booleanVariables; for (auto const& variable : moduleToRename.getBooleanVariables()) { @@ -880,7 +943,7 @@ namespace storm { } booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), moduleRenaming.getLineNumber())); } - + // Rename the integer variables. std::vector integerVariables; for (auto const& variable : moduleToRename.getIntegerVariables()) { @@ -904,13 +967,13 @@ namespace storm { } clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), moduleRenaming.getLineNumber())); } - + // Rename invariant (if present) storm::expressions::Expression invariant; if (moduleToRename.hasInvariant()) { invariant = moduleToRename.getInvariant().substitute(expressionRenaming); } - + // Rename commands. std::vector commands; for (auto const& command : moduleToRename.getCommands()) { @@ -928,13 +991,13 @@ namespace storm { updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), moduleRenaming.getLineNumber()); ++globalProgramInformation.currentUpdateIndex; } - + std::string newActionName = command.getActionName(); auto const& renamingPair = renaming.find(command.getActionName()); if (renamingPair != renaming.end()) { newActionName = renamingPair->second; } - + uint_fast64_t actionIndex = 0; auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName); if (nameIndexPair == globalProgramInformation.actionIndices.end()) { @@ -944,22 +1007,22 @@ namespace storm { } else { actionIndex = nameIndexPair->second; } - + commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), moduleRenaming.getLineNumber()); ++globalProgramInformation.currentCommandIndex; } - + return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming); } } - + storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { storm::prism::Program::ModelType finalModelType = globalProgramInformation.modelType; if (globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED) { STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'."); finalModelType = storm::prism::Program::ModelType::MDP; } - + // make sure formulas are stored in a proper order. std::vector orderedFormulas; if (this->secondRun) { @@ -969,9 +1032,9 @@ namespace storm { } } - return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); } - + void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { globalProgramInformation.hasInitialConstruct = false; } diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 2668dcb68..2a1d5beeb 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -20,7 +20,7 @@ namespace storm { namespace storm { namespace parser { class ExpressionParser; - + // A class that stores information about the parsed program. class GlobalProgramInformation { public: @@ -29,7 +29,7 @@ namespace storm { // Map the empty action to index 0. actionIndices.emplace("", 0); } - + void moveToSecondRun() { // Clear all data except the action to indices mapping. modelType = storm::prism::Program::ModelType::UNDEFINED; @@ -37,7 +37,9 @@ namespace storm { formulas.clear(); globalBooleanVariables.clear(); globalIntegerVariables.clear(); - moduleToIndexMap.clear(); + players.clear(); + playerControlledModules.clear(); + playerControlledActions.clear(); modules.clear(); rewardModels.clear(); labels.clear(); @@ -45,11 +47,11 @@ namespace storm { hasInitialConstruct = false; initialConstruct = storm::prism::InitialConstruct(); systemCompositionConstruct = boost::none; - + currentCommandIndex = 0; currentUpdateIndex = 0; } - + // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; std::vector constants; @@ -62,11 +64,15 @@ namespace storm { std::vector rewardModels; std::vector labels; std::vector observationLabels; + std::vector players; + std::set playerControlledModules; + std::set playerControlledActions; + bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; boost::optional systemCompositionConstruct; - + // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; uint_fast64_t currentUpdateIndex; @@ -81,7 +87,7 @@ namespace storm { * @return The resulting PRISM program. */ static storm::prism::Program parse(std::string const& filename, bool prismCompatability = false); - + /*! * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. * @@ -90,7 +96,7 @@ namespace storm { * @return The resulting PRISM program. */ static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool prismCompatability = false); - + private: struct modelTypeStruct : qi::symbols { modelTypeStruct() { @@ -101,10 +107,11 @@ namespace storm { ("ctmdp", storm::prism::Program::ModelType::CTMDP) ("ma", storm::prism::Program::ModelType::MA) ("pomdp", storm::prism::Program::ModelType::POMDP) - ("pta", storm::prism::Program::ModelType::PTA); + ("pta", storm::prism::Program::ModelType::PTA) + ("smg", storm::prism::Program::ModelType::SMG); } }; - + struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -115,35 +122,38 @@ namespace storm { ("ma", 5) ("pomdp", 6) ("pta", 7) - ("const", 8) - ("int", 9) - ("bool", 10) - ("module", 11) - ("endmodule", 12) - ("rewards", 13) - ("endrewards", 14) - ("true", 15) - ("false", 16) - ("min", 17) - ("max", 18) - ("floor", 19) - ("ceil", 20) - ("init", 21) - ("endinit", 22) - ("invariant", 23) - ("endinvariant", 24); + ("smg", 8) + ("const", 9) + ("int", 10) + ("bool", 11) + ("module", 12) + ("endmodule", 13) + ("rewards", 14) + ("endrewards", 15) + ("true", 16) + ("false", 17) + ("min", 18) + ("max", 19) + ("floor", 20) + ("ceil", 21) + ("init", 22) + ("endinit", 23) + ("invariant", 24) + ("endinvariant", 25) + ("player", 26) + ("endplayer", 27); } }; - + // Functor used for annotating entities with line number information. class PositionAnnotation { public: typedef void result_type; - + PositionAnnotation(Iterator first) : first(first) { // Intentionally left empty. } - + template result_type operator()(Entity& entity, First f, Last) const { entity.setLineNumber(get_line(f)); @@ -152,7 +162,7 @@ namespace storm { std::string filename; Iterator const first; }; - + /*! * Creates a grammar for the given filename and the iterator to the first input to parse. * @@ -160,32 +170,32 @@ namespace storm { * @param first The iterator to the beginning of the input. */ PrismParser(std::string const& filename, Iterator first, bool prismCompatibility); - + /*! * Sets an internal flag that indicates the second run is now taking place. */ void moveToSecondRun(); - + /*! * Parses the stored formula Expressions. */ void createFormulaIdentifiers(std::vector const& formulas); - + // A flag that stores whether the grammar is currently doing the second run. bool secondRun; bool prismCompatibility; - + /*! * Sets whether doubles literals are allowed in the parsed expression. * * @param flag Indicates whether to allow or forbid double literals in the parsed expression. */ void allowDoubleLiterals(bool flag); - + // The name of the file being parsed. std::string filename; - + /*! * Retrieves the name of the file currently being parsed. * @@ -194,22 +204,22 @@ namespace storm { std::string const& getFilename() const; mutable std::set observables; - + // Store the expressions of formulas. They have to be parsed after the first and before the second run std::vector formulaExpressions; // Stores a proper order in which formulas can be evaluated. This is necessary since formulas might depend on each other. // E.g. for "formula x = y; formula y = z;" we have to swap the order of the two formulas. std::vector formulaOrder; - + // A function used for annotating the entities with their position. phoenix::function annotate; - + // An object gathering information about the program while parsing. GlobalProgramInformation globalProgramInformation; - + // The starting point of the grammar. qi::rule start; - + // Rules for model type. qi::rule modelTypeDefinition; @@ -217,7 +227,7 @@ namespace storm { qi::rule boolExpression; qi::rule intExpression; qi::rule numericalExpression; - + // Rules for parsing the program header. qi::rule undefinedConstantDefinition; qi::rule undefinedBooleanConstantDefinition; @@ -227,45 +237,52 @@ namespace storm { qi::rule definedBooleanConstantDefinition; qi::rule definedIntegerConstantDefinition; qi::rule definedDoubleConstantDefinition; - + // Rules for global variable definitions. qi::rule globalVariableDefinition; qi::rule globalBooleanVariableDefinition; qi::rule globalIntegerVariableDefinition; - + // Rules for modules definition. qi::rule knownModuleName; qi::rule freshModuleName; qi::rule, std::vector, std::vector>, Skipper> moduleDefinition; qi::rule>, Skipper> moduleRenaming; qi::rule, Skipper> renamedModule; - + // Rules for variable definitions. qi::rule&, std::vector&, std::vector&), Skipper> variableDefinition; qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; qi::rule, Skipper> clockVariableDefinition; - + // Rules for command definitions. qi::rule, Skipper> commandDefinition; qi::rule(GlobalProgramInformation&), Skipper> updateListDefinition; qi::rule updateDefinition; qi::rule(), Skipper> assignmentDefinitionList; qi::rule assignmentDefinition; - + qi::rule knownActionName; + // Rules for reward definitions. qi::rule freshRewardModelName; qi::rule, std::vector, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; qi::rule stateActionRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; - + + // Rules for player definitions + qi::rule freshPlayerName; + qi::rule, Skipper> playerControlledActionName; + qi::rule, Skipper> playerControlledModuleName; + qi::rule, std::vector>, Skipper> playerConstruct; + // Rules for initial states expression. qi::rule initialStatesConstruct; // Rules for POMDP observables (standard prism) qi::rule observablesConstruct; - + // Rules for invariant constructs qi::rule invariantConstruct; @@ -294,28 +311,30 @@ namespace storm { // Rules for formula definitions. qi::rule formulaDefinitionRhs; qi::rule formulaDefinition; - + // Rules for identifier parsing. qi::rule identifier; qi::rule freshIdentifier; - + // Parsers that recognize special keywords and model types. storm::parser::PrismParser::keywordsStruct keywords_; storm::parser::PrismParser::modelTypeStruct modelType_; qi::symbols identifiers_; - + // Parser and manager used for recognizing expressions. std::shared_ptr manager; std::shared_ptr expressionParser; - + // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); bool isFreshIdentifier(std::string const& identifier); - bool isKnownModuleName(std::string const& moduleName); + bool isKnownModuleName(std::string const& moduleName, bool inSecondRun); bool isFreshModuleName(std::string const& moduleName); + bool isKnownActionName(std::string const& actionName, bool inSecondRun); bool isFreshLabelName(std::string const& moduleName); bool isFreshObservationLabelName(std::string const& labelName); bool isFreshRewardModelName(std::string const& moduleName); + bool isFreshPlayerName(std::string const& playerName); bool isOfBoolType(storm::expressions::Expression const& expression); bool isOfIntType(storm::expressions::Expression const& expression); bool isOfNumericalType(storm::expressions::Expression const& expression); @@ -323,7 +342,7 @@ namespace storm { bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation); void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType); - + std::shared_ptr createModuleComposition(std::string const& moduleName) const; std::shared_ptr createRenamingComposition(std::shared_ptr const& subcomposition, std::map const& renaming) const; std::shared_ptr createHidingComposition(std::shared_ptr const& subcomposition, std::set const& actionsToHide) const; @@ -355,12 +374,13 @@ namespace storm { storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::ModuleRenaming createModuleRenaming(std::map const& renaming) const; storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Player createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & commandNames); storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; void createObservablesList(std::vector const& observables); void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const; - + // An error handler function. phoenix::function handler; }; @@ -368,4 +388,3 @@ namespace storm { } // namespace storm #endif /* STORM_PARSER_PRISMPARSER_H_ */ - diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index fbe838c5d..262be870c 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -12,6 +12,7 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Pomdp.h" +#include "storm/models/sparse/Smg.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StochasticTwoPlayerGame.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -141,6 +142,8 @@ namespace storm { return std::make_shared>(std::move(components)); case storm::models::ModelType::S2pg: return std::make_shared>(std::move(components)); + case storm::models::ModelType::Smg: + return std::make_shared>(std::move(components)); } } diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index f9cbda29f..9ac504d7c 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -18,6 +18,7 @@ #include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" @@ -25,6 +26,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Smg.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" @@ -251,6 +253,28 @@ namespace storm { return verifyWithSparseEngine(env, ma, task); } + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& smg, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SparseSmgRpatlModelChecker> modelchecker(*smg); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify SMGs with this data type."); + } + + template + std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& smg, storm::modelchecker::CheckTask const& task) { + Environment env; + return verifyWithSparseEngine(env, smg, task); + } + + template std::unique_ptr verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -262,6 +286,8 @@ namespace storm { result = verifyWithSparseEngine(env, model->template as>(), task); } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { result = verifyWithSparseEngine(env, model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Smg) { + result = verifyWithSparseEngine(env, model->template as>(), task); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the sparse engine."); } diff --git a/src/storm/builder/ChoiceInformationBuilder.cpp b/src/storm/builder/ChoiceInformationBuilder.cpp deleted file mode 100644 index 6578fe590..000000000 --- a/src/storm/builder/ChoiceInformationBuilder.cpp +++ /dev/null @@ -1,38 +0,0 @@ -#include "storm/builder/ChoiceInformationBuilder.h" - -namespace storm { - namespace builder { - - void ChoiceInformationBuilder::addLabel(std::string const& label, uint_fast64_t choiceIndex) { - storm::storage::BitVector& labeledChoices = labels[label]; - labeledChoices.grow(choiceIndex + 1); - labeledChoices.set(choiceIndex, true); - } - - void ChoiceInformationBuilder::addOriginData(boost::any const& originData, uint_fast64_t choiceIndex) { - if (dataOfOrigins.size() != choiceIndex) { - dataOfOrigins.resize(choiceIndex); - } - dataOfOrigins.push_back(originData); - } - - boost::optional ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) { - if (labels.empty()) { - return boost::none; - } else { - storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices); - for (auto& label : labels) { - label.second.resize(totalNumberOfChoices, false); - result.addLabel(label.first, std::move(label.second)); - } - return result; - } - } - - std::vector ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) { - dataOfOrigins.resize(totalNumberOfChoices); - return std::move(dataOfOrigins); - } - - } -} diff --git a/src/storm/builder/ChoiceInformationBuilder.h b/src/storm/builder/ChoiceInformationBuilder.h deleted file mode 100644 index 8dbe8721a..000000000 --- a/src/storm/builder/ChoiceInformationBuilder.h +++ /dev/null @@ -1,40 +0,0 @@ -#pragma once - -#include -#include -#include -#include -#include - -#include "storm/models/sparse/ChoiceLabeling.h" -#include "storm/storage/BitVector.h" -#include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/storage/prism/Program.h" - - -namespace storm { - namespace builder { - - /*! - * This class collects information regarding the choices - */ - class ChoiceInformationBuilder { - public: - - ChoiceInformationBuilder() = default; - - void addLabel(std::string const& label, uint_fast64_t choiceIndex); - - void addOriginData(boost::any const& originData, uint_fast64_t choiceIndex); - - boost::optional buildChoiceLabeling(uint_fast64_t totalNumberOfChoices); - - std::vector buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices); - - private: - std::unordered_map labels; - std::vector dataOfOrigins; - }; - } -} - diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 8fedf075b..b80825d1d 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -4,7 +4,7 @@ #include "storm/builder/RewardModelBuilder.h" -#include "storm/builder/ChoiceInformationBuilder.h" +#include "storm/builder/StateAndChoiceInformationBuilder.h" #include "storm/exceptions/AbortException.h" #include "storm/exceptions/WrongFormatException.h" @@ -49,26 +49,26 @@ namespace storm { ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options) : generator(generator), options(options), stateStorage(generator->getStateSize()) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared>(program, generatorOptions), builderOptions) { // Intentionally left empty. } - + template ExplicitModelBuilder::ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared>(model, generatorOptions), builderOptions) { // Intentionally left empty. } - + template std::shared_ptr> ExplicitModelBuilder::build() { STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); - + switch (generator->getModelType()) { case storm::generator::ModelType::DTMC: return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Dtmc, buildModelComponents()); @@ -80,22 +80,24 @@ namespace storm { return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents()); case storm::generator::ModelType::MA: return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents()); + case storm::generator::ModelType::SMG: + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Smg, buildModelComponents()); default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type."); } - + return nullptr; } - + template StateType ExplicitModelBuilder::getOrAddStateIndex(CompressedState const& state) { StateType newIndex = static_cast(stateStorage.getNumberOfStates()); - + // Check, if the state was already registered. std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - + StateType actualIndex = actualIndexBucketPair.first; - + if (actualIndex == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { statesToExplore.emplace_front(state, actualIndex); @@ -108,7 +110,7 @@ namespace storm { STORM_LOG_ASSERT(false, "Invalid exploration order."); } } - + return actualIndex; } @@ -118,24 +120,23 @@ namespace storm { } template - void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianStates, boost::optional& stateValuationsBuilder) { - - // Create markovian states bit vector, if required. - if (generator->getModelType() == storm::generator::ModelType::MA) { - // The bit vector will be resized when the correct size is known. - markovianStates = storm::storage::BitVector(1000); + void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder) { + + // Initialize building state valuations (if necessary) + if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { + stateAndChoiceInformationBuilder.stateValuationsBuilder() = generator->initializeStateValuationsBuilder(); } // Create a callback for the next-state generator to enable it to request the index of states. std::function stateToIdCallback = std::bind(&ExplicitModelBuilder::getOrAddStateIndex, this, std::placeholders::_1); - + // If the exploration order is something different from breadth-first, we need to keep track of the remapping // from state ids to row groups. For this, we actually store the reversed mapping of row groups to state-ids // and later reverse it. if (options.explorationOrder != ExplorationOrder::Bfs) { stateRemapping = std::vector(); } - + // Let the generator create all initial states. this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback); STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(), storm::exceptions::WrongFormatException, "The model does not have a single initial state."); @@ -148,30 +149,30 @@ namespace storm { auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); uint64_t numberOfExploredStates = 0; uint64_t numberOfExploredStatesSinceLastMessage = 0; - + // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. CompressedState currentState = statesToExplore.front().first; StateType currentIndex = statesToExplore.front().second; statesToExplore.pop_front(); - + // If the exploration order differs from breadth-first, we remember that this row group was actually // filled with the transitions of a different state. if (options.explorationOrder != ExplorationOrder::Bfs) { stateRemapping.get()[currentIndex] = currentRowGroup; } - + if (currentIndex % 100000 == 0) { STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); } - + generator->load(currentState); - if (stateValuationsBuilder) { - generator->addStateValuation(currentIndex, stateValuationsBuilder.get()); + if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { + generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder()); } storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); - + // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { @@ -179,28 +180,31 @@ namespace storm { if (behavior.wasExpanded()) { this->stateStorage.deadlockStateIndices.push_back(currentIndex); } - - if (markovianStates) { - markovianStates.get().grow(currentRowGroup + 1, false); - markovianStates.get().set(currentRowGroup); - } - + if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } - + transitionMatrixBuilder.addNextValue(currentRow, currentIndex, storm::utility::one()); - + for (auto& rewardModelBuilder : rewardModelBuilders) { if (rewardModelBuilder.hasStateRewards()) { rewardModelBuilder.addStateReward(storm::utility::zero()); } - + if (rewardModelBuilder.hasStateActionRewards()) { rewardModelBuilder.addStateActionReward(storm::utility::zero()); } } + // This state shall be Markovian (to not introduce Zeno behavior) + if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) { + stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup); + } + // Other state-based information does not need to be treated, in particular: + // * StateValuations have already been set above + // * The associated player shall be the "default" player, i.e. INVALID_PLAYER_INDEX + ++currentRow; ++currentRowGroup; } else { @@ -215,36 +219,40 @@ namespace storm { } ++stateRewardIt; } - + // If the model is nondeterministic, we need to open a row group. if (!generator->isDeterministicModel()) { transitionMatrixBuilder.newRowGroup(currentRow); } - + // Now add all choices. + bool firstChoiceOfState = true; for (auto const& choice : behavior) { - + // add the generated choice information - if (choice.hasLabels()) { + if (stateAndChoiceInformationBuilder.isBuildChoiceLabels() && choice.hasLabels()) { for (auto const& label : choice.getLabels()) { - choiceInformationBuilder.addLabel(label, currentRow); + stateAndChoiceInformationBuilder.addChoiceLabel(label, currentRow); } } - if (choice.hasOriginData()) { - choiceInformationBuilder.addOriginData(choice.getOriginData(), currentRow); + if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins() && choice.hasOriginData()) { + stateAndChoiceInformationBuilder.addChoiceOriginData(choice.getOriginData(), currentRow); } - - // If we keep track of the Markovian choices, store whether the current one is Markovian. - if (markovianStates && choice.isMarkovian()) { - markovianStates.get().grow(currentRowGroup + 1, false); - markovianStates.get().set(currentRowGroup); + if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications() && choice.hasPlayerIndex()) { + STORM_LOG_ASSERT(firstChoiceOfState || stateAndChoiceInformationBuilder.hasStatePlayerIndicationBeenSet(choice.getPlayerIndex(), currentRowGroup), "There is a state where different players have an enabled choice."); // Should have been detected in generator, already + if (firstChoiceOfState) { + stateAndChoiceInformationBuilder.addStatePlayerIndication(choice.getPlayerIndex(), currentRowGroup); + } } - + if (stateAndChoiceInformationBuilder.isBuildMarkovianStates() && choice.isMarkovian()) { + stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup); + } + // Add the probabilistic behavior to the matrix. for (auto const& stateProbabilityPair : choice) { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } - + // Add the rewards to the reward models. auto choiceRewardIt = choice.getRewards().begin(); for (auto& rewardModelBuilder : rewardModelBuilders) { @@ -254,7 +262,9 @@ namespace storm { ++choiceRewardIt; } ++currentRow; + firstChoiceOfState = false; } + ++currentRowGroup; } @@ -280,24 +290,19 @@ namespace storm { break; } } - - if (markovianStates) { - // Since we now know the correct size, cut the bit vector to the correct length. - markovianStates->resize(currentRowGroup, false); - } // If the exploration order was not breadth-first, we need to fix the entries in the matrix according to // (reversed) mapping of row groups to indices. if (options.explorationOrder != ExplorationOrder::Bfs) { STORM_LOG_ASSERT(stateRemapping, "Unable to fix columns without mapping."); std::vector const& remapping = stateRemapping.get(); - + // We need to fix the following entities: // (a) the transition matrix // (b) the initial states // (c) the hash map storing the mapping states -> ids // (d) fix remapping for state-generation labels - + // Fix (a). transitionMatrixBuilder.replaceColumns(remapping, 0); @@ -306,59 +311,69 @@ namespace storm { std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } ); std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end()); this->stateStorage.initialStateIndices = std::move(newInitialStateIndices); - + // Fix (c). this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } ); this->generator->remapStateIds([&remapping] (StateType const& state) { return remapping[state]; }); } } - + template storm::storage::sparse::ModelComponents ExplicitModelBuilder::buildModelComponents() { - + // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = generator->isDeterministicModel(); - + // Prepare the component builders storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); std::vector> rewardModelBuilders; for (uint64_t i = 0; i < generator->getNumberOfRewardModels(); ++i) { rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i)); } - ChoiceInformationBuilder choiceInformationBuilder; - boost::optional markovianStates; - - // If we need to build state valuations, initialize them now. - boost::optional stateValuationsBuilder; - if (generator->getOptions().isBuildStateValuationsSet()) { - stateValuationsBuilder = generator->initializeStateValuationsBuilder(); - } - - buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder); + StateAndChoiceInformationBuilder stateAndChoiceInformationBuilder; + stateAndChoiceInformationBuilder.setBuildChoiceLabels(generator->getOptions().isBuildChoiceLabelsSet()); + stateAndChoiceInformationBuilder.setBuildChoiceOrigins(generator->getOptions().isBuildChoiceOriginsSet()); + stateAndChoiceInformationBuilder.setBuildStatePlayerIndications(generator->getModelType() == storm::generator::ModelType::SMG); + stateAndChoiceInformationBuilder.setBuildMarkovianStates(generator->getModelType() == storm::generator::ModelType::MA); + 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(), std::move(markovianStates)); - + storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel()); + + uint_fast64_t numStates = modelComponents.transitionMatrix.getColumnCount(); + uint_fast64_t numChoices = modelComponents.transitionMatrix.getRowCount(); + // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { - modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); + modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(numChoices, modelComponents.transitionMatrix.getColumnCount(), numStates)); + } + // Build the player assignment + if (stateAndChoiceInformationBuilder.isBuildStatePlayerIndications()) { + modelComponents.statePlayerIndications = stateAndChoiceInformationBuilder.buildStatePlayerIndications(numStates); + modelComponents.playerNameToIndexMap = generator->getPlayerNameToIndexMap(); + } + // Build Markovian states + if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) { + modelComponents.markovianStates = stateAndChoiceInformationBuilder.buildMarkovianStates(numStates); } // Build the choice labeling - modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); - + if (stateAndChoiceInformationBuilder.isBuildChoiceLabels()) { + modelComponents.choiceLabeling = stateAndChoiceInformationBuilder.buildChoiceLabeling(numChoices); + } // If requested, build the state valuations and choice origins - if (stateValuationsBuilder) { - modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount()); + if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { + modelComponents.stateValuations = stateAndChoiceInformationBuilder.stateValuationsBuilder().build(numStates); } - if (generator->getOptions().isBuildChoiceOriginsSet()) { - auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); + if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins()) { + auto originData = stateAndChoiceInformationBuilder.buildDataOfChoiceOrigins(numChoices); modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData); } if (generator->isPartiallyObservable()) { - std::vector classes; - classes.resize(stateStorage.getNumberOfStates()); + std::vector classes(stateStorage.getNumberOfStates()); std::unordered_map, uint32_t>>> observationActions; for (auto const& bitVectorIndexPair : stateStorage.stateToId) { uint32_t varObservation = generator->observabilityClass(bitVectorIndexPair.first); @@ -372,12 +387,12 @@ namespace storm { } return modelComponents; } - + template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } - + // Explicitly instantiate the class. template class ExplicitModelBuilder, uint32_t>; template class ExplicitStateLookup; diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 132345075..f33b37ba3 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -43,7 +43,7 @@ namespace storm { // Forward-declare classes. template class RewardModelBuilder; - class ChoiceInformationBuilder; + class StateAndChoiceInformationBuilder; template class ExplicitStateLookup { @@ -127,44 +127,42 @@ namespace storm { * * @param transitionMatrixBuilder The builder of the transition matrix. * @param rewardModelBuilders The builders for the selected reward models. - * @param choiceInformationBuilder The builder for the requested information of the choices - * @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information). - * @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states + * @param stateAndChoiceInformationBuilder The builder for the requested information of the individual states and choices */ - void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional& markovianChoices, boost::optional& stateValuationsBuilder); - + void buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder); + /*! * Explores the state space of the given program and returns the components of the model as a result. * * @return A structure containing the components of the resulting model. */ storm::storage::sparse::ModelComponents buildModelComponents(); - + /*! * Builds the state labeling for the given program. * * @return The state labeling of the given program. */ storm::models::sparse::StateLabeling buildStateLabeling(); - + /// The generator to use for the building process. std::shared_ptr> generator; - + /// The options to be used for the building process. Options options; /// Internal information about the states that were explored. storm::storage::sparse::StateStorage stateStorage; - + /// A set of states that still need to be explored. std::deque> statesToExplore; - + /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be /// built in case the exploration order is not BFS. boost::optional> stateRemapping; }; - + } // namespace adapters } // namespace storm diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.cpp b/src/storm/builder/StateAndChoiceInformationBuilder.cpp new file mode 100644 index 000000000..13d21624a --- /dev/null +++ b/src/storm/builder/StateAndChoiceInformationBuilder.cpp @@ -0,0 +1,121 @@ +#include "storm/builder/StateAndChoiceInformationBuilder.h" + +namespace storm { + namespace builder { + + StateAndChoiceInformationBuilder::StateAndChoiceInformationBuilder() : _buildChoiceLabels(false), _buildChoiceOrigins(false), _buildStatePlayerIndications(false), _buildMarkovianStates(false), _buildStateValuations(false) { + // Intentionally left empty + } + + void StateAndChoiceInformationBuilder::setBuildChoiceLabels(bool value) { + _buildChoiceLabels = value; + } + + bool StateAndChoiceInformationBuilder::isBuildChoiceLabels() const { + return _buildChoiceLabels; + } + + void StateAndChoiceInformationBuilder::addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex) { + STORM_LOG_ASSERT(_buildChoiceLabels, "Building ChoiceLabels was not enabled."); + storm::storage::BitVector& labeledChoices = _choiceLabels[label]; + labeledChoices.grow(choiceIndex + 1, false); + labeledChoices.set(choiceIndex, true); + } + + storm::models::sparse::ChoiceLabeling StateAndChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) { + storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices); + for (auto& label : _choiceLabels) { + label.second.resize(totalNumberOfChoices, false); + result.addLabel(label.first, std::move(label.second)); + } + return result; + } + + void StateAndChoiceInformationBuilder::setBuildChoiceOrigins(bool value) { + _buildChoiceOrigins = value; + } + + bool StateAndChoiceInformationBuilder::isBuildChoiceOrigins() const { + return _buildChoiceOrigins; + } + + void StateAndChoiceInformationBuilder::addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex) { + STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled."); + STORM_LOG_ASSERT(_dataOfChoiceOrigins.size() <= choiceIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order."); + if (_dataOfChoiceOrigins.size() != choiceIndex) { + _dataOfChoiceOrigins.resize(choiceIndex); + } + _dataOfChoiceOrigins.push_back(originData); + } + + std::vector StateAndChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) { + STORM_LOG_ASSERT(_buildChoiceOrigins, "Building ChoiceOrigins was not enabled."); + _dataOfChoiceOrigins.resize(totalNumberOfChoices); + _dataOfChoiceOrigins.shrink_to_fit(); + return std::move(_dataOfChoiceOrigins); + } + + void StateAndChoiceInformationBuilder::setBuildStatePlayerIndications(bool value) { + _buildStatePlayerIndications = value; + } + + bool StateAndChoiceInformationBuilder::isBuildStatePlayerIndications() const { + return _buildStatePlayerIndications; + } + + void StateAndChoiceInformationBuilder::addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex) { + STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled."); + STORM_LOG_ASSERT(_statePlayerIndications.size() <= stateIndex, "Unexpected choice index. Apparently, the choice indices are provided in an incorrect order."); + if (_statePlayerIndications.size() != stateIndex) { + _statePlayerIndications.resize(stateIndex, storm::storage::INVALID_PLAYER_INDEX); + } + _statePlayerIndications.push_back(player); + } + + bool StateAndChoiceInformationBuilder::hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const { + STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled."); + return (stateIndex < _statePlayerIndications.size()) && (_statePlayerIndications[stateIndex] == expectedPlayer); + } + + std::vector StateAndChoiceInformationBuilder::buildStatePlayerIndications(uint_fast64_t totalNumberOfStates) { + STORM_LOG_ASSERT(_buildStatePlayerIndications, "Building StatePlayerIndications was not enabled."); + _statePlayerIndications.resize(totalNumberOfStates, storm::storage::INVALID_PLAYER_INDEX); + _statePlayerIndications.shrink_to_fit(); + return std::move(_statePlayerIndications); + } + + void StateAndChoiceInformationBuilder::setBuildMarkovianStates(bool value) { + _buildMarkovianStates = value; + } + + bool StateAndChoiceInformationBuilder::isBuildMarkovianStates() const { + return _buildMarkovianStates; + } + + void StateAndChoiceInformationBuilder::addMarkovianState(uint_fast64_t markovianStateIndex) { + STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled."); + _markovianStates.grow(markovianStateIndex + 1, false); + _markovianStates.set(markovianStateIndex, true); + } + + storm::storage::BitVector StateAndChoiceInformationBuilder::buildMarkovianStates(uint_fast64_t totalNumberOfStates) { + STORM_LOG_ASSERT(_buildMarkovianStates, "Building MarkovianStates was not enabled."); + _markovianStates.resize(totalNumberOfStates, false); + return _markovianStates; + } + + void StateAndChoiceInformationBuilder::setBuildStateValuations(bool value) { + _buildStateValuations = value; + } + + bool StateAndChoiceInformationBuilder::isBuildStateValuations() const { + return _buildStateValuations; + } + + storm::storage::sparse::StateValuationsBuilder& StateAndChoiceInformationBuilder::stateValuationsBuilder() { + STORM_LOG_ASSERT(_buildStateValuations, "Building StateValuations was not enabled."); + return _stateValuationsBuilder; + } + + } +} diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.h b/src/storm/builder/StateAndChoiceInformationBuilder.h new file mode 100644 index 000000000..413dcd50f --- /dev/null +++ b/src/storm/builder/StateAndChoiceInformationBuilder.h @@ -0,0 +1,75 @@ +#pragma once + +#include +#include +#include +#include +#include + +#include "storm/models/sparse/ChoiceLabeling.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/PlayerIndex.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/storage/prism/Program.h" +#include "storm/storage/sparse/StateValuations.h" + + +namespace storm { + namespace builder { + + /*! + * This class collects information regarding the states and choices during model building. + * It is expected that the provided indices are in ascending order + */ + class StateAndChoiceInformationBuilder { + public: + + StateAndChoiceInformationBuilder(); + + void setBuildChoiceLabels(bool value); + bool isBuildChoiceLabels() const; + void addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex); + storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices); + + void setBuildChoiceOrigins(bool value); + bool isBuildChoiceOrigins() const; + void addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex); + std::vector buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices); + + void setBuildStatePlayerIndications(bool value); + bool isBuildStatePlayerIndications() const; + /*! + * @note: skipped choiceIndices get assigned the invalid player index. + */ + void addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex); + bool hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const; + std::vector buildStatePlayerIndications(uint_fast64_t totalNumberOfStates); + + void setBuildMarkovianStates(bool value); + bool isBuildMarkovianStates() const; + void addMarkovianState(uint_fast64_t markovianStateIndex); + storm::storage::BitVector buildMarkovianStates(uint_fast64_t totalNumberOfStates); + + void setBuildStateValuations(bool value); + bool isBuildStateValuations() const; + storm::storage::sparse::StateValuationsBuilder& stateValuationsBuilder(); + + private: + bool _buildChoiceLabels; + std::unordered_map _choiceLabels; + + bool _buildChoiceOrigins; + std::vector _dataOfChoiceOrigins; + + bool _buildStatePlayerIndications; + std::vector _statePlayerIndications; + + bool _buildMarkovianStates; + storm::storage::BitVector _markovianStates; + + bool _buildStateValuations; + storm::storage::sparse::StateValuationsBuilder _stateValuationsBuilder; + }; + } +} + diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index 5d69c98ab..a0efb04f9 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -3,7 +3,6 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" -#include "storm/builder/ChoiceInformationBuilder.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -81,17 +80,32 @@ namespace storm { labels = newLabels; } } - + template bool Choice::hasLabels() const { return labels.is_initialized(); } - + template std::set const& Choice::getLabels() const { return labels.get(); } - + + template + void Choice::setPlayerIndex(storm::storage::PlayerIndex playerIndex) { + this->playerIndex = playerIndex; + } + + template + bool Choice::hasPlayerIndex() const { + return playerIndex.is_initialized(); + } + + template + storm::storage::PlayerIndex const& Choice::getPlayerIndex() const { + return playerIndex.get(); + } + template void Choice::addOriginData(boost::any const& data) { if (!this->originData || this->originData->empty()) { diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h index 1dbc41760..31842ddee 100644 --- a/src/storm/generator/Choice.h +++ b/src/storm/generator/Choice.h @@ -9,6 +9,7 @@ #include #include "storm/storage/Distribution.h" +#include "storm/storage/PlayerIndex.h" namespace storm { namespace generator { @@ -64,118 +65,140 @@ namespace storm { */ template friend std::ostream& operator<<(std::ostream& out, Choice const& choice); - + /*! * Adds the given label to the labels associated with this choice. * * @param label The label to associate with this choice. */ void addLabel(std::string const& label); - + /*! * Adds the given label set to the labels associated with this choice. * * @param labelSet The label set to associate with this choice. */ void addLabels(std::set const& labels); - + /*! * Returns whether there are labels defined for this choice */ bool hasLabels() const; - + /*! * Retrieves the set of labels associated with this choice. * * @return The set of labels associated with this choice. */ std::set const& getLabels() const; - + + /*! + * Sets the players index + * + * @param The player index associated with this choice. + */ + void setPlayerIndex(storm::storage::PlayerIndex playerIndex); + + /*! + * Returns whether there is an index for the player defined for this choice. + */ + bool hasPlayerIndex() const; + + /*! + * Retrieves the players index associated with this choice + * + * @return The player index associated with this choice. + */ + storm::storage::PlayerIndex const& getPlayerIndex() const; + /*! * Adds the given data that specifies the origin of this choice w.r.t. the model specification */ void addOriginData(boost::any const& data); - + /*! * Returns whether there is origin data defined for this choice */ bool hasOriginData() const; - + /*! * Returns the origin data associated with this choice. */ boost::any const& getOriginData() const; - + /*! * Retrieves the index of the action of this choice. * * @return The index of the action of this choice. */ uint_fast64_t getActionIndex() const; - + /*! * Retrieves the total mass of this choice. * * @return The total mass. */ ValueType getTotalMass() const; - + /*! * Adds the given probability value to the given state in the underlying distribution. */ void addProbability(StateType const& state, ValueType const& value); - + /*! * Adds the given value to the reward associated with this choice. */ void addReward(ValueType const& value); - + /*! * Adds the given choices rewards to this choice. */ void addRewards(std::vector&& values); - + /*! * Retrieves the rewards for this choice under selected reward models. */ std::vector const& getRewards() const; - + /*! * Retrieves whether the choice is Markovian. */ bool isMarkovian() const; - + /*! * Retrieves the size of the distribution associated with this choice. */ std::size_t size() const; - + /*! * If the size is already known, reserves space in the underlying distribution. */ void reserve(std::size_t const& size); - + private: // A flag indicating whether this choice is Markovian or not. bool markovian; // The action index associated with this choice. uint_fast64_t actionIndex; - + // The distribution that is associated with the choice. storm::storage::Distribution distribution; - + // The total probability mass (or rates) of this choice. ValueType totalMass; - + // The reward values associated with this choice. std::vector rewards; - + // The data that stores what part of the model specification induced this choice boost::optional originData; - + // The labels of this choice boost::optional> labels; + + // The playerIndex of this choice + boost::optional playerIndex; }; template diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index b68380935..4112920e4 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -278,6 +278,11 @@ namespace storm { return classId; } + template + std::map NextStateGenerator::getPlayerNameToIndexMap() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Generating player mappings is not supported for this model input format"); + } + template void NextStateGenerator::remapStateIds(std::function const& remapping) { if (overlappingGuardStates != boost::none) { diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 126d0fa5a..eee62412d 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -11,6 +11,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/sparse/ChoiceOrigins.h" #include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/PlayerIndex.h" #include "storm/builder/BuilderOptions.h" #include "storm/builder/RewardModelInformation.h" @@ -24,44 +25,45 @@ namespace storm { namespace generator { typedef storm::builder::BuilderOptions NextStateGeneratorOptions; - + enum class ModelType { DTMC, CTMC, MDP, MA, - POMDP + POMDP, + SMG }; - + template class NextStateGenerator { public: typedef std::function StateToIdCallback; NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options); - + /*! * Creates a new next state generator. This version of the constructor default-constructs the variable information. * Hence, the subclass is responsible for suitably initializing it in its constructor. */ NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options); - + virtual ~NextStateGenerator() = default; - + uint64_t getStateSize() const; virtual ModelType getModelType() const = 0; virtual bool isDeterministicModel() const = 0; virtual bool isDiscreteTimeModel() const = 0; virtual bool isPartiallyObservable() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; - + /// Initializes a builder for state valuations by adding the appropriate variables. virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const; - + void load(CompressedState const& state); virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; bool satisfies(storm::expressions::Expression const& expression) const; - + /// Adds the valuation for the currently loaded state to the given builder virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const; /// Adds the valuation for the currently loaded state @@ -69,10 +71,12 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; - + std::string stateToString(CompressedState const& state) const; uint32_t observabilityClass(CompressedState const& state) const; + + virtual std::map getPlayerNameToIndexMap() const; virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; @@ -88,7 +92,7 @@ namespace storm { * @param remapping The remapping to apply. */ void remapStateIds(std::function const& remapping); - + protected: /*! * Creates the state labeling for the given states using the provided labels and expressions. @@ -109,25 +113,25 @@ namespace storm { virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const; void postprocess(StateBehavior& result); - + /// The options to be used for next-state generation. NextStateGeneratorOptions options; - + /// The expression manager used for evaluating expressions. std::shared_ptr expressionManager; - + /// The expressions that define terminal states. std::vector> terminalStates; - + /// Information about how the variables are packed. VariableInformation variableInformation; - + /// An evaluator used to evaluate expressions. std::unique_ptr> evaluator; - + /// The currently loaded state. CompressedState const* state; - + /// A comparator used to compare constants. storm::utility::ConstantsComparator comparator; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 6bec68bed..ead36e763 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -20,24 +20,24 @@ namespace storm { namespace generator { - + template PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator(program.substituteConstantsFormulas(), options, false) { // Intentionally left empty. } - + template PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(program.getManager(), options), program(program), rewardModels(), hasStateActionRewards(false) { STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program); STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); - + // Only after checking validity of the program, we initialize the variable information. this->checkValid(); this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet()); - + // Create a proper evalator. this->evaluator = std::make_unique>(program.getManager()); - + if (this->options.isBuildAllRewardModelsSet()) { for (auto const& rewardModel : this->program.getRewardModels()) { rewardModels.push_back(rewardModel); @@ -52,19 +52,19 @@ namespace storm { STORM_LOG_THROW(this->program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous."); } } - + // If no reward model was yet added, but there was one that was given in the options, we try to build the // standard reward model. if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) { rewardModels.push_back(this->program.getRewardModel(0)); } } - + // Determine whether any reward model has state action rewards. for (auto const& rewardModel : rewardModels) { hasStateActionRewards |= rewardModel.get().hasStateActionRewards(); } - + // If there are terminal states we need to handle, we now need to translate all labels to expressions. if (this->options.hasTerminalStates()) { for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { @@ -80,6 +80,11 @@ namespace storm { } } } + + if (program.getModelType() == storm::prism::Program::ModelType::SMG) { + moduleIndexToPlayerIndexMap = program.buildModuleIndexToPlayerIndexMap(); + actionIndexToPlayerIndexMap = program.buildActionIndexToPlayerIndexMap(); + } } template @@ -87,7 +92,7 @@ namespace storm { // We can handle all valid prism programs (except for PTAs) return program.getModelType() != storm::prism::Program::ModelType::PTA; } - + template void PrismNextStateGenerator::checkValid() const { // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. @@ -118,7 +123,7 @@ namespace storm { } #endif } - + template ModelType PrismNextStateGenerator::getModelType() const { switch (program.getModelType()) { @@ -127,16 +132,17 @@ namespace storm { case storm::prism::Program::ModelType::MDP: return ModelType::MDP; case storm::prism::Program::ModelType::MA: return ModelType::MA; case storm::prism::Program::ModelType::POMDP: return ModelType::POMDP; + case storm::prism::Program::ModelType::SMG: return ModelType::SMG; default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); } } - + template bool PrismNextStateGenerator::isDeterministicModel() const { return program.isDeterministicModel(); } - + template bool PrismNextStateGenerator::isDiscreteTimeModel() const { return program.isDiscreteTimeModel(); @@ -146,7 +152,7 @@ namespace storm { bool PrismNextStateGenerator::isPartiallyObservable() const { return program.isPartiallyObservable(); } - + template std::vector PrismNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { std::vector initialStateIndices; @@ -162,9 +168,9 @@ namespace storm { currentIntegerValues.emplace_back(0); initialState.setFromInt(variable.bitOffset, variable.bitWidth, 0); } - + initialStateIndices.emplace_back(stateToIdCallback(initialState)); - + bool done = false; while (!done) { bool changedBooleanVariable = false; @@ -177,7 +183,7 @@ namespace storm { initialState.set(booleanVariable.bitOffset, false); } } - + bool changedIntegerVariable = false; if (changedBooleanVariable) { initialStateIndices.emplace_back(stateToIdCallback(initialState)); @@ -191,37 +197,37 @@ namespace storm { currentIntegerValues[integerVariableIndex] = integerVariable.lowerBound; } initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, currentIntegerValues[integerVariableIndex]); - + if (changedIntegerVariable) { break; } } } - + if (changedIntegerVariable) { initialStateIndices.emplace_back(stateToIdCallback(initialState)); } - + done = !changedBooleanVariable && !changedIntegerVariable; } - + STORM_LOG_DEBUG("Enumerated " << initialStateIndices.size() << " initial states using brute force enumeration."); } else { // Prepare an SMT solver to enumerate all initial states. storm::utility::solver::SmtSolverFactory factory; std::unique_ptr solver = factory.create(program.getManager()); - + std::vector rangeExpressions = program.getAllRangeExpressions(); for (auto const& expression : rangeExpressions) { solver->add(expression); } solver->add(program.getInitialStatesExpression()); - + // Proceed ss long as the solver can still enumerate initial states. while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { // Create fresh state. CompressedState initialState(this->variableInformation.getTotalBitOffset(true)); - + // Read variable assignment from the solution of the solver. Also, create an expression we can use to // prevent the variable assignment from being enumerated again. storm::expressions::Expression blockingExpression; @@ -238,29 +244,29 @@ namespace storm { blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); } - + // Register initial state and return it. StateType id = stateToIdCallback(initialState); initialStateIndices.push_back(id); - + // Block the current initial state to search for the next one. if (!blockingExpression.isInitialized()) { break; } solver->add(blockingExpression); } - + STORM_LOG_DEBUG("Enumerated " << initialStateIndices.size() << " initial states using SMT solving."); } - + return initialStateIndices; } - + template StateBehavior PrismNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { // Prepare the result, in case we return early. StateBehavior result; - + // First, construct the state rewards, as we may return early if there are no choices later and we already // need the state rewards then. for (auto const& rewardModel : rewardModels) { @@ -274,7 +280,7 @@ namespace storm { } result.addStateReward(stateRewardValue); } - + // If a terminal expression was set and we must not expand this state, return now. if (!this->terminalStates.empty()) { for (auto const& expressionBool : this->terminalStates) { @@ -286,7 +292,7 @@ namespace storm { // Get all choices for the state. result.setExpanded(); - + std::vector> allChoices; if (this->getOptions().isApplyMaximalProgressAssumptionSet()) { // First explore only edges without a rate @@ -301,15 +307,15 @@ namespace storm { allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); addLabeledChoices(allChoices, *this->state, stateToIdCallback); } - + std::size_t totalNumberOfChoices = allChoices.size(); - + // If there is not a single choice, we return immediately, because the state has no behavior (other than // the state reward). if (totalNumberOfChoices == 0) { return result; } - + // If the model is a deterministic model, we need to fuse the choices into one. if (this->isDeterministicModel() && totalNumberOfChoices > 1) { Choice globalChoice; @@ -317,11 +323,11 @@ namespace storm { if (this->options.isAddOverlappingGuardLabelSet()) { this->overlappingGuardStates->push_back(stateToIdCallback(*this->state)); } - + // For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs // this is equal to the number of choices, which is why we initialize it like this here. ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast(totalNumberOfChoices) : storm::utility::zero(); - + // Iterate over all choices and combine the probabilities/rates into one choice. for (auto const& choice : allChoices) { for (auto const& stateProbabilityPair : choice) { @@ -331,20 +337,20 @@ namespace storm { globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second); } } - + if (hasStateActionRewards && !this->isDiscreteTimeModel()) { totalExitRate += choice.getTotalMass(); } - + if (this->options.isBuildChoiceLabelsSet() && choice.hasLabels()) { globalChoice.addLabels(choice.getLabels()); } - + if (this->options.isBuildChoiceOriginsSet() && choice.hasOriginData()) { globalChoice.addOriginData(choice.getOriginData()); } } - + // Now construct the state-action reward for all selected reward models. for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); @@ -355,41 +361,54 @@ namespace storm { stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); } } - + } } if (hasStateActionRewards) { globalChoice.addReward(stateActionRewardValue / totalExitRate); } } - + // Move the newly fused choice in place. allChoices.clear(); allChoices.push_back(std::move(globalChoice)); } - + + // For SMG we check whether the state has a unique player + if (program.getModelType() == storm::prism::Program::ModelType::SMG && allChoices.size() > 1) { + auto choiceIt = allChoices.begin(); + STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(), "State '" << this->stateToString(*this->state) << "' features a choice without player index."); // This should have been catched while creating the choice already + storm::storage::PlayerIndex statePlayerIndex = choiceIt->getPlayerIndex(); + STORM_LOG_ASSERT(statePlayerIndex != storm::storage::INVALID_PLAYER_INDEX, "State '" << this->stateToString(*this->state) << "' features a choice with invalid player index."); // This should have been catched while creating the choice already + for (++choiceIt; choiceIt != allChoices.end(); ++choiceIt) { + STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(), "State '" << this->stateToString(*this->state) << "' features a choice without player index."); // This should have been catched while creating the choice already + STORM_LOG_ASSERT(choiceIt->getPlayerIndex() != storm::storage::INVALID_PLAYER_INDEX, "State '" << this->stateToString(*this->state) << "' features a choice with invalid player index."); // This should have been catched while creating the choice already + STORM_LOG_THROW(statePlayerIndex == choiceIt->getPlayerIndex(), storm::exceptions::WrongFormatException, "The player for state '" << this->stateToString(*this->state) << "' is not unique. At least one choice is owned by player '" << statePlayerIndex << "' while another is owned by player '" << choiceIt->getPlayerIndex() << "'."); + } + } + // Move all remaining choices in place. for (auto& choice : allChoices) { result.addChoice(std::move(choice)); } this->postprocess(result); - + return result; } - + template CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, storm::prism::Update const& update) { CompressedState newState(state); - + // NOTE: the following process assumes that the assignments of the update are ordered in such a way that the // assignments to boolean variables precede the assignments to all integer variables and that within the // types, the assignments to variables are ordered (in ascending order) by the expression variables. // This is guaranteed for PRISM models, by sorting the assignments as soon as an update is created. - + auto assignmentIt = update.getAssignments().begin(); auto assignmentIte = update.getAssignments().end(); - + // Iterate over all boolean assignments and carry them out. auto boolIt = this->variableInformation.booleanVariables.begin(); for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { @@ -398,7 +417,7 @@ namespace storm { } newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression())); } - + // Iterate over all integer assignments and carry them out. auto integerIt = this->variableInformation.integerVariables.begin(); for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { @@ -417,13 +436,13 @@ namespace storm { newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } - + // Check that we processed all assignments. STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); - + return newState; } - + struct ActiveCommandData { ActiveCommandData(storm::prism::Module const* modulePtr, std::set const* commandIndicesPtr, typename std::set::const_iterator currentCommandIndexIt) : modulePtr(modulePtr), commandIndicesPtr(commandIndicesPtr), currentCommandIndexIt(currentCommandIndexIt) { // Intentionally left empty @@ -432,33 +451,33 @@ namespace storm { std::set const* commandIndicesPtr; typename std::set::const_iterator currentCommandIndexIt; }; - + template boost::optional>>> PrismNextStateGenerator::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter) { - + // First check whether there is at least one enabled command at each module // This avoids evaluating unnecessarily many guards. // If we find one module without an enabled command, we return boost::none. // At the same time, we store pointers to the relevant modules, the relevant command sets and the first enabled command within each set. - + // Iterate over all modules. std::vector activeCommands; for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::prism::Module const& module = program.getModule(i); - + // If the module has no command labeled with the given action, we can skip this module. if (!module.hasActionIndex(actionIndex)) { continue; } - + std::set const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); - + // If the module contains the action, but there is no command in the module that is labeled with // this action, we don't have any feasible command combinations. if (commandIndices.empty()) { return boost::none; } - + // Look up commands by their indices and check if the guard evaluates to true in the given state. bool hasOneEnabledCommand = false; for (auto commandIndexIt = commandIndices.begin(), commandIndexIte = commandIndices.end(); commandIndexIt != commandIndexIte; ++commandIndexIt) { @@ -476,23 +495,23 @@ namespace storm { break; } } - + if (!hasOneEnabledCommand) { return boost::none; } } - + // If we reach this point, there has to be at least one active command for each relevant module. std::vector>> result; // Iterate over all command sets. for (auto const& activeCommand : activeCommands) { std::vector> commands; - + auto commandIndexIt = activeCommand.currentCommandIndexIt; // The command at the current position is already known to be enabled commands.push_back(activeCommand.modulePtr->getCommand(*commandIndexIt)); - + // Look up commands by their indices and add them if the guard evaluates to true in the given state. auto commandIndexIte = activeCommand.commandIndicesPtr->end(); for (++commandIndexIt; commandIndexIt != commandIndexIte; ++commandIndexIt) { @@ -507,29 +526,29 @@ namespace storm { commands.push_back(command); } } - + result.push_back(std::move(commands)); } - + STORM_LOG_ASSERT(!result.empty(), "Expected non-empty list."); return result; } - + template std::vector> PrismNextStateGenerator::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { std::vector> result; - + // Iterate over all modules. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::prism::Module const& module = program.getModule(i); - + // Iterate over all commands. for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { storm::prism::Command const& command = module.getCommand(j); - + // Only consider unlabeled commands. if (command.isLabeled()) continue; - + if (commandFilter != CommandFilter::All) { STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter."); if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) { @@ -541,16 +560,16 @@ namespace storm { if (!this->evaluator->asBool(command.getGuardExpression())) { continue; } - + result.push_back(Choice(command.getActionIndex(), command.isMarkovian())); Choice& choice = result.back(); - + // Remember the choice origin only if we were asked to. if (this->options.isBuildChoiceOriginsSet()) { CommandSet commandIndex { command.getGlobalIndex() }; choice.addOriginData(boost::any(std::move(commandIndex))); } - + // Iterate over all updates of the current command. ValueType probabilitySum = storm::utility::zero(); for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { @@ -561,7 +580,7 @@ namespace storm { // Obtain target state index and add it to the list of known states. If it has not yet been // seen, we also add it to the set of states that have yet to be explored. StateType stateIndex = stateToIdCallback(applyUpdate(state, update)); - + // Update the choice by adding the probability/target state to it. choice.addProbability(stateIndex, probability); if (this->options.isExplorationChecksSet()) { @@ -569,7 +588,7 @@ namespace storm { } } } - + // Create the state-action reward for the newly created choice. for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); @@ -582,24 +601,30 @@ namespace storm { } choice.addReward(stateActionRewardValue); } - + + if (program.getModelType() == storm::prism::Program::ModelType::SMG) { + storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i); + STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command."); + choice.setPlayerIndex(playerOfModule); + } + if (this->options.isExplorationChecksSet()) { // Check that the resulting distribution is in fact a distribution. STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } } } - + return result; } template void PrismNextStateGenerator::generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, std::vector>::const_iterator> const& iteratorList, storm::builder::jit::Distribution& distribution, StateToIdCallback stateToIdCallback) { - + if (storm::utility::isZero(probability)) { return; } - + if (position >= iteratorList.size()) { StateType id = stateToIdCallback(state); distribution.add(id, probability); @@ -611,7 +636,7 @@ namespace storm { } } } - + template void PrismNextStateGenerator::addLabeledChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { @@ -645,6 +670,12 @@ namespace storm { // Now create the actual distribution. Choice& choice = choices.back(); + if (program.getModelType() == storm::prism::Program::ModelType::SMG) { + storm::storage::PlayerIndex const& playerOfAction = actionIndexToPlayerIndexMap.at(actionIndex); + STORM_LOG_THROW(playerOfAction != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Action " << program.getActionName(actionIndex) << " is not owned by any player but has at least one enabled, unlabeled (synchronized) command."); + choice.setPlayerIndex(playerOfAction); + } + // Remember the choice label and origins only if we were asked to. if (this->options.isBuildChoiceLabelsSet()) { choice.addLabel(program.getActionName(actionIndex)); @@ -702,7 +733,12 @@ namespace storm { } } } - + + template + std::map PrismNextStateGenerator::getPlayerNameToIndexMap() const { + return program.getPlayerNameToIndexMapping(); + } + template storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // Gather a vector of labels and their expressions. @@ -720,7 +756,7 @@ namespace storm { } } } - + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); } @@ -741,22 +777,22 @@ namespace storm { std::size_t PrismNextStateGenerator::getNumberOfRewardModels() const { return rewardModels.size(); } - + template storm::builder::RewardModelInformation PrismNextStateGenerator::getRewardModelInformation(uint64_t const& index) const { storm::prism::RewardModel const& rewardModel = rewardModels[index].get(); return storm::builder::RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards()); } - + template std::shared_ptr PrismNextStateGenerator::generateChoiceOrigins(std::vector& dataForChoiceOrigins) const { if (!this->getOptions().isBuildChoiceOriginsSet()) { return nullptr; } - + std::vector identifiers; identifiers.reserve(dataForChoiceOrigins.size()); - + std::map commandSetToIdentifierMap; // The empty commandset (i.e., the choices without origin) always has to get identifier getIdentifierForChoicesWithNoOrigin() -- which is assumed to be 0 STORM_LOG_ASSERT(storm::storage::sparse::ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() == 0, "The no origin identifier is assumed to be zero"); @@ -764,7 +800,7 @@ namespace storm { uint_fast64_t currentIdentifier = 1; for (boost::any& originData : dataForChoiceOrigins) { STORM_LOG_ASSERT(originData.empty() || boost::any_cast(&originData) != nullptr, "Origin data has unexpected type: " << originData.type().name() << "."); - + CommandSet currentCommandSet = originData.empty() ? CommandSet() : boost::any_cast(std::move(originData)); auto insertionRes = commandSetToIdentifierMap.insert(std::make_pair(std::move(currentCommandSet), currentIdentifier)); identifiers.push_back(insertionRes.first->second); @@ -772,16 +808,16 @@ namespace storm { ++currentIdentifier; } } - + std::vector identifierToCommandSetMapping(currentIdentifier); for (auto const& setIdPair : commandSetToIdentifierMap) { identifierToCommandSetMapping[setIdPair.second] = setIdPair.first; } - + return std::make_shared(std::make_shared(program), std::move(identifiers), std::move(identifierToCommandSetMapping)); } - + template class PrismNextStateGenerator; #ifdef STORM_HAVE_CARL diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index e302fd02e..e8a7a81ff 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -42,7 +42,8 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - + virtual std::map getPlayerNameToIndexMap() const override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; @@ -111,17 +112,21 @@ namespace storm { * A recursive helper function to generate a synchronziing distribution. */ void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, std::vector>::const_iterator> const& iteratorList, storm::builder::jit::Distribution& distribution, StateToIdCallback stateToIdCallback); - + // The program used for the generation of next states. storm::prism::Program program; - + // The reward models that need to be considered. std::vector> rewardModels; - + // A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; + + // Mappings from module/action indices to the programs players + std::vector moduleIndexToPlayerIndexMap; + std::map actionIndexToPlayerIndexMap; }; - + } } diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index cb24e7d8b..1d751bb2e 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -76,30 +76,35 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); } } - + boost::any CloneVisitor::visit(TimeOperatorFormula 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(GloballyFormula 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(GameFormula 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.getCoalition(), subformula)); + } + boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(LongRunAverageOperatorFormula 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(LongRunAverageRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { std::vector> subformulas; for(auto const& subF : f.getSubformulas()){ diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h index 4b1d620ee..5ff29e816 100644 --- a/src/storm/logic/CloneVisitor.h +++ b/src/storm/logic/CloneVisitor.h @@ -22,6 +22,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const override; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp index 58970c77b..d8b399e34 100644 --- a/src/storm/logic/Formula.cpp +++ b/src/storm/logic/Formula.cpp @@ -14,313 +14,317 @@ namespace storm { bool Formula::isPathFormula() const { return false; } - + bool Formula::isStateFormula() const { return false; } - + bool Formula::isMultiObjectiveFormula() const { return false; } - + bool Formula::isQuantileFormula() const { return false; } - + bool Formula::isBinaryStateFormula() const { return false; } - + bool Formula::isUnaryStateFormula() const { return false; } - + bool Formula::isBinaryBooleanStateFormula() const { return false; } - + bool Formula::isUnaryBooleanStateFormula() const { return false; } - + bool Formula::isBooleanLiteralFormula() const { return false; } - + bool Formula::isTrueFormula() const { return false; } - + bool Formula::isFalseFormula() const { return false; } - + bool Formula::isAtomicExpressionFormula() const { return false; } - + bool Formula::isAtomicLabelFormula() const { return false; } - + bool Formula::isUntilFormula() const { return false; } - + bool Formula::isBoundedUntilFormula() const { return false; } - + bool Formula::isEventuallyFormula() const { return false; } - + bool Formula::isReachabilityProbabilityFormula() const { return false; } - + bool Formula::isGloballyFormula() const { return false; } - + bool Formula::isBinaryPathFormula() const { return false; } - + bool Formula::isUnaryPathFormula() const { return false; } - + bool Formula::isConditionalProbabilityFormula() const { return false; } - + bool Formula::isConditionalRewardFormula() const { return false; } - + bool Formula::isProbabilityPathFormula() const { return false; } - + bool Formula::isRewardPathFormula() const { return false; } - + bool Formula::isTimePathFormula() const { return false; } - + bool Formula::isNextFormula() const { return false; } - + bool Formula::isLongRunAverageOperatorFormula() const { return false; } - + bool Formula::isTimeOperatorFormula() const { return false; } - + bool Formula::isCumulativeRewardFormula() const { return false; } - + bool Formula::isInstantaneousRewardFormula() const { return false; } - + bool Formula::isReachabilityRewardFormula() const { return false; } - + bool Formula::isLongRunAverageRewardFormula() const { return false; } - + bool Formula::isTotalRewardFormula() const { return false; } - + bool Formula::isReachabilityTimeFormula() const { return false; } - + + bool Formula::isGameFormula() const { + return false; + } + bool Formula::isProbabilityOperatorFormula() const { return false; } - + bool Formula::isRewardOperatorFormula() const { return false; } - + bool Formula::isOperatorFormula() const { return false; } - + bool Formula::hasQualitativeResult() const { return true; } - + bool Formula::hasQuantitativeResult() const { return false; } - + bool Formula::isInFragment(FragmentSpecification const& fragment) const { FragmentChecker checker; return checker.conformsToSpecification(*this, fragment); } - + FormulaInformation Formula::info() const { FormulaInformationVisitor visitor; return visitor.getInformation(*this); } - + std::shared_ptr Formula::getTrueFormula() { return std::shared_ptr(new BooleanLiteralFormula(true)); } - + bool Formula::isInitialFormula() const { return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init"; } - + PathFormula& Formula::asPathFormula() { return dynamic_cast(*this); } - + PathFormula const& Formula::asPathFormula() const { return dynamic_cast(*this); } - + StateFormula& Formula::asStateFormula() { return dynamic_cast(*this); } - + StateFormula const& Formula::asStateFormula() const { return dynamic_cast(*this); } - + MultiObjectiveFormula& Formula::asMultiObjectiveFormula() { return dynamic_cast(*this); } - + MultiObjectiveFormula const& Formula::asMultiObjectiveFormula() const { return dynamic_cast(*this); } - + QuantileFormula& Formula::asQuantileFormula() { return dynamic_cast(*this); } - + QuantileFormula const& Formula::asQuantileFormula() const { return dynamic_cast(*this); } - + BinaryStateFormula& Formula::asBinaryStateFormula() { return dynamic_cast(*this); } - + BinaryStateFormula const& Formula::asBinaryStateFormula() const { return dynamic_cast(*this); } - + UnaryStateFormula& Formula::asUnaryStateFormula() { return dynamic_cast(*this); } - + UnaryStateFormula const& Formula::asUnaryStateFormula() const { return dynamic_cast(*this); } - + ConditionalFormula& Formula::asConditionalFormula() { return dynamic_cast(*this); } - + ConditionalFormula const& Formula::asConditionalFormula() const { return dynamic_cast(*this); } - + BinaryBooleanStateFormula& Formula::asBinaryBooleanStateFormula() { return dynamic_cast(*this); } - + BinaryBooleanStateFormula const& Formula::asBinaryBooleanStateFormula() const { return dynamic_cast(*this); } - + UnaryBooleanStateFormula& Formula::asUnaryBooleanStateFormula() { return dynamic_cast(*this); } - + UnaryBooleanStateFormula const& Formula::asUnaryBooleanStateFormula() const { return dynamic_cast(*this); } - + BooleanLiteralFormula& Formula::asBooleanLiteralFormula() { return dynamic_cast(*this); } - + BooleanLiteralFormula const& Formula::asBooleanLiteralFormula() const { return dynamic_cast(*this); } - + AtomicExpressionFormula& Formula::asAtomicExpressionFormula() { return dynamic_cast(*this); } - + AtomicExpressionFormula const& Formula::asAtomicExpressionFormula() const { return dynamic_cast(*this); } - + AtomicLabelFormula& Formula::asAtomicLabelFormula() { return dynamic_cast(*this); } - + AtomicLabelFormula const& Formula::asAtomicLabelFormula() const { return dynamic_cast(*this); } - + UntilFormula& Formula::asUntilFormula() { return dynamic_cast(*this); } - + UntilFormula const& Formula::asUntilFormula() const { return dynamic_cast(*this); } - + BoundedUntilFormula& Formula::asBoundedUntilFormula() { return dynamic_cast(*this); } - + BoundedUntilFormula const& Formula::asBoundedUntilFormula() const { return dynamic_cast(*this); } - + EventuallyFormula& Formula::asEventuallyFormula() { return dynamic_cast(*this); } - + EventuallyFormula const& Formula::asEventuallyFormula() const { return dynamic_cast(*this); } - + EventuallyFormula& Formula::asReachabilityRewardFormula() { return dynamic_cast(*this); } - + EventuallyFormula const& Formula::asReachabilityRewardFormula() const { return dynamic_cast(*this); } - + EventuallyFormula& Formula::asReachabilityProbabilityFormula() { return dynamic_cast(*this); } - + EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const { return dynamic_cast(*this); } - + EventuallyFormula& Formula::asReachabilityTimeFormula() { return dynamic_cast(*this); } @@ -328,160 +332,168 @@ namespace storm { EventuallyFormula const& Formula::asReachabilityTimeFormula() const { return dynamic_cast(*this); } - + + GameFormula& Formula::asGameFormula() { + return dynamic_cast(*this); + } + + GameFormula const& Formula::asGameFormula() const { + return dynamic_cast(*this); + } + GloballyFormula& Formula::asGloballyFormula() { return dynamic_cast(*this); } - + GloballyFormula const& Formula::asGloballyFormula() const { return dynamic_cast(*this); } - + BinaryPathFormula& Formula::asBinaryPathFormula() { return dynamic_cast(*this); } - + BinaryPathFormula const& Formula::asBinaryPathFormula() const { return dynamic_cast(*this); } - + UnaryPathFormula& Formula::asUnaryPathFormula() { return dynamic_cast(*this); } - + UnaryPathFormula const& Formula::asUnaryPathFormula() const { return dynamic_cast(*this); } - + NextFormula& Formula::asNextFormula() { return dynamic_cast(*this); } - + NextFormula const& Formula::asNextFormula() const { return dynamic_cast(*this); } - + LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() { return dynamic_cast(*this); } - + LongRunAverageOperatorFormula const& Formula::asLongRunAverageOperatorFormula() const { return dynamic_cast(*this); } - + TimeOperatorFormula& Formula::asTimeOperatorFormula() { return dynamic_cast(*this); } - + TimeOperatorFormula const& Formula::asTimeOperatorFormula() const { return dynamic_cast(*this); } - + CumulativeRewardFormula& Formula::asCumulativeRewardFormula() { return dynamic_cast(*this); } - + CumulativeRewardFormula const& Formula::asCumulativeRewardFormula() const { return dynamic_cast(*this); } - + TotalRewardFormula& Formula::asTotalRewardFormula() { return dynamic_cast(*this); } - + TotalRewardFormula const& Formula::asTotalRewardFormula() const { return dynamic_cast(*this); } - + InstantaneousRewardFormula& Formula::asInstantaneousRewardFormula() { return dynamic_cast(*this); } - + InstantaneousRewardFormula const& Formula::asInstantaneousRewardFormula() const { return dynamic_cast(*this); } - + LongRunAverageRewardFormula& Formula::asLongRunAverageRewardFormula() { return dynamic_cast(*this); } - + LongRunAverageRewardFormula const& Formula::asLongRunAverageRewardFormula() const { return dynamic_cast(*this); } - + ProbabilityOperatorFormula& Formula::asProbabilityOperatorFormula() { return dynamic_cast(*this); } - + ProbabilityOperatorFormula const& Formula::asProbabilityOperatorFormula() const { return dynamic_cast(*this); } - + RewardOperatorFormula& Formula::asRewardOperatorFormula() { return dynamic_cast(*this); } - + RewardOperatorFormula const& Formula::asRewardOperatorFormula() const { return dynamic_cast(*this); } - + OperatorFormula& Formula::asOperatorFormula() { return dynamic_cast(*this); } - + OperatorFormula const& Formula::asOperatorFormula() const { return dynamic_cast(*this); } - + std::vector> Formula::getAtomicExpressionFormulas() const { std::vector> result; this->gatherAtomicExpressionFormulas(result); return result; } - + std::vector> Formula::getAtomicLabelFormulas() const { std::vector> result; this->gatherAtomicLabelFormulas(result); return result; } - + std::set Formula::getUsedVariables() const { std::set usedVariables; this->gatherUsedVariables(usedVariables); return usedVariables; } - + std::set Formula::getReferencedRewardModels() const { std::set referencedRewardModels; this->gatherReferencedRewardModels(referencedRewardModels); return referencedRewardModels; } - + std::shared_ptr Formula::substitute(std::map const& substitution) const { storm::expressions::JaniExpressionSubstitutionVisitor> v(substitution); return substitute([&v](storm::expressions::Expression const& exp) {return v.substitute(exp);}); } - + std::shared_ptr Formula::substitute(std::function const& expressionSubstitution) const { ExpressionSubstitutionVisitor visitor; return visitor.substitute(*this, expressionSubstitution); } - + std::shared_ptr Formula::substitute(std::map const& labelSubstitution) const { LabelSubstitutionVisitor visitor(labelSubstitution); return visitor.substitute(*this); } - + std::shared_ptr Formula::substitute(std::map const& labelSubstitution) const { LabelSubstitutionVisitor visitor(labelSubstitution); return visitor.substitute(*this); } - + std::shared_ptr Formula::substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { RewardModelNameSubstitutionVisitor visitor(rewardModelNameSubstitution); return visitor.substitute(*this); } - + storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map const& labelToExpressionMapping) const { ToExpressionVisitor visitor; if (labelToExpressionMapping.empty()) { @@ -490,37 +502,37 @@ namespace storm { return visitor.toExpression(*this->substitute(labelToExpressionMapping), manager); } } - + std::shared_ptr Formula::asSharedPointer() { return this->shared_from_this(); } - + std::shared_ptr Formula::asSharedPointer() const { return this->shared_from_this(); } - + void Formula::gatherAtomicExpressionFormulas(std::vector>&) const { return; } - + void Formula::gatherAtomicLabelFormulas(std::vector>&) const { return; } - + void Formula::gatherReferencedRewardModels(std::set&) const { return; } - + void Formula::gatherUsedVariables(std::set& usedVariables) const { return; } - + std::string Formula::toString() const { std::stringstream str2; writeToStream(str2); return str2.str(); } - + std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h index dc6396e71..294637c2e 100644 --- a/src/storm/logic/Formula.h +++ b/src/storm/logic/Formula.h @@ -78,10 +78,13 @@ namespace storm { virtual bool isReachabilityRewardFormula() const; virtual bool isLongRunAverageRewardFormula() const; virtual bool isTotalRewardFormula() const; - + // Expected time formulas. virtual bool isReachabilityTimeFormula() const; - + + // Game formulas. + virtual bool isGameFormula() const; + // Type checks for abstract intermediate classes. virtual bool isBinaryPathFormula() const; virtual bool isBinaryStateFormula() const; @@ -151,7 +154,10 @@ namespace storm { EventuallyFormula& asReachabilityTimeFormula(); EventuallyFormula const& asReachabilityTimeFormula() const; - + + GameFormula& asGameFormula(); + GameFormula const& asGameFormula() const; + GloballyFormula& asGloballyFormula(); GloballyFormula const& asGloballyFormula() const; diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index e4e9a15ed..41976aa57 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -60,36 +60,40 @@ namespace storm { } return result; } - + boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + + boost::any FormulaInformationVisitor::visit(GameFormula const& f, boost::any const& data) const { + return f.getSubformula().accept(*this, data); + } + boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { return FormulaInformation(); } - + boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { FormulaInformation result; result.setContainsLongRunFormula(true); result.join(boost::any_cast(f.getSubformula().accept(*this, data))); return result; } - + boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { FormulaInformation result; result.setContainsLongRunFormula(true); return result; } - + boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { FormulaInformation result; for(auto const& subF : f.getSubformulas()){ diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h index 7ba8b70b9..617386961 100644 --- a/src/storm/logic/FormulaInformationVisitor.h +++ b/src/storm/logic/FormulaInformationVisitor.h @@ -21,6 +21,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const override; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h index 1eaf6791d..6bf5b8c50 100644 --- a/src/storm/logic/FormulaVisitor.h +++ b/src/storm/logic/FormulaVisitor.h @@ -22,6 +22,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0; diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h index bdda5c863..f054794e7 100644 --- a/src/storm/logic/Formulas.h +++ b/src/storm/logic/Formulas.h @@ -8,6 +8,7 @@ #include "storm/logic/BoundedUntilFormula.h" #include "storm/logic/CumulativeRewardFormula.h" #include "storm/logic/EventuallyFormula.h" +#include "storm/logic/GameFormula.h" #include "storm/logic/GloballyFormula.h" #include "storm/logic/InstantaneousRewardFormula.h" #include "storm/logic/NextFormula.h" diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index 170316fc7..2d1661418 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/src/storm/logic/FormulasForwardDeclarations.h @@ -17,6 +17,7 @@ namespace storm { class EventuallyFormula; class TimeOperatorFormula; class GloballyFormula; + class GameFormula; class InstantaneousRewardFormula; class LongRunAverageOperatorFormula; class LongRunAverageRewardFormula; diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index b669e75bd..94da18e87 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -188,12 +188,18 @@ namespace storm { result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; } - + + boost::any FragmentChecker::visit(GameFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + bool result = inherited.getSpecification().areGameFormulasAllowed(); + return result && boost::any_cast(f.getSubformula().accept(*this, data)); + } + boost::any FragmentChecker::visit(InstantaneousRewardFormula const&, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); return inherited.getSpecification().areInstantaneousRewardFormulasAllowed(); } - + boost::any FragmentChecker::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed(); diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h index 485a205aa..c6e6100ee 100644 --- a/src/storm/logic/FragmentChecker.h +++ b/src/storm/logic/FragmentChecker.h @@ -22,6 +22,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const override; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9405a3841..9fd7353b9 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -41,21 +41,34 @@ namespace storm { pctl.setBoundedUntilFormulasAllowed(true); pctl.setStepBoundedUntilFormulasAllowed(true); pctl.setTimeBoundedUntilFormulasAllowed(true); - + return pctl; } - + FragmentSpecification flatPctl() { FragmentSpecification flatPctl = pctl(); - + flatPctl.setNestedOperatorsAllowed(false); - + return flatPctl; } - + + FragmentSpecification rpatl() { + FragmentSpecification rpatl = propositional(); + + // TODO: Only allow OperatorFormulas when they are inside of a GameFormula? + // TODO: Require that operator formulas are required at the top level of a GameFormula? + rpatl.setGameFormulasAllowed(true); + rpatl.setRewardOperatorsAllowed(true); + rpatl.setLongRunAverageRewardFormulasAllowed(true); + rpatl.setLongRunAverageOperatorsAllowed(true); + + return rpatl; + } + FragmentSpecification prctl() { FragmentSpecification prctl = pctl(); - + prctl.setRewardOperatorsAllowed(true); prctl.setCumulativeRewardFormulasAllowed(true); prctl.setInstantaneousFormulasAllowed(true); @@ -166,6 +179,8 @@ namespace storm { reachabilityTimeFormula = false; + gameFormula = false; + nestedOperators = true; nestedPathFormulas = false; nestedMultiObjectiveFormulas = false; @@ -614,12 +629,20 @@ namespace storm { bool FragmentSpecification::isRewardAccumulationAllowed() const { return rewardAccumulation; } - + FragmentSpecification& FragmentSpecification::setRewardAccumulationAllowed(bool newValue) { rewardAccumulation = newValue; return *this; } - + bool FragmentSpecification::areGameFormulasAllowed() const { + return gameFormula; + } + + FragmentSpecification& FragmentSpecification::setGameFormulasAllowed(bool newValue) { + gameFormula = newValue; + return *this; + } + } } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index aa48c0738..19cf232ed 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -93,105 +93,109 @@ namespace storm { bool areNestedOperatorsAllowed() const; FragmentSpecification& setNestedOperatorsAllowed(bool newValue); - + bool areNestedPathFormulasAllowed() const; FragmentSpecification& setNestedPathFormulasAllowed(bool newValue); - + bool areNestedMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue); - + bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue); - + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); bool areStepBoundedUntilFormulasAllowed() const; FragmentSpecification& setStepBoundedUntilFormulasAllowed(bool newValue); - + bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); bool areRewardBoundedUntilFormulasAllowed() const; FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); - + bool areMultiDimensionalBoundedUntilFormulasAllowed() const; FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); - + bool areStepBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue); - + bool areTimeBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue); bool areRewardBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue); - + bool areMultiDimensionalCumulativeRewardFormulasAllowed() const; FragmentSpecification& setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue); - + bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); - + bool areQuantitativeOperatorResultsAllowed() const; FragmentSpecification& setQuantitativeOperatorResultsAllowed(bool newValue); bool areQualitativeOperatorResultsAllowed() const; FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue); - + bool isOperatorAtTopLevelRequired() const; FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue); - + bool isMultiObjectiveFormulaAtTopLevelRequired() const; FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue); - + bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const; FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue); - + bool isQuantileFormulaAtTopLevelRequired() const; FragmentSpecification& setQuantileFormulaAtTopLevelRequired(bool newValue); - + bool isRewardAccumulationAllowed() const; FragmentSpecification& setRewardAccumulationAllowed(bool newValue); + bool areGameFormulasAllowed() const; + FragmentSpecification& setGameFormulasAllowed(bool newValue); FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); - + private: // Flags that indicate whether it is legal to see such a formula. bool probabilityOperator; bool rewardOperator; bool expectedTimeOperator; bool longRunAverageOperator; - + bool multiObjectiveFormula; bool quantileFormula; - + bool globallyFormula; bool reachabilityProbabilityFormula; bool nextFormula; bool untilFormula; bool boundedUntilFormula; - + bool atomicExpressionFormula; bool atomicLabelFormula; bool booleanLiteralFormula; bool unaryBooleanStateFormula; bool binaryBooleanStateFormula; - + bool cumulativeRewardFormula; bool instantaneousRewardFormula; bool reachabilityRewardFormula; bool longRunAverageRewardFormula; bool totalRewardFormula; - + bool conditionalProbabilityFormula; bool conditionalRewardFormula; - + bool reachabilityTimeFormula; - + + bool gameFormula; + // Members that indicate certain restrictions. bool nestedOperators; bool nestedPathFormulas; @@ -228,7 +232,10 @@ namespace storm { // Flat PCTL. FragmentSpecification flatPctl(); - + + // rPATL for SMGs + FragmentSpecification rpatl(); + // PCTL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctl(); diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp new file mode 100644 index 000000000..64fdc60b8 --- /dev/null +++ b/src/storm/logic/GameFormula.cpp @@ -0,0 +1,37 @@ +#include "storm/logic/GameFormula.h" + +#include "storm/logic/FormulaVisitor.h" + +namespace storm { + namespace logic { + GameFormula::GameFormula(PlayerCoalition const& coalition, std::shared_ptr subformula) : UnaryStateFormula(subformula), coalition(coalition) { + // Intentionally left empty. + } + + bool GameFormula::isGameFormula() const { + return true; + } + + bool GameFormula::hasQualitativeResult() const { + return this->getSubformula().hasQualitativeResult(); + } + + bool GameFormula::hasQuantitativeResult() const { + return this->getSubformula().hasQuantitativeResult(); + } + + PlayerCoalition const& GameFormula::getCoalition() const { + return coalition; + } + + boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + std::ostream& GameFormula::writeToStream(std::ostream& out) const { + out << "<<" << coalition << ">> "; + this->getSubformula().writeToStream(out); + return out; + } + } +} diff --git a/src/storm/logic/GameFormula.h b/src/storm/logic/GameFormula.h new file mode 100644 index 000000000..bc57583eb --- /dev/null +++ b/src/storm/logic/GameFormula.h @@ -0,0 +1,33 @@ +#ifndef STORM_LOGIC_GAMEFORMULA_H_ +#define STORM_LOGIC_GAMEFORMULA_H_ + +#include "storm/logic/UnaryStateFormula.h" +#include "storm/logic/PlayerCoalition.h" +#include + +namespace storm { + namespace logic { + class GameFormula : public UnaryStateFormula { + public: + GameFormula(PlayerCoalition const& coalition, std::shared_ptr subFormula); + + virtual ~GameFormula() { + // Intentionally left empty. + } + + PlayerCoalition const& getCoalition() const; + 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; + + private: + PlayerCoalition coalition; + }; + } +} + +#endif /* STORM_LOGIC_GAMEFORMULA_H_ */ diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index 99eeb444b..22ff54cdd 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -62,31 +62,37 @@ namespace storm { } return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(GloballyFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + + boost::any LiftableTransitionRewardsVisitor::visit(GameFormula const& f, boost::any const& data) const { + STORM_LOG_WARN("Transitionbranch-based rewards might be reduced to action-based rewards. Be sure that this is correct for your property."); + // TODO: Check if this is correct + return f.getSubformula().accept(*this, data); + } + boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this, data); } - + boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { return true; } - + boost::any LiftableTransitionRewardsVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { bool result = true; for (auto const& subF : f.getSubformulas()){ diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h index c09f9c25b..bbac6b7c2 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.h +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h @@ -28,6 +28,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const override; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/logic/PlayerCoalition.cpp b/src/storm/logic/PlayerCoalition.cpp new file mode 100644 index 000000000..e744fbe1c --- /dev/null +++ b/src/storm/logic/PlayerCoalition.cpp @@ -0,0 +1,23 @@ +#include "storm/logic/PlayerCoalition.h" + +namespace storm { + namespace logic { + + PlayerCoalition::PlayerCoalition(std::vector> playerIds) : _playerIds(playerIds) { + // Intentionally left empty. + } + + std::vector> const& PlayerCoalition::getPlayers() const { + return _playerIds; + } + + std::ostream& operator<<(std::ostream& stream, PlayerCoalition const& coalition) { + bool firstItem = true; + for (auto const& id : coalition._playerIds) { + if (firstItem) { firstItem = false; } else { stream << ","; } + stream << id; + } + return stream; + } + } +} diff --git a/src/storm/logic/PlayerCoalition.h b/src/storm/logic/PlayerCoalition.h new file mode 100644 index 000000000..0ddebba34 --- /dev/null +++ b/src/storm/logic/PlayerCoalition.h @@ -0,0 +1,26 @@ +#pragma once + +#include +#include + +#include +#include "storm/storage/PlayerIndex.h" + +namespace storm { + namespace logic { + + class PlayerCoalition { + public: + PlayerCoalition() = default; + PlayerCoalition(std::vector> playerIds); + PlayerCoalition(PlayerCoalition const& other) = default; + + std::vector> const& getPlayers() const; + + friend std::ostream& operator<<(std::ostream& stream, PlayerCoalition const& playerCoalition); + + private: + std::vector> _playerIds; + }; + } +} diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp index 27ea1fa6b..8eb8444fc 100644 --- a/src/storm/logic/ToExpressionVisitor.cpp +++ b/src/storm/logic/ToExpressionVisitor.cpp @@ -46,67 +46,71 @@ namespace storm { } return result; } - + boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(ConditionalFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(EventuallyFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(TimeOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(GloballyFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + + boost::any ToExpressionVisitor::visit(GameFormula const&, boost::any const&) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(QuantileFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(NextFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(RewardOperatorFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } - + boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { storm::expressions::Expression subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); switch (f.getOperator()) { diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h index 345698f5a..675dbbcba 100644 --- a/src/storm/logic/ToExpressionVisitor.h +++ b/src/storm/logic/ToExpressionVisitor.h @@ -22,6 +22,7 @@ namespace storm { virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(GameFormula const& f, boost::any const& data) const override; virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 67f03bc9a..3704215d4 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -15,6 +15,7 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Pomdp.h" +#include "storm/models/sparse/Smg.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" @@ -199,6 +200,8 @@ namespace storm { return this->checkAtomicLabelFormula(env, checkTask.substituteFormula(stateFormula.asAtomicLabelFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula())); + } else if (stateFormula.isGameFormula()) { + return this->checkGameFormula(env, checkTask.substituteFormula(stateFormula.asGameFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } @@ -321,6 +324,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); } + template + std::unique_ptr AbstractModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << "."); + } + /////////////////////////////////////////////// // Explicitly instantiate the template class. /////////////////////////////////////////////// @@ -331,9 +339,11 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; #ifdef STORM_HAVE_CARL template class AbstractModelChecker>>; + template class AbstractModelChecker>>; template class AbstractModelChecker>; template class AbstractModelChecker>; @@ -341,12 +351,14 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; #endif // DD template class AbstractModelChecker>; diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 80bf18fb6..59149711c 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -88,13 +88,15 @@ namespace storm { virtual std::unique_ptr checkTimeOperatorFormula(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask); virtual std::unique_ptr checkUnaryBooleanStateFormula(Environment const& env, CheckTask const& checkTask); - + // The methods to check multi-objective formulas. virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask); - + // The methods to check quantile formulas. virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask); - + + // The methods to check game formulas. + virtual std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask); }; } } diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 898795fda..6598d5a85 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -9,6 +9,7 @@ #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" +#include "storm/logic/PlayerCoalition.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/exceptions/InvalidOperationException.h" @@ -51,7 +52,7 @@ namespace storm { */ template CheckTask substituteFormula(NewFormulaType const& newFormula) const { - CheckTask result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); + CheckTask result(newFormula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); result.updateOperatorInformation(); return result; } @@ -104,7 +105,7 @@ namespace storm { */ template CheckTask convertValueType() const { - return CheckTask(this->formula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); + return CheckTask(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); } /*! @@ -135,6 +136,28 @@ namespace storm { optimizationDirection = dir; } + /*! + * Retrieves whether a player coalition was set. + */ + bool isPlayerCoalitionSet() const { + return static_cast(playerCoalition); + } + + /*! + * Retrieves the player coalition (if set). + */ + storm::logic::PlayerCoalition const& getPlayerCoalition() const { + return playerCoalition.get(); + } + + /*! + * Sets the player coalition. + */ + CheckTask& setPlayerCoalition(storm::logic::PlayerCoalition const& coalition) { + playerCoalition = coalition; + return *this; + } + /*! * Retrieves whether a reward model was set. */ @@ -261,6 +284,7 @@ namespace storm { * * @param formula The formula to attach to the task. * @param optimizationDirection If set, the probabilities will be minimized/maximized. + * @param playerCoalition If set, the given coalitions of players will be assumed. * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values * for the initial states. @@ -270,7 +294,7 @@ namespace storm { * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional playerCoalition, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint) : formula(formula), optimizationDirection(optimizationDirection), playerCoalition(playerCoalition), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) { // Intentionally left empty. } @@ -279,6 +303,9 @@ namespace storm { // If set, the probabilities will be minimized/maximized. boost::optional optimizationDirection; + + // If set, the given coalitions of players will be assumed. + boost::optional playerCoalition; // If set, the reward property has to be interpreted over this model. boost::optional rewardModel; diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index cbd135612..a7bc77b77 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -8,6 +8,7 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Smg.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -22,13 +23,13 @@ namespace storm { SparsePropositionalModelChecker::SparsePropositionalModelChecker(SparseModelType const& model) : model(model) { // Intentionally left empty. } - + template bool SparsePropositionalModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::propositional()); } - + template std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); @@ -38,19 +39,19 @@ namespace storm { return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); } } - + template std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); } - + template SparseModelType const& SparsePropositionalModelChecker::getModel() const { return model; } - + // Explicitly instantiate the template class. template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; @@ -58,9 +59,11 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; - + template class SparsePropositionalModelChecker>; + #ifdef STORM_HAVE_CARL template class SparsePropositionalModelChecker>>; + template class SparsePropositionalModelChecker>>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; @@ -68,12 +71,14 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; + template class SparsePropositionalModelChecker>; #endif } } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp new file mode 100644 index 000000000..6c42b3e30 --- /dev/null +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -0,0 +1,76 @@ +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" + +#include +#include + +#include "storm/utility/macros.h" +#include "storm/utility/FilteredRewardModel.h" + +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" + +#include "storm/logic/FragmentSpecification.h" + +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + template + SparseSmgRpatlModelChecker::SparseSmgRpatlModelChecker(SparseSmgModelType const& model) : SparsePropositionalModelChecker(model) { + // Intentionally left empty. + } + + template + bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { + storm::logic::Formula const& formula = checkTask.getFormula(); + + return formula.isInFragment(storm::logic::rpatl()); + } + + template + bool SparseSmgRpatlModelChecker::canHandle(CheckTask const& checkTask) const { + bool requiresSingleInitialState = false; + if (canHandleStatic(checkTask, &requiresSingleInitialState)) { + return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1; + } else { + return false; + } + } + + 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())); + } + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Only game formulas with Operatorformulas as subformula are supported."); + } + + template + std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not implemented."); + } + + 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."); + } + + template class SparseSmgRpatlModelChecker>; +#ifdef STORM_HAVE_CARL + template class SparseSmgRpatlModelChecker>; +#endif + } +} diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h new file mode 100644 index 000000000..abf3243a5 --- /dev/null +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -0,0 +1,37 @@ +#ifndef STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ +#define STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ + +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/models/sparse/Smg.h" +#include "storm/utility/solver.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/storage/StronglyConnectedComponent.h" + +namespace storm { + namespace modelchecker { + + template + class SparseSmgRpatlModelChecker : public SparsePropositionalModelChecker { + public: + typedef typename SparseSmgModelType::ValueType ValueType; + typedef typename SparseSmgModelType::RewardModelType RewardModelType; + + explicit SparseSmgRpatlModelChecker(SparseSmgModelType const& model); + + /*! + * Returns false, if this task can certainly not be handled by this model checker (independent of the concrete model). + * @param requiresSingleInitialState if not nullptr, this flag is set to true iff checking this formula requires a model with a single initial state + */ + static bool canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState = nullptr); + + // The implemented methods of the AbstractModelChecker interface. + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + }; + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_SPARSESMGRPATLMODELCHECKER_H_ */ diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp index d556448bb..4da6d9e77 100644 --- a/src/storm/models/ModelType.cpp +++ b/src/storm/models/ModelType.cpp @@ -19,6 +19,8 @@ namespace storm { return ModelType::S2pg; } else if (type == "POMDP") { return ModelType::Pomdp; + } else if (type == "SMG") { + return ModelType::Smg; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known."); } @@ -44,6 +46,9 @@ namespace storm { case ModelType::Pomdp: os << "POMDP"; break; + case ModelType::Smg: + os << "SMG"; + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type."); } diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h index b183a598d..d9d7b0dc8 100644 --- a/src/storm/models/ModelType.h +++ b/src/storm/models/ModelType.h @@ -7,11 +7,11 @@ namespace storm { namespace models { // All supported model types. enum class ModelType { - Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp + Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp, Smg }; ModelType getModelType(std::string const& type); - + std::ostream& operator<<(std::ostream& os, ModelType const& type); } } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index bf9d69d4c..2bdddcbb7 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -58,18 +58,19 @@ namespace storm { STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of rows of transition matrix does not match state count."); STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of columns of transition matrix does not match state count."); STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); - } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton) || this->isOfType(ModelType::Pomdp)) { + } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton) || this->isOfType(ModelType::Pomdp) || this->isOfType(ModelType::Smg)) { STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of row groups (" << this->getTransitionMatrix().getRowGroupCount() << ") of transition matrix does not match state count (" << stateCount << ")."); STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of columns of transition matrix does not match state count."); STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); - } else { - STORM_LOG_THROW(this->isOfType(ModelType::S2pg), storm::exceptions::IllegalArgumentException, "Invalid model type."); + } else if (this->isOfType(ModelType::S2pg)) { STORM_LOG_THROW(components.player1Matrix.is_initialized(), storm::exceptions::IllegalArgumentException, "No player 1 matrix given for stochastic game."); STORM_LOG_ASSERT(components.player1Matrix->isProbabilistic(), "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry."); STORM_LOG_THROW(stateCount == components.player1Matrix->getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p1 matrix does not match state count."); STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount() == components.player1Matrix->getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix."); + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Invalid model type."); } - + // Branch on continuous/discrete timing if (this->isOfType(ModelType::Ctmc) || this->isOfType(ModelType::MarkovAutomaton)) { STORM_LOG_THROW(components.rateTransitions || components.exitRates.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create continuous time model: no rates are given."); @@ -79,6 +80,17 @@ namespace storm { STORM_LOG_WARN_COND(!components.rateTransitions && !components.exitRates.is_initialized(), "Rates specified for discrete-time model. The rates will be ignored."); } STORM_LOG_WARN_COND(this->isOfType(ModelType::MarkovAutomaton) || !components.markovianStates.is_initialized(), "Markovian states given for a model that is not a Markov automaton (will be ignored)."); + + // Treat stochastic multiplayer games + if (this->isOfType(ModelType::Smg)) { + STORM_LOG_THROW(components.statePlayerIndications.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create stochastic multiplayer game: Missing player indications."); + // playerNameToIndexMap is optional. + STORM_LOG_THROW(stateCount == components.statePlayerIndications->size(), storm::exceptions::IllegalArgumentException, "Size of state player indications (" << components.statePlayerIndications->size() << ") of SMG does not match state count (" << stateCount << ")."); + } else { + STORM_LOG_WARN_COND(!components.statePlayerIndications.is_initialized(), "statePlayerIndications given for a model that is not a stochastic multiplayer game (will be ignored)."); + STORM_LOG_WARN_COND(!components.playerNameToIndexMap.is_initialized(), "playerNameToIndexMap given for a model that is not a stochastic multiplayer game (will be ignored)."); + } + } template diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp new file mode 100644 index 000000000..40481ee06 --- /dev/null +++ b/src/storm/models/sparse/Smg.cpp @@ -0,0 +1,85 @@ +#include "storm/models/sparse/Smg.h" + +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/constants.h" +#include "storm/utility/vector.h" +#include "storm/adapters/RationalFunctionAdapter.h" + +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace models { + namespace sparse { + + template + Smg::Smg(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::Smg, components), statePlayerIndications(components.statePlayerIndications.get()) { + if (components.playerNameToIndexMap) { + playerNameToIndexMap = components.playerNameToIndexMap.get(); + } + // Otherwise the map remains empty. + } + + template + Smg::Smg(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::Smg, std::move(components)), statePlayerIndications(std::move(components.statePlayerIndications.get())) { + if (components.playerNameToIndexMap) { + playerNameToIndexMap = std::move(components.playerNameToIndexMap.get()); + } + // Otherwise the map remains empty. + } + + template + std::vector const& Smg::getStatePlayerIndications() const { + return statePlayerIndications; + } + + template + 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 { + auto findIt = playerNameToIndexMap.find(playerName); + STORM_LOG_THROW(findIt != playerNameToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown player name '" << playerName << "'."); + return findIt->second; + } + + template + storm::storage::BitVector Smg::computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const { + // Create a set and a bit vector encoding the coalition for faster access + std::set coalitionAsIndexSet; + for (auto const& player : coalition.getPlayers()) { + if (player.type() == typeid(std::string)) { + coalitionAsIndexSet.insert(getPlayerIndex(boost::get(player))); + } else { + STORM_LOG_ASSERT(player.type() == typeid(storm::storage::PlayerIndex), "Player identifier has unexpected type."); + coalitionAsIndexSet.insert(boost::get(player)); + } + } + storm::storage::BitVector coalitionAsBitVector(*coalitionAsIndexSet.rbegin()+1, false); + 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) { + auto const& pi = statePlayerIndications[state]; + if (pi < coalitionAsBitVector.size() && coalitionAsBitVector.get(pi)) { + result.set(state, true); + } + } + + return result; + } + + template class Smg; + template class Smg; + + template class Smg>; + template class Smg; + } // namespace sparse + } // namespace models +} // namespace storm diff --git a/src/storm/models/sparse/Smg.h b/src/storm/models/sparse/Smg.h new file mode 100644 index 000000000..b16475c18 --- /dev/null +++ b/src/storm/models/sparse/Smg.h @@ -0,0 +1,50 @@ +#ifndef STORM_MODELS_SPARSE_SMG_H_ +#define STORM_MODELS_SPARSE_SMG_H_ + +#include "storm/models/sparse/NondeterministicModel.h" +#include "storm/storage/PlayerIndex.h" +#include "storm/storage/BitVector.h" +#include "storm/logic/PlayerCoalition.h" + +namespace storm { + namespace models { + namespace sparse { + + /*! + * This class represents a stochastic multiplayer game. + */ + template> + class Smg : public NondeterministicModel { + public: + /*! + * Constructs a model from the given data. + * + * @param components The components for this model. + */ + Smg(storm::storage::sparse::ModelComponents const& components); + Smg(storm::storage::sparse::ModelComponents&& components); + + Smg(Smg const& other) = default; + Smg& operator=(Smg const& other) = default; + + Smg(Smg&& other) = default; + Smg& operator=(Smg&& other) = default; + + std::vector const& getStatePlayerIndications() const; + 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 + std::vector statePlayerIndications; + // A mapping of player names to player indices. + std::map playerNameToIndexMap; + }; + + } // namespace sparse + } // namespace models +} // namespace storm + +#endif /* STORM_MODELS_SPARSE_SMG_H_ */ diff --git a/src/storm/storage/PlayerIndex.h b/src/storm/storage/PlayerIndex.h new file mode 100644 index 000000000..7a903192d --- /dev/null +++ b/src/storm/storage/PlayerIndex.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace storage { + + typedef uint_fast64_t PlayerIndex; + PlayerIndex const INVALID_PLAYER_INDEX = std::numeric_limits::max(); + } +} \ No newline at end of file diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 3e59f4090..584817ce8 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -15,37 +15,37 @@ namespace storm { namespace storage { - + SymbolicModelDescription::SymbolicModelDescription(storm::jani::Model const& model) : modelDescription(model) { // Intentionally left empty. } - + SymbolicModelDescription::SymbolicModelDescription(storm::prism::Program const& program) : modelDescription(program) { // Intentionally left empty. } - + SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) { this->modelDescription = model; return *this; } - + SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) { this->modelDescription = program; return *this; } - + bool SymbolicModelDescription::hasModel() const { return static_cast(modelDescription); } - + bool SymbolicModelDescription::isJaniModel() const { return modelDescription.get().which() == 0; } - + bool SymbolicModelDescription::isPrismProgram() const { return modelDescription.get().which() == 1; } - + SymbolicModelDescription::ModelType SymbolicModelDescription::getModelType() const { if (this->isJaniModel()) { storm::jani::Model const& janiModel = this->asJaniModel(); @@ -65,12 +65,13 @@ namespace storm { case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP; case storm::prism::Program::ModelType::POMDP: return SymbolicModelDescription::ModelType::POMDP; case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA; + case storm::prism::Program::ModelType::SMG: return SymbolicModelDescription::ModelType::SMG; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type."); } } } - + storm::expressions::ExpressionManager& SymbolicModelDescription::getManager() const { if (this->isPrismProgram()) { return this->asPrismProgram().getManager(); @@ -78,15 +79,15 @@ namespace storm { return this->asJaniModel().getManager(); } } - + void SymbolicModelDescription::setModel(storm::jani::Model const& model) { modelDescription = model; } - + void SymbolicModelDescription::setModel(storm::prism::Program const& program) { modelDescription = program; } - + storm::jani::Model const& SymbolicModelDescription::asJaniModel() const { STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type."); return boost::get(modelDescription.get()); @@ -120,7 +121,7 @@ namespace storm { } return result; } - + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; @@ -131,7 +132,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); } } - + std::pair> SymbolicModelDescription::toJani(std::vector const& properties, bool makeVariablesGlobal) const { if (this->isJaniModel()) { return std::make_pair(*this, std::vector()); @@ -143,12 +144,12 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); } } - + SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { std::map substitution = parseConstantDefinitions(constantDefinitionString); return preprocess(substitution); } - + SymbolicModelDescription SymbolicModelDescription::preprocess(std::map const& constantDefinitions) const { if (this->isJaniModel()) { storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstantsFunctions(); @@ -158,7 +159,7 @@ namespace storm { } return *this; } - + std::map SymbolicModelDescription::parseConstantDefinitions(std::string const& constantDefinitionString) const { if (this->isJaniModel()) { return storm::utility::cli::parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString); @@ -166,7 +167,7 @@ namespace storm { return storm::utility::cli::parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString); } } - + void SymbolicModelDescription::requireNoUndefinedConstants() const { if (this->isJaniModel()) { storm::utility::jani::requireNoUndefinedConstants(this->asJaniModel()); @@ -174,7 +175,7 @@ namespace storm { storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram()); } } - + bool SymbolicModelDescription::hasUndefinedConstants() const { if (this->isPrismProgram()) { return this->asPrismProgram().hasUndefinedConstants(); @@ -182,7 +183,7 @@ namespace storm { return this->asJaniModel().hasUndefinedConstants(); } } - + std::vector SymbolicModelDescription::getUndefinedConstants() const { std::vector result; if (this->isPrismProgram()) { @@ -198,7 +199,7 @@ namespace storm { } return result; } - + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) { if (model.isPrismProgram()) { out << model.asPrismProgram(); @@ -228,6 +229,9 @@ namespace storm { case SymbolicModelDescription::ModelType::POMDP: out << "pomdp"; break; + case SymbolicModelDescription::ModelType::SMG: + out << "smg"; + break; } return out; } diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index da07e10f8..495091755 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -7,39 +7,39 @@ namespace storm { namespace storage { - + class SymbolicModelDescription { public: enum class ModelType { - DTMC, CTMC, MDP, MA, POMDP + DTMC, CTMC, MDP, MA, POMDP, SMG }; - + SymbolicModelDescription() = default; SymbolicModelDescription(storm::jani::Model const& model); SymbolicModelDescription(storm::prism::Program const& program); SymbolicModelDescription& operator=(storm::jani::Model const& model); SymbolicModelDescription& operator=(storm::prism::Program const& program); - + bool hasModel() const; bool isJaniModel() const; bool isPrismProgram() const; - + ModelType getModelType() const; storm::expressions::ExpressionManager& getManager() const; void setModel(storm::jani::Model const& model); void setModel(storm::prism::Program const& program); - + storm::jani::Model const& asJaniModel() const; storm::jani::Model& asJaniModel(); storm::prism::Program const& asPrismProgram() const; storm::prism::Program& asPrismProgram(); - + std::vector getParameterNames() const; - + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; - + /*! * Ensures that this model is a JANI model by, e.g., converting prism to jani. * If labels or reward models had to be converted during conversion, the renamings are applied to the given properties @@ -49,20 +49,20 @@ namespace storm { * @note The returned property vector might be empty in case no renaming is necessary. */ std::pair> toJani(std::vector const& properties, bool makeVariablesGlobal) const; - + SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; SymbolicModelDescription preprocess(std::map const& constantDefinitions) const; - + std::map parseConstantDefinitions(std::string const& constantDefinitionString) const; - + void requireNoUndefinedConstants() const; bool hasUndefinedConstants() const; std::vector getUndefinedConstants() const; - + private: boost::optional> modelDescription; }; - + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model); std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 79748e5da..ee2487002 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -324,18 +324,22 @@ namespace storm { } return opDecl; } - + boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { ExportJsonType opDecl; opDecl["op"] = "G"; opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); return opDecl; } - + + boost::any FormulaToJaniJson::visit(storm::logic::GameFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Conversion of game formulas to Jani is not supported."); + } + boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula"); } - + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { ExportJsonType opDecl; if(f.hasBound()) { diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 7c11358c6..9408cff82 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -57,6 +57,7 @@ namespace storm { virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::GameFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const; diff --git a/src/storm/storage/prism/Player.cpp b/src/storm/storage/prism/Player.cpp new file mode 100644 index 000000000..2b288f67f --- /dev/null +++ b/src/storm/storage/prism/Player.cpp @@ -0,0 +1,48 @@ +#include "storm/storage/prism/Player.h" +#include + +namespace storm { + namespace prism { + Player::Player(std::string const& playerName, std::unordered_set const& controlledModules, std::unordered_set const& controlledActions, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledActions(controlledActions) { + // Nothing to do here. + } + + std::string const& Player::getName() const { + return this->playerName; + } + + std::unordered_set const& Player::getModules() const { + return this->controlledModules; + } + + std::unordered_set const& Player::getActions() const { + return this->controlledActions; + } + + std::ostream& operator<<(std::ostream& stream, Player const& player) { + stream << "player"; + if (player.getName() != "") { + stream << " " << player.getName(); + } + bool firstElement = true; + for (auto const& module : player.getModules()) { + if (firstElement) { + firstElement = false; + } else { + stream << ","; + } + stream << std::endl << "\t" << module; + } + for (auto const& action : player.getActions()) { + if (firstElement) { + firstElement = false; + } else { + stream << ","; + } + stream << std::endl << "\t[" << action << "]"; + } + stream << std::endl << "endplayer" << std::endl; + return stream; + } + } // namespace prism +} // namespace storm diff --git a/src/storm/storage/prism/Player.h b/src/storm/storage/prism/Player.h new file mode 100644 index 000000000..c680bf8cc --- /dev/null +++ b/src/storm/storage/prism/Player.h @@ -0,0 +1,66 @@ +#pragma once + +#include +#include + +#include "storm/storage/prism/LocatedInformation.h" + +namespace storm { + namespace prism { + + class Player : public LocatedInformation { + public: + /*! + * Creates a player with the given name, controlled modules and actions. + * + * @param playerName The name of the player. + * @param controlledModules The controlled modules. + * @param controlledActions The controlled actions. + * @param filename The filename in which the player is defined. + * @param lineNumber The line number in which the player is defined. + */ + Player(std::string const& playerName, std::unordered_set const& controlledModules, std::unordered_set const& controlledActions, std::string const& filename = "", uint_fast32_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + Player() = default; + Player(Player const& other) = default; + Player& operator=(Player const& other) = default; + Player(Player&& other) = default; + Player& operator=(Player&& other) = default; + + /*! + * Retrieves the name of the player. + * + * @return The name of the player. + */ + std::string const& getName() const; + + /*! + * Retrieves all controlled Modules of the player. + * + * @return The modules controlled by the player. + */ + std::unordered_set const& getModules() const; + + /*! + * Retrieves all controlled Actions of the player. + * + * @return The Actions controlled by the player. + */ + std::unordered_set const& getActions() const; + + friend std::ostream& operator<<(std::ostream& stream, Player const& player); + private: + // The name of the player. + std::string playerName; + + // The modules associated with this player. + std::unordered_set controlledModules; + + // The Actions associated with this player. + std::unordered_set controlledActions; + }; + + } // namespace prism +} // namespace storm + diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index cdd41f7c3..0a892e20c 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -16,6 +16,7 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/InternalException.h" #include "storm/solver/SmtSolver.h" #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" @@ -32,14 +33,14 @@ namespace storm { CompositionValidityChecker(storm::prism::Program const& program) : program(program) { // Intentionally left empty. } - + void check(Composition const& composition) { composition.accept(*this, boost::any()); if (appearingModules.size() != program.getNumberOfModules()) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Not every module is used in the system composition."); } } - + virtual boost::any visit(ModuleComposition const& composition, boost::any const&) override { bool isValid = program.hasModule(composition.getModuleName()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist."); @@ -49,10 +50,10 @@ namespace storm { std::set synchronizingActionIndices = program.getModule(composition.getModuleName()).getSynchronizingActionIndices(); return synchronizingActionIndices; } - + virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override { std::set subSynchronizingActionIndices = boost::any_cast>(composition.getSubcomposition().accept(*this, data)); - + std::set newSynchronizingActionIndices = subSynchronizingActionIndices; for (auto const& namePair : composition.getActionRenaming()) { if (!program.hasAction(namePair.first)) { @@ -68,14 +69,14 @@ namespace storm { newSynchronizingActionIndices.insert(toIndex); } } - - + + return newSynchronizingActionIndices; } - + virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override { std::set subSynchronizingActionIndices = boost::any_cast>(composition.getSubcomposition().accept(*this, data)); - + for (auto const& action : composition.getActionsToHide()) { if (!program.hasAction(action)) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'."); @@ -86,34 +87,34 @@ namespace storm { subSynchronizingActionIndices.erase(it); } } - + return subSynchronizingActionIndices; } - + virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override { std::set leftSynchronizingActionIndices = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); std::set rightSynchronizingActionIndices = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); - + std::set synchronizingActionIndices; std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin())); - + return synchronizingActionIndices; } - + virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override { std::set leftSynchronizingActionIndices = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); std::set rightSynchronizingActionIndices = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); - + std::set synchronizingActionIndices; std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin())); - + return synchronizingActionIndices; } - + virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override { std::set leftSynchronizingActionIndices = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, data)); std::set rightSynchronizingActionIndices = boost::any_cast>(composition.getRightSubcomposition().accept(*this, data)); - + for (auto const& action : composition.getSynchronizingActions()) { if (!program.hasAction(action)) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'."); @@ -125,32 +126,32 @@ namespace storm { STORM_LOG_THROW(it != rightSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException, "Cannot synchronize on action '" << action << "', because module '" << composition.getRightSubcomposition() << " does not have this action."); } } - + std::set synchronizingActionIndices; std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin())); - + return synchronizingActionIndices; } - + private: storm::prism::Program const& program; std::set appearingModules; }; - - Program::Program(std::shared_ptr manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::map const& actionToIndexMap, std::vector const& rewardModels, std::vector