Supplementary Material for the Paper "Configurable Verification of Timed Automata with Discrete Variables"

<p>The tool we used for producing the experimental data is implemented as a prototype in the open source model checking framework <a href="http://theta.inf.mit.bme.hu">Theta</a>. Source code is available on <a href="https://github.com/FTSRG/theta">GitHub</a>. The experimental data is based on <a href="https://github.com/FTSRG/theta/tree/be86f967998b7065cd55cb629322bffd8333af54">this commit</a>.</p> <p><strong>Prerequisites</strong></p> <p><a href="https://www.oracle.com/technetwork/java/javase/downloads/jdk11-downloads-5066655.html">Java SE Runtime Environment 11</a></p> <p><strong>Building the tool</strong></p> <p>See the <a href="http://github.com/ftsrg/theta/blob/be86f967998b7065cd55cb629322bffd8333af54/hu.bme.mit.theta.xta/README.md">build instructions</a>.</p> <p><strong>Usage</strong></p> <pre><code> $ java -jar theta-xta-cli.jar --clock &lt;LU|FWITP|BWITP&gt; Refinement strategy for clock variables --discrete &lt;NONE|FWITP|BWITP&gt; Refinement strategy for clock variables --model &lt;MODEL&gt; Path of the input model --search &lt;BFS|DFS|RANDOM&gt; Search strategy </code> </pre> <p><strong>Example</strong></p> <pre><code> $ java -jar theta-xta-cli.jar --model models\c1.xta --clock FWITP --discrete BWITP --search DFS </code> </pre> <p><strong>Sample output</strong></p> <pre><code> AlgorithmTimeInMs: 3482 // Total execution time in ms ExpandTimeInMs: 2128 // Time spend with expansion in ms CloseTimeInMs: 1301 // Time spent with covering nodes in ms ExpandExplRefinementTimeInMs: 901 // Expand refinement time for explicit domain in ms ExpandZoneRefinementTimeInMs: 84 // Expand refinement time for zone domain in ms CloseExplRefinementTimeInMs: 890 // Close refinement time for explicit domain in ms CloseZoneRefinementTimeInMs: 145 // Close refinement time for zone domain in ms CoverageChecks: 628201 // Number of coverage checks CoverageAttempts: 6069 // Number of attempts for forced coverage CoverageSuccesses: 6065 // Number of successes for forced coverage ExplRefinementSteps: 33560 // Number of refinements steps for explicit domain ZoneRefinementSteps: 1544 // Number of refinements steps for zone domain ArgDepth: 879 // Depth of the reachability graph ArgNodes: 14973 // Number of nodes in the reachability graph ArgNodesExpanded: 9307 // Number of expanded nodes in the reachability graph </code> </pre> <p>For the experiments, we used JVM switches <code>-Xmx6G</code> and <code>-Xss8m</code>.</p>