Help with trivial spec: set generation

[Jeenu Viswambharan]

Hi,

I'm having trouble writing up a rather trivial spec: fill a set that sum to a given total. Or rather, I'm verifying that the actions in spec generates such a set.

For example, given a goal 3, I'd expect either of these to be generated:

{<<0: 1>>, <<1: 1>>, <<2: 1>>}

{<<0: 1>>, <<1: 2>>}

{<<0: 2>>, <<1: 1>>}

{<<0: 3>>}

When running TLC, it complains about reaching deadlock, which I believe is when it reached the final state and no more states can be generated. That's fair enough, but how do I say it's not really deadlock, but is the final state and not error?

Also, in an attempt to get TLC to ignore this particular path and explore further, I specified -deadlock. Sometimes it complains about stuttering, and other times goes ahead with a runaway, seemingly infinite, counterexample. I'm unable to consistently reproduce the latter, despite specifying the seed and fp value printed by TLC (output in the repo).

I'd like to think there's something wrong with my spec, but am struggling to find what. I'd appreciate if someone can take a look and tell me what's wrong: https://bitbucket.org/jeenuv/test_spec/.

Thanks,

Jeenu

[Jeenu Viswambharan]

Correction: I think I had a local change earlier, but am able to reproduce.

[Stephan Merz]

Hello,

TLC reports a deadlock when no action is applicable anymore, and as you suspect, this may well represent termination. Just uncheck deadlock checking in the Toolbox or run TLC from the command line with option -deadlock, as you did.

I suggest that you check invariant properties before checking liveness properties. Typically, you may want to verify the invariant

done => AlreadyFilled = total

A problem with your spec with regard to liveness properties is that you did not specify any fairness conditions. Since stuttering steps are always possible, it is not guaranteed that the total will be reached in every run, and this is what TLC tells you when it reports a counter-example ending in stuttering. I suggest that you add the fairness condition

WF_vars(Next)

that requires that a non-stuttering transition will eventually occur when such a transition is enabled.

Besides, there is an issue in your definition

AlreadyFilled ==
  SumSet({ q : <<i, q>> \in fills })

Assume that fills = {<<0,1>>, <<1,1>>}, then the argument to SumSet will be {1} (which is the same as {1,1}), and so AlreadyFilled will evaluate to 1 instead of 2. This problem leads to your specification having an infinite state space.

I suggest that you represent the candidate solution as a sequence and use a variant of fold that applies to sequences (see below). Alternatively, you could use a multiset representation, but there is less library support. Also, instead of recomputing the sum of the values in the current candidate, you could store it in an additional variable of your spec.

Finally, for such combinatorial problems you may consider eschewing transition system specifications altogether and just write a constant specification, as shown below (adapted from your spec, also note that you could use the Community modules [1] that provide pre-defined fold operations). [2] The idea is to let TLC compute all solutions as a set of sequences whose elements are integers in the set 1.. total. Unfortunately, we cannot simply write

result == { seq \in Seq(1 .. total) : SumSeq(seq) = total }

because the expression on the right-hand side quantifies over an infinite set. So we'll bound the set of candidates to sequences whose length is at most `total' – again, the Community modules contain the appropriate definition.

In order to evaluate the result from the Toolbox, create a model and enter a value for the constant parameter `total'. In the Model Overview pane, click on "Evaluate Constant Expressions' and enter `result' (without quotes) in the Expression field, then launch TLC. Evaluation succeeds for values of total up to 7: beyond that, the candidate set becomes too large.

Hope this helps,

Stephan

[1] https://github.com/tlaplus/CommunityModules

[2] It depends on the context in which the spec will be used which approach is preferable.

-------------------------------- MODULE Sum --------------------------------

EXTENDS Naturals, Sequences, TLC

CONSTANTS

  total

SeqOf(set, n) == 

  (***************************************************************************)

  (* All sequences up to length n with all elements in set.                  *)

  (***************************************************************************)

  UNION {[1..m -> set] : m \in 0..n}

FoldSeq(op(_,_), base, seq) ==

  LET RECURSIVE f(_)

      f(s) == IF s = << >> THEN base

              ELSE op(Head(s), f(Tail(s)))

  IN  f(seq)

SumSeq(seq) ==

  FoldSeq(

    LAMBDA a, b: a + b,

    0,

    seq)

Candidates ==  

  (*************************************************************************)

  (* Candidate sequences contain the numbers up to `total' and are of      *)

  (* length at most `total'.                                               *)

  (*************************************************************************)

  SeqOf(1..total, total)

result == { seq \in Candidates : SumSeq(seq) = total }

=============================================================================

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d1e6b7dc-11bb-4a79-84db-3df47c5edbfcn%40googlegroups.com.

[Jeenu Viswambharan]

Ah, that I could lose fills when adding to a set was completely lost on me. Thanks! For brevity, I choose to keep the quantity in a separate variable than to re-compute. With that, I got TLC completing its run (repo updated).

It bothers me that I still have to pass -deadlock on the command line, though, without which TLC still calls out deadlock. I tried specifying weak fairness, as you suggested, as a conjunct to the spec formula, but that didn't change anything.

Is it a bad thing that I've to specify the -deadlock flag? Do you reckon it's a property of how this particular spec is written, or any spec that has a terminal state?

Jeenu

[Stephan Merz]

Disabling deadlock checking is standard practice when verifying algorithms whose executions are expected to terminate. Checking for deadlocks is mainly useful for algorithms that are expected to run forever, which is the case for many distributed algorithms.

Also, I suggested adding the fairness condition for verifying the liveness properties that you stated in the original version, in particular for verifying termination, i.e. the property <> done. It won't have an effect on deadlock checking: note that absence of deadlock is a safety property.

Stephan

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b7417987-5e60-4f4f-ab96-f9a4c71d50c2n%40googlegroups.com.