Carnegie Mellon: The Rare Glitch Project                                                          E. Clarke and D. Kroenig
Abstraction Hierarchy: Formalization
Formalizing TTP/C
4
4
5
7
6
11
12
11
12
Msg Slot Level
Macro Tick Level
8
9
Slide shows states and transition relation. If one considers a transition from, e.g., state 4 to 11, there must be a path in  the machine for the lower level that starts in state 4 and ends in state 11. The number of transitions done by the lower level is fixed in this example (it is exactly the number of macro ticks for the given message slot).