---

1

There are exceptions to this rule, notably for the (Slime-)types in the expressions. The type-fields are not included in the constructors. The corresponding fields will be set later.

2

If one does not allow propositions like step_1_is_active, taking a transition can only disable another transition by deactivating its source steps, the guards will remain true.

3

If during a run a transition is taking which enters an already active step, the SFC is either built using a strange programming style or there is a mistake. But in principle, there seems to be no reason to enforce target steps to be inactive.