Skip to content

Latest commit

 

History

History
120 lines (89 loc) · 3.26 KB

clock-sync-steps.md

File metadata and controls

120 lines (89 loc) · 3.26 KB
Raw

Clock Synchronization with Apalache

Version 1: Introducing clocks

  1. Open ClockSync1 and MC_ClockSync1.

  2. Notice how the variables time, hc, and adj are declared.

  3. Check the type annotations that start with @type.

  4. Check the test in MC_ClockSync1.

  5. Run:

    $ apalache check --init=Test1_Init \
    --next=Test1_Next --inv=Test1_Inv --length=1 MC_ClockSync1.tla

  6. The tool reports no error.

Version 2: Sending messages

  1. Open ClockSync2 and MC_ClockSync2.

  2. Check constants t_min and t_max.

  3. Notice that variables msgs and state are added.

  4. Check the test in MC_ClockSync2.

  5. Run:

    $ apalache check --init=Test2_Init \
    --next=Test2_Next --inv=Test2_Inv --length=1 MC_ClockSync2.tla

  6. The tool reports no error.

Version 3: Receiving messages

  1. Open ClockSync3 and MC_ClockSync3.

  2. Notice that variable rcvd is added.

  3. Check the test in MC_ClockSync3.

  4. Run:

    $ apalache check --init=Test3_Init \
    --next=Test3_Next --inv=Test3_Inv --length=1 MC_ClockSync3.tla

  5. The tool reports no error.

Version 4: Adjusting clocks

  1. Open ClockSync4 and MC_ClockSync4.

  2. Notice that variable diff is added.

  3. Check the test in MC_ClockSync4.

  4. Run:

    $ apalache check --init=Test4_Init \
    --next=Test4_Next --inv=Test4_Inv --length=1 MC_ClockSync4.tla

  5. The tool reports no error.

  6. Check the invariant SkewInv in ClockSync4.

  7. Run:

    $ apalache check --inv=SkewInv MC_ClockSync4.tla

  8. The tool reports an error. Open counterexample1.tla.

Version 5: Ignoring self-messages

  1. Open ClockSync5 and MC_ClockSync5.

  2. Notice the changes in AdjustClock.

  3. Run:

    $ apalache check --inv=SkewInv MC_ClockSync5.tla

  4. The tool reports no error.

Version 6: Parameterizing the set of processes

  1. Open ClockSync6 and MC_ClockSync6.

  2. Notice that we made Proc a constant.

  3. Check the operator DiffSum and how it is used.

  4. Run:

    $ apalache check --inv=SkewInv MC_ClockSync6.tla

Version 6p: ConstInit to check arbitrary t_min and t_max

  1. Open MC_ClockSync6p.

  2. Check the operator ConstInit.

  3. Check how we have changed the bound in SkewInv.

  4. Run:

    $ apalache check --cinit=ConstInit --inv=SkewInv MC_ClockSync6p.tla

  5. The tool reports no error.