enduser/FSP.md

+[[_TOC_]]
+
+# 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)
+
+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
+The deterministic keyword produces a deterministic LTS that preserves that 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 keyword
+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 keyword
+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).
+```
+
+
+# Modal Transition Systems
+Modal transition systems (MTS) can be modelled by using a question mark (?) on event labels.
+```
+A = (a -> b? -> A | a? -> A).
+```
+
+# Abstract keyword
+The abstract keyword builds an MTS from a FSP process adding to each state maybe
+transitions on labels that are not enabled in the original process.
+It can be applied both to sequential and composite processes.
+
+```
+abstract A = (a -> b -> A | a->STOP | b->END).
+
+B = (a -> b -> B | b? -> B).
+abstract ||COMP = (B).
+```
+
+# End
+
+---
+Back to [End User](../End-User)
\ No newline at end of file