Decompose the WAIT2 component into WAIT for waiting the high level of non-persistent signal sig and WAIT0 for its low level. The control module W2C toggles between WAIT and WAIT0 according to the polarity of its ctrl input.

Behaviour of W2C is captured by the following STG.

Verify the STG for consistency, deadlocks, output-persistency and input-properness.

Note that this STG has CSC conflicts. Resolve them either automatically or manually, e.g. by concurrency reduction, as follows:

Proceed to synthesis and technology mapping with either MPSat or Petrify backend. The result should look similar to this:

Experiment with reset strategies using Initialisation analyser tool. One can notice that ctr input is initially set to 0 by CYCLE module, also C-element U2 can be explicitly reset. These lead to initialisation of ctrl_1 and ctrl_0 to 0, which reset san_1 and san_0 (outputs of WAIT and WAIT0).