Leslie
I forgot the beginning of the spec:---------------------------- MODULE TestTemporal ----------------------------EXTENDS Sequences, NaturalsVARIABLE sCONSTANT X
On Tuesday, June 25, 2013 1:02:56 PM UTC+2, Giuliano wrote: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--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.