dehnert
9 years ago
51 changed files with 2107 additions and 1188 deletions
-
2src/CMakeLists.txt
-
858src/builder/ExplicitPrismModelBuilder.cpp
-
181src/builder/ExplicitPrismModelBuilder.h
-
22src/builder/ExplorationOrder.cpp
-
17src/builder/ExplorationOrder.h
-
105src/generator/Choice.cpp
-
150src/generator/Choice.h
-
23src/generator/CompressedState.cpp
-
30src/generator/CompressedState.h
-
24src/generator/NextStateGenerator.h
-
404src/generator/PrismNextStateGenerator.cpp
-
108src/generator/PrismNextStateGenerator.h
-
50src/generator/PrismStateLabelingGenerator.cpp
-
31src/generator/PrismStateLabelingGenerator.h
-
57src/generator/StateBehavior.cpp
-
73src/generator/StateBehavior.h
-
20src/generator/StateLabelingGenerator.h
-
77src/generator/VariableInformation.cpp
-
75src/generator/VariableInformation.h
-
4src/parser/PrismParser.cpp
-
14src/settings/ArgumentValidators.h
-
21src/settings/modules/GeneralSettings.cpp
-
19src/settings/modules/GeneralSettings.h
-
246src/storage/BitVector.cpp
-
9src/storage/BitVector.h
-
7src/storage/BitVectorHashMap.cpp
-
9src/storage/BitVectorHashMap.h
-
62src/storage/Distribution.cpp
-
34src/storage/Distribution.h
-
209src/storage/SparseMatrix.cpp
-
61src/storage/SparseMatrix.h
-
6src/storage/dd/Add.cpp
-
8src/storage/prism/Program.cpp
-
12src/storage/prism/Program.h
-
2src/storage/prism/RewardModel.cpp
-
4src/utility/constants.cpp
-
4src/utility/storm.h
-
32test/functional/builder/ExplicitPrismModelBuilderTest.cpp
-
8test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
2test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
8test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
2test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
-
2test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
-
16test/functional/storage/BitVectorHashMapTest.cpp
-
18test/functional/storage/BitVectorTest.cpp
-
2test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp
-
4test/functional/storage/SparseMatrixTest.cpp
-
8test/functional/utility/GraphTest.cpp
-
29test/functional/utility/ModelInstantiatorTest.cpp
858
src/builder/ExplicitPrismModelBuilder.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,22 @@ |
|||||
|
#include "src/builder/ExplorationOrder.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace builder { |
||||
|
|
||||
|
std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order) { |
||||
|
switch (order) { |
||||
|
case ExplorationOrder::Dfs: |
||||
|
out << "depth-first"; |
||||
|
break; |
||||
|
case ExplorationOrder::Bfs: |
||||
|
out << "breadth-first"; |
||||
|
break; |
||||
|
default: |
||||
|
out << "undefined"; |
||||
|
break; |
||||
|
} |
||||
|
return out; |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,17 @@ |
|||||
|
#ifndef STORM_BUILDER_EXPLORATIONORDER_H_ |
||||
|
#define STORM_BUILDER_EXPLORATIONORDER_H_ |
||||
|
|
||||
|
#include <ostream> |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace builder { |
||||
|
|
||||
|
// An enum that contains all currently supported exploration orders. |
||||
|
enum class ExplorationOrder { Dfs, Bfs }; |
||||
|
|
||||
|
std::ostream& operator<<(std::ostream& out, ExplorationOrder const& order); |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_BUILDER_EXPLORATIONORDER_H_ */ |
||||
@ -0,0 +1,105 @@ |
|||||
|
#include "src/generator/Choice.h"
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
|
||||
|
#include "src/utility/constants.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceRewards() { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::begin() { |
||||
|
return distribution.begin(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::begin() const { |
||||
|
return distribution.cbegin(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::end() { |
||||
|
return distribution.end(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::end() const { |
||||
|
return distribution.cend(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void Choice<ValueType, StateType>::addChoiceLabel(uint_fast64_t label) { |
||||
|
if (!choiceLabels) { |
||||
|
choiceLabels = LabelSet(); |
||||
|
} |
||||
|
choiceLabels->insert(label); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void Choice<ValueType, StateType>::addChoiceLabels(LabelSet const& labelSet) { |
||||
|
if (!choiceLabels) { |
||||
|
choiceLabels = LabelSet(); |
||||
|
} |
||||
|
choiceLabels->insert(labelSet.begin(), labelSet.end()); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getChoiceLabels() const { |
||||
|
return *choiceLabels; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
uint_fast64_t Choice<ValueType, StateType>::getActionIndex() const { |
||||
|
return actionIndex; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
ValueType Choice<ValueType, StateType>::getTotalMass() const { |
||||
|
return totalMass; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) { |
||||
|
totalMass += value; |
||||
|
distribution.addProbability(state, value); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) { |
||||
|
choiceRewards.push_back(value); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::vector<ValueType> const& Choice<ValueType, StateType>::getChoiceRewards() const { |
||||
|
return choiceRewards; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
bool Choice<ValueType, StateType>::isMarkovian() const { |
||||
|
return markovian; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::size_t Choice<ValueType, StateType>::size() const { |
||||
|
return distribution.size(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) { |
||||
|
out << "<"; |
||||
|
for (auto const& stateProbabilityPair : choice) { |
||||
|
out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; |
||||
|
} |
||||
|
out << ">"; |
||||
|
return out; |
||||
|
} |
||||
|
|
||||
|
template class Choice<double>; |
||||
|
template class Choice<storm::RationalFunction>; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,150 @@ |
|||||
|
#ifndef STORM_GENERATOR_CHOICE_H_ |
||||
|
#define STORM_GENERATOR_CHOICE_H_ |
||||
|
|
||||
|
#include <cstdint> |
||||
|
#include <functional> |
||||
|
|
||||
|
#include <boost/optional.hpp> |
||||
|
#include <boost/container/flat_set.hpp> |
||||
|
|
||||
|
#include "src/storage/Distribution.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
// A structure holding information about a particular choice. |
||||
|
template<typename ValueType, typename StateType=uint32_t> |
||||
|
struct Choice { |
||||
|
public: |
||||
|
typedef boost::container::flat_set<uint_fast64_t> LabelSet; |
||||
|
|
||||
|
Choice(uint_fast64_t actionIndex = 0, bool markovian = false); |
||||
|
|
||||
|
Choice(Choice const& other) = default; |
||||
|
Choice& operator=(Choice const& other) = default; |
||||
|
Choice(Choice&& other) = default; |
||||
|
Choice& operator=(Choice&& other) = default; |
||||
|
|
||||
|
/*! |
||||
|
* Returns an iterator to the distribution associated with this choice. |
||||
|
* |
||||
|
* @return An iterator to the first element of the distribution. |
||||
|
*/ |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::iterator begin(); |
||||
|
|
||||
|
/*! |
||||
|
* Returns an iterator to the distribution associated with this choice. |
||||
|
* |
||||
|
* @return An iterator to the first element of the distribution. |
||||
|
*/ |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::const_iterator begin() const; |
||||
|
|
||||
|
/*! |
||||
|
* Returns an iterator past the end of the distribution associated with this choice. |
||||
|
* |
||||
|
* @return An iterator past the end of the distribution. |
||||
|
*/ |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::iterator end(); |
||||
|
|
||||
|
/*! |
||||
|
* Returns an iterator past the end of the distribution associated with this choice. |
||||
|
* |
||||
|
* @return An iterator past the end of the distribution. |
||||
|
*/ |
||||
|
typename storm::storage::Distribution<ValueType, StateType>::const_iterator end() const; |
||||
|
|
||||
|
/*! |
||||
|
* Inserts the contents of this object to the given output stream. |
||||
|
* |
||||
|
* @param out The stream in which to insert the contents. |
||||
|
*/ |
||||
|
template<typename ValueTypePrime, typename StateTypePrime> |
||||
|
friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice); |
||||
|
|
||||
|
/*! |
||||
|
* Adds the given label to the labels associated with this choice. |
||||
|
* |
||||
|
* @param label The label to associate with this choice. |
||||
|
*/ |
||||
|
void addChoiceLabel(uint_fast64_t label); |
||||
|
|
||||
|
/*! |
||||
|
* Adds the given label set to the labels associated with this choice. |
||||
|
* |
||||
|
* @param labelSet The label set to associate with this choice. |
||||
|
*/ |
||||
|
void addChoiceLabels(LabelSet const& labelSet); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the set of labels associated with this choice. |
||||
|
* |
||||
|
* @return The set of labels associated with this choice. |
||||
|
*/ |
||||
|
LabelSet const& getChoiceLabels() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the index of the action of this choice. |
||||
|
* |
||||
|
* @return The index of the action of this choice. |
||||
|
*/ |
||||
|
uint_fast64_t getActionIndex() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the total mass of this choice. |
||||
|
* |
||||
|
* @return The total mass. |
||||
|
*/ |
||||
|
ValueType getTotalMass() const; |
||||
|
|
||||
|
/*! |
||||
|
* Adds the given probability value to the given state in the underlying distribution. |
||||
|
*/ |
||||
|
void addProbability(StateType const& state, ValueType const& value); |
||||
|
|
||||
|
/*! |
||||
|
* Adds the given value to the reward associated with this choice. |
||||
|
*/ |
||||
|
void addChoiceReward(ValueType const& value); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the rewards for this choice under selected reward models. |
||||
|
*/ |
||||
|
std::vector<ValueType> const& getChoiceRewards() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the choice is Markovian. |
||||
|
*/ |
||||
|
bool isMarkovian() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the size of the distribution associated with this choice. |
||||
|
*/ |
||||
|
std::size_t size() const; |
||||
|
|
||||
|
private: |
||||
|
// A flag indicating whether this choice is Markovian or not. |
||||
|
bool markovian; |
||||
|
|
||||
|
// The action index associated with this choice. |
||||
|
uint_fast64_t actionIndex; |
||||
|
|
||||
|
// The distribution that is associated with the choice. |
||||
|
storm::storage::Distribution<ValueType, StateType> distribution; |
||||
|
|
||||
|
// The total probability mass (or rates) of this choice. |
||||
|
ValueType totalMass; |
||||
|
|
||||
|
// The reward values associated with this choice. |
||||
|
std::vector<ValueType> choiceRewards; |
||||
|
|
||||
|
// The labels that are associated with this choice. |
||||
|
boost::optional<LabelSet> choiceLabels; |
||||
|
}; |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice); |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_CHOICE_H_ */ |
||||
@ -0,0 +1,23 @@ |
|||||
|
#include "src/generator/CompressedState.h"
|
||||
|
|
||||
|
#include "src/generator/VariableInformation.h"
|
||||
|
#include "src/storage/expressions/ExpressionEvaluator.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) { |
||||
|
for (auto const& booleanVariable : variableInformation.booleanVariables) { |
||||
|
evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset)); |
||||
|
} |
||||
|
for (auto const& integerVariable : variableInformation.integerVariables) { |
||||
|
evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator); |
||||
|
template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator); |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,30 @@ |
|||||
|
#ifndef STORM_GENERATOR_COMPRESSEDSTATE_H_ |
||||
|
#define STORM_GENERATOR_COMPRESSEDSTATE_H_ |
||||
|
|
||||
|
#include "src/storage/BitVector.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace expressions { |
||||
|
template<typename ValueType> class ExpressionEvaluator; |
||||
|
} |
||||
|
|
||||
|
namespace generator { |
||||
|
|
||||
|
typedef storm::storage::BitVector CompressedState; |
||||
|
|
||||
|
class VariableInformation; |
||||
|
|
||||
|
/*! |
||||
|
* Unpacks the compressed state into the evaluator. |
||||
|
* |
||||
|
* @param state The state to unpack. |
||||
|
* @param variableInformation The information about how the variables are packed with the state. |
||||
|
* @param evaluator The evaluator into which to load the state. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_COMPRESSEDSTATE_H_ */ |
||||
|
|
||||
@ -0,0 +1,24 @@ |
|||||
|
#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_ |
||||
|
#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_ |
||||
|
|
||||
|
#include <vector> |
||||
|
#include <cstdint> |
||||
|
|
||||
|
#include "src/generator/CompressedState.h" |
||||
|
#include "src/generator/StateBehavior.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
template<typename ValueType, typename StateType = uint32_t> |
||||
|
class NextStateGenerator { |
||||
|
public: |
||||
|
typedef std::function<StateType (CompressedState const&)> StateToIdCallback; |
||||
|
|
||||
|
virtual bool isDeterministicModel() const = 0; |
||||
|
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; |
||||
|
virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) = 0; |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */ |
||||
@ -0,0 +1,404 @@ |
|||||
|
#include "src/generator/PrismNextStateGenerator.h"
|
||||
|
|
||||
|
#include <boost/container/flat_map.hpp>
|
||||
|
|
||||
|
#include "src/utility/constants.h"
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/exceptions/WrongFormatException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void PrismNextStateGenerator<ValueType, StateType>::addRewardModel(storm::prism::RewardModel const& rewardModel) { |
||||
|
selectedRewardModels.push_back(rewardModel); |
||||
|
hasStateActionRewards |= rewardModel.hasStateActionRewards(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void PrismNextStateGenerator<ValueType, StateType>::setTerminalExpression(storm::expressions::Expression const& terminalExpression) { |
||||
|
this->terminalExpression = terminalExpression; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
bool PrismNextStateGenerator<ValueType, StateType>::isDeterministicModel() const { |
||||
|
return program.isDeterministicModel(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::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<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound)); |
||||
|
} |
||||
|
|
||||
|
// Register initial state and return it.
|
||||
|
StateType id = stateToIdCallback(initialState); |
||||
|
return {id}; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) { |
||||
|
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
|
||||
|
unpackStateIntoEvaluator(state, variableInformation, evaluator); |
||||
|
|
||||
|
// Prepare the result, in case we return early.
|
||||
|
StateBehavior<ValueType, StateType> result; |
||||
|
|
||||
|
// First, construct the state rewards, as we may return early if there are no choices later and we already
|
||||
|
// need the state rewards then.
|
||||
|
for (auto const& rewardModel : selectedRewardModels) { |
||||
|
ValueType stateRewardValue = storm::utility::zero<ValueType>(); |
||||
|
if (rewardModel.get().hasStateRewards()) { |
||||
|
for (auto const& stateReward : rewardModel.get().getStateRewards()) { |
||||
|
if (evaluator.asBool(stateReward.getStatePredicateExpression())) { |
||||
|
stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression())); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
result.addStateReward(stateRewardValue); |
||||
|
} |
||||
|
|
||||
|
// If a terminal expression was set and we must not expand this state, return now.
|
||||
|
if (terminalExpression && evaluator.asBool(terminalExpression.get())) { |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
// Get all choices for the state.
|
||||
|
std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(state, stateToIdCallback); |
||||
|
std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(state, stateToIdCallback); |
||||
|
for (auto& choice : allLabeledChoices) { |
||||
|
allChoices.push_back(std::move(choice)); |
||||
|
} |
||||
|
|
||||
|
std::size_t totalNumberOfChoices = allChoices.size(); |
||||
|
|
||||
|
// If there is not a single choice, we return immediately, because the state has no behavior (other than
|
||||
|
// the state reward).
|
||||
|
if (totalNumberOfChoices == 0) { |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
// If the model is a deterministic model, we need to fuse the choices into one.
|
||||
|
if (program.isDeterministicModel() && totalNumberOfChoices > 1) { |
||||
|
Choice<ValueType> globalChoice; |
||||
|
|
||||
|
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
|
||||
|
// this is equal to the number of choices, which is why we initialize it like this here.
|
||||
|
ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>(); |
||||
|
|
||||
|
// Iterate over all choices and combine the probabilities/rates into one choice.
|
||||
|
for (auto const& choice : allChoices) { |
||||
|
for (auto const& stateProbabilityPair : choice) { |
||||
|
if (program.isDiscreteTimeModel()) { |
||||
|
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices); |
||||
|
} else { |
||||
|
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
if (hasStateActionRewards && !program.isDiscreteTimeModel()) { |
||||
|
totalExitRate += choice.getTotalMass(); |
||||
|
} |
||||
|
|
||||
|
if (buildChoiceLabeling) { |
||||
|
globalChoice.addChoiceLabels(choice.getChoiceLabels()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// Now construct the state-action reward for all selected reward models.
|
||||
|
for (auto const& rewardModel : selectedRewardModels) { |
||||
|
ValueType stateActionRewardValue = storm::utility::zero<ValueType>(); |
||||
|
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; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
globalChoice.addChoiceReward(stateActionRewardValue); |
||||
|
} |
||||
|
|
||||
|
// Move the newly fused choice in place.
|
||||
|
allChoices.clear(); |
||||
|
allChoices.push_back(std::move(globalChoice)); |
||||
|
} |
||||
|
|
||||
|
// Move all remaining choices in place.
|
||||
|
for (auto& choice : allChoices) { |
||||
|
result.addChoice(std::move(choice)); |
||||
|
} |
||||
|
|
||||
|
result.setExpanded(); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) { |
||||
|
CompressedState newState(state); |
||||
|
|
||||
|
auto assignmentIt = update.getAssignments().begin(); |
||||
|
auto assignmentIte = update.getAssignments().end(); |
||||
|
|
||||
|
// Iterate over all boolean assignments and carry them out.
|
||||
|
auto boolIt = variableInformation.booleanVariables.begin(); |
||||
|
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { |
||||
|
while (assignmentIt->getVariable() != boolIt->variable) { |
||||
|
++boolIt; |
||||
|
} |
||||
|
newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression())); |
||||
|
} |
||||
|
|
||||
|
// Iterate over all integer assignments and carry them out.
|
||||
|
auto integerIt = variableInformation.integerVariables.begin(); |
||||
|
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { |
||||
|
while (assignmentIt->getVariable() != integerIt->variable) { |
||||
|
++integerIt; |
||||
|
} |
||||
|
int_fast64_t assignedValue = 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<int_fast64_t>(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 << ")."); |
||||
|
} |
||||
|
|
||||
|
// Check that we processed all assignments.
|
||||
|
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); |
||||
|
|
||||
|
return newState; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) { |
||||
|
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>())); |
||||
|
|
||||
|
// Iterate over all modules.
|
||||
|
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { |
||||
|
storm::prism::Module const& module = program.getModule(i); |
||||
|
|
||||
|
// If the module has no command labeled with the given action, we can skip this module.
|
||||
|
if (!module.hasActionIndex(actionIndex)) { |
||||
|
continue; |
||||
|
} |
||||
|
|
||||
|
std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); |
||||
|
|
||||
|
// If the module contains the action, but there is no command in the module that is labeled with
|
||||
|
// this action, we don't have any feasible command combinations.
|
||||
|
if (commandIndices.empty()) { |
||||
|
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>(); |
||||
|
} |
||||
|
|
||||
|
std::vector<std::reference_wrapper<storm::prism::Command const>> commands; |
||||
|
|
||||
|
// 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())) { |
||||
|
commands.push_back(command); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// If there was no enabled command although the module has some command with the required action label,
|
||||
|
// we must not return anything.
|
||||
|
if (commands.size() == 0) { |
||||
|
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>(); |
||||
|
} |
||||
|
|
||||
|
result.get().push_back(std::move(commands)); |
||||
|
} |
||||
|
|
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { |
||||
|
std::vector<Choice<ValueType>> result; |
||||
|
|
||||
|
// Iterate over all modules.
|
||||
|
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { |
||||
|
storm::prism::Module const& module = program.getModule(i); |
||||
|
|
||||
|
// Iterate over all commands.
|
||||
|
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { |
||||
|
storm::prism::Command const& command = module.getCommand(j); |
||||
|
|
||||
|
// Only consider unlabeled commands.
|
||||
|
if (command.isLabeled()) continue; |
||||
|
|
||||
|
// Skip the command, if it is not enabled.
|
||||
|
if (!evaluator.asBool(command.getGuardExpression())) { |
||||
|
continue; |
||||
|
} |
||||
|
|
||||
|
result.push_back(Choice<ValueType>(command.getActionIndex())); |
||||
|
Choice<ValueType>& choice = result.back(); |
||||
|
|
||||
|
// Remember the command labels only if we were asked to.
|
||||
|
if (buildChoiceLabeling) { |
||||
|
choice.addChoiceLabel(command.getGlobalIndex()); |
||||
|
} |
||||
|
|
||||
|
// Iterate over all updates of the current command.
|
||||
|
ValueType probabilitySum = storm::utility::zero<ValueType>(); |
||||
|
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { |
||||
|
storm::prism::Update const& update = command.getUpdate(k); |
||||
|
|
||||
|
// Obtain target state index and add it to the list of known states. If it has not yet been
|
||||
|
// seen, we also add it to the set of states that have yet to be explored.
|
||||
|
StateType stateIndex = stateToIdCallback(applyUpdate(state, update)); |
||||
|
|
||||
|
// Update the choice by adding the probability/target state to it.
|
||||
|
ValueType probability = evaluator.asRational(update.getLikelihoodExpression()); |
||||
|
choice.addProbability(stateIndex, probability); |
||||
|
probabilitySum += probability; |
||||
|
} |
||||
|
|
||||
|
// Create the state-action reward for the newly created choice.
|
||||
|
for (auto const& rewardModel : selectedRewardModels) { |
||||
|
ValueType stateActionRewardValue = storm::utility::zero<ValueType>(); |
||||
|
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(); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
choice.addChoiceReward(stateActionRewardValue); |
||||
|
} |
||||
|
|
||||
|
// 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 << ")."); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { |
||||
|
std::vector<Choice<ValueType>> result; |
||||
|
|
||||
|
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { |
||||
|
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex); |
||||
|
|
||||
|
// Only process this action label, if there is at least one feasible solution.
|
||||
|
if (optionalActiveCommandLists) { |
||||
|
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get(); |
||||
|
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size()); |
||||
|
|
||||
|
// Initialize the list of iterators.
|
||||
|
for (size_t i = 0; i < activeCommandList.size(); ++i) { |
||||
|
iteratorList[i] = activeCommandList[i].cbegin(); |
||||
|
} |
||||
|
|
||||
|
// As long as there is one feasible combination of commands, keep on expanding it.
|
||||
|
bool done = false; |
||||
|
while (!done) { |
||||
|
boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); |
||||
|
boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); |
||||
|
|
||||
|
currentTargetStates->emplace(state, storm::utility::one<ValueType>()); |
||||
|
|
||||
|
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { |
||||
|
storm::prism::Command const& command = *iteratorList[i]; |
||||
|
|
||||
|
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { |
||||
|
storm::prism::Update const& update = command.getUpdate(j); |
||||
|
|
||||
|
for (auto const& stateProbabilityPair : *currentTargetStates) { |
||||
|
// Compute the new state under the current update and add it to the set of new target states.
|
||||
|
CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update); |
||||
|
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// If there is one more command to come, shift the target states one time step back.
|
||||
|
if (i < iteratorList.size() - 1) { |
||||
|
delete currentTargetStates; |
||||
|
currentTargetStates = newTargetStates; |
||||
|
newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// At this point, we applied all commands of the current command combination and newTargetStates
|
||||
|
// contains all target states and their respective probabilities. That means we are now ready to
|
||||
|
// add the choice to the list of transitions.
|
||||
|
result.push_back(Choice<ValueType>(actionIndex)); |
||||
|
|
||||
|
// Now create the actual distribution.
|
||||
|
Choice<ValueType>& choice = result.back(); |
||||
|
|
||||
|
// Remember the command labels only if we were asked to.
|
||||
|
if (buildChoiceLabeling) { |
||||
|
// Add the labels of all commands to this choice.
|
||||
|
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { |
||||
|
choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// Add the probabilities/rates to the newly created choice.
|
||||
|
ValueType probabilitySum = storm::utility::zero<ValueType>(); |
||||
|
for (auto const& stateProbabilityPair : *newTargetStates) { |
||||
|
StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); |
||||
|
choice.addProbability(actualIndex, stateProbabilityPair.second); |
||||
|
probabilitySum += stateProbabilityPair.second; |
||||
|
} |
||||
|
|
||||
|
// 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 << ")."); |
||||
|
|
||||
|
// Create the state-action reward for the newly created choice.
|
||||
|
for (auto const& rewardModel : selectedRewardModels) { |
||||
|
ValueType stateActionRewardValue = storm::utility::zero<ValueType>(); |
||||
|
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(); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
choice.addChoiceReward(stateActionRewardValue); |
||||
|
} |
||||
|
|
||||
|
// Dispose of the temporary maps.
|
||||
|
delete currentTargetStates; |
||||
|
delete newTargetStates; |
||||
|
|
||||
|
// Now, check whether there is one more command combination to consider.
|
||||
|
bool movedIterator = false; |
||||
|
for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { |
||||
|
++iteratorList[j]; |
||||
|
if (iteratorList[j] != activeCommandList[j].end()) { |
||||
|
movedIterator = true; |
||||
|
} else { |
||||
|
// Reset the iterator to the beginning of the list.
|
||||
|
iteratorList[j] = activeCommandList[j].begin(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
done = !movedIterator; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
template class PrismNextStateGenerator<double>; |
||||
|
template class PrismNextStateGenerator<storm::RationalFunction>; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,108 @@ |
|||||
|
#ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ |
||||
|
#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 { |
||||
|
|
||||
|
template<typename ValueType, typename StateType = uint32_t> |
||||
|
class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> { |
||||
|
public: |
||||
|
typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback; |
||||
|
|
||||
|
PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling); |
||||
|
|
||||
|
/*! |
||||
|
* Adds a reward model to the list of selected reward models () |
||||
|
*/ |
||||
|
void addRewardModel(storm::prism::RewardModel const& rewardModel); |
||||
|
|
||||
|
/*! |
||||
|
* Sets an expression such that if it evaluates to true in a state, prevents the exploration. |
||||
|
*/ |
||||
|
void setTerminalExpression(storm::expressions::Expression const& terminalExpression); |
||||
|
|
||||
|
virtual bool isDeterministicModel() const override; |
||||
|
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override; |
||||
|
virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) 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::prism::Update const& update); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by |
||||
|
* modules. |
||||
|
* |
||||
|
* This function will iterate over all modules and retrieve all commands that are labeled with the given |
||||
|
* action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which |
||||
|
* the inner lists contain all commands of exactly one module. If a module does not have *any* (including |
||||
|
* disabled) commands, there will not be a list of commands of that module in the result. If, however, the |
||||
|
* module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there |
||||
|
* is no legal transition possible. |
||||
|
* |
||||
|
* @param The program in which to search for active commands. |
||||
|
* @param state The current state. |
||||
|
* @param actionIndex The index of the action label to select. |
||||
|
* @return A list of lists of active commands or nothing. |
||||
|
*/ |
||||
|
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves all unlabeled choices possible from the given state. |
||||
|
* |
||||
|
* @param state The state for which to retrieve the unlabeled choices. |
||||
|
* @return The unlabeled choices of the state. |
||||
|
*/ |
||||
|
std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves all labeled choices possible from the given state. |
||||
|
* |
||||
|
* @param state The state for which to retrieve the unlabeled choices. |
||||
|
* @return The labeled choices of the state. |
||||
|
*/ |
||||
|
std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); |
||||
|
|
||||
|
// The program used for the generation of next states. |
||||
|
storm::prism::Program const& program; |
||||
|
|
||||
|
// The reward models that need to be considered. |
||||
|
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels; |
||||
|
|
||||
|
// A flag that stores whether at least one of the selected reward models has state-action rewards. |
||||
|
bool hasStateActionRewards; |
||||
|
|
||||
|
// A flag that stores whether or not to build the choice labeling. |
||||
|
bool buildChoiceLabeling; |
||||
|
|
||||
|
// An optional expression that governs which states must not be explored. |
||||
|
boost::optional<storm::expressions::Expression> terminalExpression; |
||||
|
|
||||
|
// Information about how the variables are packed. |
||||
|
VariableInformation const& variableInformation; |
||||
|
|
||||
|
// An evaluator used to evaluate expressions. |
||||
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator; |
||||
|
|
||||
|
// A comparator used to compare constants. |
||||
|
storm::utility::ConstantsComparator<ValueType> comparator; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */ |
||||
@ -0,0 +1,50 @@ |
|||||
|
#include "src/generator/PrismStateLabelingGenerator.h"
|
||||
|
|
||||
|
#include "src/generator/CompressedState.h"
|
||||
|
|
||||
|
#include "src/storage/expressions/ExpressionEvaluator.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
PrismStateLabelingGenerator<ValueType, StateType>::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
storm::models::sparse::StateLabeling PrismStateLabelingGenerator<ValueType, StateType>::generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) { |
||||
|
std::vector<storm::prism::Label> const& labels = program.getLabels(); |
||||
|
|
||||
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager()); |
||||
|
storm::models::sparse::StateLabeling result(states.size()); |
||||
|
|
||||
|
// Initialize labeling.
|
||||
|
for (auto const& label : labels) { |
||||
|
result.addLabel(label.getName()); |
||||
|
} |
||||
|
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.getStatePredicateExpression())) { |
||||
|
result.addLabelToState(label.getName(), 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 class PrismStateLabelingGenerator<double, uint32_t>; |
||||
|
template class PrismStateLabelingGenerator<storm::RationalFunction, uint32_t>; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,31 @@ |
|||||
|
#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ |
||||
|
#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ |
||||
|
|
||||
|
#include "src/generator/StateLabelingGenerator.h" |
||||
|
|
||||
|
#include "src/generator/VariableInformation.h" |
||||
|
|
||||
|
#include "src/storage/prism/Program.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType, typename StateType = uint32_t> |
||||
|
class PrismStateLabelingGenerator : public StateLabelingGenerator<StateType> { |
||||
|
public: |
||||
|
PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation); |
||||
|
|
||||
|
virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override; |
||||
|
|
||||
|
private: |
||||
|
// The program for which to generate the labels. |
||||
|
storm::prism::Program const& program; |
||||
|
|
||||
|
// Information about how the variables are packed. |
||||
|
VariableInformation const& variableInformation; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */ |
||||
@ -0,0 +1,57 @@ |
|||||
|
#include "src/generator/StateBehavior.h"
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
StateBehavior<ValueType, StateType>::StateBehavior() : expanded(false) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
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); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
void StateBehavior<ValueType, StateType>::setExpanded(bool newValue) { |
||||
|
this->expanded = newValue; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
bool StateBehavior<ValueType, StateType>::wasExpanded() const { |
||||
|
return expanded; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
bool StateBehavior<ValueType, StateType>::empty() const { |
||||
|
return choices.empty(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::begin() const { |
||||
|
return choices.begin(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
typename std::vector<Choice<ValueType, StateType>>::const_iterator StateBehavior<ValueType, StateType>::end() const { |
||||
|
return choices.end(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType, typename StateType> |
||||
|
std::vector<ValueType> const& StateBehavior<ValueType, StateType>::getStateRewards() const { |
||||
|
return stateRewards; |
||||
|
} |
||||
|
|
||||
|
template class StateBehavior<double>; |
||||
|
template class StateBehavior<storm::RationalFunction>; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,73 @@ |
|||||
|
#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: |
||||
|
/*! |
||||
|
* Creates an empty behavior, i.e. the state was not yet expanded. |
||||
|
*/ |
||||
|
StateBehavior(); |
||||
|
|
||||
|
/*! |
||||
|
* 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); |
||||
|
|
||||
|
/*! |
||||
|
* Sets whether the state was expanded. |
||||
|
*/ |
||||
|
void setExpanded(bool newValue = true); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the state was expanded. |
||||
|
*/ |
||||
|
bool wasExpanded() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the behavior is empty in the sense that there are no available choices. |
||||
|
*/ |
||||
|
bool empty() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves an iterator to the choices available in the behavior. |
||||
|
*/ |
||||
|
typename std::vector<Choice<ValueType, StateType>>::const_iterator begin() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves an iterator past the choices available in the behavior. |
||||
|
*/ |
||||
|
typename std::vector<Choice<ValueType, StateType>>::const_iterator end() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the list of state rewards under selected reward models. |
||||
|
*/ |
||||
|
std::vector<ValueType> const& getStateRewards() const; |
||||
|
|
||||
|
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; |
||||
|
|
||||
|
// A flag indicating whether the state was actually expanded. |
||||
|
bool expanded; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_PRISM_STATEBEHAVIOR_H_ */ |
||||
@ -0,0 +1,20 @@ |
|||||
|
#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_ |
||||
|
#define STORM_GENERATOR_STATELABELINGGENERATOR_H_ |
||||
|
|
||||
|
#include "src/models/sparse/StateLabeling.h" |
||||
|
|
||||
|
#include "src/storage/BitVectorHashMap.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template<typename StateType = uint32_t> |
||||
|
class StateLabelingGenerator { |
||||
|
public: |
||||
|
virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */ |
||||
@ -0,0 +1,77 @@ |
|||||
|
#include "src/generator/VariableInformation.h"
|
||||
|
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/exceptions/InvalidArgumentException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) { |
||||
|
for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { |
||||
|
booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset); |
||||
|
++totalBitOffset; |
||||
|
booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1; |
||||
|
} |
||||
|
for (auto const& integerVariable : program.getGlobalIntegerVariables()) { |
||||
|
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); |
||||
|
int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); |
||||
|
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); |
||||
|
integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth); |
||||
|
totalBitOffset += bitwidth; |
||||
|
integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1; |
||||
|
} |
||||
|
for (auto const& module : program.getModules()) { |
||||
|
for (auto const& booleanVariable : module.getBooleanVariables()) { |
||||
|
booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), totalBitOffset); |
||||
|
++totalBitOffset; |
||||
|
booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = booleanVariables.size() - 1; |
||||
|
} |
||||
|
for (auto const& integerVariable : module.getIntegerVariables()) { |
||||
|
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); |
||||
|
int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); |
||||
|
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); |
||||
|
integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, totalBitOffset, bitwidth); |
||||
|
totalBitOffset += bitwidth; |
||||
|
integerVariableToIndexMap[integerVariable.getExpressionVariable()] = integerVariables.size() - 1; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { |
||||
|
uint_fast64_t result = totalBitOffset; |
||||
|
if (roundTo64Bit) { |
||||
|
result = ((result >> 6) + 1) << 6; |
||||
|
} |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { |
||||
|
auto const& booleanIndex = booleanVariableToIndexMap.find(variable); |
||||
|
if (booleanIndex != booleanVariableToIndexMap.end()) { |
||||
|
return booleanVariables[booleanIndex->second].bitOffset; |
||||
|
} |
||||
|
auto const& integerIndex = integerVariableToIndexMap.find(variable); |
||||
|
if (integerIndex != integerVariableToIndexMap.end()) { |
||||
|
return integerVariables[integerIndex->second].bitOffset; |
||||
|
} |
||||
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); |
||||
|
} |
||||
|
|
||||
|
uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { |
||||
|
auto const& integerIndex = integerVariableToIndexMap.find(variable); |
||||
|
if (integerIndex != integerVariableToIndexMap.end()) { |
||||
|
return integerVariables[integerIndex->second].bitWidth; |
||||
|
} |
||||
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,75 @@ |
|||||
|
#ifndef STORM_GENERATOR_VARIABLEINFORMATION_H_ |
||||
|
#define STORM_GENERATOR_VARIABLEINFORMATION_H_ |
||||
|
|
||||
|
#include <vector> |
||||
|
#include <boost/container/flat_map.hpp> |
||||
|
|
||||
|
#include "src/storage/expressions/Variable.h" |
||||
|
#include "src/storage/prism/Program.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
// A structure storing information about the boolean variables of the program. |
||||
|
struct BooleanVariableInformation { |
||||
|
BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); |
||||
|
|
||||
|
// The boolean variable. |
||||
|
storm::expressions::Variable variable; |
||||
|
|
||||
|
// Its initial value. |
||||
|
bool initialValue; |
||||
|
|
||||
|
// Its bit offset in the compressed state. |
||||
|
uint_fast64_t bitOffset; |
||||
|
}; |
||||
|
|
||||
|
// A structure storing information about the integer variables of the program. |
||||
|
struct IntegerVariableInformation { |
||||
|
IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); |
||||
|
|
||||
|
// The integer variable. |
||||
|
storm::expressions::Variable variable; |
||||
|
|
||||
|
// Its initial value. |
||||
|
int_fast64_t initialValue; |
||||
|
|
||||
|
// The lower bound of its range. |
||||
|
int_fast64_t lowerBound; |
||||
|
|
||||
|
// The upper bound of its range. |
||||
|
int_fast64_t upperBound; |
||||
|
|
||||
|
// Its bit offset in the compressed state. |
||||
|
uint_fast64_t bitOffset; |
||||
|
|
||||
|
// Its bit width in the compressed state. |
||||
|
uint_fast64_t bitWidth; |
||||
|
}; |
||||
|
|
||||
|
// A structure storing information about the used variables of the program. |
||||
|
struct VariableInformation { |
||||
|
VariableInformation() = default; |
||||
|
VariableInformation(storm::prism::Program const& program); |
||||
|
uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; |
||||
|
|
||||
|
// Provide methods to access the bit offset and width of variables in the compressed state. |
||||
|
uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; |
||||
|
uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; |
||||
|
|
||||
|
// The total bit offset over all variables. |
||||
|
uint_fast64_t totalBitOffset; |
||||
|
|
||||
|
// The known boolean variables. |
||||
|
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap; |
||||
|
std::vector<BooleanVariableInformation> booleanVariables; |
||||
|
|
||||
|
// The known integer variables. |
||||
|
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap; |
||||
|
std::vector<IntegerVariableInformation> integerVariables; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */ |
||||
Reference in new issue
xxxxxxxxxx