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

Re: [tlaplus] Help with trivial spec: set generation


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


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,


[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


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) ==
      f(s) == IF s = << >> THEN base
              ELSE op(Head(s), f(Tail(s)))
  IN  f(seq)

SumSeq(seq) ==
    LAMBDA a, b: a + b,

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 }


On 21 Aug 2021, at 13:15, Jeenu Viswambharan <jeenuv@xxxxxxxxx> wrote:


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


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

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6AC4EE1F-8791-4A14-B4EF-3F1CB212A014%40gmail.com.