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

Re: [tlaplus] How to define an invariant that describes a sorted sequence

The syntax for quantifiers bounds is "variable \in set", the _expression_ "i < j" doesn't fit that pattern. You want to write

\A i \in 1..Len(myList), j \in 1..Len(myList) : i < j => myList[i] < myList[j]


On 26 Jan 2019, at 18:05, Pramod Biligiri <pramodb...@xxxxxxxxx> wrote:

I'm trying to define an invariant that specfies a sequence should be (strictly) ordered, and am not getting the correct syntax. My sequence is called myList and the invariant is called Ordered

     Ordered == \A i \in 1..Len(myList), j \in 1..Len(myList), i < j: myList[i] < myList[j]
end define;       


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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.