sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

explicit model builder supports non-default reward models 

Former-commit-id: 97aabc54bb
tempestpy_adaptions
sjunges 9 years ago
parent
ed94184ec8
commit
7884fc37ed
3 changed files with 61 additions and 59 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 107
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 9
      src/builder/ExplicitPrismModelBuilder.h
  3. 4
      src/utility/storm.h

107
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -63,23 +63,23 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder;
};
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::VariableInformation::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) {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::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.
}
template <typename ValueType, typename IndexType>
uint_fast64_t ExplicitPrismModelBuilder<ValueType, IndexType>::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
template <typename ValueType, typename RewardModelType, typename IndexType>
uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
if (booleanIndex != booleanVariableToIndexMap.end()) {
return booleanVariables[booleanIndex->second].bitOffset;
@ -91,8 +91,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
}
template <typename ValueType, typename IndexType>
uint_fast64_t ExplicitPrismModelBuilder<ValueType, IndexType>::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
template <typename ValueType, typename RewardModelType, typename IndexType>
uint_fast64_t ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
return integerVariables[integerIndex->second].bitWidth;
@ -100,23 +100,23 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@ -130,8 +130,8 @@ namespace storm {
}
}
template <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
if (formula.isAtomicExpressionFormula()) {
terminalStates = formula.asAtomicExpressionFormula().getExpression();
} else if (formula.isAtomicLabelFormula()) {
@ -160,8 +160,8 @@ namespace storm {
}
}
template <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
// If we already had terminal states, we need to erase them.
if (terminalStates) {
terminalStates.reset();
@ -200,8 +200,8 @@ namespace storm {
}
}
template <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
// If there is at least one constant that is defined, and the constant definition map does not yet exist,
@ -216,8 +216,8 @@ namespace storm {
}
}
template <typename ValueType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
template <typename ValueType, typename RewardModelType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
// Start by defining the undefined constants in the model.
storm::prism::Program preparedProgram;
if (options.constantDefinitions) {
@ -299,16 +299,16 @@ namespace storm {
ModelComponents modelComponents = buildModelComponents(preparedProgram, selectedRewardModels, options);
std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> result;
switch (program.getModelType()) {
case storm::prism::Program::ModelType::DTMC:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Dtmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::CTMC:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
break;
case storm::prism::Program::ModelType::MDP:
result = std::shared_ptr<storm::models::sparse::Model<ValueType>>(new storm::models::sparse::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Mdp<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
break;
default:
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model from probabilistic program: cannot handle this model type.");
@ -318,8 +318,8 @@ namespace storm {
return result;
}
template <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
}
@ -328,13 +328,13 @@ namespace storm {
}
}
template <typename ValueType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
return applyUpdate(variableInformation, state, state, update, evaluator);
}
template <typename ValueType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
CompressedState newState(state);
auto assignmentIt = update.getAssignments().begin();
@ -367,8 +367,8 @@ namespace storm {
return newState;
}
template <typename ValueType, typename IndexType>
IndexType ExplicitPrismModelBuilder<ValueType, IndexType>::getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
template <typename ValueType, typename RewardModelType, typename IndexType>
IndexType ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getOrAddStateIndex(CompressedState const& state, StateInformation& stateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
uint32_t newIndex = stateInformation.reachableStates.size();
// Check, if the state was already registered.
@ -382,8 +382,8 @@ namespace storm {
return actualIndexBucketPair.first;
}
template <typename ValueType, typename IndexType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> ExplicitPrismModelBuilder<ValueType, IndexType>::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex) {
template <typename ValueType, typename RewardModelType, typename IndexType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, 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.
@ -425,8 +425,8 @@ namespace storm {
return result;
}
template <typename ValueType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
@ -476,8 +476,8 @@ namespace storm {
return result;
}
template <typename ValueType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
@ -571,8 +571,8 @@ namespace storm {
return result;
}
template <typename ValueType, typename IndexType>
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
template <typename ValueType, typename RewardModelType, typename IndexType>
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
// Create choice labels, if requested,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabels;
if (commandLabels) {
@ -890,8 +890,8 @@ namespace storm {
return choiceLabels;
}
template <typename ValueType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, IndexType>::buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options) {
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options) {
ModelComponents modelComponents;
uint_fast64_t bitOffset = 0;
@ -936,7 +936,7 @@ namespace storm {
// Prepare the transition matrix builder and the reward model builders.
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
std::vector<RewardModelBuilder<ValueType>> rewardModelBuilders;
std::vector<RewardModelBuilder<typename RewardModelType::ValueType>> rewardModelBuilders;
for (auto const& rewardModel : selectedRewardModels) {
rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
}
@ -987,8 +987,8 @@ namespace storm {
return modelComponents;
}
template <typename ValueType, typename IndexType>
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
std::vector<storm::prism::Label> const& labels = program.getLabels();
@ -1019,10 +1019,11 @@ namespace storm {
}
// Explicitly instantiate the class.
template class ExplicitPrismModelBuilder<double, uint32_t>;
template class ExplicitPrismModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
#ifdef STORM_HAVE_CARL
template class ExplicitPrismModelBuilder<RationalFunction, uint32_t>;
template class ExplicitPrismModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
template class ExplicitPrismModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
#endif
}
}

9
src/builder/ExplicitPrismModelBuilder.h
View File

@ -9,6 +9,7 @@
#include <boost/functional/hash.hpp>
#include <boost/container/flat_set.hpp>
#include <boost/container/flat_map.hpp>
#include <src/models/sparse/StandardRewardModel.h>
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/SimpleValuation.h"
@ -35,7 +36,7 @@ namespace storm {
// Forward-declare classes.
template <typename ValueType> struct RewardModelBuilder;
template<typename ValueType, typename IndexType = uint32_t>
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
class ExplicitPrismModelBuilder {
public:
typedef storm::storage::BitVector CompressedState;
@ -118,7 +119,7 @@ namespace storm {
storm::models::sparse::StateLabeling stateLabeling;
// The reward models associated with the model.
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
// A vector that stores a labeling for each choice.
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
@ -212,7 +213,7 @@ namespace storm {
* @param rewardModel The reward model that is to be built.
* @return The explicit model that was given by the probabilistic program.
*/
static std::shared_ptr<storm::models::sparse::Model<ValueType>> translateProgram(storm::prism::Program program, Options const& options = Options());
static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translateProgram(storm::prism::Program program, Options const& options = Options());
private:
static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
@ -289,7 +290,7 @@ namespace storm {
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
/*!
* Explores the state space of the given program and returns the components of the model as a result.

4
src/utility/storm.h
View File

@ -93,8 +93,8 @@ namespace storm {
// Customize and perform model-building.
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(formulas);
typename storm::builder::ExplicitPrismModelBuilder<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>::Options options;
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
// Generate command labels if we are going to build a counterexample later.

Write Preview
Loading…
Cancel
Save