50 views

Skip to first unread message

Nov 27, 2019, 10:48:27 AM11/27/19

to tlaplus

Hi

I'm trying to implement algorithm to find loops in graph .

Graph is defined as adjacency matrix or function of [1..Dim,1..Dim -> {0,1}] where matrix[x,y] = 1 is existence of edge from vertex x to vertex y

Each transition is defined with an respective operator concerning current and next states of each variable

For some reason , I'm getting 'deadlock reached' report and I don't understand why ?

My understanding from error trace is for some reason 'checkArcToBeginning' was not enabled . But I'm not sure how to advance from here

Thanks in advance for help

Lev

Nov 27, 2019, 12:24:42 PM11/27/19

to tla...@googlegroups.com

please also share your loop_utils module.

Thanks

Markus

Nov 29, 2019, 6:57:08 AM11/29/19

to tla...@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

/\ 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 }

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3b87f2b3-235b-45a5-94af-4c577837be9a%40googlegroups.com.

<loop_utils.tla>

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu