User Tools

Site Tools


help:reach

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 }

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 – 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

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 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

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

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.

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