Host and Clock from ShiViz module do not appear in error trace

[Alexander-N]

As suggested in #37 (comment) I tried using ALIAS to make Host and Clock from the ShiViz module appear in the error trace. While ALIAS works in principle, it seems to get ignored as soon as I add Host or Clock:

---- CONFIG testAlias ----
SPECIFICATION Spec
INVARIANT NotTwo
ALIAS Alias
======================

----------------------------- MODULE testAlias -----------------------------
EXTENDS Integers, ShiViz

(*--algorithm testAlias
variables x=0;
begin
  x := 1;
  x := 2;
end algorithm; *)

\* BEGIN TRANSLATION (chksum(pcal) = "b3726e35" /\ chksum(tla) = "e9b2f587")
VARIABLES x, pc

vars == << x, pc >>

Init == (* Global variables *)
        /\ x = 0
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ x' = 1
         /\ pc' = "Lbl_2"

Lbl_2 == /\ pc = "Lbl_2"
         /\ x' = 2
         /\ pc' = "Done"

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1 \/ Lbl_2
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

NotTwo == x /= 2
Alias == [
  test |-> x + 2,
  Host |-> Host
]
=============================================================================

[lemmy]

As outlined in tlaplus/tlaplus#543, error-reporting for ALIAS still hasn't been figured out. What I assume is that your Shiviz.tla still has LOCAL INSTANCE Toolbox?!

[Alexander-N]

What I assume is that your Shiviz.tla still has LOCAL INSTANCE Toolbox

It's the new version which has INSTANCE Toolbox.

[lemmy]

I see what is going on here. Your spec is not a "trace spec", i.e., one that re-defines the _TETrace operator. The Toolbox!_TETrace works iff there is a definition override in place. You can generate a "trace spec" from your original spec.

More fundamentally, though, your spec describes a single-process algorithm for which ShiViz doesn't work (pc has to be a function), and doesn't really make sense anyway.

---- MODULE testAlias_TTrace ----
EXTENDS testAlias, Toolbox, TLC, ShiViz

\* TE declaration
TTraceExpression == 
    [
        x |-> x
        ,pc |-> pc
        ,e |-> Host
    ]

\* TraceDef definition
TTraceTraceDef == INSTANCE TTraceTraceDef
_def_ov == TTraceTraceDef!_def_ov

\* INVARIANT definition
_inv ==
    ~(pc = "Done" /\ x = 2)
----

\* TRACE INIT definition traceExploreInit
_SpecTEInit ==
    /\ x = _TETrace[1].x
    /\ pc = _TETrace[1].pc

----

\* TRACE NEXT definition traceExploreNext
_SpecTENext ==
    /\ \E i,j \in DOMAIN _TETrace:
        /\ \/ j = i + 1
        /\ x  = _TETrace[i].x
        /\ x' = _TETrace[j].x
        /\ pc  = _TETrace[i].pc
        /\ pc' = _TETrace[j].pc

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

---- MODULE TTraceTraceDef ----
EXTENDS testAlias, Toolbox, TLC

_def_ov == 
    <<
    ([pc |-> "Lbl_1",x |-> 0]),
    ([pc |-> "Lbl_2",x |-> 1]),
    ([pc |-> "Done",x |-> 2])
    >>

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

[Alexander-N]

Thank you, but I must admit I'm a bit lost on what the problem is and how it is solved. Is there anything I could read to learn about this?

Sorry for the bad example, the spec I'm interested in is not a single-process one, I'm experimenting with visualizing https://github.com/Alexander-N/tla-specs/blob/main/dual-writes/dual_writes_shiviz.tla.

[lemmy]

Why don't you evaluate your ShiViz trace expressions in the Toolbox? On the command line, things are in flux and still have rough edges.