-- Zeilenkommentar

MODULE floor ( lvl, el )
VAR
   ebut  :  boolean;
   fbut  :  { on, blink, off };
ASSIGN
   init(ebut)  := 0;
   init(fbut)  := off;
   next(ebut)  := case
      el.door = closed & next(el.door) = open & el.pos = lvl : 0;
      !ebut                                                  : {0,1};
      1                                                      : ebut;
   esac;
   next(fbut)  := case
--      fbut = off &  next(el.moving)                          : { blink, off };
--      fbut = off & !next(el.moving)                          : { on, off };
      fbut = off &  el.moving                                 : { blink, off };
      fbut = off & !el.moving                                 : { on, off };
      el.door = closed & next(el.door) = open & el.pos = lvl : off;
--      fbut = blink & !next(el.moving)                        : on;
--      fbut = on    &  next(el.moving)                        : blink;
      1                                                      : fbut;
   esac;
DEFINE
   request  := ebut | !( fbut = off );

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

MODULE elevator ( S1req, S2req, S3req )
VAR
   noSensorTime   :  { 0, 1, 2 };
   doorClosedTime :  { 0, 1 };
   pos            :  { S1, S2, S3, S12, S23 };
   door           :  { open, closed };
   dir            :  { up, down };
   moving         :  boolean;
   sensor         :  boolean;
ASSIGN
   init(pos)      := S1;
   init(door)     := closed;
   init(dir)      := up;
   init(moving)   := 0;
   init(sensor)   := 0;
   next(dir) := case
      pos = S1 & next(pos) = S12 : up;
      pos = S2 & next(pos) = S23 : up;
      pos = S2 & next(pos) = S12 : down;
      pos = S3 & next(pos) = S23 : down;
      1                          : dir;
   esac;
   next(moving) := !( pos = next(pos) );
   next(sensor) := case
      door = open & next(door) = open : {0,1}; -- Tuere schliesst nicht
      1                               : 0;
   esac;
   next(pos) := case
      pos = S12 & dir = up              : S2; -- Bewegung fortsetzen
      pos = S12 & dir = down            : S1;
      pos = S23 & dir = up              : S3;
      pos = S23 & dir = down            : S2;
      door = open | doorClosedTime = 0
                  | next(door) = open   : pos;
      -- ab hier gilt ( door = closed & doorClosedTime = 1 & next(door)=closed)
      !S1req & !S2req & !S3req          : pos;
      -- ab hier muss ein Request vorliegen
      pos = S1 & S1req                 : pos;
      pos = S2 & S2req                 : pos;
      pos = S3 & S3req                 : pos;
      -- ab hier wird der FS nicht mehr auf dem aktuellen SW benoetigt
      pos = S2 & dir = up   & S3req    : S23;
      pos = S2 & dir = down & S1req    : S12;
      pos = S2 & S1req                 : S12;
      pos = S2 & S3req                 : S23;
      pos = S1                         : S12; 
      pos = S3                         : S23;
      1                                : pos;
   esac;
   next(noSensorTime) := case
      door = open & !sensor & noSensorTime = 0 : 1;
      door = open & !sensor & noSensorTime = 1 : 2;
      1                                        : 0;
   esac;
   next(door) := case
      door = closed & !moving & ( pos = S1 & S1req 
                                | pos = S2 & S2req 
                                | pos = S3 & S3req ) : open;
      door = open & noSensorTime = 2 & !sensor       : closed;
      1                                              : door;
   esac;
   next(doorClosedTime) := case
      door = closed  : 1;
      1              : 0;
   esac;
-------------------------------------------------------------------------------

MODULE main
VAR
   s1 : floor( S1, el );
   s2 : floor( S2, el );
   s3 : floor( S3, el );
   el : elevator( s1.request, s2.request, s3.request );

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

FAIRNESS !s1.request -- schliesst ALLE Pfade aus, also auch, dass einmal der Knopf gedr"uckt wird, der Fahrstuhl aber nie S1 erreicht !!!
FAIRNESS !s2.request
FAIRNESS !s3.request
FAIRNESS ( !el.sensor & AX !el.sensor )

SPEC
   EF EG s1.request

SPEC
     AG( !( s1.fbut = off ) -> A[ ( !( s1.fbut = off ) ) U ( ( el.pos = S1 ) & ( el.door = open ) ) ] )
   & AG( !( s2.fbut = off ) -> A[ ( !( s2.fbut = off ) ) U ( ( el.pos = S2 ) & ( el.door = open ) ) ] )   
   & AG( !( s3.fbut = off ) -> A[ ( !( s3.fbut = off ) ) U ( ( el.pos = S3 ) & ( el.door = open ) ) ] )

--SPEC
--   AG( (!( s1.fbut = off )) -> (s1.fbut = blink <-> el.moving) 
--     & (!( s2.fbut = off )) -> (s2.fbut = blink <-> el.moving)
--     & (!( s3.fbut = off )) -> (s3.fbut = blink <-> el.moving)
--     )

--SPEC
--   AG( el.door = open -> AX( el.door = closed -> AX( !el.moving ) ) )

--SPEC
--   AG( el.door = closed -> AX( el.door = open -> AX( el.door = open & AX( el.door = open ) ) ) )

--SPEC
--     AG( s1.request -> AF( el.pos = S1 ) )
--   & AG( s2.request -> AF( el.pos = S2 ) )
--   & AG( s3.request -> AF( el.pos = S3 ) )