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


PetriNet net = (
	alphabet = {"#6#assume true;" "#7#n1 := n0 + 1;" "#8#assume n0 == 0 || n1 < n0;" "#9#assume !(critical == 0);" "#10#assume critical == 0;" "#11#critical := 1;" "#12#critical := 0;" "#13#n1 := 0;" "#15#assume !true;" "#16#assume true;" "#19#assume true;" "#20#n0 := n1 + 1;" "#21#assume n1 == 0 || n0 < n1;" "#22#assume !(critical == 0);" "#23#assume critical == 0;" "#24#critical := 1;" "#25#critical := 0;" "#26#n0 := 0;" "#28#assume !true;" "#29#assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" },
	places = {"5#L56true" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "7#L57true" "8#Thread1FINALtrue" "9#L58true" "10#L54true" "11#Thread1EXITtrue" "12#L59true" "13#L60true" "14#L55true" "15#~initENTRYtrue" "17#L38true" "18#L39true" "19#Thread0FINALtrue" "20#L35true" "21#L40true" "22#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "23#L41true" "24#Thread0EXITtrue" "25#L36true" "26#L37true" "27#~initENTRYtrue" "28#true" "30#(= critical 0)" "Black: 28#true" "Black: 30#(= critical 0)" },
	transitions = {
		({"Black: 30#(= critical 0)" "7#L57true" "28#true" } "#10#assume critical == 0;" {"Black: 28#true" "9#L58true" "30#(= critical 0)" })
		({"23#L41true" } "#26#n0 := 0;" {"20#L35true" })
		({"26#L37true" } "#21#assume n1 == 0 || n0 < n1;" {"17#L38true" })
		({"Black: 30#(= critical 0)" "21#L40true" "28#true" } "#25#critical := 0;" {"Black: 28#true" "23#L41true" "30#(= critical 0)" })
		({"5#L56true" } "#8#assume n0 == 0 || n1 < n0;" {"7#L57true" })
		({"17#L38true" "Black: 30#(= critical 0)" } "#22#assume !(critical == 0);" {"Black: 30#(= critical 0)" "22#Thread0Err0ASSERT_VIOLATIONASSERTtrue" })
		({"Black: 28#true" "27#~initENTRYtrue" "15#~initENTRYtrue" } "critical := 0;n0 := 0;n1 := 1;assume true;" {"Black: 28#true" "20#L35true" "10#L54true" })
		({"Black: 28#true" "18#L39true" "30#(= critical 0)" } "#24#critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" "28#true" })
		({"13#L60true" } "#13#n1 := 0;" {"10#L54true" })
		({"Black: 30#(= critical 0)" "18#L39true" } "#24#critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" })
		({"Black: 30#(= critical 0)" "27#~initENTRYtrue" "28#true" "15#~initENTRYtrue" } "critical := 0;n0 := 0;n1 := 1;assume true;" {"Black: 28#true" "20#L35true" "10#L54true" "30#(= critical 0)" })
		({"Black: 28#true" "12#L59true" } "#12#critical := 0;" {"Black: 28#true" "13#L60true" })
		({"Black: 28#true" "17#L38true" } "#23#assume critical == 0;" {"Black: 28#true" "18#L39true" })
		({"8#Thread1FINALtrue" } "#16#assume true;" {"11#Thread1EXITtrue" })
		({"Black: 30#(= critical 0)" "28#true" "12#L59true" } "#12#critical := 0;" {"Black: 28#true" "13#L60true" "30#(= critical 0)" })
		({"Black: 30#(= critical 0)" "17#L38true" "28#true" } "#23#assume critical == 0;" {"Black: 28#true" "18#L39true" "30#(= critical 0)" })
		({"20#L35true" } "#19#assume true;" {"25#L36true" })
		({"14#L55true" } "#7#n1 := n0 + 1;" {"5#L56true" })
		({"Black: 30#(= critical 0)" "7#L57true" } "#9#assume !(critical == 0);" {"Black: 30#(= critical 0)" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" })
		({"10#L54true" } "#6#assume true;" {"14#L55true" })
		({"19#Thread0FINALtrue" } "#29#assume true;" {"24#Thread0EXITtrue" })
		({"25#L36true" } "#20#n0 := n1 + 1;" {"26#L37true" })
		({"Black: 28#true" "7#L57true" } "#10#assume critical == 0;" {"Black: 28#true" "9#L58true" })
		({"Black: 28#true" "9#L58true" "30#(= critical 0)" } "#11#critical := 1;" {"Black: 30#(= critical 0)" "28#true" "12#L59true" })
		({"Black: 28#true" "21#L40true" } "#25#critical := 0;" {"Black: 28#true" "23#L41true" })
		({"Black: 30#(= critical 0)" "9#L58true" } "#11#critical := 1;" {"Black: 30#(= critical 0)" "12#L59true" })
	},
	initialMarking = {"Black: 30#(= critical 0)" "27#~initENTRYtrue" "28#true" "15#~initENTRYtrue" },
	acceptingPlaces = {"6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "22#Thread0Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"#6#assume true;" "#7#n1 := n0 + 1;" "#8#assume n0 == 0 || n1 < n0;" "#9#assume !(critical == 0);" "#10#assume critical == 0;" "#11#critical := 1;" "#12#critical := 0;" "#13#n1 := 0;" "#15#assume !true;" "#16#assume true;" "#19#assume true;" "#20#n0 := n1 + 1;" "#21#assume n1 == 0 || n0 < n1;" "#22#assume !(critical == 0);" "#23#assume critical == 0;" "#24#critical := 1;" "#25#critical := 0;" "#26#n0 := 0;" "#28#assume !true;" "#29#assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" },
	states = {"34#true" "35#false" "36#(<= 1 n1)" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" },
	initialStates = {"34#true" },
	finalStates = {"35#false" },
	transitions = {
		("34#true" "#6#assume true;" "34#true")
		("34#true" "#7#n1 := n0 + 1;" "34#true")
		("34#true" "#8#assume n0 == 0 || n1 < n0;" "34#true")
		("34#true" "#9#assume !(critical == 0);" "34#true")
		("34#true" "#10#assume critical == 0;" "34#true")
		("34#true" "#11#critical := 1;" "34#true")
		("34#true" "#12#critical := 0;" "34#true")
		("34#true" "#13#n1 := 0;" "34#true")
		("34#true" "#15#assume !true;" "35#false")
		("34#true" "#16#assume true;" "34#true")
		("34#true" "#19#assume true;" "34#true")
		("34#true" "#20#n0 := n1 + 1;" "34#true")
		("34#true" "#21#assume n1 == 0 || n0 < n1;" "34#true")
		("34#true" "#22#assume !(critical == 0);" "34#true")
		("34#true" "#23#assume critical == 0;" "34#true")
		("34#true" "#24#critical := 1;" "34#true")
		("34#true" "#25#critical := 0;" "34#true")
		("34#true" "#26#n0 := 0;" "34#true")
		("34#true" "#28#assume !true;" "35#false")
		("34#true" "#29#assume true;" "34#true")
		("34#true" "critical := 0;n0 := 0;n1 := 1;assume true;" "36#(<= 1 n1)")
		("35#false" "#6#assume true;" "35#false")
		("35#false" "#7#n1 := n0 + 1;" "35#false")
		("35#false" "#8#assume n0 == 0 || n1 < n0;" "35#false")
		("35#false" "#9#assume !(critical == 0);" "35#false")
		("35#false" "#10#assume critical == 0;" "35#false")
		("35#false" "#11#critical := 1;" "35#false")
		("35#false" "#12#critical := 0;" "35#false")
		("35#false" "#13#n1 := 0;" "35#false")
		("35#false" "#15#assume !true;" "35#false")
		("35#false" "#16#assume true;" "35#false")
		("35#false" "#19#assume true;" "35#false")
		("35#false" "#20#n0 := n1 + 1;" "35#false")
		("35#false" "#21#assume n1 == 0 || n0 < n1;" "35#false")
		("35#false" "#22#assume !(critical == 0);" "35#false")
		("35#false" "#23#assume critical == 0;" "35#false")
		("35#false" "#24#critical := 1;" "35#false")
		("35#false" "#25#critical := 0;" "35#false")
		("35#false" "#26#n0 := 0;" "35#false")
		("35#false" "#28#assume !true;" "35#false")
		("35#false" "#29#assume true;" "35#false")
		("35#false" "critical := 0;n0 := 0;n1 := 1;assume true;" "35#false")
		("36#(<= 1 n1)" "#6#assume true;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#7#n1 := n0 + 1;" "34#true")
		("36#(<= 1 n1)" "#8#assume n0 == 0 || n1 < n0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#9#assume !(critical == 0);" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#10#assume critical == 0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#11#critical := 1;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#12#critical := 0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#13#n1 := 0;" "34#true")
		("36#(<= 1 n1)" "#15#assume !true;" "35#false")
		("36#(<= 1 n1)" "#16#assume true;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#19#assume true;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#20#n0 := n1 + 1;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("36#(<= 1 n1)" "#21#assume n1 == 0 || n0 < n1;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#22#assume !(critical == 0);" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#23#assume critical == 0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#24#critical := 1;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#25#critical := 0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#26#n0 := 0;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "#28#assume !true;" "35#false")
		("36#(<= 1 n1)" "#29#assume true;" "36#(<= 1 n1)")
		("36#(<= 1 n1)" "critical := 0;n0 := 0;n1 := 1;assume true;" "36#(<= 1 n1)")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#6#assume true;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#7#n1 := n0 + 1;" "36#(<= 1 n1)")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#8#assume n0 == 0 || n1 < n0;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#9#assume !(critical == 0);" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#10#assume critical == 0;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#11#critical := 1;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#12#critical := 0;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#13#n1 := 0;" "34#true")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#15#assume !true;" "35#false")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#16#assume true;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#19#assume true;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#20#n0 := n1 + 1;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#21#assume n1 == 0 || n0 < n1;" "35#false")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#22#assume !(critical == 0);" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#23#assume critical == 0;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#24#critical := 1;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#25#critical := 0;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#26#n0 := 0;" "36#(<= 1 n1)")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#28#assume !true;" "35#false")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "#29#assume true;" "37#(and (<= 1 n1) (<= (+ n1 1) n0))")
		("37#(and (<= 1 n1) (<= (+ n1 1) n0))" "critical := 0;n0 := 0;n1 := 1;assume true;" "36#(<= 1 n1)")
	}
);