examples and small fix regarding changes of elimination model checker

Former-commit-id: 2cc4247372

examples/pmdp/firewire/firewire.nm

@@ -0,0 +1,176 @@
+// firewire protocol with integer semantics
+// dxp/gxn 14/06/01
+
+// CLOCKS
+// x1 (x2) clock for node1 (node2)
+// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
+
+mdp
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 85;
+const int rc_fast_min = 76;
+// slow
+const int rc_slow_max = 167;
+const int rc_slow_min = 159;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast
+const double fast1; // = 0.5;
+const double slow1=1-fast1;
+const double fast2; // = 0.5;
+const double slow2=1-fast2;
+
+module wire12
+	
+	// local state
+	w12 : [0..9];
+	// 0 - empty
+	// 1 -	rec_req
+	// 2 -  rec_req_ack
+	// 3 -	rec_ack
+	// 4 -	rec_ack_idle
+	// 5 -	rec_idle
+	// 6 -	rec_idle_req
+	// 7 -	rec_ack_req
+	// 8 -	rec_req_idle
+	// 9 -	rec_idle_ack
+	
+	// clock for wire12
+	y1 : [0..delay+1];
+	y2 : [0..delay+1];
+
+	// empty
+	// do not need y1 and y2 to increase as always reset when this state is left
+	// similarly can reset y1 and y2 when we re-enter this state
+	[snd_req12]  w12=0 -> (w12'=1) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=0 -> (w12'=3) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0);
+	[time]       w12=0 -> (w12'=w12);	
+	// rec_req
+	[snd_req12]  w12=1 -> (w12'=1);
+	[rec_req12]  w12=1 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=1 -> (w12'=2) & (y2'=0);
+	[snd_idle12] w12=1 -> (w12'=8) & (y2'=0);
+	[time]       w12=1 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_ack
+	[snd_ack12] w12=2 -> (w12'=2);
+	[rec_req12] w12=2 -> (w12'=3);
+	[time]      w12=2 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack
+	[snd_ack12]  w12=3 -> (w12'=3);
+	[rec_ack12]  w12=3 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=3 -> (w12'=4) & (y2'=0);
+	[snd_req12]  w12=3 -> (w12'=7) & (y2'=0);
+	[time]       w12=3 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_idle
+	[snd_idle12] w12=4 -> (w12'=4);
+	[rec_ack12]  w12=4 -> (w12'=5);
+	[time]       w12=4 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle
+	[snd_idle12] w12=5 -> (w12'=5);
+	[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_req12]  w12=5 -> (w12'=6) & (y2'=0);
+	[snd_ack12]  w12=5 -> (w12'=9) & (y2'=0);
+	[time]       w12=5 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_req
+	[snd_req12]  w12=6 -> (w12'=6);
+	[rec_idle12] w12=6 -> (w12'=1);
+	[time]       w12=6 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_req
+	[snd_req12] w12=7 -> (w12'=7);
+	[rec_ack12] w12=7 -> (w12'=1);
+	[time]      w12=7 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_idle
+	[snd_idle12] w12=8 -> (w12'=8);
+	[rec_req12]  w12=8 -> (w12'=5);
+	[time]       w12=8 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_ack
+	[snd_ack12]  w12=9 -> (w12'=9);
+	[rec_idle12] w12=9 -> (w12'=3);
+	[time]       w12=9 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	
+endmodule
+
+module node1
+	
+	// clock for node1
+	x1 : [0..168];
+	
+	// local state
+	s1 : [0..8];
+	// 0 - root contention
+	// 1 - rec_idle
+	// 2 - rec_req_fast
+	// 3 - rec_req_slow
+	// 4 - rec_idle_fast
+	// 5 - rec_idle_slow
+	// 6 - snd_req
+	// 7- almost_root
+	// 8 - almost_child
+	
+	// added resets to x1 when not considered again until after rest
+	// removed root and child (using almost root and almost child)
+	
+	// root contention immediate state)
+	[snd_idle12] s1=0 -> fast1 : (s1'=2) & (x1'=0) +  slow1 : (s1'=3) & (x1'=0);
+	[rec_idle21] s1=0 -> (s1'=1);
+	// rec_idle immediate state)
+	[snd_idle12] s1=1 -> fast1 : (s1'=4) & (x1'=0) +  slow1 : (s1'=5) & (x1'=0);
+	[rec_req21]  s1=1 -> (s1'=0);
+	// rec_req_fast
+	[rec_idle21] s1=2 -> (s1'=4);	
+	[snd_ack12]  s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
+	[time]       s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_req_slow
+	[rec_idle21] s1=3 -> (s1'=5);
+	[snd_ack12]  s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
+	[time]       s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// rec_idle_fast
+	[rec_req21] s1=4 -> (s1'=2);
+	[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
+	[time]      s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_idle_slow
+	[rec_req21] s1=5 -> (s1'=3);
+	[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
+	[time]      s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// snd_req 
+	// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1
+	// also can set x1 to 0 upon entering this state
+	[rec_req21] s1=6 -> (s1'=0);
+	[rec_ack21] s1=6 -> (s1'=8);
+	[time]      s1=6 -> (s1'=s1);
+	// almost root (immediate) 
+	// loop in final states to remove deadlock
+	[] s1=7 & s2=8 -> (s1'=s1);
+	[] s1=8 & s2=7 -> (s1'=s1);
+	[time] s1=7 -> (s1'=s1);
+	[time] s1=8 -> (s1'=s1);
+	
+endmodule
+
+// construct remaining automata through renaming
+module wire21=wire12[w12=w21, y1=z1, y2=z2, 
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,
+	rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21]
+endmodule
+module node2=node1[s1=s2, s2=s1, x1=x2, fast1=fast2, slow1=slow2,
+	rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12,
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21]
+endmodule
+
+// labels
+label "done" = (s1=8 & s2=7) | (s1=7 & s2=8);
+
+// reward structures
+
+// time
+rewards "time"	
+	[time] true : 1;
+endrewards
+
+// time nodes sending
+rewards "time_sending"
+	[time] (w12>0 | w21>0) : 1;
+endrewards

examples/pmdp/firewire/firewire.prop

@@ -0,0 +1,4 @@
+Pmin=?[ F (s1=8 & s2=7) ]
+//R{"time"}min=? [ F "done" ]
+//R{"time"}max=? [ F "done" ]
+//R{"time_sending"}max=? [ F "done" ]

examples/pmdp/zeroconf/zeroconf.nm

@@ -0,0 +1,258 @@
+// IPv4: PTA model with digitial clocks
+// one concrete host attempting to choose an ip address 
+// when a number of (abstract) hosts have already got ip addresses
+// gxn/dxp/jzs 02/05/03
+
+// model is an mdp
+mdp
+
+// reset or noreset model
+const bool reset=false;
+
+//-------------------------------------------------------------
+
+// we suppose that
+// - the abstract hosts have already picked their addresses 
+//   and always defend their addresses
+// - the concrete host never picks the same ip address twice 
+//   (this can happen only with a verys small probability)
+
+// under these assumptions we do not need message types because:
+// 1) since messages to the concrete host will never be a probe, 
+//    this host will react to all messages in the same way
+// 2) since the abstract hosts always defend their addresses, 
+//    all messages from the host will get an arp reply if the ip matches
+
+// following from the above assumptions we require only three abstract IP addresses
+// (0,1 and 2) which correspond to the following sets of IP addresses:
+
+// 0 - the IP addresses of the abstract hosts which the concrete host 
+//     previously tried to configure
+// 1 - an IP address of an abstract host which the concrete host is 
+//     currently trying to configure
+// 2 - a fresh IP address which the concrete host is currently trying to configure
+
+// if the host picks an address that is being used it may end up picking another ip address
+// in which case there may still be messages corresponding to the old ip address
+// to be sent both from and to the host which the host should now disregard
+// (since it will never pick the same ip address)
+
+// to deal with this situation: when a host picks a new ip address we reconfigure the 
+// messages that are still be be sent or are being sent by changing the ip address to 0 
+// (an old ip address of the host)
+
+// all the messages from the abstract hosts for the 'old' address (in fact the
+// set of old addresses since it may have started again more than once)  
+// can arrive in any order since they are equivalent to the host - it ignores then all
+
+// also the messages for the old and new address will come from different hosts
+// (the ones with that ip address) which we model by allowing them to arrive in any order
+// i.e. not neccessarily in the order they where sent
+
+//-------------------------------------------------------------
+
+
+//-------------------------------------------------------------
+// VARIABLES
+//const int N; // number of abstract hosts
+const int K; // number of probes to send
+const double loss; // probability of message loss
+
+// PROBABILITIES
+const double old; //=N/65024; // probability pick an ip address being used
+const double new = (1-old); // probability pick a new ip address
+
+// TIMING CONSTANTS
+const int CONSEC = 2;  // time interval between sending consecutive probles 
+const int TRANSTIME = 1; // upper bound on transmission time delay
+const int LONGWAIT = 60; // minimum time delay after a high number of address collisions
+const int DEFEND = 10;
+
+const int TIME_MAX_X = 60; // max value of clock x
+const int TIME_MAX_Y = 10; // max value of clock y
+const int TIME_MAX_Z = 1;  // max value of clock z
+
+// OTHER CONSTANTS
+const int MAXCOLL = 10;  // maximum number of collisions before long wait
+// size of buffers for other hosts
+const int B0 = 20;  // buffer size for one abstract host
+const int B1 = 8;  // buffer sizes for all abstract hosts
+
+//-------------------------------------------------------------
+// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
+module environment
+	
+	// buffer of concrete host
+	b_ip7 : [0..2]; // ip address of message in buffer position 8
+	b_ip6 : [0..2]; // ip address of message in buffer position 7
+	b_ip5 : [0..2]; // ip address of message in buffer position 6
+	b_ip4 : [0..2]; // ip address of message in buffer position 5
+	b_ip3 : [0..2]; // ip address of message in buffer position 4
+	b_ip2 : [0..2]; // ip address of message in buffer position 3
+	b_ip1 : [0..2]; // ip address of message in buffer position 2
+	b_ip0 : [0..2]; // ip address of message in buffer position 1
+	n : [0..8]; // number of places in the buffer used (from host)
+	
+	// messages to be sent from abstract hosts to concrete host
+	n0  : [0..B0]; // number of messages which do not have the host's current ip address
+	n1  : [0..B1]; // number of messages which have the host's current ip address
+	
+	b : [0..2]; // local state
+	// 0 - idle
+	// 1 - sending message from concrete host 
+	// 2 - sending message from abstract host
+	
+	z : [0..1]; // clock of environment (needed for the time to send a message)
+	
+	ip_mess : [0..2]; // ip in the current message being sent
+	// 0 - different from concrete host
+	// 1 - same as the concrete host and in use
+	// 2 - same as the concrete host and not in use
+	
+	// RESET/RECONFIG: when host is about to choose new ip address
+	// suppose that the host cannot choose the same ip address
+	// (since happens with very small probability). 
+	// Therefore all messages will have a different ip address, 
+	// i.e. all n1 messages become n0 ones.
+	// Note this include any message currently being sent (ip is set to zero 0)
+	[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers 
+	               & (ip_mess'=0) // message being set
+	               & (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model)
+	               & (b_ip7'=0) 
+	               & (b_ip6'=0) 
+	               & (b_ip5'=0) 
+	               & (b_ip4'=0) 
+	               & (b_ip3'=0) 
+	               & (b_ip2'=0) 
+	               & (b_ip1'=0) 
+	               & (b_ip0'=0);
+	// note: prevent anything else from happening when reconfiguration needs to take place
+	
+	// time passage (only if no messages to send or sending a message)
+	[time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message
+	[time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message
+	
+	// get messages to be sent (so message has same ip address as host)
+	[send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1);
+	[send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1);
+	[send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1);
+	[send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1);
+	[send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1);
+	[send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1);
+	[send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1);
+	[send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1);
+	[send] l>0 & n=8 -> (n'=n); // buffer full so lose message
+	
+	// start sending message from host
+	[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) 
+	                                & (n'=n-1)
+	                                & (b_ip7'=0) 
+	                                & (b_ip6'=b_ip7) 
+	                                & (b_ip5'=b_ip6) 
+	                                & (b_ip4'=b_ip5) 
+	                                & (b_ip3'=b_ip4) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1) // send message
+	                         + loss : (n'=n-1)
+	                                & (b_ip7'=0) 
+	                                & (b_ip6'=b_ip7) 
+	                                & (b_ip5'=b_ip6) 
+	                                & (b_ip4'=b_ip5) 
+	                                & (b_ip3'=b_ip4) 
+	                                & (b_ip2'=b_ip3) 
+	                                & (b_ip1'=b_ip2) 
+	                                & (b_ip0'=b_ip1); // lose message
+	
+	// start sending message to host
+	[] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
+	[] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
+	
+	// finish sending message from host
+	[] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
+	[] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
+	[] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+	// finish sending message to host
+	[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
+	
+endmodule
+
+//-------------------------------------------------------------
+// CONCRETE HOST
+module host0
+	
+	x : [0..TIME_MAX_X]; // first clock of the host
+	y : [0..TIME_MAX_Y]; // second clock of the host
+	
+	coll : [0..MAXCOLL]; // number of address collisions
+	probes : [0..K]; // counter (number of probes sent)
+	mess : [0..1]; // need to send a message or not
+	defend : [0..1]; // defend (if =1, try to defend IP address)
+	
+	ip : [1..2]; // ip address (1 - in use & 2 - fresh)
+	
+	l : [0..4] init 1; // location
+	// 0 : RECONFIGURE 
+	// 1 : RANDOM
+	// 2 : WAITSP
+	// 3 : WAITSG 
+	// 4 : USE
+	
+	// RECONFIGURE
+	[reset] l=0 -> (l'=1);
+	
+	// RANDOM (choose IP address)
+	[rec] (l=1) -> 1: true; // get message (ignore since have no ip address)
+	// small number of collisions (choose straight away)
+	[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) 
+		                     + 1/3*old : (l'=2) & (ip'=1) & (x'=1) 
+		                     + 1/3*old : (l'=2) & (ip'=1) & (x'=2) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=0) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=1) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=2); 
+	// large number of collisions: (wait for LONGWAIT)
+	[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X));
+	[]     l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) 
+			                                   + 1/3*old : (l'=2) & (ip'=1) & (x'=1) 
+			                                   + 1/3*old : (l'=2) & (ip'=1) & (x'=2) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=0) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=1) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=2);
+	
+	// WAITSP 
+	// let time pass
+	[time]  l=2 & x<2 -> (x'=min(x+1,2));
+	// send probe
+	[send] l=2 & x=2  & probes<K -> (x'=0) & (probes'=probes+1);
+	// sent K probes and waited 2 seconds
+	[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
+	// get message and ip does not match: ignore
+	[rec] l=2 & ip_mess!=ip -> (l'=l);
+	// get a message with matching ip: reconfigure
+	[rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	
+	// WAITSG (sends two gratuitious arp probes)
+	// time passage
+	[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); 
+	[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND));
+	
+	// receive message and same ip: defend
+	[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	// receive message and same ip: defer
+	[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	// receive message and different ip
+	[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l);
+	
+		
+	// send probe reply or message for defence
+	[send] l=3 & mess=1 -> (mess'=0);
+	// send first gratuitous arp message
+	[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
+	// send second gratuitous arp message (move to use)
+	[send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
+	
+	// USE (only interested in reaching this state so do not need to add anything here)
+	[] l=4 -> 1 : true;
+	
+endmodule

examples/pmdp/zeroconf/zeroconf.prop

@@ -0,0 +1,2 @@
+Pmin=? [ F (l=4 & ip=1) ]
+Pmax=? [ F (l=4 & ip=1) ]

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -9,8 +9,17 @@
 namespace storm {
     namespace modelchecker {
         
+        //forward declaration of friend class
+        namespace region {
+            template<typename ParametricModelType, typename ConstantType>
+            class SparseDtmcRegionModelChecker;
+        }
+        
         template<typename SparseDtmcModelType>
         class SparseDtmcEliminationModelChecker : public SparsePropositionalModelChecker<SparseDtmcModelType> {
+            
+            template<typename ParametricModelType, typename ConstantType> friend class storm::modelchecker::region::SparseDtmcRegionModelChecker;
+            
         public:
             typedef typename SparseDtmcModelType::ValueType ValueType;
             typedef typename SparseDtmcModelType::RewardModelType RewardModelType;

src/modelchecker/region/SparseDtmcRegionModelChecker.cpp

@@ -402,16 +402,18 @@ namespace storm {
                 //now compute the functions using methods from elimination model checker
                 storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates;
                 storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true);
-                boost::optional<std::vector<ParametricType>> stateRewards;
+                std::vector<ParametricType> values;
                 if(this->isComputeRewards()){
-                    stateRewards = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates);
+                    values = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates);
+                } else {
+                    values = oneStepProbabilities;
                 }
 //                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>> eliminationModelChecker(simpleModel);
 //                std::vector<std::size_t> statePriorities = eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities);
 //                this->reachabilityFunction=std::make_shared<ParametricType>(eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), stateRewards, statePriorities));
-	    //      std::vector<ParametricType> reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>>::computeReachabilityValues(
-	 //                   forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), oneStepProbabilities);
-		//  this->reachabilityFunction=std::make_shared<ParametricType>(std::move(reachFuncVector[*newInitialStates.begin()]));
+	          std::vector<ParametricType> reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>>::computeReachabilityValues(
+	                    forwardTransitions, values, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), oneStepProbabilities);
+		  this->reachabilityFunction=std::make_shared<ParametricType>(std::move(reachFuncVector[*simpleModel.getInitialStates().begin()]));
                    /* std::string funcStr = " (/ " +
                                     this->reachabilityFunction->nominator().toString(false, true) + " " +
                                     this->reachabilityFunction->denominator().toString(false, true) +