diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 5312e05cc..d00cfcc52 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -342,7 +342,7 @@ namespace storm { storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const { auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName); - STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'."); + STORM_LOG_THROW(actionName.empty() || nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'."); return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); } diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 4dba68d8e..0b4ab22ac 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -7,7 +7,7 @@ namespace storm { namespace storage { template - const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863}; + const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191}; template BitVectorHashMap::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 0372925a2..d5db82905 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -1,5 +1,6 @@ #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" #include "src/storage/expressions/BooleanLiteralExpression.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" @@ -45,7 +46,7 @@ namespace storm { std::shared_ptr firstOperandSimplified = this->getFirstOperand()->simplify(); std::shared_ptr secondOperandSimplified = this->getSecondOperand()->simplify(); - if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) { + if (firstOperandSimplified->isLiteral() || secondOperandSimplified->isLiteral()) { switch (this->getOperatorType()) { case OperatorType::And: if (firstOperandSimplified->isTrue()) { @@ -69,7 +70,21 @@ namespace storm { return firstOperandSimplified; } break; - case OperatorType::Xor: break; + case OperatorType::Xor: + if (firstOperandSimplified->isTrue()) { + if (secondOperandSimplified->isFalse()) { + return firstOperandSimplified; + } else if (secondOperandSimplified->isTrue()) { + return this->getManager().boolean(false).getBaseExpressionPointer(); + } + } else if (firstOperandSimplified->isFalse()) { + if (secondOperandSimplified->isTrue()) { + return secondOperandSimplified; + } else if (secondOperandSimplified->isFalse()) { + return this->getManager().boolean(false).getBaseExpressionPointer(); + } + } + break; case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { return secondOperandSimplified; @@ -84,6 +99,10 @@ namespace storm { return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) { return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), true)); + } else if (firstOperandSimplified->isTrue() && secondOperandSimplified->isFalse()) { + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), false)); + } else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isTrue()) { + return std::shared_ptr(new BooleanLiteralExpression(this->getManager(), false)); } break; } diff --git a/src/storage/expressions/ExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp similarity index 74% rename from src/storage/expressions/ExpressionEvaluator.cpp rename to src/storage/expressions/ExprtkExpressionEvaluator.cpp index e54beaaca..7c11c4fc5 100644 --- a/src/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -1,9 +1,9 @@ -#include "src/storage/expressions/ExpressionEvaluator.h" +#include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace expressions { - ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) { + ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) { for (auto const& variableTypePair : manager) { if (variableTypePair.second.isBooleanType()) { @@ -17,7 +17,7 @@ namespace storm { symbolTable.add_constants(); } - bool ExpressionEvaluator::asBool(Expression const& expression) { + bool ExprtkExpressionEvaluator::asBool(Expression const& expression) { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -27,7 +27,7 @@ namespace storm { return expressionPair->second.value() == ValueType(1); } - int_fast64_t ExpressionEvaluator::asInt(Expression const& expression) { + int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -37,7 +37,7 @@ namespace storm { return static_cast(expressionPair->second.value()); } - double ExpressionEvaluator::asDouble(Expression const& expression) { + double ExprtkExpressionEvaluator::asDouble(Expression const& expression) { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -47,7 +47,7 @@ namespace storm { return static_cast(expressionPair->second.value()); } - ExpressionEvaluator::CompiledExpressionType& ExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) { + ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) { std::pair result = this->compiledExpressions.emplace(expression, CompiledExpressionType()); CompiledExpressionType& compiledExpression = result.first->second; compiledExpression.register_symbol_table(symbolTable); @@ -55,15 +55,15 @@ namespace storm { return compiledExpression; } - void ExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) { + void ExprtkExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) { this->booleanValues[variable.getOffset()] = static_cast(value); } - void ExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { + void ExprtkExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { this->integerValues[variable.getOffset()] = static_cast(value); } - void ExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) { + void ExprtkExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) { this->rationalValues[variable.getOffset()] = static_cast(value); } } diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h similarity index 92% rename from src/storage/expressions/ExpressionEvaluator.h rename to src/storage/expressions/ExprtkExpressionEvaluator.h index 1d5322774..8aa771130 100644 --- a/src/storage/expressions/ExpressionEvaluator.h +++ b/src/storage/expressions/ExprtkExpressionEvaluator.h @@ -12,14 +12,14 @@ namespace storm { namespace expressions { - class ExpressionEvaluator { + class ExprtkExpressionEvaluator { public: /*! * Creates an expression evaluator that is capable of evaluating expressions managed by the given manager. * * @param manager The manager responsible for the expressions. */ - ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); + ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager); bool asBool(Expression const& expression); int_fast64_t asInt(Expression const& expression); diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index c4850c42d..ec7baaa48 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -8,6 +8,7 @@ TEST(PrismParser, StandardModelTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm")); + result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm")); @@ -84,12 +85,12 @@ TEST(PrismParser, ComplexTest) { endinit rewards "testrewards" - [stateRew] true : a + 7; + [a] true : a + 7; max(f, a) <= 8 : 2*b; endrewards rewards "testrewards2" - [stateRew] true : a + 7; + [b] true : a + 7; max(f, a) <= 8 : 2*b; endrewards)"; diff --git a/test/functional/storage/ExpressionEvalutionTest.cpp b/test/functional/storage/ExpressionEvalutionTest.cpp index c622f6e73..b9ff1cbc3 100644 --- a/test/functional/storage/ExpressionEvalutionTest.cpp +++ b/test/functional/storage/ExpressionEvalutionTest.cpp @@ -2,7 +2,7 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/SimpleValuation.h" -#include "src/storage/expressions/ExpressionEvaluator.h" +#include "src/storage/expressions/ExprtkExpressionEvaluator.h" TEST(ExpressionEvaluation, NaiveEvaluation) { std::shared_ptr manager(new storm::expressions::ExpressionManager()); @@ -44,7 +44,7 @@ TEST(ExpressionEvaluation, ExprTkEvaluation) { ASSERT_NO_THROW(z = manager->declareRationalVariable("z")); storm::expressions::Expression iteExpression = storm::expressions::ite(x, y + z, manager->integer(3) * z); - storm::expressions::ExpressionEvaluator eval(*manager); + storm::expressions::ExprtkExpressionEvaluator eval(*manager); eval.setRationalValue(z, 5.5); eval.setBooleanValue(x, true); diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 358015988..787a5a6d5 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -275,7 +275,7 @@ TEST(Expression, SubstitutionTest) { storm::expressions::Expression tempExpression; ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression); - std::map substution = { std::make_pair(manager->getVariable("y"), rationalVarExpression), std::make_pair(manager->getVariable("x"), manager->boolean(true)) }; + std::map substution = { std::make_pair(manager->getVariable("y"), manager->rational(2.7)), std::make_pair(manager->getVariable("x"), manager->boolean(true)) }; storm::expressions::Expression substitutedExpression; ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution)); EXPECT_TRUE(substitutedExpression.simplify().isTrue());