Quelle World.vdmrt Sprache: VDM

% WORLD.vdmrt

\subsubsection{Top-level specification -- the \texttt{World} class}

This specification was developed and checked using the first release of the DESTECS tool,
which is based on Overture version 1.0.0 (Release Candidate 1). The VDM-RT dialect has been
chosen here because the ChessWay is using a distributed controller architecture.
The \texttt{World} class is the top-level entry point of the ChessWay VDM++ discrete event
specification. All necessary simulation constants are defined here.

\begin{vdm_al}
class World

values
  -- in this model use nanosecond resolution
  public SIM_RESOLUTION = 1E9;

  -- maximum simulation time is 10 seconds
  public MAX_SIM_TIME = 20 * SIM_RESOLUTION

instance variables
  -- are we running a co-simulation or not
  public static cosim : bool := false

\end{vdm_al}

First decision is to define the discrete time step size used in the model.
The current release of the DESTECS tool provides a default granuarity of 1~nsec.
Since the controllers in the ChessWay are likely to run at 10~kHz in practice,
this should cause no problems when modelling. As a convenience, we run
simulations for 10~seconds at the moment.
A major trade-off is the simulation time step versus simulation (execution) time.
Currently performance is (s)low, taking about 5 minutes to simulate 10 seconds,
this is mainly caused by the trace (log) files generated by the DESTECS tool
which become very huge (up to 100~Mbyte for a single run). The entry point of
the specification is the \texttt{Run} operation. Starting the simulation is
performed by creating a debug configuration in the DESTECS tool that will execute
the operation \texttt{new World().Run()}. This operation will create an instance
of the model and the environment and then load a user-defined scenario.
This scenario defines the initial settings of all ChessWay devices (such as
the safety, direction and on/off switches). The scenarios also specify the
evolution of the state of those settings over time, during the simulation run.
These scenarios basically provide an abstract (and discrete time) representation
of their continuous time behaviors.

\begin{vdm_al}
operations
  -- top-level access function for ChessWay co-simulation
  public run : () ==> ()
  run () ==
    ( -- set the co-simulation indicator
      cosim := true;
      -- execute the same model
      RunScenario("steeringsignal1.csv") );

  -- top-level access function for ChessWay DE only simulation
  public RunVdmRt : () ==> ()
  RunVdmRt () == RunScenario("scenario1.txt");

  -- top-level access function to run a particular scenario
  public RunScenario: seq1 of char ==> ()
  RunScenario (fname) ==
    ( -- create an instance of the Environment model
      dcl env : Environment :=
        new Environment(self, MAX_SIM_TIME);

      -- load a simulation scenario
      if cosim
      then env.loadCsvFile("USER", fname)
      else env.loadScenario(fname);

      -- link the environment to the system controllers
      ChessWay`lctrl.setEnvironment(env);
      ChessWay`rctrl.setEnvironment(env);

      -- cross link the two system controller models
      ChessWay`lctrl.setRightController(ChessWay`rctrl);
      ChessWay`rctrl.setLeftController(ChessWay`lctrl);

      -- announce start of simulation run
      IO`print("Starting ChessWay DE simulation\n");

   -- initialize the system tasks
      ChessWay`lctrl.PowerUp();
      ChessWay`rctrl.PowerUp();

      -- start the environment and periodic loopcontroller tasks
      startlist({env, ChessWay`lctrl, ChessWay`rctrl});

      -- wait for simulation run end (lock main DESTECS GUI thread)
      waitForSimulationEnd();

      -- announce end of simulation run
      IO`print("ChessWay DE simulation completed at ");
      IO`print(time / SIM_RESOLUTION);
      IO`print(" sec\n") )
\end{vdm_al}

The \texttt{RunScenario} operation instantiates the entire simulation model.
The model consists of two main parts, the so-called environment model,
represented by the \texttt{Environment} class and the system model, represented
by the \texttt{ChessWay} system class. The \texttt{ChessWay} class is implicitly
constructed by the interpreter at startup. Note that the environment model is
basically an abstraction of those elements in the physical (and continous time) world
that have an impact on the behavior of our system. The primary elements we are concerned
about here are the wheels and the person standing on the ChessWay. Note that their
behavior are best described in continous time, but here we have made an discrete time
approximation, in order to execute and test our discrete controller model of the ChessWay.

First, the user scenario is loaded and the environment model is statically
linked to the ChessWay system model. These static links are just to facilitate
the modeling and simulation process, they have no counterpart in reality. Once
these links are put in place, simulation can commence by starting the ChessWay
controllers, by calling the \texttt{PowerUp} operations on both the left
and right controller instances. These operations in turn will start
the periodic controller threads internal to those objects. The
penultimate step is to start the environment simulator thread, in order to
execute the scenario. Finally, the main DESTECS interpreter thread will wait
for the simulation to finish, by calling \texttt{waitForSimulationEnd},
after which some statistics are printed, and control is given back to
the user running the simulation.

\begin{vdm_al}
instance variables
  -- boolean to indicate when simulation run is complete
  public finish : bool := false

operations
  -- auxiliary operation to wait for simulation run to finish
  private waitForSimulationEnd: () ==> ()
  waitForSimulationEnd () ==
    -- print conditional diagnostics
    if ChessWay`debug
    then ( ChessWay`lctrl.printDiagnostics();
           ChessWay`rctrl.printDiagnostics() );

  public signal: () ==> ()
  signal () ==
    ( finish := true;
      IO`println("Environment requests end of simulation") );

sync
  -- the environment task has to unlock the main thread
  per waitForSimulationEnd => finish

end World
\end{vdm_al}

The operation \texttt{waitForSimulationEnd} is an operation guarded by a
permission predicate which is initially \texttt{false}. This implies that
the main DESTECS interpreter thread, which always has the highest
priority, will immediately block as soon as this operation is called. This
will cause the lower priority threads in the model (the environment and the two
controller processes) to continue nominally and these will cause simulation
time to elapse. It is the environment thread that will set the \texttt{finish}
instance variable to \texttt{true}, causing the simulation to halt, because
the DESTECS user-interface interpreter thread resumes control causing all other
threads to freeze because it always has the highest priority.

quality91%

¤ Dauer der Verarbeitung: 0.18 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.