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

PetriNet net = (
	alphabet = {"assume true;" "assume lock != 2;" "deadline := clk + delay;" "assume lock == 0;" "lock := 2;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 2;" "assume !(lock != 2);" "assume !(critical == 0);" "assume critical == 0;" "critical := 2;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "assume true;" "clk := clk + 1;" "assume !true;" "assume true;" "assume true;" "assume lock != 1;" "deadline := clk + delay;" "assume lock == 0;" "lock := 1;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 1;" "assume !(lock != 1);" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" },
	places = {"5#L79true" "6#L80true" "7#L81true" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" "9#L82true" "10#L75-2true" "12#L85true" "13#L74true" "14#L75true" "15#L86true" "16#L87true" "17#L76true" "18#L77true" "20#L78true" "21#~initENTRYtrue" "25#L34true" "26#L35true" "27#~initENTRYtrue" "29#L56true" "30#L57true" "31#L58true" "32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "33#L51-2true" "34#L50true" "35#L61true" "36#L62true" "37#L51true" "38#L52true" "40#L63true" "41#L53true" "42#L54true" "44#L55true" "45#~initENTRYtrue" "46#true" "48#(= critical 0)" "Black: 48#(= critical 0)" "Black: 46#true" },
	transitions = {
		({"Black: 48#(= critical 0)" "46#true" "15#L86true" } "critical := 0;" {"48#(= critical 0)" "16#L87true" "Black: 46#true" })
		({"Black: 46#true" "10#L75-2true" } "assume critical == 0;" {"Black: 46#true" "12#L85true" })
		({"5#L79true" } "assume clk <= deadline;" {"6#L80true" })
		({"25#L34true" } "assume true;" {"26#L35true" })
		({"31#L58true" } "assume lock == 1;" {"33#L51-2true" })
		({"18#L77true" } "assume lock == 0;" {"20#L78true" })
		({"38#L52true" } "deadline := clk + delay;" {"41#L53true" })
		({"48#(= critical 0)" "Black: 46#true" "35#L61true" } "critical := 1;" {"Black: 48#(= critical 0)" "36#L62true" "46#true" })
		({"Black: 46#true" "36#L62true" } "critical := 0;" {"Black: 46#true" "40#L63true" })
		({"Black: 48#(= critical 0)" "35#L61true" } "critical := 1;" {"Black: 48#(= critical 0)" "36#L62true" })
		({"44#L55true" } "assume clk <= deadline;" {"29#L56true" })
		({"13#L74true" } "assume true;" {"14#L75true" })
		({"33#L51-2true" "Black: 48#(= critical 0)" } "assume !(critical == 0);" {"32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "Black: 48#(= critical 0)" })
		({"Black: 48#(= critical 0)" "10#L75-2true" } "assume !(critical == 0);" {"Black: 48#(= critical 0)" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" })
		({"26#L35true" } "clk := clk + 1;" {"25#L34true" })
		({"29#L56true" } "deadline := clk + wait;" {"30#L57true" })
		({"33#L51-2true" "Black: 48#(= critical 0)" "46#true" } "assume critical == 0;" {"48#(= critical 0)" "Black: 46#true" "35#L61true" })
		({"42#L54true" } "lock := 1;" {"44#L55true" })
		({"6#L80true" } "deadline := clk + wait;" {"7#L81true" })
		({"40#L63true" } "lock := 0;" {"34#L50true" })
		({"Black: 48#(= critical 0)" "10#L75-2true" "46#true" } "assume critical == 0;" {"48#(= critical 0)" "Black: 46#true" "12#L85true" })
		({"37#L51true" } "assume !(lock != 1);" {"33#L51-2true" })
		({"9#L82true" } "assume lock == 2;" {"10#L75-2true" })
		({"48#(= critical 0)" "Black: 46#true" "12#L85true" } "critical := 2;" {"Black: 48#(= critical 0)" "46#true" "15#L86true" })
		({"Black: 48#(= critical 0)" "12#L85true" } "critical := 2;" {"Black: 48#(= critical 0)" "15#L86true" })
		({"Black: 48#(= critical 0)" "36#L62true" "46#true" } "critical := 0;" {"48#(= critical 0)" "Black: 46#true" "40#L63true" })
		({"14#L75true" } "assume !(lock != 2);" {"10#L75-2true" })
		({"37#L51true" } "assume lock != 1;" {"38#L52true" })
		({"16#L87true" } "lock := 0;" {"13#L74true" })
		({"Black: 46#true" "15#L86true" } "critical := 0;" {"16#L87true" "Black: 46#true" })
		({"30#L57true" } "assume clk >= deadline;" {"31#L58true" })
		({"17#L76true" } "deadline := clk + delay;" {"18#L77true" })
		({"34#L50true" } "assume true;" {"37#L51true" })
		({"Black: 48#(= critical 0)" "21#~initENTRYtrue" "27#~initENTRYtrue" "45#~initENTRYtrue" "46#true" } "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" {"48#(= critical 0)" "34#L50true" "Black: 46#true" "25#L34true" "13#L74true" })
		({"7#L81true" } "assume clk >= deadline;" {"9#L82true" })
		({"41#L53true" } "assume lock == 0;" {"42#L54true" })
		({"14#L75true" } "assume lock != 2;" {"17#L76true" })
		({"33#L51-2true" "Black: 46#true" } "assume critical == 0;" {"35#L61true" "Black: 46#true" })
		({"20#L78true" } "lock := 2;" {"5#L79true" })
	},
	initialMarking = {"Black: 48#(= critical 0)" "21#~initENTRYtrue" "27#~initENTRYtrue" "45#~initENTRYtrue" "46#true" },
	acceptingPlaces = {"32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" }
);

FiniteAutomaton nwa = (
	alphabet = {"assume true;" "assume lock != 2;" "deadline := clk + delay;" "assume lock == 0;" "lock := 2;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 2;" "assume !(lock != 2);" "assume !(critical == 0);" "assume critical == 0;" "critical := 2;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "assume true;" "clk := clk + 1;" "assume !true;" "assume true;" "assume true;" "assume lock != 1;" "deadline := clk + delay;" "assume lock == 0;" "lock := 1;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 1;" "assume !(lock != 1);" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" },
	states = {"52#true" "53#false" "54#(<= lock 1)" },
	initialStates = {"52#true" },
	finalStates = {"53#false" },
	transitions = {
		("52#true" "assume true;" "52#true")
		("52#true" "assume lock != 2;" "52#true")
		("52#true" "deadline := clk + delay;" "52#true")
		("52#true" "assume lock == 0;" "54#(<= lock 1)")
		("52#true" "assume clk <= deadline;" "52#true")
		("52#true" "deadline := clk + wait;" "52#true")
		("52#true" "assume clk >= deadline;" "52#true")
		("52#true" "assume lock == 2;" "52#true")
		("52#true" "assume !(lock != 2);" "52#true")
		("52#true" "assume !(critical == 0);" "52#true")
		("52#true" "assume critical == 0;" "52#true")
		("52#true" "critical := 2;" "52#true")
		("52#true" "critical := 0;" "52#true")
		("52#true" "lock := 0;" "54#(<= lock 1)")
		("52#true" "assume true;" "52#true")
		("52#true" "clk := clk + 1;" "52#true")
		("52#true" "assume true;" "52#true")
		("52#true" "assume lock != 1;" "52#true")
		("52#true" "deadline := clk + delay;" "52#true")
		("52#true" "assume lock == 0;" "54#(<= lock 1)")
		("52#true" "lock := 1;" "54#(<= lock 1)")
		("52#true" "assume clk <= deadline;" "52#true")
		("52#true" "deadline := clk + wait;" "52#true")
		("52#true" "assume clk >= deadline;" "52#true")
		("52#true" "assume lock == 1;" "54#(<= lock 1)")
		("52#true" "assume !(lock != 1);" "54#(<= lock 1)")
		("52#true" "assume !(critical == 0);" "52#true")
		("52#true" "assume critical == 0;" "52#true")
		("52#true" "critical := 1;" "52#true")
		("52#true" "critical := 0;" "52#true")
		("52#true" "lock := 0;" "54#(<= lock 1)")
		("52#true" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" "52#true")
		("54#(<= lock 1)" "assume true;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock != 2;" "54#(<= lock 1)")
		("54#(<= lock 1)" "deadline := clk + delay;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock == 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "lock := 2;" "52#true")
		("54#(<= lock 1)" "assume clk <= deadline;" "54#(<= lock 1)")
		("54#(<= lock 1)" "deadline := clk + wait;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume clk >= deadline;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock == 2;" "53#false")
		("54#(<= lock 1)" "assume !(lock != 2);" "53#false")
		("54#(<= lock 1)" "assume !(critical == 0);" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume critical == 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "critical := 2;" "54#(<= lock 1)")
		("54#(<= lock 1)" "critical := 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "lock := 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume true;" "54#(<= lock 1)")
		("54#(<= lock 1)" "clk := clk + 1;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume true;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock != 1;" "54#(<= lock 1)")
		("54#(<= lock 1)" "deadline := clk + delay;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock == 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "lock := 1;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume clk <= deadline;" "54#(<= lock 1)")
		("54#(<= lock 1)" "deadline := clk + wait;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume clk >= deadline;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume lock == 1;" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume !(lock != 1);" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume !(critical == 0);" "54#(<= lock 1)")
		("54#(<= lock 1)" "assume critical == 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "critical := 1;" "54#(<= lock 1)")
		("54#(<= lock 1)" "critical := 0;" "54#(<= lock 1)")
		("54#(<= lock 1)" "lock := 0;" "54#(<= lock 1)")
	}
);