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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Thu, 25 Jun 2015 11:15:57 +0200*References*: <d5ce7281-3521-4201-af5e-c1167d74b9ff@googlegroups.com>

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**

> 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.

**Follow-Ups**:**Re: [tlaplus] How to define a Sorted Array***From:*Piyush Bansal

**References**:**How to define a Sorted Array***From:*Piyush Bansal

- Prev by Date:
**How to define a Sorted Array** - Next by Date:
**Re: [tlaplus] How to define a Sorted Array** - Previous by thread:
**How to define a Sorted Array** - Next by thread:
**Re: [tlaplus] How to define a Sorted Array** - Index(es):