[tlaplus] [Beginner][Help with debug]Getting deadlock report and don't understand why

[Lev Broido <lev.broido@xxxxxxxxx>]

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

-- 
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/f37711ca-6850-4664-a920-eb24f51e199a%40googlegroups.com.

Attachment: loop_search_v2.tla
Description: Binary data

Attachment: MC.out
Description: Binary data