- qlock-depth.maude is used to generate all states located at depth 3.

- qlock-d1-0.maude is used in the 1st layer. A counetrexample of inWs1 |-> inCs1 is found, which is used to suppress it, allowing the 2nd counterexample to be found. Repeating this process, all counterexamples are found.

- qlock-d1.maude uses all 227 counterexamples of inWs1 |-> inCs1 found in the 1st layer. So, no more counterexample is found.

- qlock.maude is the specification used for the model checking experiments in the 2nd layer.

- qlock-d2.maude is used to model check inWs1 |-> inCs1 for each of the 820 states located at depth 3.

- qlock-d2-2.maude is used to model check <> inCs1 for each of the 227 states located at depth 3, where the 227 states are obtained from the 227 counterexamples.

- mcs-dep.maude is the specification used for the 1st and 2nd layer model checking experiments.

- mcs-d1.maude is used to model check inWs1 |-> inCs1 in the 1st layer and to generate all states located at depth 8.

- mcs-d2.maude is used to model check inWs1 |-> inCS1 in the 2nd layer.

- mcs-d2-2.maude is used to generate all states located at depth 16.

- mcs.maude is the specification used for the model checking experiments in the 3rd layer.

The 3,730,668 model checking problems are partitioned into the following 28 files:

- m3-1.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (1).

- m3-2.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (2).

- m3-3.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (3).

- m3-4.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (4).

- m3-5.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (5).

- m3-6.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (6).

- m3-7.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (7).

- m3-8.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (8).

- m3-9.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (9).

- m3-10.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (10).

- m3-11.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (11).

- m3-12.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (12).

- m3-13.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (13).

- m3-14.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (14).

- m3-15.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (15).

- m3-16.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (16).

- m3-17.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (17).

- m3-18.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (18).

- m3-19.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (19).

- m3-20.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (20).

- m3-21.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (21).

- m3-22.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (22).

- m3-23.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (23).

- m3-24.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (24).

- m3-25.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (25).

- m3-26.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (26).

- m3-27.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (27).

- m3-28.maude is used to model check inWs1 |-> inCs1 in the 3rd layer (28).

Nov 09, 2020; May 9, 2019 by ogata