Level finder #811

konnov · 2021-05-06T12:57:05Z

This PR implements computation of TLA+ levels (that are described in Specifying Systems). In a nutshell, a TLA+ expression is assigned one of the four levels:

Level 0: the expression is only using constants.
Level 1: the expression is using constants, state variables, but no action or temporal operators.
Level 2: the expression is using action operators, but no temporal operators.
Level 3: the expression using temporal operators.

The concept of levels may be reused in other code. That's why it is placed in tlair. The code in this PR is required in #810.

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

shonfeder

A few suggestions, but looks good to me overall.

shonfeder · 2021-05-06T17:16:12Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala

+    case OperEx(op, args @ _*)
+        if op == TlaActionOper.prime || op == TlaActionOper.enabled
+          || op == TlaActionOper.unchanged || op == TlaActionOper.stutter
+          || op == TlaActionOper.nostutter || op == TlaActionOper.composition =>
+      TlaLevelAction.join(args.map(find))
+
+    case OperEx(op, args @ _*)
+        if op == TlaTempOper.box || op == TlaTempOper.diamond || op == TlaTempOper.leadsTo
+          || op == TlaTempOper.weakFairness || op == TlaTempOper.strongFairness
+          || op == TlaTempOper.guarantees || op == TlaTempOper.AA || op == TlaTempOper.EE =>
+      TlaLevelTemporal.join(args.map(find))
+
+    case OperEx(_, args @ _*) =>
+      TlaLevelConst.join(args.map(find))


It could just be a matter of taste, but IMO this approach is a bit easier to read (assuming it's feasible):

Suggested change

case OperEx(op, args @ _*)

if op == TlaActionOper.prime || op == TlaActionOper.enabled

|| op == TlaActionOper.unchanged || op == TlaActionOper.stutter

|| op == TlaActionOper.nostutter || op == TlaActionOper.composition =>

TlaLevelAction.join(args.map(find))

case OperEx(op, args @ _*)

if op == TlaTempOper.box || op == TlaTempOper.diamond || op == TlaTempOper.leadsTo

|| op == TlaTempOper.weakFairness || op == TlaTempOper.strongFairness

|| op == TlaTempOper.guarantees || op == TlaTempOper.AA || op == TlaTempOper.EE =>

TlaLevelTemporal.join(args.map(find))

case OperEx(_, args @ _*) =>

TlaLevelConst.join(args.map(find))

case OperEx(op, args @ _*) =>

val ctor = op match {

case TlaActionOper.prime | TlaActionOper.enabled

| TlaActionOper.unchanged | TlaActionOper.stutter

| TlaActionOper.nostutter | TlaActionOper.composition => TlaLevelAction

case TlaTempOper.box | TlaTempOper.diamond

| TlaTempOper.leadsTo | TlaTempOper.weakFairness

| TlaTempOper.strongFairness | TlaTempOper.guarantees

| TlaTempOper.AA | TlaTempOper.EE => TlaLevelTemporal

case _ => TlaLevelConst

}

ctor.join(args.map(find))

Good point. I think I will just introduce a map.

shonfeder · 2021-05-06T17:17:27Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala

+    case _ =>
+      TlaLevelConst


Could this catchall come back to bite us if new expressions are introduced? Would it be worth while to explicitly enumerate the other constructors here instead of having a wildcard?

I doubt that, as the types of expressions were stable for long time.

shonfeder · 2021-05-06T17:23:17Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala

+
+      case TlaOperDecl(name, _, _) =>
+        cacheLevel(Set(name), name)
+        levelCacheMap(name)


Given that we are caching results, why don't we first check whether the name is cached before we try to add it to the cache?

yep, added that

shonfeder · 2021-05-06T17:32:04Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala

+      case TlaConstDecl(_) =>
+        TlaLevelConst
+
+      case TlaVarDecl(_) =>
+        TlaLevelState
+
+      case TlaAssumeDecl(_) =>
+        TlaLevelConst
+


unless I missunderstand, it seems like where checking for this and then determining the level in two parallel ways, Once here by pattern matching, and once when we construct the level finder, when we cache to the various sets. Couldn't we handle all of this logic with the _.contains checks and the caching lookup?

The code in apply is also handling the cases of ASSUME and THEOREM. Also, this code avoids an extra lookup in defs, consts and vars (but that's not the main point).

What happens if I write an assume declaration with primes?

SANY will tell you that it does not like your spec. I found that out a couple of months ago :D

It will even complain if you use state variables in ASSUME.

Ok, what about the expression (1 + 1)' outside of assume? Just because it has a prime operator, does not mean its level isn't 0.

Well, syntactically (1 + 1)' is level 2. Semantically, it is level 0. It looks like the book is not precise about whether we should compute the levels semantically or syntactically.

shonfeder · 2021-05-06T17:36:11Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala

+  }
+
+  /**
+   * Join the levels by computing the smallest level that covers both of `this` and `that`.


I'm surprised that joining gives the least, rather than greatest level. Is this because its actually more difficult to handle , e.g., constants than handling temporal formulas?

no-no, it's actually the maximum of the two levels, just badly formulated

shonfeder · 2021-05-06T17:40:26Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala

+  private val INT_TO_LEVEL = Seq(TlaLevelConst, TlaLevelState, TlaLevelAction, TlaLevelTemporal)
+
+  def fromInt(level: Int): TlaLevel = {
+    if (level < 0 || level >= INT_TO_LEVEL.length) {
+      throw new IllegalArgumentException(s"Unexpected level of TlaValue: $level")
+    } else {
+      INT_TO_LEVEL(level)
+    }
+  }


Since we already have the Int values inhe Const objects, why not just have fromInt give level.level? It seems like this duplicates the logic: we record the int once as a position in the sequence and another time explicitly in the level attribute.

Good point. Fixed that.

Kukovec

LGTM

Kukovec · 2021-05-06T18:30:24Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala

+  private val INT_TO_LEVEL = Seq(TlaLevelConst, TlaLevelState, TlaLevelAction, TlaLevelTemporal)
+
+  def fromInt(levelNo: Int): TlaLevel = {
+    INT_TO_LEVEL.find(_.level == levelNo) match {


Minor gripe,I would use an indexed collection and do boundary tests here, instead of find.

I've replaced it with find, which should be ok for a list of 4 elements

Ha-ha. My solution was exactly as you suggest, and @shonfeder did not like it :P

konnov added 3 commits May 6, 2021 14:30

add tla levels and pbt tests for them

895b94f

add TlaDeclLevelFinder and property-based tests for it

546042d

remove tla-script from this branch

ed6ded1

konnov requested review from shonfeder and Kukovec May 6, 2021 12:57

konnov added 2 commits May 6, 2021 18:37

Merge branch 'unstable' into igor/levels

4d40613

entry in unreleased

c14b828

shonfeder approved these changes May 6, 2021

View reviewed changes

konnov added 3 commits May 6, 2021 19:59

introduced a map of levels

c57de8a

more logical cache lookup

a001410

addressing comments by Shon

36faf8c

konnov enabled auto-merge (squash) May 6, 2021 18:19

konnov merged commit 95ebc85 into unstable May 6, 2021

Kukovec approved these changes May 6, 2021

View reviewed changes

konnov deleted the igor/levels branch May 6, 2021 18:41

apalache-bot mentioned this pull request May 10, 2021

[release] 0.15.5 #818

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Level finder #811

Level finder #811

konnov commented May 6, 2021 •

edited

Loading

shonfeder left a comment

shonfeder May 6, 2021

konnov May 6, 2021

shonfeder May 6, 2021

konnov May 6, 2021

shonfeder May 6, 2021

konnov May 6, 2021

shonfeder May 6, 2021

konnov May 6, 2021

Kukovec May 6, 2021

konnov May 6, 2021

konnov May 6, 2021

Kukovec May 6, 2021

konnov May 6, 2021

shonfeder May 6, 2021

konnov May 6, 2021

shonfeder May 6, 2021

konnov May 6, 2021

Kukovec left a comment

Kukovec May 6, 2021

konnov May 6, 2021 •

edited

Loading

konnov May 6, 2021

Level finder #811

Level finder #811

Conversation

konnov commented May 6, 2021 • edited Loading

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

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

Kukovec left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov May 6, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented May 6, 2021 •

edited

Loading

konnov May 6, 2021 •

edited

Loading