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

nondeterministic

module abs10000 

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

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