FrontSOS holds the result of a single symbolic rule application of the SOS rules, i.e., of a single macro step of a statement S. The meaning of the components are as follows:

• rsdStmts is a set of triples (phi,lbls,S') such that statement S' would have to be executed in the next step if now phi holds. S' is thereby resumed from the control flow labels lbls. If statement S instantaneously terminates, rsdStmts is an empty set.
• surfActs are guarded actions that belong to the surface of S.
• instantC is the condition for instantaneous execution of S.
• transfer holds the information to select the right reincarnations of the local variables (see documentation of Transfer).
• substLVs is the final renaming of the local variables of S.
• labels is the set of labels that occur in statement S.

Note that he disjunction of the path conditions in rsdStmts is the negation of the instant predicate instantC. The enter predicate can also be constructed as a kind of disjunction of the rsdStmts that tells us under which condition phi we enter a residual statement S'.