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.