Reachability analysis and simulation tools for high-level nets spend a significant amount of the computing time in performing enabling tests, determining the assignments under which transitions are enabled.
Unlike the majority of earlier work on computing enabled transition bindings, the techniques presented in this paper are highly independent of the algebraic operations supported by the high-level net formalism.
Performing enabling tests is viewed as a unification problem. A unification algorithm is presented and modifications to it are suggested. One variant of the algorithm constructs finite unfoldings for nets with unbounded domains. Some heuristics for optimising the enabling tests are discussed and their usefulness is evaluated based on experiments. The algorithms have been implemented in the reachability analyser Maria.
Analyse-Arcs
should be k>n or k=n+1.