On the automatic generation of the minimally restrictive liveness enforcing supervisory policy for manufacturing- and service-systems modeled by a class of general Free Choice Petri nets

References [1], [2] provide the theoretical underpinnings for the synthesis of a minimally restrictive, liveness enforcing supervisory policy (LESP) for ordinary Free-Choice Petri nets (FCPNs), and a class of general FCPNs. The observations in these references apply equally to other families of PNs that satisfy the property that the existence of an LESP for a member of the family implies that there is an LESP whenever the same structure is initialized with a larger marking (eg. [3]). In this paper we present, after a fashion, the implementation details of the procedures outlined in references [1], [2] using an illustrative example. We refer the reader to [4] for additional details and examples.