Hi Ben,
I am not clear about the following table you have given. According to the table, result for attempt m @ cycle 3 is a fail for assertion a[*1:] |-> p) and the result for assertion a |-> p for attempt k at cycle 3 is also a fail. For assertion a |-> p, attempt t @cycle 4 is vacuous pass but for assertion (a[*1:] |-> p) @cycle 4, for all threads of attempts m, n, k, t, a[*1:$] is not true so it should also be a vacuous pass. So that would mean both the assertions are equivalent. For case II @cylce 4 you have shown V, vacuous pass but for case I @cycle 4, you have just shown - as result. What does that mean? Can you please elaborate why result is not V for case I @cycle 4 and why Case I and Case II are not equivalent.
rgs,
-sunil
case I
attempt m n k t y
cycle 1 2 3 4 5
a== 1 1 1 0 X . ..
p== 1 1 0 X X
assertion a[*1:$] |-> p)
4 attempt m S A F - // result for attempt m thread 3 @ cycle 3 is FAIL
--
Case II
assertion a |-> p
4 attempt m P -------------
4 attempt n - P ------------
4 attempt k ---------F -------
4 attempt t ------------V // vacuous true, vacuous result
// Remember that ALL threads of antecedent must be tested. Simulator may optimize; e.g., for a[*1:$], any occurrence of a==0 means that all other occurrences are false.