ShiViz module error because operator definition override not visible when instance marked local

[Alexander-N]

I have been trying to use the ShiViz module in this spec without success. After I add either Host or Clock to the error-trace exploration I'm getting the following error (Toolbox version 1.7.1):

Error(s) from running the Trace Explorer:
Attempted to enumerate S \ T when S:
Nat
is not enumerable.
Error(s) from running the Trace Explorer:
TLC was unable to fingerprint.

Fingerprint Stack Trace:
1) line 14, col 21 to line 14, col 29 of module Toolbox
0) line 14, col 18 to line 14, col 42 of module Toolbox

Reason:
Attempted to enumerate S \ T when S:
Nat
is not enumerable.

Error seems to persist after overwriting Nat with 1..100.

[lemmy]

This works:

• Generated "trace spec" (TE)
• Inlined most of TE into its main module
• Inlined ShiViz module
• Explicitly defined _TETrace (and _TEPosition) in TE

The underlying issue is that TLC apparently does not honour the re-definition of _TETrace, and, thus, tries to evaluated Nat \ {0} ...

---- MODULE dual_writes_TTrace ----
EXTENDS TLCExt, Json, dual_writes, Sequences

CONSTANTS ClientA, ClientB

_trace == 
    <<
    ([StorageValues |-> (Database :> 0 @@ Cache :> 0),pc |-> (ClientA :> "WriteDatabase" @@ ClientB :> "WriteDatabase")]),
    ([StorageValues |-> (Database :> ClientA @@ Cache :> 0),pc |-> (ClientA :> "WriteCache" @@ ClientB :> "WriteDatabase")]),
    ([StorageValues |-> (Database :> ClientB @@ Cache :> 0),pc |-> (ClientA :> "WriteCache" @@ ClientB :> "WriteCache")]),
    ([StorageValues |-> (Database :> ClientB @@ Cache :> ClientB),pc |-> (ClientA :> "WriteCache" @@ ClientB :> "Done")]),
    ([StorageValues |-> (Database :> ClientB @@ Cache :> ClientA),pc |-> (ClientA :> "Done" @@ ClientB :> "Done")])
    >>
----

_TETrace == _trace
_TEPosition == TLCGet("level")

_prop ==
    ~<>[](
        StorageValues = ((Database :> ClientB @@ Cache :> ClientA))
        /\
        pc = ((ClientA :> "Done" @@ ClientB :> "Done"))
    )
----

_init ==
    /\ StorageValues = _TETrace[1].StorageValues
    /\ pc = _TETrace[1].pc
----

_next ==
    /\ \E i,j \in DOMAIN _TETrace:
        /\ \/ j = i + 1
        /\ StorageValues  = _TETrace[i].StorageValues
        /\ StorageValues' = _TETrace[j].StorageValues
        /\ pc  = _TETrace[i].pc
        /\ pc' = _TETrace[j].pc

-----------------------------------------------------------------------------

LOCAL FnHost ==
    LET host[i \in DOMAIN _TETrace] ==
        (*************************************************************************)
        (* The pc value that has been modified in (the current) state n compared *)
        (* to the predecessor state n-1.                                         *)
        (*************************************************************************)
        IF i = 1 THEN "--"
        ELSE IF _TETrace[i-1].pc = _TETrace[i].pc
                THEN host[i-1] \* pc variable has not changed.
                ELSE CHOOSE p \in DOMAIN _TETrace[i-1].pc :
                            _TETrace[i-1].pc[p] # _TETrace[i].pc[p]
    IN TLCEval(host)

Host == FnHost[_TEPosition]
    
-----------------------------------------------------------------------------

LOCAL clock(n) == 
   IF n = 1 THEN [p \in DOMAIN _TETrace[n].pc |-> 0] \* In the init state, all clocks are 0.
   ELSE [p \in DOMAIN _TETrace[n].pc |-> IF p = FnHost[n] 
                                    THEN 1
                                    ELSE 0]

LOCAL sum(F, G) == 
   [d \in DOMAIN F |-> F[d] + G[d]]

LOCAL FnClock == 
    LET vclock[i \in DOMAIN _TETrace] == 
        IF i = 1
        THEN clock(i)
        ELSE sum(TLCEval(vclock[i-1]), clock(i))
    IN TLCEval(vclock)

Clock ==
   (*************************************************************************)
   (* The pc variable formatted as a Json object as required by ShiViz.     *)
   (*************************************************************************)
   FnClock[_TEPosition]


_expression == 
    [
        StorageValues |-> StorageValues
        ,pc |-> pc
        ,h |-> Host
        ,c |-> Clock
    ]

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

[lemmy]

Btw. the Json module won't work without its Java module override.

[Alexander-N]

Thank you! How can I generate the trace spec? I added the most recent CommunityModules-deps.jar to the library path locations, but I'm getting

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NoClassDefFoundError
: tlc2/value/impl/KSubsetValue

There are no errors in the user or progress output.

[lemmy]

Don't bother with the trace spec--this should work with the Toolbox too. I hope to look into it tomorrow.

About KSubsetValue: You will need a recent build of TLC from https://github.com/tlaplus/tlaplus/releases#latest-tla-files

[lemmy]

The fix is to change the third line in ShiViz.tla from:

LOCAL INSTANCE Toolbox

to

INSTANCE Toolbox

Regression introduced with a39cb8a

[lemmy]

Fixed in https://github.com/tlaplus/CommunityModules/releases/tag/202103291751

[lemmy]

FWIW: TLC's behavior WRT LOCAL is considered a bug.

[Alexander-N]

Thanks @lemmy! Another unrelated problem I had was that Host and Clock did not seem to appear in in the TLC console output. But it works through the export error-trace button.

[lemmy]

@Alexander-N If you want Host and Clock to appear in TLC's error-trace, you should check out the new-ish ALIAS feature.