--------------------------------------------------------------
-- Übung 23.5.2006 -------------------------------------------
--------------------------------------------------------------
-- Waterlevel-Monitor
--
-- Anforderungen
-- - kontrolliert die Höhe des Wasserspiegels
-- - Pumpe wird dazu ein- und ausgeschaltet
-- - Pumpe an:  der Wasserspiegel steigt um eine Einheit/Zeit-
--              einheit
-- - Pumpe aus: der Wasserspiegel sinkt um zwei Einheiten/
                Zeiteinheit
-- - minimaler Wasserspiegel:  1
-- - maximaler Wasserspiegel: 12
-- - die Pumpe benötigt zwei Zeiteinheiten, um auf ein Signal
-- - zu reagieren
--
-- Initialzustand
-- - Wasserspiegel: 1
-- - Pumpe an
--------------------------------------------------------------

-- Status der Pumpe
datatype status = ON | OFF

-- Signalisiere das Erreichen von min und max
channel min,max
-- erhöhe Wasserspiegel, erniedrige Wasserspiegel, lese Wasserspiegel
channel level_inc, level_dec, level_read  : {1..12}

-- Prozess, um den aktuellen Wasserspiegel zu merken
LEVEL(value) = -- erhöhe Wasserspiegel um 1 (pro Zeiteinheit)
	       level_inc -> LEVEL(value+1)
             []
	       -- erniedrige Wasserspiegel um 2 (pro Zeiteinheit)
	       level_dec -> LEVEL(value-2)
             []
	       -- gib Wasserspiegel aus
               level_read!value -> LEVEL(value)

-- Prozess, um das Erhöhen und Erniedrigen des Wasserspiegels durch die
-- Pumpe zu simulieren
PUMP(status) = -- min wird bald erreicht, Pumpe anschalten
	       min ->
	       PUMP(ON)
              []
	       -- max wird bald erreicht, Pumpe ausschalten
               max ->
	       PUMP(OFF)
              []
	       -- wenn der Status ON ist: 
               -- Level steigt um eine Einheit/Zeiteinheit
               -- WAIT for level_inc, um Nichtdeterminismus bei 
               -- gleichzeitigem max-Event zu vermeiden
	       (status == ON) & WAIT 1;
				level_inc ->
			        PUMP(status)
              []
               -- wenn der Status OFF ist:
               -- Level sinkt um zwei Einheiten/Zeiteinheit
	       -- WAIT for level_dec, um Nichtdeterminismus bei
	       -- gleichzeitigem min-Event zu vermeiden
               (status == OFF) & WAIT 1;
	                         level_dec ->
				 PUMP(status)

-- Prozess, der das Ein-und Ausschalten der Pumpe regelt
PUMPEN = level_read?x ->           -- lese Level
         if(x == 5) then           -- wenn 5, signalisiere min
	   WAIT 2;                 -- um Pumpe auszuschalten
	   min ->                  -- zwei Zeiteinheiten Verzögerung
	   PUMPEN;
         else if(x == 10) then     -- wenn 10, signalisiere max
           WAIT 2;                 -- um Pumpe anzuschalten
	   max ->                  -- zwei Zeiteinheiten Verzögerung
           PUMPEN;
         else
           WAIT 1;	           -- Achtung: bei synchronisierten Prozessen
           PUMPEN                  -- kann nur Zeit verstreichen, wenn in
                                   -- allen Teilprozessen Zeit vergeht, 
                                   -- darum muss auch hier ein WAIT eingebaut
                                   -- werden, um zu verhindern, dass sofort
                                   -- wieder level_read ausgeführt wird!

-- alle Prozesse synchronisieren
SYSTEM = (PUMPEN
        [| {| min, max |}
         PUMP(ON))
        [| {| level_dec, level_inc, level_read |} |]
	 LEVEL(1)