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.

Prerequisites

Java SE Runtime Environment 11

Building the tool

See the build instructions.

Usage

$ java -jar theta-xta-cli.jar
--clock Refinement strategy for clock variables
--discrete Refinement strategy for clock variables
--model Path of the input model
--search 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.