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

*From*: Kulpreet Singh <zapfmann@xxxxxxxxx>*Date*: Sat, 22 Jul 2023 02:45:25 -0700 (PDT)

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>>}

{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"

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.

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

- Prev by Date:
**Re: [tlaplus] JavaNullPointerException on Prove Step or Module - problem persisted but has now vanished** - Next by Date:
**[tlaplus] Re: Any tool(s) for generating TLA+?** - Previous by thread:
**Re: [tlaplus] About always and eventually.** - Next by thread:
**Re: [tlaplus] Directed Graph from Specifying Systems** - Index(es):