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

*From*: Pramod Biligiri <pramodb...@xxxxxxxxx>*Date*: Sun, 27 Jan 2019 18:21:16 +0530*References*: <CA+UMGiGcDG9aLqpsXtZS88Bzo7AQt+1ekaFh2VFhT+qF_DOAFA@mail.gmail.com> <04B2CD14-83B4-4660-AAB3-22B1862FCC7A@gmail.com>

Thanks! That worked.

Pramod

On Sat, Jan 26, 2019 at 10:52 PM Stephan Merz <stepha...@xxxxxxxxx> wrote:

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]Regards,StephanOn 26 Jan 2019, at 18:05, Pramod Biligiri <pramodb...@xxxxxxxxx> wrote:Hi,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 Ordereddefine

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

end define;Thanks,Pramod--

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.

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.

**References**:**How to define an invariant that describes a sorted sequence***From:*Pramod Biligiri

**Re: [tlaplus] How to define an invariant that describes a sorted sequence***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] How to Avoid Attempted to check set membership in a tuple value.** - Next by Date:
**Two Questions about (State) Constraints in TLC** - Previous by thread:
**Re: [tlaplus] How to define an invariant that describes a sorted sequence** - Next by thread:
**How to Avoid Attempted to check set membership in a tuple value.** - Index(es):