1. The formalization of Figure 5.31 has a minor flaw that may become relevant if the PN is part of a cyclic system. Find and fix the error (i.e., modify the PN in such a way that it behaves properly even if repeated cyclically). 2. Continue with the analysis of the preceding specifications, trying to discover ambiguous or questionable points. 3. Find other inadequacies and trouble spots in the foregoing initial formalization.