module mobile. 
import helmet.

% Code Mobility 

type place    Place -> list Agent -> list Facts -> o.
type agent    Place -> Def -> Thread -> Res -> Agent.  
type send     Agent -> Msg -> Res -> o.
type residue  Place -> list Agent -> o. 
type go       Place -> o. 
type exdb     Agent -> Op -> list Facts -> list Facts -> o.
type db       Op -> o.

sel Agent Agents Others  || anti || place P Agents DB -->   
 Agent || place P Others DB.  
       
true   || agent P Agent (go Q,Msgs) NewAgent  || place Q Agents DB  -->
 anti  || place Q ((agent Q Agent Msgs NewAgent)::Agents) DB.
    
exdb Agent Op DB NewDB || agent P Agent (db Op) NewAgent  || 
 place P Agents DB -->
  anti || place P Agents NewDB.
    
exdb Agent Op DB NewDB || agent P Agent (db Op,Msgs) NewAgent || 
 place P Agents DB -->
  agent P Agent Msgs NewAgent || place P Agents NewDB.

send Agent Msg NewAgent || agent P Agent Msg NewAgent  || residue P Rs  -->
 anti  || residue P (NewAgent::Rs).
   
send Agent Msg IntAgent || 
 agent P Agent (Msg,Msgs) NewAgent || place P Agents DB -->
  anti || place P ((agent P IntAgent Msgs Res)::Agents) DB. 
       
type app Info -> o.
type store o.
type get Info -> o.

exdb  Agent (get X) (X::DB) (X::DB).
exdb  Agent (store) DB NewDB:- append Agent DB NewDB.

send  Agent (app Y) (Y::Agent):-
  print "\n I've just stolen ",write Y.

type start o.
type ex o.
type trace o.
 
initial 
(place 1 
  ((agent 1 nil 
    (go 2,db (get X),app X,go 3,db (get Y),app Y,go 1,db store) 
     Outa
   )::nil
  ) 
  (1000::nil)| 
 place 2 nil (2000::nil) | 
 place 3 nil (3000::nil) |
 place 4 nil (4000::nil) |    
 residue 1 nil | 
 residue 2 nil |
 residue 3 nil |
 residue 4 nil
).
        
%start :-   spyon => ehhfsolve anti.  
start :-   ehhfsolve anti.