Graphical Animations of State Machines

Updated at 2017 Jul 10 - Version 1.2


Some case studies for running tool:
1. Alternating Bit Protocol (ABP)

- The picture of state machine ABP: ABP.svg

- The input file for 150 states: inputABP.txt

- The input file for 500 states: inputABP500.txt

2. MCS protocol

- The picture of state machine MCS: MCS.svg

- The input file: inputMCS.txt

3. Qlock Mutual exclusion protocol

This case has a counterexample - loop

- The picture of state machine Qlock: qlock.svg

- Another picture of state machine Qlock: qlock2.svg

- The input file: inputQlock.txt

4. Mobile Robots Perpetual Exploration Algorithm (MRPEA)

- The picture of state machine MRPEA: ringRobot.svg

- The input file: Robot.txt

Maude function for generating a long sequence of states.

- The GENERATEPATH function: generateSeqSates.maude

- An example for using function to generate a long sequence of states of ABP: ABP.maude

Note: To make input file contains correctly sequence of states, please use command: '-no-wrap' in maude when starting maude.


User Guide Experiments About