// region graph model of abstract firewire protocol
// dxp/gxn 29/05/2001

mdp

// CONSTANTS
const int delay; // wire delay
const double fast; // probability of choosing fast
const double slow=1-fast; // probability of choosing slow

// INDEPENDENT VARIABLES
// x1 : [0...n1]
// x2 : [0..1]
// if x1 =i and x2=0, then x=i
// if x1 =i and x2=1, then x=(i,i+1)

// SUCCESSOR TRANSITIONS
// x2=0, then move to x2'=1
// x2=1, then move to x1'=x1+1 and  x2'=0

module process

x1 : [0..167];
x2 : [0..1];

s : [0..10];
// 0 -start_start
// 1 -fast_start
// 2 -start_fast
// 3 -start_slow
// 4 -slow_start
// 5 -fast_fast
// 6 -fast_slow
// 7 -slow_fast
// 8 -slow_slow
// 9 -done

// successor transitions for states 0 up to 4 (all have same invariant)
[] s<=4 & (x1<delay) & (x2=0) -> (x2'=1);
[] s<=4 & (x1<delay) & (x2=1) -> (x1'=x1+1) & (x2'=0);
// flip coins
[] s=0 -> fast : (s'=1) + slow : (s'=4); // start_start
[] s=0 -> fast : (s'=2) + slow : (s'=3); // start_start
[] s=1 -> fast : (s'=5) & (x1'=0) & (x2'=0) + slow : (s'=6) & (x1'=0) & (x2'=0); // fast_start
[] s=2 -> fast : (s'=5) & (x1'=0) & (x2'=0) + slow : (s'=7) & (x1'=0) & (x2'=0); // start_fast
[] s=3 -> fast : (s'=6) & (x1'=0) & (x2'=0) + slow : (s'=8) & (x1'=0) & (x2'=0); // start_slow
[] s=4 -> fast : (s'=7) & (x1'=0) & (x2'=0) + slow : (s'=8) & (x1'=0) & (x2'=0); // slow_start
// fast_fast
[] s=5 & x1<85 & x2=0 -> (x2'=1);
[] s=5 & x1<85 & x2=1 -> (x1'=x1+1) & (x2'=0);
[] s=5 & x1>=76 -> (s'=0) & (x1'=0) & (x2'=0);
[] (s=5) & (x1>=76-delay) -> (s'=9) & (x1'=0) & (x2'=0);
// fast_slow
[] s=6 & x1<167 & x2=0 -> (x2'=1);
[] s=6 & x1<167 & x2=1 -> (x1'=x1+1) & (x2'=0);
[] (s=6) & (x1>=159-delay) -> (s'=9) & (x1'=0) & (x2'=0);
// slow_fast
[] s=7 & x1<167 & x2=0 -> (x2'=1);
[] s=7 & x1<167 & x2=1 -> (x1'=x1+1) & (x2'=0);
[] (s=7) & (x1>=159-delay) -> (s'=9) & (x1'=0) & (x2'=0);
// slow_slow
[] s=8 & x1<167 & x2=0 -> (x2'=1);
[] s=8 & x1<167 & x2=1 -> (x1'=x1+1) & (x2'=0);
[] s=8 & x1>=159 -> (s'=0) & (x1'=0) & (x2'=0);
[] (s=8) & (x1>=159-delay) -> (s'=9) & (x1'=0) & (x2'=0);
// done
[] s=9 -> (s'=9);

endmodule