Re: [tlaplus] How to define a Sorted Array

Dear Sir,

Thank you, for your help. I got the concept.

Now I am facing some different problem: no user output is printed and statistics also show everything as zero.

You can check that attached file.

Regards,

Piyush

On Thursday, June 25, 2015 at 2:45:56 PM UTC+5:30, Stephan Merz wrote:

Dear Piyush,

of course you can turn the variable arr into a constant (your PlusCal algorithm can refer to it just like it refers to N). See TLA+ module attached to this message. When you create your model, you instantiate the constant arr by the _expression_ [i \in 1..N |-> i+1] or whatever _expression_ you want to test.

On the other side, you could be more adventurous and define TLA+ operators

IsSorted(a) == \A i \in 1 .. N-1 : a[i] <= a[i+1]
SortedArrays == { a \in [ 1..N -> 1..N+1 ] : IsSorted(a) }

then write

variables arr \in SortedArrays

TLC will enumerate all sorted arrays and check your algorithm for all of them. Of course, state explosion will kill you very quickly …

Best regards,
Stephan