// Date:  30.3.2011
// Author: heizmann@informatik.uni-freiburg.de

assert(accepts(se7en, []));
assert(!accepts(se7en, [a b c]));
assert(accepts(se7en, [a a a]));
assert(accepts(se7en, [a b b a a]));
assert(!accepts(se7en, [a c ]));
assert(!accepts(se7en, [a b c a a]));
assert(accepts(se7en, [a a a c]));
assert(!accepts(se7en, [a a a b c]));
assert(accepts(se7en, [a a a c b]));

assert(!isEmpty(se7en));
print(finitePrefix( se7en));


PetriNet se7en = (
  alphabet = {a b c},
  places = {p0 p1 p2 q0 q1 q2 q3},
  transitions = {
    ({p0 q0} c {p0 q0}) 
    ({p0} a {p1}) 
    ({p1} a {p2}) 
    ({p2} a {p0}) 
    ({q0} b {q1}) 
    ({q1} b {q2}) 
    ({q2} b {q3}) 
    ({q3} b {q0})},
  initialMarking = {p0 q0},
  acceptingPlaces = {p0 q0}
);