====== 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:
<code reach>
// 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 }
}
</code>

<code reach>
// all transitions are not enabled
forall t in TRANSITIONS { ~@t }
</code>
===== Comments =====
%%C++%%-style comments are supported:
  * from **%%//%%** to the end of the line
  * enclosed in **%%/*…*/%%** 

===== Type system =====
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.

===== Constants =====
  * **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!")

===== Names (identifiers) =====
Built of English letters, digits and '_', not starting with a digit, case sensitive.

===== Pre-defined names =====

  * 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

===== 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 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 
  * <del>**cond** place</del> or <del>**cond** set_of_places</del> -- Removed (superseded by **C**) since July 2023
  * <del>**ev** transition</del> or <del>**ev** signal</del> or <del>**ev** set_of_transitions</del> or <del>**ev** set_of_signals</del> -- Removed (superseded by **E**) since July 2023
  * <del>**pls** condition</del> or <del>**pls** set_of_conditions</del> -- Removed (superseded by **P**) since July 2023
  * <del>**tran** event</del> or <del>**tran** set_of_events</del> or <del>**tran** signal</del> or <del>**tran** set_of_signals</del> -- Removed (superseded by **T**) since July 2023
  * <del>**sig** event</del> or <del>**sig** transition</del> or <del>**sig** set_of_events</del> or <del>**sig** set_of_ transitions</del> -- 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
===== Binary operators =====
  * &, |, ^, %%->%%, %%<->%% -- 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
===== Indexing and conditional operators =====
  * 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++
===== Multi-operand operators =====
  * **[**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.
===== Iterators =====

  * **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.:

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

The identifiers within a tuple pattern must be distinct.

===== Name declaration =====
  * **let** var**=**value **{** expression **}** -- Creates a name with a fixed value and scope

===== Operator precedence and associativity =====

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