This folder contains content to reproduce the experimental results for the
NASA ATC 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/  Empty folder. The parameter instantiated instances are stored
|               in this folder.
|
|-- resources/cmds/  nuXmv command scripts to extract information regarding
|                    the model to be checked.
|
|-- instances.list.csv  The CSV file contain unique numbering for all 1,620
|                       models. The different parameter instantiated models
|                       are referenced using the number in this file (used
|                       internally)
|
|-- all.py    Helper python script to generate parameter instantiated SMV
|             models for all 1,620 models.
|
|-- simple.py   Python script to check all 1,620 models against properties.
|
|-- d3.py     Main python script that runs D^3 on the ATC models.
|
|--param_result.py  Helper python script to extract JSON of results for all
|                   phases from the result archive in
|                   ../plots/results_archive.7z and store them in ../results/
|
|-- *.py      All other python script are used from within simple.py and d3.py.

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

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

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

Table 1 in the paper corresponds to the experimental results obtained on the
NASA-ATC benchmark. Details on how to reproduce the results are given below.
Please follow each step very carefully.

Step -1: Fire up a terminal window with

    TACAS_Paper_152_Artifact/NASA_ATC/scripts/

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

Step 0: Generate all possible 1,620 models corresponding to every parameter
configuration.

      command: python all.py

(command takes around 10 minutes to finish)

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

---> Results for individual model checking. Column 4 of Table 1 <----

Step 1: Check each of the 1,620 models for every phase.

1.1: View all available options for simple.py

      command: python simple.py -h

The output for the above command is:

usage: simple.py [-h] [-p PHASE] [--perform-checking]

Check each of the 1,620 NASA ATC models

optional arguments:
  -h, --help          show this help message and exit
  -p PHASE            Checking phase for all models. Value between 1..5
                      1: Airspace Validation
                      2: Nominal Validation
                      3: Extended Validation
                      4: Nominal Verification
                      5: Extended Verification
  --perform-checking  If specified, model checking is performed using nuXmv.
                      Otherwise, results are read from file (../results/).

NOTE: Since experiments take up to 250 hours to complete, we RECOMMNEND using
the simple.py script without the --perform-checking option enabled. Without
this option, model checking results (true/false/unknown and time) are read
from a file in ../results/. If enabled, nuXmv is called to check every
model-property pair.

1.2 Reproduce timing results of Column 4

Column 4, Phase 1:

      command: python simple.py -p 1

Column 4, Phase 2:

      command: python simple.py -p 2

Column 4, Phase 3:

      command: python simple.py -p 3

Column 4, Phase 4:

      command: python simple.py -p 4

Column 4, Phase 5:

      command: python simple.py -p 5

NOTE: Instead of reading results from file, specify --perform-checking in the
commands above to run nuXmv. e.g. for phase 4 the command becomes

      command: python simple.py --perform-checking -p 4

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

---> Results for model checking with D^3. Column 5 of Table 1 <----

Step 2: Check NASA-ATC models using D^3

2.1: View all available options for d3.py

      command: python d3.py -h

The output for the above command is

usage: d3.py [-h] [-p PHASE] [--only-generate] [--perform-checking]
             [--only-dependence]

Run D^3 on the NASA ATC models

optional arguments:
  -h, --help          show this help message and exit
  -p PHASE            Checking phase for all models. Value between 1..5
                      1: Airspace Validation
                      2: Nominal Validation
                      3: Extended Validation
                      4: Nominal Verification
                      5: Extended Verification
  --only-generate     Only generate the SMV models each reduced parameter
                      configurations.
  --perform-checking  If specified, model checking is performed using nuXmv.
                      Otherwise, results are read from file (../results/).
  --only-dependence   Establish dependencies for all properties in
                      the model, and store results (../results/)

NOTE: (Optional) We do not use the --only-generate option for artifact
evaluation since the required models were already generated in Step 0.
However, if Step 2 is run without running Step 0, execute

      command: python d3.py --only-generate

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 -p <NUMBER> --only-dependence

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

NOTE: Since experiments take up to 250 hours to complete, we RECOMMNEND using
the d3.py script without the --perform-checking option enabled. Without this
option, model checking results (true/false/unknown and time) are read from a
file in ../results/. If enabled, nuXmv is called to check model-property pair.

2.2: Reproducing timing results of Column 5 (In this mode, D^3 is run with the
Maximum Dependence Heuristic (H1))

Column 5, Phase 1:

      command: python d3.py -p 1

Column 5, Phase 2:

      command: python d3.py -p 2

Column 5, Phase 3:

      command: python d3.py -p 3

Column 5, Phase 4:

      command: python d3.py -p 4

Column 5, Phase 5:

      command: python d3.py -p 5

IMPORTANT: The total timing results output using the commands above is less than what is reported in Table 1. This is due to the fact that the timing in Column 5 of Table 1 also includes the time taken to find dependencies between LTL properties.

NOTE: Instead of reading results from file, specify --perform-checking in the
commands above to run nuXmv. e.g. for phase 5 the command becomes

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

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

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