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.