RFC006: Framework for unit-testing #817
Replies: 1 comment 5 replies
-
|
@lemmy wrote in #741 (comment):
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
=============================================================================== |
Beta Was this translation helpful? Give feedback.
-
|
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 TraceInv ==
/\ x > 0 => x' >= x
/\ x < 0 => x' <= x |
Beta Was this translation helpful? Give feedback.
-
|
Yes, we have just added support for action invariants over two states, see #816. Trace invariants are just a natural extension of it.
I have an impression that making a Swiss knife out of everything makes it hard for the users to discover reasonable use 8000 cases. |
Beta Was this translation helpful? Give feedback.
-
I consider myself in good company: https://twitter.com/MSFTResearch/status/1392183384772943872 ;-) |
Beta Was this translation helpful? Give feedback.
-
|
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 ---- 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
==== |
Beta Was this translation helpful? Give feedback.
-
|
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. |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
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.
Beta Was this translation helpful? Give feedback.
All reactions