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.