Problem with the symmetry set option

[Giuliano <giulia...@xxxxxxx>]

Hello, I have the following spec with TLC configured to replace Seq(x) by BSeq(x) == UNION {[1..n -> x] : n \in {1,2}}, to use the state constraint Len(s) <= 2, to replace X with the set of model values {x1,x2}, and to check the temporal formula Test.

Running TLC like that produces no errors. However if I check the symmetry set option for X then TLC reports that the temporal formula is violated but shows an error trace that does not violate it.

Is TLC expected to find that the formula is violated or is it a bug?

After reading page 246 of Specifying Systems I believe that, when X is a symmetry set, the state graph should be of the form 

{(<<>>,<<x1>>),(<<x1>>,<<x1,x2>>),(<<x1>>,<<x1,x1>>)}.

If it is the case then the formula Test should not be found violated.

Is this correct?

Maybe the toolbox should display a warning when checking a temporal formula in the presence of a symmetry set, since the resulting behavior can be tricky to understand.

Init == s = <<>>

Next == \E x \in X : s' = Append(s,x)

Prefix(s1,s2) == 

    /\ Len(s1) <= Len(s2)

    /\ \A i \in DOMAIN s1 : s1[i] = s2[i]

    

Test == \A s1 \in Seq(X) : []( (s1 = s) => []Prefix(s1,s) )

Thanks,

Giuliano