// Benchmark for difference of Petri net and DFA  
// Generated from
// Bakery.bpl_AllErrorsAtOnce_Iteration3_AbstractionAfterDifference.ats (2018/08/13 05:05:17)
// Bakery.bpl_AllErrorsAtOnce_Iteration4_EagerFloydHoareAutomaton.ats (2018/08/13 05:05:18)

PetriNet net = (
	alphabet = {"assume true;" "n1 := n0 + 1;" "assume n0 == 0 || n1 < n0;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n1 := 0;" "assume !true;" "assume true;" "assume true;" "n0 := n1 + 1;" "assume n1 == 0 || n0 < n1;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n0 := 0;" "assume !true;" "assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" },
	places = {"5#L56true" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "7#L57true" "9#L58true" "10#L54true" "12#L59true" "13#L60true" "14#L55true" "15#~initENTRYtrue" "17#L38true" "18#L39true" "20#L35true" "21#L40true" "22#L41true" "24#L36true" "25#L37true" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "27#~initENTRYtrue" "28#true" "30#(= critical 0)" "Black: 28#true" "Black: 30#(= critical 0)" "34#true" "36#(<= 1 n1)" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "41#true" "43#(= n0 0)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "45#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" },
	transitions = {
		({"Black: 30#(= critical 0)" "21#L40true" "28#true" } "critical := 0;" {"Black: 28#true" "22#L41true" "30#(= critical 0)" })
		({"Black: 43#(= n0 0)" "36#(<= 1 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "13#L60true" } "n1 := 0;" {"34#true" "Black: 36#(<= 1 n1)" "10#L54true" "43#(= n0 0)" })
		({"Black: 30#(= critical 0)" "7#L57true" "28#true" } "assume critical == 0;" {"Black: 28#true" "9#L58true" "30#(= critical 0)" })
		({"37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" "14#L55true" } "n1 := n0 + 1;" {"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "36#(<= 1 n1)" "5#L56true" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "45#(<= 1 n1)" })
		({"37#(and (<= 1 n1) (<= (+ n1 1) n0))" "13#L60true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" } "n1 := 0;" {"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "41#true" "10#L54true" })
		({"34#true" "43#(= n0 0)" "14#L55true" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "34#true" "5#L56true" "44#(and (= n0 0) (<= (+ n0 1) n1))" })
		({"5#L56true" } "assume n0 == 0 || n1 < n0;" {"7#L57true" })
		({"34#true" "13#L60true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" } "n1 := 0;" {"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "41#true" "10#L54true" })
		({"Black: 36#(<= 1 n1)" "24#L36true" "43#(= n0 0)" } "n0 := n1 + 1;" {"Black: 43#(= n0 0)" "Black: 36#(<= 1 n1)" "41#true" "25#L37true" })
		({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "36#(<= 1 n1)" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "24#L36true" "44#(and (= n0 0) (<= (+ n0 1) n1))" } "n0 := n1 + 1;" {"37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "25#L37true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" })
		({"36#(<= 1 n1)" "45#(<= 1 n1)" "13#L60true" } "n1 := 0;" {"34#true" "Black: 36#(<= 1 n1)" "41#true" "10#L54true" })
		({"Black: 30#(= critical 0)" "34#true" "Black: 36#(<= 1 n1)" "41#true" "27#~initENTRYtrue" "28#true" "15#~initENTRYtrue" } "critical := 0;n0 := 0;n1 := 1;assume true;" {"Black: 28#true" "36#(<= 1 n1)" "20#L35true" "10#L54true" "44#(and (= n0 0) (<= (+ n0 1) n1))" "30#(= critical 0)" })
		({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "36#(<= 1 n1)" "14#L55true" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "5#L56true" "Black: 36#(<= 1 n1)" })
		({"Black: 28#true" "18#L39true" "30#(= critical 0)" } "critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" "28#true" })
		({"Black: 43#(= n0 0)" "34#true" "44#(and (= n0 0) (<= (+ n0 1) n1))" "13#L60true" } "n1 := 0;" {"34#true" "10#L54true" "43#(= n0 0)" })
		({"Black: 30#(= critical 0)" "18#L39true" } "critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" })
		({"34#true" "43#(= n0 0)" "13#L60true" } "n1 := 0;" {"34#true" "10#L54true" "43#(= n0 0)" })
		({"Black: 28#true" "12#L59true" } "critical := 0;" {"Black: 28#true" "13#L60true" })
		({"Black: 28#true" "17#L38true" } "assume critical == 0;" {"Black: 28#true" "18#L39true" })
		({"20#L35true" } "assume true;" {"24#L36true" })
		({"Black: 30#(= critical 0)" "28#true" "12#L59true" } "critical := 0;" {"Black: 28#true" "13#L60true" "30#(= critical 0)" })
		({"17#L38true" "Black: 30#(= critical 0)" } "assume !(critical == 0);" {"Black: 30#(= critical 0)" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" })
		({"Black: 43#(= n0 0)" "22#L41true" "41#true" } "n0 := 0;" {"20#L35true" "43#(= n0 0)" })
		({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "24#L36true" "44#(and (= n0 0) (<= (+ n0 1) n1))" } "n0 := n1 + 1;" {"Black: 36#(<= 1 n1)" "25#L37true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" })
		({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "14#L55true" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "5#L56true" })
		({"Black: 30#(= critical 0)" "17#L38true" "28#true" } "assume critical == 0;" {"Black: 28#true" "18#L39true" "30#(= critical 0)" })
		({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "25#L37true" } "assume n1 == 0 || n0 < n1;" {"17#L38true" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" })
		({"34#true" "41#true" "13#L60true" } "n1 := 0;" {"34#true" "41#true" "10#L54true" })
		({"Black: 30#(= critical 0)" "7#L57true" } "assume !(critical == 0);" {"Black: 30#(= critical 0)" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" })
		({"22#L41true" "45#(<= 1 n1)" } "n0 := 0;" {"20#L35true" "44#(and (= n0 0) (<= (+ n0 1) n1))" })
		({"Black: 28#true" "21#L40true" } "critical := 0;" {"Black: 28#true" "22#L41true" })
		({"10#L54true" } "assume true;" {"14#L55true" })
		({"Black: 28#true" "7#L57true" } "assume critical == 0;" {"Black: 28#true" "9#L58true" })
		({"Black: 28#true" "9#L58true" "30#(= critical 0)" } "critical := 1;" {"Black: 30#(= critical 0)" "28#true" "12#L59true" })
		({"Black: 30#(= critical 0)" "9#L58true" } "critical := 1;" {"Black: 30#(= critical 0)" "12#L59true" })
	},
	initialMarking = {"Black: 43#(= n0 0)" "Black: 30#(= critical 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "Black: 36#(<= 1 n1)" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "41#true" "27#~initENTRYtrue" "28#true" "15#~initENTRYtrue" },
	acceptingPlaces = {"6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"assume true;" "n1 := n0 + 1;" "assume n0 == 0 || n1 < n0;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n1 := 0;" "assume !true;" "assume true;" "assume true;" "n0 := n1 + 1;" "assume n1 == 0 || n0 < n1;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n0 := 0;" "assume !true;" "assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" },
	states = {"50#true" "51#false" "52#(<= 1 n1)" "53#(<= 2 n0)" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "56#(and (<= 2 n0) (<= 1 n1))" },
	initialStates = {"50#true" },
	finalStates = {"51#false" },
	transitions = {
		("50#true" "assume true;" "50#true")
		("50#true" "n1 := n0 + 1;" "50#true")
		("50#true" "assume n0 == 0 || n1 < n0;" "50#true")
		("50#true" "assume !(critical == 0);" "50#true")
		("50#true" "assume critical == 0;" "50#true")
		("50#true" "critical := 1;" "50#true")
		("50#true" "critical := 0;" "50#true")
		("50#true" "n1 := 0;" "50#true")
		("50#true" "assume true;" "50#true")
		("50#true" "n0 := n1 + 1;" "50#true")
		("50#true" "assume n1 == 0 || n0 < n1;" "50#true")
		("50#true" "assume !(critical == 0);" "50#true")
		("50#true" "assume critical == 0;" "50#true")
		("50#true" "critical := 1;" "50#true")
		("50#true" "critical := 0;" "50#true")
		("50#true" "n0 := 0;" "50#true")
		("50#true" "critical := 0;n0 := 0;n1 := 1;assume true;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "assume true;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "n0 := n1 + 1;" "56#(and (<= 2 n0) (<= 1 n1))")
		("52#(<= 1 n1)" "assume true;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "n1 := n0 + 1;" "50#true")
		("52#(<= 1 n1)" "assume n0 == 0 || n1 < n0;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "assume critical == 0;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "critical := 1;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "critical := 0;" "52#(<= 1 n1)")
		("52#(<= 1 n1)" "n1 := 0;" "50#true")
		("53#(<= 2 n0)" "assume n1 == 0 || n0 < n1;" "53#(<= 2 n0)")
		("53#(<= 2 n0)" "assume true;" "53#(<= 2 n0)")
		("53#(<= 2 n0)" "n1 := n0 + 1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("53#(<= 2 n0)" "assume critical == 0;" "53#(<= 2 n0)")
		("53#(<= 2 n0)" "critical := 1;" "53#(<= 2 n0)")
		("53#(<= 2 n0)" "critical := 0;" "53#(<= 2 n0)")
		("53#(<= 2 n0)" "n0 := 0;" "50#true")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume n1 == 0 || n0 < n1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume !(critical == 0);" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume critical == 0;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume n0 == 0 || n1 < n0;" "51#false")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "critical := 1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "critical := 0;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume !(critical == 0);" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "n0 := 0;" "52#(<= 1 n1)")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "assume critical == 0;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "critical := 1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "critical := 0;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("54#(and (<= 2 n0) (<= (+ n0 1) n1))" "n1 := 0;" "53#(<= 2 n0)")
		("56#(and (<= 2 n0) (<= 1 n1))" "assume n1 == 0 || n0 < n1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "assume true;" "56#(and (<= 2 n0) (<= 1 n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "n1 := n0 + 1;" "54#(and (<= 2 n0) (<= (+ n0 1) n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "assume n0 == 0 || n1 < n0;" "56#(and (<= 2 n0) (<= 1 n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "assume critical == 0;" "56#(and (<= 2 n0) (<= 1 n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "critical := 1;" "56#(and (<= 2 n0) (<= 1 n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "critical := 0;" "56#(and (<= 2 n0) (<= 1 n1))")
		("56#(and (<= 2 n0) (<= 1 n1))" "n1 := 0;" "53#(<= 2 n0)")
	}
);