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

// Reveals bug in unfolding.

BranchingProcess bp = finitePrefix(ReservoirDogs);
print(numberOfConditions(bp));
assert(numberOfConditions(bp) == 8);

assert(!isEmpty(ReservoirDogs));


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