evaluation

Evaluation

This folder contains protocols and raw data of our series of experiments.

The first series of experiments empirically evaluates the correctness of our implementation and compares our implementation it to the paper. The second series tries to empirically observe key difference of low-connectivity state space exploration.

The folder structure is as follows:

• data/ contains raw data of the experiments.
• assets/ contains external assets, for example, a screenshotted plot from the Grapple paper.
• output-assets/ contains the PDFs of all plots and is used by the writeup.

General evaluation of the implementation and comparison with the paper

• EXP-00 Comparison with the Grapple Paper using the Waypoints Model
• EXP-01 Comparison of Waypoints and HLL as Indicators of State Space Coverage
• EXP-02 Maximum Size Hash Table
• EXP-03 Multiple VTs Sharing a Kernel
• EXP-04 Improving State Space Coverage Growth using Start Overs

Low-Connectivity model evaluation

• EXP-10 Comparison of Exploration of the Dining Philosophers Problem with Different Number of Processes
• EXP-11 Comparing Models by their BFS Frontiers: Relative and Absolute
• EXP-12 Comparing Models by Percentage of VTs Finding a Violation, Unique States Visited, Total States Visited, and State Space Coverage
• EXP-13 Comparing the Start Over Strategy on Low-Connectivity Models

Jupyter Environment

The experiments are evaluated in a VSCode development container using VSCode Jupyter Notebooks. They should, however, work in any miniconda environment.