Graphical Animations of State Machines

Last updated: 2022 May 05




Some case studies for running tool:
Aoki Rajkumar protocol (or the merging protocol or the AR protocol) - Updated by 2022 May 05

- The state picture template of the AR protocol (4 vehicles in non-through and through lanes, and 2 spaces): AR_4NT4T2S.svg

- The input file of the AR protocol with 48 states (2 vehilces in non-through lane, 4 in through lane and 2 spaces): inputAR_2NT4T2S_48

- The input file of the AR protocol with 49 states (2 vehilces in non-through lane, 4 in through lane and 2 spaces): inputAR_2NT4T2S_49

- The input file of the AR protocol with 50 states (2 vehilces in non-through lane, 4 in through lane and 2 spaces): inputAR_2NT4T2S_50

Needham-Schroeder-lowe public (NSLPK) protocol

- The picture of state machine of NSLPK protocol: NSLPK.svg

- The input file of NSLPK: inputNSLPK

- The sequence diagram for NSLPK protocol: sequenceDiagramDemo

- The input file of NSLPK for sequence diagram: inputNSLPK_sequencediagram

- The input file of NSPK for sequence diagram (nonce secret property): inputNSPK_sequencediagram

Lim-Jeong-Park-Lee protocol

- The revised picture of state machine revised LJPL protocol for situation 1: LJPL1.svg

- The revised picture of state machine revised LJPL protocol for situation 2: LJPL2.svg

- The flexible picture of state machine revised LJPL protocol: LJPL_flexible.svg

- The input file of LJPL for situation 1: inputLJPL1

- The input file of LJPL for situation 2: inputLJPL2

Anderson protocol

- The revised picture of state machine Anderson protocol for 3 processes: Anderson_revised_3P.svg

- The revised picture of state machine Anderson protocol for 4 processes: Anderson_revised_4P.svg

- The simple picture state machine Anderson protocol for 3 processes: Anderson_simple_3P.svg

- The input file of Anderson for 3 processes: inputAnderson_3P

- The input file of Anderson for 4 processes: inputAnderson_4P_200

MCS protocol

- The revised picture of state machine MCS: mcs_revised.svg

- The old picture state machine MCS: mcs_old.svg

- The simple picture state machine MCS: mcs_simple.svg

- The input file of MCS: inputMCS

- The revised picture of state machine MCS (7 processes): mcs_revised_7P.svg

- The input file of MCS (7 processes): inputMCS_7P

TVS

- The revised picture of state machine TVS: TVS_revised.svg

- The simple picture state machine TVS: TVS_simple.svg

- The input file of TVS: inputTVS

Suzuki-Kasami protocol (SKP)

- The picture of state machine SKP: SKP.svg

- The input file for 200 states (3 nodes, each node enters CS only once ): inputSKP_v1

- The input file for 1000 states (3 nodes, each node enters CS 10 times): inputSKP_v2

- The input file for 175 states (3 nodes, network can contain up to 15 messages): inputSKP_v15mes

Test And Set protocol (TAS)

- The revised picture of state machine TAS: TAS_revised.svg

- The simple picture state machine TAS: TAS_simple.svg

- The input file of TAS: inputTAS

Qlock & its variants

- The revised picture of state machine FQlock1: FQlock1_revised.svg

- The simple picture state machine FQlock0 or Fqlock1: FQlock_simple.svg

- The revised picture of state machine Qlock: Qlock_5p.svg

- The input file of FQlock0: inputFQlock0

- The input file of FQlock0_counterexample: inputFQlock0_CounterExample

- The input file of FQlock1: inputFQlock1

- The input file of Qlock: inputQlock

- The input file of Qlock(1k states): inputQlock_5p_1k

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 SKP: skp_generate.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