Quelle EnvTask.vdmrt Sprache: VDM

class EnvironmentTask

instance variables
  -- use a unique identifier for each generated event
  --static temporarily commented out because LookUp does not work
  private num : nat := 0;

  -- we limit the number of inserted stimuli
  protected max_stimuli : nat := 0;

  -- administration for the event traces
  -- e2s is used for all out-going stimuli (environment to system)
  -- s2e is used for all received responses (system to environment)
  protected e2s : map nat to nat := {|->};
  protected s2e : map nat to nat := {|->}

functions
  -- checkResponseTimes verifies for each received response whether
  -- or not the elapse time did (not) exceed the user-defined limit
  public checkResponseTimes: map nat to nat * map nat to nat * nat -> bool
  checkResponseTimes (pe2s, ps2e, plim) ==
    forall idx in set dom ps2e &
      ps2e(idx) - pe2s(idx) <= plim
  -- the responses received should also be sent
  pre dom ps2e inter dom pe2s = dom ps2e

operations
  public EnvironmentTask: nat ==> EnvironmentTask
  EnvironmentTask (pno) == max_stimuli := pno;

  public getNum: () ==> nat
  getNum () == ( dcl res : nat := num; num := num + 1; return res );

  -- Run shall be overloaded to implement the event generation loop
  -- towards the system. typically, it starts a periodic thread
  public Run: () ==> ()
  Run () == is subclass responsibility;

  public HandleEvent: nat ==> ()
  HandleEvent (pev) == is subclass responsibility;

  -- logEnvToSys is used to register when an event was inserted into
  -- the system. note that the 'time' keyword refers to the internal
  -- simulation wall clock of VDMTools
  public logEnvToSys: nat ==> ()
  logEnvToSys (pev) == e2s := e2s munion {pev |-> time};

  -- logSysToEnv is used to register when an event was received from}
  -- the system. note that the 'time' keyword refers to the internal}
  -- simulation wall clock of VDMTools}
  public logSysToEnv: nat ==> ()
  logSysToEnv (pev) == s2e := s2e munion {pev |-> time};

  -- getMinMaxAverage calculates the minimum, maximum and average
  -- response times that were observed during execution of the model
  -- note that getMinMaxAverage is blocked until the number of
  -- system responses is equal to the number of sent stimuli
  -- termination is ensured because only a maximum number of stimuli
  -- is allowed to be inserted in the system, so eventually all
  -- stimuli can be processed by the system. this method only works
  -- when each stimulus leads to exactly one response, which is the
  -- case in this instance
  public getMinMaxAverage: () ==> nat * nat * real
  getMinMaxAverage () ==
    ( dcl min : [nat] := nil, max : [nat] := nil, diff : nat := 0;
      for all cnt in set dom s2e do
        let dt = s2e(cnt) - e2s(cnt) in
          ( if min = nil then min := dt
            else (if min > dt then min := dt);
            if max = nil then max := dt
            else (if max < dt then max := dt);
            diff := diff + dt );
      return mk_(min, max, diff / card dom s2e) )
pre card dom s2e > 0;

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

sync
  -- getNum is mutually exclusive to ensure unique values
  mutex (getNum);
  -- getMinMaxAverage is blocked until all responses have been received
  per getMinMaxAverage => card dom s2e >= max_stimuli;

  per IsFinished => #fin(logSysToEnv) > 0;

end EnvironmentTask

quality91%

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