Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMRT/CyberRailRT/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 5 kB

Quelle CyberRail.vdmrt Sprache: VDM

\section{CyberRail class}

\begin{vdm_al}

class CyberRail

instance variables

private normalState : bool := true;
private curtime : nat := 0;

private railway : RailwayGrid;
private q_APM_out : ActivePlanManager;
private q_Env_in : seq of MessageTypes`MessageT := [];
private q_APM_in : seq of MessageTypes`MessageT := [];
private busy : bool := false;
private timeout : nat := 0;

types

public NavigationInput ::
departureLocation : String
arrivalLocation : String
transportChoice : Choice
id_token : nat1

inv n == len n.departureLocation > 0 and
len n.arrivalLocation > 0 ;

public String = seq of char;
public Choice = <Cheapest>|<Quickest>

operations

public setRailwayGrid : RailwayGrid ==> ()
setRailwayGrid(grid)== (
railway := grid;
);

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

public calculateTransportPlan : NavigationInput * TokenDevice ==>
                                [TransportPlan`DTO]
calculateTransportPlan(navInput, tokenDevice) ==
(
dcl tempPlan : TransportPlan;
dcl tempGrid : RailwayGrid`Grid := railway.getGrid();
def l = {r | r in set tempGrid
            & r(1).departureLocation = navInput.departureLocation and
              r(len r).arrivalLocation = navInput.arrivalLocation}
in (
  if card l = 0
  then
  (
   return nil;
  )
  else if navInput.transportChoice = <Cheapest>
  then
   tempPlan :=  new TransportPlan(findCheapest(l),
                                  <Cheapest>,
                                  navInput.id_token)
  else tempPlan :=  new TransportPlan(findQuickest(l),
                                      <Quickest>,
                                      navInput.id_token);
);
return tempPlan.getByValue();
)
pre exists r in set railway.getGrid() &
      r(1).departureLocation = navInput.departureLocation and
      r(len r).arrivalLocation = navInput.arrivalLocation;

public setActiveRoute : nat ==> ()
setActiveRoute(id_Route) == is not yet specified;

private findCheapest : RailwayGrid`Grid ==> [seq of TransportPlan`Route]
findCheapest(list) ==
(
dcl sum : real := 0;
dcl cheap : real := 9999;
dcl rtn : seq of TransportPlan`Route := [];

for all s in set list do
(
  sum := 0;
  for r in s do
   sum := sum + r.fee;
  if sum < cheap then
  (
   cheap := sum;
   rtn := s;
  );
);
return rtn;
);

private findQuickest : RailwayGrid`Grid ==> [seq of TransportPlan`Route]
findQuickest (list) == findCheapest(list);

public setQ_APM_out : ActivePlanManager ==> ()
setQ_APM_out(apm) == (
q_APM_out := apm;
);

async public addToStimuliQueue : MessageTypes`MessageT ==> ()
addToStimuliQueue(msg) ==
(
q_Env_in := q_Env_in ^ [msg];
);

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

public handleEvents : () ==> ()
handleEvents() ==
(
duration(0)(
if len q_Env_in > 0 or len q_APM_in > 0
then(
  busy := true;
  if(len q_Env_in > 0)
  then
   handleQ_Env_in()

  else if ( normalState and len q_APM_in > 0)
  then
    handleQ_APM_in();
  )
  else
   busy := false;

  if(not normalState and (curtime + timeout) <= time)
  then
   finalizeInactiveRoute();
);

);

private handleQ_Env_in : () ==> ()
handleQ_Env_in() == (
let msg = hd q_Env_in
in
  (cases msg:
mk_MessageTypes`INACTIVEROUTE(-) -> handleInactiveRoute(msg),
mk_MessageTypes`ACTIVEROUTE(-) -> skip,
mk_MessageTypes`ADDROUTE(-) -> skip,
mk_MessageTypes`REMOVEROUTE(-) -> skip
   end;
   );
reduce_Q_Env();
)
pre len q_Env_in > 0;

private handleQ_APM_in : () ==> ()
handleQ_APM_in() == (
let msg = hd q_APM_in
in
  (cases msg:
mk_MessageTypes`CALCPLAN(navi, tokenDevice) ->
       handleCalcPlan(navi, tokenDevice)
   end;
   );
reduce_Q_APM();
)
pre len q_APM_in > 0;

private handleCalcPlan : CyberRail`NavigationInput * TokenDevice ==> ()
handleCalcPlan(navi, tokenDevice)==(
q_APM_out.addToSystemQueue( mk_MessageTypes`RETURNPLAN(
       calculateTransportPlan(navi, tokenDevice), tokenDevice))
);

private handleInactiveRoute : MessageTypes`MessageT ==> ()
handleInactiveRoute(msg) ==
(
normalState := false;
curtime := time;
let mk_MessageTypes`INACTIVEROUTE(routeid) = msg in
(
  q_APM_out.addToSystemQueue(mk_MessageTypes`STRATEGYINIT());
  railway.setInactiveRoute(routeid);
  q_APM_out.addToSystemQueue(mk_MessageTypes`STRATEGYNOTIFY(routeid));
);

);

private finalizeInactiveRoute : () ==> ()
finalizeInactiveRoute()==
(
q_APM_out.addToSystemQueue(mk_MessageTypes`STRATEGYEND());
normalState := true;
);

public setInactiveRoute : nat ==> ()
setInactiveRoute(id_Route) == (
skip;
);

private reduce_Q_APM : () ==> ()
reduce_Q_APM () == q_APM_in := tl q_APM_in
pre len q_APM_in > 0;

private reduce_Q_Env : () ==> ()
reduce_Q_Env () == q_Env_in := tl q_Env_in
pre len q_APM_in > 0;

thread
while(true) do
(
  handleEvents();
   )

sync
per handleEvents => (len q_Env_in + len q_APM_in) > 0;

per isFinished =>  (len q_Env_in + len q_APM_in) = 0;

mutex(reduce_Q_Env,addToStimuliQueue);
mutex(reduce_Q_APM,addToSystemQueue);
mutex(reduce_Q_Env);
mutex(reduce_Q_APM);
mutex(calculateTransportPlan);
mutex(addToStimuliQueue);
mutex(addToSystemQueue);
end CyberRail
\end{vdm_al}

quality93%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.