// maximum expected operations for one test and set operation is less than 10 filter(forall, t=1 => R{"process0"}<=10 [ F t=1 & (l0=8 | l0=9) ]) filter(forall, t=1 => R{"process1"}<=10 [ F t=1 & (l1=8 | l1=9) ]) // display actual values for process 0 (once test starts) R{"process0"}max=? [ F t=1 & (l0=8 | l0=9) {t=1} ]