From ff5902a17c15465ed63dff3fdb1b0104e6d6833c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Oct 2014 17:03:02 +0200 Subject: [PATCH] Some fixes. Former-commit-id: 7b2b46d34750b6e08d98ffac46c4b646f35900cd --- src/adapters/ExplicitModelAdapter.h | 6 +- .../expressions/ExpressionEvaluation.h | 210 +++++++++--------- 2 files changed, 111 insertions(+), 105 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 9699f1745..e6eab4322 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -351,6 +351,7 @@ namespace storm { // behaviour for this is undefined anyway, a warning should be issued in that case. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::prism::Command const& command = *iteratorList[i]; + std::cout << command << std::endl; for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { storm::prism::Update const& update = command.getUpdate(j); @@ -366,6 +367,7 @@ namespace storm { boost::container::flat_set newLabelSet = valueLabelSetPair.second; newLabelSet.insert(update.getGlobalIndex()); + std::cout << "got new value " << valueLabelSetPair.first << " * " << updateProbability << " = " << valueLabelSetPair.first * updateProbability << std::endl; newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet); } @@ -407,6 +409,7 @@ namespace storm { } ValueType probabilitySum = utility::constantZero(); + std::cout << "resetting prob sum" << std::endl; for (auto const& stateProbabilityPair : *newTargetStates) { std::pair flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation); @@ -418,12 +421,13 @@ namespace storm { for (auto const& probabilityLabelPair : stateProbabilityPair.second) { addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second); probabilitySum += probabilityLabelPair.first; + std::cout << "increasing prob sum by " << probabilityLabelPair.first << std::endl; } } // Check that the resulting distribution is in fact a distribution. if (!storm::utility::isOne(probabilitySum)) { - LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command."); + LOG4CPLUS_ERROR(logger, "Sum of update probabilities (" << probabilitySum << ") is not one for some command."); throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do sum to " << probabilitySum << " to one for some command."; } diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 95a076088..156e8b0d3 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -1,4 +1,4 @@ -/** +/** * @file: ExpressionEvaluation.h * @author: Sebastian Junges * @@ -20,73 +20,74 @@ #include "src/storage/parameters.h" namespace storm { -namespace expressions { - - template - struct StateType - { - typedef int type; - }; - + namespace expressions { + + template + struct StateType + { + typedef int type; + }; + #ifdef PARAMETRIC_SYSTEMS - template<> - struct StateType - { - typedef std::map type; - }; - - template<> - struct StateType - { - typedef std::map type; - }; - - struct ExpressionEvaluationSettings { - static const bool useFactorizedPolynomials = false; - }; - - struct FactorizedPolynomialsEvaluationSettings : ExpressionEvaluationSettings { - static const bool useFactorizedPolynomials = true; - }; + template<> + struct StateType + { + typedef std::map type; + }; + + template<> + struct StateType + { + typedef std::map type; + }; #endif - template - class ExpressionEvaluationVisitor : public ExpressionVisitor - { + template + class ExpressionEvaluationVisitor : public ExpressionVisitor + { public: ExpressionEvaluationVisitor(S* sharedState) : mSharedState(sharedState), cache(new carl::Cache>()) { - + } - - virtual ~ExpressionEvaluationVisitor() { + + ExpressionEvaluationVisitor(S* sharedState, std::shared_ptr>> cache) + : mSharedState(sharedState), cache(cache) + { + } + + + virtual ~ExpressionEvaluationVisitor() { + } - virtual void visit(IfThenElseExpression const* expression) + virtual void visit(IfThenElseExpression const* expression) { std::cout << "ite" << std::endl; } - - virtual void visit(BinaryBooleanFunctionExpression const* expression) + + virtual void visit(BinaryBooleanFunctionExpression const* expression) { std::cout << "bbf" << std::endl; } - virtual void visit(BinaryNumericalFunctionExpression const* expression) + virtual void visit(BinaryNumericalFunctionExpression const* expression) { - ExpressionEvaluationVisitor* visitor = new ExpressionEvaluationVisitor(mSharedState); + ExpressionEvaluationVisitor* visitor = new ExpressionEvaluationVisitor(mSharedState, this->cache); expression->getFirstOperand()->accept(visitor); mValue = visitor->value(); - expression->getSecondOperand()->accept(visitor); + expression->getSecondOperand()->accept(visitor); switch(expression->getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: mValue += visitor->value(); break; case BinaryNumericalFunctionExpression::OperatorType::Minus: + std::cout << "mValue: " << mValue << " - " << visitor->value() << std::endl; mValue -= visitor->value(); + std::cout << mValue << std::endl; break; case BinaryNumericalFunctionExpression::OperatorType::Times: mValue *= visitor->value(); @@ -101,13 +102,13 @@ namespace expressions { delete visitor; } - virtual void visit(BinaryRelationExpression const* expression) + virtual void visit(BinaryRelationExpression const* expression) { std::cout << "br" << std::endl; } - virtual void visit(VariableExpression const* expression) + virtual void visit(VariableExpression const* expression) { - std::string const& varName= expression->getVariableName(); + std::string const& varName= expression->getVariableName(); auto it = mSharedState->find(varName); if(it != mSharedState->end()) { @@ -120,89 +121,90 @@ namespace expressions { mValue = convertVariableToPolynomial(nVar); } } - virtual void visit(UnaryBooleanFunctionExpression const* expression) + virtual void visit(UnaryBooleanFunctionExpression const* expression) { std::cout << "ubf" << std::endl; } - virtual void visit(UnaryNumericalFunctionExpression const* expression) + virtual void visit(UnaryNumericalFunctionExpression const* expression) { std::cout << "unf" << std::endl; } - virtual void visit(BooleanLiteralExpression const* expression) + virtual void visit(BooleanLiteralExpression const* expression) { std::cout << "bl" << std::endl; } - virtual void visit(IntegerLiteralExpression const* expression) + virtual void visit(IntegerLiteralExpression const* expression) { mValue = T(typename T::PolyType(typename T::CoeffType(expression->getValue()))); } - virtual void visit(DoubleLiteralExpression const* expression) + virtual void visit(DoubleLiteralExpression const* expression) { std::stringstream str; str << std::fixed << std::setprecision( 3 ) << expression->getValue(); mValue = T(carl::rationalize(str.str())); } - - template> = carl::dummy> - T convertVariableToPolynomial(carl::Variable const& nVar) { - return T(typename T::PolyType(typename T::PolyType::PolyType(nVar), cache)); - } - - template> = carl::dummy> - T convertVariableToPolynomial(carl::Variable const& nVar) { - return T(nVar); - } - - const T& value() const - { - return mValue; - } - + + template> = carl::dummy> + T convertVariableToPolynomial(carl::Variable const& nVar) { + return T(typename T::PolyType(typename T::PolyType::PolyType(nVar), cache)); + } + + template> = carl::dummy> + T convertVariableToPolynomial(carl::Variable const& nVar) { + return T(nVar); + } + + const T& value() const + { + return mValue; + } + private: - S* mSharedState; - T mValue; - carl::Cache>* cache; - }; - - template - class ExpressionEvaluation - { + S* mSharedState; + T mValue; + std::shared_ptr>> cache; + }; + + template + class ExpressionEvaluation + { public: - ExpressionEvaluation() : mState() - { - - } - - - T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) - { - ExpressionEvaluationVisitor::type>* visitor = new ExpressionEvaluationVisitor::type>(&mState); - Expression expressionToTranslate = expr.substitute(*val); - expressionToTranslate.getBaseExpression().accept(visitor); - T result = visitor->value(); -// result.simplify(); - delete visitor; - return result; - } - + ExpressionEvaluation() : mState(), cache(new carl::Cache>()) + { + // Intentionally left empty. + } + + + T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) + { + ExpressionEvaluationVisitor::type>* visitor = new ExpressionEvaluationVisitor::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::type mState; - }; - - /** - * For doubles, we keep using the getValueAs from the expressions, as this should be more efficient. - */ - template<> - class ExpressionEvaluation - { + std::shared_ptr>> cache; + }; + + /** + * For doubles, we keep using the getValueAs from the expressions, as this should be more efficient. + */ + template<> + class ExpressionEvaluation + { public: - double evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) const - { - return expr.evaluateAsDouble(val); - } - }; - -} + double evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) const + { + return expr.evaluateAsDouble(val); + } + }; + + } } #endif \ No newline at end of file