diff --git a/CMakeLists.txt b/CMakeLists.txt index 5161e4a22..b1900b90e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -148,7 +148,7 @@ else(CLANG) # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. set (CLANG ON) # Set standard flags for clang - set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") + set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 408faf8eb..dcf76c96f 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -248,13 +248,13 @@ namespace storm { template struct DdPrismModelBuilder::SystemResult { - SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, boost::optional> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { + SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, storm::dd::Add const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { // Intentionally left empty. } storm::dd::Add allTransitionsDd; typename DdPrismModelBuilder::ModuleDecisionDiagram globalModule; - boost::optional> stateActionDd; + storm::dd::Add stateActionDd; }; template @@ -719,16 +719,12 @@ namespace storm { storm::dd::Add result = createSystemFromModule(generationInfo, system); - // For MDPs and DTMCs, we need a DD that maps states to the legal choices and states to the number of - // available choices, respectively. As it happens, the construction is the same in both cases. - boost::optional> stateActionDd; - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables); - } + // Create an auxiliary DD that is used later during the construction of reward models. + storm::dd::Add stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables); // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - result = result / stateActionDd.get(); + result = result / stateActionDd; } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { // For MDPs, we need to throw away the nondeterminism variables from the generation information that // were never used. @@ -742,7 +738,7 @@ namespace storm { } template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, boost::optional> const& stateActionDd) { + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { // Start by creating the state reward vector. boost::optional> stateRewards; @@ -775,26 +771,21 @@ namespace storm { storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getRewardValueExpression()); storm::dd::Add synchronization = generationInfo.manager->getAddOne(); - if (stateActionReward.isLabeled()) { - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex()); - } - states *= globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()).guardDd * reachableStatesAdd; - } else { - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - synchronization = getSynchronizationDecisionDiagram(generationInfo); - } - states *= globalModule.independentAction.guardDd * reachableStatesAdd; + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex()); } - + ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; + states *= actionDd.guardDd * reachableStatesAdd; storm::dd::Add stateActionRewardDd = synchronization * states * rewards; // If we are building the state-action rewards for an MDP, we need to make sure that the encoding // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the // legal state-actions. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - STORM_LOG_THROW(static_cast(stateActionDd), storm::exceptions::InvalidStateException, "A DD that reflects the legal choices of each state was not build, but was expected to exist."); - stateActionRewardDd *= stateActionDd.get(); + stateActionRewardDd *= stateActionDd; + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { + // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. + stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); } // Perform some sanity checks. @@ -805,10 +796,9 @@ namespace storm { stateActionRewards.get() += stateActionRewardDd; } - // Scale state-action rewards for DTMCs. - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - STORM_LOG_THROW(static_cast(stateActionDd), storm::exceptions::InvalidStateException, "A DD that reflects the number of choices per state was not build, but was expected to exist."); - stateActionRewards.get() /= stateActionDd.get(); + // Scale state-action rewards for DTMCs and CTMCs. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { + stateActionRewards.get() /= stateActionDd; } } @@ -856,8 +846,7 @@ namespace storm { // Scale transition rewards for DTMCs. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - STORM_LOG_THROW(static_cast(stateActionDd), storm::exceptions::InvalidStateException, "A DD that reflects the number of choices per state was not build, but was expected to exist."); - transitionRewards.get() /= stateActionDd.get(); + transitionRewards.get() /= stateActionDd; } } @@ -901,7 +890,7 @@ namespace storm { SystemResult system = createSystemDecisionDiagram(generationInfo); storm::dd::Add transitionMatrix = system.allTransitionsDd; ModuleDecisionDiagram const& globalModule = system.globalModule; - boost::optional> stateActionDd = system.stateActionDd; + storm::dd::Add stateActionDd = system.stateActionDd; // Cut the transitions and rewards to the reachable fragment of the state space. storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); @@ -912,9 +901,7 @@ namespace storm { storm::dd::Bdd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); storm::dd::Add reachableStatesAdd = reachableStates.toAdd(); transitionMatrix *= reachableStatesAdd; - if (stateActionDd) { - stateActionDd.get() *= reachableStatesAdd; - } + stateActionDd *= reachableStatesAdd; // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 57ee60414..a815ddf06 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -194,7 +194,7 @@ namespace storm { static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, boost::optional> const& stateActionDd); + static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 9b96164f2..ca28a9d3e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -549,6 +549,16 @@ namespace storm { initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); } + // At this point, we determine whether there are reward models with state-action rewards, because we might + // want to know that quickly later on. + bool hasStateActionRewards = false; + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt) { + if (rewardModelIt->get().hasStateActionRewards()) { + hasStateActionRewards = true; + break; + } + } + // Insert the initial state in the global state to index mapping and state queue. uint32_t stateIndex = getOrAddStateIndex(initialState, stateInformation, stateQueue); stateInformation.initialStateIndices.push_back(stateIndex); @@ -666,6 +676,23 @@ namespace storm { } } + // If there is one state-action reward model, we need to scale the rewards according to the + // multiple choices. + ValueType totalExitMass = storm::utility::zero(); + if (hasStateActionRewards) { + if (discreteTimeModel) { + totalExitMass = static_cast(totalNumberOfChoices); + } else { + // In the CTMC, we need to compute the exit rate of the state here, sin + for (auto const& choice : allUnlabeledChoices) { + totalExitMass += choice.getTotalMass(); + } + for (auto const& choice : allLabeledChoices) { + totalExitMass += choice.getTotalMass(); + } + } + } + // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { if (commandLabels) { @@ -678,7 +705,7 @@ namespace storm { for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (!stateActionReward.isLabeled()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitMass; } } } @@ -704,7 +731,7 @@ namespace storm { for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) { if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitMass; } } } diff --git a/src/utility/prism.h b/src/utility/prism.h index c3399a240..f894b464f 100644 --- a/src/utility/prism.h +++ b/src/utility/prism.h @@ -137,6 +137,15 @@ namespace storm { return actionIndex; } + /*! + * Retrieves the total mass of this choice. + * + * @return The total mass. + */ + ValueType getTotalMass() const { + return totalMass; + } + /*! * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, * yet. @@ -170,6 +179,7 @@ namespace storm { } void addProbability(KeyType state, ValueType value) { + totalMass += value; distribution[state] += value; } @@ -180,7 +190,10 @@ namespace storm { private: // The distribution that is associated with the choice. std::map distribution; - + + // The total probability mass (or rates) of this choice. + ValueType totalMass; + // The index of the action name. uint_fast64_t actionIndex;