Action name in error trace

[Michel Charpentier]

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]

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]

Hi.

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

Let's take DieHard.tla as an example (https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla#L105-L110).

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]

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]

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

ocad...@gmail.com

========================