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

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. Prerequisites Java SE Runtime Environment 11 Building the tool See the build instructions. Usage $ java -jar theta-xta-cli.jar --clock LU|FWITP|BWITP Refinement strategy for clock variables --discrete NONE|FWITP|BWITP Refinement strategy for clock variables --model MODEL Path of the input model --search BFS|DFS|RANDOM Search strategy Example $ java -jar theta-xta-cli.jar --model models\c1.xta --clock FWITP --discrete BWITP --search DFS Sample output 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 For the experiments, we used JVM switches -Xmx6G and -Xss8m.