Level finder

UNRELEASED.md

@@ -14,6 +14,7 @@
 
 * Docker: Use openjdk-16 for the runtime in the app image, see #807
 * Documentation: Introduce TypeAlises operator convention, see #808
+* tlair: TlaExLevelFinder and TlaDeclLevelFinder to compute TLA+ levels, see #811
 
 ### Bug fixes
 

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

@@ -0,0 +1,59 @@
+package at.forsyte.apalache.tla.lir
+
+/**
+ * This class computes the level of a TLA+ declaration by using TlaExLevelFinder. See Lamport. Specifying Systems, p. 322.
+ *
+ * @param module a TLA module that contains the declarations to query
+ * @author Igor Konnov
+ */
+class TlaDeclLevelFinder(module: TlaModule) {
+  private val consts = Set(module.constDeclarations.map(_.name): _*)
+  private val vars = Set(module.varDeclarations.map(_.name): _*)
+  private val defs = Map(module.operDeclarations map { d => d.name -> d }: _*)
+  private var levelCacheMap: Map[String, TlaLevel] = Map()
+
+  def apply(decl: TlaDecl): TlaLevel = {
+    decl match {
+      case TlaConstDecl(_) =>
+        TlaLevelConst
+
+      case TlaVarDecl(_) =>
+        TlaLevelState
+
+      case TlaAssumeDecl(_) =>
+        TlaLevelConst
+
+      case TlaOperDecl(name, _, _) =>
+        cacheLevel(Set(name), name)
+        levelCacheMap(name)
+
+      case TlaTheoremDecl(_, _) =>
+        TlaLevelConst
+    }
+  }
+
+  private def cacheLevel(callers: Set[String], name: String): TlaLevel = {
+    def levelOfName(name: String): TlaLevel = {
+      if (consts.contains(name)) {
+        TlaLevelConst
+      } else if (vars.contains(name)) {
+        TlaLevelState
+      } else {
+        if (!callers.contains(name) && defs.contains(name)) {
+          // as the module comes from the parser, we assume that defs contains a definition for the name `name`
+          levelCacheMap.get(name) match {
+            case Some(level) => level
+
+            case None => cacheLevel(callers + name, name)
+          }
+        } else {
+          TlaLevelConst
+        }
+      }
+    }
+
+    val level = new TlaExLevelFinder(levelOfName)(defs(name).body)
+    levelCacheMap += name -> level
+    level
+  }
+}

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

@@ -0,0 +1,47 @@
+package at.forsyte.apalache.tla.lir
+
+import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaTempOper}
+
+/**
+ * This class computes the level of a TLA+ expression. See Lamport. Specifying Systems, p. 322.
+ *
+ * @param nameLevel a function that returns the level of a name.
+ * @author Igor Konnov
+ */
+class TlaExLevelFinder(nameLevel: String => TlaLevel) {
+  def apply(ex: TlaEx): TlaLevel = find(ex)
+
+  private def find: TlaEx => TlaLevel = {
+    case NameEx(name) =>
+      nameLevel(name)
+
+    case OperEx(op, args @ _*) =>
+      val level = TlaExLevelFinder.levelOfOper.getOrElse(op, TlaLevelConst)
+      level.join(args.map(find))
+
+    case LetInEx(body, defs @ _*) =>
+      find(body).join(defs.map(d => find(d.body)))
+
+    case _ =>
+      TlaLevelConst
+  }
+}
+
+object TlaExLevelFinder {
+  private val levelOfOper = Map(
+      TlaActionOper.prime -> TlaLevelAction,
+      TlaActionOper.enabled -> TlaLevelAction,
+      TlaActionOper.unchanged -> TlaLevelAction,
+      TlaActionOper.stutter -> TlaLevelAction,
+      TlaActionOper.nostutter -> TlaLevelAction,
+      TlaActionOper.composition -> TlaLevelAction,
+      TlaTempOper.box -> TlaLevelTemporal,
+      TlaTempOper.diamond -> TlaLevelTemporal,
+      TlaTempOper.leadsTo -> TlaLevelTemporal,
+      TlaTempOper.weakFairness -> TlaLevelTemporal,
+      TlaTempOper.strongFairness -> TlaLevelTemporal,
+      TlaTempOper.guarantees -> TlaLevelTemporal,
+      TlaTempOper.AA -> TlaLevelTemporal,
+      TlaTempOper.EE -> TlaLevelTemporal
+  )
+}

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

@@ -0,0 +1,93 @@
+package at.forsyte.apalache.tla.lir
+
+/**
+ * The level of a TLA+ expression, as explained in: Lamport. Specifying Systems, p. 322.
+ */
+sealed trait TlaLevel extends Ordered[TlaLevel] {
+
+  /**
+   * The level number as assigned in the book.
+   */
+  val level: Int
+
+  /**
+   * A textual representation of the level.
+   */
+  val name: String
+
+  /**
+   * Compare this level to another level.
+   *
+   * @param that the level to compare
+   * @return 0, if the levels are equal; a negative number if `this` is smaller than `that`, and a positive number
+   *         if `this` is larger than `that`.
+   */
+  override def compare(that: TlaLevel): Int = {
+    level - that.level
+  }
+
+  /**
+   * Join the levels by computing the maximum of the levels of `this` and `that`.
+   *
+   * @param that the level to join with
+   * @return the minimal level j that satisfies: `j <= this` and `j <= that`.
+   */
+  def join(that: TlaLevel): TlaLevel = {
+    TlaLevel.fromInt(Math.max(level, that.level))
+  }
+
+  /**
+   * Join the level with a sequence of level.
+   *
+   * @param otherLevels a sequence of levels
+   * @return the join of `this` and otherLevels
+   */
+  def join(otherLevels: Seq[TlaLevel]): TlaLevel = {
+    otherLevels.foldLeft(this) { case (l, r) => l.join(r) }
+  }
+}
+
+object TlaLevel {
+  private val INT_TO_LEVEL = Seq(TlaLevelConst, TlaLevelState, TlaLevelAction, TlaLevelTemporal)
+
+  def fromInt(levelNo: Int): TlaLevel = {
+    INT_TO_LEVEL.find(_.level == levelNo) match {
+      case Some(level) => level
+
+      case None =>
+        throw new IllegalArgumentException(s"Unexpected level: $levelNo")
+    }
+  }
+}
+
+/**
+ * Constant level: constants and constant-level expressions.
+ */
+case object TlaLevelConst extends TlaLevel {
+  override val level: Int = 0
+  override val name: String = "Constant"
+}
+
+/**
+ * State level: the constant-level, state variables, and expressions over them that are not actions or temporal formulas.
+ */
+case object TlaLevelState extends TlaLevel {
+  override val level: Int = 1
+  override val name: String = "State"
+}
+
+/**
+ * Action level: the state level, state variables, primed state variables, and action operators.
+ */
+case object TlaLevelAction extends TlaLevel {
+  override val level: Int = 2
+  override val name: String = "Action"
+}
+
+/**
+ * Temporal level: the action level and temporal formulas.
+ */
+case object TlaLevelTemporal extends TlaLevel {
+  override val level: Int = 3
+  override val name: String = "Temporal"
+}