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

[Lev Broido <lev.broido@xxxxxxxxx>]

Thanks for fast answer .

Attached

Lev

On Wednesday, November 27, 2019 at 7:24:42 PM UTC+2, Markus Alexander Kuppe wrote:

On 27.11.19 07:48, Lev Broido wrote:
> 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

Hi Lev,

please also share your loop_utils module.

Thanks
Markus

-- 
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/3b87f2b3-235b-45a5-94af-4c577837be9a%40googlegroups.com.

Attachment: loop_utils.tla
Description: Binary data