Petrify reads a Signal Transition Graph (STG) and generates another STG which should be simpler than the original description. Initially, petrify performs a token flow analysis of the initial STG and produces a transition system (TS). In the initial TS, all transitions with the same label are considered as one event. The TS is then transformed and transitions relabeled to fulfill the conditions required to obtain an STG.
Full details and