sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added some syntatic sugar to PRISM parser in order to enhance performance tests of symbolic model checker 

Former-commit-id: d85ce26536
tempestpy_adaptions
dehnert 9 years ago
parent
329fee6b32
commit
b297cdf38f
9 changed files with 576 additions and 44 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 31
      src/parser/ExpressionParser.cpp
  2. 23
      src/parser/ExpressionParser.h
  3. 7
      src/parser/FormulaParser.cpp
  4. 3
      src/parser/FormulaParser.h
  5. 148
      src/storage/prism/Program.cpp
  6. 2
      src/utility/storm.cpp
  7. 134
      test/performance/builder/csma3_4.nm
  8. 98
      test/performance/builder/leader5.nm
  9. 174
      test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp

31
src/parser/ExpressionParser.cpp
View File

@ -5,47 +5,54 @@
namespace storm {
namespace parser {
ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> 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<char, uint_fast64_t> 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);

23
src/parser/ExpressionParser.h
View File

@ -120,15 +120,15 @@ namespace storm {
// A parser used for recognizing the operators at the "multiplication" precedence level.
multiplicationOperatorStruct multiplicationOperator_;
struct powerOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
powerOperatorStruct() {
struct infixPowerOperatorStruct : qi::symbols<char, storm::expressions::OperatorType> {
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<char, storm::expressions::OperatorType> {
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<char, storm::expressions::OperatorType> {
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<char, storm::expressions::Expression> {
trueFalseOperatorStruct(storm::expressions::ExpressionManager const& manager) {
add
@ -200,13 +210,14 @@ namespace storm {
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> powerExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> prefixPowerExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> infixPowerExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::OperatorType>, Skipper> floorCeilExpression;
qi::rule<Iterator, std::string(), Skipper> identifier;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).

7
src/parser/FormulaParser.cpp
View File

@ -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); });
}

3
src/parser/FormulaParser.h
View File

@ -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<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
FormulaParser(storm::prism::Program const& program);
FormulaParser(FormulaParser const& other);
FormulaParser& operator=(FormulaParser const& other);

148
src/storage/prism/Program.cpp
View File

@ -2,6 +2,7 @@
#include <algorithm>
#include <sstream>
#include <boost/algorithm/string/join.hpp>
#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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<std::string> 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<std::string> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<std::string> 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<std::string> 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<storm::expressions::Variable> 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<storm::expressions::Variable> 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<std::string> 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<std::string> 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<storm::expressions::Variable> 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<std::string> 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);

2
src/utility/storm.cpp
View File

@ -35,7 +35,7 @@ namespace storm {
}
std::vector<std::shared_ptr<storm::logic::Formula>> 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);
}
}

134
test/performance/builder/csma3_4.nm
View File

@ -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<sigma) -> (b'=2);
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
[send3] (b=1|b=2) & (y1<sigma) -> (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<sigma) -> (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<lambda) -> (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<slot) -> (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);

98
test/performance/builder/leader5.nm
View File

@ -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<N-1) -> (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<N-1) -> (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;

174
test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
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<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
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<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
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<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("time");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(1460287ul, model->getNumberOfStates());
EXPECT_EQ(2396727ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save