enduser/MTSA-Syntax.md

@@ -197,21 +197,6 @@ As with `deterministic`, in composite processes hiding is applied before the min
 minimal M = (a -> v -> M | a -> v -> M).
 ```
 
-
-## 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}.
-```
-
-
 ## Compose
 The `compose` keyword is supposed to force the parallel composition of a composite process to be computed explicitly, rather than kept in the deferred form. However the is not the MTSA. Thus, it makes not effect at all.
 
@@ -343,36 +328,6 @@ guide** — and some are not currently functional. They are collected here as a
 list to be documented and verified over time. The full index is in the
 [MTSA Keyword Reference](FSP-Keywords).
 
-## 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
-
 ## Animation / Visualisation
 These keywords are related to the scenebeans animation capabilities developed originally for LTSA. This functionality has not received attention in many years and may not be fully functional.