#define N 4 /* number of cores */
#define M 2 /* number of FPUs */
#define any M

/* Message types used by the protocol. Do not change. */
mtype = {req_fpu, grant_fpu, free_fpu};

/* Message channels used by the protocol. Do not change. */
chan from_core[N] = [1] of { mtype, byte };
chan to_core[N] = [1] of { mtype, byte };

/* A process modelling the FPU use of a core. Do not change. */
proctype core(byte id) {
    byte my_fpu = M;
    do
        :: from_core[id] ! req_fpu, any;
           to_core[id] ? grant_fpu, my_fpu;
           atomic {
               printf("MSC: Core %d using FPU %d\n", id, my_fpu);
               from_core[id] ! free_fpu, my_fpu;
               my_fpu = M
           }
    od
}

active proctype fpu_controller() {
    /* Add your Promela model of the FPU controller here. */
        
    /* Following line added to make a syntactically valid Promela model */
    /* Remove it first. */
    skip
}

/* The init process for starting all other processes. */

init {
    int id;
    atomic {
        id = 0;
        do
            :: (id < N) -> run core(id); id++
            :: (id == N) -> break
        od;
        id = 0
    }
}