enduser/Fluents-and-LTL-properties.md

+
 MTSA supports fluent linear temporal logic formulae [FLTL](https://doi.org/10.1145/949952.940106) to write properties that can be checked against models and also as a form of constructing models.
 
 
@@ -20,13 +21,13 @@ fluent Ready[i:N] = <ready[i], reset[i]> initially False
 
 # Assertions in FLTL
 
-FLTL properties are constructed with the assert keyword using fluent or events as atoms, non-temporal operators  -- || (or), && (and), <-> (iff), -> (implication), !( (negation) --, quantifiers ----- forall, exists--, and temporal operators -- U (Until). W (weak until), X (next), <> (eventually), [] (always).
+FLTL properties are constructed with the `assert` keyword using `fluent` names or action names as atoms, non-temporal operators (`||` (or), `&&` (and), `<->` (iff), `->` (implication), `!` (negation)), quantifiers (`forall`, `exists`), and temporal operators (`U` (Until), `W` (weak until), `X` (next), `<>` (eventually), `[]` (always)).
 
 ```
 assert ALL_READY = forall[i:N] ([]<>Ready[i])
 ```
 
-To check a behaviour model against a property, a composite process must be chosen from the pulldown menu at the top of the application window. Then Check->LTL from the menu.
+To check a behaviour model against a property, select a composite process from the pulldown menu at the top of the application window, then use **Check > LTL** from the menu.
 
 # Observers defined in FLTL
 
@@ -37,12 +38,12 @@ ltl_property ONOFF = ([](on -> X off) && [](off -> X on) && on)
 ||MONITORED_SYS = (ONOFF || SYS).
 ```
 
-The ltl_property keyword works similarly to the property keyword, except that the former takes a safety property expressed in FLTL and the latter a sequential process defined in FSP.
+The `ltl_property` keyword works similarly to the `property` keyword, except that the former takes a safety property expressed in FLTL and the latter a sequential process defined in FSP.
 
 
 # Constraints defined in FLTL
 
-The constraint keyword builds a process that constrains all behaviour that violates a given FLTL safety property. Where ltl_property flags an error, constraint impedes the event that would flag that error.
+The `constraint` keyword builds a process that constrains all behaviour that violates a given FLTL safety property. Where `ltl_property` flags an error, `constraint` impedes the event that would flag that error.
 
 ```
 constraint ONOFF2 = ([](on -> X off) && [](off -> X on) && on)
@@ -51,7 +52,7 @@ constraint ONOFF2 = ([](on -> X off) && [](off -> X on) && on)
 
 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 of an alphabetised next.
+This implies that the interpretation of the next operator (`X`) is of an alphabetised next.
 
 ```
 constraint P = [] (p -> X q)