Bahnübergang:

- Zug darf den Bahnübergang nur überqueren, wenn die 
  Schranken geschlossen sind

- Anfangszustand: Schranke oben (90 Grad)
- Schranken schließen: 10 Grad pro 10 Zeiteinheiten
- Schranken öffnen: 10 Grad pro 10 Zeiteinheiten

- Schranke muss immer vollständig geschlossen sein, wenn sich
  ein Zug nähert, aber nicht immer vollständig geöffnet:
  nähert sich ein zweiter Zug, wird die Schranke wieder 
  geschlossen, obwohl sie noch nicht vollständig geöffnet war

- falls die Schranke noch nicht vollständig geöffnet war, 
  bevor der nächste Schließvorgang beginnt, werden 10 Grad 
  zur aktuellen Position addiert (Sicherheitsbedingung)


Unser Rundkurs:

|------------------------------------------------------------|

Zug
                                     sig        nah da weg sig
|-------------------------------------|----------|---|---|---|
             [500, 600]                   100      10  10  10

------------------------------------------------------------------------------
-- Spezifikation mit Timed CSP
------------------------------------------------------------------------------

-- Events für den Zug
channel sig_nah, sig_weg, nah, da, weg

-- Events für die Schranke
channel auf, zu

-- Variable position, kann gelesen und beschrieben werden
channel lese_position, schreibe_position

------------------------------------------------------------------------------
-- Prozess für die Variable
------------------------------------------------------------------------------

-- entweder lesen oder schreiben
VAR(value) = lese_position!value -> VAR(value)
            []
             schreibe_position?newValue -> VAR(newValue)

-- am Anfang ist die Position 90 Grad
VAR_PROCESS = VAR(90)

------------------------------------------------------------------------------
-- Prozess für den Zug
------------------------------------------------------------------------------

ZUG = Wait 500;                     -- 500 Zeiteinheiten warten
      (|~| d : {0..100} @ Wait d);  -- internal choice: nichtdeterministisch
                                    -- zwischen 0 und 100 Zeiteinheiten warten
      sig_nah ->                    -- hallo, Zug kommt
      Wait 100;                     
      nah ->                        -- kurz vom Bahnübergang
      Wait 10;
      da ->                         -- am Bahnübergang
      Wait 10;
      weg ->                        -- kurz nach dem Bahnübergang
      Wait 10;
      sig_weg ->                    -- hallo, wir sind weg
      ZUG                           -- und wieder von vorn

------------------------------------------------------------------------------
-- Prozess für den Controller
------------------------------------------------------------------------------

CONTROLLER = sig_nah ->	            -- Signal nah kommt
             zu ->                  -- dann Schranken schließen
             sig_weg ->             -- Signal weg kommt
	     auf ->                 -- dann Schranken öffnen
             CONTROLLER

------------------------------------------------------------------------------
-- Prozess für den Bahnübergang
------------------------------------------------------------------------------

BAHNUEBERGANG = HEBEN               -- der Anfang

SENKEN = lese_position?pos ->                           -- aktuelle Position
         (pos == 0) & auf -> HEBEN                      -- wenn 0, auf auf-
                                                        -- Signal warten und
                                                        -- in den Hebeprozess
                                                        -- übergehen
        []
         (pos > 0)  & Wait 10;                          -- wenn noch nicht 
                                                        -- unten, weiter 
                      schreibe_position.(pos - 10) ->   -- senken, Position
                      SENKEN                            -- neu setzen

HEBEN = lese_position?pos ->                            -- aktuelle Position
         (pos == 90) & zu -> SENKEN                     -- wenn 90 Grad, auf
                                                        -- zu-Signal warten,
                                                        -- in den Senkprozess
                                                        -- übergehen
        []
         (pos < 90)  & Wait 10;                         -- wenn weniger als 90
                       schreibe_position.(pos + 10) ->  -- weiter heben, neue
                       HEBEN                            -- Position setzen
        []
         zu ->                                          -- zu-Signal kommt
	 schreibe_position.(pos + 10) ->                -- Position schreiben
	 SENKEN                                         -- wegen Sicherheits-
                                                        -- bedingung, in den
                                                        -- Senkprozess über-
                                                        -- gehen

------------------------------------------------------------------------------
-- Gesamtsystem aus Variablenprozess, Zug, Bahnübergang und Controller
------------------------------------------------------------------------------

-- Variablenprozess synchronisiert sich über alle schreibe_position- und 
-- lese_position-Events mit dem Bahnübergang

-- Zug synchronisiert sich über sig_nah- und sig_weg-Events mit dem 
-- Controller (bzw. dem Prozess, in dem der Controller läuft)

-- Bahnübergang synchronisiert sich über alle auf- und zu-Events mit dem 
-- Controller (bzw. dem Prozess, in dem der Controller läuft)

SYSTEM = ((VAR_PROCESS                                 
          [| {| schreibe_position, lese_position |} |]
          BAHNUEBERGANG)
          [| {auf, zu} |]
          CONTROLLER)
          [| {sig_nah, sig_weg} |]
          ZUG

------------------------------------------------------------------------------