enduser/Modal-Transition-Systems.md

 # Modal Transition Systems
+The tool, as its name suggests support model checking and synthesis using modal transition systems. This functionality has not received attention in many years and may not be fully functional. 
+
+### component
+The `component` keyword is intended to build a Modal Transition System (MTS)
+*component* by projecting a composed system onto a given interface alphabet
+(the actions listed after `|`), abstracting away the rest of the behaviour:
+
+```
+component ||NAME = (P || Q) | {interfaceActions}.
+```
+
+The `optimistic` and `pessimistic` keywords are MTS refinement operations, applied as
+a prefix to a modal model:
+
+* `optimistic` — the *optimistic* model: the maximal implementation, treating *maybe* transitions as present, e.g. `optimistic ||M = (...)`.
+* `pessimistic` — the dual *pessimistic* model: the minimal implementation, dropping *maybe* transitions and keeping only required behaviour.
+
+Other Modal Transition System and scenario keywords, not yet documented:
+
+* `restricts` — scenario restriction
+* `instances` — scenario instances
+* `condition` — a named Fluent Propositional Logic predicate used inside triggered scenarios (`eTS`/`uTS`), referenced by the pre/main charts.
+* `prechart` — prechart in a triggered scenario
+* `mainchart` — main chart in a triggered scenario
+* `eTS` — existentially triggered scenario
+* `uTS` — universally triggered scenario
+* `starenv` — star environment
+* `buchi` — Büchi automaton specification
+### Abstract
+The `abstract` keyword builds a Modal Transition System (MTS) from the LTS resulting
+from compiling an FSP process, adding a *may* transition for every label that is
+disabled (not enabled) in a state.
+The keyword can be used with sequential and composite processes.
+
+```
+abstract LOWER = (a -> b -> LOWER).
+
+LOWER = (a -> b -> LOWER).
+abstract ||PL = (LOWER)\{a}.
+```
+
+
 
 Modal transition systems (MTS) can be modelled by using a question mark (`?`) on event labels to indicate may-transitions (transitions that may or may not be present in an implementation).