# Re: [tlaplus] How to define a Sorted Array

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



Attachment: BinarySearch.tla
Description: Binary data



> On 25 Jun 2015, at 10:53, Piyush Bansal <bansal....@xxxxxxxxx> wrote:
>
> Hi,
>
> I am writing tla+ algorithm for Binary Search, I need to define input array 'arr' to sorted. For the verification purpose I did
>
>
> variables arr = [ i \in 1..N |-> i + 1].
>
> Complete pluscal algorithm for BinarySearc.tla is as follows:
>
>
> ---------------------------- MODULE BinarySearch ----------------------------
> EXTENDS Naturals, TLC
>
> CONSTANT N      (* Size of arrays *)
> CONSTANT MAXINT (* Max integer value *)
> (***************************************************************************
> --fair algorithm Binsearch {
>    variables arr = [ i \in 1..N |-> i + 1];
>              x \in 2..N;          (* Value to find *)
>              found = FALSE;
>              l = 1;               (* All elements to the left of l are < x *)
>              r = N;               (* All elements to the right of r are > x *)
>              p = 1;               (* Pivot *)
>
>    (* Main *)
>    {
>        print <<arr, x>>;
>
>        while ((l <= r) /\ (~ found)) {
>            p := (l + r) \div 2;
>
>            if (arr[p] = x)
>                found := TRUE
>            else if (arr[p] < x)e
>                l := p+1
>            else (* arr[p] > x *)
>                r := p-1
>        };
>
>        assert( found <=> (\E j \in 1..N : arr[j] = x) )
>    }
> }
>
> ***************************************************************************)
> ==============================================================================
>
>
> Is it possible to define array 'arr' as CONSTANT, so that I can input it in the TLC model checker with other constants.
>
>
> Regards,
> Piyush
>
> PS: I tried to (1)attach the BinarySearch.tla and (2) Change the font, but not able to do. Can some guide me for this as well.
>
> --
> 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/d/optout.