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

[tlaplus] Directed Graph from Specifying Systems

I tried using the directed graph operator Path from Specifying Systems book, however, I can't figure how to put in a state constraint that will let me use the operator.

Here's the Path spec straight from the book.

Path(G) == \* The set of paths in G, where a path is represented as a sequence of nodes
    {p \in Seq(G.node): /\ p # <<>>
                        /\ \A i \in 1..(Len(p) - 1): <<p[i], p[i+1] \in G.edge>>}

Here's how I am trying to use it in the "evaluate constant _expression_" section

Path([node |-> {1, 2, 3}, edge |-> {<<1, 2>>, <<2, 3>>}])

I get the error

"Attempted to enumerate { x \in S : p(x) } when S:
Seq({1, 2, 3})
is not enumerable"

I tried putting a constraint when trying to use in the TLC model checker, but I still have the issue that Seq(...) is non enumerable.

Has anyone successfully used this Path operator in a Spec? If so, would love any tips on how to make it work. Meanwhile, I have switched to using Giuliano Losa's DiGraph from https://github.com/nano-o/TLA-Library/blob/master/DiGraph.tla which works, but I am curious to know how the non-enumerable Seq(...) problem can be solved when it is invoked from inside an operator.


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/1b46b49c-e154-4a4a-949d-41c7db5864e8n%40googlegroups.com.