// Author: heizmann@informatik.uni-freiburg.de
// Date:  2020-02-10
//
// Reveals bug in removeDead. Word accepted before but not afterwards.

assert(accepts(net, ["aym0" "aym1" "aym2" "ayo1" "ayo2" "ayo3" "ayo4" "ayt2" "ayo5" "ayt3" "ayt4" "ayt5" "aym3" "ayo6" "aym4" ]));
PetriNet vital = removeDead(net);
assert(accepts(vital, ["aym0" "aym1" "aym2" "ayo1" "ayo2" "ayo3" "ayo4" "ayt2" "ayo5" "ayt3" "ayt4" "ayt5" "aym3" "ayo6" "aym4" ]));

PetriNet net = (
	alphabet = {"a13" "ayt5" "ayt4" "ayt3" "ayt2" "a20" "a21" "a24" "a23" "a26" "a25" "a1" "ayo4" "aym2" "a2" "ayo3" "aym1" "aym4" "ayo6" "a4" "ayo5" "aym3" "a5" "aym0" "ayo2" "ayo1" },
	places = {"t4" "t5" "t6" "White:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:36#(<= 0 x)" "White:70#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 5 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:72#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 6 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "White:36#(<= 0 x)" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" "White:62#(and (<= 3 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o1" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o2" "o3" "m1" "o4" "m2" "White:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m3" "o5" "White:66#(and (<= 4 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m4" "o6" "o7" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "mAssert" "Black:72#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 6 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:70#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 5 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:50#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 0 x))" "White:34#true" "White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:62#(and (<= 3 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "t2" "t3" "mInit" "Black:66#(and (<= 4 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" },
	transitions = {
		({"o2" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "ayo2" {"o3" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" })
		({"o2" "White:50#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 0 x))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "ayo2" {"o3" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" })
		({"o2" "White:34#true" } "ayo2" {"o3" "White:34#true" })
		({"Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "t3" } "ayt3" {"t4" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"Black:72#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 6 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m4" "o7" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "aym4" {"Black:72#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 6 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "mAssert" })
		({"o3" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" } "ayo3" {"o4" "White:34#true" })
		({"Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "o3" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "ayo3" {"o4" "White:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" })
		({"o3" "White:34#true" } "ayo3" {"o4" "White:34#true" })
		({"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o6" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" } "ayo6" {"White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o7" })
		({"White:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o6" } "ayo6" {"White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o7" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"White:34#true" "o6" } "ayo6" {"White:34#true" "o7" })
		({"t6" "m3" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" } "aym3" {"White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "m4" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"t6" "m3" "White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "aym3" {"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m4" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t6" "m3" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "aym3" {"m4" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" })
		({"t6" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:70#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 5 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m3" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "Black:62#(and (<= 3 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:66#(and (<= 4 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "aym3" {"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:70#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 5 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m4" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "Black:62#(and (<= 3 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:66#(and (<= 4 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "t2" } "ayt2" {"White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "t3" })
		({"White:36#(<= 0 x)" "t2" } "ayt2" {"Black:36#(<= 0 x)" "White:34#true" "t3" })
		({"White:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "t2" } "ayt2" {"Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "t3" })
		({"White:50#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 0 x))" "t2" } "ayt2" {"White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "t3" })
		({"White:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "t2" } "ayt2" {"White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "t3" })
		({"White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "t2" } "ayt2" {"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" "t3" })
		({"White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "t2" } "ayt2" {"White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "t3" })
		({"t4" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" } "ayt4" {"t5" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"t4" "White:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "ayt4" {"t5" "Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t4" "White:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "ayt4" {"t5" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"t4" "White:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "ayt4" {"t5" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t4" "White:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" } "ayt4" {"t5" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" })
		({"t4" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" } "ayt4" {"t5" "White:37#(<= 0 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t4" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" } "ayt4" {"t5" "White:41#(<= 2 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t4" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" } "ayt4" {"t5" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" })
		({"t4" "White:34#true" } "ayt4" {"t5" "White:34#true" })
		({"o4" "White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" } "ayo4" {"o5" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"o4" "White:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" } "ayo4" {"Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "o5" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"o4" "White:34#true" } "ayo4" {"o5" "White:34#true" })
		({"t5" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "ayt5" {"t6" "Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"Black:36#(<= 0 x)" "White:34#true" "mInit" } "aym0" {"m1" "White:36#(<= 0 x)" })
		({"o1" "White:36#(<= 0 x)" } "ayo1" {"Black:36#(<= 0 x)" "o2" "White:50#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 0 x))" })
		({"o1" "Black:36#(<= 0 x)" } "ayo1" {"o2" "Black:36#(<= 0 x)" })
		({"o5" "White:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" } "ayo5" {"White:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "o6" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" })
		({"White:39#(<= 1 IncrementProcess1Thread1of1ForFork0_localx)" "o5" } "ayo5" {"White:34#true" "o6" })
		({"o5" "White:34#true" } "ayo5" {"White:34#true" "o6" })
		({"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m2" } "aym2" {"Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "m3" "t2" })
		({"m1" } "aym1" {"o1" "m2" })
	},
	initialMarking = {"Black:64#(and (<= 4 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:36#(<= 0 x)" "Black:68#(and (<= 5 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:52#(and (<= 0 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:58#(and (<= 2 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:72#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 6 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:54#(and (<= 1 IncrementProcess1Thread1of1ForFork0_localx) (<= 1 x))" "Black:60#(and (<= 3 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "Black:70#(and (<= 5 IncrementProcess2Thread1of1ForFork1_localx) (<= 5 x) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "White:34#true" "Black:56#(and (<= 2 x) (<= 1 IncrementProcess1Thread1of1ForFork0_localx))" "Black:62#(and (<= 3 x) (<= 3 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" "mInit" "Black:66#(and (<= 4 x) (<= 4 IncrementProcess2Thread1of1ForFork1_localx) (<= 2 IncrementProcess1Thread1of1ForFork0_localx))" },
	acceptingPlaces = {"mAssert" }
);