From 01bd1fbc7669b4388ea3d0a41d017c0156f5e51f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 17 Jan 2015 12:22:49 +0100
Subject: [PATCH] Model building works again for parametric systems.
Former-commit-id: d3f3e357cac3bd440485800bec96f9602e64a43e
---
src/adapters/extendedCarl.h | 1 +
src/builder/ExplicitPrismModelBuilder.cpp | 47 ++--
src/builder/ExplicitPrismModelBuilder.h | 14 +-
.../reachability/CollectConstraints.h | 6 +-
src/models/Dtmc.h | 4 +-
.../expressions/ExpressionEvaluation.h | 209 ------------------
.../expressions/ExpressionEvaluator.cpp | 36 +++
src/storage/expressions/ExpressionEvaluator.h | 43 +++-
.../expressions/ExpressionEvaluatorBase.cpp | 12 +-
.../expressions/ExpressionEvaluatorBase.h | 3 +-
.../expressions/ExprtkExpressionEvaluator.cpp | 51 +++--
.../expressions/ExprtkExpressionEvaluator.h | 39 ++--
.../expressions/ToRationalFunctionVisitor.cpp | 102 +++++++++
.../expressions/ToRationalFunctionVisitor.h | 53 +++++
src/storage/parameters.h | 6 +-
src/stormParametric.cpp | 2 +-
16 files changed, 339 insertions(+), 289 deletions(-)
delete mode 100644 src/storage/expressions/ExpressionEvaluation.h
create mode 100644 src/storage/expressions/ToRationalFunctionVisitor.cpp
create mode 100644 src/storage/expressions/ToRationalFunctionVisitor.h
diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h
index fddb4950f..1fb6ca9c0 100644
--- a/src/adapters/extendedCarl.h
+++ b/src/adapters/extendedCarl.h
@@ -23,6 +23,7 @@ namespace carl
std::hash<carl::MultivariatePolynomial<C,O,P>> h;
return h(p);
}
+
template<typename Pol>
inline size_t hash_value(carl::RationalFunction<Pol> const& f)
{
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index ce88522eb..4b69e3988 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -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>;
}
}
\ No newline at end of file
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index ee35e4108..9b024ea04 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -12,7 +12,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/SimpleValuation.h"
-#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
#include "src/storage/BitVectorHashMap.h"
#include "src/models/AbstractModel.h"
#include "src/models/AtomicPropositionsLabeling.h"
@@ -132,7 +132,7 @@ namespace storm {
static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, bool commandLabels = false, bool rewards = true, std::string const& rewardModelName = "", std::string const& constantDefinitionString = "");
private:
- static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator);
+ static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
/*!
* Applies an update to the given state and returns the resulting new state object. This methods does not
@@ -142,7 +142,7 @@ namespace storm {
* @params update The update to apply.
* @return The resulting state.
*/
- static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator);
+ static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
/*!
* Applies an update to the given state and returns the resulting new state object. The update is evaluated
@@ -154,7 +154,7 @@ namespace storm {
* @param update The update to apply.
* @return The resulting state.
*/
- static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator);
+ static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
/*!
* Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
@@ -184,11 +184,11 @@ namespace storm {
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
- static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExprtkExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex);
+ static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex);
- static std::vector<Choice<ValueType>> 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);
+ static std::vector<Choice<ValueType>> 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);
- static std::vector<Choice<ValueType>> 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);
+ static std::vector<Choice<ValueType>> 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);
/*!
* Builds the transition matrix and the transition reward matrix based for the given program.
*
diff --git a/src/modelchecker/reachability/CollectConstraints.h b/src/modelchecker/reachability/CollectConstraints.h
index cd7fa90f3..d77273770 100644
--- a/src/modelchecker/reachability/CollectConstraints.h
+++ b/src/modelchecker/reachability/CollectConstraints.h
@@ -8,7 +8,6 @@
#pragma once
#include "src/models/Dtmc.h"
-
namespace storm {
namespace modelchecker {
namespace reachability {
@@ -18,6 +17,7 @@ namespace modelchecker {
private:
std::unordered_set<carl::Constraint<ValueType>> wellformedConstraintSet;
std::unordered_set<carl::Constraint<ValueType>> graphPreservingConstraintSet;
+ storm::utility::ConstantsComparator<ValueType> comparator;
public:
std::unordered_set<carl::Constraint<ValueType>> const& wellformedConstraints() const {
@@ -33,7 +33,7 @@ namespace modelchecker {
for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state)
{
ValueType sum;
- assert(storm::utility::isZero(sum));
+ assert(comparator.isZero(sum));
for(auto const& transition : dtmc.getRows(state))
{
sum += transition.getValue();
@@ -44,7 +44,7 @@ namespace modelchecker {
graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT);
}
}
- assert(!sum.isConstant() || storm::utility::isOne(sum));
+ assert(!comparator.isConstant(sum) || comparator.isOne(sum));
if(!sum.isConstant()) {
wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
}
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 8c082690f..1eaa9e138 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -354,9 +354,7 @@ private:
}
return true;
}
-
-
-
+
};
diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h
deleted file mode 100644
index 89a32b038..000000000
--- a/src/storage/expressions/ExpressionEvaluation.h
+++ /dev/null
@@ -1,209 +0,0 @@
-/**
- * @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"
-#include "IfThenElseExpression.h"
-#include "DoubleLiteralExpression.h"
-#include "BinaryNumericalFunctionExpression.h"
-
-#include "src/storage/parameters.h"
-#include "IntegerLiteralExpression.h"
-#include "BinaryExpression.h"
-#include "src/storage/parameters.h"
-
-namespace storm {
- namespace expressions {
-
- template<typename T>
- struct StateType
- {
- typedef int type;
- };
-
-#ifdef PARAMETRIC_SYSTEMS
- template<>
- struct StateType<Polynomial>
- {
- typedef std::map<std::string, carl::Variable> type;
- };
-
- template<>
- struct StateType<RationalFunction>
- {
- typedef std::map<std::string, carl::Variable> type;
- };
-#endif
-
- template<typename T, typename S>
- class ExpressionEvaluationVisitor : public ExpressionVisitor
- {
- public:
- ExpressionEvaluationVisitor(S* sharedState)
- : mSharedState(sharedState), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>())
- {
-
- }
-
- ExpressionEvaluationVisitor(S* sharedState, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache)
- : mSharedState(sharedState), cache(cache)
- {
-
- }
-
-
- virtual ~ExpressionEvaluationVisitor() {
-
- }
-
- virtual void visit(IfThenElseExpression const* expression)
- {
- std::cout << "ite" << std::endl;
-
- }
-
- virtual void visit(BinaryBooleanFunctionExpression const* expression)
- {
- std::cout << "bbf" << std::endl;
- }
- virtual void visit(BinaryNumericalFunctionExpression const* expression)
- {
- ExpressionEvaluationVisitor* visitor = new ExpressionEvaluationVisitor(mSharedState, this->cache);
- expression->getFirstOperand()->accept(visitor);
- mValue = visitor->value();
- expression->getSecondOperand()->accept(visitor);
- switch(expression->getOperatorType())
- {
- case BinaryNumericalFunctionExpression::OperatorType::Plus:
- mValue += visitor->value();
- break;
- case BinaryNumericalFunctionExpression::OperatorType::Minus:
- mValue -= visitor->value();
- break;
- case BinaryNumericalFunctionExpression::OperatorType::Times:
- mValue *= visitor->value();
- break;
- case BinaryNumericalFunctionExpression::OperatorType::Divide:
- mValue /= visitor->value();
- break;
- default:
- // TODO exception.
- assert(false);
- }
-
- delete visitor;
- }
- virtual void visit(BinaryRelationExpression const* expression)
- {
- std::cout << "br" << std::endl;
- }
- virtual void visit(VariableExpression const* expression)
- {
- std::string const& varName= expression->getVariableName();
- auto it = mSharedState->find(varName);
- if(it != mSharedState->end())
- {
- mValue = convertVariableToPolynomial(it->second);
-// mValue = T(typename T::PolyType(typename T::PolyType::PolyType(it->second), cache));
- }
- else
- {
- carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(varName);
- mSharedState->emplace(varName,nVar);
- mValue = convertVariableToPolynomial(nVar);
- }
- }
- virtual void visit(UnaryBooleanFunctionExpression const* expression)
- {
- std::cout << "ubf" << std::endl;
- }
- virtual void visit(UnaryNumericalFunctionExpression const* expression)
- {
- std::cout << "unf" << std::endl;
- }
- virtual void visit(BooleanLiteralExpression const* expression)
- {
- std::cout << "bl" << std::endl;
- }
- virtual void visit(IntegerLiteralExpression const* expression)
- {
- mValue = T(typename T::PolyType(typename T::CoeffType(expression->getValue())));
- }
- virtual void visit(DoubleLiteralExpression const* expression)
- {
- std::stringstream str;
- str << std::fixed << std::setprecision( 3 ) << expression->getValue();
- mValue = T(carl::rationalize<cln::cl_RA>(str.str()));
- }
-
- template<typename TP = typename T::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
- T convertVariableToPolynomial(carl::Variable const& nVar) {
- return T(typename T::PolyType(typename T::PolyType::PolyType(nVar), cache));
- }
-
- template<typename TP = typename T::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
- T convertVariableToPolynomial(carl::Variable const& nVar) {
- return T(nVar);
- }
-
- const T& value() const
- {
- return mValue;
- }
-
- private:
- S* mSharedState;
- T mValue;
- std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
- };
-
- template<typename T>
- class ExpressionEvaluation
- {
- public:
- ExpressionEvaluation() : mState(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>(100000))
- {
- // Intentionally left empty.
- }
-
-
- T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val)
- {
- ExpressionEvaluationVisitor<T, typename StateType<T>::type>* visitor = new ExpressionEvaluationVisitor<T, typename StateType<T>::type>(&mState, cache);
- Expression expressionToTranslate = expr.substitute(*val);
- expressionToTranslate.getBaseExpression().accept(visitor);
- T result = visitor->value();
- // result.simplify();
- delete visitor;
- return result;
- }
-
- protected:
- typename StateType<T>::type mState;
- std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
- };
-
- /**
- * 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
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluator.cpp b/src/storage/expressions/ExpressionEvaluator.cpp
index e69de29bb..cf927a0ff 100644
--- a/src/storage/expressions/ExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExpressionEvaluator.cpp
@@ -0,0 +1,36 @@
+#include "src/storage/expressions/ExpressionEvaluator.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+ namespace expressions {
+ ExpressionEvaluator<double>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluator(manager) {
+ // Intentionally left empty.
+ }
+
+#ifdef PARAMETRIC_SYSTEMS
+ ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
+ // Intentionally left empty.
+ }
+
+ void ExpressionEvaluator<RationalFunction>::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
+ ExprtkExpressionEvaluatorBase::setBooleanValue(variable, value);
+ this->variableToExpressionMap[variable] = this->getManager().boolean(value);
+ }
+
+ void ExpressionEvaluator<RationalFunction>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
+ ExprtkExpressionEvaluatorBase::setIntegerValue(variable, value);
+ this->variableToExpressionMap[variable] = this->getManager().integer(value);
+ }
+
+ void ExpressionEvaluator<RationalFunction>::setRationalValue(storm::expressions::Variable const& variable, double value) {
+ ExprtkExpressionEvaluatorBase::setRationalValue(variable, value);
+ this->variableToExpressionMap[variable] = this->getManager().rational(value);
+ }
+
+ RationalFunction ExpressionEvaluator<RationalFunction>::asRational(Expression const& expression) const {
+ Expression substitutedExpression = expression.substitute(variableToExpressionMap);
+ return this->rationalFunctionVisitor.toRationalFunction(substitutedExpression);
+ }
+#endif
+ }
+}
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h
index 5291029c4..5229807f0 100644
--- a/src/storage/expressions/ExpressionEvaluator.h
+++ b/src/storage/expressions/ExpressionEvaluator.h
@@ -1,11 +1,46 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_
+#define STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_
+
+#include <unordered_map>
+
+#include "src/storage/parameters.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
+#include "src/storage/expressions/ToRationalFunctionVisitor.h"
+
namespace storm {
namespace expressions {
- template<RationalType>
+ template<typename RationalType>
class ExpressionEvaluator;
template<>
- class ExpressionEvaluator<double> {
+ class ExpressionEvaluator<double> : public ExprtkExpressionEvaluator {
+ public:
+ ExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
+ };
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ class ExpressionEvaluator<RationalFunction> : public ExprtkExpressionEvaluatorBase<RationalFunction> {
+ public:
+ ExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
+
+ void setBooleanValue(storm::expressions::Variable const& variable, bool value) override;
+ void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override;
+ void setRationalValue(storm::expressions::Variable const& variable, double value) override;
+
+ RationalFunction asRational(Expression const& expression) const override;
+
+ private:
+ // A mapping of variables to their expressions.
+ std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> variableToExpressionMap;
- }
+ // A visitor that can be used to translate expressions to rational functions.
+ mutable ToRationalFunctionVisitor<RationalFunction> rationalFunctionVisitor;
+ };
+#endif
}
-}
\ No newline at end of file
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp
index 1eb76b10b..a750946e3 100644
--- a/src/storage/expressions/ExpressionEvaluatorBase.cpp
+++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp
@@ -1,15 +1,23 @@
#include "src/storage/expressions/ExpressionEvaluatorBase.h"
#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/parameters.h"
namespace storm {
namespace expressions {
- ExpressionEvaluatorBase::ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()) {
+ template<typename RationalType>
+ ExpressionEvaluatorBase<RationalType>::ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()) {
// Intentionally left empty.
}
- storm::expressions::ExpressionManager const& ExpressionEvaluatorBase::getManager() const {
+ template<typename RationalType>
+ storm::expressions::ExpressionManager const& ExpressionEvaluatorBase<RationalType>::getManager() const {
return *manager;
}
+
+ template class ExpressionEvaluatorBase<double>;
+#ifdef STORM_HAVE_CARL
+ template class ExpressionEvaluatorBase<RationalFunction>;
+#endif
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluatorBase.h b/src/storage/expressions/ExpressionEvaluatorBase.h
index 53a848611..b88c1aae7 100644
--- a/src/storage/expressions/ExpressionEvaluatorBase.h
+++ b/src/storage/expressions/ExpressionEvaluatorBase.h
@@ -5,13 +5,14 @@
namespace storm {
namespace expressions {
+ template<typename RationalReturnType>
class ExpressionEvaluatorBase {
public:
ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager);
virtual bool asBool(Expression const& expression) const = 0;
virtual int_fast64_t asInt(Expression const& expression) const = 0;
- virtual double asDouble(Expression const& expression) const = 0;
+ virtual RationalReturnType asRational(Expression const& expression) const = 0;
virtual void setBooleanValue(storm::expressions::Variable const& variable, bool value) = 0;
virtual void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) = 0;
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
index 58d6176d3..11799faa5 100644
--- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -1,11 +1,13 @@
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/parameters.h"
#include "src/utility/macros.h"
namespace storm {
namespace expressions {
- ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase(manager), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
+ template<typename RationalType>
+ ExprtkExpressionEvaluatorBase<RationalType>::ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase<RationalType>(manager), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
for (auto const& variableTypePair : manager) {
if (variableTypePair.second.isBooleanType()) {
@@ -19,7 +21,8 @@ namespace storm {
symbolTable.add_constants();
}
- bool ExprtkExpressionEvaluator::asBool(Expression const& expression) const {
+ template<typename RationalType>
+ bool ExprtkExpressionEvaluatorBase<RationalType>::asBool(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@@ -29,7 +32,8 @@ namespace storm {
return expressionPair->second.value() == ValueType(1);
}
- int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) const {
+ template<typename RationalType>
+ int_fast64_t ExprtkExpressionEvaluatorBase<RationalType>::asInt(Expression const& expression) const {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@@ -39,17 +43,8 @@ namespace storm {
return static_cast<int_fast64_t>(expressionPair->second.value());
}
- double ExprtkExpressionEvaluator::asDouble(Expression const& expression) const {
- BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
- auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
- if (expressionPair == this->compiledExpressions.end()) {
- CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expressionPtr);
- return static_cast<double>(compiledExpression.value());
- }
- return static_cast<double>(expressionPair->second.value());
- }
-
- ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) const {
+ template<typename RationalType>
+ typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(BaseExpression const* expression) const {
std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression, CompiledExpressionType());
CompiledExpressionType& compiledExpression = result.first->second;
compiledExpression.register_symbol_table(symbolTable);
@@ -58,16 +53,38 @@ namespace storm {
return compiledExpression;
}
- void ExprtkExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
+ template<typename RationalType>
+ void ExprtkExpressionEvaluatorBase<RationalType>::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
this->booleanValues[variable.getOffset()] = static_cast<ValueType>(value);
}
- void ExprtkExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
+ template<typename RationalType>
+ void ExprtkExpressionEvaluatorBase<RationalType>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
this->integerValues[variable.getOffset()] = static_cast<ValueType>(value);
}
- void ExprtkExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) {
+ template<typename RationalType>
+ void ExprtkExpressionEvaluatorBase<RationalType>::setRationalValue(storm::expressions::Variable const& variable, double value) {
this->rationalValues[variable.getOffset()] = static_cast<ValueType>(value);
}
+
+ ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<double>(manager) {
+ // Intentionally left empty.
+ }
+
+ double ExprtkExpressionEvaluator::asRational(Expression const& expression) const {
+ BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
+ auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
+ if (expressionPair == this->compiledExpressions.end()) {
+ CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expressionPtr);
+ return static_cast<double>(compiledExpression.value());
+ }
+ return static_cast<double>(expressionPair->second.value());
+ }
+
+ template class ExprtkExpressionEvaluatorBase<double>;
+#ifdef STORM_HAVE_CARL
+ template class ExprtkExpressionEvaluatorBase<RationalFunction>;
+#endif
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h
index c84276ef2..9377f3522 100644
--- a/src/storage/expressions/ExprtkExpressionEvaluator.h
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.h
@@ -11,24 +11,19 @@
namespace storm {
namespace expressions {
- class ExprtkExpressionEvaluator : public ExpressionEvaluatorBase {
+ template <typename RationalType>
+ class ExprtkExpressionEvaluatorBase : public ExpressionEvaluatorBase<RationalType> {
public:
- /*!
- * Creates an expression evaluator that is capable of evaluating expressions managed by the given manager.
- *
- * @param manager The manager responsible for the expressions.
- */
- ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
+ ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager);
- bool asBool(Expression const& expression) const;
- int_fast64_t asInt(Expression const& expression) const;
- double asDouble(Expression const& expression) const;
-
- void setBooleanValue(storm::expressions::Variable const& variable, bool value);
- void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value);
- void setRationalValue(storm::expressions::Variable const& variable, double value);
+ bool asBool(Expression const& expression) const override;
+ int_fast64_t asInt(Expression const& expression) const override;
- private:
+ void setBooleanValue(storm::expressions::Variable const& variable, bool value) override;
+ void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override;
+ void setRationalValue(storm::expressions::Variable const& variable, double value) override;
+
+ protected:
typedef double ValueType;
typedef exprtk::expression<ValueType> CompiledExpressionType;
typedef std::unordered_map<BaseExpression const*, CompiledExpressionType> CacheType;
@@ -39,7 +34,7 @@ namespace storm {
* @param expression The expression that is to be compiled.
*/
CompiledExpressionType& getCompiledExpression(BaseExpression const* expression) const;
-
+
// The parser used.
mutable exprtk::parser<ValueType> parser;
@@ -54,6 +49,18 @@ namespace storm {
// A mapping of expressions to their compiled counterpart.
mutable CacheType compiledExpressions;
};
+
+ class ExprtkExpressionEvaluator : public ExprtkExpressionEvaluatorBase<double> {
+ public:
+ /*!
+ * Creates an expression evaluator that is capable of evaluating expressions managed by the given manager.
+ *
+ * @param manager The manager responsible for the expressions.
+ */
+ ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
+
+ double asRational(Expression const& expression) const override;
+ };
}
}
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
new file mode 100644
index 000000000..4e6516095
--- /dev/null
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -0,0 +1,102 @@
+#include "src/storage/expressions/ToRationalFunctionVisitor.h"
+
+#include <sstream>
+
+#include "src/utility/macros.h"
+
+#ifdef STORM_HAVE_CARL
+
+namespace storm {
+ namespace expressions {
+ template<typename RationalFunctionType>
+ ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
+ // Intentionally left empty.
+ }
+
+ template<typename RationalFunctionType>
+ RationalFunctionType ToRationalFunctionVisitor<RationalFunctionType>::toRationalFunction(Expression const& expression) {
+ return boost::any_cast<RationalFunctionType>(expression.accept(*this));
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryBooleanFunctionExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryNumericalFunctionExpression const& expression) {
+ RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this));
+ RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this));
+ switch(expression.getOperatorType()) {
+ case BinaryNumericalFunctionExpression::OperatorType::Plus:
+ return firstOperandAsRationalFunction + secondOperandAsRationalFunction;
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Minus:
+ return firstOperandAsRationalFunction - secondOperandAsRationalFunction;
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Times:
+ return firstOperandAsRationalFunction * secondOperandAsRationalFunction;
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Divide:
+ return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
+ break;
+ default:
+ STORM_LOG_ASSERT(false, "Illegal operator type.");
+ }
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryRelationExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(VariableExpression const& expression) {
+ auto variablePair = variableToVariableMap.find(expression.getVariable());
+ if (variablePair != variableToVariableMap.end()) {
+ return convertVariableToPolynomial(variablePair->second);
+ } else {
+ carl::Variable carlVariable = carl::VariablePool::getInstance().getFreshVariable(expression.getVariableName());
+ variableToVariableMap.emplace(expression.getVariable(), carlVariable);
+ return convertVariableToPolynomial(carlVariable);
+ }
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryBooleanFunctionExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(UnaryNumericalFunctionExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BooleanLiteralExpression const& expression) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression) {
+ return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::CoeffType(expression.getValue())));
+ }
+
+ template<typename RationalFunctionType>
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
+ std::stringstream str;
+ str << std::fixed << std::setprecision(3) << expression.getValue();
+ return RationalFunctionType(carl::rationalize<cln::cl_RA>(str.str()));
+ }
+
+ template class ToRationalFunctionVisitor<storm::RationalFunction>;
+
+ }
+}
+
+#endif
\ No newline at end of file
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h
new file mode 100644
index 000000000..51cc96761
--- /dev/null
+++ b/src/storage/expressions/ToRationalFunctionVisitor.h
@@ -0,0 +1,53 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
+
+#include "src/storage/parameters.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Expressions.h"
+#include "src/storage/expressions/ExpressionVisitor.h"
+#include "src/storage/expressions/Variable.h"
+
+#ifdef STORM_HAVE_CARL
+namespace storm {
+ namespace expressions {
+
+ template<typename RationalFunctionType>
+ class ToRationalFunctionVisitor : public ExpressionVisitor {
+ public:
+ ToRationalFunctionVisitor();
+
+ RationalFunctionType toRationalFunction(Expression const& expression);
+
+ virtual boost::any visit(IfThenElseExpression const& expression) override;
+ virtual boost::any visit(BinaryBooleanFunctionExpression const& expression) override;
+ virtual boost::any visit(BinaryNumericalFunctionExpression const& expression) override;
+ virtual boost::any visit(BinaryRelationExpression const& expression) override;
+ virtual boost::any visit(VariableExpression const& expression) override;
+ virtual boost::any visit(UnaryBooleanFunctionExpression const& expression) override;
+ virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
+ virtual boost::any visit(BooleanLiteralExpression const& expression) override;
+ virtual boost::any visit(IntegerLiteralExpression const& expression) override;
+ virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+
+ private:
+ template<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
+ RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+ return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
+ }
+
+ template<typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
+ RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) {
+ return RationalFunctionType(variable);
+ }
+
+ // A mapping from our variables to carl's.
+ std::unordered_map<storm::expressions::Variable, carl::Variable> variableToVariableMap;
+
+ // The cache that is used in case the underlying type needs a cache.
+ std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
+ };
+ }
+}
+#endif
+
+#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */
\ No newline at end of file
diff --git a/src/storage/parameters.h b/src/storage/parameters.h
index c9eb066f7..7455690d2 100644
--- a/src/storage/parameters.h
+++ b/src/storage/parameters.h
@@ -2,13 +2,11 @@
#define STORM_STORAGE_PARAMETERS_H_
#include "storm-config.h"
-#ifdef STORM_HAVE_CARL
+#ifdef STORM_HAVE_CARL
#include "../adapters/extendedCarl.h"
-namespace storm
-{
-// typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
+namespace storm {
typedef carl::Variable Variable;
typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index 20a32cda1..3517b95c6 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -143,7 +143,7 @@ int main(const int argc, const char** argv) {
std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename();
std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
- std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, true, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants);
+ std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program, true, false, storm::settings::generalSettings().isSymbolicRewardModelNameSet() ? storm::settings::generalSettings().getSymbolicRewardModelName() : "", constants);
model->printModelInformationToStream(std::cout);