Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
48/190
Things become a bit more involved when data may change over time and thus needs to
be stored in a variable. Here we show three methods of dealing with this: global variables,
facts, and shared sets used e.g. as global databases.
2.4.1
Global variables
A standard method is similar to the style using global constants mentioned before in the
introduction to this section. The shared variable is declared in an outer entity and may be
used in any inner one. See the following example.
% @verbatim ( Modifiable shared variable by inheritance )
% @clatse ( - - nb 2)
% @ofmc ( NO )
specification S h a r e d V a r i a b l e 1 _ U n s a f e
channel_model CCM
entity Environment {
symbols
succ ( nat ): nat ;
entity Session (A , B : agent ) {
symbols
SharedVar : nat ;
entity Alice ( Actor , B : agent ) {
body {
SharedVar := succ ( SharedVar );
% this refers two times to the inherited
% shared variable - does not work for OFMC !
Actor * - > B : i ; % just an authentic signal to B
}
}
entity Bob (A , Actor : agent ) {
body {
A * - > Actor : i ;
assert t e s t _ S h a r e d V a r _ s t i l l _ 1 : SharedVar = 1;
% should report violation because now
% " shared ( SharedVarId , succ (1))" holds
}
}
FP7-ICT-2007-1
Project No. 216471