diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 28a4a03df..6085d5271 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -377,6 +377,19 @@ namespace storm { return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables); } + template + storm::dd::Dd DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction) { + storm::dd::Dd synchronization = generationInfo.manager->getOne(true); + for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { + if (synchronizationAction && synchronizationAction.get() == i) { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true); + } else { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); + } + } + return synchronization; + } + template storm::dd::Dd DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { // If the model is an MDP, we need to encode the nondeterminism using additional variables. @@ -405,24 +418,10 @@ namespace storm { } // Add variables for synchronization. - storm::dd::Dd synchronization = generationInfo.manager->getOne(true); - for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); - } - result *= synchronization; + result *= getSynchronizationDecisionDiagram(generationInfo); for (auto& synchronizingAction : synchronizingActionToDdMap) { - synchronization = generationInfo.manager->getOne(true); - - for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { - if (i == synchronizingAction.first) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true); - } else { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); - } - } - - synchronizingAction.second *= synchronization; + synchronizingAction.second *= getSynchronizationDecisionDiagram(generationInfo, synchronizingAction.first); } // Now, we can simply add all synchronizing actions to the result. @@ -516,6 +515,64 @@ namespace storm { return std::make_pair(result, system); } + template + std::pair, storm::dd::Dd> DdPrismModelBuilder::createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, storm::dd::Dd transitionMatrix) { + // Start by creating the state reward vector. + storm::dd::Dd stateRewards = generationInfo.manager->getZero(); + for (auto const& stateReward : rewardModel.getStateRewards()) { + storm::dd::Dd states = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getStatePredicateExpression()); + storm::dd::Dd rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression()); + + // Restrict the rewards to those states that satisfy the condition. + rewards = states * rewards; + + // Perform some sanity checks. + STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + + // Add the rewards to the global state reward vector. + stateRewards += rewards; + } + + // Then build the transition reward matrix. + storm::dd::Dd transitionRewards = generationInfo.manager->getZero(); + for (auto const& transitionReward : rewardModel.getTransitionRewards()) { + storm::dd::Dd states = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getStatePredicateExpression()); + storm::dd::Dd rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); + + storm::dd::Dd synchronization; + if (transitionReward.isLabeled()) { + synchronization = getSynchronizationDecisionDiagram(generationInfo); + } else { + synchronization = getSynchronizationDecisionDiagram(generationInfo, transitionReward.getActionIndex()); + } + + storm::dd::Dd transitionRewardDd = synchronization * states * rewards; + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + transitionRewardDd += transitionMatrix.notZero() * transitionRewardDd; + } else { + transitionRewardDd += transitionMatrix * transitionRewardDd; + } + + // Perform some sanity checks. + STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); + + // Add the rewards to the global transition reward matrix. + transitionRewards += transitionRewardDd; + } + + // Scale transition rewards for DTMCs + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { + for (uint_fast64_t i = 0; i < generationInfo.program.getRewardModels().size(); ++i){ + // Divide transition rewards through transition matrix + transitionRewardsDds[i] = transitionRewardsDds[i] / systemDds.independentActionDd.commandsDd; + } + } + + return std::make_pair(stateRewards, transitionRewards); + } + template std::pair, storm::dd::Dd> DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { // There might be nondeterministic variables. In that case the program must be prepared before translating. @@ -597,6 +654,25 @@ namespace storm { } std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl; + + // Finally, we build the DDs for a reward structure, if requested. + boost::optional, storm::dd::Dd>> stateAndTransitionRewards; + if (options.buildRewards) { + // If a specific reward model was selected or one with the empty name exists, select it. + storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); + if (options.rewardModelName) { + rewardModel = preparedProgram.getRewardModel(options.rewardModelName.get()); + } else if (preparedProgram.hasRewardModel("")) { + rewardModel = preparedProgram.getRewardModel(""); + } else if (preparedProgram.hasRewardModel()) { + // Otherwise, we select the first one. + rewardModel = preparedProgram.getRewardModel(0); + } + + STORM_LOG_TRACE("Building reward structure."); + stateAndTransitionRewards = createRewardDecisionDiagrams(generationInfo, rewardModel, transitionMatrix); + } + return std::make_pair(reachableStates, transitionMatrix); } @@ -1670,7 +1746,7 @@ namespace storm { // transitionRewardsDds[i] = transitionRewardsDds[i] / systemDds.independentActionDd.commandsDd; // } // } -// +// // // Pair to store state and transition rewards // return std::make_pair(stateRewardsDds, transitionRewardsDds); // } diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index e8854939a..63670b259 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -295,8 +295,12 @@ namespace storm { static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); + static storm::dd::Dd getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction = boost::optional()); + static storm::dd::Dd createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); + static std::pair, storm::dd::Dd>createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, storm::dd::Dd transitionMatrix); + static std::pair, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo); static storm::dd::Dd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index ba214ea2a..510be417a 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -44,36 +44,27 @@ namespace storm { notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; notStateFormula.name("negation formula"); - eventuallyFormula = (qi::lit("F") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1)]; + eventuallyFormula = (qi::lit("F") >> -(qi::lit("<=") >> qi::uint_) >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; eventuallyFormula.name("eventually formula"); - globallyFormula = (qi::lit("G") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)]; globallyFormula.name("globally formula"); - nextFormula = (qi::lit("X") >> simpleFormula)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)]; + nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - boundedUntilFormula = (simpleFormula >> (qi::lit("U<=") >> qi::uint_ >> simpleFormula))[qi::_val = phoenix::bind(&FormulaParser::createBoundedUntilFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; - boundedUntilFormula.name("bounded until formula"); + pathFormulaWithoutUntil = eventuallyFormula | globallyFormula | nextFormula | stateFormula; + pathFormulaWithoutUntil.name("path formula"); - untilFormula = (simpleFormula >> (qi::lit("U") >> simpleFormula))[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -(qi::lit("<=") >> qi::uint_) >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); - simplePathFormula = eventuallyFormula | globallyFormula | nextFormula | boundedUntilFormula | untilFormula; - simplePathFormula.name("simple path formula"); - - conditionalFormula = (simplePathFormula >> (qi::lit("||") > simplePathFormula))[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)]; conditionalFormula.name("conditional formula"); - pathFormula = conditionalFormula | simplePathFormula; + pathFormula = conditionalFormula; pathFormula.name("path formula"); - simpleFormula = stateFormula | simplePathFormula; - simpleFormula.name("simple formula"); - - formula = stateFormula | pathFormula; - formula.name("formula"); - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); @@ -104,14 +95,13 @@ namespace storm { /*! * Enable the following lines to print debug output for most the rules. debug(start); - debug(comments); debug(stateFormula); debug(orStateFormula); debug(andStateFormula); debug(probabilityOperator); debug(rewardOperator); debug(steadyStateOperator); - debug(formula); + debug(pathFormulaWithoutUntil); debug(pathFormula); debug(conditionalFormula); debug(nextFormula); @@ -136,7 +126,7 @@ namespace storm { qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(formula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -203,8 +193,12 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParser::createEventuallyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); + std::shared_ptr FormulaParser::createEventuallyFormula(boost::optional const& stepBound, std::shared_ptr const& subformula) const { + if (stepBound) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(stepBound.get()))); + } else { + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula)); + } } std::shared_ptr FormulaParser::createGloballyFormula(std::shared_ptr const& subformula) const { @@ -215,12 +209,12 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParser::createUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) { - return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); - } - - std::shared_ptr FormulaParser::createBoundedUntilFormula(std::shared_ptr const& leftSubformula, unsigned stepBound, std::shared_ptr const& rightSubformula) const { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(stepBound))); + std::shared_ptr FormulaParser::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional const& stepBound, std::shared_ptr const& rightSubformula) { + if (stepBound) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(stepBound.get()))); + } else { + return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); + } } std::shared_ptr FormulaParser::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 72f1877f4..e1f424b9b 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -126,10 +126,10 @@ namespace storm { qi::rule(), Skipper> expectedTimeOperator; qi::rule(), Skipper> steadyStateOperator; - qi::rule(), Skipper> formula; qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; qi::rule(), Skipper> pathFormula; + qi::rule(), Skipper> pathFormulaWithoutUntil; qi::rule(), Skipper> simplePathFormula; qi::rule(), Skipper> atomicStateFormula; qi::rule label; @@ -160,11 +160,10 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional const& stepBound, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula); - std::shared_ptr createBoundedUntilFormula(std::shared_ptr const& leftSubformula, unsigned stepBound, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional const& stepBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createRewardOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const;