//
// This file has been generated with Kappa
//
// -- state encoding: instances
// -- compaction : relative
// -- further compaction: yes

nondeterministic

module abs10000 

tg : [0..11] init 0; 
n : [0..55] init 0;

[] (tg=8)&(n=48..49)| (tg=8)&(n=45)| (tg=8)&(n=42)| (tg=8)&(n=38)-> 1.000000:(tg'=0)&(n'=34) ;
[] (tg=9)&(n=36..55)| (tg=9)&(n=29..34)| (tg=9)&(n=24..26)| (tg=9)&(n=19)-> 1.000000:(tg'=11)&(n'=0) ;
[] (tg=9)&(n=35..55)| (tg=9)&(n=0..33)-> 1.000000:(tg'=10)&(n'=0) ;
[] (tg=6)&(n=1..2)| (tg=7)&(n=1..2)| (tg=8)&(n=1..2)| (tg=5)&(n=3..5)-> 1.000000:(tg'=9)&(n'=n+2) ;
[] (tg=6)&(n=3..5)| (tg=7)&(n=3..5)| (tg=8)&(n=3..5)| (tg=5)&(n=6..9)-> 1.000000:(tg'=9)&(n'=n+3) ;
[] (tg=6)&(n=6..9)| (tg=7)&(n=6..9)| (tg=8)&(n=6..9)| (tg=5)&(n=10..14)-> 1.000000:(tg'=9)&(n'=n+4) ;
[] (tg=6)&(n=10..14)| (tg=7)&(n=10..14)| (tg=8)&(n=10..14)| (tg=5)&(n=15..20)-> 1.000000:(tg'=9)&(n'=n+5) ;
[] (tg=8)&(n=21..26)| (tg=8)&(n=28..31)-> 1.000000:(tg'=0)&(n'=n+8) ;
[] (tg=8)&(n=15..20)| (tg=8)&(n=27)| (tg=5)&(n=21..32)-> 1.000000:(tg'=0)&(n'=n+7) ;
[] (tg=6)&(n=28..32)| (tg=7)&(n=28..32)| (tg=8)&(n=28..32)-> 1.000000:(tg'=9)&(n'=n+8) ;
[] (tg=5)&(n=0)| (tg=5)&(n=33)| (tg=8)&(n=33)-> 1.000000:(tg'=0)&(n'=n+1) ;
[] (tg=6)&(n=0)| (tg=7)&(n=0)| (tg=8)&(n=0)| (tg=5)&(n=1..2)| (tg=6)&(n=33)| (tg=7)&(n=33)| (tg=8)&(n=33)-> 1.000000:(tg'=9)&(n'=n+1) ;
[] (tg=5)&(n=34)| (tg=8)&(n=34)-> 1.000000:(tg'=0) ;
[] (tg=5)&(n=0)| (tg=5)&(n=34)| (tg=6)&(n=34)| (tg=7)&(n=34)| (tg=8)&(n=34)-> 1.000000:(tg'=9) ;
[] (tg=8)&(n=10..14)| (tg=5)&(n=15..20)| (tg=8)&(n=35..37)-> 1.000000:(tg'=0)&(n'=n+6) ;
[] (tg=5)&(n=39)| (tg=8)&(n=39)-> 1.000000:(tg'=0)&(n'=n-5) ;
[] (tg=6)&(n=39)| (tg=7)&(n=39)| (tg=8)&(n=39)-> 1.000000:(tg'=9)&(n'=n-5) ;
[] (tg=8)&(n=6..9)| (tg=5)&(n=10..14)| (tg=5)&(n=35..38)| (tg=8)&(n=40..41)-> 1.000000:(tg'=0)&(n'=n+5) ;
[] (tg=5)&(n=43)| (tg=8)&(n=43)-> 1.000000:(tg'=0)&(n'=n-9) ;
[] (tg=6)&(n=43)| (tg=7)&(n=43)| (tg=8)&(n=43)-> 1.000000:(tg'=9)&(n'=n-9) ;
[] (tg=8)&(n=3..5)| (tg=5)&(n=6..9)| (tg=5)&(n=40..42)| (tg=8)&(n=44)-> 1.000000:(tg'=0)&(n'=n+4) ;
[] (tg=5)&(n=46)| (tg=8)&(n=46)-> 1.000000:(tg'=0)&(n'=n-12) ;
[] (tg=6)&(n=46)| (tg=7)&(n=46)| (tg=8)&(n=46)-> 1.000000:(tg'=9)&(n'=n-12) ;
[] (tg=8)&(n=1..2)| (tg=5)&(n=3..5)| (tg=5)&(n=44..45)| (tg=8)&(n=47)-> 1.000000:(tg'=0)&(n'=n+3) ;
[] (tg=6)&(n=21..27)| (tg=7)&(n=21..27)| (tg=8)&(n=21..27)| (tg=5)&(n=28..33)| (tg=6)&(n=35..38)| (tg=7)&(n=35..38)| (tg=8)&(n=35..38)| (tg=6)&(n=40..42)| (tg=7)&(n=40..42)| (tg=8)&(n=40..42)| (tg=6)&(n=44..45)| (tg=7)&(n=44..45)| (tg=8)&(n=44..45)| (tg=6)&(n=47)| (tg=7)&(n=47)| (tg=8)&(n=47)-> 1.000000:(tg'=9)&(n'=n+7) ;
[] (tg=6)&(n=48)| (tg=7)&(n=48)| (tg=8)&(n=48)-> 1.000000:(tg'=9)&(n'=n-14) ;
[] (tg=8)&(n=0)| (tg=5)&(n=1..2)| (tg=8)&(n=32)| (tg=5)&(n=47..49)-> 1.000000:(tg'=0)&(n'=n+2) ;
[] (tg=6)&(n=15..20)| (tg=7)&(n=15..20)| (tg=8)&(n=15..20)| (tg=5)&(n=21..27)| (tg=5)&(n=35..49)-> 1.000000:(tg'=9)&(n'=n+6) ;
[] (tg=6)&(n=49)| (tg=7)&(n=49)| (tg=8)&(n=49)-> 1.000000:(tg'=9)&(n'=n-15) ;
[] (tg=5)&(n=50)| (tg=8)&(n=50)-> 1.000000:(tg'=0)&(n'=n-16) ;
[] (tg=5)&(n=50)| (tg=6)&(n=50)| (tg=7)&(n=50)| (tg=8)&(n=50)-> 1.000000:(tg'=9)&(n'=n-16) ;
[] (tg=0)&(n=0..51)-> 0.500000:(tg'=1) + 0.500000:(tg'=2) ;
[] (tg=0)&(n=0..51)-> 0.500000:(tg'=3) + 0.500000:(tg'=4) ;
[] (tg=1)&(n=0..51)-> 0.500000:(tg'=5) + 0.500000:(tg'=6) ;
[] (tg=2)&(n=0..51)-> 0.500000:(tg'=7) + 0.500000:(tg'=8) ;
[] (tg=3)&(n=0..51)-> 0.500000:(tg'=5) + 0.500000:(tg'=7) ;
[] (tg=4)&(n=0..51)-> 0.500000:(tg'=6) + 0.500000:(tg'=8) ;
[] (tg=5)&(n=51)| (tg=8)&(n=51)-> 1.000000:(tg'=0)&(n'=n-17) ;
[] (tg=5)&(n=51)| (tg=6)&(n=51)| (tg=7)&(n=51)| (tg=8)&(n=51)-> 1.000000:(tg'=9)&(n'=n-17) ;


endmodule