Added transformations for quantification over special integer sets #1431

Kukovec · 2022-03-02T16:00:27Z

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

First part of #1407, without the plumbing.

codecov-commenter · 2022-03-02T16:13:02Z

Codecov Report

Merging #1431 (325b56e) into unstable (b908195) will increase coverage by 0.03%.
The diff coverage is 93.75%.

@@             Coverage Diff              @@
##           unstable    #1431      +/-   ##
============================================
+ Coverage     74.57%   74.61%   +0.03%     
============================================
  Files           358      359       +1     
  Lines         11357    11373      +16     
  Branches        559      542      -17     
============================================
+ Hits           8470     8486      +16     
  Misses         2887     2887

Impacted Files	Coverage Δ
...alache/tla/pp/IntegerQuantificationOptimizer.scala	`93.75% <93.75%> (ø)`
...he/io/annotations/parser/CommentPreprocessor.scala	`93.97% <0.00%> (+1.20%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b908195...325b56e. Read the comment docs.

bugarela

LGTM, I just left some opinion/questions for the testing part.

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestQuantificationOptimizer.scala

shonfeder

A few small comments and suggestions, one one more substantive (but totally optional) suggestion about the organization of the logic in the transformation.

shonfeder · 2022-03-02T17:32:51Z

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

+ * This transformation rewrites expressions of the form `(\A | \E) x \in S: P`, where S is one of `Int`, `Nat`, `a..b`,
+ * into `(\A | \E) x: Q` (unbounded quantification).


Should this communicate that the rewriting generally moves the bounds from variable binding in the quantifier into constraints in the expression that is quantified over? iiuc, this is part of the key idea, not simply that that it produces unbounded quantification.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

shonfeder · 2022-03-02T18:51:04Z

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestQuantificationOptimizer.scala

+  test("Translation of Nat") {
+    val natSet = tla.natSet().as(SetT1(IntT1()))
+
+    forSetWithPredicates(Gen.const(natSet), postPredE, postPredA)
+  }
+
+  test("Translation of Int") {
+    val intSet = tla.intSet().as(SetT1(IntT1()))
+
+    forSetWithPredicates(Gen.const(intSet), postPredE, postPredA)
+  }
+
+  test("Translation of a..b") {
+    forSetWithPredicates(rangeGen, postPredE, postPredA)
+  }


What are the properties being tested for here? It's not clear to me from the names of the test. I can see that you are testing certain transformations, but it would help with readability of the tests IMO to include in the name what properties of the transformations are being checked for.

In my experience, the point of property based tests it to end up with something that looks like: "forall x: T. P(x)where theTis determined by generators of expressions of the appropriate type, andPis the test of what should hold of every instance ofx`. I am not really able to figure out whether that is happening in these tests in some way. Maybe after the fix discussed with Gabriela that will be clearer for me. I'll check back after those changes are int!

If you want the above formulation, P(ex) := transform((\E | \A) x \in S: p(ex)) = (\E | \A) x: q(ex),

Basically, does the transformation have the expected shape for Q

thpani

I like the implementation, only a few comments there.
The tests, I found rather difficult to follow. I think this can be resolved with some restructuring and renaming, see my comments inline.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

thpani · 2022-03-03T07:45:54Z

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

+ */
+
+@Singleton
+class IntegerQuantificationOptimizer(tracker: TransformationTracker) extends TlaExTransformation {


General question, do we have a naming scheme for these? I see both Optimizers and Simplifiers in the codebase, is there any difference?

Not really. IMO a simplifier translates an expression into another expression that is equivalent under certain conditions and structurally simpler. An optimizer may produce a more complex expression, which nevertheless improves performance.

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestQuantificationOptimizer.scala

konnov

Just a few comments, as there are good reviews already. I agree with Thomas that these transformations are not about optimizations. Maybe they are simplifications.

konnov · 2022-03-04T08:03:33Z

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

+ */
+
+@Singleton
+class IntegerQuantificationOptimizer(tracker: TransformationTracker) extends TlaExTransformation {


Not really. IMO a simplifier translates an expression into another expression that is equivalent under certain conditions and structurally simpler. An optimizer may produce a more complex expression, which nevertheless improves performance.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/IntegerQuantificationOptimizer.scala

shonfeder

LGTM!

Thank you for taking the time to add this feature in incrementally! :)

* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds * apalache-mc/apalache#425 * apalache-mc/apalache#1431 Github issue heidihoward#5 heidihoward#5 [Apalache] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds * apalache-mc/apalache#425 * apalache-mc/apalache#1431 Github issue #5 #5 [Apalache] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Added transformations for quantification over special integer sets

8ab0cf1

Kukovec requested review from thpani, konnov, bugarela and shonfeder March 2, 2022 16:00

bugarela approved these changes Mar 2, 2022

View reviewed changes

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestQuantificationOptimizer.scala Outdated Show resolved Hide resolved

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestQuantificationOptimizer.scala Outdated Show resolved Hide resolved

shonfeder reviewed Mar 2, 2022

View reviewed changes

thpani reviewed Mar 3, 2022

View reviewed changes

konnov approved these changes Mar 4, 2022

View reviewed changes

Kukovec added 3 commits March 4, 2022 12:14

PR comments

0803569

typo

670f7b2

Merge branch 'unstable' into jk/unboundedForms

047f9a2

shonfeder approved these changes Mar 4, 2022

View reviewed changes

Merge branch 'unstable' into jk/unboundedForms

325b56e

Kukovec enabled auto-merge (squash) March 4, 2022 14:04

Kukovec merged commit 6402105 into unstable Mar 4, 2022

shonfeder deleted the jk/unboundedForms branch March 4, 2022 15:30

konnov mentioned this pull request Dec 21, 2022

[FEATURE] Rewrite \E x \in a..b: p to \E x \in Int: a <= x /\ x <= b /\ p #1407

Open

lemmy mentioned this pull request Aug 19, 2024

Inductive invariant validation. heidihoward/pbft-tlaplus#6

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added transformations for quantification over special integer sets #1431

Added transformations for quantification over special integer sets #1431

Kukovec commented Mar 2, 2022

codecov-commenter commented Mar 2, 2022 •

edited

Loading

bugarela left a comment

shonfeder left a comment

shonfeder Mar 2, 2022

shonfeder Mar 2, 2022

shonfeder Mar 2, 2022

Kukovec Mar 2, 2022 •

edited

Loading

Kukovec Mar 2, 2022

thpani left a comment

thpani Mar 3, 2022

konnov Mar 4, 2022

konnov left a comment

konnov Mar 4, 2022

shonfeder left a comment

		* This transformation rewrites expressions of the form `(\A \| \E) x \in S: P`, where S is one of `Int`, `Nat`, `a..b`,
		* into `(\A \| \E) x: Q` (unbounded quantification).

Added transformations for quantification over special integer sets #1431

Added transformations for quantification over special integer sets #1431

Conversation

Kukovec commented Mar 2, 2022

codecov-commenter commented Mar 2, 2022 • edited Loading

Codecov Report

bugarela left a comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

shonfeder Mar 2, 2022

Choose a reason for hiding this comment

shonfeder Mar 2, 2022

Choose a reason for hiding this comment

shonfeder Mar 2, 2022

Choose a reason for hiding this comment

Kukovec Mar 2, 2022 • edited Loading

Choose a reason for hiding this comment

Kukovec Mar 2, 2022

Choose a reason for hiding this comment

thpani left a comment

Choose a reason for hiding this comment

thpani Mar 3, 2022

Choose a reason for hiding this comment

konnov Mar 4, 2022

Choose a reason for hiding this comment

konnov left a comment

Choose a reason for hiding this comment

konnov Mar 4, 2022

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

codecov-commenter commented Mar 2, 2022 •

edited

Loading

Kukovec Mar 2, 2022 •

edited

Loading