Skip to content

GitLab

MTSA Syntax · Changes

Page history
Update MTSA Syntax authored by Sebastian Uchitel's avatar Sebastian Uchitel
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
enduser/MTSA-Syntax.md 0 → 100644
View page @ a0c1908f
MTSA Syntax currently supports writing sequential and concurrent processes modelled as LTS using the Finite State Processes (FSP) language. It also supports writing formulae in Fluent Linear Temporal Logic for model checking and synthesis. There is additional syntax for modelling modal transition systems and markov decision processes.
[[_TOC_]]
# Basic FSP syntax
MTSA preserves the full syntax supported by LTSA. Some references for its syntax are [FSP-Syntax by Jeff Magee](https://www.doc.ic.ac.uk/~jnm/LTSdocumention/FSP-notation.html) and [Notes on FSP, Alan Williams, Donal Fellows, and Howard Barringer](https://www.cs.man.ac.uk/~howard/Teaching/COMP30112/fsp-notes.pdf)
Here we cover some aspects:
## const, range, set
`const` declares a named integer constant, `range` a named integer interval, and
`set` a named collection of labels.
```
const N = 3
range R = 1..N
set Colours = {red, green, blue}
SERVER = (request[i:R] -> reply[i] -> SERVER).
```
A `set` can be used wherever a similarly as a range — for example as a choice
over its elements, or to extend a process alphabet with `+`:
```
set Colours = {red, green, blue}
LIGHT = (show[Colours] -> LIGHT). // one branch per element of the set
set Ext = {pause, resume}
P = (run -> P) + Ext. // alphabet extension
```
## Set size (`#`) and set element access (`@`)
The `#` operator gives the **size** (number of elements) of a set, as an integer, so
it can be used anywhere an integer expression is expected — range bounds, constants,
guards:
```
set Nodes = {n1, n2, n3, n4}
range Ids = 1..#Nodes
const NumNodes = #Nodes
```
The `@(set, i)` operator selects an **element** of a set by its 0-based index `i`,
yielding that label. It is typically used to pass a set element as a process
parameter, and combines naturally with `#` to instantiate one process per element:
```
set UID = {red, green, blue}
PROC(U=1) = (act[U] -> PROC).
||SYS = (forall[i:1..#UID] p[i]:PROC(@(UID, i-1))).
```
Here `@(UID, 0)`, `@(UID, 1)` and `@(UID, 2)` are `red`, `green` and `blue`. An index
outside `0 .. #set - 1` is a compile-time error.
## when
A `when` guard makes a branch of a choice available only while its boolean condition
holds. It is the standard way to encode state-dependent behaviour in an indexed
process.
```
const Max = 2
BUFFER = COUNT[0],
COUNT[i:0..Max] = (when (i<Max) put -> COUNT[i+1]
| when (i>0) get -> COUNT[i-1]).
```
## if / then / else
Inside a process body, `if (cond) then (P) else (Q)` selects between two
sub-behaviours according to a boolean condition over constants and indices.
```
A = (b -> if (1<2) then (a -> A) else (c -> A)).
```
## forall
`forall` replicates a parallel composition over an index range: `forall[i:R] ...`
composes one copy of the process per value of `i`. It is used in composite (`||`)
definitions.
```
const N = 3
USER = (acquire -> use -> release -> USER).
||USERS = (forall[i:1..N] u[i]:USER).
```
The indexed-prefix shorthand `(u[i:1..N]:USER)` is equivalent.
## foreach
Inside a process body, `foreach[i:R] <choices>` replicates the choice expression that
follows once for each value of `i` in the range or set — a shorthand for a large `|`
choice, and most useful combined with `when` guards or indexed labels.
```
range R = 0..2
P = (foreach[j:R] sel[j] -> P).
// equivalent to P = (sel[0] -> P | sel[1] -> P | sel[2] -> P).
```
With an index-dependent guard:
```
const N = 2
range R = 1..N
SW = SW[1],
SW[cur:R] = (foreach[t:R] when (t!=cur) switch[t] -> SW[t]).
```
## def
`def NAME(p1, ...) = <expression>` declares a parameterised expression macro: a named
arithmetic expression over its parameters that is substituted wherever `NAME(args)`
appears in another expression. It is handy for factoring out index arithmetic used by
indexed processes.
```
const N = 3
def Next(i) = (i+1) % N
TOKEN = TOKEN[0],
TOKEN[i:0..N-1] = (use[i] -> pass -> TOKEN[Next(i)]).
```
Here `Next(i)` computes the next position in a ring of `N`, so the token passes
`0 -> 1 -> 2 -> 0 -> ...`. Note `def` defines an *expression*, not a process.
## rigid
`rigid <expr>` is a *rigid* (time-invariant) proposition, valid only inside an FLTL
assertion (`assert`, `ltl_property`, `constraint`). The arithmetic expression over
constants/parameters is evaluated **once at compile time**: it becomes `true` when
`<expr> > 0` and `false` otherwise. This lets a parameterised assertion switch on a
compile-time condition. It is an advanced, rarely used feature inherited from LTSA.
```
const K = 1
fluent Fa = <a, b>
P = (a -> b -> P).
assert A = (rigid (K>0) -> []<> Fa)
```
# Modifiers to process definitions
## Deterministic
The `deterministic` keyword produces a deterministic LTS that preserves the traces of the original one.
It can be used with sequential and composite processes.
Note that in composite processes the keyword takes precedence over hiding.
```
deterministic A = (a -> b -> A | a -> c -> A).
B = (a -> b -> B | a -> c -> B).
deterministic ||COMP = (B)\{a}.
C = (a -> b -> C | a -> c -> C)\{a}.
deterministic ||COMP2 = (C).
```
## Closure
The `closure` keyword adds new transitions to the LTS resulting
from compiling an FSP process according to the transitive
closure of the transition relation over tau (silent) events.
The keyword can be used with sequential and composite processes.
```
closure A = (a -> b -> A)\{b}.
B = (d -> a -> b -> B | d -> a -> c -> B).
closure ||COMP = (B)\{a}.
```
## Property
The `property` keyword adds an error state and for every event and every other state
it adds a transition to it if the event is not enabled in that state.
It requires a deterministic LTS.
```
property POLITE
= (knock->enter->POLITE).
```
## Minimal keyword
The `minimal` keyword produces a minimal LTS, equivalent to the original one up to bisimulation.
It can be used with sequential and composite processes.
As with `deterministic`, in composite processes hiding is applied before the minimisation.
```
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.
```
A = (a -> b -> A).
B = (b -> c -> B).
compose ||COMP = (A || B).
```
# Other Keywords
## Progress
The `progress` keyword declares a progress (liveness) property. It asserts that, in
any infinite execution under fair choice, at least one of the actions in the given
set occurs infinitely often.
```
progress HEADS = {heads}
progress HEADSorTAILS = {heads, tails}
```
The keyword also accepts a conditional `if ... then ...` which asserts that, in
any infinite execution under fair choice, if at least one of the actions in the `if` happens infinitely then at least one of the actions in the `then` occurs infinitely often too.
```
progress P = if {enter} then {work}
```
# Fluent Linear Temporal Logic (FLTL)
MTSA supports Fluent Linear Temporal Logic (FLTL) to express and check temporal
properties over the traces of a system. A *fluent* is a boolean proposition defined
by the actions that make it true and the actions that make it false. FLTL formulas
are then written over fluents (and, directly, over action names) using the usual
boolean and temporal operators.
## Fluents
A fluent is declared with the set of actions that turn it on (initiating) and the
set of actions that turn it off (terminating), plus an optional initial value `1` (true) or `0` (false, the default).
```
fluent LIGHT_ON = <switchOn, switchOff> initially 0
```
Either side may be a set of actions.
```
fluent LIGHT_ON = <{switchOn, turnOn}, {switchOff, turnOff}> initially 0
```
Fluents can be indexed meaning that various fluents are defined, each with its own index.
```
const N = 2
range R = 1..N
fluent HELD[i:R] = <acquire[i], release[i]>
```
The `initially` clause may be an expression over the indices.
```
const N = 3
range T = 0..N
fluent AT[i:T] = <arrive[i], {leave[i]}> initially (i==0)
```
Note that `True` and `False` are **not** built-in; to write `initially False` you
must first declare the constants (`const False = 0` and `const True = 1`).
```
const False = 0
const True = 1
fluent LIGHT_ON = <switchOn, switchOff> initially False
```
## Temporal operators
FLTL formulas combine fluents and action names with the boolean connectives
`!`, `&&`, `||`, `->`, `<->` and the temporal operators:
* `[] f` — *always* f (globally)
* `<> f` — *eventually* f
* `X f` — f holds in the *next* state
* `f U g` — f holds *until* g (strong until)
* `f W g` — f holds *unless/weak until* g
* `forall [i:R] f`, `exists [i:R] f` — quantification over an index range
## Assert
`assert` gives a name to an FLTL formula so it can be checked against a system
(in the GUI: *Check ▸ LTL Property*).
```
LIGHT = (switchOn -> switchOff -> LIGHT).
fluent LIGHT_ON = <switchOn, switchOff> initially 0
assert ALWAYS_EVENTUALLY_ON = []<> LIGHT_ON
assert NO_DOUBLE_ON = [](switchOn -> X(!switchOn W switchOff))
```
## ltl_property
`ltl_property` compiles an FLTL safety formula into a *property process* (an LTS with an error state) that can be composed with a system to monitor it, analogous to a
`property` definition but written in FLTL.
```
range R = 1..2
fluent In[i:R] = <enter[i], exit[i]> initially 0
ltl_property MUTEX = [](!In[1] || !In[2])
```
## constraint
`constraint` compiles an FLTL safety formula into a *constraining process*: unlike
a property (which flags violations with an error state), a constraint only allows
the behaviours that satisfy the formula. It is typically used to restrict a model
or an environment.
```
range R = 1..2
fluent In[i:R] = <enter[i], exit[i]> initially 0
constraint MUTEX = [](!In[1] || !In[2])
```
# Unsupported
The keywords below are recognised by the parser but are **not yet documented in this
guide** — and some are not currently functional. They are collected here as a working
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.
* `menu` — defines a menu
* `animation` — animation specification
* `actions` — action labelling
* `controls` — control definition
* `target` — inside an `animation` declaration, binds the XML scene to a composition.
## Probabilistic
MTSA also supports some mdp model checking. This functionality has not received attention in many years and may not be fully functional.
* `probabilistic` — marks a process/composition as probabilistic; transitions carry probability distributions, e.g. `t -> {0.4:P1 + 0.6:P2}`. Currently it must be paired with `mdp`.
* `mdp` — selects the Markov Decision Process interpretation; composition builds an MDP abstraction. Written as `probabilistic mdp ||C = (R || A).`
## Distribution
Splits a monolithic model into per-component models over given alphabets. Declared as
a block: `distribution C1, C2, ... = { distributedAlphabets = {A1, ...} systemModel = SYS [outputFileName = "..."] }`.
* `distribution` — opens the block; takes the comma-separated component names (needs exactly one alphabet per component).
* `distributedAlphabets` — the alphabets (one per component) to project the system onto.
* `systemModel` — the monolithic process to be distributed.
* `outputFileName` — optional string path where the distribution result is written.
## Miscellaneous
* `import` — imports an external LTS from an Aldebaran `.aut` file as a named process, bypassing FSP compilation: `import NAME = "file.aut".`
---
[← End User](End-User)
\ No newline at end of file