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

*From*: Kulpreet Singh <zapfmann@xxxxxxxxx>*Date*: Tue, 25 Jul 2023 18:42:41 +0200*References*: <1b46b49c-e154-4a4a-949d-41c7db5864e8n@googlegroups.com> <303D76D2-053B-45E5-9BBD-28DF659C7889@lemmster.de>

Thanks Markus, The link to the Graph module in CommunityMoules was very helpful. I switched to using the SimplePath, which made my life easier. Thanks again Kulpreet On Mon, 24 Jul 2023 at 03:47, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote: > > 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. -- 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/CAN8S4uZisDmFOwEsv-%3DPZLx3dMuXfCB5d5ycFnZmHQRC8eDwsA%40mail.gmail.com.

**References**:**[tlaplus] Directed Graph from Specifying Systems***From:*Kulpreet Singh

**Re: [tlaplus] Directed Graph from Specifying Systems***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] TLA+ and C++ templates** - Next by Date:
**[tlaplus] test** - Previous by thread:
**Re: [tlaplus] Directed Graph from Specifying Systems** - Next by thread:
**[tlaplus] A TLA+ AutoRepair Program with GPT-4** - Index(es):