Bilddatei AutomatedStockBroker.vdmpp   Sprache: VDM

class AutomatedStockBroker is subclass of GLOBAL
  
instance variables
  stocks : seq of StockRecord;
  stockWatchers : map StockIdentifier to StockWatcher;
  actionLog : seq of ActionEvent := [];
  balance : int;
  inv balance >= 0;
  -- no stock can have the same name  
  inv forall x,y in set inds stocks & x <> y => stocks(x).Name <> stocks(y).Name;

  --says that foreach ActionEvent in the log if there exist a next action with the same 
  --Stock name, it should have a different ActionType. this insures that you dont sell or buy the same
  --two times in a row
  inv let stockIdentifiers = {si.Name | si in set elems stocks}
      in 
        forall stockIdentifier in set stockIdentifiers & 
          let allEventsStock = [ e | e in seq actionLog 
                                   & e.StockName = stockIdentifier]
          in 
            (forall i in set inds allEventsStock & 
               (i <> len allEventsStock) => 
               (allEventsStock(i).Type <> allEventsStock(i+1).Type)); 
       
  inv MaxOneOfEachActionTypePerTime(actionLog);    
  

operations

public AutomatedStockBroker: nat ==> AutomatedStockBroker
AutomatedStockBroker(startCash) == (
  balance := startCash;
  stocks := [];
  stockWatchers := {|->};
);

public AddStock: StockRecord * nat1 ==> ()
AddStock(sRecord,priority) == (
  stocks := stocks(1,...,priority-1) ^ [sRecord] 
            ^ stocks(priority+1,...,len stocks);
  if (World`simulate)
  then stockWatchers(sRecord.Name) := new StockWatcher(sRecord)
  else stockWatchers(sRecord.Name) := new StockWatcher(sRecord,testValues(sRecord.Name));
)
pre sRecord.Name not in set { x.Name | x in seq stocks}
post (sRecord.Name in set dom stockWatchers) 
     and (sRecord = stocks(priority)); 
  
public GetActionLog:() ==> seq of ActionEvent
GetActionLog() == 
  return actionLog;
  
public GetStocksWithActiveActionTrigger: StockState ==> seq of StockRecord
GetStocksWithActiveActionTrigger(ss) == 
  return [e | e in seq stocks  
            & (stockWatchers(e.Name).GetTriggeredAction() <> nil)
              and (e.State = ss)]
post let res = RESULT in forall i in set inds res & res(i).State = ss;
  
pure FindValidBuy: seq of StockRecord * nat ==> [StockRecord]
FindValidBuy(potBuys,time) ==  
  return let affordableStocks = 
    [x | x in seq potBuys & CanAfford(x,balance)]
     in 
     (
      if(len affordableStocks > 0)
      then let x in seq affordableStocks be st  
       (forall y in seq affordableStocks & (stockWatchers(x.Name).GetStockValue(time)) >= 
       (stockWatchers(y.Name).GetStockValue(time)))
       in x
      else nil 
     );
    
pure FindValidSell: seq of StockRecord * nat ==> StockRecord
FindValidSell(potSells,time) == 
  return let x in seq potSells be st  
    (forall y in seq potSells & 
      (stockWatchers(x.Name).GetStockValue(time) - x.Cost) >= 
      (stockWatchers(y.Name).GetStockValue(time) - y.Cost))
    in x  
pre len potSells > 0
post IsGTAll(stockWatchers(RESULT.Name).GetStockValue(time) - RESULT.Cost,
  {stockWatchers(x.Name).GetStockValue(time) - x.Cost | x in seq potSells});

  PerformBuy: StockRecord * nat ==> ()
  PerformBuy(potAction,time) == 
   let sw = stockWatchers(potAction.Name),value = sw.GetStockValue(time)  
   in
   (
    actionLog := [mk_ActionEvent(<Buy>,time,potAction.Name,value)] ^ actionLog;
    balance := balance - value;

    let i in set inds stocks be st stocks(i).Name = potAction.Name
     in
    (
     stocks(i) := mu(potAction, State |-> <Bought>, Cost |-> value );
     sw.updateStockRecord(stocks(i))
    ) 
   )
  pre potAction.State = <PotentialBuy> and 
   stockWatchers(potAction.Name).GetTriggeredAction() = <Buy>
  post balance >= 0;

  PerformSell: StockRecord * nat ==> ()
  PerformSell(potAction,time) == 
   let sw = stockWatchers(potAction.Name),value = sw.GetStockValue(time) 
   in
   (
    actionLog := [mk_ActionEvent(<Sell>,time,potAction.Name,value)] ^ actionLog;
    balance := balance + value;
    
    let i in set inds stocks be st stocks(i).Name = potAction.Name
     in
    (
     stocks(i) := mu(potAction, State |-> <PotentialBuy>, Cost |-> 0);
     sw.updateStockRecord(stocks(i))
    ) 
   )
  pre potAction.State = <Bought> and 
   stockWatchers(potAction.Name).GetTriggeredAction() = <Sell>  
  post balance >= 0;
  
  ObserveAllStocks: nat ==> ()
  ObserveAllStocks(time) == 
   for all i in set inds stocks do
    let stock = stocks(i), csw = stockWatchers(stock.Name)
     in csw.ObserveStock(time);

  public Step: nat ==> ()
  Step(time) == (

   ObserveAllStocks(time);
      
   let potBuys = GetStocksWithActiveActionTrigger(<PotentialBuy>) , 
    potSells = GetStocksWithActiveActionTrigger(<Bought>),
    validBuy = FindValidBuy(potBuys,time)
    in
    (
     if(len potSells > 0)
     then (PerformSell(FindValidSell(potSells,time), time);)
     else skip;
     IO`print("\npot sels : ");
     IO`print(potSells);

     if(validBuy <> nil)
     then (PerformBuy(validBuy, time);)
     else skip;
     IO`print("\npot buys : ");
     IO`print(potBuys);
    );  
   
   IO`print("\n");
   IO`print("Finished step : ");
   IO`print(time);
   IO`print(" with actionLog : ");
   IO`print(actionLog);
   IO`print(" and Balance : ");
   IO`print(balance);
   IO`print("\n");
  )
  post MaxOneOfEachActionTypePerTime(actionLog);

functions

IsGTAll: int * set of int -> bool
IsGTAll(sv,ssv) == 
  forall i in set ssv & sv >= i;

CanAfford: StockRecord * nat -> bool
CanAfford(sr,balance) == 
  sr.Cost <= balance;
    
MaxOneOfEachActionTypePerTime: seq of ActionEvent -> bool
MaxOneOfEachActionTypePerTime(actionLog) == 
  forall x,y in set inds actionLog & 
     (x <> y and actionLog(x).Time = actionLog(y).Time) => 
     (actionLog(x).Type <> actionLog(y).Type)

end AutomatedStockBroker