diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp new file mode 100644 index 000000000..fc213467a --- /dev/null +++ b/src/generator/JaniNextStateGenerator.cpp @@ -0,0 +1,89 @@ +//#include "src/generator/JaniNextStateGenerator.h" +// +//#include "src/models/sparse/StateLabeling.h" +// +//#include "src/storage/expressions/SimpleValuation.h" +// +//#include "src/utility/constants.h" +//#include "src/utility/macros.h" +//#include "src/exceptions/InvalidSettingsException.h" +//#include "src/exceptions/WrongFormatException.h" +// +//namespace storm { +// namespace generator { +// +// template +// JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : NextStateGenerator(options), model(model.substituteConstants()), variableInformation(this->model), evaluator(this->model.getManager()), state(nullptr), comparator() { +// STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); +// STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models."); +// +// // If there are terminal states we need to handle, we now need to translate all labels to expressions. +// if (this->options.hasTerminalStates()) { +// for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { +// if (expressionOrLabelAndBool.first.isExpression()) { +// terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); +// } else { +// STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models."); +// } +// } +// } +// } +// +// template +// uint64_t JaniNextStateGenerator::getStateSize() const { +// return variableInformation.getTotalBitOffset(true); +// } +// +// template +// ModelType JaniNextStateGenerator::getModelType() const { +// switch (model.getModelType()) { +// case storm::jani::ModelType::DTMC: return ModelType::DTMC; +// case storm::jani::ModelType::CTMC: return ModelType::CTMC; +// case storm::jani::ModelType::MDP: return ModelType::MDP; +// case storm::jani::ModelType::MA: return ModelType::MA; +// default: +// STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); +// } +// } +// +// template +// bool JaniNextStateGenerator::isDeterministicModel() const { +// return model.isDeterministicModel(); +// } +// +// template +// std::vector JaniNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { +// // FIXME: This only works for models with exactly one initial state. We should make this more general. +// CompressedState initialState(variableInformation.getTotalBitOffset()); +// +// // We need to initialize the values of the variables to their initial value. +// for (auto const& booleanVariable : variableInformation.booleanVariables) { +// initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); +// } +// for (auto const& integerVariable : variableInformation.integerVariables) { +// initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); +// } +// +// // Register initial state and return it. +// StateType id = stateToIdCallback(initialState); +// return {id}; +// } +// +// template +// void JaniNextStateGenerator::load(CompressedState const& state) { +// // Since almost all subsequent operations are based on the evaluator, we load the state into it now. +// unpackStateIntoEvaluator(state, variableInformation, evaluator); +// +// // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. +// this->state = &state; +// } +// +// template +// bool JaniNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { +// if (expression.isTrue()) { +// return true; +// } +// return evaluator.asBool(expression); +// } +// } +//} \ No newline at end of file diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h new file mode 100644 index 000000000..b93f5a9db --- /dev/null +++ b/src/generator/JaniNextStateGenerator.h @@ -0,0 +1,68 @@ +//#pragma once +// +//#include "src/generator/NextStateGenerator.h" +//#include "src/generator/VariableInformation.h" +// +//#include "src/storage/jani/Model.h" +//#include "src/storage/expressions/ExpressionEvaluator.h" +// +//#include "src/utility/ConstantsComparator.h" +// +//namespace storm { +// namespace generator { +// +// template +// class JaniNextStateGenerator : public NextStateGenerator { +// public: +// typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; +// +// JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); +// +// virtual uint64_t getStateSize() const override; +// virtual ModelType getModelType() const override; +// virtual bool isDeterministicModel() const override; +// virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; +// +// virtual void load(CompressedState const& state) override; +// virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; +// virtual bool satisfies(storm::expressions::Expression const& expression) const override; +// +// virtual std::size_t getNumberOfRewardModels() const override; +// virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; +// +// virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override; +// +// virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; +// +// private: +// /*! +// * Applies an update to the state currently loaded into the evaluator and applies the resulting values to +// * the given compressed state. +// * @params state The state to which to apply the new values. +// * @params update The update to apply. +// * @return The resulting state. +// */ +// CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update); +// +// /*! +// * Retrieves all choices labeled with the silent action possible from the given state. +// * +// * @param state The state for which to retrieve the silent choices. +// * @return The silent action choices of the state. +// */ +// std::vector> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); +// +// /*! +// * Retrieves all choices labeled with some non-silent action possible from the given state. +// * +// * @param state The state for which to retrieve the non-silent choices. +// * @return The non-silent action choices of the state. +// */ +// std::vector> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); +// +// // The model used for the generation of next states. +// storm::jani::Model model; +// }; +// +// } +//} \ No newline at end of file diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 547b76c15..6e9f67fa6 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -4,6 +4,11 @@ #include "src/logic/Formulas.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/SimpleValuation.h" + +#include "src/models/sparse/StateLabeling.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidSettingsException.h" @@ -207,15 +212,82 @@ namespace storm { } template - NextStateGenerator::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) { + NextStateGenerator::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) { // Intentionally left empty. } - + template NextStateGeneratorOptions const& NextStateGenerator::getOptions() const { return options; } + template + uint64_t NextStateGenerator::getStateSize() const { + return variableInformation.getTotalBitOffset(true); + } + + template + void NextStateGenerator::load(CompressedState const& state) { + // Since almost all subsequent operations are based on the evaluator, we load the state into it now. + unpackStateIntoEvaluator(state, variableInformation, evaluator); + + // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. + this->state = &state; + } + + template + bool NextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { + if (expression.isTrue()) { + return true; + } + return evaluator.asBool(expression); + } + + template + storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector> labelsAndExpressions) { + // Make the labels unique. + std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; } ); + auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair const& a, std::pair const& b) { return a.first == b.first; } ); + labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it)); + + for (auto const& expression : this->options.getExpressionLabels()) { + std::stringstream stream; + stream << expression; + labelsAndExpressions.push_back(std::make_pair(stream.str(), expression)); + } + + // Prepare result. + storm::models::sparse::StateLabeling result(states.size()); + + // Initialize labeling. + for (auto const& label : labelsAndExpressions) { + result.addLabel(label.first); + } + for (auto const& stateIndexPair : states) { + unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator); + + for (auto const& label : labelsAndExpressions) { + // Add label to state, if the corresponding expression is true. + if (evaluator.asBool(label.second)) { + result.addLabelToState(label.first, stateIndexPair.second); + } + } + } + + // Also label the initial state with the special label "init". + result.addLabel("init"); + for (auto index : initialStateIndices) { + result.addLabelToState("init", index); + } + + return result; + } + + template + storm::expressions::SimpleValuation NextStateGenerator::toValuation(CompressedState const& state) const { + return unpackStateIntoValuation(state, variableInformation, *expressionManager); + } + template class NextStateGenerator; template class NextStateGenerator; diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 668b2f0be..7e5c1e869 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -8,13 +8,18 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/BitVectorHashMap.h" +#include "src/storage/expressions/ExpressionEvaluator.h" +#include "src/generator/VariableInformation.h" #include "src/generator/CompressedState.h" #include "src/generator/StateBehavior.h" +#include "src/utility/ConstantsComparator.h" + namespace storm { namespace expressions { class Expression; + class ExpressionManager; } namespace models { @@ -155,28 +160,52 @@ namespace storm { public: typedef std::function StateToIdCallback; - NextStateGenerator(NextStateGeneratorOptions const& options); + NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options); - virtual uint64_t getStateSize() const = 0; + uint64_t getStateSize() const; virtual ModelType getModelType() const = 0; virtual bool isDeterministicModel() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; - virtual void load(CompressedState const& state) = 0; + void load(CompressedState const& state); virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; - virtual bool satisfies(storm::expressions::Expression const& expression) const = 0; + bool satisfies(storm::expressions::Expression const& expression) const; virtual std::size_t getNumberOfRewardModels() const = 0; virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; - virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const = 0; + storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; protected: + /*! + * Creates the state labeling for the given states using the provided labels and expressions. + */ + storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector> labelsAndExpressions); + + /// The options to be used for next-state generation. NextStateGeneratorOptions options; + + /// The expression manager used for evaluating expressions. + std::shared_ptr expressionManager; + + /// The expressions that define terminal states. + std::vector> terminalStates; + + /// Information about how the variables are packed. + VariableInformation variableInformation; + + /// An evaluator used to evaluate expressions. + storm::expressions::ExpressionEvaluator evaluator; + + /// The currently loaded state. + CompressedState const* state; + + /// A comparator used to compare constants. + storm::utility::ConstantsComparator comparator; }; } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 5e4a1d6ed..c1e70e1ab 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -15,7 +15,12 @@ namespace storm { namespace generator { template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator(options), program(program.substituteConstants()), rewardModels(), variableInformation(this->program), evaluator(this->program.getManager()), state(nullptr), comparator() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator(program.substituteConstants(), options, false) { + // Intentionally left empty. + } + + template + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), VariableInformation(program), options), program(program.substituteConstants()), rewardModels() { STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); if (this->options.isBuildAllRewardModelsSet()) { @@ -50,19 +55,14 @@ namespace storm { if (this->options.hasTerminalStates()) { for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { if (expressionOrLabelAndBool.first.isExpression()) { - terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); + this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); } else { - terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second)); + this->terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second)); } } } } - - template - uint64_t PrismNextStateGenerator::getStateSize() const { - return variableInformation.getTotalBitOffset(true); - } - + template ModelType PrismNextStateGenerator::getModelType() const { switch (program.getModelType()) { @@ -83,13 +83,13 @@ namespace storm { template std::vector PrismNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { // FIXME: This only works for models with exactly one initial state. We should make this more general. - CompressedState initialState(variableInformation.getTotalBitOffset()); + CompressedState initialState(this->variableInformation.getTotalBitOffset()); // We need to initialize the values of the variables to their initial value. - for (auto const& booleanVariable : variableInformation.booleanVariables) { + for (auto const& booleanVariable : this->variableInformation.booleanVariables) { initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); } - for (auto const& integerVariable : variableInformation.integerVariables) { + for (auto const& integerVariable : this->variableInformation.integerVariables) { initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); } @@ -98,23 +98,6 @@ namespace storm { return {id}; } - template - void PrismNextStateGenerator::load(CompressedState const& state) { - // Since almost all subsequent operations are based on the evaluator, we load the state into it now. - unpackStateIntoEvaluator(state, variableInformation, evaluator); - - // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it. - this->state = &state; - } - - template - bool PrismNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { - if (expression.isTrue()) { - return true; - } - return evaluator.asBool(expression); - } - template StateBehavior PrismNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { // Prepare the result, in case we return early. @@ -126,8 +109,8 @@ namespace storm { ValueType stateRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateRewards()) { for (auto const& stateReward : rewardModel.get().getStateRewards()) { - if (evaluator.asBool(stateReward.getStatePredicateExpression())) { - stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); + if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) { + stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression())); } } } @@ -135,9 +118,9 @@ namespace storm { } // If a terminal expression was set and we must not expand this state, return now. - if (!terminalStates.empty()) { - for (auto const& expressionBool : terminalStates) { - if (evaluator.asBool(expressionBool.first) == expressionBool.second) { + if (!this->terminalStates.empty()) { + for (auto const& expressionBool : this->terminalStates) { + if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) { return result; } } @@ -191,8 +174,8 @@ namespace storm { if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { for (auto const& choice : allChoices) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; } } @@ -223,21 +206,21 @@ namespace storm { auto assignmentIte = update.getAssignments().end(); // Iterate over all boolean assignments and carry them out. - auto boolIt = variableInformation.booleanVariables.begin(); + auto boolIt = this->variableInformation.booleanVariables.begin(); for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { while (assignmentIt->getVariable() != boolIt->variable) { ++boolIt; } - newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression())); + newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression())); } // Iterate over all integer assignments and carry them out. - auto integerIt = variableInformation.integerVariables.begin(); + auto integerIt = this->variableInformation.integerVariables.begin(); for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { while (assignmentIt->getVariable() != integerIt->variable) { ++integerIt; } - int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); + int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); @@ -275,7 +258,7 @@ namespace storm { // Look up commands by their indices and add them if the guard evaluates to true in the given state. for (uint_fast64_t commandIndex : commandIndices) { storm::prism::Command const& command = module.getCommand(commandIndex); - if (evaluator.asBool(command.getGuardExpression())) { + if (this->evaluator.asBool(command.getGuardExpression())) { commands.push_back(command); } } @@ -308,7 +291,7 @@ namespace storm { if (command.isLabeled()) continue; // Skip the command, if it is not enabled. - if (!evaluator.asBool(command.getGuardExpression())) { + if (!this->evaluator.asBool(command.getGuardExpression())) { continue; } @@ -330,7 +313,7 @@ namespace storm { StateType stateIndex = stateToIdCallback(applyUpdate(state, update)); // Update the choice by adding the probability/target state to it. - ValueType probability = evaluator.asRational(update.getLikelihoodExpression()); + ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression()); choice.addProbability(stateIndex, probability); probabilitySum += probability; } @@ -340,8 +323,8 @@ namespace storm { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); } } } @@ -349,7 +332,7 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } } @@ -395,9 +378,9 @@ namespace storm { // and otherwise insert it. auto targetStateIt = newTargetStates->find(newTargetState); if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()); + targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()); } else { - newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression())); } } } @@ -435,15 +418,15 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + STORM_LOG_THROW(!program.isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); // Create the state-action reward for the newly created choice. for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { - if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); + if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { + stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); } } } @@ -476,7 +459,7 @@ namespace storm { template storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { - // Gather a vector of labels and their expressions so we can iterate it over it a lot. + // Gather a vector of labels and their expressions. std::vector> labels; if (this->options.isBuildAllLabelsSet()) { for (auto const& label : program.getLabels()) { @@ -487,43 +470,8 @@ namespace storm { labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName))); } } - - // Make the labels unique. - std::sort(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; } ); - auto it = std::unique(labels.begin(), labels.end(), [] (std::pair const& a, std::pair const& b) { return a.first == b.first; } ); - labels.resize(std::distance(labels.begin(), it)); - - for (auto const& expression : this->options.getExpressionLabels()) { - std::stringstream stream; - stream << expression; - labels.push_back(std::make_pair(stream.str(), expression)); - } - - // Prepare result. - storm::models::sparse::StateLabeling result(states.size()); - - // Initialize labeling. - for (auto const& label : labels) { - result.addLabel(label.first); - } - for (auto const& stateIndexPair : states) { - unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator); - - for (auto const& label : labels) { - // Add label to state, if the corresponding expression is true. - if (evaluator.asBool(label.second)) { - result.addLabelToState(label.first, stateIndexPair.second); - } - } - } - // Also label the initial state with the special label "init". - result.addLabel("init"); - for (auto index : initialStateIndices) { - result.addLabelToState("init", index); - } - - return result; + return NextStateGenerator::label(states, initialStateIndices, labels); } template @@ -536,12 +484,7 @@ namespace storm { storm::prism::RewardModel const& rewardModel = rewardModels[index].get(); return RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards()); } - - template - storm::expressions::SimpleValuation PrismNextStateGenerator::toValuation(CompressedState const& state) const { - return unpackStateIntoValuation(state, variableInformation, program.getManager()); - } - + template class PrismNextStateGenerator; template class PrismNextStateGenerator; } diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index c3d3c63d9..273ac5bf6 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -2,12 +2,8 @@ #define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ #include "src/generator/NextStateGenerator.h" -#include "src/generator/VariableInformation.h" #include "src/storage/prism/Program.h" -#include "src/storage/expressions/ExpressionEvaluator.h" - -#include "src/utility/ConstantsComparator.h" namespace storm { namespace generator { @@ -19,23 +15,25 @@ namespace storm { PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); - virtual uint64_t getStateSize() const override; virtual ModelType getModelType() const override; virtual bool isDeterministicModel() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; - virtual void load(CompressedState const& state) override; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; - virtual bool satisfies(storm::expressions::Expression const& expression) const override; virtual std::size_t getNumberOfRewardModels() const override; virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; private: + /*! + * A delegate constructor that is used to preprocess the program before the constructor of the superclass is + * being called. The last argument is only present to distinguish the signature of this constructor from the + * public one. + */ + PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag); + /*! * Applies an update to the state currently loaded into the evaluator and applies the resulting values to * the given compressed state. @@ -85,23 +83,8 @@ namespace storm { // The reward models that need to be considered. std::vector> rewardModels; - // The expressions that define terminal states. - std::vector> terminalStates; - // A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; - - // Information about how the variables are packed. - VariableInformation variableInformation; - - // An evaluator used to evaluate expressions. - storm::expressions::ExpressionEvaluator evaluator; - - // The currently loaded state. - CompressedState const* state; - - // A comparator used to compare constants. - storm::utility::ConstantsComparator comparator; }; } diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 29b0d9dd6..a8f442571 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -353,6 +353,10 @@ namespace storm { this->initialStatesExpression = initialStatesExpression; } + bool Model::isDeterministicModel() const { + return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC; + } + bool Model::checkValidity(bool logdbg) const { // TODO switch to exception based return value. diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 460fb50c1..b826763eb 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -243,6 +243,11 @@ namespace storm { */ void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression); + /*! + * Determines whether this model is a deterministic one in the sense that each state only has one choice. + */ + bool isDeterministicModel() const; + /*! * Checks if the model is valid JANI, which should be verified before any further operations are applied to a model. */