Re: [tlaplus] Directed Graph from Specifying Systems

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Hi Kulpreet,

TLC is unable to evaluate your expression involving  Path  since there are infinitely many paths, and a state constraint doesn't apply here due to your formula being constant-level.  However, TLC can still evaluate if a certain path is an element of the set of all paths.  For example, it can evaluate the expression:  <<1,2,3>> \in Path([node |-> {1, 2, 3}, edge |-> {<<1, 2>>, <<2, 3>>}]) .

It's worth noting that the CommunityModules Graphs module [1] defines an additional operator called  SimplePath, which TLC evaluates without any issues.  Other operators such as  AreConnectedIn  and  IsStronglyConnected  are defined based on  SimplePath.

Markus

[1] https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla

> On Jul 22, 2023, at 11:45 AM, Kulpreet Singh <zapfmann@xxxxxxxxx> wrote:
> 
> 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.
> 
> Regards
> Kulpreet
> 
> 
> 
> -- 
> 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.

-- 
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/303D76D2-053B-45E5-9BBD-28DF659C7889%40lemmster.de.