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)

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

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

|-- models/   These are the original published seven WBS model taken from the
|             website of the paper:
|
|             Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D.,
|             Kimberly, G., Petri, T., Robinson, R., Tonetta, S.: Formal
|             design and safety analysis of AIR6110 wheel brake system. In:
|             CAV (2015)
|
|             The original licenses can be found in this folder.
|             DO NOT MODIFY THE CONTENTS OF THIS FOLDER.
|
|-- tools/    Binary for tools used in the analysis. The tools are used 'as is'
|             from the original tool distribution and are included with these
|             artifacts for completeness. The original licenses are included.
|             REDISTRIBUTION IS PROHIBITED.
|             INCLUDED FOR ARTIFACT EVALUATION PURPOSES ONLY.
|
|-- scripts/  Python scripts to reproduce the experiments in the paper. For
|             further details, refer to the README in the folder.
|
|-- plots/    Python script to generate the plots in the paper for the WBS
|             benchmark. The pdf for plots concerning the benchmark are also
|             included.
|
|-- results/  Contains results for all model-property pair and dependencies
|             between properties. These are included to speed up result
|             reproduction by reading model checking directly, rather than
|             checking models using nuXmv.
|             USED FOR FAST REPRODUCTION OF RESULTS FOR ARTIFACT EVALUATION.
|             DO NOT MODIFY.

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

For details on how to perform the experiments and reproduce data in the paper,
refer to the README in /scripts/.

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