In reply to hisingh:
If you have
seq |=> strong (…) similarly for |->, #=#, #-#
the strength applies to the consequent only. Hence if the simulator has not entered the consequent there is no failure at the end of sim.
if the antecedent is in progress at end of Sim the assertion does not fail even if the property is strong.
A ##1 1 |-> strong(B ##1 c) ;
If end of Sim is at A then no failure
If end of Sim at the ##1 |->
Then B is evaluated. Regardless of B, assertion fails because of the strong.