CFA
     @global
     var flag1, flag2:{0..1} init 0;
     var turn:{1..2} init 1;
     var prcs:{1..2};
 


	@automaton dek1			@automaton dek2
	A1 {@start @label "idle1"}.			B1 {@start @label "idle2"}.
	A2 {@label "trying1"}.			B2 {@label "trying2"}.
	A3 {@label "incs1"}.			B3 {@label "incs2"}.
	A5 {@label "trying1"}.			B5 {@label "trying2"}.
	A6 {@label "trying1"}.			B6 {@label "trying2"}.
	A7 {@label "trying1"}.			B7 {@label "trying2"}.
	A8 {@label "trying1"}.			B8 {@label "trying2"}.
	A1 [flag1'=1 & prcs'=1] A2			B1 [flag2'=1 & prcs'=2] B2
	A2 [flag2=0 & prcs'=1] A3			B2 [flag1=0 & prcs'=2] B3
	A3 [turn'=2 & prcs'=1] A4			B3 [turn'=1 & prcs'=2] B4
	A4 [flag1'=0 & prcs'=1] A1			B4 [flag2'=0 & prcs'=2] B1
	A2 [flag2=1 & prcs'=1] A5			B2 [flag1=1 & prcs'=2] B5
	A5 [turn=1 & prcs'=1] A2			B5 [turn=2 & prcs'=2] B2
	A5 [turn=2 & prcs'=1] A6			B5 [turn=1 & prcs'=2] B6
	A6 [flag1'=0 & prcs'=1] A7			B6 [flag2'=0 & prcs'=2] B7
	A7 [turn=2 & prcs'=1] A7			B7 [turn=1 & prcs'=2] B7
	A7 [turn=1 & prcs'=1] A8			B7 [turn=2 & prcs'=2] B8
	A8 [flag1'=1 & prcs'=1] A2			B8 [flag2'=1 & prcs'=2] B2