enduser/fsp_keywords.md

+[[_TOC_]]
+
+# Choice
+If x and y are actions then (x-> P | y-> Q) describes a process which initially engages in either of the actions x or y.
+After the first action has occurred, the subsequent behavior is described by P if the first action was x and Q if the first action was y.
+
+Deterministic choice 
+```
+DRINKS = (red->coffee->DRINKS |blue->tea->DRINKS).
+```
+Non Deterministic choice
+```
+COIN = (toss->HEADS|toss->TAILS),
+HEADS= (heads->COIN),
+TAILS= (tails->COIN).
+```
+
+
+# Indexed Processes and Actions
+Imagine you need to define the same set of actions with several processes. For instance, you want to define a clique graph.
+
+```
+CLIQUE = NODE[0],
+NODE[i:0..10] = (move[j:0..10] -> NODE[j]).
+```
+
+In the above example we use index i for **NODE** and index j for _move_.
+
+
+# Const and Range
+Same example using constant named N and ranges.
+
+```
+const N = 10
+range I = 0..N
+range J = 0..N
+
+CLIQUE = NODE[0],
+NODE[I] = (move[j:J] -> NODE[j]).
+```
+
+
+You may also use math expressions **( + * / - )**, for example:
+
+```
+const N = 5
+range T = 0..N-1
+range R = 0..2*N
+
+
+SUM = (in[a:T][b:T]->TOTAL[a+b]),
+TOTAL[s:R] = (out[s]->SUM).
+```
+
+And you can also use math expressions
+
+# Guarded Actions
+
+The choice (when B x -> P | y -> Q) means that when the guard B is true then the actions x and y are both eligible to be chosen, otherwise if B is false then the action x cannot be chosen.
+
+```
+COUNTDOWN (N=3) = (start->COUNTDOWN[N]),
+COUNTDOWN[i:0..N] = (when(i>0) tick->COUNTDOWN[i-1]
+			|when(i==0)beep->STOP
+			|stop->STOP
+			).
+```
+
+# Conditional guard
+
+```
+const False = 0
+const True = 1
+range Reserved = False..True
+
+range Seats = 1..5
+
+TERMINAL = (choose[r:Reserved]
+	-> if (!r) then
+		(seat[s:Seats].reserve -> TERMINAL)
+	else
+		TERMINAL).
+```
+
+# 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}.
+```
+
+# Constraint keyword
+The constraint keyword builds an LTS from an FLTL formula such
+that its traces are all traces that satisfy the formula.
+
+The formula must be a safety property.
+The alphabet of the resulting LTS contains exactly all events that appear
+in the formula or in fluent definitions used by the formula.
+This implies that the interpetation of the next operator (X) is like an alphabetised next.
+
+```
+constraint P = [] (p -> X q)
+
+fluent A = <a, c>
+fluent B = <b, c>
+
+constraint Q = [](A -> X B)
+```
+
+# 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).
+```
+
+# 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](https://bitbucket.org/lnahabedian/mtsa/wiki/enduser/enduser)
\ No newline at end of file