/*
  This is a B specification of the CAMA Location abstraction. It is
  the foundation for the cCAMA implementation of the scoping mechanism.
  L. Laibinis, A. Iliasov, E. Troubitsyna, A. Romanovsky
*/
MACHINE
  location

SETS
  AGENTS; 
  SCOPES;
  ROLES;
  PUBLIC_DATA;
  RESULT = {Success,Failure}

DEFINITIONS
  DCriteria == PUBLIC_DATA --> BOOL;
  RoleData == struct (min_a:NATURAL, max_a:NATURAL, criteria:DCriteria);
  DScopeDescriptor == (ROLES +-> RoleData);
  DScopeRequest    == (ROLES +-> NATURAL * DCriteria);
  min_agents(scope,role) == ((ScopeAttributes(scope))(role))'min_a;
  max_agents(scope,role) == ((ScopeAttributes(scope))(role))'max_a;
  role_criteria(scope,role) == ((ScopeAttributes(scope))(role))'criteria;
  role_data(agent,role) == (AgentRoleData(agent))(role)


CONSTANTS
  DefaultRole,    /* default role 'Agent' */
  AgentFailure,   /* special agent_id indicating creation failure */
  ScopeFailure,   /* special scope_id indicating creation failure */
  Creators        /* roles that have right to create scopes */


PROPERTIES
  DefaultRole: ROLES &
  AgentFailure: AGENTS &
  ScopeFailure: SCOPES &
  Creators <: ROLES

VARIABLES
  AgentNames,       /* Agent names issued so far by the location */
  Scopes,           /* Created scopes */
  ScopeRolesTaken,  /* The number of roles currently taken in scopes */
  AgentRoleData,    /* Public role data disclosed by agents */  
  AgentScopes,      /* All the scopes created by corresponding agents */
  ScopeAttributes,  /* Scope descriptions provided by scope creators */
  AgentRoles        /* The roles taken by agents in active scopes */

INVARIANT
  AgentNames <: AGENTS &
  Scopes <: SCOPES &
  ScopeRolesTaken: SCOPES * ROLES +-> NATURAL &
  AgentRoleData: AgentNames --> (ROLES +-> PUBLIC_DATA) &
  AgentScopes: AGENTS <-> SCOPES &
  ScopeAttributes:  Scopes --> DScopeDescriptor &
  AgentRoles: AGENTS*SCOPES +-> ROLES &
  dom(AgentScopes) <: AgentNames &
  ran(AgentScopes) <: Scopes &
  dom(AgentRoles) = AgentScopes 
 
INITIALISATION
  BEGIN
    Scopes        := {} ||
    AgentNames    := {} ||
    AgentRoleData := {} ||
    AgentScopes   := {} ||
    AgentRoles    := {} ||
    ScopeAttributes := {} ||
    ScopeRolesTaken := {}
  END

OPERATIONS


/* Connect request from some agent */
a_id <-- Engage =
  ANY Role_and_Data WHERE
      Role_and_Data : ROLES +-> PUBLIC_DATA & 
      card(Role_and_Data) >= 1 & DefaultRole : dom(Role_and_Data) & 
      AgentNames <<: AGENTS-{AgentFailure}
  THEN
         CHOICE 
           ANY name WHERE name: AGENTS-{AgentFailure} & 
               name/: AgentNames 
           THEN
             AgentNames := AgentNames \/ {name} || 
             AgentRoleData := AgentRoleData \/ {name |-> Role_and_Data} ||
             a_id := name
           END
         OR
           a_id := AgentFailure
         END
  END;


/* Disconnect request from some agent */
rr <-- Disengage = 
  ANY a_id WHERE a_id: AgentNames 
  THEN
    IF not(a_id:dom(AgentScopes)) THEN
      AgentNames := AgentNames - {a_id} ||
      AgentRoleData := {a_id} <<| AgentRoleData ||
      rr := Success
    ELSE
      rr := Failure 
    END  
  END;
      

/* Scope create request from some agent */
scope_id <-- CreateScope =
  ANY a_id, scopeDescr, role WHERE
      a_id: AgentNames & scopeDescr: DScopeDescriptor & role: ROLES &
      role: Creators & role: dom(scopeDescr) & role: dom(AgentRoleData(a_id)) &
      Scopes <<: SCOPES-{ScopeFailure}
  THEN
    CHOICE
      ANY newScope WHERE newScope: SCOPES-{ScopeFailure} & 
          newScope /: Scopes & (a_id|->newScope) /: AgentScopes
      THEN
        Scopes := Scopes \/ {newScope} ||
        AgentScopes := AgentScopes \/ {a_id |-> newScope} ||
        scope_id := newScope ||
        ScopeRolesTaken := ScopeRolesTaken <+ {(newScope,role) |-> 1} ||
        AgentRoles := AgentRoles \/ {(a_id|->newScope) |-> role} || 
        ScopeAttributes := ScopeAttributes <+ {newScope |-> scopeDescr}
      END
    OR
      scope_id := ScopeFailure
    END  
  END; 


/* Scope remove request */
result <-- DeleteScope =
  ANY a_id, scope_id WHERE
      a_id: AgentNames & scope_id: Scopes &
      (a_id |-> scope_id): AgentScopes & 
      ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) > 0
  THEN
    CHOICE
      result := Success ||
      AgentScopes := AgentScopes |>> {scope_id} ||
      ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) := 
           ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) - 1 ||
      AgentRoles := (AgentScopes |>> {scope_id}) <| AgentRoles ||
      Scopes := Scopes - {scope_id} ||
      ScopeAttributes:= {scope_id} <<| ScopeAttributes
    OR
      result := Failure
    END
  END;


/* Scope join request */
result <-- JoinScope =
  ANY a_id, scope_id, role WHERE
      a_id: AgentNames & scope_id: Scopes & role: ROLES & 
      role: dom(AgentRoleData(a_id))
  THEN
    IF
      (a_id |-> scope_id) /: AgentScopes &
      role: dom(ScopeAttributes(scope_id)) &
      ScopeRolesTaken(scope_id,role) < max_agents(scope_id,role) & 
      (role_criteria(scope_id,role))(role_data(a_id,role)) = TRUE
    THEN
      AgentScopes := AgentScopes \/ {a_id |-> scope_id} || 
      ScopeRolesTaken(scope_id, role) := ScopeRolesTaken(scope_id, role) + 1 ||
      AgentRoles := AgentRoles \/ {(a_id |-> scope_id) |-> role} ||
      result := Success     
    ELSE
      result := Failure
    END
  END;


/* Scope leave request */
result <-- LeaveScope =
  ANY a_id, scope_id WHERE
      a_id: AgentNames & scope_id:Scopes & 
      ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) > 0
  THEN
    IF (a_id,scope_id):AgentScopes THEN
      AgentScopes := AgentScopes - {a_id |-> scope_id} ||
      ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) := 
         ScopeRolesTaken(scope_id,AgentRoles(a_id,scope_id)) - 1 ||
      AgentRoles := {a_id |-> scope_id}<<| AgentRoles ||
      result := Success
      /* Scope STATUS may change and that can affect other agents */
    ELSE
      result := Failure
    END
  END;


/* Get id's of the matching scopes */
scopes <-- GetScopes =
  ANY a_id, scopeRequest WHERE
      a_id: AgentNames & scopeRequest: DScopeRequest 
  THEN
    scopes :: iseq(Scopes)
  END

END