User Manual for Rodin v.2.3: Visibility of identifiers

3.2.7 Visibility of identifiers

This table shows which identifiers can be used in predicates or expressions.

Sets: Sets that are defined in the context (in case of an axiom) or in a seen context. If a context extends another context, the sets of the extended context are treated as if they are defined in the extending context.
Constants: Like the sets, constants that are defined in the context (in case of an axiom) or in a seen context.
Concrete Variables: Variables that are defined in the machine itself. This does not include variables of refined machines.
Abstract Variables: Variables that are defined in an abstract machine.
Concrete Parameters: Parameters that are defined in the event itself. This does not include parameters of refined events.
Abstract Parameters: Parameters that are defined in an abstract event.

			concrete	abstract	concrete	abstract
	sets	constants	variables	variables	parameters	parameters
axiom	$\times$	$\times$
invariant	$\times$	$\times$	$\times$	$\times$
variant	$\times$	$\times$	$\times$	$\times$
guard	$\times$	$\times$	$\times$	$\times$	$\times$
witness $^{*}$	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$
action $^{*}$	$\times$	$\times$	$\times$	$\times$	$\times$

$\mbox{}^{*}$ Witnesses and actions have additional identifiers in their scope. See 3.2.3.4.4 for details on witnesses resp. 3.3.8 for the scope of the different assignments in actions.

Rodin Handbook

3.2.7 Visibility of identifiers