Contents

1. Introduction to the Tool
2. Installation with Docker
3. Installation without Docker
4. Running the tool
5. Benchmarks
6. File Format

---

Introduction to the Tool

This artifact is a prototype implementation of the reachability procedure for the model Generalized Timed Automata (GTA) proposed in the CAV paper A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation.

Generalized Timed Automata (GTA) unifies the features of various models such as timed automata, event-clock automata (with and without diagonal constraints), and automata with timers. We implement the new simulation-based zone algorithm for checking reachability in this unified model as given in the paper.

Given a Generalized Timed Automata and an initial state, we compute all the states reachable from the initial state. For details regarding the algorithm please refer to the paper.

Our tool is built on the tool TChecker (version 3), and uses many operations that are present in the tool. For more details on TChecker please visit, https://github.com/ticktac-project/tchecker.

---

Installation with Docker

Downloading the Docker Image

DOI: 10.6084/m9.figshare.22734839.v1

Link for accessing the docker image: https://doi.org/10.6084/m9.figshare.22734839.v1

Requirements for running the Docker Image

• Docker (version >=23.0.4)

Instructions to load the docker image:

Run the following command to load the docker image:

sudo docker load < gta_v3.tar

The terminal should then display:

Loaded image: gta:3

---

Running Docker Image:

Run the following command to start the interactive terminal:

sudo docker run -it gta:3

For running the tool go to (Running the tool)[#Running-the-tool]

---

Installation without Docker

Requirements for installing TChecker Tool

• g++ (version >=9.3.0)
• CMake (version >=2.8)
• flex (version >=2.6.4)
• bison (version >=3.5.1)
• boost library (version >=1.65.0)
• Catch2 (version 2)

NOTE: Our tool works with the above requirements, but it may also work with older versions as well.

Catch2 version 2 can be obtained from Catch2 github repository. Please download the v2.x branch, it can be downloaded using the command:

git clone https://github.com/catchorg/Catch2.git -b v2.x
cd Catch2
cmake -Bbuild -H. -DBUILD_TESTING=OFF
sudo cmake --build build/ --target install

Please, refer to Catch2 tutorial for installation instructions.

Requirements for installing Parser Tool

• python (version >= 3.9)

To verify that python is installed: the command python3 --version should work and should output a version >=3.9.

Compile

To compile the TChecker tool, run the following command

  ./compile.sh

The command should create a build_dir directory and an install_dir directory.

---

Running the tool

• To run the tool on a input_file with path file_path execute the following command:

    `./run.sh file_path`
  

• To run the G-simulation tool on a input_file with path file_path containing a General Timed Automata (Note: this is also the default option with ./run.sh), execute the following command:

    ./run.sh gta_gsim file_path
  

• To run the G-simulation tool on a input_file with path file_path containing a Timed Automata, execute the following command:

    ./run.sh gsim file_path
  

• To run the parser that takes input an ECA file with name input_file and path input_file_path, and outputs a Timed Automata (according to Alur & Dill) in output_file execute the following command:

    ./run.sh eca input_file_path/input_file output_file
  

---

Benchmarks

The directory examples_gta contains GTA benchmarks.

---

File Format

Please, refer to Using GTA-Model or to file tchecker/doc/file-format-combined.md.