Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
51/190
on ( shared ( SharedVarId , ? ValueOfSharedVar )): {
retract ( shared ( SharedVarId , ValueOfSharedVar ));
shared ( SharedVarId , succ ( ValueOfSharedVar ));
}
}
Actor * - >
B: i;
% handover to B
}
}
entity Bob (A , Actor : agent , SharedVarId : protocol_id ) {
body {
A * - > Actor : i ;
% handover from A
assert t e s t _ S h a r e d V a r _ s t i l l _ 1 : shared ( SharedVarId , 1);
% reads the current value
% should report violation because now
% " shared ( SharedVarId , succ (1))" holds
}
}
body {
SharedVarId := fresh ();
shared ( SharedVarId , 1); % sets the initial value
new Alice (A ,B , SharedVarId );
new Bob (A ,B , SharedVarId );
}
}
body
any A B . Session (A , B ) where A != B & ! dishonest ( A );
}
This model uses all the mechanisms just described to achieve essentially the same effect as
the previous example.18
This variant is more involved than the previous one, but has the advantage that all three
model checkers, SATMC, OFMC and CL-AtSe can deal with it without problems.
2.4.3
Shared databases
A very typical way to implement shared databases is via sets, which by the semantics of
ASLan++ are implemented using references to (global) facts. This technique will be used,
18
Regarding semantics, there is one caveat: when changing the value of the shared variable, there might
be race conditions if between the retraction of the old value and the introduction of the new value there is
interleaving with any other entity instances that use the same shared variable. Yet due to default optimization
options of the translator, the retraction and the introduction are typically executed in a single atomic
transition.
FP7-ICT-2007-1
Project No. 216471