Counting number of events on clock a, while clock o is forbidden

[ben2]

In reply to Jadoon:

Use the implication operator after the rst
$rose(rst) |=> (a[->4]) intersect !o[*]) ##1 a[->1]