help:reach

The language REACH is used for specifying reachability properties. Using a language for specifying properties has the following advantages:

- Custom properties can be easily and concisely speciﬁed.
- The user does not have to modify the model in any way, in particular the model does not have to be translated into an input language of some model checker.
- Almost any reachability analyser can be used as the back-end.

For example, the following alternative REACH predicates express the deadlock property:

// each transition has a place in its preset that is not marked // (and so the transition is not enabled) forall t in TRANSITIONS { exists p in pre t { ~$p } }

// all transitions are not enabled forall t in TRANSITIONS { ~@t }

C++-style comments are supported:

- from
**//**to the end of the line - enclosed in
**/*…*/**

Each value belongs to one of the following types:

- Boolean
- integer
- string
- event of the unfolding prefix
- condition of the unfolding prefix
- place of the Petri net
- transition of the Petri net
- signal of the STG
- set of
*T*where*T*is a type (set of set of set … of*T*is allowed) - tuples with at least two elements, with the elements of any allowed types, including tuples
- special type for the
**fail**expression

The types are never mentioned explicitly, but rather derived from the structure of the sub-expression.

**true**,**false**are the two constants forming type Boolean- integer constants, e.g. 3, 10, -33
- C-style string constants enclosed in quotation marks (e.g. “Hello world!”)

Built of English letters, digits and '_', not starting with a digit, case sensitive.

- CONDITIONS – the set of conditions of the unfolding prefix, including the postsets of cut-off events
- EVENTS – the set of events of the unfolding prefix, including cut-offs
- CUTOFFS – the set of cut-off events of the unfolding prefix
- PLACES – the set of places of the Petri net
- TRANSITIONS – the set of transitions of the Petri net
- SIGNALS – the set of all signals of the STG
- INPUTS – the set of input signals of the STG
- OUTPUTS – the set of output signals of the STG
- INTERNAL – the set of internal signals of the STG
- DUMMY – the set of dummy signals of the STG
- LOCAL – the set of local (i.e. output and internal) signals of the STG

**fail**string – Creates a special failure expression to report errors; has a complicated semantics**$**event or**$**condition or**$**place or**$**signal – Interpreted on the configuration C to be reached: returns true iff the event is in C, or the condition is in Cut(C), or the place is in Mark(C), or the signal is 1 in Code(C)**@**event or**@**transition or**@**signal – Interpreted on the configuration C to be reached: returns true iff C enables event/transition/signal**'**signal – Interpreted on the configuration C to be reached: returns true iff the next state of signal is high in the final state of C; equivalent to ($ signal ^ @ signal)**C**number – Finds a condition by number**E**number – Finds an event by number**P**name or**P**number – Finds a place by name or number**T**name or**T**number – Finds a transition by name or number**S**name or**S**number – Finds a signal by name or number**PP**regular_expression – Finds a set of places whose names match the given regular expression**TT**regular_expression – Finds a set of transitions whose names match the given regular expression**SS**regular_expression – Finds a set of signals whose names match the given regular expression**#**event or**#**condition or**#**place or**#**transition or**#**signal – Returns the number of a condition, event, place, transition or signal**name**place or**name**transition or**name**signal – Returns the name of a place, transition or signal**string**expression – Returns a string representation of the argument**len**string – Returns the length of a string**downclose**event or**downclose**set_of_events – Downcloses an event or a set thereof, returning a set of events**trig**event – Computes the set of triggers of an event, returning a set of events**is_init**event or**is_init**condition or**is_init**place or**is_init**transition or**is_init**signal – Checks if a condition/place is initially marked, or an event/transition/signal is initially enabled**is_cutoff**event – Checks if an event is cut-off**is_input**signal or**is_input**transition or**is_input**event – Checks if a signal, transition or event is an input**is_output**signal or**is_output**transition or**is_output**event – Checks if a signal, transition or event is an output**is_internal**signal or**is_internal**transition or**is_internal**event – Checks if a signal, transition or event is internal**is_dummy**signal or**is_dummy**transition or**is_dummy**event – Checks if a signal, transition or event is dummy**is_local**signal or**is_local**transition or**is_local**event – Checks if a signal, transition or event is local;**is_local***x*is equivalent to (**is_output***x*|**is_internal***x*)**is_plus**event or**is_plus**transition – Checks if an STG event or transition has a sign '+'**is_minus**event or**is_minus**transition – Checks if an STG event or transition has a sign '-'**~**bool – Boolean negation**-**number – Unary minus**pre**event or**pre**condition or**pre**place or**pre**transition or**pre**set_of_events or**pre**set_of_conditions or**pre**set_of_places or**pre**set_of_transitions – Preset of a node or set of nodes**post**event or**post**condition or**post**place or**post**transition or**post**set_of_events or**post**set_of_conditions or**post**set_of_places or**post**set_of_transitions – Postset of a node or set of nodes**cond**place or**cond**set_of_places – Set of conditions corresponding to a place or a place set**ev**transition or**ev**signal or**ev**set_of_transitions or**ev**set_of_signals – Set of events corresponding to a transition, a signal, a transition set or a signal set**pls**condition or**pls**set_of_conditions – Place corresponding to a condition, or place set corresponding to a condition set**tran**event or**tran**set_of_events or**tran**signal or**tran**set_of_signals – Transition corresponding to an event, or transition set corresponding to an event set, a signal or a signal set**sig**event or**sig**transition or**sig**set_of_events or**sig**set_of_ transitions – Signal corresponding to an event or a transition, or signal set corresponding to event set or an transition set**card**set – Set cardinality**is_empty**set – Checks if a set is empty**pick**set – Picks the element from a singleton set

- &, |, ^, ->, <-> – Boolean AND, OR, XOR, implication, and equivalence
- +, -, *, /, % – Numerical operators as usual
- =, != – Equality and non-equality for non-Booleans, as long as the argument types agree; for Booleans use <-> and ^ instead
- <, <=, >, >= – Numerical comparisons and set inclusion
- + – String concatenation
- +, *, \ – Set union, intersection, and difference
- element
**in**set – Set membership

- string
**[**number**]**– Returns a string comprised of a single characters at the given position; the characters are indexed starting from 0 - string
**[**number**..**number**]**– Returns a substring of a string; either of the numbers can be omitted, in which case the beginning or the end of the string is substituted instead of it; the characters are indexed starting from 0 - tuple
**[**number**]**– Returns the element of a tuple at the given position; the elements are indexed starting from 0; the index must be a numerical literal, not just an expression of numeric type – this necessary for determining the type of this sub-expression before the expansion stage - condition
**?**expression**:**expression – Conditional expression, like in C/C++

**[**number**](**bool**,**bool**,**…**,**bool**)**– Multi-operand threshold operator**{**expression**,**expression**,**…**,**expression**}**– Constructs a set out of several expressions of the same type; an empty set cannot be constructed in this way, as its type cannot be determined**(**expression**,**expression**,**…**,**expression**)**– Constructs a tuple out of several expressions; the tuples must have at least two elements

**forall**var**in**set**s.t.**predicate**{**expression**}**– Constructs an AND-expression by filtering and transforming elements of the given set**exists**var**in**set**s.t.**predicate**{**expression**}**– Constructs an OR-expression by filtering and transforming elements of the given set**xorsum**var**in**set**s.t.**predicate**{**expression**}**– Constructs an XOR-expression by filtering and transforming elements of the given set**threshold[**number**]**var**in**set**s.t.**predicate**{**expression**}**– Constructs a threshold operator by filtering and transforming elements of the given set; if**[**number**]**is dropped, 2 is assumed**gather**var**in**set**s.t.**predicate**{**expression**}**– Constructs a set by filtering and transforming elements of the given set

The **s.t.** clause is optional. The `var`

can be replaced by a tuple pattern, e.g.:

forall ((x,),,y) in { ((1,2),3,4), ((5,6),7,8) } { x<y } /* evaluates to true as 1<4 and 5<8 */

The identifiers within a tuple pattern must be distinct.

**let**var**=**value**{**expression**}**– Creates a name with a fixed value and scope

The precedence of operators in the decreasing order is as follows. The associativity is specified in parentheses wherever relevant. Some binary operators are non-associative, i.e. A **op** B **op** C is a syntax error.

- postfix unary operators – these are string and tuple indexing;
- prefix unary operators;
- *, /, % (left-associative)
- +, -, \ (left-associative)
**in**(non-associative)- =, !=, >, <, >=, <= (non-associative)
- & (left-associative)
- ^ (left-associative)
- | (left-associative)
- -> (right-associative)
- <-> (left-associative)
- ?: (right-associative), i.e. A ? B : C ? D : E is parsed as A ? B : (C ? D : E) rather than (A ? B : C) ? D : E