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


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Eisbach/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle Environment.vdmrt Sprache: VDM

-----------------------------------------------
-- Author: Sune Wolff - 20022462
-- Created: 20/4 - 2008
-- Updated:
-- Description: Environment class of the HomeAutomation project
-----------------------------------------------

--
-- class definition
--
class Environment

--
-- instance variables
--
instance variables

  private io       : IO := new IO();
  private inlines  : seq of inline := [];
  private outlines : seq of outline := [];
  private simtime  : nat;
  private finished : bool := false;
  private envTemp  : int := 20;
  private envHumid : int := 75;
--  inv envTemp >= 0;
--  inv envHumid >= 0;

--
-- Types definition section
--
types

-- Input file: TempIn, HumidIn, TimeIn
public inline = nat * nat * nat;
-- Output: Time, TempValue, HumidValue
public outline = nat * nat * nat;

--
-- Operations definition section
--
operations

public Environment: seq of char ==> Environment
Environment(fname) ==
(def mk_ (-,mk_(t,input)) = io.freadval[nat * seq of inline](fname)
  in
   (inlines := input;
    simtime := t;
    envTemp := 20;
    envHumid := 75;
   );
)
pre fname <> []
post inlines <> [] and simtime > 0;

private CreateSignal: () ==> ()
CreateSignal() ==
(if len inlines > 0
  then (dcl curtime : nat := time;
def mk_ (tempIn, humidIn, timeIn) = hd inlines
        in
         (if timeIn <= curtime
          then (SetTemp(tempIn);
                SetHumid(humidIn);
                inlines := tl inlines;
                return
               );
         );
       );
  if (time >= simtime)
  then (ShowResults();
        finished := true;
        return;
       );
);

private ShowResults: () ==> ()
ShowResults() ==
(IO`print("Time, Temperature, Humidity\n");

  for all i in set inds outlines
  do
   (IO`print("\n");
    IO`print(outlines(i));
   );
);

public HandleEvent: nat * nat * nat ==> ()
HandleEvent(curTime, TempValue, HumidValue) ==
  outlines := outlines ^ [mk_ (curTime, TempValue, HumidValue)];

public SetTemp: nat ==> ()
SetTemp(t) ==
(envTemp := t;
  HandleEvent(time, envTemp, envHumid);
);

public SetHumid: nat ==> ()
SetHumid(h) ==
(envHumid := h;
  HandleEvent(time, envTemp, envHumid);
);

public ReadTemp: () ==> int
ReadTemp() ==
  return envTemp;

public IncTemp: () ==> ()
IncTemp() ==
(envTemp := envTemp + 1;
  HandleEvent(time, envTemp, envHumid);
);

public DecTemp: () ==> ()
DecTemp() ==
(envTemp := envTemp - 1;
  HandleEvent(time, envTemp, envHumid);
);

public ReadHumid: () ==> nat
ReadHumid() ==
  return envHumid;

public IncHumid: () ==> ()
IncHumid() ==
(envHumid := envHumid + 1;
  HandleEvent(time, envTemp, envHumid);
);

public DecHumid: () ==> ()
DecHumid() ==
(envHumid := envHumid - 1;
  HandleEvent(time, envTemp, envHumid);
);

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

sync

  mutex(IncTemp);
  mutex(DecTemp);
  mutex(SetTemp);
  mutex(ReadTemp, IncTemp, DecTemp, SetTemp);
  mutex(IncHumid);
  mutex(DecHumid);
  mutex(SetHumid);
  mutex(ReadHumid, IncHumid, DecHumid, SetHumid);
  mutex(HandleEvent);
  per IsFinished => finished;

--
-- Thread definition section
--
thread

-- period of thread (period, jitter, delay, offset)
periodic(1000E6,0,0,0) (CreateSignal)

end Environment

quality94%

¤ 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.