States missing from dump?

18 views
Skip to first unread message

leroy.va...@gmail.com

unread,
Dec 11, 2019, 2:22:44 PM12/11/19
to tlaplus
Hi,

when running TLC with the `-dump` flag on the following model:

```
---- MODULE Bug ----
CONSTANTS Data
VARIABLES state

Init == state = {}
Next == \E e \in Data: state' = state \union {e}
====
```

with the following config:

```
CONSTANTS Data = {d1, d2}

INIT Init
NEXT Next
```

I get the following output in the dump:

```
State 1:
state = {}

State 2:
state = {}

State 3:
state = {}

State 4:
state = {d1}
```

For some reason the first three states are duplicated and two states are missing. Generating a graphical dump using `-dump dot states` gives me the output I expect:

states.dot.png



Is this a bug or is my expectation wrong? I don't have a lot of TLA+ experience yet :)

Thanks in advance,

-Leroy

Markus Kuppe

unread,
Dec 11, 2019, 2:55:03 PM12/11/19
to tla...@googlegroups.com
On 11.12.19 11:19, leroy.va...@gmail.com wrote:
> Is this a bug or is my expectation wrong? I don't have a lot of TLA+
> experience yet :)


It appears this is a bug in TLC. Can you please open a new issue at
GitHub [1]?

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues

Leroy van Engelen

unread,
Dec 12, 2019, 4:04:18 AM12/12/19
to tlaplus
On Wednesday, December 11, 2019 at 8:55:03 PM UTC+1, Markus Alexander Kuppe wrote:
On 11.12.19 11:19, leroy.v...@gmail.com wrote:
> Is this a bug or is my expectation wrong? I don't have a lot of TLA+
> experience yet :)


It appears this is a bug in TLC.  Can you please open a new issue at
GitHub [1]?

Sure, done! 
Reply all
Reply to author
Forward
0 new messages