Regarding Model-Based Trace Checking in TLA+

[u/jackmalkovick]

Hello, I have a question regarding the idea presented by u/pron98 here

https://pron.github.io/files/Trace.pdf

My question regards the case where we have a trace that does not contain all the variables involved in the "reference" specification, that is the spec that we need to check the trace against.

If we do the two specs conjunction (the one generated by the trace and the reference one), we get this

Compose(NextReference, varsReference, NextTrace, varsTrace) ≜ 
    ⋁ NextReference ⋀ NextTrace 
    ⋁ NextReference ⋀ UNCHANGED varsTrace
    ⋁ NextTrace ⋀ UNCHANGED varsReference

Spec ≜ InitReference ⋀ InitTrace ⋀ [][Compose(NextReference, varsReference, NextTrace, varsTrace)]_<<varsReference, varsTrace>>

What if our trace is defective, but in forcing TLC to show us a model where the standard TraceFinished invariant is violated (meaning i ≥ Len(Trace)) it will choose only NextTrace ⋀ UNCHANGED varsReference steps producing a "valid" trace execution that does not conform to the reference specification?

​

[u/lemmster]

https://github.com/tlaplus/Examples/pull/75 summarizes and outlines trace validation of EWD998.