A Divide & Conquer Approach to Leads-to Model
Checking
Case Study 1 -
Qlock
- 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.
Case
Study 2 - MCS
- 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