Added some parametrix models. Included percentage of eliminated states to get a feeling for the remaining running time.

Former-commit-id: bad5f32663

examples/pdtmc/brp/brp_64-5.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 = 5;
+
+// 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-2.pm

@@ -0,0 +1,75 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N = 10; // number of inputs in each bundle
+const int K = 2; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+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
+module multiplex
+
+	u : [1..M]; // number of stages
+	c : [0..N]; // counter (number of copies of the nand done)
+
+	s : [0..4]; // local state
+	// 0 - initial state
+	// 1 - set x inputs
+	// 2 - set y inputs
+	// 3 - set outputs
+	// 4 - done
+
+	z : [0..N]; // number of new outputs equal to 1
+	zx : [0..N]; // number of old outputs equal to 1
+	zy : [0..N]; // need second copy for y
+	// initially 9 since initially probability of stimulated state is 0.9
+
+	x : [0..1]; // value of first input
+	y : [0..1]; // value of second input
+	
+	[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+	[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+	[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+	// choose x permute selection (have zx stimulated inputs)
+	// note only need y to be random	
+	[] s=1 & u=1  -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+	[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+	[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+	// choose x randomly from selection (have zy stimulated inputs)
+	[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+	[] s=2 & u>1 & zy<(N-c) & zy>0  -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+	[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+	[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+	// use nand gate
+	[] s=3 & z<N & c<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=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 -> (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;
+endrewards
+

examples/pdtmc/nand/nand_10-3.pm

@@ -0,0 +1,75 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N = 10; // number of inputs in each bundle
+const int K = 3; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+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
+module multiplex
+
+	u : [1..M]; // number of stages
+	c : [0..N]; // counter (number of copies of the nand done)
+
+	s : [0..4]; // local state
+	// 0 - initial state
+	// 1 - set x inputs
+	// 2 - set y inputs
+	// 3 - set outputs
+	// 4 - done
+
+	z : [0..N]; // number of new outputs equal to 1
+	zx : [0..N]; // number of old outputs equal to 1
+	zy : [0..N]; // need second copy for y
+	// initially 9 since initially probability of stimulated state is 0.9
+
+	x : [0..1]; // value of first input
+	y : [0..1]; // value of second input
+	
+	[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+	[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+	[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+	// choose x permute selection (have zx stimulated inputs)
+	// note only need y to be random	
+	[] s=1 & u=1  -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+	[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+	[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+	// choose x randomly from selection (have zy stimulated inputs)
+	[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+	[] s=2 & u>1 & zy<(N-c) & zy>0  -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+	[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+	[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+	// use nand gate
+	[] s=3 & z<N & c<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=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 -> (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;
+endrewards
+

examples/pdtmc/nand/nand_10-4.pm

@@ -0,0 +1,75 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N = 10; // number of inputs in each bundle
+const int K = 4; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+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
+module multiplex
+
+	u : [1..M]; // number of stages
+	c : [0..N]; // counter (number of copies of the nand done)
+
+	s : [0..4]; // local state
+	// 0 - initial state
+	// 1 - set x inputs
+	// 2 - set y inputs
+	// 3 - set outputs
+	// 4 - done
+
+	z : [0..N]; // number of new outputs equal to 1
+	zx : [0..N]; // number of old outputs equal to 1
+	zy : [0..N]; // need second copy for y
+	// initially 9 since initially probability of stimulated state is 0.9
+
+	x : [0..1]; // value of first input
+	y : [0..1]; // value of second input
+	
+	[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+	[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+	[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+	// choose x permute selection (have zx stimulated inputs)
+	// note only need y to be random	
+	[] s=1 & u=1  -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+	[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+	[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+	// choose x randomly from selection (have zy stimulated inputs)
+	[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+	[] s=2 & u>1 & zy<(N-c) & zy>0  -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+	[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+	[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+	// use nand gate
+	[] s=3 & z<N & c<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=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 -> (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;
+endrewards
+

examples/pdtmc/nand/nand_10-5.pm

@@ -0,0 +1,75 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N = 10; // number of inputs in each bundle
+const int K = 5; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+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
+module multiplex
+
+	u : [1..M]; // number of stages
+	c : [0..N]; // counter (number of copies of the nand done)
+
+	s : [0..4]; // local state
+	// 0 - initial state
+	// 1 - set x inputs
+	// 2 - set y inputs
+	// 3 - set outputs
+	// 4 - done
+
+	z : [0..N]; // number of new outputs equal to 1
+	zx : [0..N]; // number of old outputs equal to 1
+	zy : [0..N]; // need second copy for y
+	// initially 9 since initially probability of stimulated state is 0.9
+
+	x : [0..1]; // value of first input
+	y : [0..1]; // value of second input
+	
+	[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+	[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+	[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+	// choose x permute selection (have zx stimulated inputs)
+	// note only need y to be random	
+	[] s=1 & u=1  -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+	[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+	[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+	// choose x randomly from selection (have zy stimulated inputs)
+	[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+	[] s=2 & u>1 & zy<(N-c) & zy>0  -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+	[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+	[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+	// use nand gate
+	[] s=3 & z<N & c<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=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;
+	
+endmodule
+
+label "target" = s=4 & z/N<0.1;
+
+// rewards: final value of gate
+rewards
+	[] s=0 & (c=N) & (u=M) : z/N;
+endrewards
+

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -23,9 +23,7 @@ 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);
             }
             
@@ -64,7 +62,7 @@ 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;
+                std::cout << "Solving parametric 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);
@@ -173,11 +171,19 @@ namespace storm {
                 }
             }
             
+            static int chunkCounter = 0;
             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;
+                
+                ++counter;
+                if (counter > matrix.getNumberOfRows() / 10) {
+                    ++chunkCounter;
+                    std::cout << "Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl;
+                    counter = 0;
+                }
+                
                 bool hasSelfLoop = false;
                 ValueType loopProbability = storm::utility::constantZero<ValueType>();
                 
@@ -422,6 +428,11 @@ namespace storm {
                 return this->data[index];
             }
             
+            template<typename ValueType>
+            typename FlexibleSparseMatrix<ValueType>::index_type FlexibleSparseMatrix<ValueType>::getNumberOfRows() const {
+                return this->data.size();
+            }
+            
             template<typename ValueType>
             FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
                 FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix.getRowCount());
@@ -447,7 +458,7 @@ namespace storm {
             #ifdef PARAMETRIC_SYSTEMS
             template class FlexibleSparseMatrix<RationalFunction>;
             template class SparseSccModelChecker<RationalFunction>;
-            #endif            
+            #endif
         } // namespace reachability
     } // namespace modelchecker
 } // namespace storm

src/modelchecker/reachability/SparseSccModelChecker.h

@@ -20,6 +20,8 @@ namespace storm {
                 
                 row_type& getRow(index_type);
                 
+                index_type getNumberOfRows() const;
+                
             private:
                 std::vector<row_type> data;
             };

src/storage/expressions/ExpressionEvaluation.h

@@ -82,6 +82,7 @@ namespace expressions {
 						mValue *= visitor->value();
 						break;
 					case BinaryNumericalFunctionExpression::OperatorType::Divide:
+                        assert(false);
 						mValue /= visitor->value();
 						break;
 					default:
@@ -124,7 +125,7 @@ namespace expressions {
 			}
             virtual void visit(IntegerLiteralExpression const* expression) 
 			{
-				mValue = T(expression->getValue());
+				mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10));
 			}
             virtual void visit(DoubleLiteralExpression const* expression) 
 			{
@@ -161,7 +162,7 @@ namespace expressions {
             Expression expressionToTranslate = expr.substitute(*val);
 			expressionToTranslate.getBaseExpression().accept(visitor);
 			T result = visitor->value();
-			result.simplify();
+//			result.simplify();
 			delete visitor;
 			return result;
 		}