// Benchmark for difference of Petri net and DFA  
// Generated from
// Peterson.bpl_AllErrorsAtOnce_Iteration1_AbstractionAfterDifference.ats (2018/07/30 09:54:59)
// Peterson.bpl_AllErrorsAtOnce_Iteration2_EagerFloydHoareAutomaton.ats (2018/07/30 09:54:59)


PetriNet net = (
	alphabet = {"#4#assume true;" "#5#flag1 := 1;" "#6#turn := 0;" "#7#assume flag0 == 0 || turn == 1;" "#8#assume !(critical == 0);" "#9#assume critical == 0;" "#10#critical := 1;" "#11#critical := 0;" "#12#flag1 := 0;" "#14#assume !true;" "#15#assume true;" "#18#assume true;" "#19#flag0 := 1;" "#20#turn := 1;" "#21#assume flag1 == 0 || turn == 0;" "#22#assume !(critical == 0);" "#23#assume critical == 0;" "#24#critical := 1;" "#25#critical := 0;" "#26#flag0 := 0;" "#28#assume !true;" "#29#assume true;" "critical := 0;assume true;" },
	places = {"5#L56true" "6#L52true" "7#L57true" "8#Thread1FINALtrue" "9#L58true" "10#L53true" "11#L54true" "12#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "13#Thread1EXITtrue" "14#L59true" "15#L55true" "16#~initENTRYtrue" "18#L33true" "19#L38true" "20#L39true" "21#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "22#Thread0FINALtrue" "23#L34true" "24#L35true" "25#Thread0EXITtrue" "26#L36true" "27#L37true" "28#L32true" "29#~initENTRYtrue" "30#true" "32#(= critical 0)" "Black: 32#(= critical 0)" "Black: 30#true" },
	transitions = {
		({"14#L59true" } "#12#flag1 := 0;" {"6#L52true" })
		({"18#L33true" } "#19#flag0 := 1;" {"23#L34true" })
		({"Black: 30#true" "5#L56true" } "#9#assume critical == 0;" {"Black: 30#true" "7#L57true" })
		({"11#L54true" } "#6#turn := 0;" {"15#L55true" })
		({"19#L38true" "Black: 30#true" } "#25#critical := 0;" {"Black: 30#true" "20#L39true" })
		({"16#~initENTRYtrue" "Black: 30#true" "29#~initENTRYtrue" } "critical := 0;assume true;" {"Black: 30#true" "6#L52true" "28#L32true" })
		({"Black: 32#(= critical 0)" "9#L58true" "30#true" } "#11#critical := 0;" {"32#(= critical 0)" "Black: 30#true" "14#L59true" })
		({"Black: 32#(= critical 0)" "26#L36true" } "#22#assume !(critical == 0);" {"Black: 32#(= critical 0)" "21#Thread0Err0ASSERT_VIOLATIONASSERTtrue" })
		({"23#L34true" } "#20#turn := 1;" {"24#L35true" })
		({"Black: 30#true" "26#L36true" } "#23#assume critical == 0;" {"Black: 30#true" "27#L37true" })
		({"32#(= critical 0)" "Black: 30#true" "27#L37true" } "#24#critical := 1;" {"Black: 32#(= critical 0)" "19#L38true" "30#true" })
		({"Black: 32#(= critical 0)" "27#L37true" } "#24#critical := 1;" {"Black: 32#(= critical 0)" "19#L38true" })
		({"Black: 32#(= critical 0)" "5#L56true" } "#8#assume !(critical == 0);" {"Black: 32#(= critical 0)" "12#Thread1Err0ASSERT_VIOLATIONASSERTtrue" })
		({"20#L39true" } "#26#flag0 := 0;" {"28#L32true" })
		({"10#L53true" } "#5#flag1 := 1;" {"11#L54true" })
		({"32#(= critical 0)" "Black: 30#true" "7#L57true" } "#10#critical := 1;" {"Black: 32#(= critical 0)" "9#L58true" "30#true" })
		({"6#L52true" } "#4#assume true;" {"10#L53true" })
		({"28#L32true" } "#18#assume true;" {"18#L33true" })
		({"Black: 32#(= critical 0)" "7#L57true" } "#10#critical := 1;" {"Black: 32#(= critical 0)" "9#L58true" })
		({"Black: 32#(= critical 0)" "5#L56true" "30#true" } "#9#assume critical == 0;" {"32#(= critical 0)" "Black: 30#true" "7#L57true" })
		({"Black: 32#(= critical 0)" "19#L38true" "30#true" } "#25#critical := 0;" {"32#(= critical 0)" "Black: 30#true" "20#L39true" })
		({"22#Thread0FINALtrue" } "#29#assume true;" {"25#Thread0EXITtrue" })
		({"16#~initENTRYtrue" "Black: 32#(= critical 0)" "29#~initENTRYtrue" "30#true" } "critical := 0;assume true;" {"32#(= critical 0)" "Black: 30#true" "6#L52true" "28#L32true" })
		({"Black: 32#(= critical 0)" "26#L36true" "30#true" } "#23#assume critical == 0;" {"32#(= critical 0)" "Black: 30#true" "27#L37true" })
		({"24#L35true" } "#21#assume flag1 == 0 || turn == 0;" {"26#L36true" })
		({"8#Thread1FINALtrue" } "#15#assume true;" {"13#Thread1EXITtrue" })
		({"Black: 30#true" "9#L58true" } "#11#critical := 0;" {"Black: 30#true" "14#L59true" })
		({"15#L55true" } "#7#assume flag0 == 0 || turn == 1;" {"5#L56true" })
	},
	initialMarking = {"16#~initENTRYtrue" "Black: 32#(= critical 0)" "29#~initENTRYtrue" "30#true" },
	acceptingPlaces = {"21#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "12#Thread1Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"#4#assume true;" "#5#flag1 := 1;" "#6#turn := 0;" "#7#assume flag0 == 0 || turn == 1;" "#8#assume !(critical == 0);" "#9#assume critical == 0;" "#10#critical := 1;" "#11#critical := 0;" "#12#flag1 := 0;" "#14#assume !true;" "#15#assume true;" "#18#assume true;" "#19#flag0 := 1;" "#20#turn := 1;" "#21#assume flag1 == 0 || turn == 0;" "#22#assume !(critical == 0);" "#23#assume critical == 0;" "#24#critical := 1;" "#25#critical := 0;" "#26#flag0 := 0;" "#28#assume !true;" "#29#assume true;" "critical := 0;assume true;" },
	states = {"36#true" "37#false" "38#(<= 1 flag0)" "39#(and (<= turn 0) (<= 1 flag0))" },
	initialStates = {"36#true" },
	finalStates = {"37#false" },
	transitions = {
		("36#true" "#4#assume true;" "36#true")
		("36#true" "#5#flag1 := 1;" "36#true")
		("36#true" "#6#turn := 0;" "36#true")
		("36#true" "#7#assume flag0 == 0 || turn == 1;" "36#true")
		("36#true" "#8#assume !(critical == 0);" "36#true")
		("36#true" "#9#assume critical == 0;" "36#true")
		("36#true" "#10#critical := 1;" "36#true")
		("36#true" "#11#critical := 0;" "36#true")
		("36#true" "#12#flag1 := 0;" "36#true")
		("36#true" "#14#assume !true;" "37#false")
		("36#true" "#15#assume true;" "36#true")
		("36#true" "#18#assume true;" "36#true")
		("36#true" "#19#flag0 := 1;" "38#(<= 1 flag0)")
		("36#true" "#20#turn := 1;" "36#true")
		("36#true" "#21#assume flag1 == 0 || turn == 0;" "36#true")
		("36#true" "#22#assume !(critical == 0);" "36#true")
		("36#true" "#23#assume critical == 0;" "36#true")
		("36#true" "#24#critical := 1;" "36#true")
		("36#true" "#25#critical := 0;" "36#true")
		("36#true" "#26#flag0 := 0;" "36#true")
		("36#true" "#28#assume !true;" "37#false")
		("36#true" "#29#assume true;" "36#true")
		("36#true" "critical := 0;assume true;" "36#true")
		("37#false" "#4#assume true;" "37#false")
		("37#false" "#5#flag1 := 1;" "37#false")
		("37#false" "#6#turn := 0;" "37#false")
		("37#false" "#7#assume flag0 == 0 || turn == 1;" "37#false")
		("37#false" "#8#assume !(critical == 0);" "37#false")
		("37#false" "#9#assume critical == 0;" "37#false")
		("37#false" "#10#critical := 1;" "37#false")
		("37#false" "#11#critical := 0;" "37#false")
		("37#false" "#12#flag1 := 0;" "37#false")
		("37#false" "#14#assume !true;" "37#false")
		("37#false" "#15#assume true;" "37#false")
		("37#false" "#18#assume true;" "37#false")
		("37#false" "#19#flag0 := 1;" "37#false")
		("37#false" "#20#turn := 1;" "37#false")
		("37#false" "#21#assume flag1 == 0 || turn == 0;" "37#false")
		("37#false" "#22#assume !(critical == 0);" "37#false")
		("37#false" "#23#assume critical == 0;" "37#false")
		("37#false" "#24#critical := 1;" "37#false")
		("37#false" "#25#critical := 0;" "37#false")
		("37#false" "#26#flag0 := 0;" "37#false")
		("37#false" "#28#assume !true;" "37#false")
		("37#false" "#29#assume true;" "37#false")
		("37#false" "critical := 0;assume true;" "37#false")
		("38#(<= 1 flag0)" "#4#assume true;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#5#flag1 := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#6#turn := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("38#(<= 1 flag0)" "#7#assume flag0 == 0 || turn == 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#8#assume !(critical == 0);" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#9#assume critical == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#10#critical := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#11#critical := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#12#flag1 := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#14#assume !true;" "37#false")
		("38#(<= 1 flag0)" "#15#assume true;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#18#assume true;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#19#flag0 := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#20#turn := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#21#assume flag1 == 0 || turn == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#22#assume !(critical == 0);" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#23#assume critical == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#24#critical := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#25#critical := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "#26#flag0 := 0;" "36#true")
		("38#(<= 1 flag0)" "#28#assume !true;" "37#false")
		("38#(<= 1 flag0)" "#29#assume true;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "critical := 0;assume true;" "38#(<= 1 flag0)")
		("39#(and (<= turn 0) (<= 1 flag0))" "#4#assume true;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#5#flag1 := 1;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#6#turn := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#7#assume flag0 == 0 || turn == 1;" "37#false")
		("39#(and (<= turn 0) (<= 1 flag0))" "#8#assume !(critical == 0);" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#9#assume critical == 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#10#critical := 1;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#11#critical := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#12#flag1 := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#14#assume !true;" "37#false")
		("39#(and (<= turn 0) (<= 1 flag0))" "#15#assume true;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#18#assume true;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#19#flag0 := 1;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#20#turn := 1;" "38#(<= 1 flag0)")
		("39#(and (<= turn 0) (<= 1 flag0))" "#21#assume flag1 == 0 || turn == 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#22#assume !(critical == 0);" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#23#assume critical == 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#24#critical := 1;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#25#critical := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "#26#flag0 := 0;" "36#true")
		("39#(and (<= turn 0) (<= 1 flag0))" "#28#assume !true;" "37#false")
		("39#(and (<= turn 0) (<= 1 flag0))" "#29#assume true;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "critical := 0;assume true;" "39#(and (<= turn 0) (<= 1 flag0))")
	}
);