From b297cdf38fe47acd6e066ac59fb80fecc87270c4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 14 Dec 2015 15:58:37 +0100 Subject: [PATCH] added some syntatic sugar to PRISM parser in order to enhance performance tests of symbolic model checker Former-commit-id: d85ce2653628398c47bae0c574746220a23301fa --- src/parser/ExpressionParser.cpp | 31 ++-- src/parser/ExpressionParser.h | 23 ++- src/parser/FormulaParser.cpp | 7 + src/parser/FormulaParser.h | 3 + src/storage/prism/Program.cpp | 148 ++++++++++++--- src/utility/storm.cpp | 2 +- test/performance/builder/csma3_4.nm | 134 ++++++++++++++ test/performance/builder/leader5.nm | 98 ++++++++++ .../SymbolicMdpPrctlModelCheckerTest.cpp | 174 ++++++++++++++++++ 9 files changed, 576 insertions(+), 44 deletions(-) create mode 100644 test/performance/builder/csma3_4.nm create mode 100644 test/performance/builder/leader5.nm create mode 100644 test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index c67f808e0..8bb55c625 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,47 +5,54 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); if (allowBacktracking) { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; } else { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > iteExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; } floorCeilExpression.name("floor/ceil expression"); if (allowBacktracking) { - minMaxExpression = ((minMaxOperator_ >> qi::lit("(")) >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> iteExpression[qi::_val = qi::_1] >> +(qi::lit(",") >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]); } else { - minMaxExpression = ((minMaxOperator_ >> qi::lit("(")) > plusExpression > qi::lit(",") > plusExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] > qi::lit("(")) > iteExpression[qi::_val = qi::_1] > +(qi::lit(",") > iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]); } minMaxExpression.name("min/max expression"); + if (allowBacktracking) { + prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> iteExpression >> qi::lit(",") >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + } else { + prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > iteExpression > qi::lit(",") > iteExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + } + prefixPowerExpression.name("pow expression"); + identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)]; identifierExpression.name("identifier expression"); literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)]; literalExpression.name("literal expression"); - atomicExpression = floorCeilExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression; + atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression; atomicExpression.name("atomic expression"); unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createUnaryExpression, phoenix::ref(*this), qi::_1, qi::_2)]; unaryExpression.name("unary expression"); if (allowBacktracking) { - powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; } else { - powerExpression = unaryExpression[qi::_val = qi::_1] > -(powerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; } - powerExpression.name("power expression"); + infixPowerExpression.name("power expression"); if (allowBacktracking) { - multiplicationExpression = powerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; } else { - multiplicationExpression = powerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > powerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; } multiplicationExpression.name("multiplication expression"); @@ -92,7 +99,7 @@ namespace storm { debug(relativeExpression); debug(plusExpression); debug(multiplicationExpression); - debug(powerExpression); + debug(infixPowerExpression); debug(unaryExpression); debug(atomicExpression); debug(literalExpression); diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 19c129b4a..4277819b2 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -120,15 +120,15 @@ namespace storm { // A parser used for recognizing the operators at the "multiplication" precedence level. multiplicationOperatorStruct multiplicationOperator_; - struct powerOperatorStruct : qi::symbols { - powerOperatorStruct() { + struct infixPowerOperatorStruct : qi::symbols { + infixPowerOperatorStruct() { add ("^", storm::expressions::OperatorType::Power); } }; // A parser used for recognizing the operators at the "power" precedence level. - powerOperatorStruct powerOperator_; + infixPowerOperatorStruct infixPowerOperator_; struct unaryOperatorStruct : qi::symbols { unaryOperatorStruct() { @@ -162,7 +162,17 @@ namespace storm { // A parser used for recognizing the operators at the "min/max" precedence level. minMaxOperatorStruct minMaxOperator_; + + struct prefixPowerOperatorStruct : qi::symbols { + prefixPowerOperatorStruct() { + add + ("pow", storm::expressions::OperatorType::Power); + } + }; + // A parser used for recognizing the operators at the "power" precedence level. + prefixPowerOperatorStruct prefixPowerOperator_; + struct trueFalseOperatorStruct : qi::symbols { trueFalseOperatorStruct(storm::expressions::ExpressionManager const& manager) { add @@ -200,13 +210,14 @@ namespace storm { qi::rule, Skipper> equalityExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; - qi::rule, Skipper> powerExpression; + qi::rule, Skipper> prefixPowerExpression; + qi::rule, Skipper> infixPowerExpression; qi::rule unaryExpression; qi::rule atomicExpression; qi::rule literalExpression; qi::rule identifierExpression; - qi::rule, Skipper> minMaxExpression; - qi::rule, Skipper> floorCeilExpression; + qi::rule, Skipper> minMaxExpression; + qi::rule, Skipper> floorCeilExpression; qi::rule identifier; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 082474187..53fbe6522 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -173,6 +173,13 @@ namespace storm { // Intentionally left empty. } + FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { + // Make the formulas of the program available to the parser. + for (auto const& formula : program.getFormulas()) { + this->addIdentifierExpression(formula.getName(), formula.getExpression()); + } + } + FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) { other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); } diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 25dc6514f..68ee3c5ab 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -9,6 +9,8 @@ #include "src/storage/expressions/Expression.h" #include "src/utility/macros.h" +#include "src/storage/prism/Program.h" + namespace storm { namespace parser { @@ -18,6 +20,7 @@ namespace storm { class FormulaParser { public: FormulaParser(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + FormulaParser(storm::prism::Program const& program); FormulaParser(FormulaParser const& other); FormulaParser& operator=(FormulaParser const& other); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 6c60f08f3..3b4be36aa 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -2,6 +2,7 @@ #include #include +#include #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" @@ -548,8 +549,17 @@ namespace storm { // Check defining expressions of defined constants. if (constant.isDefined()) { std::set containedVariables = constant.getExpression().getVariables(); - bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers."); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } } // Record the new identifier for future checks. @@ -563,8 +573,17 @@ namespace storm { for (auto const& variable : this->getGlobalBooleanVariables()) { // Check the initial value of the variable. std::set containedVariables = variable.getInitialValueExpression().getVariables(); - bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Record the new identifier for future checks. variables.insert(variable.getExpressionVariable()); @@ -575,17 +594,40 @@ namespace storm { for (auto const& variable : this->getGlobalIntegerVariables()) { // Check that bound expressions of the range. std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } containedVariables = variable.getLowerBoundExpression().getVariables(); - isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Check the initial value of the variable. containedVariables = variable.getInitialValueExpression().getVariables(); - isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Record the new identifier for future checks. variables.insert(variable.getExpressionVariable()); @@ -599,8 +641,16 @@ namespace storm { for (auto const& variable : module.getBooleanVariables()) { // Check the initial value of the variable. std::set containedVariables = variable.getInitialValueExpression().getVariables(); - bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Record the new identifier for future checks. variables.insert(variable.getExpressionVariable()); @@ -609,17 +659,41 @@ namespace storm { for (auto const& variable : module.getIntegerVariables()) { // Check that bound expressions of the range. std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - bool isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants."); - + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } + containedVariables = variable.getLowerBoundExpression().getVariables(); - isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants."); + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Check the initial value of the variable. containedVariables = variable.getInitialValueExpression().getVariables(); - isValid = std::includes(constants.begin(), constants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Record the new identifier for future checks. variables.insert(variable.getExpressionVariable()); @@ -648,8 +722,16 @@ namespace storm { for (auto& command : module.getCommands()) { // Check the guard. std::set containedVariables = command.getGuardExpression().getVariables(); - bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression() << " refers to unknown identifiers."); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression() << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'."); // Record which types of commands were seen. @@ -668,8 +750,16 @@ namespace storm { // Check all updates. for (auto const& update : command.getUpdates()) { containedVariables = update.getLikelihoodExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers."); + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Check all assignments. std::set alreadyAssignedVariables; @@ -687,8 +777,16 @@ namespace storm { STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'."); containedVariables = assignment.getExpression().getVariables(); - isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assigned expression refers to unknown identifiers."); + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } // Add the current variable to the set of assigned variables (of this update). alreadyAssignedVariables.insert(assignedVariable); diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 5361010eb..a690af6f8 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -35,7 +35,7 @@ namespace storm { } std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) { - storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + storm::parser::FormulaParser formulaParser(program); return parseFormulas(formulaParser, inputString); } } \ No newline at end of file diff --git a/test/performance/builder/csma3_4.nm b/test/performance/builder/csma3_4.nm new file mode 100644 index 000000000..77e5070b2 --- /dev/null +++ b/test/performance/builder/csma3_4.nm @@ -0,0 +1,134 @@ +// CSMA/CD protocol - probabilistic version of kronos model (3 stations) +// gxn/dxp 04/12/01 + +mdp + +// note made changes since cannot have strict inequalities +// in digital clocks approach and suppose a station only sends one message + +// simplified parameters scaled +const int sigma=1; // time for messages to propagate along the bus +const int lambda=30; // time to send a message + +// actual parameters +const int N = 3; // number of processes +const int K = 4; // exponential backoff limit +const int slot = 2*sigma; // length of slot +const int M = floor(pow(2, K))-1 ; // max number of slots to wait +//const int lambda=782; +//const int sigma=26; + +//---------------------------------------------------------------------------------------------------------------------------- +// the bus +module bus + + b : [0..2]; + // b=0 - idle + // b=1 - active + // b=2 - collision + + // clocks of bus + y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) + y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) + + // a sender sends (ok - no other message being sent) + [send1] (b=0) -> (b'=1); + [send2] (b=0) -> (b'=1); + [send3] (b=0) -> (b'=1); + + // a sender sends (bus busy - collision) + [send1] (b=1|b=2) & (y1 (b'=2); + [send2] (b=1|b=2) & (y1 (b'=2); + [send3] (b=1|b=2) & (y1 (b'=2); + + // finish sending + [end1] (b=1) -> (b'=0) & (y1'=0); + [end2] (b=1) -> (b'=0) & (y1'=0); + [end3] (b=1) -> (b'=0) & (y1'=0); + + // bus busy + [busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); + [busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); + [busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); + + // collision detected + [cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); + + // time passage + [time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 + [time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 + [time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- +// model of first sender +module station1 + + // LOCAL STATE + s1 : [0..5]; + // s1=0 - initial state + // s1=1 - transmit + // s1=2 - collision (set backoff) + // s1=3 - wait (bus busy) + // s1=4 - successfully sent + + // LOCAL CLOCK + x1 : [0..max(lambda,slot)]; + + // BACKOFF COUNTER (number of slots to wait) + bc1 : [0..M]; + + // COLLISION COUNTER + cd1 : [0..K]; + + // start sending + [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending + [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff + + // transmitting + [time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass + [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished + [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) + [cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important + + // set backoff (no time can pass in this state) + // probability depends on which transmission this is (cd1) + [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; + [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; + [] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; + [] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; + + // wait until backoff counter reaches 0 then send again + [time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot) + [time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) + [send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) + [busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) + + // once finished nothing matters + [time] (s1>=4) -> (x1'=0); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule +module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward structure for expected time +rewards "time" + [time] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- + +// labels/formulae +label "all_delivered" = s1=4&s2=4&s3=4; +label "one_delivered" = s1=4|s2=4|s3=4; +label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3); diff --git a/test/performance/builder/leader5.nm b/test/performance/builder/leader5.nm new file mode 100644 index 000000000..bf434f2f7 --- /dev/null +++ b/test/performance/builder/leader5.nm @@ -0,0 +1,98 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const int N= 5; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..5-1]; + + // STATES + s1 : [0..4]; + // 0 make choice + // 1 have not received neighbours choice + // 2 active + // 3 inactive + // 4 leader + + // PREFERENCE + p1 : [0..1]; + + // VARIABLES FOR SENDING AND RECEIVING + receive1 : [0..2]; + // not received anything + // received choice + // received counter + sent1 : [0..2]; + // not send anything + // sent choice + // sent counter + + // pick value + [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); + + // send preference + [p12] (s1=1) & (sent1=0) -> (sent1'=1); + // receive preference + // stay active + [p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p51] (s1=1) & (receive1=0) & (p1=0) & (p5=1) -> (s1'=3) & (receive1'=1); + + // send preference (can now reset preference) + [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (already sent preference) + // not received counter yet + [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); + // received counter (pick again) + [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive counter and not sent yet (note in this case do not pass it on as will send own counter) + [c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // send preference (must have received preference) and can now reset + [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); + // send counter (must have received counter first) and can now reset + [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + + // receive preference + [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); + // receive counter + [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+1) & (receive1'=2); + + // done + [done] (s1=4) -> (s1'=s1); + // add loop for processes who are inactive + [done] (s1=3) -> (s1'=s1); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule +module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards "rounds" + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; + diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..f6ad1823f --- /dev/null +++ b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,174 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/utility/solver.h" +#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/parser/FormulaParser.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/StandardRewardModel.h" +#include "src/settings/SettingsManager.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" + +#include "src/settings/modules/GeneralSettings.h" + +TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(27299ul, model->getNumberOfStates()); + EXPECT_EQ(74365ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(27299ul, model->getNumberOfStates()); + EXPECT_EQ(74365ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/csma3_4.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser(program); + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("time"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(1460287ul, model->getNumberOfStates()); + EXPECT_EQ(2396727ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.90468935682619855, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.90468935682619855, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ F (min_backoff_after_success < 4) ]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file