// Benchmark for difference of Petri net and DFA  
// Generated from
// SimpleParallelProgram.bpl_AllErrorsAtOnce_Iteration2_AbstractionAfterDifference.ats (2018/08/13 05:05:49)
// SimpleParallelProgram.bpl_AllErrorsAtOnce_Iteration3_EagerFloydHoareAutomaton.ats (2018/08/13 05:05:49)

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

FiniteAutomaton nwa = (
	alphabet = {"x := x + 2;" "assume true;" "x := x + 1;" "assume !(x <= 3);" "assume x <= 3;" "assume true;" "x := 0;assume true;" },
	states = {"32#false" "33#(<= x 0)" "34#(<= x 1)" "35#(<= x 3)" "31#true" },
	initialStates = {"31#true" },
	finalStates = {"32#false" },
	transitions = {
		("33#(<= x 0)" "x := x + 2;" "35#(<= x 3)")
		("33#(<= x 0)" "x := x + 1;" "34#(<= x 1)")
		("34#(<= x 1)" "x := x + 2;" "35#(<= x 3)")
		("34#(<= x 1)" "assume x <= 3;" "34#(<= x 1)")
		("34#(<= x 1)" "assume true;" "34#(<= x 1)")
		("35#(<= x 3)" "assume true;" "35#(<= x 3)")
		("35#(<= x 3)" "x := x + 1;" "31#true")
		("35#(<= x 3)" "assume !(x <= 3);" "32#false")
		("35#(<= x 3)" "assume x <= 3;" "35#(<= x 3)")
		("35#(<= x 3)" "assume true;" "35#(<= x 3)")
		("31#true" "assume true;" "31#true")
		("31#true" "assume x <= 3;" "35#(<= x 3)")
		("31#true" "x := 0;assume true;" "33#(<= x 0)")
	}
);