enduser/FSP.md

@@ -24,7 +24,7 @@ deterministic ||COMP2 = (C).
 ```
 
 
-## Closure keyword
+# 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
@@ -39,7 +39,7 @@ closure ||COMP = (B)\{a}.
 ```
 
 
-## Property keyword
+# 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.
@@ -47,28 +47,4 @@ 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
+```
\ No newline at end of file