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:

forall t in TRANSITIONS { 
  exists p in pre t { ~$p }
}
forall t in tran EVENTS { ~@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)
  • 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

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

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; the characters are indexed starting from 0
  • 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