A software tool for the automatic synthesis of minimally restrictive liveness enforcing supervisory policies for a class of general Petri net models of manufacturing- and service-systems.