Bugfixes in Desugarer and propagation of primes

UNRELEASED.md

@@ -12,8 +12,14 @@
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
 ### Bug fixes
 
- * handling big integers, #450
+ * handling big integers, see #450
+ * expanding tuples in quantifiers, see #476
+ * unfolding UNCHANGED for arbitrary expressions, see #471
+ * unfolding UNCHANGED <<>>, see #475
 
 ### Features
 
- * constant simplification over strings, #197
+ * constant simplification over strings, see #197
+ * propagation of primes inside expressions,
+   e.g., (f[i])' becomes f'[i'] if both f and i are state variables
+

docs/src/apalache/features.md

@@ -13,9 +13,9 @@ Construct  | Supported? | Milestone | Comment
 ``F(x1, ..., x_n) == exp`` | ✔ / ✖ | - | Every application of `F` is replaced with its body. Recursive operators need [unrolling annotations](./principles.md#recursive-operators).
 ``f[x ∈ S] == exp`` | ✔ / ✖ | - | Only recursive functions that return integers or Booleans are supported.
 ``INSTANCE M WITH ...`` | ✔ / ✖ | - | No special treatment for ``~>``, ``\cdot``, ``ENABLED``
-``N(x1, ..., x_n) == INSTANCE M WITH...`` | ✔ / ✖ | - | Parameterized instances are not supported yet, LOCAL operator definitions inside instances may fail to work
+``N(x1, ..., x_n) == INSTANCE M WITH...`` | ✔ / ✖ | - | Parameterized instances are not supported
 ``THEOREM P`` | ✔ / ✖ | - | Parsed but not used
-``LOCAL def`` | ✔ | - | Handled by SANY
+``LOCAL def`` | ✔ | - | Replaced with local LET-IN definitions
 
 ### The constant operators
 
@@ -53,7 +53,7 @@ Operator  | Supported? | Milestone | Comment
 ------------------------|:------------------:|:---------------:|--------------
 `f[e]` | ✔ | - |
 `DOMAIN f` | ✔ | - |
-`[ x \in S ↦ e]` | ✔ / ✖ | - |  
+`[ x \in S ↦ e]` | ✔ | - |  
 `[ S -> T ]` | ✔ | - | Sometimes, the functions sets are expanded
 `[ f EXCEPT ![e1] = e2 ]` | ✔ | - |
 
@@ -89,7 +89,7 @@ Construct  | Supported? | Milestone | Comment
 `"c1...c_n"` | ✔ | - | A string is always mapped to a unique uninterpreted constant
 `STRING` | ✖ | - | It is an infinite set. We cannot handle infinite sets.
 `d1...d_n` | ✔ | - | As long as the SMT solver (Z3) accepts that large number
-`d1...d_n.d_n+1...d_m` | ✖ | - | Technical issue. We will implemented upon a user request.
+`d1...d_n.d_n+1...d_m` | ✖ | - | Technical issue. We will implement it upon a user request.
 
 #### Miscellaneous Constructs
 
@@ -98,14 +98,14 @@ Construct  | Supported? | Milestone | Comment
 `IF p THEN e1 ELSE e2` | ✔ | - | Provided that both e1 and e2 have the same type
 `CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> e` | ✔ | - | See the comment above
 `CASE p1 -> e1 [] ... [] p_n -> e_n` | ✖ | - | Introduce the default arm with `OTHER`.
-``LET d1 == e1 ... d_n == e_n IN e`` | ✔ / ✖ | `0.7-dev-calls` | All applications of `d1`, ..., `d_n` are replaced with the expressions `e1`, ... `e_n` respectively. LET-definitions without arguments are kept in place.
+``LET d1 == e1 ... d_n == e_n IN e`` | ✔ |  | All applications of `d1`, ..., `d_n` are replaced with the expressions `e1`, ... `e_n` respectively. LET-definitions without arguments are kept in place.
 multi-line `/\` and `\/` | ✔ | - |
 
 ### The Action Operators
 
 Construct  | Supported? | Milestone | Comment
 ------------------------|:------------------:|:---------------:|--------------
-``e'`` | ✔ / ✖ | - | Provided that e is a variable
+``e'`` | ✔ | - |
 ``[A]_e`` | ✖ | - | It does not matter for safety
 ``< A >_e`` | ✖ | - |
 ``ENABLED A`` | ✖ | - |
@@ -141,8 +141,8 @@ Operator  | Supported? | Milestone | Comment
 Operator  | Supported? | Milestone | Comment
 ------------------------|:------------------:|:---------------:|--------------
 ``<<...>>``, ``Head``, ``Tail``, ``Len``, ``SubSeq``, `Append`, `\o`, `f[e]` | ✔ | - | The sequence constructor ``<<...>>`` needs a [type annotation](types-and-annotations.md).
-``EXCEPT`` | ✖ | `0.9` | this operator do not seem to be often used
-``Seq(S)`` | ✖ | - | We need an upper bound on the length of the sequences.
+``EXCEPT`` | ✖ |   | If you need it, let us know, issue #324
+``Seq(S)`` | ✖ | - | If you need it, let us know, issue #314
 ``SelectSeq`` | ✖ | - | will not be supported in the near future
 
 ### FiniteSets

test/tla/ExistTuple476.tla

@@ -0,0 +1,17 @@
+------------------ MODULE ExistTuple476 ----------------------
+(* A regression test for the issue:
+   https://github.com/informalsystems/apalache/issues/476
+ *)
+EXTENDS Integers
+
+VARIABLES x, y
+
+Init ==
+    x = 0 /\ y = 0
+
+Next ==
+    \E <<i, j>> \in (1..2) \X (3..4):
+        /\ x' = i
+        /\ y' = j
+
+==============================================================

test/tla/UnchangedExpr471.tla

@@ -0,0 +1,22 @@
+------------------------ MODULE UnchangedExpr471 ----------------------------
+(* A regression test for UNCHANGED e:
+   see issue: https://github.com/informalsystems/apalache/issues/471
+ *)
+EXTENDS Integers
+
+CONSTANT N
+
+VARIABLES f, i
+
+ConstInit ==
+    N' = 3
+
+Init ==
+    /\ f = [ j \in 1..3 |-> j * 2]
+    /\ i = 2
+
+Next ==
+    UNCHANGED <<f, i, f[i], N>>
+
+==============================================================================
+

test/tla/cli-integration-tests.md

@@ -110,6 +110,24 @@ EXITCODE: OK
 ## running the check command
 
 
+### check UnchangedExpr471.tla reports no error: regression for issue 471
+
+```sh
+$ apalache-mc check --cinit=ConstInit --length=1 UnchangedExpr471.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
+### check ExistTuple476.tla reports no error: regression for issue 476
+
+```sh
+$ apalache-mc check --length=1 ExistTuple476.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
 ### check InvSub for SafeMath reports no error: regression for issue 450
 
 ```sh

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

@@ -2,9 +2,10 @@ package at.forsyte.apalache.tla.pp
 
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.convenience._
-import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaFunOper, TlaOper, TlaSetOper}
+import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaBoolOper, TlaFunOper, TlaOper, TlaSetOper}
 import at.forsyte.apalache.tla.lir.transformations.standard.FlatLanguagePred
 import at.forsyte.apalache.tla.lir.transformations.{LanguageWatchdog, TlaExTransformation, TransformationTracker}
+
 import javax.inject.Singleton
 
 /**
@@ -45,15 +46,40 @@ class Desugarer(tracker: TransformationTracker) extends TlaExTransformation {
 
       case OperEx(TlaActionOper.unchanged, args @ _*) =>
         // flatten all tuples, e.g., convert <<x, <<y, z>> >> to [x, y, z]
-        val flatArgs = flattenTuples(tla.tuple(args.map(transform) :_*))
-        // and map every x to x' = x
+        val flatArgs = flattenTuplesInUnchanged(tla.tuple(args.map(transform) :_*))
+        // map every x to x' = x
         val eqs = flatArgs map { x => tla.eql(tla.prime(x), x) }
-        tla.and(eqs :_*)
+        // x' = x /\ y' = y /\ z' = z
+        eqs match {
+          case Seq() =>
+            // results from UNCHANGED <<>>, UNCHANGED << << >> >>, etc.
+            tla.bool(true)
+
+          case Seq(one) =>
+            one
+
+          case _ =>
+            tla.and(eqs: _*)
+        }
 
       case OperEx(TlaSetOper.filter, boundEx, setEx, predEx) =>
+        // rewrite { <<x, <<y, z>> >> \in XYZ: P(x, y, z) }
+        // to { x_y_z \in XYZ: P(x_y_z[1], x_y_z[1][1], x_y_z[1][2]) }
         OperEx(TlaSetOper.filter, collapseTuplesInFilter(transform(boundEx), transform(setEx), transform(predEx)) :_*)
 
+      case OperEx(TlaBoolOper.exists, boundEx, setEx, predEx) =>
+        // rewrite \E <<x, <<y, z>> >> \in XYZ: P(x, y, z)
+        // to \E x_y_z \in XYZ: P(x_y_z[1], x_y_z[1][1], x_y_z[1][2])
+        OperEx(TlaBoolOper.exists, collapseTuplesInFilter(transform(boundEx), transform(setEx), transform(predEx)) :_*)
+
+      case OperEx(TlaBoolOper.forall, boundEx, setEx, predEx) =>
+        // rewrite \A <<x, <<y, z>> >> \in XYZ: P(x, y, z)
+        // to \A x_y_z \in XYZ: P(x_y_z[1], x_y_z[1][1], x_y_z[1][2])
+        OperEx(TlaBoolOper.forall, collapseTuplesInFilter(transform(boundEx), transform(setEx), transform(predEx)) :_*)
+
       case OperEx(TlaSetOper.map, args @ _*) =>
+        // rewrite { <<x, <<y, z>> >> \in XYZ |-> e(x, y, z) }
+        // to { x_y_z \in XYZ |-> e(x_y_z[1], x_y_z[1][1], x_y_z[1][2])
         val trArgs = args map transform
         OperEx(TlaSetOper.map, collapseTuplesInMap(trArgs.head, trArgs.tail) :_*)
 
@@ -81,15 +107,21 @@ class Desugarer(tracker: TransformationTracker) extends TlaExTransformation {
         LetInEx( transform( body ), defs map { d => d.copy( body = transform( d.body ) ) } : _* )
   }
 
-  private def flattenTuples(ex: TlaEx): Seq[TlaEx] = ex match {
+  private def flattenTuplesInUnchanged(ex: TlaEx): Seq[TlaEx] = ex match {
     case OperEx(TlaFunOper.tuple, args @ _*) =>
-      args.map(flattenTuples).reduce(_ ++ _)
+      if (args.isEmpty) {
+        // Surprisingly, somebody has written UNCHANGED << >>, see issue #475.
+        Seq()
+      } else {
+        args.map(flattenTuplesInUnchanged).reduce(_ ++ _)
+      }
 
-    case NameEx(_) =>
-      Seq(ex)
+    case ValEx(_) =>
+      Seq()   // no point in priming literals
 
     case _ =>
-      throw new IllegalArgumentException("Expected a variable or a tuple of variables, found: " + ex)
+      // in general, UNCHANGED e becomes e' = e
+      Seq(ex)
   }
 
   private def expandExcept(topFun: TlaEx, accessors: Seq[TlaEx], newValues: Seq[TlaEx]): TlaEx = {

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala

@@ -2,15 +2,22 @@ package at.forsyte.apalache.tla.pp.passes
 
 import java.io.File
 import java.nio.file.Path
-
 import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin}
 import at.forsyte.apalache.tla.imp.src.SourceStore
-import at.forsyte.apalache.tla.lir.TlaModule
+import at.forsyte.apalache.tla.lir.{TlaDecl, TlaModule, TlaOperDecl}
 import at.forsyte.apalache.tla.lir.io.PrettyWriter
 import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
-import at.forsyte.apalache.tla.lir.transformations.{TlaModuleTransformation, TransformationTracker}
+import at.forsyte.apalache.tla.lir.transformations.{
+  TlaModuleTransformation,
+  TransformationTracker
+}
 import at.forsyte.apalache.tla.lir.transformations.standard._
-import at.forsyte.apalache.tla.pp.{Desugarer, Keramelizer, Normalizer, UniqueNameGenerator}
+import at.forsyte.apalache.tla.pp.{
+  Desugarer,
+  Keramelizer,
+  Normalizer,
+  UniqueNameGenerator
+}
 import com.google.inject.Inject
 import com.google.inject.name.Named
 import com.typesafe.scalalogging.LazyLogging
@@ -22,14 +29,16 @@ import com.typesafe.scalalogging.LazyLogging
   * @param tracker transformation tracker
   * @param nextPass next pass to call
   */
-class PreproPassImpl @Inject()( val options: PassOptions,
-                                gen: UniqueNameGenerator,
-                                renaming: IncrementalRenaming,
-                                tracker: TransformationTracker,
-                                sourceStore: SourceStore,
-                                changeListener: ChangeListener,
-                                @Named("AfterPrepro") nextPass: Pass with TlaModuleMixin)
-    extends PreproPass with LazyLogging {
+class PreproPassImpl @Inject() (
+    val options: PassOptions,
+    gen: UniqueNameGenerator,
+    renaming: IncrementalRenaming,
+    tracker: TransformationTracker,
+    sourceStore: SourceStore,
+    changeListener: ChangeListener,
+    @Named("AfterPrepro") nextPass: Pass with TlaModuleMixin
+) extends PreproPass
+    with LazyLogging {
 
   private var outputTlaModule: Option[TlaModule] = None
 
@@ -48,10 +57,12 @@ class PreproPassImpl @Inject()( val options: PassOptions,
   override def execute(): Boolean = {
     logger.info("  > Before preprocessing: unique renaming")
     val input = tlaModule.get
+    val varSet = input.varDeclarations.map(_.name).toSet
 
     val transformationSequence: List[(String, TlaModuleTransformation)] =
       List(
         ("Desugarer", ModuleByExTransformer(Desugarer(tracker))),
+        ("PrimePropagation", createModuleTransformerForPrimePropagation(varSet)),
         ("UniqueRenamer", renaming.renameInModule),
         ("Normalizer", ModuleByExTransformer(Normalizer(tracker))),
         ("Keramelizer", ModuleByExTransformer(Keramelizer(gen, tracker)))
@@ -65,7 +76,10 @@ class PreproPassImpl @Inject()( val options: PassOptions,
         logger.info(s"  > $name")
         val transfomed = xformer(m)
         // dump the result of preprocessing after every transformation, in case the next one fails
-        PrettyWriter.write(transfomed, new File(outdir.toFile, s"out-prepro-$name.tla"))
+        PrettyWriter.write(
+          transfomed,
+          new File(outdir.toFile, s"out-prepro-$name.tla")
+        )
         transfomed
     }
 
@@ -78,13 +92,24 @@ class PreproPassImpl @Inject()( val options: PassOptions,
     outputTlaModule = Some(afterModule)
 
     if (options.getOrElse("general", "debug", false)) {
-      val sourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener)
+      val sourceLocator =
+        SourceLocator(sourceStore.makeSourceMap, changeListener)
       outputTlaModule.get.operDeclarations foreach sourceLocator.checkConsistency
     }
 
     true
   }
 
+  private def createModuleTransformerForPrimePropagation(varSet: Set[String])
+      : ModuleByExTransformer = {
+    val cinitName = options.getOrElse("checker", "cinit", "CInit") + "Primed"
+    val includeAllButConstInit: TlaDecl => Boolean = {
+      case TlaOperDecl(name, _, _) => cinitName != name
+      case _                       => true
+    }
+    ModuleByExTransformer(new PrimePropagation(tracker, varSet), includeAllButConstInit)
+  }
+
   /**
     * Get the next pass in the chain. What is the next pass is up
     * to the module configuration and the pass outcome.
@@ -93,7 +118,7 @@ class PreproPassImpl @Inject()( val options: PassOptions,
     */
   override def next(): Option[Pass] = {
     outputTlaModule map { m =>
-      nextPass.setModule( m )
+      nextPass.setModule(m)
       nextPass
     }
   }