byte printer = 0;

inline test(i) {
    i == 0 -> i++
}

active [2] proctype usern(){
do
:: 
   if 
   :: test(printer) -> printf("user %d is printing\n", _pid);   
                       printer--
   fi   
od    							
}

active proctype verifier(){
       assert (printer <= 1)
}