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

factored out some parts from the PRISM next-state generator into the superclass 

Former-commit-id: bb40e2ec4b
main
dehnert 10 years ago
parent
4cc780cbc0
commit
1d3539ab9a
8 changed files with 318 additions and 125 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. 89
      src/generator/JaniNextStateGenerator.cpp
  2. 68
      src/generator/JaniNextStateGenerator.h
  3. 76
      src/generator/NextStateGenerator.cpp
  4. 39
      src/generator/NextStateGenerator.h
  5. 131
      src/generator/PrismNextStateGenerator.cpp
  6. 31
      src/generator/PrismNextStateGenerator.h
  7. 4
      src/storage/jani/Model.cpp
  8. 5
      src/storage/jani/Model.h

89
src/generator/JaniNextStateGenerator.cpp
View File

@ -0,0 +1,89 @@
//#include "src/generator/JaniNextStateGenerator.h"
//
//#include "src/models/sparse/StateLabeling.h"
//
//#include "src/storage/expressions/SimpleValuation.h"
//
//#include "src/utility/constants.h"
//#include "src/utility/macros.h"
//#include "src/exceptions/InvalidSettingsException.h"
//#include "src/exceptions/WrongFormatException.h"
//
//namespace storm {
// namespace generator {
//
// template<typename ValueType, typename StateType>
// JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), model(model.substituteConstants()), variableInformation(this->model), evaluator(this->model.getManager()), state(nullptr), comparator() {
// STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
// STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
//
// // If there are terminal states we need to handle, we now need to translate all labels to expressions.
// if (this->options.hasTerminalStates()) {
// for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
// if (expressionOrLabelAndBool.first.isExpression()) {
// terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
// } else {
// STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models.");
// }
// }
// }
// }
//
// template<typename ValueType, typename StateType>
// uint64_t JaniNextStateGenerator<ValueType, StateType>::getStateSize() const {
// return variableInformation.getTotalBitOffset(true);
// }
//
// template<typename ValueType, typename StateType>
// ModelType JaniNextStateGenerator<ValueType, StateType>::getModelType() const {
// switch (model.getModelType()) {
// case storm::jani::ModelType::DTMC: return ModelType::DTMC;
// case storm::jani::ModelType::CTMC: return ModelType::CTMC;
// case storm::jani::ModelType::MDP: return ModelType::MDP;
// case storm::jani::ModelType::MA: return ModelType::MA;
// default:
// STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
// }
// }
//
// template<typename ValueType, typename StateType>
// bool JaniNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
// return model.isDeterministicModel();
// }
//
// template<typename ValueType, typename StateType>
// std::vector<StateType> JaniNextStateGenerator<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>
// void JaniNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
// unpackStateIntoEvaluator(state, variableInformation, evaluator);
//
// // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
// this->state = &state;
// }
//
// template<typename ValueType, typename StateType>
// bool JaniNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
// if (expression.isTrue()) {
// return true;
// }
// return evaluator.asBool(expression);
// }
// }
//}

68
src/generator/JaniNextStateGenerator.h
View File

@ -0,0 +1,68 @@
//#pragma once
//
//#include "src/generator/NextStateGenerator.h"
//#include "src/generator/VariableInformation.h"
//
//#include "src/storage/jani/Model.h"
//#include "src/storage/expressions/ExpressionEvaluator.h"
//
//#include "src/utility/ConstantsComparator.h"
//
//namespace storm {
// namespace generator {
//
// template<typename ValueType, typename StateType = uint32_t>
// class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
// public:
// typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
//
// JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
//
// virtual uint64_t getStateSize() const override;
// virtual ModelType getModelType() const override;
// virtual bool isDeterministicModel() const override;
// virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
//
// virtual void load(CompressedState const& state) override;
// virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
// virtual bool satisfies(storm::expressions::Expression const& expression) const override;
//
// virtual std::size_t getNumberOfRewardModels() const override;
// virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
//
// virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override;
//
// virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
//
// private:
// /*!
// * Applies an update to the state currently loaded into the evaluator and applies the resulting values to
// * the given compressed state.
// * @params state The state to which to apply the new values.
// * @params update The update to apply.
// * @return The resulting state.
// */
// CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update);
//
// /*!
// * Retrieves all choices labeled with the silent action possible from the given state.
// *
// * @param state The state for which to retrieve the silent choices.
// * @return The silent action choices of the state.
// */
// std::vector<Choice<ValueType>> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
//
// /*!
// * Retrieves all choices labeled with some non-silent action possible from the given state.
// *
// * @param state The state for which to retrieve the non-silent choices.
// * @return The non-silent action choices of the state.
// */
// std::vector<Choice<ValueType>> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
//
// // The model used for the generation of next states.
// storm::jani::Model model;
// };
//
// }
//}

76
src/generator/NextStateGenerator.cpp
View File

@ -4,6 +4,11 @@
#include "src/logic/Formulas.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/storage/expressions/SimpleValuation.h"
#include "src/models/sparse/StateLabeling.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidSettingsException.h"
@ -207,15 +212,82 @@ namespace storm {
}
template<typename ValueType, typename StateType>
NextStateGenerator<ValueType, StateType>::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
NextStateGeneratorOptions const& NextStateGenerator<ValueType, StateType>::getOptions() const {
return options;
}
template<typename ValueType, typename StateType>
uint64_t NextStateGenerator<ValueType, StateType>::getStateSize() const {
return variableInformation.getTotalBitOffset(true);
}
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
unpackStateIntoEvaluator(state, variableInformation, evaluator);
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
}
template<typename ValueType, typename StateType>
bool NextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
if (expression.isTrue()) {
return true;
}
return evaluator.asBool(expression);
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
// Make the labels unique.
std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it));
for (auto const& expression : this->options.getExpressionLabels()) {
std::stringstream stream;
stream << expression;
labelsAndExpressions.push_back(std::make_pair(stream.str(), expression));
}
// Prepare result.
storm::models::sparse::StateLabeling result(states.size());
// Initialize labeling.
for (auto const& label : labelsAndExpressions) {
result.addLabel(label.first);
}
for (auto const& stateIndexPair : states) {
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator);
for (auto const& label : labelsAndExpressions) {
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.second)) {
result.addLabelToState(label.first, stateIndexPair.second);
}
}
}
// Also label the initial state with the special label "init".
result.addLabel("init");
for (auto index : initialStateIndices) {
result.addLabelToState("init", index);
}
return result;
}
template<typename ValueType, typename StateType>
storm::expressions::SimpleValuation NextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
return unpackStateIntoValuation(state, variableInformation, *expressionManager);
}
template class NextStateGenerator<double>;
template class NextStateGenerator<storm::RationalFunction>;

39
src/generator/NextStateGenerator.h
View File

@ -8,13 +8,18 @@
#include "src/storage/expressions/Expression.h"
#include "src/storage/BitVectorHashMap.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
#include "src/generator/VariableInformation.h"
#include "src/generator/CompressedState.h"
#include "src/generator/StateBehavior.h"
#include "src/utility/ConstantsComparator.h"
namespace storm {
namespace expressions {
class Expression;
class ExpressionManager;
}
namespace models {
@ -155,28 +160,52 @@ namespace storm {
public:
typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
NextStateGenerator(NextStateGeneratorOptions const& options);
NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options);
virtual uint64_t getStateSize() const = 0;
uint64_t getStateSize() const;
virtual ModelType getModelType() const = 0;
virtual bool isDeterministicModel() const = 0;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
virtual void load(CompressedState const& state) = 0;
void load(CompressedState const& state);
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
virtual bool satisfies(storm::expressions::Expression const& expression) const = 0;
bool satisfies(storm::expressions::Expression const& expression) const;
virtual std::size_t getNumberOfRewardModels() const = 0;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const = 0;
storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0;
NextStateGeneratorOptions const& getOptions() const;
protected:
/*!
* Creates the state labeling for the given states using the provided labels and expressions.
*/
storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
/// The options to be used for next-state generation.
NextStateGeneratorOptions options;
/// The expression manager used for evaluating expressions.
std::shared_ptr<storm::expressions::ExpressionManager const> expressionManager;
/// The expressions that define terminal states.
std::vector<std::pair<storm::expressions::Expression, bool>> terminalStates;
/// Information about how the variables are packed.
VariableInformation variableInformation;
/// An evaluator used to evaluate expressions.
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
/// The currently loaded state.
CompressedState const* state;
/// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;
};
}
}

131
src/generator/PrismNextStateGenerator.cpp
View File

@ -15,7 +15,12 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator<ValueType, StateType>(options), program(program.substituteConstants()), rewardModels(), variableInformation(this->program), evaluator(this->program.getManager()), state(nullptr), comparator() {
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator<ValueType, StateType>(program.substituteConstants(), options, false) {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), VariableInformation(program), options), program(program.substituteConstants()), rewardModels() {
STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
if (this->options.isBuildAllRewardModelsSet()) {
@ -50,19 +55,14 @@ namespace storm {
if (this->options.hasTerminalStates()) {
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
if (expressionOrLabelAndBool.first.isExpression()) {
terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
this->terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
}
}
}
}
template<typename ValueType, typename StateType>
uint64_t PrismNextStateGenerator<ValueType, StateType>::getStateSize() const {
return variableInformation.getTotalBitOffset(true);
}
template<typename ValueType, typename StateType>
ModelType PrismNextStateGenerator<ValueType, StateType>::getModelType() const {
switch (program.getModelType()) {
@ -83,13 +83,13 @@ namespace storm {
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());
CompressedState initialState(this->variableInformation.getTotalBitOffset());
// We need to initialize the values of the variables to their initial value.
for (auto const& booleanVariable : variableInformation.booleanVariables) {
for (auto const& booleanVariable : this->variableInformation.booleanVariables) {
initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
}
for (auto const& integerVariable : variableInformation.integerVariables) {
for (auto const& integerVariable : this->variableInformation.integerVariables) {
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
}
@ -98,23 +98,6 @@ namespace storm {
return {id};
}
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
unpackStateIntoEvaluator(state, variableInformation, evaluator);
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
}
template<typename ValueType, typename StateType>
bool PrismNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
if (expression.isTrue()) {
return true;
}
return evaluator.asBool(expression);
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
// Prepare the result, in case we return early.
@ -126,8 +109,8 @@ namespace storm {
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()));
if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression()));
}
}
}
@ -135,9 +118,9 @@ namespace storm {
}
// If a terminal expression was set and we must not expand this state, return now.
if (!terminalStates.empty()) {
for (auto const& expressionBool : terminalStates) {
if (evaluator.asBool(expressionBool.first) == expressionBool.second) {
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
return result;
}
}
@ -191,8 +174,8 @@ namespace storm {
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
for (auto const& choice : allChoices) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
}
}
@ -223,21 +206,21 @@ namespace storm {
auto assignmentIte = update.getAssignments().end();
// Iterate over all boolean assignments and carry them out.
auto boolIt = variableInformation.booleanVariables.begin();
auto boolIt = this->variableInformation.booleanVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
while (assignmentIt->getVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression()));
newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
auto integerIt = variableInformation.integerVariables.begin();
auto integerIt = this->variableInformation.integerVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
while (assignmentIt->getVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<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 << ").");
@ -275,7 +258,7 @@ namespace storm {
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (evaluator.asBool(command.getGuardExpression())) {
if (this->evaluator.asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
@ -308,7 +291,7 @@ namespace storm {
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!evaluator.asBool(command.getGuardExpression())) {
if (!this->evaluator.asBool(command.getGuardExpression())) {
continue;
}
@ -330,7 +313,7 @@ namespace storm {
StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
// Update the choice by adding the probability/target state to it.
ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
@ -340,8 +323,8 @@ namespace storm {
ValueType stateActionRewardValue = storm::utility::zero<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();
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
}
}
}
@ -349,7 +332,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
}
}
@ -395,9 +378,9 @@ namespace storm {
// and otherwise insert it.
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression());
targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression());
} else {
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()));
}
}
}
@ -435,15 +418,15 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
STORM_LOG_THROW(!program.isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
// Create the state-action reward for the newly created choice.
for (auto const& rewardModel : rewardModels) {
ValueType stateActionRewardValue = storm::utility::zero<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();
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
}
}
}
@ -476,7 +459,7 @@ namespace storm {
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
// Gather a vector of labels and their expressions so we can iterate it over it a lot.
// Gather a vector of labels and their expressions.
std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
if (this->options.isBuildAllLabelsSet()) {
for (auto const& label : program.getLabels()) {
@ -487,43 +470,8 @@ namespace storm {
labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
}
}
// Make the labels unique.
std::sort(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
auto it = std::unique(labels.begin(), labels.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
labels.resize(std::distance(labels.begin(), it));
for (auto const& expression : this->options.getExpressionLabels()) {
std::stringstream stream;
stream << expression;
labels.push_back(std::make_pair(stream.str(), expression));
}
// Prepare result.
storm::models::sparse::StateLabeling result(states.size());
// Initialize labeling.
for (auto const& label : labels) {
result.addLabel(label.first);
}
for (auto const& stateIndexPair : states) {
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator);
for (auto const& label : labels) {
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.second)) {
result.addLabelToState(label.first, stateIndexPair.second);
}
}
}
// Also label the initial state with the special label "init".
result.addLabel("init");
for (auto index : initialStateIndices) {
result.addLabelToState("init", index);
}
return result;
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, labels);
}
template<typename ValueType, typename StateType>
@ -536,12 +484,7 @@ namespace storm {
storm::prism::RewardModel const& rewardModel = rewardModels[index].get();
return RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards());
}
template<typename ValueType, typename StateType>
storm::expressions::SimpleValuation PrismNextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
return unpackStateIntoValuation(state, variableInformation, program.getManager());
}
template class PrismNextStateGenerator<double>;
template class PrismNextStateGenerator<storm::RationalFunction>;
}

31
src/generator/PrismNextStateGenerator.h
View File

@ -2,12 +2,8 @@
#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
#include "src/generator/NextStateGenerator.h"
#include "src/generator/VariableInformation.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
#include "src/utility/ConstantsComparator.h"
namespace storm {
namespace generator {
@ -19,23 +15,25 @@ namespace storm {
PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
virtual uint64_t getStateSize() const override;
virtual ModelType getModelType() const override;
virtual bool isDeterministicModel() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
virtual void load(CompressedState const& state) override;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
virtual bool satisfies(storm::expressions::Expression const& expression) const override;
virtual std::size_t getNumberOfRewardModels() const override;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
virtual storm::expressions::SimpleValuation toValuation(CompressedState const& state) const override;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
private:
/*!
* A delegate constructor that is used to preprocess the program before the constructor of the superclass is
* being called. The last argument is only present to distinguish the signature of this constructor from the
* public one.
*/
PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag);
/*!
* Applies an update to the state currently loaded into the evaluator and applies the resulting values to
* the given compressed state.
@ -85,23 +83,8 @@ namespace storm {
// The reward models that need to be considered.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> rewardModels;
// The expressions that define terminal states.
std::vector<std::pair<storm::expressions::Expression, bool>> terminalStates;
// A flag that stores whether at least one of the selected reward models has state-action rewards.
bool hasStateActionRewards;
// Information about how the variables are packed.
VariableInformation variableInformation;
// An evaluator used to evaluate expressions.
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
// The currently loaded state.
CompressedState const* state;
// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;
};
}

4
src/storage/jani/Model.cpp
View File

@ -353,6 +353,10 @@ namespace storm {
this->initialStatesExpression = initialStatesExpression;
}
bool Model::isDeterministicModel() const {
return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
}
bool Model::checkValidity(bool logdbg) const {
// TODO switch to exception based return value.

5
src/storage/jani/Model.h
View File

@ -243,6 +243,11 @@ namespace storm {
*/
void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
/*!
* Determines whether this model is a deterministic one in the sense that each state only has one choice.
*/
bool isDeterministicModel() const;
/*!
* Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
*/

Write Preview
Loading…
Cancel
Save