|
class StockWatcher is subclass of GLOBAL
instance variables
eventHistory : seq of Event;
stockRecord : StockRecord;
sm : [StockMarket];
currentlyTriggeredAction : [ActionType];
inv eventHistory(len eventHistory).Type = <EntersNoActionRegion>
and
forall e in set inds eventHistory & e <> len eventHistory =>
(eventHistory(e).Type = <LeavesNoActionRegion> => eventHistory(e + 1).Type = <LowerLimit>
or eventHistory(e + 1).Type = <UpperLimit>)
and
(eventHistory(e).Type = <EntersNoActionRegion> => eventHistory(e + 1).Type = <LeavesNoActionRegion>
or eventHistory(e + 1).Type = <Valley>
or eventHistory(e + 1).Type = <Peak>);
operations
public StockWatcher: StockRecord * seq1 of Event ==> StockWatcher
StockWatcher(sr, predefinedEvents) == (
eventHistory := predefinedEvents;
sm := nil;
stockRecord := sr;
currentlyTriggeredAction := nil;
)
pre let val = predefinedEvents(len predefinedEvents).Value
in
IsInRegion(val,sr.NoActionReg);
public StockWatcher: StockRecord ==> StockWatcher
StockWatcher(sr) == (
sm := World`stockMarket;
stockRecord := sr;
eventHistory := [mk_Event(<EntersNoActionRegion>,0,
sm.GetStock(stockRecord.Name).GetCurrentValue())];
currentlyTriggeredAction := nil;
)
pre (sr.Name in set World`stockMarket.GetStockNames())
and
let val = World`stockMarket.GetStock(sr.Name).GetCurrentValue()
in
IsInRegion(val,sr.NoActionReg);
UpdateEvents : nat ==> ()
UpdateEvents(time) ==
let stock = sm.GetStock(stockRecord.Name)
in
let stockHistory = stock.GetValueHistory(), reg = stockRecord.NoActionReg,
l = reg.LowerValue, u = reg.UpperValue, cv = stock.GetCurrentValue()
in
(if IsInRegion(hd stockHistory, reg) and
not IsInRegion(stockHistory(2), reg)
then eventHistory := [mk_Event(<EntersNoActionRegion>,time,cv)] ^ eventHistory
elseif not IsInRegion(hd stockHistory, reg) and
IsInRegion(stockHistory(2), reg)
then eventHistory := [mk_Event(<LeavesNoActionRegion>,time,cv)] ^ eventHistory;
if hd stockHistory = u and stockHistory(2) <> u
then eventHistory := [mk_Event(<UpperLimit>,time,cv)] ^ eventHistory
elseif hd stockHistory = l
and stockHistory(2) <> l
then eventHistory := [mk_Event(<LowerLimit>,time,cv)] ^ eventHistory
elseif not IsInRegion(hd stockHistory, reg) and IsPeak(stockHistory)
then eventHistory := [mk_Event(<Peak>,time,cv)] ^ eventHistory
elseif (not IsInRegion(hd stockHistory, reg)
and IsValley(stockHistory) )
then eventHistory := [mk_Event(<Valley>,time,cv)] ^ eventHistory;
IO`print(eventHistory)
)
pre let stockHistory = sm.GetStock(stockRecord.Name).GetValueHistory()
in len stockHistory >= 2
post eventHistory(len eventHistory).Type = <EntersNoActionRegion>
and
forall e in set inds eventHistory & e <> len eventHistory =>
(eventHistory(e).Type = <LeavesNoActionRegion> => eventHistory(e + 1).Type = <LowerLimit>
or eventHistory(e + 1).Type = <UpperLimit>)
and
(eventHistory(e).Type = <EntersNoActionRegion> => eventHistory(e + 1).Type = <LeavesNoActionRegion>
or eventHistory(e + 1).Type = <Valley>
or eventHistory(e + 1).Type = <Peak>);
UpdateAction : nat ==> ()
UpdateAction(tim) ==
let actionTrigger = stockRecord.Triggers(stockRecord.State)
in
currentlyTriggeredAction :=
if IsActionTriggeredAtTime(tim,actionTrigger,eventHistory) and
not IsInRegion(GetStockValue(tim), stockRecord.NoActionReg)
then actionTrigger.Action
else nil;
public ObserveStock : nat ==> ()
ObserveStock(time) == (
if (World`simulate)
then UpdateEvents(time);
UpdateAction(time);
)
post NoActiveTriggerInNoActionRegion(GetStockValue(time),stockRecord.NoActionReg,currentlyTriggeredAction);
public updateStockRecord : StockRecord ==> ()
updateStockRecord(sr) ==
stockRecord := sr;
pure public GetStockValue : nat ==> StockValue
GetStockValue(time) ==
if World`simulate
then return eventHistory(1).Value
else return eventHistory(len eventHistory - time).Value
pre len eventHistory > 0;
pure public GetTriggeredAction : () ==> [ActionType]
GetTriggeredAction() ==
return currentlyTriggeredAction;
functions
NoActiveTriggerInNoActionRegion: StockValue * Region * [ActionType] -> bool
NoActiveTriggerInNoActionRegion(sv,reg,at) ==
IsInRegion(sv,reg) => at = nil;
IsInRegion: StockValue * Region -> bool
IsInRegion(sv,reg) ==
let u = reg.UpperValue , l = reg.LowerValue
in
sv >= l and sv <= u;
IsPeak: seq of StockValue -> bool
IsPeak(svs) ==
let current = hd svs
in
let indicesOneAbove = {i | i in set inds svs
& current+1 = svs(i) and i <> len svs}
in
exists i in set indicesOneAbove &
forall v in set {2,...,i} & current+1 = svs(v)
and
svs(i+1) = current;
IsValley: seq of StockValue -> bool
IsValley(svs) ==
let current = hd svs
in
let indicesOneBelow = {i | i in set inds svs & current-1 = svs(i) and i <> len svs}
in
exists i in set indicesOneBelow &
forall v in set {2,...,i} & current-1 = svs(v)
and
svs(i+1) = current;
FindLowestIndexFromTime: nat * seq of Event -> nat1
FindLowestIndexFromTime(time,events) ==
let pastEvents = { x | x in set inds events & events(x).TimeStamp <= time }
in
let i,j in set pastEvents be st (i <> j) => (events(i).TimeStamp <= events(j).TimeStamp)
in
i;
public IsActionTriggeredAtTime: nat * ActionTrigger * seq of Event -> bool
IsActionTriggeredAtTime(time,action,eventHistory) ==
let tgr = action.Trigger
in
let index = FindLowestIndexFromTime(time,eventHistory),
s = eventHistory(index,...,index + len tgr - 1)
in
((forall i in set inds s & s(i).Type = tgr(i))
and (s(1).TimeStamp = time)
and len s = len tgr)
end StockWatcher
¤ Dauer der Verarbeitung: 0.18 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.
|
