⏰ Analyzer for Timed Automata

This project provides an analyzer for Timed Automata. The analyzer is written in Rust and compiled to WebAssembly to offer a fast and efficient tool to implement analyses for websites. Currently, the analyzer offers functionality to find unreachable locations in a given TA.

🚀 Getting Started

To use the tool in your JavaScript/TypeScript project, simply install the package timed-automata-analyzer with your favorite package manager. Then map your Timed Automata into the TA model provided by the analyzer. When this is done, you can find unreachable locations by using the function findUnreachableLocations(ta). The function returns an array of strings containing the names of all unreachable locations. If all locations are reachable, the array is empty.

Note that the analyzer validates the input TA before starting the analysis. In case of any validation issues (e.g., missing initial location), findUnreachableLocations(ta) throws an error.

🦀 Developing the Tool

In case you want to contribute to the tool or fork the repository, only few steps are necessary:

• As a first step, you need to install Rust. See the Rust website for information on how to do this.
• Additionally, you need to install wasm-pack with cargo install wasm-pack for WebAssembly outputs.
• The WebAssembly binary (including glue code for JavaScript/TypeScript and an npm package) is generated by running wasm-pack build --target bundler and published to the npm registry by running wasm-pack publish.
• This project includes an extensive test suite. Tests can be run with cargo test.
• For linting, this project uses the built-in linter of Rust as well as Clippy. To run the linters, execute cargo check and cargo clippy, respectively.
• For further information on compiling Rust to WebAssembly, see the MDN Web Docs.

💡 Additional Information

• Most of the algorithms for checking reachability are based on the paper Timed Automata: Semantics, Algorithms and Tools.
• In case you want to see the analyzer in action, I built a React app for modeling and analyzing Timed Automata. The React app is available here, while the repository for the React app is available here.
• An introduction to Timed Automata can be found in Wikipedia.
• The original paper on Timed Automata is Automata for modeling real-time systems by Alur and Dill.