NodeOfEFSM holds the data stored for one state of the EFSM generated by function ComputeStateTrans. An EFSM is an array of such nodes, so that every node has its own index in the array. The initial node always has index 0. The contents of the record NodeOfEFSM is as follows:

• sccIndex is the index of the SCC of this node; this is also the index of the node reached first by the traversal in the same SCC.
• labels is the set of control flow labels that hold in the node.
• thisStmt is the Quartz statement associated with the node.
• rsdStmts is a set of pairs (phi,i) which mean that if condition phi holds now, a transition to EFSM node i will take place.
• surfActs is the set of guarded actions that are executed in this state.
• transfer maps each QName of a local variable to its transfer incarnations to determine their reaction to absence.
• instantC holds iff thisStmt instantaneouly terminats; it is the disjunction of the path conditions in rsdStmts.