module mainframe is

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

type RATE is
   -- either numeric values
   RATE (R: real),    -- where R > 0.0
   -- or symbolic values for parameters that may take different values
   BETA, DELTA2, MU2
end type

type PHASE is
   1, -- low load
   2, -- high load
   3  -- idle
end type

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

channel DELAY is
   (R: RATE)
end channel

channel SIZE is
   (N: nat)
end channel

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

process MAIN [C, FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, PROG_JOB_READY,
              REPAIR, USER_JOB, USER_JOB_READY: DELAY,
              Z_AVAIL: none, Z_PROG_QUEUE, Z_USER_QUEUE: SIZE] 
             (ALPHA, BETA, DELTA1, DELTA2, LAMBDA1, LAMBDA2, MU1, MU2,
              NU, PHI, XI: RATE, INIT_PHASE: PHASE, PROG_SIZE, USER_SIZE: nat) is
   par FAIL, PROG_JOB, USER_JOB in
      LOADS [C, FAIL, PROG_JOB, USER_JOB]
            (DELTA1, DELTA2, LAMBDA1, LAMBDA2, MU1, MU2, PHI, INIT_PHASE)
   ||
      MACHINE [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, PROG_JOB_READY,
               REPAIR, USER_JOB, USER_JOB_READY, Z_AVAIL, Z_PROG_QUEUE, Z_USER_QUEUE]
              (ALPHA, BETA, NU, XI, PROG_SIZE, USER_SIZE)
   end par
end process

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

process LOADS [C, FAIL, PROG_JOB, USER_JOB: DELAY]
              (DELTA1, DELTA2, LAMBDA1, LAMBDA2, MU1, MU2, PHI: RATE,
               INIT_PHASE: PHASE) is
   par C in
       -- FailLoad
      LOAD [C, FAIL] (DELTA1, DELTA2, PHI, INIT_PHASE)
   ||
      -- ProgLoad
      LOAD [C, PROG_JOB] (LAMBDA1, LAMBDA2, PHI, INIT_PHASE)
   ||
      -- UserLoad
      LOAD [C, USER_JOB] (MU1, MU2, PHI, INIT_PHASE)
   end par
end process

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

process LOAD [C, JOB: DELAY] (R1, R2, PHI: RATE, in var P: PHASE) is
   loop
      case P in
         1 -> 
            -- low-load phase
            loop PHASE1 in
               alt
                  JOB (R1)
               []
                  C (PHI);
                  break PHASE1
               end alt
            end loop;
            P := 2
      |  2 -> 
            -- high-load phase
            loop PHASE2 in
               alt
                  JOB (R2)
               []
                  C (PHI);
                  break PHASE2
               end alt
            end loop;
            P := 3
      |  3 ->
            -- idle phase
            C (PHI);
            P := 1
      end case
   end loop
end process

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

process MACHINE [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, PROG_JOB_READY,
        REPAIR, USER_JOB, USER_JOB_READY: DELAY, Z_AVAIL: none, 
        Z_PROG_QUEUE, Z_USER_QUEUE: SIZE] (ALPHA, BETA, NU, XI: RATE,
        PROG_SIZE, USER_SIZE: nat) is
   par FAIL, GET_PROG_JOB, GET_USER_JOB, REPAIR in
      QUEUES [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, REPAIR, USER_JOB,
              Z_AVAIL, Z_PROG_QUEUE, Z_USER_QUEUE] (ALPHA, BETA, PROG_SIZE, USER_SIZE)
   ||
      par FAIL, REPAIR in
         PROCESSOR [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB_READY,
                    REPAIR, USER_JOB_READY] (NU, XI)
      ||
         PROCESSOR [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB_READY,
                    REPAIR, USER_JOB_READY] (NU, XI)
      ||
         PROCESSOR [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB_READY,
                    REPAIR, USER_JOB_READY] (NU, XI)
      ||
         PROCESSOR [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB_READY,
                    REPAIR, USER_JOB_READY] (NU, XI)
      end par
   end par
end process

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

process QUEUES [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, REPAIR,
                USER_JOB: DELAY, Z_AVAIL: none,
                Z_PROG_QUEUE, Z_USER_QUEUE: SIZE]
               (ALPHA, BETA: RATE, PROG_SIZE, USER_SIZE: nat) is
   par GET_PROG_JOB, GET_USER_JOB, PROG_JOB, USER_JOB in
      FAIL_QUEUE [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, REPAIR,
                  USER_JOB, Z_AVAIL] (BETA)
   ||
      par GET_PROG_JOB in
         PROG_JOB_QUEUE [GET_PROG_JOB, PROG_JOB, Z_PROG_QUEUE] (ALPHA, PROG_SIZE)
      ||
         USER_JOB_QUEUE [GET_PROG_JOB, GET_USER_JOB, USER_JOB, Z_USER_QUEUE]
                        (ALPHA, USER_SIZE)
      end par
   end par
end process

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

process FAIL_QUEUE [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB, REPAIR,
                    USER_JOB: DELAY, Z_AVAIL: none] (BETA: RATE) is
   -- see F0 and F1 page 13 of the paper
   loop
      alt
         Z_AVAIL
      []
         FAIL (?any RATE);
         REPAIR (BETA)
      []
         GET_USER_JOB (?any RATE)
      []
         GET_PROG_JOB (?any RATE)
      []
         USER_JOB (?any RATE)
      []
         PROG_JOB (?any RATE)
      end alt
   end loop
end process

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

process PROG_JOB_QUEUE [GET_PROG_JOB, PROG_JOB: DELAY, Z_PROG_QUEUE: SIZE]
                       (ALPHA: RATE, L: nat) is
   -- see Q0...Ql page 13 of the paper
   var I: nat in
      I := 0;
      loop
         alt
            Z_PROG_QUEUE (I)
         []
            only if I < L then
               PROG_JOB (?any RATE);
               I := I + 1
            end if
         []
            only if I > 0 then
               GET_PROG_JOB (ALPHA);
               I := I - 1
            end if
         end alt
      end loop
   end var
end process

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

process USER_JOB_QUEUE [GET_PROG_JOB, GET_USER_JOB, USER_JOB: DELAY,
                        Z_USER_QUEUE: SIZE] (ALPHA: RATE, L: nat) is
   -- see R0...Rl page 13 of the paper
   var I: nat in
      I := 0;
      loop
         alt
            Z_USER_QUEUE (I)
         []
            only if I == 0 then
               GET_PROG_JOB (?any RATE)
            end if
         []
            only if I < L then
               USER_JOB (?any RATE);
               I := I + 1
            end if
         []
            only if I > 0 then
               GET_USER_JOB (ALPHA);
               I := I - 1
            end if
         end alt
      end loop
   end var
end process

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

process PROCESSOR [FAIL, GET_PROG_JOB, GET_USER_JOB, PROG_JOB_READY, REPAIR, 
                   USER_JOB_READY: DELAY] (NU, XI: RATE) is
   loop
      alt
         GET_USER_JOB (?any RATE);
         alt
            USER_JOB_READY (NU)
         []
            FAILURE [FAIL, REPAIR]
         end alt
      []
         GET_PROG_JOB (?any RATE);
         alt
            PROG_JOB_READY (XI)
            -- here, bug in the original paper! (was: USER_JOB_READY instead
            -- of PROG_JOB_READY) 
         []
            FAILURE [FAIL, REPAIR]
         end alt
      []
         FAILURE [FAIL, REPAIR]
      end alt
   end loop
end process

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

process FAILURE [FAIL, REPAIR: DELAY] is
   FAIL (?any RATE);
   REPAIR (?any RATE)
end process

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

end module