End User

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:

Hello World
FSP language options
Fluents & LTL
Modal Transition Systems
Discrete Event Controller Synthesis

← Home