In reply to rkp:
vld must occur at least 10 (or 2 in your model) times between req and ack.
// v is initialized to a max count; let count==2 as an example
(vld[->1] ##0 (v>0, v=v-1))[*1:$] ##1 !vld[*1:$] ##0 $rose(ack);
// passes if 1 vld then an ack, or 2 non-sequential vld then ack,
// fails if 3 vld in any order before an ack .
// At every vld, v=v-1. Two sequential vld followed by a $rose(ack) do not make a pass.
// vld 0 0 1 0 0 x
// ack x x x 0 1 <--- PASS here
//
// vld 0 0 1 1 0 x
// ack x x x 0 <-- FAIL here, v is decremented by 2
// other threads are still tested until v<0
If you want vld must occur at least 2 in my model, between req and ack.
you’ll need to tune the conditions. Also, making a requirement that ack and vld are not in the same cycle.
See my next reply that is a modification to your approach