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


PetriNet net = (
	alphabet = {"#2#x := x + 2;" "#3#assume true;" "#4#x := x + 1;" "#5#assume !(x <= 3);" "#6#assume x <= 3;" "#7#assume true;" "x := 0;assume true;" },
	places = {"5#Thread1ENTRYtrue" "6#Thread1FINALtrue" "7#Thread1EXITtrue" "8#~initENTRYtrue" "10#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "11#Thread0FINALtrue" "12#Thread0ENTRYtrue" "13#Thread0EXITtrue" "14#L27true" "15#~initENTRYtrue" "16#true" "18#(<= x 0)" "19#(<= x 1)" "21#true" "23#(<= x 0)" "24#(<= x 2)" "25#(<= x 3)" "Black: 21#true" },
	transitions = {
		({"16#true" "25#(<= x 3)" "Black: 21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "21#true" "14#L27true" })
		({"18#(<= x 0)" "5#Thread1ENTRYtrue" "25#(<= x 3)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"19#(<= x 1)" "5#Thread1ENTRYtrue" "24#(<= x 2)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"16#true" "5#Thread1ENTRYtrue" "23#(<= x 0)" } "#2#x := x + 2;" {"16#true" "6#Thread1FINALtrue" "24#(<= x 2)" })
		({"19#(<= x 1)" "23#(<= x 0)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "24#(<= x 2)" "14#L27true" })
		({"18#(<= x 0)" "8#~initENTRYtrue" "25#(<= x 3)" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"6#Thread1FINALtrue" } "#3#assume true;" {"7#Thread1EXITtrue" })
		({"19#(<= x 1)" "24#(<= x 2)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"18#(<= x 0)" "23#(<= x 0)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"19#(<= x 1)" "24#(<= x 2)" "14#L27true" })
		({"19#(<= x 1)" "5#Thread1ENTRYtrue" "25#(<= x 3)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"18#(<= x 0)" "21#true" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "Black: 21#true" "12#Thread0ENTRYtrue" })
		({"21#true" "14#L27true" } "#6#assume x <= 3;" {"25#(<= x 3)" "Black: 21#true" "11#Thread0FINALtrue" })
		({"16#true" "23#(<= x 0)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"19#(<= x 1)" "8#~initENTRYtrue" "25#(<= x 3)" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"16#true" "21#true" "5#Thread1ENTRYtrue" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"19#(<= x 1)" "21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "21#true" "14#L27true" })
		({"19#(<= x 1)" "24#(<= x 2)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "25#(<= x 3)" "14#L27true" })
		({"16#true" "5#Thread1ENTRYtrue" "24#(<= x 2)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"16#true" "23#(<= x 0)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "24#(<= x 2)" "14#L27true" })
		({"18#(<= x 0)" "21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"19#(<= x 1)" "21#true" "14#L27true" })
		({"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" } "#2#x := x + 2;" {"16#true" "6#Thread1FINALtrue" "24#(<= x 2)" })
		({"19#(<= x 1)" "21#true" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "Black: 21#true" "12#Thread0ENTRYtrue" })
		({"18#(<= x 0)" "24#(<= x 2)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"19#(<= x 1)" "25#(<= x 3)" "14#L27true" })
		({"16#true" "24#(<= x 2)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"16#true" "5#Thread1ENTRYtrue" "25#(<= x 3)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"19#(<= x 1)" "25#(<= x 3)" "Black: 21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "21#true" "14#L27true" })
		({"19#(<= x 1)" "5#Thread1ENTRYtrue" "23#(<= x 0)" } "#2#x := x + 2;" {"16#true" "6#Thread1FINALtrue" "24#(<= x 2)" })
		({"18#(<= x 0)" "23#(<= x 0)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"16#true" "8#~initENTRYtrue" "25#(<= x 3)" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"16#true" "21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "21#true" "14#L27true" })
		({"18#(<= x 0)" "21#true" "5#Thread1ENTRYtrue" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"16#true" "21#true" "14#L27true" } "#5#assume !(x <= 3);" {"16#true" "21#true" "10#Thread0Err0ASSERT_VIOLATIONASSERTtrue" })
		({"18#(<= x 0)" "25#(<= x 3)" "Black: 21#true" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"19#(<= x 1)" "21#true" "14#L27true" })
		({"16#true" "24#(<= x 2)" "12#Thread0ENTRYtrue" } "#4#x := x + 1;" {"16#true" "25#(<= x 3)" "14#L27true" })
		({"Black: 21#true" "14#L27true" } "#6#assume x <= 3;" {"11#Thread0FINALtrue" "Black: 21#true" })
		({"18#(<= x 0)" "5#Thread1ENTRYtrue" "24#(<= x 2)" "Black: 21#true" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"16#true" "21#true" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "Black: 21#true" "12#Thread0ENTRYtrue" })
		({"18#(<= x 0)" "24#(<= x 2)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"19#(<= x 1)" "23#(<= x 0)" "8#~initENTRYtrue" "15#~initENTRYtrue" } "x := 0;assume true;" {"18#(<= x 0)" "5#Thread1ENTRYtrue" "23#(<= x 0)" "12#Thread0ENTRYtrue" })
		({"19#(<= x 1)" "21#true" "5#Thread1ENTRYtrue" } "#2#x := x + 2;" {"16#true" "21#true" "6#Thread1FINALtrue" })
		({"11#Thread0FINALtrue" } "#7#assume true;" {"13#Thread0EXITtrue" })
	},
	initialMarking = {"16#true" "21#true" "8#~initENTRYtrue" "15#~initENTRYtrue" },
	acceptingPlaces = {"10#Thread0Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"#2#x := x + 2;" "#3#assume true;" "#4#x := x + 1;" "#5#assume !(x <= 3);" "#6#assume x <= 3;" "#7#assume true;" "x := 0;assume true;" },
	states = {"32#(<= x 3)" "28#true" "29#false" "30#(<= x 0)" "31#(<= x 1)" },
	initialStates = {"28#true" },
	finalStates = {"29#false" },
	transitions = {
		("32#(<= x 3)" "#2#x := x + 2;" "28#true")
		("32#(<= x 3)" "#3#assume true;" "32#(<= x 3)")
		("32#(<= x 3)" "#4#x := x + 1;" "28#true")
		("32#(<= x 3)" "#5#assume !(x <= 3);" "29#false")
		("32#(<= x 3)" "#6#assume x <= 3;" "32#(<= x 3)")
		("32#(<= x 3)" "#7#assume true;" "32#(<= x 3)")
		("32#(<= x 3)" "x := 0;assume true;" "30#(<= x 0)")
		("28#true" "#2#x := x + 2;" "28#true")
		("28#true" "#3#assume true;" "28#true")
		("28#true" "#4#x := x + 1;" "28#true")
		("28#true" "#5#assume !(x <= 3);" "28#true")
		("28#true" "#6#assume x <= 3;" "32#(<= x 3)")
		("28#true" "#7#assume true;" "28#true")
		("28#true" "x := 0;assume true;" "30#(<= x 0)")
		("29#false" "#2#x := x + 2;" "29#false")
		("29#false" "#3#assume true;" "29#false")
		("29#false" "#4#x := x + 1;" "29#false")
		("29#false" "#5#assume !(x <= 3);" "29#false")
		("29#false" "#6#assume x <= 3;" "29#false")
		("29#false" "#7#assume true;" "29#false")
		("29#false" "x := 0;assume true;" "29#false")
		("30#(<= x 0)" "#2#x := x + 2;" "32#(<= x 3)")
		("30#(<= x 0)" "#3#assume true;" "30#(<= x 0)")
		("30#(<= x 0)" "#4#x := x + 1;" "31#(<= x 1)")
		("30#(<= x 0)" "#5#assume !(x <= 3);" "29#false")
		("30#(<= x 0)" "#6#assume x <= 3;" "30#(<= x 0)")
		("30#(<= x 0)" "#7#assume true;" "30#(<= x 0)")
		("30#(<= x 0)" "x := 0;assume true;" "30#(<= x 0)")
		("31#(<= x 1)" "#2#x := x + 2;" "32#(<= x 3)")
		("31#(<= x 1)" "#3#assume true;" "31#(<= x 1)")
		("31#(<= x 1)" "#4#x := x + 1;" "32#(<= x 3)")
		("31#(<= x 1)" "#5#assume !(x <= 3);" "29#false")
		("31#(<= x 1)" "#6#assume x <= 3;" "31#(<= x 1)")
		("31#(<= x 1)" "#7#assume true;" "31#(<= x 1)")
		("31#(<= x 1)" "x := 0;assume true;" "30#(<= x 0)")
	}
);