Lazy Reachability Checking for Timed Automata with Discrete Variables

Downloads

Measurement data: measurements.csv.
Input models: models.zip.
Tool propotype: theta-xta-cli.jar.

The tool is implemented as a prototype in the open source model checking framework Theta. Source code is available on GitHub. The precompiled version, as well as the measurement data is based on this commit.

How to run the tool

Prerequisites

Java SE Runtime Environment 8

Usage


$ java -jar theta-xta-cli.jar
  --algorithm <SEQITP|LU|EXPLSEQITP|EXPLLU>  Algorithm
  --model <MODEL>                             Path of the input model
  --search <DFS|BFS|RANDOM>                   Search strategy

For the --algorithm switch, prefix EXPL marks configurations with refinement for discrete variables.

Example


$ java -jar theta-xta-cli.jar --model engine-classic.xta --algorithm EXPLSEQITP --search DFS

Sample output


AlgorithmTimeInMs: 525                // Total execution time in ms
ExpandTimeInMs: 447                   // Time spend with expansion in ms
CloseTimeInMs: 63                     // Time spent with covering nodes in ms
ExpandExplRefinementTimeInMs: 53      // Expand refinement time for explicit domain in ms
ExpandZoneRefinementTimeInMs: 210     // Expand refinement time for zone domain in ms
CloseExplRefinementTimeInMs: 2        // Close refinement time for explicit domain in ms
CloseZoneRefinementTimeInMs: 44       // Close refinement time for zone domain in ms
CoverageChecks: 171                   // Number of coverage checks
CoverageAttempts: 83                  // Number of attempts for forced coverage
CoverageSuccesses: 83                 // Number of successes for forced coverage
ExplRefinementSteps: 232              // Number of refinements steps for explicit domain
ZoneRefinementSteps: 638              // Number of refinements steps for zone domain
ArgDepth: 83                          // Depth of the reachability graph
ArgNodes: 614                         // Number of nodes in the reachability graph
ArgNodesExpanded: 532                 // Number of expanded nodes in the reachability graph

For the experiments, we used JVM switches -Xmx6G and -Xss8m. The increased stack size is necessary due to a known bug in the implementation of Stream.flatMap() in JDK8.