Marking
After modeling the plants and requirements, marking should be considered. Every automaton, whether plant or requirement, must have at least one marked location. A marked location is a location that indicates a safe, stable, or resting state. Synthesis will guarantee that a marked location can always be reached, thus ensuring a form of liveness.
Physical systems typically keep operating, repeating their behavior. Therefore, in practice, the entire system can often be brought back to the initial state. As such, it is then typically enough to make the initial locations marked.
An exception is automata that have some kind of initialization behavior/sequence. For such automata, make the first location that is part of the loop after the initialization sequence, a marked location. The locations from the initialization sequence can no longer be reached after initialization is finished. The first location after that initialization sequence is part of the 'normal' behavior and can be seen as the initial location of the behavior after initialization.
Note that marking every location reduces the value of supervisor synthesis, as it essentially disables its non-blockingness guarantee. This may hide issues related to deadlocks and livelocks.
For advanced uses of marking, see the CIF language tutorial section on marker predicates.
The next step in the process to apply synthesis-based engineering in practice is to synthesize a supervisor.