---------------------------------------------------------------------
-- Fischer's Protocol, Übung am 30.5.2006 
---------------------------------------------------------------------
-- wechselseitiger Ausschluss für Zugriff auf kritische Region 
-- N Prozesse, Prozess 1: pid = 1, Prozess 2: pid = 2, ...
-- atomares read/write, benötigt a Zeiteinheiten
-- gemeinsame Variable k, initialisiert mit 0
-- Wartezeit b > a für zwei Prozesse
---------------------------------------------------------------------
-- void process(int i)
-- {
--   while(1)
--   {
--     do
--     {
--       waitfor(k == 0);        //warte auf k == 0
--       k = i;                  //k auf pid setzen, a Zeiteinheiten 
--       wait(b);                //b > a
--     } while(k != i)		 //wenn k nicht pid, dann von vorn
--     //critical section
--     k = 0;                    //a Zeiteinheiten
--   }
-- }
----------------------------------------------------------------------

-- channel zum Lesen und Schreiben der shared variable k
channel read_k, write_k : {0..2}
-- Anzeigen der kritischen Region
channel critical_section : {1..2}

-- Prozess, um den Wert von k zu lesen und zu schreiben
-- verbraucht jeweils a Zeiteinheiten
K(value) = read_k!value -> WAIT a; K(value)
          []
	   write_k?newX -> WAIT a; K(newX)
	   
-- ein Prozess mit pid i
PROCESS(i) = read_k?k ->                -- k lesen
             if(k == 0) then            -- wenn k == 0, weitermachen
	       write_k!i ->             -- k auf pid setzen            
	       WAIT b;                  -- b Zeiteinheiten warten 
	       read_k?k2 ->             -- erneut lesen
	       if(k2 == i) then         -- wurde k überschrieben?
	         critical_section!i ->  -- nein, dann kritische Region
		 write_k!0 ->           -- nach kritischem Abschnitt k=0
		 PROCESS(i)             -- um anderen Prozessen Eintritt
                                        -- in die kritische Region zu 
					-- gewähren
	       else                     -- k überschrieben, weiter warten,
	         PROCESS(i)		-- bis Prozess i dran ist
	      else                      -- wenn k != 0, weiter auf k==0
	         PROCESS(i)             -- warten

-- zwei Prozesse, pids 1 und 2
PROCESSES = PROCESS(1) ||| PROCESS(2)

-- System besteht aus den beiden Prozessen, synchronisiert mit dem
-- Variablenprozess
SYS = PROCESSES
     [| {| write_k, read_k |} |]
      K(0)