|
|
@ -61,7 +61,9 @@ namespace storm { |
|
|
|
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); |
|
|
|
|
|
|
|
storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); |
|
|
|
STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants."); |
|
|
|
if (!std::is_same<ValueType, RationalFunction>::value) { |
|
|
|
STORM_LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants."); |
|
|
|
} |
|
|
|
|
|
|
|
// Now that we have defined all the constants in the program, we need to substitute their appearances in
|
|
|
|
// all expressions in the program so we can then evaluate them without having to store the values of the
|
|
|
@ -105,7 +107,7 @@ namespace storm { |
|
|
|
} |
|
|
|
|
|
|
|
template <typename ValueType, typename IndexType> |
|
|
|
void ExplicitPrismModelBuilder<ValueType, IndexType>::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator) { |
|
|
|
void ExplicitPrismModelBuilder<ValueType, 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)); |
|
|
|
} |
|
|
@ -115,12 +117,12 @@ 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::ExprtkExpressionEvaluator const& evaluator) { |
|
|
|
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) { |
|
|
|
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::ExprtkExpressionEvaluator const& evaluator) { |
|
|
|
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) { |
|
|
|
CompressedState newState(state); |
|
|
|
|
|
|
|
auto assignmentIt = update.getAssignments().begin(); |
|
|
@ -166,7 +168,7 @@ namespace storm { |
|
|
|
} |
|
|
|
|
|
|
|
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::ExprtkExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) { |
|
|
|
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) { |
|
|
|
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.
|
|
|
@ -209,7 +211,7 @@ namespace storm { |
|
|
|
} |
|
|
|
|
|
|
|
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::ExprtkExpressionEvaluator const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) { |
|
|
|
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) { |
|
|
|
std::vector<Choice<ValueType>> result; |
|
|
|
|
|
|
|
// Iterate over all modules.
|
|
|
@ -237,7 +239,7 @@ namespace storm { |
|
|
|
} |
|
|
|
|
|
|
|
// Iterate over all updates of the current command.
|
|
|
|
double probabilitySum = 0; |
|
|
|
ValueType probabilitySum = storm::utility::zero<ValueType>(); |
|
|
|
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { |
|
|
|
storm::prism::Update const& update = command.getUpdate(k); |
|
|
|
|
|
|
@ -246,7 +248,7 @@ namespace storm { |
|
|
|
uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), stateInformation, stateQueue); |
|
|
|
|
|
|
|
// Update the choice by adding the probability/target state to it.
|
|
|
|
ValueType probability = evaluator.asDouble(update.getLikelihoodExpression()); |
|
|
|
ValueType probability = evaluator.asRational(update.getLikelihoodExpression()); |
|
|
|
choice.addProbability(stateIndex, probability); |
|
|
|
probabilitySum += probability; |
|
|
|
} |
|
|
@ -260,7 +262,7 @@ namespace storm { |
|
|
|
} |
|
|
|
|
|
|
|
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::ExprtkExpressionEvaluator const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) { |
|
|
|
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) { |
|
|
|
std::vector<Choice<ValueType>> result; |
|
|
|
|
|
|
|
for (uint_fast64_t actionIndex : program.getActionIndices()) { |
|
|
@ -294,7 +296,7 @@ namespace storm { |
|
|
|
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(variableInformation, stateProbabilityPair.first, currentState, update, evaluator); |
|
|
|
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asDouble(update.getLikelihoodExpression())); |
|
|
|
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
@ -322,7 +324,7 @@ namespace storm { |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
double probabilitySum = 0; |
|
|
|
ValueType probabilitySum = storm::utility::zero<ValueType>(); |
|
|
|
for (auto const& stateProbabilityPair : *newTargetStates) { |
|
|
|
uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue); |
|
|
|
choice.addProbability(actualIndex, stateProbabilityPair.second); |
|
|
@ -385,12 +387,12 @@ namespace storm { |
|
|
|
|
|
|
|
// Now explore the current state until there is no more reachable state.
|
|
|
|
uint_fast64_t currentRow = 0; |
|
|
|
storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); |
|
|
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager()); |
|
|
|
while (!stateQueue.empty()) { |
|
|
|
// Get the current state and unpack it.
|
|
|
|
storm::storage::BitVector currentState = stateQueue.front(); |
|
|
|
stateQueue.pop(); |
|
|
|
ValueType stateIndex = stateInformation.stateStorage.getValue(currentState); |
|
|
|
IndexType stateIndex = stateInformation.stateStorage.getValue(currentState); |
|
|
|
unpackStateIntoEvaluator(currentState, variableInformation, evaluator); |
|
|
|
|
|
|
|
// Retrieve all choices for the current state.
|
|
|
@ -432,7 +434,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
@ -443,7 +445,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (transitionReward.isLabeled() && transitionReward.getActionIndex() == globalChoice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
@ -486,7 +488,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
@ -502,7 +504,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (transitionReward.isLabeled() && transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
@ -544,7 +546,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
@ -573,7 +575,7 @@ namespace storm { |
|
|
|
// Now add all rewards that match this choice.
|
|
|
|
for (auto const& transitionReward : transitionRewards) { |
|
|
|
if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); |
|
|
|
stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asRational(transitionReward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
@ -659,7 +661,7 @@ namespace storm { |
|
|
|
|
|
|
|
template <typename ValueType, typename IndexType> |
|
|
|
storm::models::AtomicPropositionsLabeling ExplicitPrismModelBuilder<ValueType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { |
|
|
|
storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); |
|
|
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager()); |
|
|
|
|
|
|
|
std::vector<storm::prism::Label> const& labels = program.getLabels(); |
|
|
|
|
|
|
@ -690,7 +692,7 @@ namespace storm { |
|
|
|
|
|
|
|
template <typename ValueType, typename IndexType> |
|
|
|
std::vector<ValueType> ExplicitPrismModelBuilder<ValueType, IndexType>::buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) { |
|
|
|
storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); |
|
|
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager()); |
|
|
|
|
|
|
|
std::vector<ValueType> result(stateInformation.reachableStates.size()); |
|
|
|
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { |
|
|
@ -700,7 +702,7 @@ namespace storm { |
|
|
|
|
|
|
|
// Add this reward to the state if the state is included in the state reward.
|
|
|
|
if (evaluator.asBool(reward.getStatePredicateExpression())) { |
|
|
|
result[index] += ValueType(evaluator.asDouble(reward.getRewardValueExpression())); |
|
|
|
result[index] += ValueType(evaluator.asRational(reward.getRewardValueExpression())); |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
@ -709,5 +711,6 @@ namespace storm { |
|
|
|
|
|
|
|
// Explicitly instantiate the class.
|
|
|
|
template class ExplicitPrismModelBuilder<double, uint32_t>; |
|
|
|
template class ExplicitPrismModelBuilder<RationalFunction, uint32_t>; |
|
|
|
} |
|
|
|
} |
xxxxxxxxxx