# Re: [tlaplus] Cannot select an Behaviour Spec for TLC-Model-Checker

 Hi Jonathan,you already found out about the problem of what is the root module.Your spec contained a few infelicities, such as "mid[f]", which should in fact have been "mid" or a confusion of r and v in the first assertion. I also suggest you make N a parameter that you instantiate in your model rather than defining it in the context module. The result is attached (don't forget to translate the PlusCal algorithm before running TLC), and it seems to work based on the few tests that I made.Regards,Stephan

Attachment: BinarySearchContext.tla
Description: Binary data

Attachment: BinarySearch.tla
Description: Binary data

 On 14 Mar 2017, at 06:08, Jonathan Ostroff wrote:To answer my own question, the first module to be defined appears to be the root module. So I needed to start the specification with BinarySearch.tla not the context module (even though the dependency is the other way). Any hints on how to improve on the specifications still appreciated. Jonathan=============================I have written a binary search algorithm with two modules as shown below. Both modules appear to parse and the BinarySearch seems to translate without errors.\* BEGIN TRANSLATION …. …. …. Spec == /\ Init /\ [][Next]_vars        /\ WF_vars(Next)Termination == <>(pc = "Done")\* END TRANSLATIONHowever, when selecting TLC-Model-Checker —> new Module, the No Behaviour-Spec button is selected, and the Temporal Formula button cannot be selected for Spec. So I cannot check the model.This has not happened with other algorithms so I am wondering what I did wrong?(Also, any help on writing the specifications for this algorithm would be appreciated).ThanksJonathan===============------------------------ MODULE BinarySearchContext ------------------------EXTENDS Sequences, Integers  IsSorted(s)  == \A i,j \in DOMAIN s: i <= j => s[i] <= s[j]   SortedSeq(s) == { seq \in Seq(s) : IsSorted(seq) }  Range(f) == { f[x] : x \in DOMAIN f }  SortedSeqN(s,N) == UNION { { seq \in [ 1..n -> s ] : IsSorted(seq) } : n \in 1..N }  N == 7  Vals == 0..N+1  SmallSortedS == { seq \in SortedSeqN(1..N,N) : seq[1] = 1 }=============================================================================PlusCal options (-termination)---------------------------- MODULE BinarySearch ----------------------------EXTENDS  BinarySearchContext, Integers, TLC(***************************************************************************--algorithm BinarySearchvariables       f \in SmallSortedS    , v \in Vals \* target    , p = 1, q = Len(f)    , mid = -2    , r = 0    , found = FALSEbegin    if v <= f[q] then        while p <= q /\ ~found do            mid := (p+q) \div 2;            if v = f[mid] then                r := mid[f];                found := TRUE;            elsif v > f[mid] then                p := mid + 1            else                q := mid - 1            end if;        end while;    end if;    print v;    assert (v \in Range(f) => r \in DOMAIN f /\ f[r] = v) ;    assert (r = 0 <=> ~ v \in Range(f)) ;    end algorithm ***************************************************************************) -- 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 https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.

• References: