|
@ -7,7 +7,7 @@ |
|
|
#include "storm/storage/expressions/LinearityCheckVisitor.h"
|
|
|
#include "storm/storage/expressions/LinearityCheckVisitor.h"
|
|
|
#include "storm/storage/expressions/SimpleValuation.h"
|
|
|
#include "storm/storage/expressions/SimpleValuation.h"
|
|
|
#include "storm/storage/expressions/ExpressionEvaluator.h"
|
|
|
#include "storm/storage/expressions/ExpressionEvaluator.h"
|
|
|
#include "storm/storage/expressions/ValueTypeToExpression.h"
|
|
|
|
|
|
|
|
|
#include "storm/storage/expressions/RationalFunctionToExpression.h"
|
|
|
#include "storm/exceptions/InvalidTypeException.h"
|
|
|
#include "storm/exceptions/InvalidTypeException.h"
|
|
|
#include "storm/adapters/RationalFunctionAdapter.h"
|
|
|
#include "storm/adapters/RationalFunctionAdapter.h"
|
|
|
#include "storm-parsers/parser/ValueParser.h"
|
|
|
#include "storm-parsers/parser/ValueParser.h"
|
|
@ -299,27 +299,27 @@ TEST(Expression, SimplificationTest) { |
|
|
storm::expressions::Expression falseExpression; |
|
|
storm::expressions::Expression falseExpression; |
|
|
storm::expressions::Expression threeExpression; |
|
|
storm::expressions::Expression threeExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(trueExpression = manager->boolean(true)); |
|
|
|
|
|
ASSERT_NO_THROW(falseExpression = manager->boolean(false)); |
|
|
|
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
|
|
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression tempExpression; |
|
|
|
|
|
storm::expressions::Expression simplifiedExpression; |
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression); |
|
|
|
|
|
ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); |
|
|
|
|
|
EXPECT_TRUE(simplifiedExpression.isTrue()); |
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(trueExpression = manager->boolean(true)); |
|
|
|
|
|
ASSERT_NO_THROW(falseExpression = manager->boolean(false)); |
|
|
|
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
|
|
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression tempExpression; |
|
|
|
|
|
storm::expressions::Expression simplifiedExpression; |
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression); |
|
|
|
|
|
ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); |
|
|
|
|
|
EXPECT_TRUE(simplifiedExpression.isFalse()); |
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = trueExpression || intVarExpression > threeExpression); |
|
|
|
|
|
ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); |
|
|
|
|
|
EXPECT_TRUE(simplifiedExpression.isTrue()); |
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = falseExpression && intVarExpression > threeExpression); |
|
|
|
|
|
ASSERT_NO_THROW(simplifiedExpression = tempExpression.simplify()); |
|
|
|
|
|
EXPECT_TRUE(simplifiedExpression.isFalse()); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(Expression, SimpleEvaluationTest) { |
|
|
TEST(Expression, SimpleEvaluationTest) { |
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression trueExpression; |
|
|
storm::expressions::Expression trueExpression; |
|
|
storm::expressions::Expression falseExpression; |
|
|
storm::expressions::Expression falseExpression; |
|
|
storm::expressions::Expression threeExpression; |
|
|
storm::expressions::Expression threeExpression; |
|
@ -327,7 +327,7 @@ TEST(Expression, SimpleEvaluationTest) { |
|
|
storm::expressions::Expression boolVarExpression; |
|
|
storm::expressions::Expression boolVarExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
storm::expressions::Expression rationalVarExpression; |
|
|
storm::expressions::Expression rationalVarExpression; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(trueExpression = manager->boolean(true)); |
|
|
ASSERT_NO_THROW(trueExpression = manager->boolean(true)); |
|
|
ASSERT_NO_THROW(falseExpression = manager->boolean(false)); |
|
|
ASSERT_NO_THROW(falseExpression = manager->boolean(false)); |
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
@ -335,23 +335,23 @@ TEST(Expression, SimpleEvaluationTest) { |
|
|
ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); |
|
|
ASSERT_NO_THROW(boolVarExpression = manager->declareBooleanVariable("x")); |
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); |
|
|
ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression tempExpression; |
|
|
storm::expressions::Expression tempExpression; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); |
|
|
ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager)); |
|
|
ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(manager)); |
|
|
storm::expressions::SimpleValuation valuation(manager); |
|
|
storm::expressions::SimpleValuation valuation(manager); |
|
|
ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false)); |
|
|
ASSERT_NO_THROW(valuation.setBooleanValue(manager->getVariable("x"), false)); |
|
|
ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0)); |
|
|
ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 0)); |
|
|
ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0)); |
|
|
ASSERT_NO_THROW(valuation.setRationalValue(manager->getVariable("z"), 0)); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); |
|
|
EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); |
|
|
EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); |
|
|
ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3)); |
|
|
ASSERT_NO_THROW(valuation.setIntegerValue(manager->getVariable("y"), 3)); |
|
|
EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); |
|
|
EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression)); |
|
|
ASSERT_NO_THROW(tempExpression = storm::expressions::ite(intVarExpression < threeExpression, trueExpression, falseExpression)); |
|
|
ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); |
|
|
ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); |
|
@ -360,30 +360,30 @@ TEST(Expression, SimpleEvaluationTest) { |
|
|
|
|
|
|
|
|
TEST(Expression, VisitorTest) { |
|
|
TEST(Expression, VisitorTest) { |
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression threeExpression; |
|
|
storm::expressions::Expression threeExpression; |
|
|
storm::expressions::Expression piExpression; |
|
|
storm::expressions::Expression piExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
storm::expressions::Expression intVarExpression; |
|
|
storm::expressions::Expression rationalVarExpression; |
|
|
storm::expressions::Expression rationalVarExpression; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
|
ASSERT_NO_THROW(threeExpression = manager->integer(3)); |
|
|
ASSERT_NO_THROW(piExpression = manager->rational(3.14)); |
|
|
ASSERT_NO_THROW(piExpression = manager->rational(3.14)); |
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
ASSERT_NO_THROW(intVarExpression = manager->declareIntegerVariable("y")); |
|
|
ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); |
|
|
ASSERT_NO_THROW(rationalVarExpression = manager->declareRationalVariable("z")); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression; |
|
|
storm::expressions::Expression tempExpression = intVarExpression + rationalVarExpression * threeExpression; |
|
|
storm::expressions::LinearityCheckVisitor visitor; |
|
|
storm::expressions::LinearityCheckVisitor visitor; |
|
|
EXPECT_TRUE(visitor.check(tempExpression)); |
|
|
EXPECT_TRUE(visitor.check(tempExpression)); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(Expression, ValueTypeToExpressionTest) { |
|
|
|
|
|
|
|
|
TEST(Expression, RationalFunctionToExpressionTest) { |
|
|
storm::parser::ValueParser<storm::RationalFunction> parser; |
|
|
storm::parser::ValueParser<storm::RationalFunction> parser; |
|
|
parser.addParameter("p"); |
|
|
parser.addParameter("p"); |
|
|
parser.addParameter("q"); |
|
|
parser.addParameter("q"); |
|
|
auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2"); |
|
|
auto rationalFunction = parser.parseValue("((5*p^(3))+(q*p*7)+2)/2"); |
|
|
|
|
|
|
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager()); |
|
|
auto transformer = storm::expressions::ValueTypeToExpression<storm::RationalFunction>(manager); |
|
|
|
|
|
|
|
|
auto transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager); |
|
|
|
|
|
|
|
|
storm::expressions::Expression expr; |
|
|
storm::expressions::Expression expr; |
|
|
EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); |
|
|
EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); |
|
@ -396,10 +396,10 @@ TEST(Expression, ValueTypeToExpressionTest) { |
|
|
EXPECT_EQ(rationalFunction.toString(), result.toString()); |
|
|
EXPECT_EQ(rationalFunction.toString(), result.toString()); |
|
|
|
|
|
|
|
|
rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2"); |
|
|
rationalFunction = parser.parseValue("(5*((p^(3))+(q*p)))/2"); |
|
|
transformer = storm::expressions::ValueTypeToExpression<storm::RationalFunction>(manager); |
|
|
|
|
|
|
|
|
transformer = storm::expressions::RationalFunctionToExpression<storm::RationalFunction>(manager); |
|
|
EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); |
|
|
EXPECT_NO_THROW(expr = transformer.toExpression(rationalFunction)); |
|
|
ASSERT_NO_THROW(rationalFunction.simplify()); |
|
|
ASSERT_NO_THROW(rationalFunction.simplify()); |
|
|
ASSERT_NO_THROW(result = visitor.toRationalFunction(expr)); |
|
|
ASSERT_NO_THROW(result = visitor.toRationalFunction(expr)); |
|
|
ASSERT_NO_THROW(result.simplify()); |
|
|
ASSERT_NO_THROW(result.simplify()); |
|
|
EXPECT_EQ(rationalFunction.toString(), result.toString()); |
|
|
EXPECT_EQ(rationalFunction.toString(), result.toString()); |
|
|
} |
|
|
|
|
|
|
|
|
} |