ass1_q2.mch

这里几个源代码是用BToolkit软件写的。这是关于一些操作

 
MACHINE           ass1_q2

SETS		  ITEMS; ORDER

CONSTANTS         AMOUNT, maxamount

PROPERTIES	  maxamount :NAT& AMOUNT=0..maxamount &	maxamount =100	  

VARIABLES         orderlist, stock, stockelem

INVARIANT         stockelem<:ITEMS&
		  orderlist :ITEMS <-> AMOUNT& 
		  stock :ITEMS <-> AMOUNT&
		  dom(stock) = stockelem 
		  

INITIALISATION    orderlist := {} || stock := {} ||stockelem := {}
		

OPERATIONS

  receiveorder(ii:ITEMS; mm :AMOUNT)=
		PRE ii |-> mm /: orderlist
		THEN orderlist := orderlist \/ {ii |-> mm}

		END;


  
  receivestock(ii:ITEMS;mm:AMOUNT)=
		
		IF ii /:dom(stock)
		
		THEN    stockelem := stockelem \/ {ii} ||
			stock := stock \/ {ii |-> mm}
		ELSE 	stock(ii):= stock(ii)+mm
		END;

  oo <-- howmany(ii:ITEMS)=
		PRE stock[{ii}] /= {}
		THEN oo := stock(ii)
		END;


  oo <-- whereisitem(ii:ITEMS)=
		PRE orderlist /= {}
		THEN oo := orderlist|> orderlist[{ii}]
		END;


  oo <-- totordered(ii:ITEMS)=
		PRE orderlist[{ii}] /= {}
		THEN oo := SIGMA(elm).(elm:orderlist[{ii}]|elm)
 		END;


  oo <-- lowstock(nn:AMOUNT)=
		PRE stock /= {}
 		THEN oo := {ii|ii:dom(stock)& nn >stock(ii)}
		END;


  oo <-- oneoflowest=
		PRE stock /={} 
		THEN oo := {ii|ii:dom(stock)&stock(ii)=min(ran(stock))}
		END;
  
  
 serviceorder(ii:ITEMS;mm:AMOUNT) =	
		PRE orderlist /={} & ii:dom(stock) & stock(ii)>mm
		THEN 
			IF ii:dom(stock)& mm < stock(ii)
			THEN stock(ii):= stock(ii)-mm ||
			     orderlist:= orderlist-{ii |-> mm}
			END
		END 

END