-- Ammunition Storage System without Compatibility Groups
-- For Chapter 6 (sets)
-- Second version: with distributed operators & cardinality

types

Point :: x : nat
         y : nat;

StoreName = token;

Object :: position : Point
          xlength  : nat
          ylength  : nat; 

Store :: contents : set of Object
         xbound   : nat
         ybound   : nat
	 name     : StoreName

inv mk_Store(contents, xbound, ybound, -) ==

-- 1. objects fit within bounds of the store
   (forall o in set contents & InBounds(o,xbound,ybound))
   and 

-- 2. no two distinct objects overlap
   not exists o1, o2 in set contents & o1 <> o2 and Overlap(o1,o2);

--
-- Additional material for distributed operators
--

Site = set of Store
inv site == 
   forall st1, st2 in set site & st1.name = st2.name => st1 = st2;

InventoryItem :: store : StoreName   
                 item  : Object;

Inventory = set of InventoryItem


functions

-- Auxiliary functions for invariant

InBounds : Object * nat * nat -> bool
InBounds(o,xbound,ybound) == 
   o.position.x + o.xlength <= xbound and 
   o.position.y + o.ylength <= ybound;

Overlap : Object * Object -> bool
Overlap(o1,o2) ==
   Points(o1) inter Points(o2) <> {}; 

Points : Object -> set of Point
Points(mk_Object(pos,xlen,ylen)) == 
   {mk_Point(x,y) | x in set {pos.x ,..., pos.x + xlen},
                    y in set {pos.y ,..., pos.y + ylen}};


-- Main Functionality

NumObjects : Store -> nat
NumObjects(s) == card s.contents;


RoomAt: nat * nat * Store * Point -> bool
RoomAt(xlength,ylength,s,p) == 
   let new_o = mk_Object(p,xlength,ylength) in 
      InBounds(new_o,s.xbound,s.ybound) and 
      not exists o1 in set s.contents & Overlap(o1,new_o);


SuggestPos(xlength,ylength:nat, s:Store) p:[Point]
post if exists pt:Point & RoomAt(xlength,ylength,s,pt) 
     then RoomAt(xlength,ylength,s,p)
     else p = nil;


Place: nat * nat * Store * Point -> Store
Place(xlength,ylength,s,p) == 
   let new_o = mk_Object(p,xlength,ylength) in 
   mk_Store(s.contents union {new_o},
            s.xbound,
            s.ybound,
            s.name)
pre RoomAt(xlength,ylength,s,p);

Remove : Store * set of Point -> Store
Remove(mk_Store(contents,xbound,ybound,name),sp) == 
   let os = {o |o in set contents & o.position in set sp} in
   mk_Store(contents\os, xbound, ybound, name);

SiteInventory : Site -> Inventory
SiteInventory(site) == 
  dunion {StoreInventory(store)|store in set site};

StoreInventory : Store -> Inventory
StoreInventory(store) == 
  {mk_InventoryItem(store.name,o) | o in set store.contents}