model/schedule: comput "reduadant" measurement, print along with traces

This will help debuggability. For instance, it will be more obvious that
right now, the 'deadlock.c' test is completing executions as "redundant"
when in fact they should be deadlocks.