RFC006: Framework for unit-testing

[konnov]

RFC006 describes in detail a framework for unit-testing of TLA+ specifications. There are plenty of ideas in the PR #741, which is hard to find, unless you know about it. Let's continue the discussion in this thread.

[konnov]

@lemmy wrote in #741 (comment):

Yep. I don't like the idea of exposing the trace explicitly. Once you do that, the users will write arbitrary code involving traces, which makes it much harder to analyze for symbolic techniques.

Power to the People tools. ✊

I think it is clear to me now why I did not want to have an explicit operator like TLCExt.Trace. The issue with this approach is not only that it is hard for Apalache to carry the trace as part of the state, but also that you can define the computation of a TLA+ spec by using the computation history.

A cleaner approach would be to define predicates on computations, similar to LTL, which is a special language for such predicates. (Actually, LTL is defined over infinite traces, but for the finite-state systems we are talking about finite lassos.) Here is an example of how one could specify a trace invariant:

------------------------------- MODULE TraceInv -------------------------------
EXTENDS Integers, Sequences

VARIABLE
    \* @typeAlias: STATE = [x: Int];
    \* @type: Int;
    x

Init ==
    x = 1 \/ x = -1

Next ==
    x' = x + x

\* @type: Seq(STATE) => Bool;
TraceInv(hist) ==
    /\ hist[1].x > 0 =>
        hist[Len(hist)].x >= hist[1].x
    /\ hist[1].x < 0 =>
        hist[Len(hist)].x <= hist[1].x
===============================================================================

[lemmy]

TLCExt!Trace is nothing more than an ("built-in") history variable (that doesn't require users to modify the spec). If users want to define the computation through a computation history, this has always been possible via a user-defined history variable. TraceInv seems to trade an explicit operator for an implicit one by introducing a special model-checker hook (like TLC has "hooks" for action- and state-constraints). In principle, TLC could provide a similar hook. However, where TLCExt!Trace might appear anywhere (Invariants, state- and action-constraints, properties, behavior spec, ...), possibly producing bogus results, TraceInv is limited to one use-case.

Getting back to the original discussion, will it be possible to write (stuttering sensitive) action-level formulas? I find this more readable compared to the variant with hist above.

TraceInv ==
/\ x > 0 => x' >= x
/\ x < 0 => x' <= x

[konnov]

Yes, we have just added support for action invariants over two states, see #816. Trace invariants are just a natural extension of it.

However, where TLCExt!Trace might appear anywhere (Invariants, state- and action-constraints, properties, behavior spec, ...), possibly producing bogus results, TraceInv is limited to one use-case.

I have an impression that making a Swiss knife out of everything makes it hard for the users to discover reasonable use cases.

[lemmy]

I have an impression that making a Swiss knife out of everything makes it hard for the users to discover reasonable use cases.

I consider myself in good company: https://twitter.com/MSFTResearch/status/1392183384772943872 ;-)

[lemmy]

Btw. this is not too different from what TLC generates to re-create a specific trace (on top of which users can evaluate trace expressions, i.e. via expression):

---- MODULE EWD840_TEExpression ----
EXTENDS TLCExt, Toolbox, Naturals, TLC, EWD840

expression == 
    [
        \* To hide variables of the `EWD840` spec from the error trace,
        \* remove the variables below.  The trace will be written in the order
        \* of the fields of this record.
        tpos |-> tpos
        ,active |-> active
        ,tcolor |-> tcolor
        ,color |-> color
        
        \* Put additional constant-, state-, and action-level expressions here:
        \*,_stateNumber |-> _TEPosition
        \* ,_tposUnchanged |-> tpos = tpos'
        
        \* Format the `tpos` variable as Json value.
        \* ,_tposJson |->
        \*     LET J == INSTANCE Json
        \*     IN J!ToJson(tpos)
        
        \* Lastly, you may build expression over arbitrary sets of states by
        \* leveraging the _TETrace operator.  For example, this is how to
        \* count the number of times a spec variable changed up to the current
        \* state in the trace.
        \* ,_tposModCount |->
        \*     LET F[s \in DOMAIN _TETrace] ==
        \*         IF s = 1 THEN 0
        \*         ELSE IF _TETrace[s].tpos # _TETrace[s-1].tpos
        \*             THEN 1 + F[s-1] ELSE F[s-1]
        \*     IN F[_TEPosition - 1]
    ]

=============================================================================
---- MODULE EWD840_TTrace_1620775755 ----
EXTENDS TLCExt, Toolbox, Naturals, TLC, EWD840, Json

_expression ==
    LET EWD840_TEExpression == INSTANCE EWD840_TEExpression
    IN EWD840_TEExpression!expression
----

_trace ==
    LET EWD840_TETrace == INSTANCE EWD840_TETrace
    IN EWD840_TETrace!trace
----

_prop ==
    ~(([]<>(
            color = ((0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"))
            /\
            tpos = (1)
            /\
            tcolor = ("black")
            /\
            active = ((0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE))
    ))/\([]<>(
            color = ((0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"))
            /\
            tpos = (0)
            /\
            tcolor = ("black")
            /\
            active = ((0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE))
    )))
----

_init ==
    /\ tpos = _TETrace[1].tpos
    /\ active = _TETrace[1].active
    /\ tcolor = _TETrace[1].tcolor
    /\ color = _TETrace[1].color
----

_action ==
    /\ \E i,j \in DOMAIN _TETrace:
        /\ \/ j = i + 1
           \/ /\ i = 23
              /\ j = 2
        /\ tpos  = _TETrace[i].tpos
        /\ tpos' = _TETrace[j].tpos
        /\ active  = _TETrace[i].active
        /\ active' = _TETrace[j].active
        /\ tcolor  = _TETrace[i].tcolor
        /\ tcolor' = _TETrace[j].tcolor
        /\ color  = _TETrace[i].color
        /\ color' = _TETrace[j].color

=============================================================================
---- MODULE EWD840_TETrace ----
EXTENDS TLC, EWD840

trace == 
    <<
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 0,tcolor |-> "black",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 0,tcolor |-> "black",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 3,tcolor |-> "white",active |-> (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 3,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 3,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 2,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 1,tcolor |-> "black",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "black" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 0,tcolor |-> "black",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 4,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 3,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> FALSE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 3,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 2,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 2,tcolor |-> "white",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE)]),
    ([color |-> (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white" @@ 4 :> "white"),tpos |-> 1,tcolor |-> "black",active |-> (0 :> TRUE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE @@ 4 :> TRUE)])
    >>
=============================================================================
---- CONFIG EWD840_TTrace_1620775755 ----
CONSTANTS  N = 5
PROPERTY _prop
CHECK_DEADLOCK FALSE
INIT  _init
NEXT Next \* Next from the original spec
ACTION_CONSTRAINT _action
CONSTANT _TETrace <- _trace
ALIAS _expression
====

[konnov]

Sure, it should not be much different. However a trace predicate makes a difference to us, as we construct this predicate, check it and forget about the constraint. See #822. The explicit approach would require us to carry the trace constraints all the time.