|
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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
