This folder contains content to reproduce the experimental results for the
Boeing WBS models in the paper.

  Dureja, R., Rozier, K.Y.: More Scalable LTL Model Checking via
      Discovering Design-Space Dependencies (D3). In: TACAS (2018)

-------------------------------------------------------------------------------

System Requirements
===================

The only other system requirement besides the included tools is Python 2.7
available in PATH.

-------------------------------------------------------------------------------

Directory Structure
===================

|-- instances/  Contains three things
|               1. Flattened SMV models generated from ../models/
|               2. Universal models generated from flattened SMV models by
|                  removing transitions.
|               3. XML file for properties to be checked for each model.
|
|-- resources/cmds/  nuXmv command scripts to extract information regarding
|                    the model to be checked.
|
|-- d3.py     Main python script that runs D^3 on the WBS models.
|
|-- *.py      All other python script are used from within D^3.

-------------------------------------------------------------------------------

Step-by-Step Instructions
=========================

**General Comment: Statements marked with "(Optional)" are not required for
artifacts reproduction by the evaluation committee.**

Table 2 in the paper corresponds to the experiments results obtained on the
Boeing-WBS benchmark. Details on how to reproduce the results are given below.
Please follow each step very carefully.

Step 0: Fire up a terminal window with

    TACAS_Paper_152_Artifact/Boeing-WBS/scripts/

as the active directory. All commands below are contingent on the correctness
of the current active directory.

-------------------------------------------------------------------------------

---> Results for checking all properties one-by-one. Column 2,3 of Table 2 <---

Step 1: Check all properties for seven models. ("single" columns)

1.: View all available options for d3.py

      command: python d3.py -h

The output for the above command is:

Run D^3 on the Boeing WBS models

optional arguments:
  -h, --help          show this help message and exit
  -i INSTANCE         Model number to check. Value between 1..7
  -m MODE             Heuristic to use for CheckRP (default = None) 1: Maximum
                      Dependence, 2: Property Affinity
  -t THRESHOLD        Threshold to use for Property Affinity heuristic
                      (default = 1.0)
  --perform-checking  If specified, model checking is performed using nuXmv.
                      Otherwise, results are read from file (../results/).
                      NOTE: For D^3 with property affinity heuristic, model
                      checking is always performed!
  --only-dependence   Establish dependencies for all properties in the model,
                      and store results (../results/)
  --only-individual   Check specified model one-by-one against properties, and
                      store results (../results/)

NOTE: The experiments in this benchmark takes about a minute for each model.
Therefore, the option --perform-checking is can be used for fast artifact
reproduction. It is always enabled when checking all properties for a model.

1.2: Check all properties for a model.

Model 1:

      command: python d3.py -i 1 --only-individual

Model 2:

      command: python d3.py -i 2 --only-individual

Model 3:

      command: python d3.py -i 3 --only-individual

Model 4:

      command: python d3.py -i 4 --only-individual

Model 5:

      command: python d3.py -i 5 --only-individual

Model 6:

      command: python d3.py -i 6 --only-individual

Model 7:

      command: python d3.py -i 7 --only-individual

NOTE: When running these commands, nuXmv is used to check the properties,
instead of reading results from a file. Therefore, the timing output might
differ slightly compared to results reported in the paper due to change in
experimental setup. However, the count of checker runs should be the same.

-------------------------------------------------------------------------------

---> Results of checking properties with CheckRP. Columns 4,5 of Table 2 <---

NOTE: (Optional) We do not use the --only-dependence option for artifact
evaluation since the property dependencies are already stored in a file in ../
results/. Once established, property dependencies do not change. If for some
reason dependencies need to be re-established, execute

      command: python d3.py -i <NUMBER> --only-dependence

where <NUMBER> is the phase number. Dependence results will be stored in the
folder ../results/.

Step 2: Check properties using CheckRP without any heuristics

Model 1:

      command: python d3.py -i 1 --perform-checking

Model 2:

      command: python d3.py -i 2 --perform-checking

Model 3:

      command: python d3.py -i 3 --perform-checking

Model 4:

      command: python d3.py -i 4 --perform-checking

Model 5:

      command: python d3.py -i 5 --perform-checking

Model 6:

      command: python d3.py -i 6 --perform-checking

Model 7:

      command: python d3.py -i 7 --perform-checking

NOTE: When running these commands, nuXmv is used to check the properties,
instead of reading results from a file. Therefore, the timing output might
differ slightly compared to results reported in the paper due to change in
experimental setup. However, the count of checker runs should be the same.

-------------------------------------------------------------------------------

---> Results of checking properties with CheckRP with Heuristic 1 (Maximum
Dependence). Columns 6,7 of Table 2 <---

Step 3: Check properties using CheckRP + Maximum Dependence Heuristic (H1)

Model 1:

      command: python d3.py -i 1 -m 1

Model 2:

      command: python d3.py -i 2 -m 1

Model 3:

      command: python d3.py -i 3 -m 1

Model 4:

      command: python d3.py -i 4 -m 1

Model 5:

      command: python d3.py -i 5 -m 1

Model 6:

      command: python d3.py -i 6 -m 1

Model 7:

      command: python d3.py -i 7 -m 1

NOTE: When running these commands, checking results are reused from Step 1 for
fast reproduction. The timing output might differ slightly compared
to results reported in the paper due to change in experimental setup. However,
the count of checker runs should be the same.

-------------------------------------------------------------------------------

---> Results of checking properties with CheckRP with Heuristic 1 (Property
Affinity). Columns 8,9 of Table 2 <---

Step 4: Check properties using CheckRP + Property Affinity Heuristic (H1)

4.1: In the command above, replace "-m 1" with "-m 2". e.g.

      command: python d3.py -i 3 -m 2

check properties for model 3 using CheckRP + H1.

NOTE: (Optional) The grouping threshold can be changed using

      command: python d3.py -i 5 -t 0.95 -m 2

which sets the threshold to 0.95. Default value is 1.0.

NOTE: When running these commands, checking results are reused from Step 1 for
fast reproduction. The timing output might differ slightly compared
to results reported in the paper due to change in experimental setup.

NOTE: The count of checker runs might vary in different runs of the same
command. This is due to non-determinism in the grouping algorithm used. The
results in the table in the paper is the maximum of values returned in
multiple runs at the time of evaluation.

-------------------------------------------------------------------------------

For further information, contact Rohit Dureja (dureja@iastate.edu)
