# GPSL syntax

**Generic Property Specification Language** (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis (aka LTL for Plug).

In GPSL each property is associated with a named variable. All these variables form the *property set*
Any subset of the *property set* can be verified during an analysis run.

### Assertions: Syntax & Semantics

There are two Boolean constants predefined in the language: **true** and **false**

Atomic proposition in GPSL are strings of characters enclosed between pairs of `|`

(ie. `| string of characters |`

). Each atomic proposition can be prefixed with two identifiers specifying the atomic proposition language and the ‘verification’ module on which it should be interpreted.

### Boolean Operators

Two expressions f and g can be combined using the following Boolean operators

Operation | syntax0 | syntax1 | syntax2 | syntax3 | syntax4 |
---|---|---|---|---|---|

negation | not f | !f | ~f | ||

disjunction | f or g | f | g | f \/ g | f + g | |

conjunction | f and g | f & g | f && g | f /\ g | f * g |

exclusion | f xor g | f ^ g | |||

implication | f implies g | f -> g | f => g | ||

equivalence | f iff g | f <-> g | f <=> g |

### Let Expressions

To simplify the expression of large formula GPSL uses Let expression forms to introduce variables.

```
let
v1 = expr
v2 = expr
...
vn = expr
in
v1 op v2
```

## Temporal Logic: Syntax & Semantics

The support for LTL is enabled using LTL3Buchi conversion [1].

### Temporal Logic Operators

Two expressions f and g can be combined using the following Boolean operators

operation | syntax0 | syntax1 | syntax2 |
---|---|---|---|

Next | X f | next f | () f |

Eventually | F f | eventually f | <> f |

Always | G f | globally f | [] f |

Strong Until | f U g | f until g | |

Weak Until | f W g | ||

Weak Release | f R g | f release g | f V g |

Strong Release | f M g |

## Some examples

```
aliceCS = |{Alice}1@CS|
bobCS = |{Bob}1@CS|
exclusionI = []!(|{Alice}1@I| && |{Bob}1@I|)
exclusion = []!(aliceCS && bobCS)
eventuallyOneInCS = []<>(aliceCS || bobCS)
fairness =
let
aliceFlagUP=|{sys}1:flags[0] = true|,
bobFlagUP=|{sys}1:flags[1] = true|
in
([] ( (aliceFlagUP -> (<> aliceCS) )
&& (bobFlagUP -> (<> bobCS))))
idling = let
aliceFlagUP=|{sys}1:flags[0]=true|,
bobFlagUP=|{sys}1:flags[1]=true|
in
([] (!aliceFlagUP -> (![] aliceCS))
&& (!bobFlagUP -> (![] bobCS)) )
infoften = [] <> bobCS
all = (exclusion & eventuallyOneInCS & fairness & idling)
```

## References

[1] Babiak, Tomáš, et al. “LTL to Büchi automata translation: Fast and more deterministic.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2012.