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

*From*: Piyush Bansal <bansal....@xxxxxxxxx>*Date*: Thu, 25 Jun 2015 04:09:45 -0700 (PDT)*References*: <d5ce7281-3521-4201-af5e-c1167d74b9ff@googlegroups.com> <7D0E1C41-ED2A-4E53-AEAB-6142A8A649E8@gmail.com>

Dear Sir,

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

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

**Attachment:
BinarySearch.tla**

**Follow-Ups**:**Re: [tlaplus] How to define a Sorted Array***From:*Markus Alexander Kuppe

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

**Re: [tlaplus] How to define a Sorted Array***From:*Stephan Merz

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