<variable definition> ::=
dcl
[revealed| exported | revealed exported | exported revealed]
<variables of sort> {, <variables of sort> }*<end>
<variables of sort> ::=
<variable name>
[ <exported as>] {, <variable name> [<exported as>]}*
<sort> [:= <ground expression>]
<exported as> ::= as <remote variable identifier>
<exported as> may only be used for a variable with the exported attribute. Two exported variables in a process, including possible services, cannot mention the same <remote variable identifier>.
When a variable is created and the <ground expression> is present, then the variable is associated with the value of the <ground expression>. Otherwise, the variable has no value associated, i.e. the variable is "undefined".
The revealed attribute allows all other processes of the same block to read the value of a variable, provided they have a <view definition> with the same name and sort.
The exported attribute allows a variable to be used as an exported variable.