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

The tool we used for producing the experimental data is implemented as a prototype in the open source model checking framework Theta. Source code is available on GitHub. The experimental data is based on this commit. <strong>Prerequisites</strong> Java SE Runtime Environment 11 <strong>Building the tool</strong> See the build instructions. <strong>Usage</strong> <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> <strong>Example</strong> <pre><code> $ java -jar theta-xta-cli.jar --model models\c1.xta --clock FWITP --discrete BWITP --search DFS </code> </pre> <strong>Sample output</strong> <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> For the experiments, we used JVM switches <code>-Xmx6G</code> and <code>-Xss8m</code>.