Skip to content

GitLab

FSP · Changes

Page history
suchitel updated page: FSP authored by Sebastian Uchitel's avatar Sebastian Uchitel
Hide whitespace changes
Inline Side-by-side
Showing with 7 additions and 7 deletions
enduser/FSP.md
View page @ 0aa4f4ad
[[_TOC_]] [[_TOC_]]
# Basic FSP syntax # Basic FSP syntax
MTSA preserves the full syntax of 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) 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)
The syntax for sequential and composite processes has remained the same in MTSA. Multiple additions have been made regarding modifiers for composite processes, hence we cover them below. The syntax for sequential and composite processes has remained the same in MTSA. Multiple additions have been made regarding modifiers for composite processes, hence we cover them below.
# Deterministic keyword # Deterministic keyword
The deterministic keyword produces a deterministic LTS that preserves that traces of the original one. The `deterministic` keyword produces a deterministic LTS that preserves the traces of the original one.
It can be used with sequential and composite processes. It can be used with sequential and composite processes.
Note that in composite processes the keyword takes precedence over hiding. Note that in composite processes the keyword takes precedence over hiding.
...@@ -25,9 +25,9 @@ deterministic ||COMP2 = (C). ...@@ -25,9 +25,9 @@ deterministic ||COMP2 = (C).
# Closure keyword # Closure keyword
The closure keyword adds new transitions to the LTS resulting The `closure` keyword adds new transitions to the LTS resulting
from compiling an FSP process according to the transitive from compiling an FSP process according to the transitive
closure of the transition relation over tau (silent) events closure of the transition relation over tau (silent) events.
The keyword can be used with sequential and composite processes. The keyword can be used with sequential and composite processes.
``` ```
...@@ -40,8 +40,8 @@ closure ||COMP = (B)\{a}. ...@@ -40,8 +40,8 @@ closure ||COMP = (B)\{a}.
# Property keyword # Property keyword
The property keyword adds an error state and for every event and every other state 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 adds a transition to it if the event is not enabled in that state.
It requires a deterministic LTS. It requires a deterministic LTS.
``` ```
...@@ -50,4 +50,4 @@ property POLITE ...@@ -50,4 +50,4 @@ property POLITE
``` ```
--- ---
[← End User](End-User) [← End User](End-User)
\ No newline at end of file