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

some fixes for using something different from doubles for templated value type :) 

Former-commit-id: d26d06b265
main
sjunges 11 years ago
parent
f9a0c94c1b
commit
8142a8e004
6 changed files with 164 additions and 42 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. 52
      src/adapters/ExplicitModelAdapter.h
  2. 4
      src/models/Ctmdp.h
  3. 23
      src/models/Dtmc.h
  4. 4
      src/models/Mdp.h
  5. 99
      src/storage/expressions/ExpressionEvaluation.h
  6. 16
      src/utility/constants.h

52
src/adapters/ExplicitModelAdapter.h
View File

@ -30,6 +30,7 @@
#include "src/settings/Settings.h"
#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/storage/expressions/ExpressionEvaluation.h"
namespace storm {
namespace adapters {
@ -321,7 +322,7 @@ namespace storm {
return result;
}
static std::list<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
static std::list<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue, expressions::ExpressionEvaluation<ValueType>& eval) {
std::list<Choice<ValueType>> result;
StateType const* currentState = stateInformation.reachableStates[stateIndex];
@ -346,7 +347,7 @@ namespace storm {
Choice<ValueType>& choice = result.back();
choice.addChoiceLabel(command.getGlobalIndex());
double probabilitySum = 0;
ValueType probabilitySum = utility::constantZero<ValueType>();
// Iterate over all updates of the current command.
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(k);
@ -360,7 +361,7 @@ namespace storm {
}
// Update the choice by adding the probability/target state to it.
double probabilityToAdd = update.getLikelihoodExpression().evaluateAsDouble(currentState);
ValueType probabilityToAdd = eval.evaluate(update.getLikelihoodExpression(),currentState);
probabilitySum += probabilityToAdd;
boost::container::flat_set<uint_fast64_t> labels;
labels.insert(update.getGlobalIndex());
@ -368,14 +369,14 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
LOG_THROW(!storm::utility::isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
}
}
return result;
}
static std::list<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
static std::list<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue, expressions::ExpressionEvaluation<ValueType>& eval) {
std::list<Choice<ValueType>> result;
for (std::string const& action : program.getActions()) {
@ -395,9 +396,9 @@ namespace storm {
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>* currentTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>* newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
(*currentTargetStates)[new StateType(*currentState)] = storm::storage::LabeledValues<double>(1.0);
std::unordered_map<StateType*, storm::storage::LabeledValues<ValueType>, StateHash, StateCompare>* currentTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<ValueType>, StateHash, StateCompare>();
std::unordered_map<StateType*, storm::storage::LabeledValues<ValueType>, StateHash, StateCompare>* newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<ValueType>, StateHash, StateCompare>();
(*currentTargetStates)[new StateType(*currentState)] = storm::storage::LabeledValues<ValueType>(ValueType(1));
// FIXME: This does not check whether a global variable is written multiple times. While the
// behaviour for this is undefined anyway, a warning should be issued in that case.
@ -410,9 +411,9 @@ namespace storm {
for (auto const& stateProbabilityPair : *currentTargetStates) {
StateType* newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update);
storm::storage::LabeledValues<double> newProbability;
storm::storage::LabeledValues<ValueType> newProbability;
double updateProbability = update.getLikelihoodExpression().evaluateAsDouble(currentState);
ValueType updateProbability = eval.evaluate(update.getLikelihoodExpression(),currentState);
for (auto const& valueLabelSetPair : stateProbabilityPair.second) {
// Copy the label set, so we can modify it.
boost::container::flat_set<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
@ -441,7 +442,7 @@ namespace storm {
delete currentTargetStates;
currentTargetStates = newTargetStates;
newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<double>, StateHash, StateCompare>();
newTargetStates = new std::unordered_map<StateType*, storm::storage::LabeledValues<ValueType>, StateHash, StateCompare>();
}
}
@ -458,7 +459,7 @@ namespace storm {
choice.addChoiceLabel(iteratorList[i]->getGlobalIndex());
}
double probabilitySum = 0;
ValueType probabilitySum = utility::constantZero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation);
@ -474,7 +475,7 @@ namespace storm {
}
// Check that the resulting distribution is in fact a distribution.
if (std::abs(1 - probabilitySum) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
if (!storm::utility::isOne(probabilitySum)) {
LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command.");
throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command.";
}
@ -519,7 +520,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 std::vector<boost::container::flat_set<uint_fast64_t>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder) {
static std::vector<boost::container::flat_set<uint_fast64_t>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder, expressions::ExpressionEvaluation<ValueType>& eval) {
std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabels;
// Initialize a queue and insert the initial state.
@ -550,8 +551,8 @@ namespace storm {
uint_fast64_t currentState = stateQueue.front();
// Retrieve all choices for the current state.
std::list<Choice<ValueType>> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue);
std::list<Choice<ValueType>> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue);
std::list<Choice<ValueType>> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, eval);
std::list<Choice<ValueType>> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue, eval);
uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
@ -582,7 +583,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
stateToRewardMap[stateProbabilityPair.first] += eval.evaluate(transitionReward.getRewardValueExpression(),stateInformation.reachableStates.at(currentState));
}
}
}
@ -595,7 +596,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
stateToRewardMap[stateProbabilityPair.first] += eval.evaluate(transitionReward.getRewardValueExpression(),stateInformation.reachableStates.at(currentState));
}
}
}
@ -633,7 +634,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
stateToRewardMap[stateProbabilityPair.first] += eval.evaluate(transitionReward.getRewardValueExpression(),stateInformation.reachableStates.at(currentState));
}
}
@ -660,7 +661,7 @@ namespace storm {
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
stateToRewardMap[stateProbabilityPair.first] += eval.evaluate(transitionReward.getRewardValueExpression(),stateInformation.reachableStates.at(currentState));
}
}
@ -694,6 +695,7 @@ namespace storm {
*/
static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
ModelComponents modelComponents;
expressions::ExpressionEvaluation<ValueType> eval;
VariableInformation variableInformation;
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
@ -718,7 +720,7 @@ namespace storm {
// Build the transition and reward matrices.
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0);
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder, eval);
// Finalize the resulting matrices.
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
@ -728,7 +730,7 @@ namespace storm {
modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);
// Finally, construct the state rewards.
modelComponents.stateRewards = buildStateRewards(rewardModel.getStateRewards(), stateInformation);
modelComponents.stateRewards = buildStateRewards(rewardModel.getStateRewards(), stateInformation, eval);
// After everything has been created, we can delete the states.
for (auto state : stateInformation.reachableStates) {
@ -780,14 +782,14 @@ namespace storm {
* @param stateInformation Information about the state space.
* @return A vector containing the state rewards for the state space.
*/
static std::vector<ValueType> buildStateRewards(std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) {
static std::vector<ValueType> buildStateRewards(std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation, expressions::ExpressionEvaluation<ValueType>& eval) {
std::vector<ValueType> result(stateInformation.reachableStates.size());
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
result[index] = ValueType(0);
for (auto const& reward : rewards) {
// Add this reward to the state if the state is included in the state reward.
if (reward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
result[index] += ValueType(reward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates[index]));
result[index] += eval.evaluate(reward.getRewardValueExpression(),stateInformation.reachableStates[index]);
}
}
}
@ -795,6 +797,8 @@ namespace storm {
}
};
} // namespace adapters
} // namespace storm

4
src/models/Ctmdp.h
View File

@ -127,12 +127,10 @@ private:
*/
bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > precision) return false;
if (storm::utility::isOne(sum)) return false;
}
return true;
}

23
src/models/Dtmc.h
View File

@ -46,8 +46,8 @@ public:
* @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state.
*/
Dtmc(storm::storage::SparseMatrix<T> const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
boost::optional<std::vector<T>> const& optionalStateRewardVector = {}, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix = {},
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = {})
: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@ -190,11 +190,11 @@ public:
// The number of transitions of the new Dtmc is the number of transitions transfered
// from the old one plus one transition for each state to s_b.
storm::storage::SparseMatrixBuilder<T> newMatBuilder(newStateCount, subSysTransitionCount + newStateCount);
storm::storage::SparseMatrixBuilder<T> newMatBuilder(newStateCount,newStateCount,subSysTransitionCount + newStateCount);
// Now fill the matrix.
newRow = 0;
T rest = 0;
T rest = utility::constantZero<T>();
for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) {
if(subSysStates.get(row)){
// Transfer transitions
@ -299,8 +299,7 @@ private:
*/
bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
// not square
@ -310,18 +309,26 @@ private:
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) {
if (sum == T(0)) {
LOG4CPLUS_ERROR(logger, "Row " << row << " is a deadlock (sum == " << sum << ").");
return false;
}
if (std::abs(sum - 1) > precision) {
if (storm::utility::isOne(sum)) {
LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum << ".");
return false;
}
}
return true;
}
};
} // namespace models
} // namespace storm

4
src/models/Mdp.h
View File

@ -198,13 +198,11 @@ private:
*/
bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > precision) {
if (!storm::utility::isOne(sum)) {
return false;
}
}

99
src/storage/expressions/ExpressionEvaluation.h
View File

@ -0,0 +1,99 @@
/**
* @file: ExpressionEvaluation.h
* @author: Sebastian Junges
*
* @since April 4, 2014
*/
#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATION_H_
#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATION_H_
#include "ExpressionVisitor.h"
#include "BaseExpression.h"
namespace storm {
namespace expressions {
template<typename T>
struct StateType
{
typedef int type;
};
template<typename T, typename S>
class ExpressionEvaluationVisitor : public ExpressionVisitor
{
public:
ExpressionEvaluationVisitor(S* sharedState)
: mSharedState(sharedState)
{
}
virtual void visit(IfThenElseExpression const* expression) = 0;
virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0;
virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0;
virtual void visit(BinaryRelationExpression const* expression) = 0;
virtual void visit(BooleanConstantExpression const* expression) = 0;
virtual void visit(DoubleConstantExpression const* expression) = 0;
virtual void visit(IntegerConstantExpression const* expression) = 0;
virtual void visit(VariableExpression const* expression) = 0;
virtual void visit(UnaryBooleanFunctionExpression const* expression) = 0;
virtual void visit(UnaryNumericalFunctionExpression const* expression) = 0;
virtual void visit(BooleanLiteralExpression const* expression) = 0;
virtual void visit(IntegerLiteralExpression const* expression) = 0;
virtual void visit(DoubleLiteralExpression const* expression) = 0;
const T& value() const
{
return mValue;
}
private:
S* mSharedState;
T mValue;
};
template<typename T>
class ExpressionEvaluation
{
public:
ExpressionEvaluation() : mState()
{
}
T evaluate(Expression const& expr, storm::expressions::SimpleValuation const*)
{
ExpressionEvaluationVisitor<T, typename StateType<T>::type>* visitor = new ExpressionEvaluationVisitor<T, typename StateType<T>::type>(&mState);
expr.getBaseExpression().accept(visitor);
T result = visitor->value();
delete visitor;
return result;
}
protected:
typename StateType<T>::type mState;
};
/**
* For doubles, we keep using the getValueAs from the expressions, as this should be more efficient.
*/
template<>
class ExpressionEvaluation<double>
{
public:
double evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) const
{
return expr.evaluateAsDouble(val);
}
};
}
}
#endif

16
src/utility/constants.h
View File

@ -21,6 +21,7 @@
#include "src/exceptions/InvalidArgumentException.h"
#include "src/storage/BitVector.h"
#include "src/storage/LabeledValues.h"
#include "src/settings/Settings.h"
namespace storm {
@ -202,6 +203,21 @@ inline storm::storage::LabeledValues<double> constantInfinity() {
/*! @endcond */
template<typename T>
inline bool isOne(T sum)
{
return (sum-T(1)).isZero();
}
template<>
inline bool isOne(double sum)
{
storm::settings::Settings* s = storm::settings::Settings::getInstance();
double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
return std::abs(sum - 1) < precision;
}
} //namespace utility
} //namespace storm

Write Preview
Loading…
Cancel
Save