module PROB (TYPES, CHANNELS, CONSTANTS) is

process ALT [PROB: PROB] (ID: PID, S: STEP, P0: PROB, P1: PROB) is
   alt
      PROB (ID, S, P0)
   []
      PROB (ID, S, P1)
   end alt
end process

process MAIN [PROB: PROB] (S: STEP) is
   var P0: PROB, P1: PROB, VOID: BOOL in
      VOID := false;
      case S in
         3 ->
            P0 := PH;
            P1 := 1_PH
      |  4 | 5 | 6 ->
            P0 := PV;
            P1 := 1_PV
      |  7 ->
            P0 := PF;
            P1 := 1_PF;
            if H = N and Q >= T then
               VOID := true
            end if
      end case;
      if VOID then
         stop
      else
         loop
            par
               ALT [...] (1 of PID, S, P0, P1)
            ||
               ALT [...] (2 of PID, S, P0, P1)
            ||
               ALT [...] (3 of PID, S, P0, P1)
            ||
               ALT [...] (4 of PID, S, P0, P1)
            end par
         end loop
      end if
   end var
end process

end module