FSP-Keywords.md

+# MTSA Keyword Reference
+
+Complete list of keywords recognised by the MTSA parser.
+
+## Core FSP
+
+* `const` — constant declaration
+* `range` — range definition
+* `set` — set definition
+* `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
+
+## 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
+
+## LTL / Fluents
+
+* `fluent` — declares a fluent with initiating and terminating action sets
+* `assert` — declares an FLTL property
+* `ltl_property` — builds a safety observer process from an FLTL formula
+* `constraint` — builds a constraining process from an FLTL safety formula
+* `initially` — sets the initial value of a fluent
+
+## Animation / Visualisation
+
+* `menu` — defines a menu
+* `animation` — animation specification
+* `actions` — action labelling
+* `controls` — control definition
+
+## Controller Synthesis (GR1)
+
+* `controller` (alias: `gr`) — GR1 controller synthesis
+* `controllerSpec` — declares a controller goal specification
+* `safety` — safety processes within a `controllerSpec`
+* `assumption` — liveness assumptions within a `controllerSpec`
+* `liveness` — liveness guarantees within a `controllerSpec`
+* `controllable` — set of controllable actions
+* `checkCompatibility` — checks whether GR1 assumptions are compatible
+* `permissive` — permissive controller mode
+* `controlled_det` — controlled determinism
+* `nonblocking` — non-blocking requirement
+* `lazyness` — controller laziness parameter
+* `non_transient` — non-transient constraint
+* `reachability` — reachability analysis
+
+## DCS / Non-blocking
+
+* `heuristic` — triggers Directed Controller Synthesis
+* `marking` — marks states for non-blocking synthesis
+* `disturbances` — disturbance specification
+* `partialOrderReduction` — enables partial order reduction
+* `compositional` — compositional synthesis approach
+* `monolithicDirector` — monolithic director synthesis
+
+## RTC Controllers
+
+* `rtc` — Reactive Test Case controller
+* `rtcAnalysis` — RTC analysis controller
+* `failure` — fault/failure specification
+* `test_latency` — test latency specification
+* `exceptionHandling` — exception handling
+
+## Modal Transition Systems / Scenarios
+
+* `restricts` — scenario restriction
+* `instances` — scenario instances
+* `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
+
+## Fluent Activity / Concurrency
+
+* `activityFluents` — activity fluent declarations
+* `concurrencyFluents` — concurrency fluent declarations
+
+## Control Stack
+
+* `controlstack` — control stack specification
+* `tier` — control tier definition
+
+## Probabilistic
+
+* `mdp` — Markov Decision Process
+* `probabilistic` — probabilistic specification
+* `optimistic` — optimistic strategy
+* `pessimistic` — pessimistic strategy
+
+## Updating Controller
+
+* `updatingController` — updating controller problem
+* `oldController` — reference to the old controller
+* `oldGoal` — old goal specification
+* `newGoal` — new goal specification
+* `mapping` — state mapping
+* `transition` — transition specification
+* `graphUpdate` — graph update specification
+* `initialState` — initial state in the update graph
+* `transitions` — transitions in the update graph
+
+## Distribution
+
+* `distribution` — probability distribution
+* `systemModel` — system model specification
+* `outputFileName` — output file name
+* `distributedAlphabets` — distributed alphabets
+
+## Exploration
+
+* `exploration` — exploration specification
+* `environment` — exploration environment
+* `model` — exploration model
+* `goal` — exploration goal
+* `environment_actions` — environment action set
+
+## Miscellaneous
+
+* `component` — component definition
+* `condition` — condition specification
+* `plant` — plant model declaration
+* `target` — target specification
+* `import` — module import
+* `def` — definition
+
+---
+[← FSP](FSP)
\ No newline at end of file