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


	@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] A2			B1 [flag2'=1] B2
	A2 [flag2=0] A3			B2 [flag1'=0] B3
	A3 [turn'=2] A4			B3 [turn'=1] B4
	A4 [flag1'=0] A1			B4 [flag2'=0] B1
	A2 [flag2=1] A5			B2 [flag1=1] B5
	A5 [turn=1] A2			B5 [turn=2] B2
	A5 [turn=2] A6			B5 [turn=1] B6
	A6 [flag1'=0] A7			B6 [flag2'=0] B7
	A7 [turn=2] A7			B7 [turn=1] B7
	A7 [turn=1] A8			B7 [turn=2] B8
	A8 [flag1'=1] A2			B8 [flag2'=1] B2