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