RFC006: proposal on unit-testing and property-based testing for TLA+ #741

konnov · 2021-04-15T18:27:13Z

This is an RFC to discuss unit testing and PBT for TLA+. Once we agreed on that internally, we should get the feedback from a wider audience.

Compiled version in pdf.

To see the code in the RFC, run the following:

git clone https://github.com/informalsystems/apalache -b igor/rfc-unit && cargo install mdbook \
  && cd apalache/docs && mdbook serve

~~Tests added for any new code~~
~~Ran make fmt-fix (or had formatting run automatically on all files edited)~~
Documentation added for any new functionality
Entry added to UNRELEASED.md for any new functionality

vitorenesduarte

It's great to see this! I'll do another pass later, but here are some initial comments. I really like the idea of apalache-mc example!!

docs/src/adr/006rfc-unit-testing.md

test/tla/ChangRobertsTyped_Test.tla

vitorenesduarte · 2021-04-15T19:31:49Z

test/tla/ChangRobertsTyped_Test.tla

+    \* restrict the contents with TypeOK,
+    \* so we don't generate useless data structures
+    /\ TypeOK


Would it make sense to have a way to define generators that are useful and then invoke them here?

Can you elaborate? Do you want to have generators in TypeOK?

vitorenesduarte · 2021-04-15T19:32:04Z

test/tla/ChangRobertsTyped_Test.tla

+\* Note that succ(n) is not referring to state variables,
+\* so we can test it in isolation.
+\*
+\* @testStateless


Could we go with @test instead of @testStateless? Or do we predict that @test could be used in the future for something else?

I don't know. I think this is actually a rare case, when we have a stateless operator. When I was writing this text, it was not even clear to me, why cannot we directly tag succ with @require and @ensure.

In the MBT for IBC, we have a single module changing the state: IBC
The remaining modules (ICS02 and ICS03) only contain stateless operators that are then invoked by the IBC one.

I don't know if this is a common idiom, however.

It's reasonable to expect that people would write larger specs like this. So far, I have not seen it often. It may also be a difference between people who come from imperative and functional languages.

vitorenesduarte · 2021-04-15T19:32:14Z

test/tla/ChangRobertsTyped_Test.tla

+(*
+ * A test setup for ChangRobertsTyped.
+ *)
+EXTENDS Integers, Apalache


Why do we need to import Apalache?

We are using Gen, which is defined in Apalache. If you are not using Gen, you would not need it.

Co-authored-by: Vitor Enes <vitorenesduarte@gmail.com>

konnov · 2021-04-16T10:46:46Z

I have added a section on testing executions

vitorenesduarte · 2021-04-16T13:15:28Z

test/tla/ChangRobertsTyped_Test.tla

+(*************************** EXECUTION TESTS **********************************)
+\* Execute a sequence of 5 actions, similar to TestAction_n0.
+\* We test a final state with Assert_n0.
+\* Additionally, every state in an execution is tested for Correctness.
+\*
+\* @require("ConstInit")
+\* @require("Prepare_n0")
+\* @invariant("Correctness")
+\* @ensure("Assert_noWinner")
+\* @testExecution(5)
+TestExec_n0_n1 ==
+    \* in this test, we only execute actions by processes 1 and 2
+    \E self \in { 1, 2 }:
+        n0(self) \/ n1(self)


I really like this idea!

I wonder if it would be possible to somehow write the following:

IfExec(trace) == /\ trace[0].action.name = "create_client" /\ trace[0].action.id = 1 /\ trace[0].action.height = 3 /\ trace[1].action.name = "update_client" /\ trace[1].action.id = 1 /\ trace[1].action.height = 2 ThenExec(trace) == /\ trace[0].outcome = "ok" /\ trace[1].outcome = "invalid_height" \* @require("IfExec") \* @ensure("ThenExec") \* @testExecution(2, "Init", "Next") \* the execution doesn't have to start at `Init`; \* instead, the execution can start from any state reachable from `Init` by applying `Next`

I don't think I'm using @require and @ensure correctly (i.e. as in the other examples), but I believe that it conveys the idea.

If something like this was supported, it could probably also be used to generate MBT tests in a much nicer way.

Do you like to refer to the intermediate states in a trace? The idea was the you can talk about the variables of the first state and the last state. Otherwise, we are quickly approaching temporal logic :)

@andrey-kuprianov what is your take on that? How far is it from the tests you need in MBT?

Do you like to refer to the intermediate states in a trace?

Yes. My example is bad in that sense. I should have used a trace with more than 2 states.

I think @shonfeder and you are asking about more or less the same thing. I don't like the idea of having trace explicitly. I guess what you are asking for is a temporal property. Instead of giving an explicit index, we could write A /\ []B /\ <>C. This would be the syntax for advanced users :-)

Related: Trace operator in CommunityModules https://github.com/tlaplus/CommunityModules/blob/4337afb74653cedcc2a24107759bf1613812db34/modules/TLCExt.tla#L42-L56

Also seems related to state- and action-constraints.

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.

I am also not sure what to do about the primed and unprimed variables in this test. It would be nice to make it less of a hack.

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. ✊

shonfeder

Exciting stuff! Our discussion with @istoilkovska today seems to really confirm the utility of this stuff.

I posed some questions, just to help us consider different angles.

docs/src/adr/006rfc-unit-testing.md

shonfeder · 2021-04-16T15:25:30Z

test/tla/ChangRobertsTyped_Test.tla

+\* @require("ConstInit")
+\* @require("Prepare_n0")
+\* @ensure("Assert_n0")
+\* @testAction
+TestAction_n0 ==
+    \E self \in Node:
+        n0(self)


Is it impossible to express this effectively without the require and ensure annotations? E.g., is it impossible for this to be expressed as something like?

TestAction_n0 == /\ Require(ConstInit) /\ Require(Prepare_n0) /\ \E self \in Node: n0(self) /\ Ensure(Assert_n0)

I ask because, imo, it's generally not great when a parallel system of annotations starts to emerge, and preferable to express things within the language as much as possible. Of course, if it's really essential, then worth pursuing.

If it is essential, we should maybe work out a coherent syntax for the annotations. E.g., the annotations here don't really fit with the type annotations: here we're missing a trailing ; and we use a quoted argument, rather than a colon an unquoted term.

If it is essential, we should maybe work out a coherent syntax for the annotations. E.g., the annotations here don't really fit with the type annotations: here we're missing a trailing ; and we use a quoted argument, rather than a colon an unquoted term.

We have two kinds of syntax for single-argument string annotations: https://apalache.informal.systems/docs/adr/004adr-annotations.html

I ask because, imo, it's generally not great when a parallel system of annotations starts to emerge, and preferable to express things within the language as much as possible. Of course, if it's really essential, then worth pursuing.

I know what you mean. Several times we tried to express a DSL in TLA+ itself, and it happened to be a disaster. I think there are two reasons for that: (1) TLA+ is not an imperative language, (2) formulas have a very flexible structure, so it is tempting to combine things in unexpected ways.

Another reason for having @require and @ensure in annotations is that you can see them like that in contracts for verification tools, e.g., see Dafny, Ivy, VeriFast. So I am just copying what works well :-)

I see! Thanks for explaining. This seems well motivated to me.

I'd be in favor of adding a section to the RFC to record the motivation for putting this in annotations instead of as a DSL.

shonfeder · 2021-04-16T15:53:44Z

test/tla/ChangRobertsTyped_Test.tla

+\* @require("Prepare_n0")
+\* @invariant("Correctness")
+\* @ensure("Assert_noWinner")
+\* @testExecution(5)


again, I think we can probably settle on either having to quote args or not? If ConstInit is an operator name, then it shouldn't be a string, right? Or else, what happens when we want to supply a string to one of these annotations?

True, annotations are another layer. Some languages support contracts right in the language, e.g., Scala has requires as part of the language. Maybe one day TLA+ will have it too, but for the moment annotations would work too.

I think this reply may have meant for a different comment? (But I am convinced :))

shonfeder · 2021-04-16T15:54:39Z

test/tla/ChangRobertsTyped_Test.tla

+\*
+\* @require("ConstInit")
+\* @require("Prepare_n0")
+\* @invariant("Correctness")


With the invariants in particular, couldn't this just be in the body of the operator as well?

I will add a discussion on that in the document. The problem is that all of these annotations can be written directly in TLA by writing temporal formulas. However, this often leads to confusion. Moreover, people start writing very powerful formulas right away. What we need in a test: (1) How to initialize the system, (2) what to execute, (3) what to check. Decomposing a formula into these three components is surprisingly hard, unless people are following a very rigid syntax, which nobody wants to follow.

This is a good reason. Let's do record these motivations, along with #741 (comment) into the RFC>

shonfeder · 2021-04-16T15:57:07Z

test/tla/ChangRobertsTyped_Test.tla

+\* @testExecution(5)
+TestExec_n0_n1 ==
+    \* in this test, we only execute actions by processes 1 and 2
+    \E self \in { 1, 2 }:


Here I'm wondering why we are not using Gen or aren't putting this constraint in a Prepare prerequisite. Not that those would be better, but it seems to me that we have like 3 different ways of accomplishing the same thing? If that's right, I think it'd be good to clarify which way is the preferred one and why. If not, it might help (at least a noob like me) to provide a paragraph justifying why we need these three different ways of stating constraints.

Gen is a bit of a hack for testing. I just realized that it is not explained in the document at all.

shonfeder · 2021-04-16T16:03:13Z

docs/src/adr/006rfc-unit-testing.md

+[Property-based testing]: https://en.wikipedia.org/wiki/QuickCheck
+[TLA+ examples]: https://github.com/tlaplus/Examples/
+[LCR]: https://github.com/tlaplus/Examples/tree/master/specifications/chang_roberts
+[ChangRobertsTyped_Test.tla]: ../../../test/tla/ChangRobertsTyped_Test.tla


I think this should be a link to the file hosted by github, otherwise the link will be broken when this is served from the generated site.

Good point. I will have to update the link, once this PR is merged.

Co-authored-by: Shon Feder <shon@informal.systems>

konnov · 2021-04-20T15:53:00Z

I have pushed more explanations. The discussions section is not finished yet. Also, added a pdf version of the file, so it is easy to read

konnov · 2021-04-21T09:49:32Z

Added discussions on the issues raised by @shonfeder and I guess also by @vitorenesduarte

shonfeder · 2021-04-21T13:14:26Z

docs/src/adr/006rfc-unit-testing.md

+
+In the rest of this section, we comment on the alternative approaches.
+
+#### 3.5.1. But I can do all of that in TLA+ 


These sections make the particular feature set and approach very well motivated, IMO. Thanks for adding them!

I was actually surprised how hard it was to express such a simple test in a dedicated operator, instead of creating a test in a separate file.

konnov · 2021-04-26T11:29:48Z

@andrey-kuprianov do you like to comment on this RFC? My plan was to post it on reddit, to see if TLA+ users would like to see a testing framework like that.

Isaac-DeFrain · 2021-04-26T13:06:11Z

@konnov you'll probably have better luck emailing the google group, I have not found many TLA+ people on Reddit

konnov · 2021-04-26T13:33:58Z

@Isaac-DeFrain, yeah, the tla mailing list too. I just want to do it in stages, so we don't get a storm of replies :)

konnov · 2021-05-08T19:12:54Z

Let's continue the discussion in #817

add RFC006

7f022bb

konnov requested review from vitorenesduarte, shonfeder, Kukovec and andrey-kuprianov April 15, 2021 18:27

konnov added 2 commits April 15, 2021 20:27

add entry in UNRELEASED

5b59ab4

fix the tests

c97c0e1

vitorenesduarte reviewed Apr 15, 2021

View reviewed changes

konnov and others added 4 commits April 16, 2021 11:06

Update docs/src/adr/006rfc-unit-testing.md

0585be9

Co-authored-by: Vitor Enes <vitorenesduarte@gmail.com>

Update docs/src/adr/006rfc-unit-testing.md

4fb4ccd

Co-authored-by: Vitor Enes <vitorenesduarte@gmail.com>

Update test/tla/ChangRobertsTyped_Test.tla

23e1542

Co-authored-by: Vitor Enes <vitorenesduarte@gmail.com>

one more section on testing executions

c47c618

konnov requested a review from istoilkovska April 16, 2021 12:19

vitorenesduarte reviewed Apr 16, 2021

View reviewed changes

shonfeder reviewed Apr 16, 2021

View reviewed changes

konnov and others added 3 commits April 16, 2021 20:13

Update docs/src/adr/006rfc-unit-testing.md

825c62e

Co-authored-by: Shon Feder <shon@informal.systems>

restructuring and addressing comments

38de069

update on generators

298772c

konnov requested a review from romac April 20, 2021 16:24

added discussions

1228814

shonfeder approved these changes Apr 21, 2021

View reviewed changes

konnov added 6 commits April 21, 2021 15:50

a few fixes

6c886fb

no useless quotes

114e032

added test options

db9c25f

the pdf version

4a2474f

Merge branch 'unstable' into igor/rfc-unit

d5e8358

mention rfc 006

b86d08b

konnov added 6 commits April 23, 2021 09:16

fix the ChangRobertsTyped_Test

a24e86c

Merge branch 'unstable' into igor/rfc-unit

1017157

bring back the quotes, for annotation parser to work

764ca05

Merge branch 'igor/rfc-unit'

124cd5b

fixed the quotes

e9b201d

Merge branch 'unstable' into igor/rfc-unit

4b128eb

konnov mentioned this pull request Apr 26, 2021

[FEATURE] Allow identifiers in annotations #768

Closed

konnov added 5 commits April 27, 2021 17:40

remove the reference to Dr. Malcolm :)

40662ff

Merge branch 'unstable' into igor/rfc-unit

3872bd4

fix formatting

262ad7e

Merge branch 'unstable' into igor/rfc-unit

3286296

using operator names in annotations, instead of strings

542dc20

konnov merged commit 4f73a46 into unstable Apr 27, 2021

konnov deleted the igor/rfc-unit branch April 27, 2021 17:46

apalache-bot mentioned this pull request May 3, 2021

[release] 0.15.4 #792

Merged


		In the rest of this section, we comment on the alternative approaches.

		#### 3.5.1. But I can do all of that in TLA+

RFC006: proposal on unit-testing and property-based testing for TLA+ #741

RFC006: proposal on unit-testing and property-based testing for TLA+ #741

Conversation

konnov commented Apr 15, 2021 • edited Loading

vitorenesduarte left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vitorenesduarte Apr 16, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented Apr 16, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lemmy May 4, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder Apr 19, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder Apr 16, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented Apr 20, 2021

konnov commented Apr 21, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented Apr 26, 2021

Isaac-DeFrain commented Apr 26, 2021

konnov commented Apr 26, 2021

konnov commented May 8, 2021

konnov commented Apr 15, 2021 •

edited

Loading

vitorenesduarte Apr 16, 2021 •

edited

Loading

lemmy May 4, 2021 •

edited

Loading

shonfeder Apr 19, 2021 •

edited

Loading

shonfeder Apr 16, 2021 •

edited

Loading