// Benchmark for difference of Petri net and DFA  
// Generated from
// Peterson.bpl_AllErrorsAtOnce_Iteration1_AbstractionAfterDifference.ats (2018/08/13 05:05:46)
// Peterson.bpl_AllErrorsAtOnce_Iteration2_EagerFloydHoareAutomaton.ats (2018/08/13 05:05:46)

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

FiniteAutomaton nwa = (
	alphabet = {"assume true;" "flag1 := 1;" "turn := 0;" "assume flag0 == 0 || turn == 1;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "flag1 := 0;" "assume !true;" "assume true;" "assume true;" "flag0 := 1;" "turn := 1;" "assume flag1 == 0 || turn == 0;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "flag0 := 0;" "assume !true;" "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" "assume true;" "36#true")
		("36#true" "flag0 := 1;" "38#(<= 1 flag0)")
		("36#true" "assume true;" "36#true")
		("36#true" "flag1 := 1;" "36#true")
		("36#true" "turn := 0;" "36#true")
		("36#true" "assume flag0 == 0 || turn == 1;" "36#true")
		("36#true" "assume critical == 0;" "36#true")
		("36#true" "critical := 1;" "36#true")
		("36#true" "critical := 0;" "36#true")
		("36#true" "flag1 := 0;" "36#true")
		("36#true" "critical := 0;assume true;" "36#true")
		("38#(<= 1 flag0)" "assume true;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "flag1 := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "turn := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("38#(<= 1 flag0)" "assume flag0 == 0 || turn == 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "assume !(critical == 0);" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "assume critical == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "critical := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "critical := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "flag1 := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "turn := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "assume flag1 == 0 || turn == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "assume !(critical == 0);" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "assume critical == 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "critical := 1;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "critical := 0;" "38#(<= 1 flag0)")
		("38#(<= 1 flag0)" "flag0 := 0;" "36#true")
		("39#(and (<= turn 0) (<= 1 flag0))" "turn := 1;" "38#(<= 1 flag0)")
		("39#(and (<= turn 0) (<= 1 flag0))" "assume flag1 == 0 || turn == 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "assume flag0 == 0 || turn == 1;" "37#false")
		("39#(and (<= turn 0) (<= 1 flag0))" "assume critical == 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "critical := 1;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "critical := 0;" "39#(and (<= turn 0) (<= 1 flag0))")
		("39#(and (<= turn 0) (<= 1 flag0))" "flag0 := 0;" "36#true")
	}
);