Start Using MTSA

Download the latest stable release from mtsa.dc.uba.ar.

You can run the application using Java 11 JRE or later. Launch it with:

java -jar mtsa-latest.jar

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