⏰ Timed-Automata Analysis

This project is a tool for modeling and analyzing Timed Automata. The tool is based on React and TypeScript and can be extended easily to also incorporate analysis techniques based on the created models. If you want to see the tool in actions, just visit this website.

🚀 Quick Start

This project utilizes Node and Yarn Classic for development. The usual commands for React projects also apply here.

• yarn install to install all dependencies and setup the project locally
• yarn start to run the app locally for development
• yarn format to format all files
• yarn lint for linting
• yarn test for running unit tests
• yarn e2e for running end-to-end tests
• yarn e2e-ui for running end-to-end tests in the UI mode of Playwright
• yarn e2e-update-snapshots for updating the end-to-end test snapshots
• yarn playwright install for installing/updating the browsers for Playwright
• yarn build to build the app for production
• yarn deploy for deployment on GitHub Pages

See package.json for further commands.

🎯 Reachability Analysis

This project supports reachability analysis for modeled TA. To start an analysis, just press the respective button in the UI. The app will then calculate reachability for all locations.

The implementation of the analysis is done in a separate project and is also available as an NPM package called timed-automata-analyzer. For maximum performance, the analyzer is written in Rust and compiled to WebAssembly.

🔗 Links

• Timed-Automata Analysis on GitHub Pages
• Introduction to Timed Automata on Wikipedia
• Original paper on Timed Automata by Alur and Dill