Quelle StableController.vdmrt Sprache: VDM

\begin{vdm_al}
class StableController is subclass of IIOSSTYPES

instance variables
private parent: Server;

private sensors: map Sensor to PigStyId := {|->}; --map sensor to grisesti
private actuators: inmap Actuator to PigStyId := {|->}; --map actuator to grisesti

private busy : bool := false;

private pigsInSty : map PigPosition to PigStyId := {|->}; --map pigID to pigsty;

operations
public StableController : Server ==> StableController
StableController(srv) ==
(
  parent := srv;
  return self;
);

-- Add a Pig to pigSty and inform the server
public AddPig: PigId * Sensor * Position ==> ()
AddPig(pigID, sensor, position) ==
(
  dcl pigStyId: PigStyId := sensors(sensor);
  dcl pigPos : PigPosition := mk_PigPosition(pigID,position);
  pigsInSty := pigsInSty munion {pigPos |-> pigStyId};
  parent.AddPig(pigID, self);
)
pre sensor in set dom sensors;

-- Remove a Pig from pigSty and inform the server
public RemovePig: PigId ==> ()
RemovePig(pigID) ==
(
  --dcl pigStyId: PigStyId := sensors(sensor);
  dcl pigPosition : PigPosition := mk_PigPosition(pigID, mk_Position(0,0));
  pigsInSty := {pigPosition} <-: pigsInSty;
  parent.RemovePig(pigID);
  )
  pre exists pp in set dom pigsInSty & pp.id = pigID;

async public PointAtPig: EventId * PigId ==> ()
PointAtPig(eventId, pigId) ==
(
  -- find pig
  let pigPos in set dom pigsInSty be st pigPos.id = pigId in
  (
   -- find pigStyID
   for all pigStyID in set rng pigsInSty do
   (
    if (pigPos.id = pigId) then
    (
     let invActuators = inverse actuators in
     (
      --World`env.handleEvent(1, <SHOW_PIG>, " " ^ [pigId], time);
      invActuators( pigStyID ).SetValues(eventId, pigPos);
      return;
     );
    );
   );
  );
);
--Pre inmap TODO

public AddActuator: Actuator * PigStyId ==> ()
AddActuator(act, sti) ==
(
  actuators := actuators munion {act |-> sti};
)
pre act not in set dom actuators;

public AddSensor: Sensor * PigStyId ==> ()
AddSensor(sens, sti) ==
(
  sensors := sensors munion {sens |-> sti};
)
pre sens not in set dom sensors;

sync
mutex(AddSensor);
mutex(AddActuator);
mutex(RemovePig,AddPig);
mutex(AddPig);
mutex(RemovePig);
--mutex(PointAtPig);

end StableController

\end{vdm_al}

\begin{rtinfo}
[TotalxCoverage]{vdm.tc}[StableController]
\end{rtinfo}

quality85%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.