% @verbatim(Modifiable shared variable implemented via facts)

specification SharedVariable2_Unsafe
channel_model CCM 

entity Environment {
  symbols
    succ(nat): nat;

  entity Session (A, B: agent) {

    symbols
      shared(protocol_id, message): fact;
      SharedVarId: protocol_id;

    entity Alice (Actor, B: agent, SharedVarId: protocol_id) {
    % note that Alice and Bob does not inherit SharedVarId, but
    % gets a copy of of the reference to SharedVar as parameter

      symbols
        ValueOfSharedVar: nat;
      body {
      % read and remove the old value and set a new value:
        retract (shared(SharedVarId, ?ValueOfSharedVar));
        shared(SharedVarId, succ(ValueOfSharedVar));
        Actor *->  B: i; % just an authentic signal to B
      }
    }

    entity Bob (A,Actor: agent, SharedVarId: protocol_id) {

      body {
        A *-> Actor: i;
        assert test_SharedVar_still_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);
}