Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
M MTSA
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 41
    • Issues 41
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Metrics
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Package Registry
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • lafhis
  • MTSA
  • Wiki
  • End User

End User · Changes

Page history
Create End User authored Jun 13, 2025 by Pablo Laciana's avatar Pablo Laciana
Show whitespace changes
Inline Side-by-side
Showing with 19 additions and 0 deletions
+19 -0
  • End-User.md End-User.md +19 -0
  • No files found.
End-User.md 0 → 100644
View page @ a725109b
# Start Using MTSA
Download the latest stable version from [here](https://bitbucket.org/lnahabedian/mtsa/downloads/). Zip may not be up-to-date, but it also contains some useful resources.
You can run the application using [Java 8 JRE](http://www.oracle.com/technetwork/java/javase/downloads/jre8-downloads-2133155.html). 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](https://www.doc.ic.ac.uk/~jnm/book/).
If you want to define your own examples, check the following sections:
* [Parse, Compile and Compose. A tiny example.][enduser/helloworld]
* [FSP language options][enduser/fsp_keywords]
* [Fluents & LTL][enduser/fltl]
* [Supervisory Control](https://bitbucket.org/lnahabedian/mtsa/wiki/enduser/supervisoryControl)
* [Reactive Synthesis](https://bitbucket.org/lnahabedian/mtsa/wiki/enduser/reactiveSynthesis)
* [DCS](https://bitbucket.org/lnahabedian/mtsa/wiki/enduser/DCS)
\ No newline at end of file
Clone repository
  • Developer
  • End User
  • devs
    • outputmessages
  • enduser
    • DCS
    • fltl
    • fsp_keywords
    • helloworld
    • reactiveSynthesis
    • supervisoryControl
  • Home