// Author: schuessf@informatik.uni-freiburg.de
// Date: 2023-05-10

PetriNet net = (
  alphabet = {a b c d e f g h},
  places = {p1 p2 p3 p4 p5 p6},
  transitions = {
    ({p1} a {p2})
    ({p1} b {p3})
    ({p1} c {p4})
    ({p2} d {p5})
    ({p3} e {p6})
    ({p4} f {p3})
    ({p5} g {p4})
    ({p6} h {p5})
  },
  initialMarking = {p1},
  acceptingPlaces = {p3}
);

assert(!buchiIsEmpty(net));