diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 2a174b4cb..1b6cf93f4 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -6,8 +6,6 @@ #include "src/models/sparse/Ctmc.h" #include "src/models/sparse/Mdp.h" - - #include "src/settings/modules/GeneralSettings.h" #include "src/utility/prism.h" @@ -18,6 +16,40 @@ namespace storm { namespace builder { + /*! + * A structure that is used to keep track of a reward model currently being built. + */ + template + struct RewardModelBuilder { + public: + RewardModelBuilder(bool deterministicModel, bool hasStateRewards, bool hasStateActionRewards, bool hasTransitionRewards) : hasStateRewards(hasStateRewards), hasStateActionRewards(hasStateActionRewards), hasTransitionRewards(hasTransitionRewards), stateRewardVector(), stateActionRewardVector(), transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0) { + // Intentionally left empty. + } + + storm::models::sparse::StandardRewardModel build(uint_fast64_t rowCount, uint_fast64_t columnCount, uint_fast64_t rowGroupCount) { + if (hasStateRewards) { + stateRewardVector.resize(rowGroupCount); + } + if (hasStateActionRewards) { + stateActionRewardVector.resize(rowCount); + } + return storm::models::sparse::StandardRewardModel(hasStateRewards ? std::move(stateRewardVector) : boost::none, hasStateActionRewards ? std::move(stateActionRewardVector) : boost::none, hasTransitionRewards ? transitionRewardMatrixBuilder.build(rowCount, columnCount, rowGroupCount) : boost::none); + } + + bool hasStateRewards; + bool hasStateActionRewards; + bool hasTransitionRewards; + + // The state reward vector. + std::vector stateRewardVector; + + // The state-action reward vector. + std::vector stateActionRewardVector; + + // A builder that is used for constructing the transition reward matrix. + storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; + }; + template ExplicitPrismModelBuilder::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { // Intentionally left empty. @@ -56,17 +88,29 @@ namespace storm { } template - ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), stateRewards(), transitionRewardMatrix(), choiceLabeling() { + ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildRewards(false), rewardModelName(), constantDefinitions() { + ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildRewards(formula.containsRewardOperator()), rewardModelName(), constantDefinitions(), labelsToBuild(std::set()), expressionLabels(std::vector()) { + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set()), expressionLabels(std::vector()) { + this->preserveFormula(formula); + } + + template + void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { + if (!buildAllRewardModels) { + if (formula.containsRewardOperator()) { + std::set referencedRewardModels = formula.getReferencedRewardModels(); + rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); + } + } + // Extract all the labels used in the formula. std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); for (auto const& formula : atomicLabelFormulas) { @@ -79,7 +123,7 @@ namespace storm { expressionLabels.get().push_back(formula.get()->getExpression()); } } - + template void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -154,45 +198,26 @@ namespace storm { // Now that the program is fixed, we we need to substitute all constants with their concrete value. preparedProgram = preparedProgram.substituteConstants(); - // Select the appropriate reward model (after the constants have been substituted). - storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); - if (options.buildRewards) { - // If a specific reward model was selected or one with the empty name exists, select it. - 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); + // Select the appropriate reward models (after the constants have been substituted). + std::vector> selectedRewardModels; + for (auto const& rewardModel : preparedProgram.getRewardModels()) { + if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { + selectedRewardModels.push_back(rewardModel); } } - ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options); + ModelComponents modelComponents = buildModelComponents(preparedProgram, selectedRewardModels, options); std::shared_ptr> result; - std::map> rewardModels; - if (options.buildRewards) { - std::string rewardModelName; - if (options.rewardModelName) { - rewardModelName = options.rewardModelName.get(); - } else { - rewardModelName = ""; - } - rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), - boost::optional>(), - rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>())); - } - switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMC: - result = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::MDP: - result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(rewardModels), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); break; default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -458,7 +483,7 @@ namespace storm { } template - boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { + boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders) { // Create choice labels, if requested, boost::optional>> choiceLabels; if (commandLabels) { @@ -486,7 +511,11 @@ namespace storm { // Now explore the current state until there is no more reachable state. uint_fast64_t currentRow = 0; + + // The evaluator used to determine the truth value of guards and predicates in the *current* state. storm::expressions::ExpressionEvaluator evaluator(program.getManager()); + + // Perform a BFS through the model. while (!stateQueue.empty()) { // Get the current state and unpack it. storm::storage::BitVector currentState = stateQueue.front(); @@ -510,7 +539,6 @@ namespace storm { } if (!deterministicModel) { transitionMatrixBuilder.newRowGroup(currentRow); - transitionRewardMatrixBuilder.newRowGroup(currentRow); } transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one()); @@ -519,32 +547,31 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); } } else if (totalNumberOfChoices == 1) { - Choice globalChoice; - if (!deterministicModel) { transitionMatrixBuilder.newRowGroup(currentRow); - transitionRewardMatrixBuilder.newRowGroup(currentRow); } - std::map stateToRewardMap; - if (!allUnlabeledChoices.empty()) { - globalChoice = allUnlabeledChoices.front(); - for (auto const& stateProbabilityPair : globalChoice) { - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); + bool labeledChoice = allUnlabeledChoices.empty() ? false : true; + Choice const& globalChoice = labeledChoice ? allLabeledChoices.front() : allUnlabeledChoices.front(); + + auto builderIt = rewardModelBuilders.begin(); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateRewards()) { + builderIt->stateRewardVector.push_back(storm::utility::zero()); + for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { + if (evaluator.asBool(stateReward.getStatePredicateExpression())) { + builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); } } } - } else { - globalChoice = allLabeledChoices.front(); - for (auto const& stateProbabilityPair : globalChoice) { - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (transitionReward.isLabeled() && transitionReward.getActionIndex() == globalChoice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.push_back(storm::utility::zero()); + for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { + if ((labeledChoice && stateActionReward.isLabeled() && stateActionReward.getActionIndex() == globalChoice.getActionIndex()) || (!labeledChoice && !stateActionReward.isLabeled())) { + if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + } } } } @@ -555,17 +582,6 @@ namespace storm { choiceLabels.get().push_back(globalChoice.getChoiceLabels()); } - for (auto const& stateProbabilityPair : globalChoice) { - transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); - } - - // Add all transition rewards to the matrix and add dummy entry if there is none. - if (!stateToRewardMap.empty()) { - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); - } - } - ++currentRow; } else { // Then, based on whether the model is deterministic or not, either add the choices individually @@ -573,7 +589,7 @@ namespace storm { if (deterministicModel) { Choice globalChoice; - std::map stateToRewardMap; + std::unordered_map stateToRewardMap; // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { @@ -581,19 +597,35 @@ namespace storm { globalChoice.addChoiceLabels(choice.getChoiceLabels()); } + auto builderIt = rewardModelBuilders.begin(); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateRewards()) { + builderIt->stateRewardVector.resize(currentRow + 1); + for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { + if (evaluator.asBool(stateReward.getStatePredicateExpression())) { + builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + } + } + } + + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.resize(currentRow + 1); + for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { + if (!stateActionReward.isLabeled()) { + if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; + } + } + } + } + } + for (auto const& stateProbabilityPair : choice) { if (discreteTimeModel) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; } else { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second; } - - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); - } - } } } for (auto const& choice : allLabeledChoices) { @@ -601,19 +633,35 @@ namespace storm { globalChoice.addChoiceLabels(choice.getChoiceLabels()); } + auto builderIt = rewardModelBuilders.begin(); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateRewards()) { + builderIt->stateRewardVector.resize(currentRow + 1); + for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { + if (evaluator.asBool(stateReward.getStatePredicateExpression())) { + builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + } + } + } + + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.resize(currentRow + 1); + for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { + if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) { + if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices; + } + } + } + } + } + for (auto const& stateProbabilityPair : choice) { if (discreteTimeModel) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; } else { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second; } - - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (transitionReward.isLabeled() && transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); - } - } } } @@ -627,18 +675,23 @@ namespace storm { transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } - // Add all transition rewards to the matrix and add dummy entry if there is none. - if (!stateToRewardMap.empty()) { - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); - } - } - ++currentRow; } else { // If the model is nondeterministic, we add all choices individually. transitionMatrixBuilder.newRowGroup(currentRow); - transitionRewardMatrixBuilder.newRowGroup(currentRow); + + // For all reward models that + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(), builderIt = rewardModelBuilders.begin(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateRewards()) { + builderIt->stateRewardVector.push_back(); + + for (auto const& stateReward : rewardModelIt->get().getStateRewards()) { + if (evaluator.asBool(stateReward.getStatePredicateExpression())) { + builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + } + } + } + } // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { @@ -647,23 +700,21 @@ namespace storm { choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels())); } - for (auto const& stateProbabilityPair : choice) { - transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); - - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(), builderIt = rewardModelBuilders.begin(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.resize(currentRow + 1); + for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { + if (!stateActionReward.isLabeled()) { + if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + } + } } } - } - // Add all transition rewards to the matrix and add dummy entry if there is none. - if (stateToRewardMap.size() > 0) { - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); - } + for (auto const& stateProbabilityPair : choice) { + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } ++currentRow; @@ -676,23 +727,21 @@ namespace storm { choiceLabels.get().emplace_back(std::move(choice.getChoiceLabels())); } - for (auto const& stateProbabilityPair : choice) { - transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); - - // Now add all rewards that match this choice. - for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(), builderIt = rewardModelBuilders.begin(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + if (rewardModelIt->get().hasStateActionRewards()) { + builderIt->stateActionRewardVector.resize(currentRow + 1); + for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) { + if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) { + if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())); + } + } } } - } - // Add all transition rewards to the matrix and add dummy entry if there is none. - if (!stateToRewardMap.empty()) { - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); - } + for (auto const& stateProbabilityPair : choice) { + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } ++currentRow; @@ -705,7 +754,7 @@ namespace storm { } template - typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, Options const& options) { + typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options) { ModelComponents modelComponents; uint_fast64_t bitOffset = 0; @@ -748,20 +797,23 @@ namespace storm { bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC; bool discreteTimeModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP; - // Build the transition and reward matrices. + // Prepare the transition matrix builder and the reward model builders. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); + std::vector> rewardModelBuilders; + for (auto const& rewardModel : selectedRewardModels) { + rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards()); + } - // Finalize the resulting matrices. - modelComponents.transitionMatrix = transitionMatrixBuilder.build(); - modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()); + modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders); - // Now build the state labeling. - modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); + // Now finalize all reward models. + auto builderIt = rewardModelBuilders.begin(); + for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) { + modelComponents.rewardModels.emplace(rewardModelIt->get().getName(), builderIt->build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); + } - // Finally, construct the state rewards. - modelComponents.stateRewards = buildStateRewards(program, variableInformation, rewardModel.getStateRewards(), stateInformation); + // Finally, build the state labeling. + modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); return modelComponents; } diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index c88932eb5..8e4cd5e3a 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -27,7 +27,10 @@ namespace storm { namespace builder { using namespace storm::utility::prism; - + + // Forward-declare classes. + template struct RewardModelBuilder; + template class ExplicitPrismModelBuilder { public: @@ -110,11 +113,8 @@ namespace storm { // The state labeling. storm::models::sparse::StateLabeling stateLabeling; - // The state reward vector. - std::vector stateRewards; - - // A matrix storing the reward for particular transitions. - storm::storage::SparseMatrix transitionRewardMatrix; + // The reward models associated with the model. + std::unordered_map> rewardModels; // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; @@ -127,7 +127,7 @@ namespace storm { Options(); /*! Creates an object representing the suggested building options assuming that the given formula is the - * only one to check. + * only one to check. Additional formulas may be preserved by calling preserveFormula. * * @param formula The formula based on which to choose the building options. */ @@ -143,14 +143,22 @@ namespace storm { */ void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString); + /*! + * Changes the options in a way that ensures that the given formula can be checked on the model once it + * has been built. + * + * @param formula The formula that is to be ''preserved''. + */ + void preserveFormula(storm::logic::Formula const& formula); + // A flag that indicates whether or not command labels are to be built. bool buildCommandLabels; - // A flag that indicates whether or not a reward model is to be built. - bool buildRewards; + // A flag that indicates whether or not all reward models are to be build. + bool buildAllRewardModels; - // An optional string, that, if given, indicates which of the reward models is to be built. - boost::optional rewardModelName; + // A list of reward models to be build in case not all reward models are to be build. + std::set rewardModelsToBuild; // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional> constantDefinitions; @@ -243,22 +251,22 @@ namespace storm { * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not. * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this * function. - * @param transitionRewardMatrix A reference to an initialized matrix which is filled with all transition - * rewards by this function. + * @param rewardModelBuilders A vector of reward model builders that is used to build the vector of selected + * reward models. * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder); + static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders); /*! * Explores the state space of the given program and returns the components of the model as a result. * * @param program The program whose state space to explore. - * @param rewardModel The reward model that is to be considered. + * @param selectedRewardModels The reward models that are to be considered. * @param options A set of options used to customize the building process. * @return A structure containing the components of the resulting model. */ - static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, Options const& options); + static ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options); /*! * Builds the state labeling for the given program. diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index 046a5176f..949dbf378 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -63,5 +63,10 @@ namespace storm { this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } + + void BinaryPathFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); + this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); + } } } \ No newline at end of file diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index 87d4de03b..4eff96117 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -32,7 +32,8 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + private: std::shared_ptr leftSubformula; std::shared_ptr rightSubformula; diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index 80b7caf9b..6993707ad 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -63,5 +63,10 @@ namespace storm { this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } + + void BinaryStateFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); + this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); + } } } \ No newline at end of file diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index 68f39a690..0fdc8dd47 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -30,7 +30,8 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + private: std::shared_ptr leftSubformula; std::shared_ptr rightSubformula; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 6cf27dfdd..4037cb723 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -378,6 +378,12 @@ namespace storm { return result; } + std::set Formula::getReferencedRewardModels() const { + std::set referencedRewardModels; + this->gatherReferencedRewardModels(referencedRewardModels); + return referencedRewardModels; + } + std::shared_ptr Formula::asSharedPointer() { return this->shared_from_this(); } @@ -394,6 +400,10 @@ namespace storm { return; } + void Formula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + return; + } + std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 746ab71a7..3c3c3b5aa 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -4,7 +4,7 @@ #include #include #include - +#include namespace storm { namespace logic { @@ -169,6 +169,7 @@ namespace storm { std::vector> getAtomicExpressionFormulas() const; std::vector> getAtomicLabelFormulas() const; + std::set getReferencedRewardModels() const; std::shared_ptr asSharedPointer(); std::shared_ptr asSharedPointer() const; @@ -177,6 +178,7 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; virtual void gatherAtomicLabelFormulas(std::vector>& atomicExpressionFormulas) const; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; private: // Currently empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 34d9891cc..dac396c69 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -46,6 +46,15 @@ namespace storm { return this->rewardModelName; } + void RewardOperatorFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + if (this->hasRewardModelName()) { + referencedRewardModels.insert(this->getRewardModelName()); + } else { + referencedRewardModels.insert(""); + } + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + } + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula), rewardModelName(rewardModelName) { // Intentionally left empty. } diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 9b2d70a35..b3d63a5a3 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -23,6 +23,8 @@ namespace storm { virtual bool containsRewardOperator() const override; virtual bool containsNestedRewardOperators() const override; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; /*! diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index d6d6dd01d..d961f1612 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -53,5 +53,9 @@ namespace storm { void UnaryPathFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } + + void UnaryPathFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + } } } \ No newline at end of file diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index f02c7a830..74501823f 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -30,7 +30,8 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + private: std::shared_ptr subformula; }; diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index ab2718d69..4bf651aa1 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -57,6 +57,10 @@ namespace storm { void UnaryStateFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } + + void UnaryStateFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + } } } \ No newline at end of file diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index f604262e8..3db2b9263 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -29,7 +29,8 @@ namespace storm { virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; - + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; + private: std::shared_ptr subformula; }; diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 07af96b33..2e93246b3 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" + #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" @@ -206,6 +208,11 @@ namespace storm { return result; } + template + std::vector SparseDtmcPrctlHelper::computeLongRunAverage(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverage(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); + } + template class SparseDtmcPrctlHelper; } } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 9880bc7b6..44d6a454b 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -45,12 +45,14 @@ namespace storm { } // Explicitly instantiate the template class. + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; #ifdef STORM_HAVE_CARL + template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 516584145..a9509ddbb 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -9,7 +9,7 @@ namespace storm { template Ctmc::Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { exitRates = createExitRateVector(this->getTransitionMatrix()); @@ -17,7 +17,7 @@ namespace storm { template Ctmc::Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere. diff --git a/src/models/sparse/Ctmc.h b/src/models/sparse/Ctmc.h index 728c645ae..db3beeb7e 100644 --- a/src/models/sparse/Ctmc.h +++ b/src/models/sparse/Ctmc.h @@ -23,7 +23,7 @@ namespace storm { * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -35,7 +35,7 @@ namespace storm { * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); Ctmc(Ctmc const& ctmc) = default; diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index 94db83d72..3942f8301 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -9,7 +9,7 @@ namespace storm { DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. @@ -19,7 +19,7 @@ namespace storm { DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // Intentionally left empty. diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h index 4061f742f..df2052806 100644 --- a/src/models/sparse/DeterministicModel.h +++ b/src/models/sparse/DeterministicModel.h @@ -26,7 +26,7 @@ namespace storm { DeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -41,7 +41,7 @@ namespace storm { DeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); DeterministicModel(DeterministicModel const& other) = default; diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index cc9725a25..a92872c0f 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -12,7 +12,7 @@ namespace storm { template Dtmc::Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); @@ -20,7 +20,7 @@ namespace storm { template Dtmc::Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, boost::optional>&& optionalChoiceLabeling) + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 4b1cdc73f..067289a4d 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -27,7 +27,7 @@ namespace storm { */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -39,7 +39,7 @@ namespace storm { * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); Dtmc(Dtmc const& dtmc) = default; diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index d0e46b625..694cb2a07 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -13,7 +13,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { this->turnRatesToProbabilities(); @@ -24,7 +24,7 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { this->turnRatesToProbabilities(); diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index dfa4f952b..eb445a569 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -28,7 +28,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -45,7 +45,7 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); MarkovAutomaton(MarkovAutomaton const& other) = default; diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 9d9c175fd..9b64449d2 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -11,7 +11,7 @@ namespace storm { template Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); @@ -21,7 +21,7 @@ namespace storm { template Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h index e82fb8e23..cf35eb33d 100644 --- a/src/models/sparse/Mdp.h +++ b/src/models/sparse/Mdp.h @@ -24,7 +24,7 @@ namespace storm { */ Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -37,7 +37,7 @@ namespace storm { */ Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); Mdp(Mdp const& other) = default; diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 6f2da7268..7a1d8beba 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -15,7 +15,7 @@ namespace storm { Model::Model(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : ModelBase(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), choiceLabeling(optionalChoiceLabeling) { @@ -28,7 +28,7 @@ namespace storm { Model::Model(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : ModelBase(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), choiceLabeling(std::move(optionalChoiceLabeling)) { @@ -105,7 +105,7 @@ namespace storm { } template - typename std::map::const_iterator Model::getUniqueRewardModel() const { + typename std::unordered_map::const_iterator Model::getUniqueRewardModel() const { STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique."); return this->rewardModels.cbegin(); } @@ -270,12 +270,12 @@ namespace storm { } template - std::map& Model::getRewardModels() { + std::unordered_map& Model::getRewardModels() { return this->rewardModels; } template - std::map const& Model::getRewardModels() const { + std::unordered_map const& Model::getRewardModels() const { return this->rewardModels; } diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 37e4cc0b3..7aadc01c9 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -2,6 +2,7 @@ #define STORM_MODELS_SPARSE_MODEL_H_ #include +#include #include #include @@ -12,8 +13,6 @@ #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" #include "src/utility/OsDetection.h" -// Forward declarations - namespace storm { namespace models { @@ -52,7 +51,7 @@ namespace storm { Model(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::unordered_map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -67,7 +66,7 @@ namespace storm { Model(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::unordered_map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); /*! @@ -156,7 +155,7 @@ namespace storm { * * @return An iterator to the name and the reward model. */ - typename std::map::const_iterator getUniqueRewardModel() const; + typename std::unordered_map::const_iterator getUniqueRewardModel() const; /*! * Retrieves whether the model has a unique reward model. @@ -304,14 +303,14 @@ namespace storm { * * @return A mapping from reward model names to the reward models. */ - std::map const& getRewardModels() const; + std::unordered_map const& getRewardModels() const; /*! * Retrieves the reward models. * * @return A mapping from reward model names to the reward models. */ - std::map& getRewardModels(); + std::unordered_map& getRewardModels(); private: // A matrix representing transition relation. @@ -321,7 +320,7 @@ namespace storm { storm::models::sparse::StateLabeling stateLabeling; // The reward models of the model. - std::map rewardModels; + std::unordered_map rewardModels; // If set, a vector representing the labels of choices. boost::optional> choiceLabeling; diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index a620095cc..a2310d073 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -10,7 +10,7 @@ namespace storm { NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. @@ -20,7 +20,7 @@ namespace storm { NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h index 1476506c3..0e67e9e15 100644 --- a/src/models/sparse/NondeterministicModel.h +++ b/src/models/sparse/NondeterministicModel.h @@ -26,7 +26,7 @@ namespace storm { NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalChoiceLabeling = boost::optional>()); /*! @@ -41,7 +41,7 @@ namespace storm { NondeterministicModel(storm::models::ModelType const& modelType, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); NondeterministicModel(NondeterministicModel const& other) = default; diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index fbd76593a..f6a3d5a54 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -4,6 +4,8 @@ #include "src/exceptions/InvalidOperationException.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace sparse { @@ -37,7 +39,12 @@ namespace storm { std::vector const& StandardRewardModel::getStateRewardVector() const { return this->optionalStateRewardVector.get(); } - + + template + std::vector& StandardRewardModel::getStateRewardVector() { + return this->optionalStateRewardVector.get(); + } + template boost::optional> const& StandardRewardModel::getOptionalStateRewardVector() const { return this->optionalStateRewardVector; @@ -53,6 +60,11 @@ namespace storm { return this->optionalStateActionRewardVector.get(); } + template + std::vector& StandardRewardModel::getStateActionRewardVector() { + return this->optionalStateActionRewardVector.get(); + } + template boost::optional> const& StandardRewardModel::getOptionalStateActionRewardVector() const { return this->optionalStateActionRewardVector; @@ -68,6 +80,11 @@ namespace storm { return this->optionalTransitionRewardMatrix.get(); } + template + storm::storage::SparseMatrix& StandardRewardModel::getTransitionRewardMatrix() { + return this->optionalTransitionRewardMatrix.get(); + } + template boost::optional> const& StandardRewardModel::getOptionalTransitionRewardMatrix() const { return this->optionalTransitionRewardMatrix; @@ -93,7 +110,7 @@ namespace storm { void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards) { if (this->hasTransitionRewards()) { if (this->hasStateActionRewards()) { - storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector); + storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector()); } else { this->optionalStateActionRewardVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); } @@ -101,8 +118,8 @@ namespace storm { if (reduceToStateRewards && this->hasStateActionRewards()) { if (this->hasStateRewards()) { - STORM_LOG_THROW(this->getStateRewardVector.size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension."); - storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); + STORM_LOG_THROW(this->getStateRewardVector().size() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible of both the state and the state-action rewards have the same dimension."); + storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); } else { this->optionalStateRewardVector = std::move(this->optionalStateRewardVector); } @@ -119,16 +136,15 @@ namespace storm { if (this->hasStateRewards()) { storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices()); } + return result; } template template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const { - std::vector pointwiseProductRowSumVector; - std::vector result(numberOfRows); if (this->hasTransitionRewards()) { - pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + std::vector pointwiseProductRowSumVector = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); storm::utility::vector::selectVectorValues(result, filter, transitionMatrix.getRowGroupIndices(), pointwiseProductRowSumVector); } @@ -138,6 +154,7 @@ namespace storm { if (this->hasStateRewards()) { storm::utility::vector::addFilteredVectorToGroupedVector(result, this->getStateRewardVector(), filter, transitionMatrix.getRowGroupIndices()); } + return result; } template @@ -182,7 +199,22 @@ namespace storm { } // Explicitly instantiate the class. + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template class StandardRewardModel; + + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template class StandardRewardModel; + +#ifdef STORM_HAVE_CARL + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template class StandardRewardModel; +#endif } } } \ No newline at end of file diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h index 52727ffad..d1c78cb15 100644 --- a/src/models/sparse/StandardRewardModel.h +++ b/src/models/sparse/StandardRewardModel.h @@ -64,6 +64,14 @@ namespace storm { * @return The state reward vector. */ std::vector const& getStateRewardVector() const; + + /*! + * Retrieves the state rewards of the reward model. Note that it is illegal to call this function if the + * reward model does not have state rewards. + * + * @return The state reward vector. + */ + std::vector& getStateRewardVector(); /*! * Retrieves an optional value that contains the state reward vector if there is one. @@ -86,6 +94,14 @@ namespace storm { * @return The state-action reward vector. */ std::vector const& getStateActionRewardVector() const; + + /*! + * Retrieves the state-action rewards of the reward model. Note that it is illegal to call this function + * if the reward model does not have state-action rewards. + * + * @return The state-action reward vector. + */ + std::vector& getStateActionRewardVector(); /*! * Retrieves an optional value that contains the state-action reward vector if there is one. @@ -108,7 +124,15 @@ namespace storm { * @return The transition reward matrix. */ storm::storage::SparseMatrix const& getTransitionRewardMatrix() const; - + + /*! + * Retrieves the transition rewards of the reward model. Note that it is illegal to call this function + * if the reward model does not have transition rewards. + * + * @return The transition reward matrix. + */ + storm::storage::SparseMatrix& getTransitionRewardMatrix(); + /*! * Retrieves an optional value that contains the transition reward matrix if there is one. * diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index acdde7b30..6158e3588 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -10,7 +10,7 @@ namespace storm { StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels, + std::unordered_map const& rewardModels, boost::optional> const& optionalPlayer1ChoiceLabeling, boost::optional> const& optionalPlayer2ChoiceLabeling) : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) { @@ -22,7 +22,7 @@ namespace storm { StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels, + std::unordered_map&& rewardModels, boost::optional>&& optionalPlayer1ChoiceLabeling, boost::optional>&& optionalPlayer2ChoiceLabeling) : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) { diff --git a/src/models/sparse/StochasticTwoPlayerGame.h b/src/models/sparse/StochasticTwoPlayerGame.h index 6bc33b4d7..d995c4695 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.h +++ b/src/models/sparse/StochasticTwoPlayerGame.h @@ -28,7 +28,7 @@ namespace storm { StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::map const& rewardModels = std::map(), + std::unordered_map const& rewardModels = std::map(), boost::optional> const& optionalPlayer1ChoiceLabeling = boost::optional>(), boost::optional> const& optionalPlayer2ChoiceLabeling = boost::optional>()); @@ -45,7 +45,7 @@ namespace storm { StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::map&& rewardModels = std::map(), + std::unordered_map&& rewardModels = std::map(), boost::optional>&& optionalPlayer1ChoiceLabeling = boost::optional>(), boost::optional>&& optionalPlayer2ChoiceLabeling = boost::optional>()); diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/models/symbolic/StandardRewardModel.h b/src/models/symbolic/StandardRewardModel.h new file mode 100644 index 000000000..adb65e384 --- /dev/null +++ b/src/models/symbolic/StandardRewardModel.h @@ -0,0 +1,36 @@ +#ifndef STORM_MODELS_SYMBOLIC_STANDARDREWARDMODEL_H_ +#define STORM_MODELS_SYMBOLIC_STANDARDREWARDMODEL_H_ + +#include + +namespace storm { + namespace models { + namespace symbolic { + + template + class StandardRewardModel { + /*! + * Builds a reward model by copying with the given reward structures. + * + * @param stateRewardVector The state reward vector. + * @param stateActionRewardVector The vector of state-action rewards. + * @param transitionRewardMatrix The matrix of transition rewards. + */ + explicit StandardRewardModel(boost::optional> const& stateRewardVector, boost::optional> const& stateActionRewardVector, boost::optional> const& transitionRewardMatrix); + + private: + // The state reward vector. + boost::optional> stateRewardVector; + + // A vector of state-action-based rewards. + boost::optional> stateActionRewardVector; + + // A matrix of transition rewards. + boost::optional> transitionRewardMatrix; + }; + + } + } +} + +#endif /* STORM_MODELS_SYMBOLIC_STANDARDREWARDMODEL_H_ */ \ No newline at end of file diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ddb348249..46466431b 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -114,14 +114,18 @@ namespace storm { stateRewardDefinition = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)]; + stateActionRewardDefinition = ((qi::lit("[") >> -(identifier[qi::_a = qi::_1]) >> qi::lit("]") >> expressionParser >> qi::lit(":")) > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)]; + stateActionRewardDefinition.name("state action reward definition"); + + transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_4, qi::_r1)]; transitionRewardDefinition.name("transition reward definition"); rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\"")) > +( stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)] - | transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_c, qi::_1)] + | stateActionRewardDefinition[phoenix::push_back(qi::_c, qi::_1)] + | transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_d, qi::_1)] ) - >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; + >> 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") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; @@ -346,24 +350,34 @@ namespace storm { return storm::prism::Label(labelName, expression, this->getFilename()); } - storm::prism::RewardModel PrismParser::createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) const { - return storm::prism::RewardModel(rewardModelName, stateRewards, transitionRewards, 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 { return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); } - storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { + storm::prism::StateActionReward PrismParser::createStateActionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName); STORM_LOG_THROW(actionName.empty() || nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'."); if (nameIndexPair == globalProgramInformation.actionIndices.end() && actionName.empty()) { - return storm::prism::TransitionReward(0, actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); + return storm::prism::StateActionReward(0, actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); } else { - return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); + return storm::prism::StateActionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); } } + storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression sourceStatePredicateExpression, storm::expressions::Expression targetStatePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { + auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName); + STORM_LOG_THROW(actionName.empty() || nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'."); + if (nameIndexPair == globalProgramInformation.actionIndices.end() && actionName.empty()) { + return storm::prism::TransitionReward(0, actionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); + } else { + return storm::prism::TransitionReward(nameIndexPair->second, actionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename()); + } + } + storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const { return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename()); } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 22510b4af..6cebd8a05 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -199,8 +199,9 @@ namespace storm { qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule, std::vector>, Skipper> rewardModelDefinition; + qi::rule, std::vector, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; + qi::rule, Skipper> stateActionRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; // Rules for initial states expression. @@ -236,9 +237,10 @@ namespace storm { storm::prism::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const; storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression); storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const; - storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) const; + storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards) const; storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; - storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::StateActionReward createStateActionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression sourceStatePredicateExpression, storm::expressions::Expression targetStatePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const; storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector const& assignments, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Command createCommand(bool markovianCommand, std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const; diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp index 6e13cb695..9b1213f2b 100644 --- a/src/storage/prism/RewardModel.cpp +++ b/src/storage/prism/RewardModel.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { + RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), rewardModelName(rewardModelName), stateRewards(stateRewards), stateActionRewards(stateActionRewards), transitionRewards(transitionRewards) { // Nothing to do here. } @@ -15,15 +15,23 @@ namespace storm { } bool RewardModel::hasStateRewards() const { - return this->stateRewards.size() > 0; + return !this->stateRewards.empty(); } std::vector const& RewardModel::getStateRewards() const { return this->stateRewards; } + bool RewardModel::hasStateActionRewards() const { + return !this->stateActionRewards.empty(); + } + + std::vector const& RewardModel::getStateActionRewards() const { + return this->stateActionRewards; + } + bool RewardModel::hasTransitionRewards() const { - return this->transitionRewards.size() > 0; + return !this->transitionRewards.empty(); } std::vector const& RewardModel::getTransitionRewards() const { @@ -36,13 +44,19 @@ namespace storm { for (auto const& stateReward : this->getStateRewards()) { newStateRewards.emplace_back(stateReward.substitute(substitution)); } + + std::vector newStateActionRewards; + newStateActionRewards.reserve(this->getStateRewards().size()); + for (auto const& stateActionReward : this->getStateActionRewards()) { + newStateActionRewards.emplace_back(stateActionReward.substitute(substitution)); + } std::vector newTransitionRewards; newTransitionRewards.reserve(this->getTransitionRewards().size()); for (auto const& transitionReward : this->getTransitionRewards()) { newTransitionRewards.emplace_back(transitionReward.substitute(substitution)); } - return RewardModel(this->getName(), newStateRewards, newTransitionRewards, this->getFilename(), this->getLineNumber()); + return RewardModel(this->getName(), newStateRewards, newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber()); } bool RewardModel::containsVariablesOnlyInRewardValueExpressions(std::set const& undefinedConstantVariables) const { @@ -51,8 +65,16 @@ namespace storm { return false; } } + for (auto const& stateActionReward : this->getStateActionRewards()) { + if (stateActionReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) { + return false; + } + } for (auto const& transitionReward : this->getTransitionRewards()) { - if (transitionReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) { + if (transitionReward.getSourceStatePredicateExpression().containsVariable(undefinedConstantVariables)) { + return false; + } + if (transitionReward.getTargetStatePredicateExpression().containsVariable(undefinedConstantVariables)) { return false; } } @@ -68,6 +90,9 @@ namespace storm { for (auto const& reward : rewardModel.getStateRewards()) { stream << reward << std::endl; } + for (auto const& reward : rewardModel.getStateActionRewards()) { + stream << reward << std::endl; + } for (auto const& reward : rewardModel.getTransitionRewards()) { stream << reward << std::endl; } diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h index f8586b9a9..c62aff61a 100644 --- a/src/storage/prism/RewardModel.h +++ b/src/storage/prism/RewardModel.h @@ -6,6 +6,7 @@ #include #include "src/storage/prism/StateReward.h" +#include "src/storage/prism/StateActionReward.h" #include "src/storage/prism/TransitionReward.h" #include "src/utility/OsDetection.h" @@ -18,11 +19,12 @@ namespace storm { * * @param rewardModelName The name of the reward model. * @param stateRewards A vector of state-based rewards. + * @param stateActionRewards A vector of state-action-based rewards. * @param transitionRewards A vector of transition-based rewards. * @param filename The filename in which the reward model is defined. * @param lineNumber The line number in which the reward model is defined. */ - RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards, std::string const& filename = "", uint_fast64_t lineNumber = 0); + RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& stateActionRewards, std::vector const& transitionRewards, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. RewardModel() = default; @@ -60,6 +62,20 @@ namespace storm { * @return The state rewards associated with this reward model. */ std::vector const& getStateRewards() const; + + /*! + * Retrieves whether there are any state-action rewards. + * + * @return True iff there are any state-action rewards. + */ + bool hasStateActionRewards() const; + + /*! + * Retrieves all state-action rewards associated with this reward model. + * + * @return The state-action rewards associated with this reward model. + */ + std::vector const& getStateActionRewards() const; /*! * Retrieves whether there are any transition rewards. @@ -100,6 +116,9 @@ namespace storm { // The state-based rewards associated with this reward model. std::vector stateRewards; + + // The state-action-based rewards associated with this reward model. + std::vector stateActionRewards; // The transition-based rewards associated with this reward model. std::vector transitionRewards; diff --git a/src/storage/prism/StateActionReward.cpp b/src/storage/prism/StateActionReward.cpp new file mode 100644 index 000000000..e768a532f --- /dev/null +++ b/src/storage/prism/StateActionReward.cpp @@ -0,0 +1,40 @@ +#include "src/storage/prism/StateActionReward.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace prism { + StateActionReward::StateActionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { + // Nothing to do here. + } + + std::string const& StateActionReward::getActionName() const { + return this->actionName; + } + + uint_fast64_t StateActionReward::getActionIndex() const { + return this->actionIndex; + } + + storm::expressions::Expression const& StateActionReward::getStatePredicateExpression() const { + return this->statePredicateExpression; + } + + storm::expressions::Expression const& StateActionReward::getRewardValueExpression() const { + return this->rewardValueExpression; + } + + bool StateActionReward::isLabeled() const { + return labeled; + } + + StateActionReward StateActionReward::substitute(std::map const& substitution) const { + return StateActionReward(this->getActionIndex(), this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + } + + std::ostream& operator<<(std::ostream& stream, StateActionReward const& stateActionReward) { + stream << "\t[" << StateActionReward.getActionName() << "] " << stateActionReward.getStatePredicateExpression() << ": " << stateActionReward.getRewardValueExpression() << ";"; + return stream; + } + + } // namespace prism +} // namespace storm diff --git a/src/storage/prism/StateActionReward.h b/src/storage/prism/StateActionReward.h new file mode 100644 index 000000000..cc4bbfa17 --- /dev/null +++ b/src/storage/prism/StateActionReward.h @@ -0,0 +1,112 @@ +#ifndef STORM_STORAGE_PRISM_STATEACTIONREWARD_H_ +#define STORM_STORAGE_PRISM_STATEACTIONREWARD_H_ + +#include + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" +#include "src/utility/OsDetection.h" + + +namespace storm { + namespace storage { + namespace expressions { + class Variable; + } + } +} + +namespace storm { + namespace prism { + class StateActionReward : public LocatedInformation { + public: + /*! + * Creates a transition reward for the transitions with the given name emanating from states satisfying the + * given expression with the value given by another expression. + * + * @param actionIndex The index of the action. + * @param actionName The name of the command that obtains this reward. + * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously + * specified name in order to obtain the reward. + * @param rewardValueExpression An expression specifying the values of the rewards to attach to the transitions. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. + */ + StateActionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + StateActionReward() = default; + StateActionReward(StateActionReward const& other) = default; + StateActionReward& operator=(StateActionReward const& other)= default; +#ifndef WINDOWS + StateActionReward(StateActionReward&& other) = default; + StateActionReward& operator=(StateActionReward&& other) = default; +#endif + + /*! + * Retrieves the action name that is associated with this transition reward. + * + * @return The action name that is associated with this transition reward. + */ + std::string const& getActionName() const; + + /*! + * Retrieves the action index of the action associated with this transition reward (if any). + * + * @return The action index of the transition reward. + */ + uint_fast64_t getActionIndex() const; + + /*! + * Retrieves the state predicate expression that is associated with this state reward. + * + * @return The state predicate expression that is associated with this state reward. + */ + storm::expressions::Expression const& getStatePredicateExpression() const; + + /*! + * Retrieves the reward value expression associated with this state reward. + * + * @return The reward value expression associated with this state reward. + */ + storm::expressions::Expression const& getRewardValueExpression() const; + + /*! + * Retrieves whether the transition reward has an action label. + * + * @return True iff the transition reward has an action label. + */ + bool isLabeled() const; + + /*! + * Substitutes all identifiers in the transition reward according to the given map. + * + * @param substitution The substitution to perform. + * @return The resulting transition reward. + */ + StateActionReward substitute(std::map const& substitution) const; + + friend std::ostream& operator<<(std::ostream& stream, StateActionReward const& stateActionReward); + + private: + // The index of the action name. + uint_fast64_t actionIndex; + + // The name of the command this transition-based reward is attached to. + std::string actionName; + + // A flag that stores whether the transition reward has an action label. + bool labeled; + + // A predicate that needs to be satisfied by states for the reward to be obtained (by taking + // a corresponding command transition). + storm::expressions::Expression statePredicateExpression; + + // The expression specifying the value of the reward obtained along the transitions. + storm::expressions::Expression rewardValueExpression; + }; + + } // namespace prism +} // namespace storm + +#endif /* STORM_STORAGE_PRISM_STATEACTIONREWARD_H_ */ diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp index aadaf7a90..2a405d7a5 100644 --- a/src/storage/prism/TransitionReward.cpp +++ b/src/storage/prism/TransitionReward.cpp @@ -3,7 +3,7 @@ namespace storm { namespace prism { - TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { + TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& sourceStatePredicateExpression, storm::expressions::Expression const& targetStatePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), labeled(actionName != ""), sourceStatePredicateExpression(sourceStatePredicateExpression), targetStatePredicateExpression(targetStatePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. } @@ -15,10 +15,14 @@ namespace storm { return this->actionIndex; } - storm::expressions::Expression const& TransitionReward::getStatePredicateExpression() const { - return this->statePredicateExpression; + storm::expressions::Expression const& TransitionReward::getSourceStatePredicateExpression() const { + return this->sourceStatePredicateExpression; } - + + storm::expressions::Expression const& TransitionReward::getTargetStatePredicateExpression() const { + return this->targetStatePredicateExpression; + } + storm::expressions::Expression const& TransitionReward::getRewardValueExpression() const { return this->rewardValueExpression; } @@ -28,11 +32,11 @@ namespace storm { } TransitionReward TransitionReward::substitute(std::map const& substitution) const { - return TransitionReward(this->getActionIndex(), this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return TransitionReward(this->getActionIndex(), this->getActionName(), this->getSourceStatePredicateExpression().substitute(substitution), this->getTargetStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) { - stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";"; + stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getSourceStatePredicateExpression() << " -> " << transitionReward.getTargetStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";"; return stream; } diff --git a/src/storage/prism/TransitionReward.h b/src/storage/prism/TransitionReward.h index 8ace7c71c..5dd43b65f 100644 --- a/src/storage/prism/TransitionReward.h +++ b/src/storage/prism/TransitionReward.h @@ -27,13 +27,15 @@ namespace storm { * * @param actionIndex The index of the action. * @param actionName The name of the command that obtains this reward. - * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously - * specified name in order to obtain the reward. + * @param sourceStatePredicateExpression The predicate that needs to hold before taking a transition with + * the previously specified name in order to obtain the reward. + * @param targetStatePredicateExpression The predicate that needs to hold after taking a transition with + * the previously specified name in order to obtain the reward. * @param rewardValueExpression An expression specifying the values of the rewards to attach to the transitions. * @param filename The filename in which the transition reward is defined. * @param lineNumber The line number in which the transition reward is defined. */ - TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& sourceStatePredicateExpression, storm::expressions::Expression const& targetStatePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. TransitionReward() = default; @@ -59,11 +61,18 @@ namespace storm { uint_fast64_t getActionIndex() const; /*! - * Retrieves the state predicate expression that is associated with this state reward. + * Retrieves the source state predicate expression that is associated with this state reward. * - * @return The state predicate expression that is associated with this state reward. + * @return The source state predicate expression that is associated with this state reward. */ - storm::expressions::Expression const& getStatePredicateExpression() const; + storm::expressions::Expression const& getSourceStatePredicateExpression() const; + + /*! + * Retrieves the target state predicate expression that is associated with this state reward. + * + * @return The target state predicate expression that is associated with this state reward. + */ + storm::expressions::Expression const& getTargetStatePredicateExpression() const; /*! * Retrieves the reward value expression associated with this state reward. @@ -99,9 +108,11 @@ namespace storm { // A flag that stores whether the transition reward has an action label. bool labeled; - // A predicate that needs to be satisfied by states for the reward to be obtained (by taking - // a corresponding command transition). - storm::expressions::Expression statePredicateExpression; + // A predicate that needs to be satisfied in the source state of transitions that can earn the reward. + storm::expressions::Expression sourceStatePredicateExpression; + + // A predicate that needs to be satisfied in the target state of transitions that can earn the reward. + storm::expressions::Expression targetStatePredicateExpression; // The expression specifying the value of the reward obtained along the transitions. storm::expressions::Expression rewardValueExpression; diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index efa026c7e..f35075a58 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -215,7 +215,6 @@ namespace storm { program = storm::parser::PrismParser::parse(programFile).simplify(); program->checkValidity(); - std::cout << program.get() << std::endl; } // Then proceed to parsing the property (if given), since the model we are building may depend on the property.