Process Rosa{
    int nbomb = 0;
    bool vaiMario = true;
    signal s;
    process p;
    port signal friggi_i;
    port signal friggi_f;
    port signal servi_i;
    port signal servi_f;
    port signal segnalaMario;

    do
        * vaiMario == true; p = receive(s) from friggi_i; ->
              vaiMario = false;
              send(nbomb) to p.ok;

        * ; p = receive(s) from friggi_f; ->
              nbomb = 30;

        * nbomb > 0 and !vaiMario; p = receive(s) from servi_i; ->
              send(s) to p.ok;

        * ; p = receive(s) from servi_f; ->
              nbomb--;
              send(nbomb) to p.rimasti;

        * ; p = receive(s) from segnalaMario; ->
            vaiMario = true;

    od
}

Process Clock{
    int now = 0;
    int alarm = -1;
    signal s;
    process p;

    do
        * ; p = receive(s) from tick; ->
          now++;
          if(now >= alarm and alarm != -1){
            alarm = -1;
            send(s) to Rosa.segnalaMario;
          }

        * ; p = receive(n) from set_timer; ->
            if(n == 0){
                alarm = -1;
                send(s) to Rosa.segnalaMario;
            } else {
              alarm = now + n;
            }

    od
}

Process Mario{
    int nbomb = 0;
    signal s;
    port int ok;
    while(true){
        send(s) to Rosa.friggi_i;
        p = receive(nbomb) from ok;
        if(nbomb > 0){
            < butta >
        }
        < friggi >
        Clock.set_timer(60 minuti);
        send(s) to Rosa.friggi_f;
   }
}

Process Piero{
    int nbomb = 0;
    signal s;
    port int rimasti;
    port signal ok;
    process p;
    process cliente;

    while(true){
        client = receive(s) from nuovo_cliente;
        send(s) to Rosa.servi_i;
        p = receive(s) from ok;
        < servi cliente >
        send(s) to cliente.rilascio;
        send(s) to Rosa.servi_f;
        p = receive(nbomb) from rimasti;
        if(rimasti == 0){
            Clock.set_timer(0);
        }
    }
}

Process Cliente{
    signal s;
    port signal rilascio;
    process p;
    send(s) to Piero.nuovo_cliente;
    p = receive(s) from rilascio;
    < mangia >
    < esci >
}

Process HWClock{
    signal s;
    while(true){
        < hw tick >
        send(s) to Clock.tick;
    }
}