Steuerung des Wasserspiegels in einem Tank

-- Kontroller der Höhe des Wasserspiegels
-- Pumpe wird entsprechend ein- und ausgeschaltet
-- Wenn die Pumpe aus ist, fällt der Wasserspiegel um
   2 Einheiten / Zeiteinheit.
-- Wenn die Pumpe an ist, steigt der Wasserspiegel um
   1 Einheit / Zeiteinheit
-- Der Wasserspiegel muss zwischen 1 und 12 liegen. 
-- Zwischen den Signalen und dem Ein/Ausschalten der
   Pumpe liegen immer zwei Zeiteinheiten.

Initialzustand

-- Am Anfang ist der Wasserspiegel 1.
-- Die Pumpe ist demnach an. 

Spezifikation

channel sig_max, sig_min
channel aus, an
channel lese_level, schreibe_level : {1..12}

-- Lesen und Schreiben des Wasserspiegels
VAR(value) = lese_level!value -> VAR(value)
            []
             schreibe_level?newValue -> VAR(newValue)

VARPROCESS = VAR(1)

-- Prozess für den Sensor
SENSOR = SENSOR_WAIT_MAX;
         SENSOR_WAIT_MIN;
	 SENSOR
         
SENSOR_WAIT_MAX = lese_level?x ->
                  if(x == 10) then
                    WAIT 2; sig_max -> SKIP
                  else WAIT 1; SENSOR_WAIT_MAX

SENSOR_WAIT_MIN = lese_level?x ->
                  if(x == 6) then
                    WAIT 2; sig_min -> SKIP
		  else WAIT 1; SENSOR_WAIT_MIN

-- Prozess für den Controller
CONTROLLER = sig_max -> 
	     aus ->
	     sig_min ->
	     an ->
	     CONTROLLER

-- Prozess für die Pumpe
PUMPE = FUELLEN

FUELLEN = aus -> LEEREN
         []
	  WAIT 0.5;
          lese_level?x ->
          schreibe_level.(x + 1) ->
	  WAIT 0.5;
	  FUELLEN

LEEREN = an -> FUELLEN
       []
         WAIT 0.5;
         lese_level?x ->
         schreibe_level.(x - 2) -> 
	 WAIT 0.5;
	 LEEREN

WASSERTANK = ((PUMPE ||| SENSOR)
            [| {| lese_level, schreibe_level |} |]
              VARPROCESS)
	    [| {an, aus, sig_max, sig_min} |]
              CONTROLLER