products/Sources/formale Sprachen/Coq/test-suite/bugs/closed/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: outer_measure_def.prf   Sprache: VDM

Untersuchung VDM©
class World

types

public TMSId = seq of char;
  
instance variables

static network : Network := new Network({|->});
env: Environment;
static public tms1: TMS := new TMS("Rotterdam", network);
static public tms2: TMS := new TMS("RWS", network);
static tms_m : map TMSId to TMS := {"Rotterdam" |-> tms1, "RWS" |-> tms2};
collaboration : bool := true;

operations

public run: ()  ==> () --Performance
  run() == (
   Run("RotterdamNetwork.csv", "TMSconfiguration.csv", 300)
 );
 
public runwithoutcollab: ()  ==> () --Performance
  runwithoutcollab() == (
   SetCollaboration(false);
   Run("RotterdamNetwork.csv", "TMSconfiguration.csv", 300)
 );
 
  public Run: seq of char * seq1 of char * [nat] ==> () --Performance
  Run(network_file, tms_file, simtime) == (
   network := ReadRoadNetwork(network_file);
   for all tid in set dom tms_m do
     tms_m(tid).ResetNetwork(network,self);
   ReadTMSs(tms_file, network);
   env := new SimulatorEnvironment(network, tms_m, simtime);
   for all tid in set dom tms_m do
     tms_m(tid).UpdateInternalEdges();
   env.Run(collaboration,network_file,tms_file)
 );
   
  public ReadRoadNetwork: seq1 of char ==> Network
  ReadRoadNetwork(file_n) ==
    let mk_(ok,lines) = CSV`flinecount(file_n)
    in
      if ok 
      then (dcl net : map Network`EdgeId to Edge := {|->};
            for i = 1 to lines do
            -- each line in the network configuration file contains
            -- - The identifier of the edge
            -- - the starting node for the edge
            -- - the ending node for the edge
            -- - the length of the edge
            -- - the number of lanes for the edge
            -- - the maximum speed for the edge
            -- - flow of cars into the edge
             let mk_(ok,[edgeid,startid,endid,l,lane,max,inflow]) = 
                  CSV`freadval[seq of (nat | seq of char)](file_n,i)
             in net(edgeid) := new Edge(max,lane,l,mk_token(startid),mk_token(endid));
             return new Network(net)
           )
      else error;
      
  public ReadTMSs: seq of char * Network ==> ()
  ReadTMSs(file_n, n) ==
    let mk_(ok,lines) = CSV`flinecount(file_n)
    in
      if ok 
      then (for i = 1 to lines do
            -- each line in the TMS configuration file contains:
            -- - the identification of the TMS
            -- - an identification of the edge included
            -- - a traffic control measure if available (alternatively nil is included)
            -- - a priority if available (alternatively nil is included)
            -- - possible suggested routes to make diversions avoiding the edge
             let mk_(ok,[tmsid,edgeid,tcm,prio,diversions]) = 
                  CSV`freadval[seq of ([nat] | seq of char |set of seq of seq of char)](file_n,i),
                  tid = tmsid
             in (  --{["A202","S109","S102","A153"],["A42","A43","A152","A153"],["A42","S114","S102","A153"]}
               if not tid in set dom tms_m 
               then tms_m(tid) := new TMS("Invalid TMS", n);-- this should never happen
               tms_m(tid).AddEdge({edgeid});
               if tcm <> nil and tcm <> "Bridge" then tms_m(tid).AddTCM(edgeid,TMS`ConvertTCM(tcm));
               if tcm <> nil and tcm = "Bridge" then tms_m(tid).AddBridge(edgeid,TMS`ConvertBridge(tcm));
               if prio <> nil then tms_m(tid).AddPriority(edgeid,prio);
--               if diversions <> nil
--               then network.AddDiversionRoutes(edgeid, 
--                                               {[r(j) | j in set inds r]
--                                               | r in set diversions})
             );
       for all tid in set dom tms_m do tms_m(tid).CalculateInterest(n);-- sort out interested edges
           )
      else error;
      
 public SetCollaboration: bool ==> ()
 SetCollaboration(b) ==
   collaboration := b;

end World

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff