From 865345c7bf69a3dd6c208aa016d55d0d03145ff8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 24 Feb 2016 10:27:52 +0100 Subject: [PATCH] a little morning code Former-commit-id: 9cb63427c66ed48e3454d1e221a4a02cf60e5514 --- src/generator/NextStateGenerator.h | 4 +-- src/generator/PrismNextStateGenerator.cpp | 7 +---- src/generator/PrismNextStateGenerator.h | 21 +++----------- src/generator/StateBehavior.cpp | 17 +++++++++++ src/generator/StateBehavior.h | 35 +++++++++++++++++++++++ 5 files changed, 59 insertions(+), 25 deletions(-) create mode 100644 src/generator/StateBehavior.cpp create mode 100644 src/generator/StateBehavior.h diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index cf89bd1e6..8e8e4bbdb 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -7,7 +7,7 @@ #include "src/storage/sparse/StateType.h" #include "src/storage/BitVector.h" -#include "src/generator/Choice.h" +#include "src/generator/StateBehavior.h" namespace storm { namespace generator { @@ -19,7 +19,7 @@ namespace storm { typedef StateType (*StateToIdCallback)(CompressedState const&); virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; - virtual std::vector> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0; + virtual StateBehavior expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0; }; } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index f49aa1b29..a23ed29a6 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -18,7 +18,7 @@ namespace storm { } template - std::vector> PrismNextStateGenerator::expand(CompressedState const& state, typename NextStateGenerator::StateToIdCallback stateToIdCallback) { + StateBehavior PrismNextStateGenerator::expand(CompressedState const& state, typename NextStateGenerator::StateToIdCallback stateToIdCallback) { // TODO } @@ -34,11 +34,6 @@ namespace storm { template CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, storm::prism::Update const& update) { - return applyUpdate(variableInformation, state, state, update); - } - - template - CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update) { CompressedState newState(state); auto assignmentIt = update.getAssignments().begin(); diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index f5fabe5f7..d3660ce05 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -23,7 +23,7 @@ namespace storm { void addRewardModel(storm::prism::RewardModel const& rewardModel); virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; - virtual std::vector> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) override; + virtual StateBehavior expand(CompressedState const& state, StateToIdCallback stateToIdCallback) override; private: /*! @@ -34,27 +34,14 @@ namespace storm { void unpackStateIntoEvaluator(CompressedState const& state); /*! - * Applies an update to the given state and returns the resulting new state object. This methods does not - * modify the given state but returns a new one. - * - * @params state The state to which to apply the update. + * 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::prism::Update const& update); - /*! - * Applies an update to the given state and returns the resulting new state object. The update is evaluated - * over the variable values of the given base state. This methods does not modify the given state but - * returns a new one. - * - * @param state The state to which to apply the update. - * @param baseState The state used for evaluating the update. - * @param update The update to apply. - * @return The resulting state. - */ - CompressedState applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update); - /*! * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by * modules. diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp new file mode 100644 index 000000000..5868a1e40 --- /dev/null +++ b/src/generator/StateBehavior.cpp @@ -0,0 +1,17 @@ +#include "src/generator/StateBehavior.h" + +namespace storm { + namespace generator { + + template + void StateBehavior::addChoice(Choice&& choice) { + choices.push_back(std::move(choice)); + } + + template + void StateBehavior::addStateReward(ValueType const& stateReward) { + stateRewards.push_back(stateReward); + } + + } +} \ No newline at end of file diff --git a/src/generator/StateBehavior.h b/src/generator/StateBehavior.h new file mode 100644 index 000000000..b4feecb34 --- /dev/null +++ b/src/generator/StateBehavior.h @@ -0,0 +1,35 @@ +#ifndef STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ +#define STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ + +#include + +#include "src/generator/Choice.h" + +namespace storm { + namespace generator { + + template + class StateBehavior { + public: + /*! + * Adds the given choice to the behavior of the state. + */ + void addChoice(Choice&& choice); + + /*! + * Adds the given state reward to the behavior of the state. + */ + void addStateReward(ValueType const& stateReward); + + private: + // The choices available in the state. + std::vector> choices; + + // The state rewards (under the different, selected reward models) of the state. + std::vector stateRewards; + }; + + } +} + +#endif /* STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ */