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