From 94b25c02cadde6fac5e89238f0ad0d1da24eb5b8 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 16 Apr 2014 21:18:12 +0200
Subject: [PATCH 1/4] Fixed bugs in some files. Made LTL a little better to
compile under WIN32.
Former-commit-id: 71377f0672171b8dd8dbd9eb34425cc1de46ab4a
---
CMakeLists.txt | 3 +++
.../ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp | 2 +-
.../ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp | 2 +-
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h | 2 +-
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h | 2 +-
src/parser/PrctlParser.cpp | 2 +-
src/parser/PrismParser.h | 2 +-
src/storage/expressions/SimpleValuation.h | 5 ++++-
src/storage/prism/LocatedInformation.h | 1 +
test/functional/solver/GmmxxLinearEquationSolverTest.cpp | 2 +-
test/functional/storage/ExpressionTest.cpp | 1 +
11 files changed, 16 insertions(+), 8 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 77b5c64a0..c6d62bdde 100644
--- a/CMakeLists.txt
+++ b/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
add_definitions(/DNOMINMAX)
+ # since nobody cares at the moment
+ add_definitions(/wd4250)
+
if(ENABLE_Z3)
set(Z3_LIB_NAME "libz3")
endif()
diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp
index f20e1eedb..55e55fbd2 100644
--- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp
+++ b/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. */
-#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L
+#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
#include <inttypes.h>
typedef int8_t flex_int8_t;
typedef uint8_t flex_uint8_t;
diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp
index 82812c039..9be4a847a 100644
--- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp
+++ b/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. */
-#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L
+#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
#include <inttypes.h>
typedef int8_t flex_int8_t;
typedef uint8_t flex_uint8_t;
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 2f03603d8..9d43dfb52 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
+++ b/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.
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 {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index 868f78722..c3e2aec58 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -410,7 +410,7 @@ namespace storm {
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;
}
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index fb58d7ee9..d929c5ac7 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -140,7 +140,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
phoenix::new_<storm::property::prctl::ReachabilityReward<double>>(qi::_1)];
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)];
instantaneousReward.name("path formula (for reward operator)");
steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 3f8f17b65..db0ae9696 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -85,7 +85,7 @@ namespace storm {
}
};
- struct keywordsStruct : qi::symbols<char, bool> {
+ struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
keywordsStruct() {
add
("dtmc", 1)
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index 35b74291b..a196921a6 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -7,6 +7,7 @@
#include <iostream>
#include "src/storage/expressions/Valuation.h"
+#include "src/utility/OsDetection.h"
namespace storm {
namespace expressions {
@@ -23,8 +24,10 @@ namespace storm {
// Instantiate some constructors and assignments with their default implementations.
SimpleValuation(SimpleValuation const&) = default;
SimpleValuation& operator=(SimpleValuation const&) = default;
- SimpleValuation(SimpleValuation&&) = default;
+#ifndef WINDOWS
+ SimpleValuation(SimpleValuation&&) = default;
SimpleValuation& operator=(SimpleValuation&&) = default;
+#endif
virtual ~SimpleValuation() = default;
/*!
diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h
index 8aa4d301e..81f5334b5 100644
--- a/src/storage/prism/LocatedInformation.h
+++ b/src/storage/prism/LocatedInformation.h
@@ -2,6 +2,7 @@
#define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_
#include <string>
+#include <cstdint>
#include "src/utility/OsDetection.h"
diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp
index 077920f13..0381be434 100644
--- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp
+++ b/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));
- 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_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());
diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp
index 0c19c5bfb..41556f6d6 100644
--- a/test/functional/storage/ExpressionTest.cpp
+++ b/test/functional/storage/ExpressionTest.cpp
@@ -1,4 +1,5 @@
#include <map>
+#include <string>
#include "gtest/gtest.h"
#include "src/storage/expressions/Expression.h"
From 311247ff0cba4b8a38637ce5e8daa5703a9e4422 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 17 Apr 2014 18:30:57 +0200
Subject: [PATCH 2/4] Added support for Xor in expression classes and added
parsing functionality for Xor, Implies and Iff.
Former-commit-id: 16e023cf26806e7d9c6c7f72073b77bfff975d61
---
src/parser/PrismParser.cpp | 28 +++++++++++++++++--
src/parser/PrismParser.h | 8 ++++--
.../BinaryBooleanFunctionExpression.cpp | 3 ++
.../BinaryBooleanFunctionExpression.h | 2 +-
src/storage/expressions/Expression.cpp | 5 ++++
src/storage/expressions/Expression.h | 1 +
test/functional/parser/PrismParserTest.cpp | 2 +-
test/functional/storage/ExpressionTest.cpp | 6 ++++
8 files changed, 49 insertions(+), 6 deletions(-)
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 6039c2c11..f46b3f691 100644
--- a/src/parser/PrismParser.cpp
+++ b/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.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");
- 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");
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 {
if (!this->secondRun) {
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 {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 3f8f17b65..de3effa32 100644
--- a/src/parser/PrismParser.h
+++ b/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/expressions/Expression.h"
+#include "src/storage/expressions/Expressions.h"
#include "src/exceptions/ExceptionMacros.h"
namespace storm {
@@ -244,8 +245,8 @@ namespace storm {
// Rules for parsing a composed expression.
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
- qi::rule<Iterator, storm::expressions::Expression(), Skipper> orExpression;
- qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
+ qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
+ 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(), qi::locals<bool>, Skipper> plusExpression;
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);
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 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 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 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 createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
index 9f5e5edeb..d5d6694ab 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
@@ -23,6 +23,7 @@ namespace storm {
switch (this->getOperatorType()) {
case OperatorType::And: 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::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break;
}
@@ -55,6 +56,7 @@ namespace storm {
return firstOperandSimplified;
}
break;
+ case OperatorType::Xor: break;
case OperatorType::Implies: if (firstOperandSimplified->isTrue()) {
return secondOperandSimplified;
} else if (firstOperandSimplified->isFalse()) {
@@ -88,6 +90,7 @@ namespace storm {
switch (this->getOperatorType()) {
case OperatorType::And: stream << " & "; break;
case OperatorType::Or: stream << " | "; break;
+ case OperatorType::Xor: stream << " ^ "; break;
case OperatorType::Implies: stream << " => "; break;
case OperatorType::Iff: stream << " <=> "; break;
}
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h
index 7a05a1ab5..8b1bb7437 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h
@@ -11,7 +11,7 @@ namespace storm {
/*!
* 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.
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 7eb94966b..5b5a2bfb6 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -166,6 +166,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)));
}
+ 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 {
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)));
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index ea7d99572..d751dfbb9 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -47,6 +47,7 @@ namespace storm {
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!() const;
diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp
index 739d9ca5b..381ca3e1b 100644
--- a/test/functional/parser/PrismParserTest.cpp
+++ b/test/functional/parser/PrismParserTest.cpp
@@ -47,7 +47,7 @@ TEST(PrismParser, SimpleFullTest) {
R"(dtmc
module mod1
b : bool;
- [a] true -> 1: (b'=true);
+ [a] true -> 1: (b'=true ^ false <=> b => false);
endmodule)";
storm::prism::Program result;
diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp
index 0c19c5bfb..6ce9f50c5 100644
--- a/test/functional/storage/ExpressionTest.cpp
+++ b/test/functional/storage/ExpressionTest.cpp
@@ -264,6 +264,12 @@ TEST(Expression, OperatorTest) {
ASSERT_NO_THROW(tempExpression = boolVarExpression.iff(boolConstExpression));
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_NO_THROW(tempExpression = threeExpression.floor());
EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int);
From d57a0c9901ca75d287ac68d3662badc777ae5c9f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 17 Apr 2014 18:41:36 +0200
Subject: [PATCH 3/4] Replaced memcpy by std::copy.
Former-commit-id: ef31cf99772064aa660ee1acfc7ab05037b8087a
---
src/storage/dd/CuddDd.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index c5fb92bbd..7ea5ab260 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -388,14 +388,14 @@ namespace storm {
std::vector<char*> ddNames;
std::string ddName("f");
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.
std::vector<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
std::vector<char*> ddVariableNames;
for (auto const& element : ddVariableNamesAsStrings) {
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.
From 1d8ae9fc899da8a46788dad1abfbc0f0b1006dcb Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Thu, 17 Apr 2014 19:11:52 +0200
Subject: [PATCH 4/4] Fixed an issue with templated variadic template arguments
(see
http://stackoverflow.com/questions/23119273/use-a-templated-variadic-template-parameter-as-specialized-parameter
for discussion)
Former-commit-id: e7d2d054b6115ba4e15a667bba293effd53d470b
---
src/parser/PrismParser.cpp | 12 +++---
src/storage/expressions/Expression.cpp | 23 ++++++------
src/storage/expressions/Expression.h | 28 ++++++++++++--
.../IdentifierSubstitutionVisitor.cpp | 37 ++++++++++---------
.../IdentifierSubstitutionVisitor.h | 6 +--
.../expressions/SubstitutionVisitor.cpp | 37 ++++++++++---------
src/storage/expressions/SubstitutionVisitor.h | 6 +--
src/storage/prism/Assignment.cpp | 2 +-
src/storage/prism/BooleanVariable.cpp | 2 +-
src/storage/prism/Command.cpp | 2 +-
src/storage/prism/Constant.cpp | 2 +-
src/storage/prism/Formula.cpp | 2 +-
src/storage/prism/IntegerVariable.cpp | 2 +-
src/storage/prism/Label.cpp | 2 +-
src/storage/prism/Program.cpp | 4 +-
src/storage/prism/StateReward.cpp | 2 +-
src/storage/prism/TransitionReward.cpp | 2 +-
src/storage/prism/Update.cpp | 2 +-
src/storage/prism/Variable.cpp | 2 +-
test/functional/storage/ExpressionTest.cpp | 2 +-
20 files changed, 100 insertions(+), 77 deletions(-)
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 6039c2c11..9679168b6 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -585,7 +585,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
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.
@@ -594,7 +594,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
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.
@@ -606,12 +606,12 @@ namespace storm {
for (auto const& assignment : update.getAssignments()) {
auto const& renamingPair = renaming.find(assignment.getVariableName());
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 {
- 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;
}
@@ -621,7 +621,7 @@ namespace storm {
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;
}
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 7eb94966b..93e356009 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -27,15 +27,21 @@ namespace storm {
// Intentionally left empty.
}
- template<template<typename... Arguments> class MapType>
- Expression Expression::substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const {
- return SubstitutionVisitor<MapType>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
+ Expression Expression::substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const {
+ return SubstitutionVisitor< std::map<std::string, Expression> >(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(MapType<std::string, std::string> const& identifierToIdentifierMap) const {
- return IdentifierSubstitutionVisitor<MapType>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+ Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
+ return IdentifierSubstitutionVisitor< std::map<std::string, std::string> >(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 {
return this->getBaseExpression().evaluateAsBool(valuation);
@@ -247,11 +253,6 @@ namespace storm {
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) {
stream << expression.getBaseExpression();
return stream;
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index ea7d99572..3001def0a 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -2,6 +2,8 @@
#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
#include <memory>
+#include <map>
+#include <unordered_map>
#include "src/storage/expressions/BaseExpression.h"
#include "src/utility/OsDetection.h"
@@ -76,8 +78,18 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* expression they are mapped to.
*/
- template<template<typename... Arguments> class MapType>
- Expression substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const;
+ Expression substitute(std::map<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.
@@ -86,8 +98,16 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* identifiers they are mapped to.
*/
- template<template<typename... Arguments> class MapType>
- Expression substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const;
+ Expression substitute(std::map<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
diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp
index 17161775a..1b058bed2 100644
--- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp
+++ b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp
@@ -1,5 +1,6 @@
#include <map>
#include <unordered_map>
+#include <string>
#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
@@ -19,18 +20,18 @@
namespace storm {
namespace expressions {
- template<template<typename... Arguments> class MapType>
- IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
+ template<typename MapType>
+ IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
// Intentionally left empty.
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
Expression IdentifierSubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this);
return Expression(this->expressionStack.top());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
// 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());
@@ -117,7 +118,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// 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());
@@ -128,7 +129,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// 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());
@@ -139,7 +140,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it.
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) {
expression->getOperand()->accept(this);
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) {
expression->getOperand()->accept(this);
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) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
// Explicitly instantiate the class with map and unordered_map.
- template class IdentifierSubstitutionVisitor<std::map>;
- template class IdentifierSubstitutionVisitor<std::unordered_map>;
+ template class IdentifierSubstitutionVisitor< std::map<std::string, std::string> >;
+ template class IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >;
}
}
diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h
index 6be7aa9ca..e8412d949 100644
--- a/src/storage/expressions/IdentifierSubstitutionVisitor.h
+++ b/src/storage/expressions/IdentifierSubstitutionVisitor.h
@@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
class IdentifierSubstitutionVisitor : public ExpressionVisitor {
public:
/*!
@@ -16,7 +16,7 @@ namespace storm {
*
* @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
@@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced.
- MapType<std::string, std::string> const& identifierToIdentifierMap;
+ MapType const& identifierToIdentifierMap;
};
}
}
diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp
index c3f2ea0a8..54b533d49 100644
--- a/src/storage/expressions/SubstitutionVisitor.cpp
+++ b/src/storage/expressions/SubstitutionVisitor.cpp
@@ -1,5 +1,6 @@
#include <map>
#include <unordered_map>
+#include <string>
#include "src/storage/expressions/SubstitutionVisitor.h"
@@ -19,18 +20,18 @@
namespace storm {
namespace expressions {
- template<template<typename... Arguments> class MapType>
- SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType<std::string, Expression> const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) {
+ template<typename MapType>
+ SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) {
// Intentionally left empty.
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
Expression SubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this);
return Expression(this->expressionStack.top());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
expression->getFirstOperand()->accept(this);
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) {
// 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());
@@ -117,7 +118,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// 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());
@@ -128,7 +129,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// 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());
@@ -139,7 +140,7 @@ namespace storm {
}
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it.
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) {
expression->getOperand()->accept(this);
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) {
expression->getOperand()->accept(this);
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) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
// Explicitly instantiate the class with map and unordered_map.
- template class SubstitutionVisitor<std::map>;
- template class SubstitutionVisitor<std::unordered_map>;
+ template class SubstitutionVisitor< std::map<std::string, Expression> >;
+ template class SubstitutionVisitor< std::unordered_map<std::string, Expression> >;
}
}
diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h
index ad29ad6ab..d46d62cee 100644
--- a/src/storage/expressions/SubstitutionVisitor.h
+++ b/src/storage/expressions/SubstitutionVisitor.h
@@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
- template<template<typename... Arguments> class MapType>
+ template<typename MapType>
class SubstitutionVisitor : public ExpressionVisitor {
public:
/*!
@@ -16,7 +16,7 @@ namespace storm {
*
* @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
@@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced.
- MapType<std::string, Expression> const& identifierToExpressionMap;
+ MapType const& identifierToExpressionMap;
};
}
}
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
index f15797e6d..3b63703ed 100644
--- a/src/storage/prism/Assignment.cpp
+++ b/src/storage/prism/Assignment.cpp
@@ -15,7 +15,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
index 478b9322d..ef88cefc4 100644
--- a/src/storage/prism/BooleanVariable.cpp
+++ b/src/storage/prism/BooleanVariable.cpp
@@ -11,7 +11,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index f075ff6c6..4b36942df 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -37,7 +37,7 @@ namespace storm {
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) {
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index 160e9ad22..3df0a26bc 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -27,7 +27,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp
index 3bf72a7de..fbda0c69d 100644
--- a/src/storage/prism/Formula.cpp
+++ b/src/storage/prism/Formula.cpp
@@ -19,7 +19,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp
index a80b6394e..1968a07ca 100644
--- a/src/storage/prism/IntegerVariable.cpp
+++ b/src/storage/prism/IntegerVariable.cpp
@@ -19,7 +19,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp
index a78f9079f..cb8a13f25 100644
--- a/src/storage/prism/Label.cpp
+++ b/src/storage/prism/Label.cpp
@@ -15,7 +15,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index cdbba3e22..1c4118b8b 100644
--- a/src/storage/prism/Program.cpp
+++ b/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() << "'.");
// 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 {
auto const& variableExpressionPair = constantDefinitions.find(constant.getName());
@@ -306,7 +306,7 @@ namespace storm {
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;
newLabels.reserve(this->getNumberOfLabels());
diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp
index ab2f0974b..a93729b52 100644
--- a/src/storage/prism/StateReward.cpp
+++ b/src/storage/prism/StateReward.cpp
@@ -15,7 +15,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp
index 0034231d8..cef7bf654 100644
--- a/src/storage/prism/TransitionReward.cpp
+++ b/src/storage/prism/TransitionReward.cpp
@@ -19,7 +19,7 @@ namespace storm {
}
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) {
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index 2e01187c9..5d65e6dd5 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -44,7 +44,7 @@ namespace storm {
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) {
diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp
index e6c884813..4aabd548c 100644
--- a/src/storage/prism/Variable.cpp
+++ b/src/storage/prism/Variable.cpp
@@ -8,7 +8,7 @@ namespace storm {
// 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.
}
diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp
index 41556f6d6..d70cbd7d1 100644
--- a/test/functional/storage/ExpressionTest.cpp
+++ b/test/functional/storage/ExpressionTest.cpp
@@ -306,7 +306,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()) };
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());
}