Browse Source

a little morning code

Former-commit-id: 9cb63427c6
tempestpy_adaptions
dehnert 9 years ago
parent
commit
865345c7bf
  1. 4
      src/generator/NextStateGenerator.h
  2. 7
      src/generator/PrismNextStateGenerator.cpp
  3. 21
      src/generator/PrismNextStateGenerator.h
  4. 17
      src/generator/StateBehavior.cpp
  5. 35
      src/generator/StateBehavior.h

4
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<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
virtual std::vector<Choice<ValueType>> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0;
virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0;
};
}
}

7
src/generator/PrismNextStateGenerator.cpp

@ -18,7 +18,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, typename NextStateGenerator<ValueType, StateType>::StateToIdCallback stateToIdCallback) {
StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, typename NextStateGenerator<ValueType, StateType>::StateToIdCallback stateToIdCallback) {
// TODO
}
@ -34,11 +34,6 @@ namespace storm {
template<typename ValueType, typename StateType>
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
return applyUpdate(variableInformation, state, state, update);
}
template<typename ValueType, typename StateType>
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update) {
CompressedState newState(state);
auto assignmentIt = update.getAssignments().begin();

21
src/generator/PrismNextStateGenerator.h

@ -23,7 +23,7 @@ namespace storm {
void addRewardModel(storm::prism::RewardModel const& rewardModel);
virtual std::vector<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
virtual std::vector<Choice<ValueType>> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) override;
virtual StateBehavior<ValueType, StateType> 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.

17
src/generator/StateBehavior.cpp

@ -0,0 +1,17 @@
#include "src/generator/StateBehavior.h"
namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
void StateBehavior<ValueType, StateType>::addChoice(Choice<ValueType, StateType>&& choice) {
choices.push_back(std::move(choice));
}
template<typename ValueType, typename StateType>
void StateBehavior<ValueType, StateType>::addStateReward(ValueType const& stateReward) {
stateRewards.push_back(stateReward);
}
}
}

35
src/generator/StateBehavior.h

@ -0,0 +1,35 @@
#ifndef STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
#define STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_
#include <cstdint>
#include "src/generator/Choice.h"
namespace storm {
namespace generator {
template<typename ValueType, typename StateType = uint32_t>
class StateBehavior {
public:
/*!
* Adds the given choice to the behavior of the state.
*/
void addChoice(Choice<ValueType, StateType>&& 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<Choice<ValueType, StateType>> choices;
// The state rewards (under the different, selected reward models) of the state.
std::vector<ValueType> stateRewards;
};
}
}
#endif /* STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ */
Loading…
Cancel
Save