Action name in error trace

39 views
Skip to first unread message

Michel Charpentier

unread,
Dec 17, 2019, 9:10:50 AM12/17/19
to tlaplus
TLC is often able to display an action name in a trace, instead of a line number.  This is very useful.  However, it seems to be failing the moment Next is not expressed as a disjunction.  I sometimes like to "factorize" ghost variables when defining Next, as in:

A == ...
B == ...

Next ==
  /\ A \/ B
  /\ ghost variables stuff

but then I lose the action names.  I'd rather not have to write:

A ==
  /\ ...
  /\ ghost variable stuff

B ==
  /\ ...
  /\ ghost variable stuff

Is there a way to avoid this duplication while retaining the action names in traces?

MC

Markus Kuppe

unread,
Dec 18, 2019, 1:58:10 PM12/18/19
to tla...@googlegroups.com
Hi Michel,

I can't think of a trick to retain action names, but can't you
reconstruct (logical) action names with trace expressions after model
checking?

Hope this helps,
Markus

Haruki Okada

unread,
May 30, 2022, 9:30:28 PM5/30/22
to tlaplus
Hi.

Related to the original question, I'd like to know the rule when action names are retained.


I found that when we re-write Next as like below, the action names are not retained. (\E \in {FALSE}... is used just to transform the formula without affecting resulting truth value)
Next ==
    \E i \in {FALSE}:
        \/ i
        \/ FillSmallJug
        \/ FillBigJug
        \/ EmptySmallJug
        \/ EmptyBigJug
        \/ SmallToBig
        \/ BigToSmall

However, when we re-write like below, I found that the action names are retained.
Next ==
    \E i \in {FALSE}:
        \/ FALSE
        \/ FillSmallJug
        \/ FillBigJug
        \/ EmptySmallJug
        \/ EmptyBigJug
        \/ SmallToBig
        \/ BigToSmall

So I'm curious retaining action name or not is determined in which rule. Is that explained in some resources?

2019年12月19日木曜日 3:58:10 UTC+9 Markus Alexander Kuppe:

Markus Kuppe

unread,
May 30, 2022, 11:05:04 PM5/30/22
to tla...@googlegroups.com
Hi,

as far as I know, there is no documentation about what actions are retained. You will have to read and debug the source [1].

Markus

[1] https://github.com/tlaplus/tlaplus/blob/6ee6e9f1fe4b6879b7e9cdc4b3e6db687e03a03c/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java#L246-L394
> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57efbd10-867e-4f4a-8b8b-a84697243793n%40googlegroups.com.

Haruki Okada

unread,
May 31, 2022, 12:27:01 AM5/31/22
to tla...@googlegroups.com
Thank you for the reference to the source.
That is exactly what I wanted to know.

2022年5月31日(火) 12:05 Markus Kuppe <tlaplus-go...@lemmster.de>:
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/MB78lt4R4U0/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/19B24DE5-926E-4858-B01A-1150DB1A838F%40lemmster.de.


--
========================
Okada Haruki
========================
Reply all
Reply to author
Forward
0 new messages