An analyzer for Timed Automata written in Rust
npm install timed-automata-analyzerThis 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.
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.
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.
In addition to the Rust code for creating the Wasm binary, this project also contains a tiny TypeScript project in the folder wasm_test.
The purpose of this Node project is to check whether the generated Wasm binary and the generate glue code work as intended (i.e., the Wasm binary can in principal be accessed).
To execute these tests, just install Node and npm on your machine, open the wasm_test folder, and run npm install and npm test.
- 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.