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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 29 Nov 2019 12:57:04 +0100*References*: <f37711ca-6850-4664-a920-eb24f51e199a@googlegroups.com> <1e0e570f-fe56-d7f2-eedd-ee32bd8eaadd@lemmster.de> <3b87f2b3-235b-45a5-94af-4c577837be9a@googlegroups.com>

Hello, the reason for the deadlock is a simple typo: States == {"CheckArcToTheBeginning", ...}
-- whereas the action fetchNext sets "CheckArcToBeginning". Because you include TypeInvariant in the next-state relation, no action is enabled when state = "CheckArcToBeginning". Two comments: 1. Rather than including invariants in the next-state action, check that they are implied by the specification. (It sometimes makes sense to include the type invariant in the initial predicate, for example if you want to consider all type-correct initial states.) 2. TLA+ encourages you to think in terms of sets and functions, and to use set-theoretic expressions rather than recursive definitions as in programming languages. For example, I rewrote your definitions as path_exists(_matrix, path) == /\ Len(path) >= 1 \* I don't understand why it matters but well ... /\ \A i \in 1 .. Len(path)-1 : _matrix[path[i], path[i+1]] = 1 find_all_loops(mx) == LET \* non-empty sequences of nodes (elements of 1..Dim) of length at most Dim node_seqs == UNION { [ 1..m -> 1..Dim ] : m \in 1 .. Dim } \* set of elements of a sequence Range(s) == { s[i] : i \in 1 .. Len(s) } \* node sequences without duplicates cand_paths == { x \in node_seqs : Cardinality(Range(x)) = Len(x) } IN { x \in cand_paths : /\ path_exists(mx,x) /\ mx[x[Len(x)], x[1]] = 1 } which I find much easier to understand. Recursive definitions are sometimes more efficient to evaluate for TLC, but this should not be your first concern when writing a specification (and I don't think it is the case here). Incidentally, TLC displays an execution leading to the deadlock state with the non-recursive definitions but not with the recursive ones. Happy TLA hacking, 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0CE99E34-569A-4B6C-B982-29C3777A044F%40gmail.com. |

**References**:**[tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why***From:*Lev Broido

**Re: [tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why***From:*Markus Kuppe

**Re: [tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why***From:*Lev Broido

- Prev by Date:
**Re: [tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why** - Next by Date:
**[tlaplus] Copying Error Traces** - Previous by thread:
**Re: [tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why** - Next by thread:
**[tlaplus] Copying Error Traces** - Index(es):