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: a863a07261

examples/pdtmc/brp/brp_2_16.pm → 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;

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;

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;

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;

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());

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>();
                 

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,11 +26,15 @@ 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 {

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.

src/storage/expressions/ExpressionEvaluation.h

@@ -158,12 +158,10 @@ 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);
+            Expression expressionToTranslate = expr.substitute(*val);
+			expressionToTranslate.getBaseExpression().accept(visitor);
 			T result = visitor->value();
 			result.simplify();
-			std::cout << " -> " << result << std::endl;
 			delete visitor;
 			return result;
 		}

src/storage/expressions/IdentifierSubstitutionVisitor.cpp → 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();
@@ -94,19 +82,7 @@ namespace storm {
             }
         }
         
-        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> >;
     }
 }

src/storage/expressions/IdentifierSubstitutionVisitor.h → 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_ */
+#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITORBASE_H_ */

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>>;
+    }
+}

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_ */

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());
+                }
+            }
+        }
+    }
+}

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_ */

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;

src/storage/prism/Constant.cpp

@@ -30,8 +30,12 @@ namespace storm {
         }
         
         Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            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) {
             stream << "const ";

src/stormParametric.cpp

@@ -31,13 +31,15 @@ int main(const int argc, const char** argv) {
         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();
         std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
 
         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);

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;