Trading Platform Spec

offer.tla

------------------------------- MODULE offer -------------------------------
EXTENDS Integers, Sequences, TLC

set ++ x == set \union {x}
set -- x == set \ {x}

People == {"alice", "bob", "eve"}
Items == {"hat"}

VARIABLES owner, offers
vars == <<owner, offers>>

Init ==
  /\ owner \in [Items -> People]
  /\ offers = {}

Propose(from, to, item) ==
  /\ owner[item] = from
  /\ offers' = offers ++ <<from, to, item>>
  /\ UNCHANGED owner

Accept(from, to, item) ==
  /\ <<from, to, item>> \in offers
  /\ offers' = offers -- <<from, to, item>>
  /\ owner' = [owner EXCEPT ![item] = to]

Reject(from, to, item) ==
  /\ <<from, to, item>> \in offers
  /\ offers' = offers -- <<from, to, item>>
  /\ UNCHANGED owner
  
  
Next ==
  \E from, to \in People, item \in Items:
    /\ from /= to
    /\ \/ Propose(from, to, item)
       \/ Accept(from, to, item)
       \/ Reject(from, to, item)

Spec == Init /\ [][Next]_vars

ValidChange(item) ==
  LET co == owner[item]
  IN co /= co' =>
    Accept(co, co', item)
    
ChangeInvariant ==
  [][\A i \in Items: ValidChange(i)]_owner 
=============================================================================