Browse Source

Merge branch 'master' into ddLayerExtensions

Former-commit-id: 9eab593479
main
dehnert 11 years ago
parent
commit
dc80b987c2
  1. 3
      CMakeLists.txt
  2. 2
      resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp
  3. 2
      resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp
  4. 2
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  5. 2
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  6. 2
      src/parser/PrctlParser.cpp
  7. 40
      src/parser/PrismParser.cpp
  8. 10
      src/parser/PrismParser.h
  9. 4
      src/storage/dd/CuddDd.cpp
  10. 3
      src/storage/expressions/BinaryBooleanFunctionExpression.cpp
  11. 2
      src/storage/expressions/BinaryBooleanFunctionExpression.h
  12. 28
      src/storage/expressions/Expression.cpp
  13. 29
      src/storage/expressions/Expression.h
  14. 37
      src/storage/expressions/IdentifierSubstitutionVisitor.cpp
  15. 6
      src/storage/expressions/IdentifierSubstitutionVisitor.h
  16. 5
      src/storage/expressions/SimpleValuation.h
  17. 37
      src/storage/expressions/SubstitutionVisitor.cpp
  18. 6
      src/storage/expressions/SubstitutionVisitor.h
  19. 2
      src/storage/prism/Assignment.cpp
  20. 2
      src/storage/prism/BooleanVariable.cpp
  21. 2
      src/storage/prism/Command.cpp
  22. 2
      src/storage/prism/Constant.cpp
  23. 2
      src/storage/prism/Formula.cpp
  24. 2
      src/storage/prism/IntegerVariable.cpp
  25. 2
      src/storage/prism/Label.cpp
  26. 1
      src/storage/prism/LocatedInformation.h
  27. 4
      src/storage/prism/Program.cpp
  28. 2
      src/storage/prism/StateReward.cpp
  29. 2
      src/storage/prism/TransitionReward.cpp
  30. 2
      src/storage/prism/Update.cpp
  31. 2
      src/storage/prism/Variable.cpp
  32. 2
      test/functional/parser/PrismParserTest.cpp
  33. 2
      test/functional/solver/GmmxxLinearEquationSolverTest.cpp
  34. 9
      test/functional/storage/ExpressionTest.cpp

3
CMakeLists.txt

@ -122,6 +122,9 @@ elseif(MSVC)
# Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max
add_definitions(/DNOMINMAX) add_definitions(/DNOMINMAX)
# since nobody cares at the moment
add_definitions(/wd4250)
if(ENABLE_Z3) if(ENABLE_Z3)
set(Z3_LIB_NAME "libz3") set(Z3_LIB_NAME "libz3")
endif() endif()

2
resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp

@ -31,7 +31,7 @@
/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */ /* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L #if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
#include <inttypes.h> #include <inttypes.h>
typedef int8_t flex_int8_t; typedef int8_t flex_int8_t;
typedef uint8_t flex_uint8_t; typedef uint8_t flex_uint8_t;

2
resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp

@ -31,7 +31,7 @@
/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */ /* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L #if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
#include <inttypes.h> #include <inttypes.h>
typedef int8_t flex_int8_t; typedef int8_t flex_int8_t;
typedef uint8_t flex_uint8_t; typedef uint8_t flex_uint8_t;

2
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@ -393,7 +393,7 @@ public:
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. // Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
if (linearEquationSolver != nullptr) { if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound()); this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound()));
} else { } else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
} }

2
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@ -410,7 +410,7 @@ namespace storm {
result.resize(this->getModel().getNumberOfStates()); result.resize(this->getModel().getNumberOfStates());
} }
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound()); this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound()));
return result; return result;
} }

2
src/parser/PrctlParser.cpp

@ -140,7 +140,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val = reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
phoenix::new_<storm::property::prctl::ReachabilityReward<double>>(qi::_1)]; phoenix::new_<storm::property::prctl::ReachabilityReward<double>>(qi::_1)];
reachabilityReward.name("path formula (for reward operator)"); reachabilityReward.name("path formula (for reward operator)");
instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_) instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::uint_)
[qi::_val = phoenix::new_<storm::property::prctl::InstantaneousReward<double>>(qi::_1)]; [qi::_val = phoenix::new_<storm::property::prctl::InstantaneousReward<double>>(qi::_1)];
instantaneousReward.name("path formula (for reward operator)"); instantaneousReward.name("path formula (for reward operator)");
steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()]; steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];

40
src/parser/PrismParser.cpp

@ -91,10 +91,10 @@ namespace storm {
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
relativeExpression.name("relative expression"); relativeExpression.name("relative expression");
andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; andExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("&")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And] | qi::lit("<=>")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff] | qi::lit("^")[qi::_a = storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor]) >> relativeExpression)[phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) [ qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [ phoenix::if_(qi::_a == storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff) [ qi::_val = phoenix::bind(&PrismParser::createIffExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createXorExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ] ];
andExpression.name("and expression"); andExpression.name("and expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)]; orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
orExpression.name("or expression"); orExpression.name("or expression");
iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
@ -271,6 +271,14 @@ namespace storm {
} }
} }
storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1.implies(e2);
}
}
storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
@ -319,6 +327,22 @@ namespace storm {
} }
} }
storm::expressions::Expression PrismParser::createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1.iff(e2);
}
}
storm::expressions::Expression PrismParser::createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return e1 ^ e2;
}
}
storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
@ -585,7 +609,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1))); booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
} }
// Rename the integer variables. // Rename the integer variables.
@ -594,7 +618,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute<std::map>(expressionRenaming), variable.getUpperBoundExpression().substitute<std::map>(expressionRenaming), variable.getInitialValueExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1))); integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
} }
// Rename commands. // Rename commands.
@ -606,12 +630,12 @@ namespace storm {
for (auto const& assignment : update.getAssignments()) { for (auto const& assignment : update.getAssignments()) {
auto const& renamingPair = renaming.find(assignment.getVariableName()); auto const& renamingPair = renaming.find(assignment.getVariableName());
if (renamingPair != renaming.end()) { if (renamingPair != renaming.end()) {
assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1)); assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1));
} else { } else {
assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1)); assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1));
} }
} }
updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute<std::map>(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1));
++globalProgramInformation.currentUpdateIndex; ++globalProgramInformation.currentUpdateIndex;
} }
@ -621,7 +645,7 @@ namespace storm {
newActionName = renamingPair->second; newActionName = renamingPair->second;
} }
commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute<std::map>(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
++globalProgramInformation.currentCommandIndex; ++globalProgramInformation.currentCommandIndex;
} }

10
src/parser/PrismParser.h

@ -25,6 +25,7 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost:
#include "src/storage/prism/Program.h" #include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h"
#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/ExceptionMacros.h"
namespace storm { namespace storm {
@ -85,7 +86,7 @@ namespace storm {
} }
}; };
struct keywordsStruct : qi::symbols<char, bool> { struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
keywordsStruct() { keywordsStruct() {
add add
("dtmc", 1) ("dtmc", 1)
@ -244,8 +245,8 @@ namespace storm {
// Rules for parsing a composed expression. // Rules for parsing a composed expression.
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression; qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression; qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> orExpression; qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression; qi::rule<Iterator, storm::expressions::Expression(), qi::locals<storm::expressions::BinaryBooleanFunctionExpression::OperatorType>, Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression; qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression; 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> multiplicationExpression;
@ -269,12 +270,15 @@ namespace storm {
bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createIffExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createXorExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;

4
src/storage/dd/CuddDd.cpp

@ -389,14 +389,14 @@ namespace storm {
std::vector<char*> ddNames; std::vector<char*> ddNames;
std::string ddName("f"); std::string ddName("f");
ddNames.push_back(new char[ddName.size() + 1]); ddNames.push_back(new char[ddName.size() + 1]);
memcpy(ddNames.back(), ddName.c_str(), 2); std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back());
// Now build the variables names. // Now build the variables names.
std::vector<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); std::vector<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
std::vector<char*> ddVariableNames; std::vector<char*> ddVariableNames;
for (auto const& element : ddVariableNamesAsStrings) { for (auto const& element : ddVariableNamesAsStrings) {
ddVariableNames.push_back(new char[element.size() + 1]); ddVariableNames.push_back(new char[element.size() + 1]);
memcpy(ddVariableNames.back(), element.c_str(), element.size() + 1); std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back());
} }
// Open the file, dump the DD and close it again. // Open the file, dump the DD and close it again.

3
src/storage/expressions/BinaryBooleanFunctionExpression.cpp

@ -23,6 +23,7 @@ namespace storm {
switch (this->getOperatorType()) { switch (this->getOperatorType()) {
case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break; case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break;
case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break; case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break;
case OperatorType::Xor: result = firstOperandEvaluation ^ secondOperandEvaluation; break;
case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break; case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break;
case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break; case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break;
} }
@ -55,6 +56,7 @@ namespace storm {
return firstOperandSimplified; return firstOperandSimplified;
} }
break; break;
case OperatorType::Xor: break;
case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { case OperatorType::Implies: if (firstOperandSimplified->isTrue()) {
return secondOperandSimplified; return secondOperandSimplified;
} else if (firstOperandSimplified->isFalse()) { } else if (firstOperandSimplified->isFalse()) {
@ -88,6 +90,7 @@ namespace storm {
switch (this->getOperatorType()) { switch (this->getOperatorType()) {
case OperatorType::And: stream << " & "; break; case OperatorType::And: stream << " & "; break;
case OperatorType::Or: stream << " | "; break; case OperatorType::Or: stream << " | "; break;
case OperatorType::Xor: stream << " ^ "; break;
case OperatorType::Implies: stream << " => "; break; case OperatorType::Implies: stream << " => "; break;
case OperatorType::Iff: stream << " <=> "; break; case OperatorType::Iff: stream << " <=> "; break;
} }

2
src/storage/expressions/BinaryBooleanFunctionExpression.h

@ -11,7 +11,7 @@ namespace storm {
/*! /*!
* An enum type specifying the different operators applicable. * An enum type specifying the different operators applicable.
*/ */
enum class OperatorType {And, Or, Implies, Iff}; enum class OperatorType {And, Or, Xor, Implies, Iff};
/*! /*!
* Creates a binary boolean function expression with the given return type, operands and operator. * Creates a binary boolean function expression with the given return type, operands and operator.

28
src/storage/expressions/Expression.cpp

@ -27,15 +27,21 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
template<template<typename... Arguments> class MapType> Expression Expression::substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const {
Expression Expression::substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const { return SubstitutionVisitor< std::map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
return SubstitutionVisitor<MapType>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
} }
Expression Expression::substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const {
return SubstitutionVisitor< std::unordered_map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
}
template<template<typename... Arguments> class MapType> Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
Expression Expression::substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const { return IdentifierSubstitutionVisitor< std::map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
return IdentifierSubstitutionVisitor<MapType>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
} }
Expression Expression::substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const {
return IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
}
bool Expression::evaluateAsBool(Valuation const* valuation) const { bool Expression::evaluateAsBool(Valuation const* valuation) const {
return this->getBaseExpression().evaluateAsBool(valuation); return this->getBaseExpression().evaluateAsBool(valuation);
@ -166,6 +172,11 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide)));
} }
Expression Expression::operator^(Expression const& other) const {
LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires boolean operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor)));
}
Expression Expression::operator&&(Expression const& other) const { Expression Expression::operator&&(Expression const& other) const {
LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands.");
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And)));
@ -247,11 +258,6 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil)));
} }
template Expression Expression::substitute<std::map>(std::map<std::string, storm::expressions::Expression> const&) const;
template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, storm::expressions::Expression> const&) const;
template Expression Expression::substitute<std::map>(std::map<std::string, std::string> const&) const;
template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, std::string> const&) const;
std::ostream& operator<<(std::ostream& stream, Expression const& expression) { std::ostream& operator<<(std::ostream& stream, Expression const& expression) {
stream << expression.getBaseExpression(); stream << expression.getBaseExpression();
return stream; return stream;

29
src/storage/expressions/Expression.h

@ -2,6 +2,8 @@
#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ #define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
#include <memory> #include <memory>
#include <map>
#include <unordered_map>
#include "src/storage/expressions/BaseExpression.h" #include "src/storage/expressions/BaseExpression.h"
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"
@ -47,6 +49,7 @@ namespace storm {
Expression operator-() const; Expression operator-() const;
Expression operator*(Expression const& other) const; Expression operator*(Expression const& other) const;
Expression operator/(Expression const& other) const; Expression operator/(Expression const& other) const;
Expression operator^(Expression const& other) const;
Expression operator&&(Expression const& other) const; Expression operator&&(Expression const& other) const;
Expression operator||(Expression const& other) const; Expression operator||(Expression const& other) const;
Expression operator!() const; Expression operator!() const;
@ -76,8 +79,18 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the * @return An expression in which all identifiers in the key set of the mapping are replaced by the
* expression they are mapped to. * expression they are mapped to.
*/ */
template<template<typename... Arguments> class MapType> Expression substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const;
Expression substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const; /*!
* Substitutes all occurrences of identifiers according to the given map. Note that this substitution is
* done simultaneously, i.e., identifiers appearing in the expressions that were "plugged in" are not
* substituted.
*
* @param identifierToExpressionMap A mapping from identifiers to the expression they are substituted with.
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* expression they are mapped to.
*/
Expression substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const;
/*! /*!
* Substitutes all occurrences of identifiers with different names given by a mapping. * Substitutes all occurrences of identifiers with different names given by a mapping.
@ -86,8 +99,16 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the * @return An expression in which all identifiers in the key set of the mapping are replaced by the
* identifiers they are mapped to. * identifiers they are mapped to.
*/ */
template<template<typename... Arguments> class MapType> Expression substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const;
Expression substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const; /*!
* Substitutes all occurrences of identifiers with different names given by a mapping.
*
* @param identifierToIdentifierMap A mapping from identifiers to identifiers they are substituted with.
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* identifiers they are mapped to.
*/
Expression substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const;
/*! /*!
* Evaluates the expression under the valuation of unknowns (variables and constants) given by the * Evaluates the expression under the valuation of unknowns (variables and constants) given by the

37
src/storage/expressions/IdentifierSubstitutionVisitor.cpp

@ -1,5 +1,6 @@
#include <map> #include <map>
#include <unordered_map> #include <unordered_map>
#include <string>
#include "src/storage/expressions/IdentifierSubstitutionVisitor.h" #include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
@ -19,18 +20,18 @@
namespace storm { namespace storm {
namespace expressions { namespace expressions {
template<template<typename... Arguments> class MapType> template<typename MapType>
IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
// Intentionally left empty. // Intentionally left empty.
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
Expression IdentifierSubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) { Expression IdentifierSubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this); expression->accept(this);
return Expression(this->expressionStack.top()); return Expression(this->expressionStack.top());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this); expression->getCondition()->accept(this);
std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top();
@ -52,7 +53,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -70,7 +71,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -88,7 +89,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -106,7 +107,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
// If the boolean constant is in the key set of the substitution, we need to replace it. // If the boolean constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -117,7 +118,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// If the double constant is in the key set of the substitution, we need to replace it. // If the double constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -128,7 +129,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// If the integer constant is in the key set of the substitution, we need to replace it. // If the integer constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -139,7 +140,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it. // If the variable is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getVariableName()); auto const& namePair = this->identifierToIdentifierMap.find(expression->getVariableName());
@ -150,7 +151,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
expression->getOperand()->accept(this); expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -164,7 +165,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
expression->getOperand()->accept(this); expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -178,23 +179,23 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) { void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
// Explicitly instantiate the class with map and unordered_map. // Explicitly instantiate the class with map and unordered_map.
template class IdentifierSubstitutionVisitor<std::map>; template class IdentifierSubstitutionVisitor< std::map<std::string, std::string> >;
template class IdentifierSubstitutionVisitor<std::unordered_map>; template class IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >;
} }
} }

6
src/storage/expressions/IdentifierSubstitutionVisitor.h

@ -8,7 +8,7 @@
namespace storm { namespace storm {
namespace expressions { namespace expressions {
template<template<typename... Arguments> class MapType> template<typename MapType>
class IdentifierSubstitutionVisitor : public ExpressionVisitor { class IdentifierSubstitutionVisitor : public ExpressionVisitor {
public: public:
/*! /*!
@ -16,7 +16,7 @@ namespace storm {
* *
* @param identifierToExpressionMap A mapping from identifiers to expressions. * @param identifierToExpressionMap A mapping from identifiers to expressions.
*/ */
IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToExpressionMap); IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap);
/*! /*!
* Substitutes the identifiers in the given expression according to the previously given map and returns the * Substitutes the identifiers in the given expression according to the previously given map and returns the
@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack; std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced. // A mapping of identifier names to expressions with which they shall be replaced.
MapType<std::string, std::string> const& identifierToIdentifierMap; MapType const& identifierToIdentifierMap;
}; };
} }
} }

5
src/storage/expressions/SimpleValuation.h

@ -7,6 +7,7 @@
#include <iostream> #include <iostream>
#include "src/storage/expressions/Valuation.h" #include "src/storage/expressions/Valuation.h"
#include "src/utility/OsDetection.h"
namespace storm { namespace storm {
namespace expressions { namespace expressions {
@ -23,8 +24,10 @@ namespace storm {
// Instantiate some constructors and assignments with their default implementations. // Instantiate some constructors and assignments with their default implementations.
SimpleValuation(SimpleValuation const&) = default; SimpleValuation(SimpleValuation const&) = default;
SimpleValuation& operator=(SimpleValuation const&) = default; SimpleValuation& operator=(SimpleValuation const&) = default;
SimpleValuation(SimpleValuation&&) = default; #ifndef WINDOWS
SimpleValuation(SimpleValuation&&) = default;
SimpleValuation& operator=(SimpleValuation&&) = default; SimpleValuation& operator=(SimpleValuation&&) = default;
#endif
virtual ~SimpleValuation() = default; virtual ~SimpleValuation() = default;
/*! /*!

37
src/storage/expressions/SubstitutionVisitor.cpp

@ -1,5 +1,6 @@
#include <map> #include <map>
#include <unordered_map> #include <unordered_map>
#include <string>
#include "src/storage/expressions/SubstitutionVisitor.h" #include "src/storage/expressions/SubstitutionVisitor.h"
@ -19,18 +20,18 @@
namespace storm { namespace storm {
namespace expressions { namespace expressions {
template<template<typename... Arguments> class MapType> template<typename MapType>
SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType<std::string, Expression> const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) {
// Intentionally left empty. // Intentionally left empty.
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
Expression SubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) { Expression SubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this); expression->accept(this);
return Expression(this->expressionStack.top()); return Expression(this->expressionStack.top());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) { void SubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this); expression->getCondition()->accept(this);
std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top();
@ -52,7 +53,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) { void SubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -70,7 +71,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) { void SubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -88,7 +89,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) { void SubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
expression->getFirstOperand()->accept(this); expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -106,7 +107,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) { void SubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
// If the boolean constant is in the key set of the substitution, we need to replace it. // If the boolean constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -117,7 +118,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) { void SubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// If the double constant is in the key set of the substitution, we need to replace it. // If the double constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -128,7 +129,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) { void SubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// If the integer constant is in the key set of the substitution, we need to replace it. // If the integer constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -139,7 +140,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(VariableExpression const* expression) { void SubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it. // If the variable is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getVariableName()); auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getVariableName());
@ -150,7 +151,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) { void SubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
expression->getOperand()->accept(this); expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -164,7 +165,7 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) { void SubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
expression->getOperand()->accept(this); expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top(); std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -178,23 +179,23 @@ namespace storm {
} }
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) { void SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) { void SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
template<template<typename... Arguments> class MapType> template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) { void SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer()); this->expressionStack.push(expression->getSharedPointer());
} }
// Explicitly instantiate the class with map and unordered_map. // Explicitly instantiate the class with map and unordered_map.
template class SubstitutionVisitor<std::map>; template class SubstitutionVisitor< std::map<std::string, Expression> >;
template class SubstitutionVisitor<std::unordered_map>; template class SubstitutionVisitor< std::unordered_map<std::string, Expression> >;
} }
} }

6
src/storage/expressions/SubstitutionVisitor.h

@ -8,7 +8,7 @@
namespace storm { namespace storm {
namespace expressions { namespace expressions {
template<template<typename... Arguments> class MapType> template<typename MapType>
class SubstitutionVisitor : public ExpressionVisitor { class SubstitutionVisitor : public ExpressionVisitor {
public: public:
/*! /*!
@ -16,7 +16,7 @@ namespace storm {
* *
* @param identifierToExpressionMap A mapping from identifiers to expressions. * @param identifierToExpressionMap A mapping from identifiers to expressions.
*/ */
SubstitutionVisitor(MapType<std::string, Expression> const& identifierToExpressionMap); SubstitutionVisitor(MapType const& identifierToExpressionMap);
/*! /*!
* Substitutes the identifiers in the given expression according to the previously given map and returns the * Substitutes the identifiers in the given expression according to the previously given map and returns the
@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack; std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced. // A mapping of identifier names to expressions with which they shall be replaced.
MapType<std::string, Expression> const& identifierToExpressionMap; MapType const& identifierToExpressionMap;
}; };
} }
} }

2
src/storage/prism/Assignment.cpp

@ -15,7 +15,7 @@ namespace storm {
} }
Assignment Assignment::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { Assignment Assignment::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Assignment(this->getVariableName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {

2
src/storage/prism/BooleanVariable.cpp

@ -11,7 +11,7 @@ namespace storm {
} }
BooleanVariable BooleanVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { BooleanVariable BooleanVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {

2
src/storage/prism/Command.cpp

@ -37,7 +37,7 @@ namespace storm {
newUpdates.emplace_back(update.substitute(substitution)); newUpdates.emplace_back(update.substitute(substitution));
} }
return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute<std::map>(substitution), newUpdates, this->getFilename(), this->getLineNumber()); return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Command const& command) { std::ostream& operator<<(std::ostream& stream, Command const& command) {

2
src/storage/prism/Constant.cpp

@ -27,7 +27,7 @@ namespace storm {
} }
Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Constant(this->getType(), this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Constant const& constant) { std::ostream& operator<<(std::ostream& stream, Constant const& constant) {

2
src/storage/prism/Formula.cpp

@ -19,7 +19,7 @@ namespace storm {
} }
Formula Formula::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { Formula Formula::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Formula(this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Formula const& formula) { std::ostream& operator<<(std::ostream& stream, Formula const& formula) {

2
src/storage/prism/IntegerVariable.cpp

@ -19,7 +19,7 @@ namespace storm {
} }
IntegerVariable IntegerVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { IntegerVariable IntegerVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute<std::map>(substitution), this->getUpperBoundExpression().substitute<std::map>(substitution), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {

2
src/storage/prism/Label.cpp

@ -15,7 +15,7 @@ namespace storm {
} }
Label Label::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { Label Label::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Label(this->getName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Label const& label) { std::ostream& operator<<(std::ostream& stream, Label const& label) {

1
src/storage/prism/LocatedInformation.h

@ -2,6 +2,7 @@
#define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ #define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_
#include <string> #include <string>
#include <cstdint>
#include "src/utility/OsDetection.h" #include "src/utility/OsDetection.h"

4
src/storage/prism/Program.cpp

@ -229,7 +229,7 @@ namespace storm {
LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'."); LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
// Now replace the occurrences of undefined constants in its defining expression. // Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute<std::map>(constantDefinitions), constant.getFilename(), constant.getLineNumber()); newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
} else { } else {
auto const& variableExpressionPair = constantDefinitions.find(constant.getName()); auto const& variableExpressionPair = constantDefinitions.find(constant.getName());
@ -306,7 +306,7 @@ namespace storm {
newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution)); newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution));
} }
storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute<std::map>(constantSubstitution); storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution);
std::vector<Label> newLabels; std::vector<Label> newLabels;
newLabels.reserve(this->getNumberOfLabels()); newLabels.reserve(this->getNumberOfLabels());

2
src/storage/prism/StateReward.cpp

@ -15,7 +15,7 @@ namespace storm {
} }
StateReward StateReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { StateReward StateReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return StateReward(this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return StateReward(this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) { std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) {

2
src/storage/prism/TransitionReward.cpp

@ -19,7 +19,7 @@ namespace storm {
} }
TransitionReward TransitionReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const { TransitionReward TransitionReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber()); return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) { std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {

2
src/storage/prism/Update.cpp

@ -44,7 +44,7 @@ namespace storm {
newAssignments.emplace_back(assignment.substitute(substitution)); newAssignments.emplace_back(assignment.substitute(substitution));
} }
return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute<std::map>(substitution), newAssignments, this->getFilename(), this->getLineNumber()); return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber());
} }
std::ostream& operator<<(std::ostream& stream, Update const& update) { std::ostream& operator<<(std::ostream& stream, Update const& update) {

2
src/storage/prism/Variable.cpp

@ -8,7 +8,7 @@ namespace storm {
// Nothing to do here. // Nothing to do here.
} }
Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) { Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
// Intentionally left empty. // Intentionally left empty.
} }

2
test/functional/parser/PrismParserTest.cpp

@ -47,7 +47,7 @@ TEST(PrismParser, SimpleFullTest) {
R"(dtmc R"(dtmc
module mod1 module mod1
b : bool; b : bool;
[a] true -> 1: (b'=true); [a] true -> 1: (b'=true ^ false <=> b => false);
endmodule)"; endmodule)";
storm::prism::Program result; storm::prism::Program result;

2
test/functional/solver/GmmxxLinearEquationSolverTest.cpp

@ -81,7 +81,7 @@ TEST(GmmxxLinearEquationSolver, qmr) {
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE)); ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, 50); storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b)); ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());

9
test/functional/storage/ExpressionTest.cpp

@ -1,4 +1,5 @@
#include <map> #include <map>
#include <string>
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
@ -264,6 +265,12 @@ TEST(Expression, OperatorTest) {
ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression)); ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression));
EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException);
ASSERT_NO_THROW(tempExpression = trueExpression ^ falseExpression);
EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
ASSERT_NO_THROW(tempExpression = boolVarExpression ^ boolConstExpression);
EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool);
ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException); ASSERT_THROW(tempExpression = trueExpression.floor(), storm::exceptions::InvalidTypeException);
ASSERT_NO_THROW(tempExpression = threeExpression.floor()); ASSERT_NO_THROW(tempExpression = threeExpression.floor());
EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
@ -305,7 +312,7 @@ TEST(Expression, SubstitutionTest) {
std::map<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleConstExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) }; std::map<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleConstExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) };
storm::expressions::Expression substitutedExpression; storm::expressions::Expression substitutedExpression;
ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute<std::map>(substution)); ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
EXPECT_TRUE(substitutedExpression.simplify().isTrue()); EXPECT_TRUE(substitutedExpression.simplify().isTrue());
} }

|||||||
100:0
Loading…
Cancel
Save