Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: HostController.vdmpp   Sprache: VDM

Original von: VDM©

--The HostController Class

-----------------------------------------------
-- Author: Sune Wolff - 20022462
-- Created: 20/4 - 2008
-- Updated:
-- Description:  HostController is the central server
-----------------------------------------------

--
-- class definition
--
class HostController

--
-- instance variables
--
instance variables

private finished : bool := false;
private print  : bool := true;

private TargetTemp : nat;
private Temp  : nat := 0;
private TargetHumid : nat;
private Humid  : nat := 0;

private NodeList : map nat to NetworkTypes`nodeType := { |-> };
private Algo  : algType := <NONE>;

--
-- Types definition section
--
types   

public algType = <THTW> | <TTW> | <TT> | <TW> | <HW> | <NONE>;

--
-- Operations definition section
--
operations

public HostController: nat * nat ==> HostController
 HostController(t, h) ==
  (TargetTemp := t;
  TargetHumid := h;
  );

public UpdateValues: () ==> ()
 UpdateValues() ==
  (for all r in set rng NodeList do
   (if (r = <HUMIDSENSOR>)
   then Humid := HA`HumidNode.ReadValue();
   if (r = <TEMPSENSOR>)
   then Temp := HA`TempNode.ReadValue();
   );
  );

public GetAlgo: () ==> algType
 GetAlgo() ==
  return Algo;

public GetTemp: () ==> nat
 GetTemp() ==
  return Temp;

public GetHumid: () ==> nat
 GetHumid() ==
  return Humid;

public Algorithm: () ==> ()
 Algorithm() ==
  (cases Algo:
   <THTW>  -> THTWAlgo(),
   <TTW>  -> TTWAlgo(),
   <TT>  -> TTAlgo(),
   <TW>  -> TWAlgo(),
   <HW>  -> HWAlgo(),
   <NONE>  -> return
  end
  );

private THTWAlgo: () ==> ()
 THTWAlgo() ==
  (if (Humid > TargetHumid)
  then (HA`WinNode.SetCorrection(<OPEN>);
   HA`ThermNode.SetCorrection(<NONE>);
   print := true;
  )
  elseif (Temp > TargetTemp+1)
  then (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<DEC>);
  print := true;
  )
  elseif (Temp < TargetTemp-1)
  then (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<INC>);
   print := true;
  )
  else (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<NONE>);
   if print
   then (TargetReachedPrint(World`timerRef.GetTime());
    );
   print := false;
   );
  );

private TTWAlgo: () ==> ()
 TTWAlgo() ==
  (if (Temp > TargetTemp + 2)
  then (HA`WinNode.SetCorrection(<OPEN>);
   HA`ThermNode.SetCorrection(<DEC>);
   print := true;
  )
  elseif (Temp > TargetTemp + 1)
  then (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<DEC>);
  print := true;
  )
  elseif (Temp < TargetTemp - 1)
  then (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<INC>);
   print := true;
  )
  else (HA`WinNode.SetCorrection(<CLOSE>);
   HA`ThermNode.SetCorrection(<NONE>);
   if print
   then (TargetReachedPrint(World`timerRef.GetTime());
    );
   print := false;
   );
  );

private TTAlgo: () ==> ()
 TTAlgo() ==
  (if (Temp > TargetTemp + 1)
  then (HA`ThermNode.SetCorrection(<DEC>);
   print := true;
  )
  elseif (Temp < TargetTemp - 1)
  then (HA`ThermNode.SetCorrection(<INC>);
  print := true;
  )
  else (HA`ThermNode.SetCorrection(<NONE>);
   if print
   then (TargetReachedPrint(World`timerRef.GetTime());
    );
   print := false;
   );
  );

private TWAlgo: () ==> ()
 TWAlgo() ==
  (if (Temp > TargetTemp + 1)
  then (HA`WinNode.SetCorrection(<OPEN>);
   print := true;
  )
  else (HA`WinNode.SetCorrection(<CLOSE>);
   if print
   then (TargetReachedPrint(World`timerRef.GetTime());
    );
   print := false;
   );
  );

private HWAlgo: () ==> ()
 HWAlgo() ==
  (if (Humid > TargetHumid)
  then (HA`WinNode.SetCorrection(<OPEN>);
   print := true;
  )
  else (HA`WinNode.SetCorrection(<CLOSE>);
   if print
   then (TargetReachedPrint(World`timerRef.GetTime());
    );
   print := false;
   );
  );

private TargetReachedPrint: nat ==> ()
TargetReachedPrint(t) ==
 (IO`print("\nTarget values reached");
  IO`print("\nAt time: ");
  IO`print(t);  
 );

private UpdateAlgorithm: () ==> ()
 UpdateAlgorithm() ==
  (if (rng NodeList = {})
  then Algo := <NONE>
  elseif (rng NodeList = {<TEMPSENSOR>, <HUMIDSENSOR>, <THERMOSTAT>, <WINDOW>})
  then Algo := <THTW>
  elseif (rng NodeList = {<TEMPSENSOR>, <THERMOSTAT>, <WINDOW>})
  then Algo := <TTW>
  elseif (rng NodeList = {<TEMPSENSOR>, <THERMOSTAT>})
  then Algo := <TT>
  elseif (rng NodeList = {<TEMPSENSOR>, <WINDOW>})
  then Algo := <TW>
  elseif (rng NodeList = {<HUMIDSENSOR>, <WINDOW>})
  then Algo := <HW>
  else Algo := <NONE>;
  );

public AddNode: nat * NetworkTypes`nodeType ==> ()
 AddNode(id, type) ==
  (NodeList := NodeList ++ {id |-> type};
  UpdateAlgorithm();
  )
pre id not in set dom NodeList
post card(dom NodeList) = card(dom NodeList~) + 1;

public RemoveNode: nat * NetworkTypes`nodeType ==> ()
 RemoveNode(id, type) ==
  (if (NodeList(id) = type)
  then NodeList := {id} <-: NodeList;
  UpdateAlgorithm();
  )
pre id in set dom NodeList
post card(dom NodeList) = card(dom NodeList~) - 1;

public Step: () ==> ()
Step() ==
 (HA`TempNode.Step();
  HA`HumidNode.Step();
  UpdateValues();
  Algorithm();
  HA`WinNode.Step();
  HA`ThermNode.Step();
 );

end HostController

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik