* A df-chain wrt a variable v used in the TUT starts with an input and ends with a cuse or a puse of v in the TUT before v is defined in the TUT, and this input affects this use of v in the TUT. Links in a df-chain must be distinct, so data dependency self-loops are ignored at this stage.

Examples about inputs, links for the ATM System can be found in the test log (testEFSM).
Examples about du-pairs, df-chains, a-paths for the ATM System can be found in the test log (testDF).

Home