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