From d35e9a6a406612c7ecef8508b4aeca0441a6524a Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 11 Aug 2020 16:32:32 +0200 Subject: [PATCH] removed plenty of empty line whitespaces --- src/storm-parsers/parser/PrismParser.cpp | 234 ++++---- src/storm-parsers/parser/PrismParser.h | 66 +-- src/storm/generator/NextStateGenerator.h | 16 +- .../generator/PrismNextStateGenerator.cpp | 176 +++--- .../storage/SymbolicModelDescription.cpp | 40 +- src/storm/storage/SymbolicModelDescription.h | 10 +- src/storm/storage/prism/Program.cpp | 527 +++++++++--------- src/storm/storage/prism/Program.h | 188 +++---- 8 files changed, 631 insertions(+), 626 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index c95c42af2..3a6be1ed2 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -23,7 +23,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 +37,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 +53,7 @@ namespace storm { // Create empty result; storm::prism::Program result; - + // Create grammar. storm::parser::PrismParser grammar(filename, first, prismCompatibility); try { @@ -62,7 +62,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 +73,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 +181,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.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 +211,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 +247,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("]")) | @@ -298,7 +298,7 @@ namespace storm { ) > -(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 +320,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 +350,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,22 +397,22 @@ 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) { STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'."); @@ -420,7 +420,7 @@ namespace storm { } 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 +428,7 @@ namespace storm { } 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 +436,7 @@ namespace storm { } return true; } - + bool PrismParser::isFreshLabelName(std::string const& labelName) { if (!this->secondRun) { for (auto const& existingLabel : this->globalProgramInformation.labels) { @@ -460,7 +460,7 @@ namespace storm { } return true; } - + bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) { if (!this->secondRun) { for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) { @@ -472,19 +472,19 @@ namespace storm { } 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 +494,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 +508,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 +540,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 +552,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 +564,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 +576,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 +588,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 +600,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 +608,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 +623,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 +635,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 +647,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 +659,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 +686,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 +697,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 +716,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 +733,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 { @@ -795,18 +795,18 @@ 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]; auto const& renaming = moduleRenaming.getRenaming(); - + if (!this->secondRun) { // Register all (renamed) variables for later use. // We already checked before, whether the renaiming is valid. @@ -837,7 +837,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,13 +852,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(); - + // Create a mapping from identifiers to the expressions they need to be replaced with. std::map expressionRenaming; for (auto const& namePair : renaming) { @@ -868,7 +868,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 +880,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 +904,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 +928,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 +944,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) { @@ -971,7 +971,7 @@ 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); } - + 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..b816b9c1f 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; @@ -45,11 +45,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; @@ -81,7 +81,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 +90,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() { @@ -152,7 +152,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 +160,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 +194,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 +217,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 +227,49 @@ 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; - + // 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 commandName; + qi::rule playerDefinition; + // 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,20 +298,20 @@ 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); @@ -323,7 +327,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; diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 59f50843e..d4633ede4 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -88,7 +88,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. @@ -100,25 +100,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..823b0305c 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()) { @@ -87,7 +87,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 +118,7 @@ namespace storm { } #endif } - + template ModelType PrismNextStateGenerator::getModelType() const { switch (program.getModelType()) { @@ -146,7 +146,7 @@ namespace storm { bool PrismNextStateGenerator::isPartiallyObservable() const { return program.isPartiallyObservable(); } - + template std::vector PrismNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { std::vector initialStateIndices; @@ -162,9 +162,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 +177,7 @@ namespace storm { initialState.set(booleanVariable.bitOffset, false); } } - + bool changedIntegerVariable = false; if (changedBooleanVariable) { initialStateIndices.emplace_back(stateToIdCallback(initialState)); @@ -191,37 +191,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 +238,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 +274,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 +286,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 +301,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 +317,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 +331,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 +355,41 @@ 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)); } - + // 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 +398,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 +417,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 +432,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 +476,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 +507,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 +541,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 +561,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 +569,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 +582,24 @@ namespace storm { } choice.addReward(stateActionRewardValue); } - + 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 +611,7 @@ namespace storm { } } } - + template void PrismNextStateGenerator::addLabeledChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) { @@ -702,7 +702,7 @@ namespace storm { } } } - + 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 +720,7 @@ namespace storm { } } } - + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); } @@ -741,22 +741,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 +764,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 +772,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/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 3e59f4090..af6dd5631 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(); @@ -78,15 +78,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 +120,7 @@ namespace storm { } return result; } - + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; @@ -131,7 +131,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 +143,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 +158,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 +166,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 +174,7 @@ namespace storm { storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram()); } } - + bool SymbolicModelDescription::hasUndefinedConstants() const { if (this->isPrismProgram()) { return this->asPrismProgram().hasUndefinedConstants(); @@ -182,7 +182,7 @@ namespace storm { return this->asJaniModel().hasUndefinedConstants(); } } - + std::vector SymbolicModelDescription::getUndefinedConstants() const { std::vector result; if (this->isPrismProgram()) { @@ -198,7 +198,7 @@ namespace storm { } return result; } - + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) { if (model.isPrismProgram()) { out << model.asPrismProgram(); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index da07e10f8..0d72bf5e3 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -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/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index cdd41f7c3..01127d555 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -32,14 +32,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 +49,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 +68,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 +86,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,18 +125,18 @@ 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