FSP-Keywords.md

@@ -10,19 +10,20 @@ Complete list of keywords recognised by the MTSA parser.
 * `when` — conditional guard on a choice
 * `if` / `then` / `else` — conditional expression
 * `forall` — universal quantification over an index range
-* `exists` — existential quantification
-* `foreach` — iteration
-* `property` — adds an error state for every event not enabled in each state
-* `progress` — declares a progress property
+* `exists` — existential quantification over an index range
+* `foreach` — iteration over a set
+* `rigid` — rigid constraint
+
 
 ## Process Modifiers
 
 * `deterministic` — produces a deterministic LTS preserving the original traces
 * `minimal` — minimises the LTS up to bisimulation
-* `compose` — explicit parallel composition
 * `closure` — adds transitions via transitive closure over tau events
 * `abstract` — builds an MTS by adding may-transitions on disabled labels
-* `rigid` — rigid constraint
+* `property` — adds an error state for every event not enabled in each state
+* `progress` — declares a progress property
+* `compose` — forces parallel composition
 
 ## LTL / Fluents
 
@@ -39,6 +40,7 @@ Complete list of keywords recognised by the MTSA parser.
 * `actions` — action labelling
 * `controls` — control definition
 
+
 ## Controller Synthesis (GR1)
 
 * `controller` (alias: `gr`) — GR1 controller synthesis
@@ -48,6 +50,9 @@ Complete list of keywords recognised by the MTSA parser.
 * `liveness` — liveness guarantees within a `controllerSpec`
 * `controllable` — set of controllable actions
 * `checkCompatibility` — checks whether GR1 assumptions are compatible
+
+
+# TO BE CHECKED
 * `permissive` — permissive controller mode
 * `controlled_det` — controlled determinism
 * `nonblocking` — non-blocking requirement
@@ -55,6 +60,7 @@ Complete list of keywords recognised by the MTSA parser.
 * `non_transient` — non-transient constraint
 * `reachability` — reachability analysis
 
+
 ## DCS / Non-blocking
 
 * `heuristic` — triggers Directed Controller Synthesis