// Example that demonstates how we can use PetriNet in
// this automata library.
// Author: heizmann@informatik.uni-freiburg.de
// Date: 2013-04-28

// We use 1-bounded Petri nets as acceptors for languages. Some regular 
// languages can be represented more succinct by petri net than by finite
// automata. E.g., the following Petri net accepts all word that end with the
// letter f and contain exactly one a, one b, one c, one d, and one e.
PetriNet oneOfEach = (
	alphabet = {a b c d e f},
	places = {p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11},
	transitions = {
		({p1} a {p2})
		({p3} b {p4})
		({p5} c {p6})
		({p7} d {p8})
		({p9} e {p10})
		({p2 p4 p6 p8 p10} f {p11})
	},
	initialMarking = {p1 p3 p5 p7 p9},
	acceptingPlaces = {p11}
);

// E.g., the following word is accepted.
assert(accepts(oneOfEach, [ e c d b a f ]));

// However the smallest deterministic finite automaton that accpets the same
// language has 33 states.
print(numberOfStates(minimizeDfaTable(petriNet2FiniteAutomaton(oneOfEach))));

// The following operation (developed by Julian Jarecki) checks if the language
// of a Petri net is empty. The basis of this algorithm is the Petri net 
// unfolding that was presented in the following publication.
// 1996TACAS - Esparza,Römer,Vogler - An Improvement of McMillan's Unfolding Algorithm
assert(!isEmpty(oneOfEach));
assert(isEmpty(acceptingNotReachable));

PetriNet acceptingNotReachable = (
	alphabet = { a },
	places = {p0 p1 p2 p3},
	transitions = {
		({p0} a {p1})
		({p0} a {p2})
		({p1 p2} a {p3})
	},
	initialMarking = {p0},
	acceptingPlaces = {p3}
);