Start Using MTSA

Download the latest stable version from here. Zip may not be up-to-date, but it also contains some useful resources.

You can run the application using Java 8 JRE. If you try to run and nothing happens, make sure the downloaded JAR has its executing bit enabled.

Once MTSA is loaded you can use some of the examples in the menu option File > Open Examples.

A good starting point for modelling and analysis, and also some help with the tool is the book Concurrency: State Models & Java Programs by Jeff Magee & Jeff Kramer and its associated website.

If you want to define your own examples, check the following sections:

• Parse, Compile and Compose. A tiny example.
• FSP language options
• Fluents & LTL
• Supervisory Control
• Reactive Synthesis
• DCS