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