From 2fa3036dc39a00b32cce120c227c7c58f8bcecfc Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 2 Oct 2014 16:07:33 +0200
Subject: [PATCH] Added functionality to replace identifiers in an expression
with the values given in an valuation. State-variables now get replaced in
probabilities specified by a parameterized model. Fixed and added some
parameterized models.
Former-commit-id: a863a072619cfacecd0d1eebe879b21206175e21
---
.../pdtmc/brp/{brp_2_16.pm => brp_16_2.pm} | 6 +-
examples/pdtmc/brp/brp_32-4.pm | 137 ++++++++++++++++++
examples/pdtmc/brp/brp_64-4.pm | 137 ++++++++++++++++++
examples/pdtmc/nand/nand_10_1.pm | 8 +-
src/adapters/ExplicitModelAdapter.h | 2 +-
.../reachability/SparseSccModelChecker.cpp | 7 +
src/storage/expressions/Expression.cpp | 11 +-
src/storage/expressions/Expression.h | 10 ++
.../expressions/ExpressionEvaluation.h | 8 +-
... => IdentifierSubstitutionVisitorBase.cpp} | 54 ++-----
....h => IdentifierSubstitutionVisitorBase.h} | 22 +--
.../IdentifierSubstitutionWithMapVisitor.cpp | 30 ++++
.../IdentifierSubstitutionWithMapVisitor.h | 28 ++++
...tifierSubstitutionWithValuationVisitor.cpp | 37 +++++
...entifierSubstitutionWithValuationVisitor.h | 27 ++++
src/storage/expressions/SimpleValuation.h | 2 +
src/storage/prism/Constant.cpp | 6 +-
src/stormParametric.cpp | 4 +-
src/utility/constants.h | 8 +-
19 files changed, 464 insertions(+), 80 deletions(-)
rename examples/pdtmc/brp/{brp_2_16.pm => brp_16_2.pm} (98%)
create mode 100755 examples/pdtmc/brp/brp_32-4.pm
create mode 100755 examples/pdtmc/brp/brp_64-4.pm
rename src/storage/expressions/{IdentifierSubstitutionVisitor.cpp => IdentifierSubstitutionVisitorBase.cpp} (68%)
rename src/storage/expressions/{IdentifierSubstitutionVisitor.h => IdentifierSubstitutionVisitorBase.h} (67%)
create mode 100644 src/storage/expressions/IdentifierSubstitutionWithMapVisitor.cpp
create mode 100644 src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h
create mode 100644 src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.cpp
create mode 100644 src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h
diff --git a/examples/pdtmc/brp/brp_2_16.pm b/examples/pdtmc/brp/brp_16_2.pm
similarity index 98%
rename from examples/pdtmc/brp/brp_2_16.pm
rename to examples/pdtmc/brp/brp_16_2.pm
index d433fb87d..7be6c8130 100644
--- a/examples/pdtmc/brp/brp_2_16.pm
+++ b/examples/pdtmc/brp/brp_16_2.pm
@@ -9,8 +9,8 @@ const int N = 16;
const int MAX = 2;
// reliability of channels
-param float pL;
-param float pK;
+const double pL;
+const double pK;
module sender
@@ -133,3 +133,5 @@ module channelL
[TO_Ack] (l=2) -> (l'=0);
endmodule
+
+label "target" = s=5;
\ No newline at end of file
diff --git a/examples/pdtmc/brp/brp_32-4.pm b/examples/pdtmc/brp/brp_32-4.pm
new file mode 100755
index 000000000..c12c5f783
--- /dev/null
+++ b/examples/pdtmc/brp/brp_32-4.pm
@@ -0,0 +1,137 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N = 32;
+// maximum number of retransmissions
+const int MAX = 4;
+
+// reliability of channels
+const double pL;
+const double pK;
+
+module sender
+
+ s : [0..6];
+ // 0 idle
+ // 1 next_frame
+ // 2 wait_ack
+ // 3 retransmit
+ // 4 success
+ // 5 error
+ // 6 wait sync
+ srep : [0..3];
+ // 0 bottom
+ // 1 not ok (nok)
+ // 2 do not know (dk)
+ // 3 ok (ok)
+ nrtr : [0..MAX];
+ i : [0..N];
+ bs : bool;
+ s_ab : bool;
+ fs : bool;
+ ls : bool;
+
+ // idle
+ [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+ // next_frame
+ [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+ // wait_ack
+ [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+ [TO_Msg] (s=2) -> (s'=3);
+ [TO_Ack] (s=2) -> (s'=3);
+ // retransmit
+ [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+// prevents more than one file being sent
+module tester
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+label "target" = s=5;
\ No newline at end of file
diff --git a/examples/pdtmc/brp/brp_64-4.pm b/examples/pdtmc/brp/brp_64-4.pm
new file mode 100755
index 000000000..230c5754b
--- /dev/null
+++ b/examples/pdtmc/brp/brp_64-4.pm
@@ -0,0 +1,137 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N = 64;
+// maximum number of retransmissions
+const int MAX = 4;
+
+// reliability of channels
+const double pL;
+const double pK;
+
+module sender
+
+ s : [0..6];
+ // 0 idle
+ // 1 next_frame
+ // 2 wait_ack
+ // 3 retransmit
+ // 4 success
+ // 5 error
+ // 6 wait sync
+ srep : [0..3];
+ // 0 bottom
+ // 1 not ok (nok)
+ // 2 do not know (dk)
+ // 3 ok (ok)
+ nrtr : [0..MAX];
+ i : [0..N];
+ bs : bool;
+ s_ab : bool;
+ fs : bool;
+ ls : bool;
+
+ // idle
+ [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+ // next_frame
+ [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+ // wait_ack
+ [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+ [TO_Msg] (s=2) -> (s'=3);
+ [TO_Ack] (s=2) -> (s'=3);
+ // retransmit
+ [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+// prevents more than one file being sent
+module tester
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+label "target" = s=5;
\ No newline at end of file
diff --git a/examples/pdtmc/nand/nand_10_1.pm b/examples/pdtmc/nand/nand_10_1.pm
index c71d22cd7..f56664199 100644
--- a/examples/pdtmc/nand/nand_10_1.pm
+++ b/examples/pdtmc/nand/nand_10_1.pm
@@ -15,8 +15,8 @@ const int M = 2*K+1; // total number of multiplexing units
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
-param double perr; //(0.02) probability nand works correctly
-param double prob1; //(0.9) probability initial inputs are stimulated
+const double perr; //(0.02) probability nand works correctly
+const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
@@ -62,10 +62,12 @@ module multiplex
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
- [] s=4 -> true;
+ [] s=4 -> (s'=s);
endmodule
+label "target" = s=4 & z/N<0.1;
+
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index ab769907d..35a7d1249 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -308,7 +308,7 @@ namespace storm {
}
// Update the choice by adding the probability/target state to it.
- ValueType probabilityToAdd = eval.evaluate(update.getLikelihoodExpression(),currentState);
+ ValueType probabilityToAdd = eval.evaluate(update.getLikelihoodExpression(), currentState);
probabilitySum += probabilityToAdd;
boost::container::flat_set<uint_fast64_t> labels;
labels.insert(update.getGlobalIndex());
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp
index 9fee06d01..b6209853f 100644
--- a/src/modelchecker/reachability/SparseSccModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp
@@ -23,7 +23,9 @@ namespace storm {
static RationalFunction&& simplify(RationalFunction&& value) {
// In the general case, we don't to anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type.
+// std::cout << "simplifying " << value << std::endl;
value.simplify();
+// std::cout << "done simplifying." << std::endl;
return std::forward<RationalFunction>(value);
}
@@ -62,6 +64,8 @@ namespace storm {
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
+ std::cout << "solving system with " << maybeStates.getNumberOfSetBits() << " states." << std::endl;
+
// Create a vector for the probabilities to go to a state with probability 1 in one step.
std::vector<ValueType> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
@@ -169,8 +173,11 @@ namespace storm {
}
}
+ static int counter = 0;
+
template<typename ValueType>
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions) {
+ std::cout << "eliminating state " << counter++ << std::endl;
bool hasSelfLoop = false;
ValueType loopProbability = storm::utility::constantZero<ValueType>();
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index ad74066b3..7ab072371 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -3,7 +3,8 @@
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/SubstitutionVisitor.h"
-#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
+#include "src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h"
+#include "src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h"
#include "src/storage/expressions/TypeCheckVisitor.h"
#include "src/storage/expressions/LinearityCheckVisitor.h"
#include "src/storage/expressions/Expressions.h"
@@ -25,13 +26,17 @@ namespace storm {
}
Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
- return IdentifierSubstitutionVisitor<std::map<std::string, std::string>>(identifierToIdentifierMap).substitute(*this);
+ return IdentifierSubstitutionWithMapVisitor<std::map<std::string, std::string>>(identifierToIdentifierMap).substitute(*this);
}
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);
+ return IdentifierSubstitutionWithMapVisitor<std::unordered_map<std::string, std::string>>(identifierToIdentifierMap).substitute(*this);
}
+ Expression Expression::substitute(SimpleValuation const& valuation) const {
+ return IdentifierSubstitutionWithValuationVisitor(valuation).substitute(*this);
+ }
+
void Expression::check(std::map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const {
return TypeCheckVisitor<std::map<std::string, storm::expressions::ExpressionReturnType>>(identifierToTypeMap).check(*this);
}
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 504e3d96e..ef69fb63a 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -5,6 +5,7 @@
#include <map>
#include <unordered_map>
+#include "src/storage/expressions/SimpleValuation.h"
#include "src/storage/expressions/BaseExpression.h"
#include "src/storage/expressions/ExpressionVisitor.h"
#include "src/utility/OsDetection.h"
@@ -108,6 +109,15 @@ namespace storm {
*/
Expression substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const;
+ /*!
+ * Substitutes all occurrences of identifiers for which the given valuation specifies a concrete value by
+ * the corresponding value.
+ *
+ * @param valuation The valuation that is used to replace the identifiers.
+ * @return The resulting expression.
+ */
+ Expression substitute(SimpleValuation const& valuation) const;
+
/*!
* Checks that all identifiers appearing in the expression have the types given by the map. An exception
* is thrown in case a violation is found.
diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h
index febd7031b..f58617708 100644
--- a/src/storage/expressions/ExpressionEvaluation.h
+++ b/src/storage/expressions/ExpressionEvaluation.h
@@ -157,13 +157,11 @@ namespace expressions {
T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val)
{
- ExpressionEvaluationVisitor<T, typename StateType<T>::type>* visitor = new ExpressionEvaluationVisitor<T, typename StateType<T>::type>(&mState);
- std::cout << expr;
- std::cout.flush();
- expr.getBaseExpression().accept(visitor);
+ ExpressionEvaluationVisitor<T, typename StateType<T>::type>* visitor = new ExpressionEvaluationVisitor<T, typename StateType<T>::type>(&mState);
+ Expression expressionToTranslate = expr.substitute(*val);
+ expressionToTranslate.getBaseExpression().accept(visitor);
T result = visitor->value();
result.simplify();
- std::cout << " -> " << result << std::endl;
delete visitor;
return result;
}
diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitorBase.cpp
similarity index 68%
rename from src/storage/expressions/IdentifierSubstitutionVisitor.cpp
rename to src/storage/expressions/IdentifierSubstitutionVisitorBase.cpp
index 19724dea1..8dcf0b4c8 100644
--- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp
+++ b/src/storage/expressions/IdentifierSubstitutionVisitorBase.cpp
@@ -1,25 +1,16 @@
-#include <map>
-#include <unordered_map>
#include <string>
-#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
+#include "src/storage/expressions/IdentifierSubstitutionVisitorBase.h"
#include "src/storage/expressions/Expressions.h"
namespace storm {
namespace expressions {
- template<typename MapType>
- IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
- // Intentionally left empty.
- }
-
- template<typename MapType>
- Expression IdentifierSubstitutionVisitor<MapType>::substitute(Expression const& expression) {
+ Expression IdentifierSubstitutionVisitorBase::substitute(Expression const& expression) {
expression.getBaseExpression().accept(this);
return Expression(this->expressionStack.top());
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this);
std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top();
expressionStack.pop();
@@ -40,8 +31,7 @@ namespace storm {
}
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(BinaryBooleanFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
expressionStack.pop();
@@ -58,8 +48,7 @@ namespace storm {
}
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(BinaryNumericalFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
expressionStack.pop();
@@ -76,8 +65,7 @@ namespace storm {
}
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(BinaryRelationExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
expressionStack.pop();
@@ -93,20 +81,8 @@ namespace storm {
this->expressionStack.push(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getRelationType())));
}
}
-
- 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());
- if (namePair != this->identifierToIdentifierMap.end()) {
- this->expressionStack.push(std::shared_ptr<BaseExpression>(new VariableExpression(expression->getReturnType(), namePair->second)));
- } else {
- this->expressionStack.push(expression->getSharedPointer());
- }
- }
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(UnaryBooleanFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
expressionStack.pop();
@@ -119,8 +95,7 @@ namespace storm {
}
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(UnaryNumericalFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
expressionStack.pop();
@@ -133,23 +108,16 @@ namespace storm {
}
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(BooleanLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
- template<typename MapType>
- void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
+ void IdentifierSubstitutionVisitorBase::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
-
- // Explicitly instantiate the class with map and 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/IdentifierSubstitutionVisitorBase.h
similarity index 67%
rename from src/storage/expressions/IdentifierSubstitutionVisitor.h
rename to src/storage/expressions/IdentifierSubstitutionVisitorBase.h
index 8e8723a70..5ad3c0e8f 100644
--- a/src/storage/expressions/IdentifierSubstitutionVisitor.h
+++ b/src/storage/expressions/IdentifierSubstitutionVisitorBase.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_
-#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_
+#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITORBASE_H_
+#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITORBASE_H_
#include <stack>
@@ -8,16 +8,8 @@
namespace storm {
namespace expressions {
- template<typename MapType>
- class IdentifierSubstitutionVisitor : public ExpressionVisitor {
+ class IdentifierSubstitutionVisitorBase : public ExpressionVisitor {
public:
- /*!
- * Creates a new substitution visitor that uses the given map to replace identifiers.
- *
- * @param identifierToExpressionMap A mapping from identifiers to expressions.
- */
- IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap);
-
/*!
* Substitutes the identifiers in the given expression according to the previously given map and returns the
* resulting expression.
@@ -32,21 +24,17 @@ namespace storm {
virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
virtual void visit(BinaryRelationExpression const* expression) override;
- virtual void visit(VariableExpression const* expression) override;
virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
virtual void visit(UnaryNumericalFunctionExpression const* expression) override;
virtual void visit(BooleanLiteralExpression const* expression) override;
virtual void visit(IntegerLiteralExpression const* expression) override;
virtual void visit(DoubleLiteralExpression const* expression) override;
- private:
+ protected:
// A stack of expression used to pass the results to the higher levels.
std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
-
- // A mapping of identifier names to expressions with which they shall be replaced.
- MapType const& identifierToIdentifierMap;
};
}
}
-#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITORBASE_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.cpp
new file mode 100644
index 000000000..ff82ffc3f
--- /dev/null
+++ b/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.cpp
@@ -0,0 +1,30 @@
+#include <map>
+#include <unordered_map>
+#include <string>
+
+#include "src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h"
+#include "src/storage/expressions/Expressions.h"
+
+namespace storm {
+ namespace expressions {
+ template<typename MapType>
+ IdentifierSubstitutionWithMapVisitor<MapType>::IdentifierSubstitutionWithMapVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
+ // Intentionally left empty.
+ }
+
+ template<typename MapType>
+ void IdentifierSubstitutionWithMapVisitor<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());
+ if (namePair != this->identifierToIdentifierMap.end()) {
+ this->expressionStack.push(std::shared_ptr<BaseExpression>(new VariableExpression(expression->getReturnType(), namePair->second)));
+ } else {
+ this->expressionStack.push(expression->getSharedPointer());
+ }
+ }
+
+ // Explicitly instantiate the class with map and unordered_map.
+ template class IdentifierSubstitutionWithMapVisitor<std::map<std::string, std::string>>;
+ template class IdentifierSubstitutionWithMapVisitor<std::unordered_map<std::string, std::string>>;
+ }
+}
diff --git a/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h b/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h
new file mode 100644
index 000000000..34a080f8a
--- /dev/null
+++ b/src/storage/expressions/IdentifierSubstitutionWithMapVisitor.h
@@ -0,0 +1,28 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHMAPVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHMAPVISITOR_H_
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/IdentifierSubstitutionVisitorBase.h"
+
+namespace storm {
+ namespace expressions {
+ template<typename MapType>
+ class IdentifierSubstitutionWithMapVisitor : public IdentifierSubstitutionVisitorBase {
+ public:
+ /*!
+ * Creates a new substitution visitor that uses the given map to replace identifiers.
+ *
+ * @param identifierToExpressionMap A mapping from identifiers to expressions.
+ */
+ IdentifierSubstitutionWithMapVisitor(MapType const& identifierToExpressionMap);
+
+ virtual void visit(VariableExpression const* expression) override;
+
+ private:
+ // A mapping of identifier names to expressions with which they shall be replaced.
+ MapType const& identifierToIdentifierMap;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHMAPVISITOR_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.cpp
new file mode 100644
index 000000000..7b6d94b87
--- /dev/null
+++ b/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.cpp
@@ -0,0 +1,37 @@
+#include <map>
+#include <unordered_map>
+#include <string>
+
+#include "src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h"
+#include "src/storage/expressions/Expressions.h"
+
+namespace storm {
+ namespace expressions {
+ IdentifierSubstitutionWithValuationVisitor::IdentifierSubstitutionWithValuationVisitor(Valuation const& valuation) : valuation(valuation) {
+ // Intentionally left empty.
+ }
+
+ void IdentifierSubstitutionWithValuationVisitor::visit(VariableExpression const* expression) {
+ // If the variable is the valuation, we need to replace it.
+ if (expression->getReturnType() == ExpressionReturnType::Bool) {
+ if (valuation.containsBooleanIdentifier(expression->getVariableName())) {
+ this->expressionStack.push(std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(valuation.getBooleanValue(expression->getVariableName()))));
+ } else {
+ this->expressionStack.push(expression->getSharedPointer());
+ }
+ } else if (expression->getReturnType() == ExpressionReturnType::Int) {
+ if (valuation.containsIntegerIdentifier(expression->getVariableName())) {
+ this->expressionStack.push(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(valuation.getIntegerValue(expression->getVariableName()))));
+ } else {
+ this->expressionStack.push(expression->getSharedPointer());
+ }
+ } else if (expression->getReturnType() == ExpressionReturnType::Double) {
+ if (valuation.containsDoubleIdentifier(expression->getVariableName())) {
+ this->expressionStack.push(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(valuation.getDoubleValue(expression->getVariableName()))));
+ } else {
+ this->expressionStack.push(expression->getSharedPointer());
+ }
+ }
+ }
+ }
+}
diff --git a/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h b/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h
new file mode 100644
index 000000000..d27e1e907
--- /dev/null
+++ b/src/storage/expressions/IdentifierSubstitutionWithValuationVisitor.h
@@ -0,0 +1,27 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHVALUATIONVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHVALUATIONVISITOR_H_
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/IdentifierSubstitutionVisitorBase.h"
+
+namespace storm {
+ namespace expressions {
+ class IdentifierSubstitutionWithValuationVisitor : public IdentifierSubstitutionVisitorBase {
+ public:
+ /*!
+ * Creates a new substitution visitor that uses the given map to replace identifiers.
+ *
+ * @param identifierToExpressionMap A mapping from identifiers to expressions.
+ */
+ IdentifierSubstitutionWithValuationVisitor(Valuation const& valuation);
+
+ virtual void visit(VariableExpression const* expression) override;
+
+ private:
+ // A mapping of identifier names to the values with which they shall be replaced.
+ Valuation const& valuation;
+ };
+ }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONWITHVALUATIONVISITOR_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index fccfe2faa..369cea261 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -16,6 +16,8 @@ namespace storm {
friend class SimpleValuationPointerHash;
friend class SimpleValuationPointerLess;
+ typedef boost::container::flat_map<std::string, boost::variant<bool, int_fast64_t, double>> map_type;
+
// Instantiate some constructors and assignments with their default implementations.
SimpleValuation() = default;
SimpleValuation(SimpleValuation const&) = default;
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index 960599577..c92161b8b 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -30,7 +30,11 @@ namespace storm {
}
Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
- return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+ if (!this->isDefined()) {
+ return *this;
+ } else {
+ 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/stormParametric.cpp b/src/stormParametric.cpp
index 917b8505d..7803501f1 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -30,6 +30,8 @@ int main(const int argc, const char** argv) {
std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, constants);
+
+ model->printModelInformationToStream(std::cout);
// Program Translation Time Measurement, End
std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
@@ -37,7 +39,7 @@ int main(const int argc, const char** argv) {
storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelChecker;
storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
- storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1");
+ storm::storage::BitVector targetStates = model->getLabeledStates("target");
// storm::storage::BitVector targetStates = model->getLabeledStates("one");
// storm::storage::BitVector targetStates = model->getLabeledStates("elected");
storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<storm::RationalFunction>>(), trueStates, targetStates);
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 123077957..2a5b8ba86 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -205,27 +205,27 @@ inline storm::storage::LabeledValues<double> constantInfinity() {
/*! @endcond */
template<typename T>
-inline bool isOne(T sum)
+inline bool isOne(T const& sum)
{
return sum == T(1);
}
#ifdef PARAMETRIC_SYSTEMS
template<>
-inline bool isOne(const RationalFunction& r)
+inline bool isOne(storm::RationalFunction const& r)
{
return r.isOne();
}
template<>
-inline bool isOne(const Polynomial& p)
+inline bool isOne(storm::Polynomial const& p)
{
return p.isOne();
}
#endif
template<>
-inline bool isOne(double sum)
+inline bool isOne(double const& sum)
{
double precision = storm::settings::generalSettings().getPrecision();
return std::abs(sum - 1) < precision;