// Testfile dumped by Ultimate at 2012/01/05 14:34:51 assert(isEmpty(net)); print(net); PetriNet net = ( alphabet = {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a16 a15 a17 a18 a19 a20 a21 a22 a23 }, places = {p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39 p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 }, transitions = { ( {p50 p10 p6 p18 p45 p40 p41 } a21 {p26 p10 p6 p18 p45 p40 p41 } ) ( {p25 p38 p35 p6 p18 p9 p41 } a6 {p32 p24 p29 p6 p18 p9 p41 } ) ( {p32 p35 p0 p6 p33 p44 p41 } a16 {p23 p35 p19 p10 p33 p39 p40 } ) ( {p47 p1 p48 p45 } a9 {p52 p1 p42 p43 } ) ( {p53 p37 p29 p19 p10 p34 p33 p39 p40 } a4 {p36 p5 p29 p0 p6 p11 p9 p44 p41 } ) ( {p23 p38 p35 p19 p10 p9 p41 } a5 {p50 p24 p29 p0 p6 p9 p41 } ) ( {p53 p37 p38 p35 p6 p18 p34 p33 p39 p40 } a4 {p36 p5 p24 p29 p6 p18 p11 p9 p44 p41 } ) ( {p52 p18 p12 p40 p41 } a13 {p30 p18 p12 p40 p41 } ) ( {p23 p29 p8 p10 p9 p39 p40 } a5 {p50 p29 p0 p18 p9 p44 p41 } ) ( {p53 p37 p29 p6 p18 p9 p39 p40 } a4 {p36 p5 p29 p6 p18 p9 p44 p41 } ) ( {p53 p37 p29 p8 p10 p34 p33 p41 } a4 {p36 p5 p29 p0 p18 p11 p9 p41 } ) ( {p49 p19 p18 p34 p12 p42 p40 } a18 {p17 p8 p6 p13 p9 p44 p45 } ) ( {p50 p19 p1 p44 p43 } a21 {p26 p2 p6 p48 p40 } ) ( {p50 p19 p1 p42 p43 } a21 {p26 p2 p6 p48 p45 } ) ( {p23 p38 p35 p8 p10 p9 p41 } a5 {p50 p24 p29 p0 p18 p9 p41 } ) ( {p23 p38 p35 p8 p10 p9 p39 p40 } a5 {p50 p24 p29 p0 p18 p9 p44 p41 } ) ( {p27 } a17 {p31 } ) ( {p23 p38 p35 p19 p10 p9 p39 p40 } a5 {p50 p24 p29 p0 p6 p9 p44 p41 } ) ( {p23 p29 p19 p10 p9 p39 p40 } a5 {p50 p29 p0 p6 p9 p44 p41 } ) ( {p23 p29 p6 p18 p9 p39 p40 } a5 {p50 p29 p6 p18 p9 p44 p41 } ) ( {p20 p38 p35 p19 p10 p34 p33 p41 } a2 {p28 p24 p29 p0 p6 p11 p9 p41 } ) ( {p20 p29 p19 p10 p34 p33 p39 p40 } a2 {p28 p29 p0 p6 p11 p9 p44 p41 } ) ( {p51 p38 p35 p6 p18 p9 p41 } a1 {p3 p24 p29 p6 p18 p9 p41 } ) ( {p51 p35 } a23 {p4 p35 } ) ( {p3 p35 p10 p11 p9 p40 } a10 {p20 p35 p10 p34 p33 p40 } ) ( {p32 p35 p0 p6 p11 p9 p44 p41 } a16 {p23 p35 p19 p10 p34 p33 p39 p40 } ) ( {p52 p18 p13 p33 p40 p41 } a13 {p30 p18 p11 p12 p40 p41 } ) ( {p23 p29 p6 p18 p9 p41 } a5 {p50 p29 p6 p18 p9 p41 } ) ( {p32 p24 p29 p10 p11 p9 p40 } a16 {p23 p38 p35 p10 p34 p33 p40 } ) ( {p3 p24 p29 p0 p6 p11 p9 p44 p41 } a10 {p20 p38 p35 p19 p10 p34 p33 p39 p40 } ) ( {p53 p37 p38 p35 p6 p18 p9 p41 } a4 {p36 p5 p24 p29 p6 p18 p9 p41 } ) ( {p32 p24 p29 p10 p33 p40 } a16 {p23 p38 p35 p10 p33 p40 } ) ( {p50 p8 p1 p42 p43 } a21 {p26 p2 p18 p48 p45 } ) ( {p3 p35 p0 p6 p33 p40 } a10 {p20 p35 p19 p10 p33 p40 } ) ( {p20 p38 p35 p6 p18 p34 p33 p39 p40 } a2 {p28 p24 p29 p6 p18 p11 p9 p44 p41 } ) ( {p32 p35 p0 p6 p33 p40 } a16 {p23 p35 p19 p10 p33 p40 } ) ( {p23 p38 p35 p19 p10 p34 p33 p41 } a5 {p50 p24 p29 p0 p6 p11 p9 p41 } ) ( {p49 p6 p33 p9 p42 p40 } a18 {p17 p6 p33 p9 p44 p45 } ) ( {p53 p37 p29 p19 p10 p34 p33 p41 } a4 {p36 p5 p29 p0 p6 p11 p9 p41 } ) ( {p3 p35 p0 p6 p11 p9 p44 p41 } a10 {p20 p35 p19 p10 p34 p33 p39 p40 } ) ( {p53 p37 p38 p35 p8 p10 p34 p33 p39 p40 } a4 {p36 p5 p24 p29 p0 p18 p11 p9 p44 p41 } ) ( {p32 p24 p29 p0 p6 p33 p44 p41 } a16 {p23 p38 p35 p19 p10 p33 p39 p40 } ) ( {p23 p38 p35 p6 p18 p9 p39 p40 } a5 {p50 p24 p29 p6 p18 p9 p44 p41 } ) ( {p3 p35 p0 p6 p11 p9 p40 } a10 {p20 p35 p19 p10 p34 p33 p40 } ) ( {p52 p18 p13 p33 p39 p45 } a13 {p30 p18 p11 p12 p42 p41 } ) ( {p52 p18 p12 p39 p45 } a13 {p30 p18 p12 p42 p41 } ) ( {p15 p7 p12 } a12 {p49 p13 p14 } ) ( {p23 p29 p6 p18 p34 p33 p39 p40 } a5 {p50 p29 p6 p18 p11 p9 p44 p41 } ) ( {p49 p6 p33 p9 p45 } a18 {p17 p6 p33 p9 p45 } ) ( {p53 p37 p29 p19 p10 p9 p39 p40 } a4 {p36 p5 p29 p0 p6 p9 p44 p41 } ) ( {p16 } a14 {p15 } ) ( {p3 p24 p29 p0 p6 p33 p40 } a10 {p20 p38 p35 p19 p10 p33 p40 } ) ( {p20 p38 p35 p19 p10 p9 p41 } a2 {p28 p24 p29 p0 p6 p9 p41 } ) ( {p52 p8 p6 p13 p33 p44 p45 } a13 {p30 p19 p18 p11 p12 p42 p40 } ) ( {p32 p35 p10 p11 p9 p44 p41 } a16 {p23 p35 p10 p34 p33 p39 p40 } ) ( {p20 p29 p8 p10 p34 p33 p39 p40 } a2 {p28 p29 p0 p18 p11 p9 p44 p41 } ) ( {p49 p6 p11 p12 p42 p40 } a18 {p17 p6 p13 p33 p44 p45 } ) ( {p25 p29 p6 p18 p9 p41 } a6 {p32 p29 p6 p18 p9 p41 } ) ( {p30 p33 p9 } a11 {p25 p33 p9 } ) ( {p32 p24 p29 p0 p6 p11 p9 p44 p41 } a16 {p23 p38 p35 p19 p10 p34 p33 p39 p40 } ) ( {p28 p13 p14 } a20 {p16 p7 p12 } ) ( {p49 p19 p18 p11 p12 p45 } a18 {p17 p8 p6 p13 p33 p45 } ) ( {p20 p38 p35 p19 p10 p34 p33 p39 p40 } a2 {p28 p24 p29 p0 p6 p11 p9 p44 p41 } ) ( {p53 p37 p38 p35 p19 p10 p9 p39 p40 } a4 {p36 p5 p24 p29 p0 p6 p9 p44 p41 } ) ( {p20 p38 p35 p8 p10 p9 p41 } a2 {p28 p24 p29 p0 p18 p9 p41 } ) ( {p50 p0 p1 p44 p43 } a21 {p26 p2 p10 p48 p40 } ) ( {p49 p6 p11 p12 p45 } a18 {p17 p6 p13 p33 p45 } ) ( {p50 p10 p6 p18 p44 p43 } a21 {p26 p10 p6 p18 p48 p40 } ) ( {p20 p38 p35 p6 p18 p34 p33 p41 } a2 {p28 p24 p29 p6 p18 p11 p9 p41 } ) ( {p20 p29 p6 p18 p9 p39 p40 } a2 {p28 p29 p6 p18 p9 p44 p41 } ) ( {p47 p2 p10 p43 } a9 {p52 p0 p1 p43 } ) ( {p20 p38 p35 p6 p18 p9 p41 } a2 {p28 p24 p29 p6 p18 p9 p41 } ) ( {p32 p24 p29 p10 p33 p44 p41 } a16 {p23 p38 p35 p10 p33 p39 p40 } ) ( {p23 p29 p6 p18 p34 p33 p41 } a5 {p50 p29 p6 p18 p11 p9 p41 } ) ( {p20 p29 p6 p18 p34 p33 p39 p40 } a2 {p28 p29 p6 p18 p11 p9 p44 p41 } ) ( {p28 p11 p14 } a20 {p16 p7 p33 } ) ( {p20 p29 p8 p10 p9 p39 p40 } a2 {p28 p29 p0 p18 p9 p44 p41 } ) ( {p50 p0 p1 p42 p43 } a21 {p26 p2 p10 p48 p45 } ) ( {p20 p38 p35 p6 p18 p9 p39 p40 } a2 {p28 p24 p29 p6 p18 p9 p44 p41 } ) ( {p3 p35 p10 p33 p44 p41 } a10 {p20 p35 p10 p33 p39 p40 } ) ( {p23 p38 p35 p6 p18 p34 p33 p41 } a5 {p50 p24 p29 p6 p18 p11 p9 p41 } ) ( {p3 p35 p0 p6 p33 p44 p41 } a10 {p20 p35 p19 p10 p33 p39 p40 } ) ( {p20 p29 p19 p10 p34 p33 p41 } a2 {p28 p29 p0 p6 p11 p9 p41 } ) ( {p50 p8 p1 p45 p40 p41 } a21 {p26 p2 p18 p45 p40 p41 } ) ( {p23 p38 p35 p6 p18 p9 p41 } a5 {p50 p24 p29 p6 p18 p9 p41 } ) ( {p53 p37 p38 p35 p6 p18 p9 p39 p40 } a4 {p36 p5 p24 p29 p6 p18 p9 p44 p41 } ) ( {p23 p38 p35 p8 p10 p34 p33 p41 } a5 {p50 p24 p29 p0 p18 p11 p9 p41 } ) ( {p3 p24 p29 p10 p11 p9 p40 } a10 {p20 p38 p35 p10 p34 p33 p40 } ) ( {p53 p37 p38 p35 p19 p10 p34 p33 p39 p40 } a4 {p36 p5 p24 p29 p0 p6 p11 p9 p44 p41 } ) ( {p50 p19 p1 p39 p43 } a21 {p26 p2 p6 p48 p41 } ) ( {p50 p19 p1 p45 p40 p41 } a21 {p26 p2 p6 p45 p40 p41 } ) ( {p3 p24 p29 p10 p11 p9 p44 p41 } a10 {p20 p38 p35 p10 p34 p33 p39 p40 } ) ( {p53 p37 p29 p8 p10 p9 p41 } a4 {p36 p5 p29 p0 p18 p9 p41 } ) ( {p51 p29 p6 p18 p9 p41 } a1 {p3 p29 p6 p18 p9 p41 } ) ( {p25 p35 } a8 {p46 p35 } ) ( {p23 p29 p19 p10 p34 p33 p39 p40 } a5 {p50 p29 p0 p6 p11 p9 p44 p41 } ) ( {p32 p24 p29 p0 p6 p33 p40 } a16 {p23 p38 p35 p19 p10 p33 p40 } ) ( {p23 p38 p35 p19 p10 p34 p33 p39 p40 } a5 {p50 p24 p29 p0 p6 p11 p9 p44 p41 } ) ( {p49 p19 p18 p11 p12 p42 p40 } a18 {p17 p8 p6 p13 p33 p44 p45 } ) ( {p3 p35 p10 p33 p40 } a10 {p20 p35 p10 p33 p40 } ) ( {p50 p0 p1 p39 p43 } a21 {p26 p2 p10 p48 p41 } ) ( {p49 p6 p34 p12 p45 } a18 {p17 p6 p13 p9 p45 } ) ( {p53 p37 p38 p35 p8 p10 p34 p33 p41 } a4 {p36 p5 p24 p29 p0 p18 p11 p9 p41 } ) ( {p52 p8 p6 p13 p33 p39 p45 } a13 {p30 p19 p18 p11 p12 p42 p41 } ) ( {p20 p29 p8 p10 p9 p41 } a2 {p28 p29 p0 p18 p9 p41 } ) ( {p32 p35 p10 p11 p9 p40 } a16 {p23 p35 p10 p34 p33 p40 } ) ( {p3 p24 p29 p10 p33 p40 } a10 {p20 p38 p35 p10 p33 p40 } ) ( {p53 p37 p38 p35 p6 p18 p34 p33 p41 } a4 {p36 p5 p24 p29 p6 p18 p11 p9 p41 } ) ( {p53 p37 p29 p8 p10 p34 p33 p39 p40 } a4 {p36 p5 p29 p0 p18 p11 p9 p44 p41 } ) ( {p23 p38 p35 p6 p18 p34 p33 p39 p40 } a5 {p50 p24 p29 p6 p18 p11 p9 p44 p41 } ) ( {p20 p38 p35 p8 p10 p9 p39 p40 } a2 {p28 p24 p29 p0 p18 p9 p44 p41 } ) ( {p53 p37 p29 p6 p18 p34 p33 p41 } a4 {p36 p5 p29 p6 p18 p11 p9 p41 } ) ( {p47 p2 p10 p48 p45 } a9 {p52 p0 p1 p42 p43 } ) ( {p20 p29 p19 p10 p9 p41 } a2 {p28 p29 p0 p6 p9 p41 } ) ( {p50 p8 p1 p44 p43 } a21 {p26 p2 p18 p48 p40 } ) ( {p20 p29 p19 p10 p9 p39 p40 } a2 {p28 p29 p0 p6 p9 p44 p41 } ) ( {p3 p24 p29 p0 p6 p11 p9 p40 } a10 {p20 p38 p35 p19 p10 p34 p33 p40 } ) ( {p26 p29 p35 p10 p6 p1 p18 p12 p33 p14 p9 p45 p40 p43 p41 } a3 {p27 p29 p35 p10 p6 p1 p18 p12 p33 p14 p9 p45 p40 p43 p41 } ) ( {p53 p37 p29 p19 p10 p9 p41 } a4 {p36 p5 p29 p0 p6 p9 p41 } ) ( {p23 p29 p8 p10 p34 p33 p41 } a5 {p50 p29 p0 p18 p11 p9 p41 } ) ( {p15 p14 } a12 {p49 p14 } ) ( {p32 p24 p29 p10 p11 p9 p44 p41 } a16 {p23 p38 p35 p10 p34 p33 p39 p40 } ) ( {p23 p38 p35 p8 p10 p34 p33 p39 p40 } a5 {p50 p24 p29 p0 p18 p11 p9 p44 p41 } ) ( {p36 p5 } a0 {p26 p16 } ) ( {p52 p8 p6 p12 p39 p45 } a13 {p30 p19 p18 p12 p42 p41 } ) ( {p3 p24 p29 p0 p6 p33 p44 p41 } a10 {p20 p38 p35 p19 p10 p33 p39 p40 } ) ( {p52 p8 p6 p12 p44 p45 } a13 {p30 p19 p18 p12 p42 p40 } ) ( {p23 p29 p8 p10 p34 p33 p39 p40 } a5 {p50 p29 p0 p18 p11 p9 p44 p41 } ) ( {p49 p19 p18 p34 p12 p45 } a18 {p17 p8 p6 p13 p9 p45 } ) ( {p20 p29 p6 p18 p34 p33 p41 } a2 {p28 p29 p6 p18 p11 p9 p41 } ) ( {p22 } a15 {p21 } ) ( {p23 p29 p19 p10 p9 p41 } a5 {p50 p29 p0 p6 p9 p41 } ) ( {p20 p29 p6 p18 p9 p41 } a2 {p28 p29 p6 p18 p9 p41 } ) ( {p17 p18 p40 p41 } a22 {p51 p18 p40 p41 } ) ( {p53 p37 p38 p35 p19 p10 p34 p33 p41 } a4 {p36 p5 p24 p29 p0 p6 p11 p9 p41 } ) ( {p26 } a19 {p47 } ) ( {p52 p18 p13 p33 p44 p45 } a13 {p30 p18 p11 p12 p42 p40 } ) ( {p16 p29 p35 p10 p6 p1 p18 p12 p33 p14 p9 p45 p40 p43 p41 } a7 {p22 p29 p35 p10 p6 p1 p18 p12 p33 p14 p9 p45 p40 p43 p41 } ) ( {p53 p37 p38 p35 p19 p10 p9 p41 } a4 {p36 p5 p24 p29 p0 p6 p9 p41 } ) ( {p28 p34 p14 } a20 {p16 p7 p9 } ) ( {p32 p35 p0 p6 p11 p9 p40 } a16 {p23 p35 p19 p10 p34 p33 p40 } ) ( {p3 p24 p29 p10 p33 p44 p41 } a10 {p20 p38 p35 p10 p33 p39 p40 } ) ( {p50 p8 p1 p39 p43 } a21 {p26 p2 p18 p48 p41 } ) ( {p50 p10 p6 p18 p39 p43 } a21 {p26 p10 p6 p18 p48 p41 } ) ( {p49 p6 p34 p12 p42 p40 } a18 {p17 p6 p13 p9 p44 p45 } ) ( {p50 p0 p1 p45 p40 p41 } a21 {p26 p2 p10 p45 p40 p41 } ) ( {p20 p38 p35 p8 p10 p34 p33 p39 p40 } a2 {p28 p24 p29 p0 p18 p11 p9 p44 p41 } ) ( {p53 p37 p29 p6 p18 p34 p33 p39 p40 } a4 {p36 p5 p29 p6 p18 p11 p9 p44 p41 } ) ( {p23 p29 p19 p10 p34 p33 p41 } a5 {p50 p29 p0 p6 p11 p9 p41 } ) ( {p49 p19 p18 p33 p9 p45 } a18 {p17 p8 p6 p33 p9 p45 } ) ( {p20 p38 p35 p19 p10 p9 p39 p40 } a2 {p28 p24 p29 p0 p6 p9 p44 p41 } ) ( {p28 p12 p33 p9 } a20 {p16 p12 p33 p9 } ) ( {p53 p37 p38 p35 p8 p10 p9 p39 p40 } a4 {p36 p5 p24 p29 p0 p18 p9 p44 p41 } ) ( {p32 p35 p10 p33 p40 } a16 {p23 p35 p10 p33 p40 } ) ( {p52 p8 p6 p13 p33 p40 p41 } a13 {p30 p19 p18 p11 p12 p40 p41 } ) ( {p32 p24 p29 p0 p6 p11 p9 p40 } a16 {p23 p38 p35 p19 p10 p34 p33 p40 } ) ( {p52 p8 p6 p12 p40 p41 } a13 {p30 p19 p18 p12 p40 p41 } ) ( {p20 p38 p35 p8 p10 p34 p33 p41 } a2 {p28 p24 p29 p0 p18 p11 p9 p41 } ) ( {p49 p19 p18 p33 p9 p42 p40 } a18 {p17 p8 p6 p33 p9 p44 p45 } ) ( {p3 p35 p10 p11 p9 p44 p41 } a10 {p20 p35 p10 p34 p33 p39 p40 } ) ( {p52 p18 p12 p44 p45 } a13 {p30 p18 p12 p42 p40 } ) ( {p53 p37 p29 p8 p10 p9 p39 p40 } a4 {p36 p5 p29 p0 p18 p9 p44 p41 } ) ( {p47 p1 p43 } a9 {p52 p1 p43 } ) ( {p53 p37 p38 p35 p8 p10 p9 p41 } a4 {p36 p5 p24 p29 p0 p18 p9 p41 } ) ( {p32 p35 p10 p33 p44 p41 } a16 {p23 p35 p10 p33 p39 p40 } ) ( {p53 p37 p29 p6 p18 p9 p41 } a4 {p36 p5 p29 p6 p18 p9 p41 } ) ( {p23 p29 p8 p10 p9 p41 } a5 {p50 p29 p0 p18 p9 p41 } ) ( {p50 p10 p6 p18 p42 p43 } a21 {p26 p10 p6 p18 p48 p45 } ) ( {p20 p29 p8 p10 p34 p33 p41 } a2 {p28 p29 p0 p18 p11 p9 p41 } ) }, initialMarking = {p7 p40 p9 p41 p10 p12 p45 p48 p18 p53 p2 p6 p33 p35 p37 p38 }, acceptingPlaces = {p4 p46 } );