-- from john
-- I modified WorkLock to be a task, and not a protected type
-- list unmodeled
-- inlined

  ----------------------------------------------------------------------
type ZERO_POS is (zero, positive);

  task ResultLock is
    entry signal;
    entry wait;
  end ResultLock;

  ----------------------------------------------------------------------
  task ASActivePool is
--    entry ASinit;
    entry StartUp;
    entry ShutDown;
    entry Get(done : out Boolean);
    entry Put;     --newWork : in out WorkList);
    entry Finished;
    entry Execute;
    entry Complete;
  end ASActivePool;

  ----------------------------------------------------------------------
  task AS1ActiveWorker is
    entry StartUp;
    entry ShutDown;
    entry Execute;
  end AS1ActiveWorker;

  task AS2ActiveWorker is
    entry StartUp;
    entry ShutDown;
    entry Execute;
  end AS2ActiveWorker;

  task AS3ActiveWorker is
    entry StartUp;
    entry ShutDown;
    entry Execute;
  end AS3ActiveWorker;

  task main;
  ----------------------------------------------------------------------
  task body ResultLock is
        value : Boolean := TRUE;
  begin
   loop
     select
       when not value => accept signal;
       value := TRUE;
     or
       when value => accept wait;
       value := FALSE;
     end select;
   end loop;

  end ResultLock;

  task body ASActivePool is
    executeDone : Boolean := TRUE;
    waitPhaseWorkers, idleWorkers : range 0 ..3;
    -- workCount : Natural;
    workCount : ZERO_POS;

    -- choice: Boolean; -- added by me

  begin

    -- accept ASinit;

    accept StartUp;

    workCount := zero;

    Outer: loop

      loop
        select accept ShutDown;
           exit Outer;
        or accept Finished;
           accept Shutdown;
           exit Outer;
        or accept Put do

	    -- nondeterministic choice
	    --choice:=...;
	      if ... then	
              	workCount := positive;
	      end if;

          end Put;
        or accept Execute;
          AS1ActiveWorker.Execute;
          AS2ActiveWorker.Execute;
          AS3ActiveWorker.Execute;
          exit;
        end select;
      end loop;


      executeDone := FALSE;
      idleWorkers := 3;
      waitPhaseWorkers := 0;

      loop
        select
          when (workCount = positive) or executeDone =>
               accept Get(done : out Boolean) do 
            if executeDone then
              done := TRUE;
              waitPhaseWorkers := waitPhaseWorkers + 1;

            else
              done := FALSE;

            -- nondeterministic choice
		-- choice:=...;
              if ... then
                workCount := positive;
	      else
		workCount := zero;
	      end if;	

              idleWorkers := idleWorkers - 1;
            end if;
          end Get;

        or accept Put do
	    -- nondeterministic choice
		--choice:=...;
	      if ... then            
                workCount := positive;
              end if;
          end Put;
          idleWorkers := idleWorkers + 1;

        or accept Finished;
          executeDone := TRUE;
          waitPhaseWorkers := waitPhaseWorkers + 1;
        end select;

        if idleWorkers = 3 and workCount=zero then
          executeDone := TRUE;
        end if;

        exit when waitPhaseWorkers = 3;
      end loop;

        accept Complete;


    end loop Outer;

  end ASActivePool;
  ----------------------------------------------------------------------

  task body AS1ActiveWorker is
    done : Boolean;
    choice_m : range 1 .. 6 :=6;

  begin
    accept StartUp;
    loop
      select accept ShutDown;
         exit;
      or accept Execute;
      end select;

      -- Repeatedly get work, process it, put new work
      loop
        -- Attempt to get new work
        ASActivePool.Get(done); 

        exit when done;

        -- Perform the work

	internal "calldoWork";
	loop
        -- nondeterministic choice
		choice_m:=...;	
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;

                  -- AS1ActiveWorker.Startup; error
                  AS2ActiveWorker.Startup;
                  AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  -- AS1ActiveWorker.ShutDown; error
                  AS2ActiveWorker.ShutDown;
                  AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
        -- nondeterministic choice for done
	done := ...;
	internal "returndoWork";

        -- Short-circuit the computation if indicated
        if done then
          ASActivePool.Finished;
          exit;
        end if;

        -- Process the results

            ResultLock.wait;
	  internal "calldoResult";
	  loop
		choice_m:=...;
        -- nondeterministic choice
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  -- AS1ActiveWorker.Startup; error
                  AS2ActiveWorker.Startup;
                  AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  -- AS1ActiveWorker.ShutDown; error
                  AS2ActiveWorker.ShutDown;
                  AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
	-- nondet choice for done
	done := ...;
	internal "returndoResult";
	
            ResultLock.signal;

          -- Short-circuit the computation if indicated
          if done then
            ASActivePool.Finished;
            exit;
          end if;

        -- Put the new work back
        ASActivePool.Put;

      end loop;

    end loop;

  end AS1ActiveWorker;
  ----------------------------------------------------------------------
  task body AS2ActiveWorker is
    done : Boolean;
    choice_m :  range 1 .. 6:=6;

  begin

    accept StartUp;
    loop

      select accept ShutDown;
         exit;
      or accept Execute;
      end select;


      -- Repeatedly get work, process it, put new work
      loop
        -- Attempt to get new work
        ASActivePool.Get(done);

        exit when done;

        
	internal "calldoWork";
	loop
        -- nondeterministic choice
	choice_m:=...;
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  AS1ActiveWorker.Startup;
                  --AS2ActiveWorker.Startup;
                  AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  AS1ActiveWorker.ShutDown;
                  --AS2ActiveWorker.ShutDown;
                  AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
	done:=...;
	internal "returndoWork";

        -- Short-circuit the computation if indicated
        if done then
          ASActivePool.Finished;
          exit;
        end if;

        -- Process the results
            ResultLock.wait;
	internal "calldoResult";
	loop
	choice_m:=...;
        -- nondeterministic choice
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  AS1ActiveWorker.Startup;
                  --AS2ActiveWorker.Startup;
                  AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  AS1ActiveWorker.ShutDown;
                  --AS2ActiveWorker.ShutDown;
                  AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
	done:=...;
	internal "returndoResult";
	--end doresult
            ResultLock.signal;

          if done then
            ASActivePool.Finished;
            exit;
          end if;

        -- Put the new work back
        ASActivePool.Put;
      end loop;
    end loop;

  end AS2ActiveWorker;
  ----------------------------------------------------------------------
  task body AS3ActiveWorker is
    done : Boolean;
    choice_m :  range 1 .. 6 :=6;

  begin
    accept StartUp;
    loop

      select accept ShutDown;
         exit;
      or accept Execute;
      end select;


      -- Repeatedly get work, process it, put new work
      loop
        -- Attempt to get new work
        ASActivePool.Get(done);

        exit when done;

        -- Perform the work
	internal "calldoWork";
	loop
	choice_m:=...;
        -- nondeterministic choice
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  AS1ActiveWorker.Startup;
                  AS2ActiveWorker.Startup;
                  --AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  AS1ActiveWorker.ShutDown;
                  AS2ActiveWorker.ShutDown;
                  --AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
	done:=...;
	internal "returndoWork";
	--end work

        if done then
          ASActivePool.Finished;
          exit;
        end if;

        -- Process the results
            ResultLock.wait;
	internal "calldoResult";
	loop
	choice_m:=...;
        -- nondeterministic choice
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  AS1ActiveWorker.Startup;
                  AS2ActiveWorker.Startup;
                  --AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  AS1ActiveWorker.ShutDown;
                  AS2ActiveWorker.ShutDown;
                  --AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
	done:=...;
	internal "returndoResult";
	-- end result

            ResultLock.signal;

          -- Short-circuit the computation if indicated
          if done then
            ASActivePool.Finished;
            exit;
          end if;

        -- Put the new work back
        ASActivePool.Put;

      end loop;

    end loop;

  end AS3ActiveWorker;
  ----------------------------------------------------------------------

-- we add here the stub

  task body main is
   choice_m :  range 1 .. 6:=6;

   begin
        loop
        -- nondeterministic choice
	 choice_m:=...;
         case choice_m is
          when 1 => -- Create;
                  ASActivePool.StartUp;


                  AS1ActiveWorker.Startup;
                  AS2ActiveWorker.Startup;
                  AS3ActiveWorker.Startup;
 
          when 2 => -- Input;
                  ASActivePool.Put;
          when 3 => -- Execute;
                  ASActivePool.Execute;
                  ASActivePool.Complete;
          when 4 => -- Destroy;
                  ASActivePool.Finished;

                  AS1ActiveWorker.ShutDown;
                  AS2ActiveWorker.ShutDown;
                  AS3ActiveWorker.ShutDown;

                  ASActivePool.ShutDown;
          when 5 => null;
          when 6 => exit;
         end case;
        end loop;
	choice_m:=6; -- reset
   end main;