[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Giuliano <giulia...@xxxxxxx>*Date*: Tue, 25 Jun 2013 04:02:56 -0700 (PDT)

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

**Follow-Ups**:**Re: Problem with the symmetry set option***From:*Giuliano

- Prev by Date:
**Re: [tlaplus] Segmentation fault** - Next by Date:
**Re: Problem with the symmetry set option** - Previous by thread:
**Re: [tlaplus] Segmentation fault** - Next by thread:
**Re: Problem with the symmetry set option** - Index(es):