How to define a Sorted Array

[Piyush Bansal]

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.

[Stephan Merz]

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

[Piyush Bansal]

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

[Markus Alexander Kuppe]

On 25.06.2015 13:09, Piyush Bansal wrote:
> 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.
>

Hi Piyush,

your spec and a newly created model work fine here. Try creating a new
model on your end and see if TLC checks it. For your current broken
model, what is printed on the "TLC console"?

Best,
Markus

[Piyush Bansal]

Hi Markus,

Thank you for the help. New model works fine. 

Is there any specific reason for such a behavior?

Regards,

Piyush

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/lXcW8Z9kjQg/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.