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

*From*: Pramod Biligiri <pramodb...@xxxxxxxxx>*Date*: Sat, 26 Jan 2019 22:35:42 +0530

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 Ordered

define

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

end define;

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

end define;

Thanks,

Pramod

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

- Prev by Date:
**Re: [tlaplus] Practical TLA+ now out** - Next by Date:
**Re: [tlaplus] How to define an invariant that describes a sorted sequence** - Previous by thread:
**Re: why need /\ item' = item?** - Next by thread:
**Re: [tlaplus] How to define an invariant that describes a sorted sequence** - Index(es):