// Benchmark for difference of Petri net and DFA  
// Generated from
// SAS09.bpl_AllErrorsAtOnce_Iteration2_AbstractionAfterDifference.ats (2018/07/30 09:55:00)
// SAS09.bpl_AllErrorsAtOnce_Iteration3_EagerFloydHoareAutomaton.ats (2018/07/30 09:55:00)


PetriNet net = (
	alphabet = {"critical := 0;assume true;" "#0#a := 0;" "#1#b := 0;" "#5#assume true;" "#6#a := a + 1;" "#8#assume !(a != -1);" "#9#assume a != -1;" "#10#assume !(b != -1);" "#11#assume b != -1;" "#12#assume true;" "#15#x := 0;" "#16#y := 0;" "#17#g := 0;" "#21#assume true;" "#22#x := x + 1;" "#23#g := g + 1;" "#25#assume !(x != -1);" "#26#assume x != -1;" "#27#assume !(y != -1);" "#28#assume y != -1;" "#29#assume !(g != -1);" "#30#assume g != -1;" "#31#assume true;" },
	places = {"5#Thread2FINALtrue" "6#L53-1true" "7#L59true" "8#Thread2Err1ASSERT_VIOLATIONASSERTtrue" "9#L54true" "10#Thread2ENTRYtrue" "11#L51true" "12#Thread2EXITtrue" "13#Thread2Err0ASSERT_VIOLATIONASSERTtrue" "14#~initENTRYtrue" "16#Thread1ENTRYtrue" "17#L37true" "18#L38true" "19#Thread1Err2ASSERT_VIOLATIONASSERTtrue" "20#L28true" "21#L29true" "22#L31-1true" "23#Thread1FINALtrue" "24#L32true" "25#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "26#Thread1EXITtrue" "27#Thread1Err1ASSERT_VIOLATIONASSERTtrue" "28#L33true" "29#~initENTRYtrue" "30#true" "32#(<= 0 Thread2_a)" "Black: 32#(<= 0 Thread2_a)" "Black: 30#true" "36#true" "38#(<= 0 Thread1_x)" "Black: 36#true" "Black: 38#(<= 0 Thread1_x)" },
	transitions = {
		({"22#L31-1true" } "#21#assume true;" {"24#L32true" })
		({"29#~initENTRYtrue" "14#~initENTRYtrue" } "critical := 0;assume true;" {"16#Thread1ENTRYtrue" "10#Thread2ENTRYtrue" })
		({"18#L38true" } "#29#assume !(g != -1);" {"19#Thread1Err2ASSERT_VIOLATIONASSERTtrue" })
		({"20#L28true" } "#16#y := 0;" {"21#L29true" })
		({"28#L33true" } "#23#g := g + 1;" {"22#L31-1true" })
		({"Black: 30#true" "10#Thread2ENTRYtrue" } "#0#a := 0;" {"Black: 30#true" "11#L51true" })
		({"22#L31-1true" "Black: 38#(<= 0 Thread1_x)" } "#25#assume !(x != -1);" {"25#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "Black: 38#(<= 0 Thread1_x)" })
		({"16#Thread1ENTRYtrue" "36#true" "Black: 38#(<= 0 Thread1_x)" } "#15#x := 0;" {"20#L28true" "38#(<= 0 Thread1_x)" "Black: 36#true" })
		({"6#L53-1true" } "#9#assume a != -1;" {"7#L59true" })
		({"6#L53-1true" } "#5#assume true;" {"9#L54true" })
		({"21#L29true" } "#17#g := 0;" {"22#L31-1true" })
		({"7#L59true" } "#11#assume b != -1;" {"5#Thread2FINALtrue" })
		({"22#L31-1true" } "#26#assume x != -1;" {"17#L37true" })
		({"Black: 32#(<= 0 Thread2_a)" "10#Thread2ENTRYtrue" "30#true" } "#0#a := 0;" {"32#(<= 0 Thread2_a)" "Black: 30#true" "11#L51true" })
		({"18#L38true" } "#30#assume g != -1;" {"23#Thread1FINALtrue" })
		({"Black: 32#(<= 0 Thread2_a)" "6#L53-1true" } "#8#assume !(a != -1);" {"Black: 32#(<= 0 Thread2_a)" "13#Thread2Err0ASSERT_VIOLATIONASSERTtrue" })
		({"16#Thread1ENTRYtrue" "Black: 36#true" } "#15#x := 0;" {"20#L28true" "Black: 36#true" })
		({"17#L37true" } "#27#assume !(y != -1);" {"27#Thread1Err1ASSERT_VIOLATIONASSERTtrue" })
		({"17#L37true" } "#28#assume y != -1;" {"18#L38true" })
		({"9#L54true" } "#6#a := a + 1;" {"6#L53-1true" })
		({"7#L59true" } "#10#assume !(b != -1);" {"8#Thread2Err1ASSERT_VIOLATIONASSERTtrue" })
		({"5#Thread2FINALtrue" } "#12#assume true;" {"12#Thread2EXITtrue" })
		({"11#L51true" } "#1#b := 0;" {"6#L53-1true" })
		({"24#L32true" } "#22#x := x + 1;" {"28#L33true" })
		({"23#Thread1FINALtrue" } "#31#assume true;" {"26#Thread1EXITtrue" })
	},
	initialMarking = {"Black: 32#(<= 0 Thread2_a)" "36#true" "Black: 38#(<= 0 Thread1_x)" "29#~initENTRYtrue" "14#~initENTRYtrue" "30#true" },
	acceptingPlaces = {"19#Thread1Err2ASSERT_VIOLATIONASSERTtrue" "8#Thread2Err1ASSERT_VIOLATIONASSERTtrue" "25#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "27#Thread1Err1ASSERT_VIOLATIONASSERTtrue" "13#Thread2Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"critical := 0;assume true;" "#0#a := 0;" "#1#b := 0;" "#5#assume true;" "#6#a := a + 1;" "#8#assume !(a != -1);" "#9#assume a != -1;" "#10#assume !(b != -1);" "#11#assume b != -1;" "#12#assume true;" "#15#x := 0;" "#16#y := 0;" "#17#g := 0;" "#21#assume true;" "#22#x := x + 1;" "#23#g := g + 1;" "#25#assume !(x != -1);" "#26#assume x != -1;" "#27#assume !(y != -1);" "#28#assume y != -1;" "#29#assume !(g != -1);" "#30#assume g != -1;" "#31#assume true;" },
	states = {"42#true" "43#false" "44#(<= 0 Thread2_b)" },
	initialStates = {"42#true" },
	finalStates = {"43#false" },
	transitions = {
		("42#true" "critical := 0;assume true;" "42#true")
		("42#true" "#0#a := 0;" "42#true")
		("42#true" "#1#b := 0;" "44#(<= 0 Thread2_b)")
		("42#true" "#5#assume true;" "42#true")
		("42#true" "#6#a := a + 1;" "42#true")
		("42#true" "#8#assume !(a != -1);" "42#true")
		("42#true" "#9#assume a != -1;" "42#true")
		("42#true" "#10#assume !(b != -1);" "42#true")
		("42#true" "#11#assume b != -1;" "42#true")
		("42#true" "#12#assume true;" "42#true")
		("42#true" "#15#x := 0;" "42#true")
		("42#true" "#16#y := 0;" "42#true")
		("42#true" "#17#g := 0;" "42#true")
		("42#true" "#21#assume true;" "42#true")
		("42#true" "#22#x := x + 1;" "42#true")
		("42#true" "#23#g := g + 1;" "42#true")
		("42#true" "#25#assume !(x != -1);" "42#true")
		("42#true" "#26#assume x != -1;" "42#true")
		("42#true" "#27#assume !(y != -1);" "42#true")
		("42#true" "#28#assume y != -1;" "42#true")
		("42#true" "#29#assume !(g != -1);" "42#true")
		("42#true" "#30#assume g != -1;" "42#true")
		("42#true" "#31#assume true;" "42#true")
		("43#false" "critical := 0;assume true;" "43#false")
		("43#false" "#0#a := 0;" "43#false")
		("43#false" "#1#b := 0;" "43#false")
		("43#false" "#5#assume true;" "43#false")
		("43#false" "#6#a := a + 1;" "43#false")
		("43#false" "#8#assume !(a != -1);" "43#false")
		("43#false" "#9#assume a != -1;" "43#false")
		("43#false" "#10#assume !(b != -1);" "43#false")
		("43#false" "#11#assume b != -1;" "43#false")
		("43#false" "#12#assume true;" "43#false")
		("43#false" "#15#x := 0;" "43#false")
		("43#false" "#16#y := 0;" "43#false")
		("43#false" "#17#g := 0;" "43#false")
		("43#false" "#21#assume true;" "43#false")
		("43#false" "#22#x := x + 1;" "43#false")
		("43#false" "#23#g := g + 1;" "43#false")
		("43#false" "#25#assume !(x != -1);" "43#false")
		("43#false" "#26#assume x != -1;" "43#false")
		("43#false" "#27#assume !(y != -1);" "43#false")
		("43#false" "#28#assume y != -1;" "43#false")
		("43#false" "#29#assume !(g != -1);" "43#false")
		("43#false" "#30#assume g != -1;" "43#false")
		("43#false" "#31#assume true;" "43#false")
		("44#(<= 0 Thread2_b)" "critical := 0;assume true;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#0#a := 0;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#1#b := 0;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#5#assume true;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#6#a := a + 1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#8#assume !(a != -1);" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#9#assume a != -1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#10#assume !(b != -1);" "43#false")
		("44#(<= 0 Thread2_b)" "#11#assume b != -1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#12#assume true;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#15#x := 0;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#16#y := 0;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#17#g := 0;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#21#assume true;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#22#x := x + 1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#23#g := g + 1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#25#assume !(x != -1);" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#26#assume x != -1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#27#assume !(y != -1);" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#28#assume y != -1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#29#assume !(g != -1);" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#30#assume g != -1;" "44#(<= 0 Thread2_b)")
		("44#(<= 0 Thread2_b)" "#31#assume true;" "44#(<= 0 Thread2_b)")
	}
);