Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ActivePlanManager.vdmrt Sprache: VDM

Original von: VDM^©

\section{ActivePlanManager class}
\begin{vdm_al}

class ActivePlanManager is subclass of Strategy

instance variables

private activeTokens : inmap TokenDevice to TransportPlan := {|->};
inv forall x,y in set dom activeTokens &
x = y =>  activeTokens(x) = activeTokens(y);
--Ensure only one TokenDevice reside in the map.
--Tests if 2 elements from domain is equal then (implication) they point
--to the same entity.

private busy : bool := false;

private q_CR_out: CyberRail;

private tokenDevices : set of TokenDevice;
private q_Tok_in : seq of MessageTypes`MessageT := [];
private q_CR_in : seq of MessageTypes`MessageT := [];
private q_Tok_out : seq of TransportPlan := [];

private state : State := <run>;

types

public State =  <run> | <halt>;

operations

--Strategy-------------------------------------------------
protected strategyInit : () ==> ()
strategyInit() ==
(
state := <halt>
);

protected strategyNotify : () ==> ()
strategyNotify() == skip; -- is subclass responsibility;

protected strategyEnd : () ==> ()
strategyEnd() ==
(
state := <run>;
);

protected handleEvents : () ==> ()
handleEvents() ==
is not yet specified;
-----------------------------------------------------------
  public ActivePlanManager : ()  ==> ActivePlanManager
  ActivePlanManager() == (skip;);

public isFinished : () ==> ()
isFinished () == skip;

  public inactiveRoute : nat ==> ()
  inactiveRoute(id_route) ==
  (
  duration(50)
  (
  for all t in set rng activeTokens do
  (

   if t.containsRoute(id_route)
   then
   (let p = inverse activeTokens in
      q_CR_out.addToSystemQueue(
                mk_MessageTypes`CALCPLAN(
                 t.getPlanAsNaviInput(),p(t)));
   )
    );
  );
);

public addTransportPlan : TransportPlan * TokenDevice ==> ()
  addTransportPlan(plan,tokenDevice) ==(

   activeTokens := activeTokens ++ {tokenDevice|-> plan};
q_Tok_out := q_Tok_out ^ [plan];
);

public removeTransportPlan : TransportPlan * TokenDevice ==> ()
  removeTransportPlan(plan,tokenDevice) ==(
  activeTokens := {tokenDevice} <-: activeTokens;
  --Restrict map to not contain a mapplet containing tokenDevice
);

public getPlans : () ==> set of TransportPlan
  getPlans() == return rng activeTokens;

public handleEvent : () ==> ()
handleEvent() == (
if((len q_CR_in + len q_Tok_in + len q_Tok_out) <> 0)
then(
  if(len q_CR_in <> 0  )
  then
    handleQ_CR_in()

  else if(state = <run> and len q_Tok_out <> 0)
  then
   handleQ_Tok_out()

  else if(state = <run> and len q_Tok_in <> 0)
  then
   handleQ_Tok_in()
)
else
  busy := false;
);

private handleQ_Tok_out : () ==> ()
handleQ_Tok_out() == (
let ptt_map = inverse activeTokens, plan = hd q_Tok_out in (
  let tokenDevice = ptt_map(plan) in (
   tokenDevice.notifyPassenger(plan);
  );
  q_Tok_out := tl q_Tok_out;
)
)
pre len q_Tok_out > 0 and
    exists plan in set rng activeTokens & plan = hd q_Tok_out;

private handleQ_CR_in : () ==> ()
handleQ_CR_in() ==
(
busy := true;

  let msg = hd q_CR_in in
  (cases msg:
    mk_MessageTypes`RETURNPLAN(-,-) -> handleTransportPlan(msg),
    --mk_MessageTypes`INACTIVEROUTE(-) -> handleInactiveRoute(msg),
    mk_MessageTypes`STRATEGYNOTIFY(-) -> handleInactiveRoute(msg),
    mk_MessageTypes`STRATEGYINIT() -> handleStrategyInit(),
    mk_MessageTypes`STRATEGYEND() -> handleStrategyEnd()
  end;
  );
  reduce_Q_CR();
)
pre len q_CR_in > 0;

private handleQ_Tok_in : () ==> ()
handleQ_Tok_in()==
(
busy := true;
  let msg = hd q_Tok_in in
  (
   cases msg:
    mk_MessageTypes`REQUESTPLAN(-,-) -> handleRequestPlan(msg)
   end;
  );
reduce_Q_Tok();
)
pre len q_Tok_in > 0;

private handleStrategyInit : () ==> ()
handleStrategyInit()== (
Logger`write("Read StrategyINIT "); Logger`write(time);
state := <halt>;
);

private handleStrategyEnd : () ==> ()
handleStrategyEnd()== (
state := <run>;
);
private handleInactiveRoute : MessageTypes`MessageT ==> ()
handleInactiveRoute(msg) ==
(
let mk_MessageTypes`STRATEGYNOTIFY(routeid) = msg in
(
  inactiveRoute(routeid);
)
);

private handleTransportPlan :  MessageTypes`MessageT ==> ()
handleTransportPlan(msg) ==
(

let mk_MessageTypes`RETURNPLAN(dto, tok) = msg in
(
  addTransportPlan(new TransportPlan(dto.routeList,
                   dto.choice, dto.id_token), tok);
)
);

private handleRequestPlan : MessageTypes`MessageT ==> ()
handleRequestPlan(msg) ==
(

let mk_MessageTypes`REQUESTPLAN(navi, tok) = msg in
  (
   q_CR_out.addToSystemQueue(
             mk_MessageTypes`CALCPLAN(navi,tok));
  )
);

private reduce_Q_Tok : () ==> ()
reduce_Q_Tok () == q_Tok_in := tl q_Tok_in
pre len q_Tok_in > 0;

private reduce_Q_CR : () ==> ()
reduce_Q_CR () == (q_CR_in := tl q_CR_in;
)
pre len q_CR_in > 0;

--Initialize CyberRail ref.
public setQ_CR_out :  CyberRail ==> ()
setQ_CR_out(cr) == (q_CR_out := cr);

public addToSystemQueue : MessageTypes`MessageT ==> ()
addToSystemQueue(msg) ==
(
q_CR_in := q_CR_in ^ [msg];
);

async public addToClientQueue : MessageTypes`MessageT ==> ()
addToClientQueue(msg)==
(
q_Tok_in := q_Tok_in ^ [msg];
);

thread
while true do
(
   handleEvent();
)

sync

per handleEvent => ((len q_CR_in + len q_Tok_in + len q_Tok_out) > 0);
per isFinished => (len q_CR_in + len q_Tok_in + len q_Tok_out)=0;
mutex(reduce_Q_Tok,addToClientQueue);
mutex(reduce_Q_CR,addToSystemQueue);
mutex(addToSystemQueue);
mutex(addToClientQueue);
mutex(handleEvent);
mutex(reduce_Q_Tok);
mutex(reduce_Q_CR);

end ActivePlanManager

\end{vdm_al}

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.