Unroller fix

CHANGES.md

@@ -15,6 +15,7 @@
  * Use [Z3-TurnKey](https://github.com/tudo-aqua/z3-turnkey) instead of a
    bespoke Z3 build, see #219
  * Use Z3 version 4.8.7.1, see #219
+ * Re-stabilized tests on recursive operators
 
 ## 0.7.2 [RELEASE]
 

test/tla/Rec2.tla

@@ -18,7 +18,11 @@ Card(S) ==
   IF S = IntSet({})
   THEN 0
   ELSE
-    LET T == S \ {CHOOSE y \in S: TRUE} IN
+    \* CHOOSE is introduced with a LET definition, to fix its value, whatever it may be
+    \* Note that CHOOSE in APALACHE is non-deterministic and therefore
+    \* S \ { CHOOSE x \in S : TRUE } leads to a false-positive C.E.
+    LET x == CHOOSE y \in S: TRUE IN
+    LET T == S \ {x} IN
     1 + Card(T)
 
 \* unfold the operator Card up to 10 times

test/tla/Rec5.tla

@@ -13,12 +13,12 @@ VARIABLES votingPower
 
 a <: b == a
 
-IntSet(S) == S <: {Int}
+StrSet(S) == S <: {STRING}
 
 RECURSIVE Sum(_)
 
 Sum(S) ==
-  IF S = IntSet({})
+  IF S = StrSet({})
   THEN 0
   ELSE LET x == CHOOSE y \in S: TRUE IN
     votingPower[x] + Sum(S \ {x})
@@ -33,6 +33,6 @@ Next ==
     votingPower' \in [Procs -> 0..MAX_POWER]
 
 Inv ==
-    Sum(votingPower) < 10
+    Sum(Procs) < 10
 
 =============================================================================

test/tla/Rec6.tla

@@ -5,10 +5,12 @@ N == 5
 
 VARIABLES set, count
 
+a <: b == a
+
 RECURSIVE Sum(_)
 
 Sum(S) ==
-  IF S = {}
+  IF S = {} <: {Int}
   THEN 0
   ELSE LET x == CHOOSE y \in S: TRUE IN
     x + Sum(S \ {x})
@@ -17,7 +19,7 @@ UNROLL_DEFAULT_Sum == 0
 UNROLL_TIMES_Sum == N
 
 Init ==
-  /\ set = {}
+  /\ set = {} <: {Int}
   /\ count = 0
 
 Next ==

test/tla/cli-integration-tests.md

@@ -315,6 +315,15 @@ The outcome is: NoError
 ...
 ```
 
+### check Rec2.tla succeeds
+
+```sh
+$ apalache-mc check --length=5 --inv=Inv Rec2.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
 ### check Rec3.tla succeeds
 ```sh
 $ apalache-mc check --length=10 --inv=Inv Rec3.tla | sed 's/I@.*//'
@@ -334,6 +343,24 @@ The outcome is: NoError
 ...
 ```
 
+### check Rec5.tla succeeds
+
+```sh
+$ apalache-mc check --length=5 --inv=Inv Rec5.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
+### check Rec6.tla succeeds
+
+```sh
+$ apalache-mc check --length=5 --inv=Inv Rec6.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
 ### check Rec8.tla succeeds
 
 ```sh
@@ -346,7 +373,7 @@ The outcome is: NoError
 ### check Rec9.tla succeeds
 
 ```sh
-$ apalache-mc check --length=5 --inv=Inv Rec9.tla | sed 's/I@.*//'
+$ apalache-mc check --length=3 --inv=Inv Rec9.tla | sed 's/I@.*//'
 ...
 The outcome is: NoError
 ...

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

@@ -0,0 +1,85 @@
+package at.forsyte.apalache.tla.pp
+
+import at.forsyte.apalache.tla.lir.oper.{BmcOper, TlaOper}
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TlaModuleTransformation, TransformationTracker}
+
+/** Replaces instances of user-defined operator applications with a LET-IN wrapper.
+  *
+  * Example:
+  * A(x,y) ~~> LET App_1 == A(x,y) IN App_1
+  *
+  * Operator constants and formal parameters are ignored.
+  */
+class AppWrap(
+               nameGenerator : UniqueNameGenerator,
+               tracker : TransformationTracker
+             ) {
+
+  import AppWrap.NAME_PREFIX
+
+  private def setTracking( oldEx : => TlaEx, newEx : => TlaEx ) : TlaEx = {
+    val tr = tracker.track {
+      _ => newEx
+    }
+    tr( oldEx )
+  }
+
+  def wrap( wrappableNames : Set[String] ) : TlaExTransformation = tracker.track {
+    case ex@OperEx( TlaOper.apply, NameEx( opName ), args@_* ) if wrappableNames.contains( opName ) && args.nonEmpty =>
+      val newArgs = args map wrap( wrappableNames )
+      val newEx =
+        if ( args == newArgs ) ex
+        else setTracking( ex, Builder.appOp( NameEx( opName ), newArgs : _* ) )
+
+      val newName = s"${NAME_PREFIX}_${opName}_${nameGenerator.newName()}"
+      val newDecl = TlaOperDecl( newName, List.empty, newEx )
+      LetInEx( Builder.appDecl( newDecl ), newDecl )
+      // On type annot. ignore the RHS
+    case ex@OperEx( BmcOper.withType, argEx, typeEx ) =>
+      val newArg = wrap( wrappableNames )(argEx)
+      if ( argEx == newArg )
+        ex
+      else
+        OperEx( BmcOper.withType, newArg, typeEx )
+    case ex@OperEx( oper, args@_* ) =>
+      val newArgs = args map wrap( wrappableNames )
+      if ( args == newArgs )
+        ex
+      else
+        OperEx( oper, newArgs : _* )
+    case ex@LetInEx( body, defs@_* ) =>
+      // Assumption: let-in defined operators are defined in dependency order
+      val (newWrappable, newDefs) = defs.foldLeft( (wrappableNames, Seq.empty[TlaOperDecl]) ) {
+        case ((partialSet, partialDecls), decl) =>
+          val newDecl = decl.copy( body = wrap( partialSet )( decl.body ) )
+          newDecl.isRecursive = decl.isRecursive
+          (partialSet + decl.name, partialDecls :+ newDecl)
+      }
+      val newBody = wrap( newWrappable )( body )
+      if ( body == newBody && defs == newDefs )
+        ex
+      else
+        LetInEx( newBody, newDefs : _* )
+    case ex => ex
+  }
+
+  def moduleTransform( wrappableNames : Set[String] ): TlaModuleTransformation = { m =>
+
+    val newDecls = m.declarations map {
+      case TlaOperDecl( name, params, body ) =>
+        TlaOperDecl( name, params, wrap( wrappableNames )(body) )
+      case d => d
+    }
+    new TlaModule( m.name, newDecls )
+  }
+}
+
+object AppWrap {
+  val NAME_PREFIX = "APP"
+
+  def apply(
+             nameGenerator : UniqueNameGenerator,
+             tracker : TransformationTracker
+           ) = new AppWrap( nameGenerator, tracker )
+}

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

@@ -0,0 +1,116 @@
+package at.forsyte.apalache.tla.pp
+
+import at.forsyte.apalache.tla.lir.oper.TlaOper
+import at.forsyte.apalache.tla.lir.transformations.standard.ReplaceFixed
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TlaModuleTransformation, TransformationTracker}
+
+class ParameterNormalizer(
+                           nameGenerator: UniqueNameGenerator,
+                           tracker: TransformationTracker,
+                           decisionFn: TlaOperDecl => Boolean
+                         ) {
+
+  // Transforms a declaration A(x,y(_,_)) == e
+  // into A(x,y) == LET x_new == x
+  //                    y_new( p1, p2) == y(p_1,p_2)
+  //                IN e[ x_new/x, y_new/y ]
+  // This allows us to limit the number of substitutions when inlining A
+  def mkParamNormalForm( decl : TlaOperDecl ) : TlaOperDecl = {
+    val normalizedLetIn = normalizeInternalLetIn( decl.body )
+    val newBody =
+      if ( decisionFn( decl ) ) paramNormal( decl.formalParams )( normalizedLetIn )
+      else normalizedLetIn
+    val newDecl = decl.copy( body = newBody )
+    // Copy doesn't preserve .isRecursive!
+    newDecl.isRecursive = decl.isRecursive
+    newDecl
+  }
+
+  private def normalizeInternalLetIn : TlaExTransformation = tracker.track {
+    case ex@LetInEx( body, defs@_* ) =>
+      val newDefs = defs map { d => mkParamNormalForm( d ) }
+      val newBody = normalizeInternalLetIn( body )
+      if ( defs == newDefs && body == newBody ) ex
+      else LetInEx( newBody, newDefs : _* )
+
+    case ex@OperEx( op, args@_* ) =>
+      val newArgs = args map normalizeInternalLetIn
+      if ( args == newArgs ) ex
+      else OperEx( op, newArgs : _* )
+
+    case ex => ex
+
+  }
+
+  private def paramNormal( paramNames : List[FormalParam] ) : TlaExTransformation = tracker.track { ex =>
+    paramNames.foldLeft( ex ) {
+      case (partialEx, fParam) =>
+        // For each formal parameter we invent a fresh operator name
+        val paramOperName = nameGenerator.newName()
+        // We split now, based on whether fParam is a simple or operator parameter
+        fParam match {
+          case SimpleFormalParam( name ) =>
+            // We replace all instances of `fParam` with `paramOperName`
+            // however, since paramOperName is an operator, we have to replace with application
+            val tr = ReplaceFixed(
+              NameEx( fParam.name ),
+              OperEx( TlaOper.apply, NameEx( paramOperName ) ),
+              tracker
+            )
+            val replaced = tr( partialEx )
+            // if fParam is simple, the introduced operator is nullary
+            val letInDef = TlaOperDecl( paramOperName, List.empty, NameEx( name ) )
+            LetInEx( replaced, letInDef )
+
+          case OperFormalParam( name, arity ) =>
+            // We again replace all instances of `fParam` with `paramOperName`
+            // As both are operators, we don't need to introduce application
+            val tr = ReplaceFixed(
+              NameEx( fParam.name ),
+              NameEx( paramOperName ),
+              tracker
+            )
+            val replaced = tr( partialEx )
+
+            // This time, the introduced operator is not nullary, so we need to invent parameters
+            val inventedParams = List.fill( arity ) {
+              nameGenerator.newName()
+            }
+            // The body is just the operator applied to all the parameters
+            val newBody = OperEx(
+              TlaOper.apply, name +: inventedParams map NameEx : _*
+            )
+            val letInDef = TlaOperDecl( paramOperName, inventedParams map SimpleFormalParam, newBody )
+            LetInEx( replaced, letInDef )
+        }
+    }
+  }
+
+  def normalize : TlaModuleTransformation = { m =>
+    // Iterates over all declarations and replaces those for which decisionFn returns true
+    // (by default, for all recursive)
+    val newDecls = m.declarations map {
+      case d : TlaOperDecl => mkParamNormalForm( d )
+      case d => d
+    }
+    new TlaModule( m.name, newDecls )
+
+  }
+
+}
+
+object ParameterNormalizer {
+
+  object DecisionFn {
+    def all : TlaOperDecl => Boolean = _ => true
+    def recursive : TlaOperDecl => Boolean = _.isRecursive
+  }
+
+  def apply(
+             nameGenerator : UniqueNameGenerator,
+             tracker : TransformationTracker,
+             decisionFn : TlaOperDecl => Boolean = DecisionFn.recursive
+           ) : ParameterNormalizer =
+    new ParameterNormalizer( nameGenerator, tracker, decisionFn )
+}