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

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.


Attachment: BinarySearchContext.tla
Description: Binary data

Attachment: BinarySearch.tla
Description: Binary data

On 14 Mar 2017, at 06:08, Jonathan Ostroff <jonathan....@xxxxxxxxx> 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. 


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.

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)
Termination == <>(pc = "Done")

However, 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).





------------------------ 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 BinarySearch
      f \in SmallSortedS
    , v \in Vals \* target
    , p = 1, q = Len(f)
    , mid = -2
    , r = 0
    , found = FALSE
    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
                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.