class ConWorld

types

public PurseId = token


instance variables

-- we separate "purses" and "authentic" below, then connect them with
-- the invariant. This will allow us to introduce inauthentic purses
-- later.  

private authentic : set of PurseId;

-- collection of purses in the world
public conPurses : map PurseId to ConPurse := {|->};
inv forall name in set dom conPurses & name in set authentic;

-- to enable message-passing
private ether : Ether;

-- a record of all previous messages sent. 
private previousmessages : set of ConPurse`TransDetails;


operations

-- initiate transaction (this is promotion?)
public ConTransfer : PurseId * PurseId * nat ==> ()
ConTransfer(name1, name2, val) ==
(
    let p1seqNo = conPurses(name1).GetSeqNo(),
        p2seqNo = conPurses(name2).GetSeqNo()
    in
    (
        ether.StartFrom(name1, mk_ConPurse`CounterPartyDetails(name2, val, p2seqNo));
        ether.StartTo(name2, mk_ConPurse`CounterPartyDetails(name1, val, p1seqNo));
    )
)
pre name1 in set dom conPurses and name2 in set dom conPurses;


-- ACCESSORS

-- return the purse object with the given name
public GetPurse : PurseId ==> ConPurse
GetPurse(name) ==
    return conPurses(name)
pre name in set dom conPurses;

-- returns the mapping conPurses 
public GetConPurses : () ==> map PurseId to ConPurse 
GetConPurses() ==
    return conPurses;

    
-- HOUSEKEEPING

-- constructor
public ConWorld : set of PurseId ==> ConWorld
ConWorld(names) == 
(
    ether := new PerfectEther(self);
    
    -- all purses are authentic (for now)
    authentic := names;
    
    -- instantiate purses
    conPurses := {name |-> new ConPurse(name, 100) | name in set names};
        
    -- introduce ether to purses
    for all purse in set rng conPurses do purse.DiscoverEther(ether);
);


functions

-- RETRIEVE FUNCTION
public retr : ConWorld -> AbWorld
retr(c) ==
    new AbWorld({name |-> retrPurse(c.GetPurse(name)) | name in set dom c.GetConPurses()}, dom c.GetConPurses());

-- helper function for retr to retrieve a single purse
public retrPurse : ConPurse -> AbPurse
retrPurse(conpurse) ==
    new AbPurse(conpurse.GetBalance(), conpurse.GetLost());

end ConWorld