| products/sources/formale sprachen/VDM/VDMRT/CyberRailRT/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: TransportPlan.vdmrt Sprache: VDMOriginal von: VDM© |
|
||||||
|
\section{TransportPlan class}
\begin{vdm_al} class TransportPlan instance variables private id_token : nat; private totalFee : real; private totalDuration : nat; private choice : CyberRail`Choice; public routeList : seq of Route := []; private routesTravled : seq of Route := []; inv len routeList > 0 => forall i in set inds routeList & i < len routeList => routeList(i).arrivalLocation = routeList(i+1).departureLocation; types public Route :: departureLocation : CyberRail`String arrivalLocation : CyberRail`String fee : real platform : CyberRail`String dur : nat id_route : nat inv r == len r.platform > 0 and len r.arrivalLocation > 0 and len r.departureLocation > 0 and r.fee >= 0 ; public DTO :: id_token : nat routeList : seq of Route choice : CyberRail`Choice operations --Constructor public TransportPlan : seq of Route * CyberRail`Choice * nat ==> TransportPlan TransportPlan(routes, pChoice, id_tok) == ( id_token := id_tok; choice := pChoice; routeList := routes; ); public getNextRoute : () ==> TransportPlan`Route getNextRoute () == ( return hd routeList; ) pre len routeList > 0; public containsRoute: nat ==> bool containsRoute(id_route) == return exists r in set elems routeList & r.id_route = id_route pre len routeList > 0; public addRoute: Route ==> () addRoute(route) ==( routeList := routeList^[route]; totalFee:= totalFee + route.fee ) pre routeList(len routeList).arrivalLocation = route.departureLocation; public routeTraveled: () ==> () routeTraveled () == ( routesTravled := routesTravled ^ [hd routeList]; routeList := tl routeList; ) pre len routeList > 0; pure public routesRemaining : () ==> nat routesRemaining() == ( return len routeList;); public getByValue : () ==> DTO getByValue()== return mk_TransportPlan`DTO(id_token, routeList, choice); public getPlanAsNaviInput: () ==> CyberRail`NavigationInput getPlanAsNaviInput() ==( return mk_CyberRail`NavigationInput((hd routeList).departureLocation, (routeList(len routeList)).arrivalLocation, choice, id_token ) ) pre len routeList > 0; public getTokenId: () ==> nat getTokenId() == return id_token; --debug public getRouteList: () ==> seq of Route getRouteList()== return routeList; sync mutex(routeTraveled); end TransportPlan \end{vdm_al} ¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
