Introduce runs #348

konnov · 2022-11-18T15:49:32Z

Closes #344. This PR introduces the concept of a run, which is not explicitly present in TLA+. I kind of skipped the discussions and ADR phase here and went straight to extending the manual and implementing the new operators in the simulator. By doing so, I have iterated several times on the syntax. After all, we have:

a new definition qualifier called run, not supported by the effects checker yet.
a new mode called Run, similar to the modes Action and Temporal.
Three Run operators:
- A.then(B) is sequential composition of A and then B.
- ~~i.times(A)~~ A.repeated(i) is sequential composition of A exactly i times.
- assert(P) tests P and produces a runtime error, if P evaluates to false.

Kukovec · 2022-11-18T16:02:02Z

I kind of skipped the discussions and ADR phase here and went straight to extending the manual and implementing the new operators in the simulator

Rules for thee, but not for me?

Kukovec · 2022-11-18T16:03:25Z

Also, the diff is 2.5 kLOC, can you please make a note as to which files are autogen/trivially changed so I can ignore them?

konnov · 2022-11-18T16:08:48Z

Also, the diff is 2.5 kLOC, can you please make a note as to which files are autogen/trivially changed so I can ignore them?

Feel free to ignore everything in generated but Tnt.g4, which is the grammar.

bugarela · 2022-11-21T10:05:33Z

doc/lang.md


 The following operator is similar to `[A]_x` of TLA+:

 ```scala
-stutter(A, x)
-A.stutter(x)
+orKeep(A, x)


Is there a scenario where someone wants to stutter over variables that are different from the set of variables being updated by the action A? I can't event understand what that would mean.

If x is always the set of variables being updated by A, WDYT about getting rid of the argument? Then we can call the operators something like optionally(A).

That's a good point. TLA+ has variables in [A]_vars, since there are no explicit assignments there. Factored it out in a separate issue, since the stuttering operators were already in the manual before: #354

bugarela · 2022-11-21T10:12:06Z

doc/lang.md


 The following operator is similar to `<A>_x` of TLA+:

 ```scala
-nostutter(A, x)
-A.nostutter(x)
+mustChange(A, x)


This looks like an expectation (like in a testing framework). WDYT of A.changing(x)?

If we remove variables in the stuttering operator, we should also remove them in this one, as this one is the negation of stuttering.

It is not exactly a negation. [A]_x is defined as A \/ x' = x and <A>_x is defined as A /\ x' # x. This second one I can see being used with a set of vars different then the set of vars being defined by A, as it can constrain A even further.

Correct. I am just saying that <A>_x was introduced as a dual of [A]_x. You are probably right that it does not make a lot of sense in the presence of effects and the requirement that all variables should be touched.

sutter/nostutter have the benefit of being clearly dual. OrKeep and MustChange have no such obvious relation in their names, IMO.

I don't know what motivates the change in names here, but I think we should at least keep the names related. So maybe something like

noChanges/changes

orKeep / noKeep (I don't like these)

?

Let's postpone this for #354

These operators are not used in specs yet, so there is no rush to pick a perfect name in this PR.

bugarela · 2022-11-21T10:16:28Z

examples/counters.tnt

+  // execute Init and then Next ten times, while asserting n < 5
+  run run4 = {
+    Init.then(10.times(all {
+      assert(n < 5),


Can you explain the motivation for adding assert? It seems like a way of reporting counterexamples, but I don't think this should be done at the language level.

Yeah, it looks like the only convenient way of specifying a failing test as a run. The expectation is basically that the run should go through, unless the assertion fails somewhere. I don't like asserts in TLC. We probably can live with asserts in the runs. But it would be great to have something better than asserts.

bugarela · 2022-11-21T10:19:07Z

tntc/src/effects/builtinSignatures.ts

+  { name: 'then', effect: '(Read[r1] & Update[u1], Read[r2] & Update[u2]) => Read[r1] & Update[r2]' },
+  { name: 'times', effect: '(Read[], Read[r] & Update[u]) => Read[r] & Update[r]' },
+  { name: 'assert', effect: '(Read[r]) => Read[r]' },


I'll have to update those to produce a Run effect, right? So we can't use those in other types of definitions that are not runs.

Yes, exactly. I did not know how to do that :)

thpani

In the end, we will have a model-checker written in TNT 😂

I've only read the language docs, I like the approach! Haven't reviewed the code.

doc/lang.md

thpani · 2022-11-21T10:33:40Z

doc/lang.md

+non-negative). If you want to repeat `A` from `i` to `j` times, you can combine
+it with `orKeep` as follows:
+
+```scala
+i.times(A).then((j - i).times(A.orKeep(vars)))


Would it make sense to promote this to a closure operator?

I was also thinking about doing that, but then what would be the difference between closure and always on finite prefixes?

Good point :)

doc/lang.md

Kukovec · 2022-11-21T12:26:00Z

doc/lang.md

+The operator `times` has the following syntax:
+
+```scala
+n.times(A)
+times(n, A)
+```


Could this lead to confusion with the set product operator? Maybe repeat is a better name.

good point. I copied this name from ruby, which reads very nice, e.g., five times A.

I will rename it to A.repeated(n).

Are you still planning to make this change? I agree that times could be confusing.

Yes, it is called repeated now

tntc/src/effects/builtinSignatures.ts

Kukovec · 2022-11-21T12:32:19Z

Also, like Thomas, I've just read the language part.

tntc/src/effects/builtinSignatures.ts

Co-authored-by: Kukovec <[email protected]> Co-authored-by: Thomas Pani <[email protected]>

Co-authored-by: Gabriela Moreira <[email protected]>

konnov · 2022-11-23T14:20:00Z

@shonfeder, for some reason I am getting this error on MacOS (zsh):

npm run integration
...
TAP version 13
0..0
not ok 0 'exit': unknown command type
  ---
  location: |
    line 26
  supported commands:
    - program
    - in
    - out
    - err
    - check
  ---

# FAILED TO PARSE TESTS

shonfeder · 2022-11-23T14:22:29Z

@konnov is your worktree clean? The mac tests are passing in CI.

konnov · 2022-11-23T14:35:28Z

@konnov is your worktree clean? The mac tests are passing in CI.

Actually, npm install -g txm helped! I had an older version.

konnov · 2022-11-23T14:41:28Z

I think I have addressed the issues, except for stuttering, which is factored out into another issue. Anybody wants to review?

shonfeder · 2022-11-23T14:44:04Z

Maybe these are more helpful debugging ideas:

Is the failure happening when running txm cli-tests.md or txm io-cli-tests.md or both?
What is the content of the failing file?

Given the error message, I'm wondering if you'll find something like

<!-- !test type ... -->
    ....

konnov · 2022-11-23T14:46:16Z

Maybe these are more helpful debugging ideas:

Is the failure happening when running txm cli-tests.md or txm io-cli-tests.md or both?

What is the content of the failing file?

Given the error message, I'm wondering if you'll find something like

    ....

It's all good. The older version of txm did not support test exit, which was introduced in io-cli-tests.md.

shonfeder · 2022-11-23T15:01:26Z

I see! Hopefully there is a way we can pin the version of our dev deps so we can automate away these kinds of issues in the future.

This should help avoid friction due to incompatible versions in our toolchain in the future. See, e.g., #348 (comment)

bugarela · 2022-11-23T18:34:07Z

Weird, I could swear that I had done this before (pinning the version in package.lock so we don't require a global installation). I was actually questioning why it wasn't working, but it seems like my change never made it through main or was reverted somehow.

Thanks for fixing this, @shonfeder!

konnov · 2022-11-24T11:14:25Z

Does anybody have cycles to get this merged? :)

shonfeder · 2022-11-25T13:15:39Z

Does anybody have cycles to get this merged? :)

I'm reviewing now. Sorry for the delay.

shonfeder

Looks like at least one left-over change you meant to make in response to previous reviews? I also have a few questions and suggestions.

doc/lang.md

shonfeder · 2022-11-25T13:23:59Z

doc/lang.md

+The operator `times` has the following syntax:
+
+```scala
+n.times(A)
+times(n, A)
+```


Are you still planning to make this change? I agree that times could be confusing.

shonfeder · 2022-11-25T13:29:21Z

doc/lang.md

@@ -1646,33 +1770,33 @@ keeping this operator.
 to identify assignments in actions. We introduced `Unchanged` only in the
 Temporal mode, which is needed for refinements.

-#### Stutter
+#### OrKeep


Why is this being renamed? Seems likely to introduce more confusion imo. "Stutter" already has a lot of docs around it in TLA+, and is specific and unusual enough no one is likely to confuse its meaning for something they already know.

But OrKeep could evoke other associations (related to disjunction, maybe intuitions about processing collections etc.) and users will lose the benefit of finding docs on TLA suttering when they search for it.

shonfeder · 2022-11-25T13:32:57Z

doc/lang.md


 The following operator is similar to `<A>_x` of TLA+:

 ```scala
-nostutter(A, x)
-A.nostutter(x)
+mustChange(A, x)


sutter/nostutter have the benefit of being clearly dual. OrKeep and MustChange have no such obvious relation in their names, IMO.

I don't know what motivates the change in names here, but I think we should at least keep the names related. So maybe something like

noChanges/changes

orKeep / noKeep (I don't like these)

?

shonfeder · 2022-11-25T13:34:21Z

examples/counters.tnt

+  run run1 = {
+    (n <- 1)
+      .then(n <- 2)
+      .then(n <- 3)
+      .then(n <- 6)
+      .then(n <- 3)
+  }


Quite cool.

How soon before users will want to be able to do:

run run1 = { n <- 1; n <- 2; n <- 6; n <- 3; }

:D

Yes, that's why we have then :)

tntc/src/runtime/impl/compilerImpl.ts

Co-authored-by: Shon Feder <[email protected]>

konnov · 2022-11-29T11:24:08Z

I think I have implemented all the required changes and introduced a follow-up issue on stuttering operators.

shonfeder · 2022-11-29T11:42:15Z

Awesome! I can’t wait to play with this feature :)

konnov added 5 commits November 14, 2022 17:41

preliminary syntax of runs

1e57e35

add toc

f6368a2

add the syntax for runs, simulator implementation of then

04cfa29

finishing the update on runs

df1ea24

add counters.tnt to the tests

4a6fc24

konnov requested review from thpani, bugarela, shonfeder and Kukovec November 18, 2022 15:49

konnov added 2 commits November 18, 2022 16:53

Merge branch 'main' into igor/runs344

f627a79

fix the failing test

293a359

konnov added 2 commits November 18, 2022 17:14

update the section on the modes

a414775

update the feature table

5863619

bugarela reviewed Nov 21, 2022

View reviewed changes

thpani reviewed Nov 21, 2022

View reviewed changes

Kukovec reviewed Nov 21, 2022

View reviewed changes

bugarela reviewed Nov 21, 2022

View reviewed changes

tntc/src/effects/builtinSignatures.ts Outdated Show resolved Hide resolved

konnov mentioned this pull request Nov 22, 2022

Remove variables in the stuttering operators #354

Open

konnov and others added 6 commits November 22, 2022 16:59

Apply suggestions from code review

6b32e8e

Co-authored-by: Kukovec <[email protected]> Co-authored-by: Thomas Pani <[email protected]>

Apply suggestions from code review

928727d

Co-authored-by: Gabriela Moreira <[email protected]>

Merge branch 'main' into igor/runs344

ae711bc

generate the parser again

5802f72

fix the tests

2f649c4

rename times to repeated

b2757ae

shonfeder pushed a commit that referenced this pull request Nov 23, 2022

Pin txm as development dependency

6fb32df

This should help avoid friction due to incompatible versions in our toolchain in the future. See, e.g., #348 (comment)

shonfeder mentioned this pull request Nov 23, 2022

Pin txm as development dependency #356

Merged

Merge branch 'main' into igor/runs344

eafcd37

shonfeder suggested changes Nov 25, 2022

View reviewed changes

konnov and others added 3 commits November 28, 2022 11:54

Update doc/lang.md

0ec84cd

Co-authored-by: Shon Feder <[email protected]>

Update doc/lang.md

fc36647

Co-authored-by: Shon Feder <[email protected]>

addressed the comments by @shonfeder

81d7785

Merge branch 'main' into igor/runs344

1d4bacf

shonfeder approved these changes Nov 29, 2022

View reviewed changes

konnov merged commit 0b906d2 into main Nov 29, 2022

konnov deleted the igor/runs344 branch November 29, 2022 17:29

Introduce runs #348

Introduce runs #348

Conversation

konnov commented Nov 18, 2022 • edited Loading

Kukovec commented Nov 18, 2022

Kukovec commented Nov 18, 2022 • edited Loading

konnov commented Nov 18, 2022 • 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

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

Choose a reason for hiding this comment

thpani left a comment • 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov Nov 23, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Kukovec commented Nov 21, 2022

konnov commented Nov 23, 2022

shonfeder commented Nov 23, 2022

konnov commented Nov 23, 2022

konnov commented Nov 23, 2022

shonfeder commented Nov 23, 2022 • edited Loading

konnov commented Nov 23, 2022

shonfeder commented Nov 23, 2022

bugarela commented Nov 23, 2022

konnov commented Nov 24, 2022

shonfeder commented Nov 25, 2022

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

konnov commented Nov 29, 2022

shonfeder commented Nov 29, 2022

konnov commented Nov 18, 2022 •

edited

Loading

Kukovec commented Nov 18, 2022 •

edited

Loading

konnov commented Nov 18, 2022 •

edited

Loading

thpani left a comment •

edited

Loading

konnov Nov 23, 2022 •

edited

Loading

shonfeder commented Nov 23, 2022 •

edited

Loading