// Benchmark for difference of Petri net and DFA  
// Generated from
// Peterson.bpl_AllErrorsAtOnce_Iteration2_AbstractionAfterDifference.ats (2018/07/30 09:54:59)
// Peterson.bpl_AllErrorsAtOnce_Iteration3_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" "36#true" "38#(<= 1 flag0)" "39#(and (<= turn 0) (<= 1 flag0))" "Black: 36#true" "Black: 38#(<= 1 flag0)" "Black: 39#(and (<= turn 0) (<= 1 flag0))" },
	transitions = {
		({"14#L59true" } "#12#flag1 := 0;" {"6#L52true" })
		({"Black: 30#true" "5#L56true" } "#9#assume critical == 0;" {"Black: 30#true" "7#L57true" })
		({"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" })
		({"20#L39true" "39#(and (<= turn 0) (<= 1 flag0))" "Black: 36#true" } "#26#flag0 := 0;" {"36#true" "Black: 39#(and (<= turn 0) (<= 1 flag0))" "28#L32true" })
		({"Black: 30#true" "26#L36true" } "#23#assume critical == 0;" {"Black: 30#true" "27#L37true" })
		({"Black: 38#(<= 1 flag0)" "11#L54true" } "#6#turn := 0;" {"Black: 38#(<= 1 flag0)" "15#L55true" })
		({"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" })
		({"Black: 39#(and (<= turn 0) (<= 1 flag0))" "15#L55true" } "#7#assume flag0 == 0 || turn == 1;" {"5#L56true" "Black: 39#(and (<= turn 0) (<= 1 flag0))" })
		({"38#(<= 1 flag0)" "Black: 39#(and (<= turn 0) (<= 1 flag0))" "11#L54true" } "#6#turn := 0;" {"39#(and (<= turn 0) (<= 1 flag0))" "Black: 38#(<= 1 flag0)" "15#L55true" })
		({"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" })
		({"18#L33true" "36#true" "Black: 38#(<= 1 flag0)" } "#19#flag0 := 1;" {"38#(<= 1 flag0)" "23#L34true" "Black: 36#true" })
		({"39#(and (<= turn 0) (<= 1 flag0))" "23#L34true" "Black: 38#(<= 1 flag0)" } "#20#turn := 1;" {"38#(<= 1 flag0)" "24#L35true" "Black: 39#(and (<= turn 0) (<= 1 flag0))" })
		({"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" })
		({"36#true" "20#L39true" } "#26#flag0 := 0;" {"36#true" "28#L32true" })
		({"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" })
		({"23#L34true" "Black: 39#(and (<= turn 0) (<= 1 flag0))" } "#20#turn := 1;" {"24#L35true" "Black: 39#(and (<= turn 0) (<= 1 flag0))" })
		({"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" })
		({"18#L33true" "Black: 36#true" } "#19#flag0 := 1;" {"23#L34true" "Black: 36#true" })
		({"20#L39true" "38#(<= 1 flag0)" "Black: 36#true" } "#26#flag0 := 0;" {"36#true" "Black: 38#(<= 1 flag0)" "28#L32true" })
	},
	initialMarking = {"16#~initENTRYtrue" "Black: 32#(= critical 0)" "36#true" "Black: 38#(<= 1 flag0)" "Black: 39#(and (<= turn 0) (<= 1 flag0))" "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 = {"44#true" "45#false" "46#(<= 1 flag1)" "47#(and (<= 1 flag1) (= turn 1))" },
	initialStates = {"44#true" },
	finalStates = {"45#false" },
	transitions = {
		("44#true" "#4#assume true;" "44#true")
		("44#true" "#5#flag1 := 1;" "46#(<= 1 flag1)")
		("44#true" "#6#turn := 0;" "44#true")
		("44#true" "#7#assume flag0 == 0 || turn == 1;" "44#true")
		("44#true" "#8#assume !(critical == 0);" "44#true")
		("44#true" "#9#assume critical == 0;" "44#true")
		("44#true" "#10#critical := 1;" "44#true")
		("44#true" "#11#critical := 0;" "44#true")
		("44#true" "#12#flag1 := 0;" "44#true")
		("44#true" "#14#assume !true;" "45#false")
		("44#true" "#15#assume true;" "44#true")
		("44#true" "#18#assume true;" "44#true")
		("44#true" "#19#flag0 := 1;" "44#true")
		("44#true" "#20#turn := 1;" "44#true")
		("44#true" "#21#assume flag1 == 0 || turn == 0;" "44#true")
		("44#true" "#22#assume !(critical == 0);" "44#true")
		("44#true" "#23#assume critical == 0;" "44#true")
		("44#true" "#24#critical := 1;" "44#true")
		("44#true" "#25#critical := 0;" "44#true")
		("44#true" "#26#flag0 := 0;" "44#true")
		("44#true" "#28#assume !true;" "45#false")
		("44#true" "#29#assume true;" "44#true")
		("44#true" "critical := 0;assume true;" "44#true")
		("45#false" "#4#assume true;" "45#false")
		("45#false" "#5#flag1 := 1;" "45#false")
		("45#false" "#6#turn := 0;" "45#false")
		("45#false" "#7#assume flag0 == 0 || turn == 1;" "45#false")
		("45#false" "#8#assume !(critical == 0);" "45#false")
		("45#false" "#9#assume critical == 0;" "45#false")
		("45#false" "#10#critical := 1;" "45#false")
		("45#false" "#11#critical := 0;" "45#false")
		("45#false" "#12#flag1 := 0;" "45#false")
		("45#false" "#14#assume !true;" "45#false")
		("45#false" "#15#assume true;" "45#false")
		("45#false" "#18#assume true;" "45#false")
		("45#false" "#19#flag0 := 1;" "45#false")
		("45#false" "#20#turn := 1;" "45#false")
		("45#false" "#21#assume flag1 == 0 || turn == 0;" "45#false")
		("45#false" "#22#assume !(critical == 0);" "45#false")
		("45#false" "#23#assume critical == 0;" "45#false")
		("45#false" "#24#critical := 1;" "45#false")
		("45#false" "#25#critical := 0;" "45#false")
		("45#false" "#26#flag0 := 0;" "45#false")
		("45#false" "#28#assume !true;" "45#false")
		("45#false" "#29#assume true;" "45#false")
		("45#false" "critical := 0;assume true;" "45#false")
		("46#(<= 1 flag1)" "#4#assume true;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#5#flag1 := 1;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#6#turn := 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#7#assume flag0 == 0 || turn == 1;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#8#assume !(critical == 0);" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#9#assume critical == 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#10#critical := 1;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#11#critical := 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#12#flag1 := 0;" "44#true")
		("46#(<= 1 flag1)" "#14#assume !true;" "45#false")
		("46#(<= 1 flag1)" "#15#assume true;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#18#assume true;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#19#flag0 := 1;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#20#turn := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("46#(<= 1 flag1)" "#21#assume flag1 == 0 || turn == 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#22#assume !(critical == 0);" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#23#assume critical == 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#24#critical := 1;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#25#critical := 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#26#flag0 := 0;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "#28#assume !true;" "45#false")
		("46#(<= 1 flag1)" "#29#assume true;" "46#(<= 1 flag1)")
		("46#(<= 1 flag1)" "critical := 0;assume true;" "46#(<= 1 flag1)")
		("47#(and (<= 1 flag1) (= turn 1))" "#4#assume true;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#5#flag1 := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#6#turn := 0;" "46#(<= 1 flag1)")
		("47#(and (<= 1 flag1) (= turn 1))" "#7#assume flag0 == 0 || turn == 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#8#assume !(critical == 0);" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#9#assume critical == 0;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#10#critical := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#11#critical := 0;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#12#flag1 := 0;" "44#true")
		("47#(and (<= 1 flag1) (= turn 1))" "#14#assume !true;" "45#false")
		("47#(and (<= 1 flag1) (= turn 1))" "#15#assume true;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#18#assume true;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#19#flag0 := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#20#turn := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#21#assume flag1 == 0 || turn == 0;" "45#false")
		("47#(and (<= 1 flag1) (= turn 1))" "#22#assume !(critical == 0);" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#23#assume critical == 0;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#24#critical := 1;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#25#critical := 0;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#26#flag0 := 0;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "#28#assume !true;" "45#false")
		("47#(and (<= 1 flag1) (= turn 1))" "#29#assume true;" "47#(and (<= 1 flag1) (= turn 1))")
		("47#(and (<= 1 flag1) (= turn 1))" "critical := 0;assume true;" "47#(and (<= 1 flag1) (= turn 1))")
	}
);