REACH language

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 specified.
• 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 or C set_of_numbers or C place or C set_of_places – Finds a condition or a set of conditions by 0-based (1-based before July 2023) number, place, or set thereof
• E number or E set_of_numbers or E transition or E set_of_transitions or E signal or E set_of_signals – Finds an event or a set of events by 0-based (1-based before July 2023) number, transition, signal, or set thereof
• P name or P set_of_names or P number or P set_of_numbers or P condition or P set_of_conditions– Finds a place or a set of places by name, 0-based (1-based before July 2023) number, condition, or set thereof
• T name or T set_of_names or T number or T set_of_numbers or T event or T set_of_events or T signal or T set_of_signals – Finds a transition or a set of transitions by name, 0-based (1-based before July 2023) number, event, signal, or set thereof
• S name or S set_of_names or S number or S set_of_numbers or S event or S set_of_events or S transition or S set_of_ transitions – Finds a signal or a set of signals by name, 0-based (1-based before July 2023) number, event, transition, or set thereof
• cond place or cond set_of_places – Removed (superseded by C) since July 2023
• ev transition or ev signal or ev set_of_transitions or ev set_of_signals – Removed (superseded by E) since July 2023
• pls condition or pls set_of_conditions – Removed (superseded by P) since July 2023
• tran event or tran set_of_events or tran signal or tran set_of_signals – Removed (superseded by T) since July 2023
• sig event or sig transition or sig set_of_events or sig set_of_ transitions – Removed (superseded by S) since July 2023
• PP regular_expression – Finds a set of places whose names match the given regular expression in POSIX ERE format
• TT regular_expression – Finds a set of transitions whose names match the given regular expression in POSIX ERE format
• SS regular_expression – Finds a set of signals whose names match the given regular expression in POSIX ERE format
• # event or # condition or # place or # transition or # signal – Returns the number of a condition, event, place, transition or signal; the number is 0-based (1-based before July 2023)
• 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 is initially enabled, or a signal is initially high
• 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
• 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 is 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, i.e. () is not allowed, and (expression) is interpreted as an expression enclosed in parentheses.

• 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