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

In reply to Jadoon:

I have to give some thought about what you wrote, but just looking at code

$rose(rst) |=> ( (a[=>5]) intersect (!o[*]) ) ##1 ( $rose(a) && $rose(o) ) ##1 ( (a[=1:$]) intersect !o[*] ) ;
// that should be 
 $rose(rst) |=> ( (a[->5]) intersect (!o[*]) ) ##[1:1000]( $rose(a) && $rose(o) ) ##1 ( 

//(a[=1:$]) intersect !o[*] ) ;
Above looks illegal (a[=1:$]
And if it is, it does not make sense.
I suggest that you explain that property in English.
Ben