The language REACH is used for specifying reachability properties. This approach 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.
Constants
true, false
integers
strings (e.g. “Hello”)
events, conditions, places, transitions, signals – cannot be directly specified, but returned by some operators, like C, E, P, T, S, etc.
Variables
Built of English letters, digits and '_', not starting with a digit, case sensitive.
Unary operators
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 – Checks if a signal is an input
is_output signal – Checks if a signal is an output
is_internal signal – Checks if a signal is internal
is_dummy signal – Checks if a signal is dummy
is_local signal – Checks if a signal is local; equivalent to (is_output signal | is_internal signal)
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
evs transition or evs signal or evs set_of_transitions or evs 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
=, != – 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
Ternary operators
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
condition ? expression : expression – Conditional expression, like in C/C++
Multi-operand operators
threshold[number](bool, bool, …, bool) – Multi-operand threshold operator; if [number] is dropped, 2 is assumed
{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
Iterators
Below the “s.t.” clause is optional:
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
Name declaration
let var=value { expression } – Creates a name with a fixed value and scope