closing #272: better diagnostics for recursive operators

CHANGES.md

@@ -1,5 +1,6 @@
 ## Unreleased #unstable
 
+ * better diagnostics for the recursive operators, see #272 
  * Use a staged docker build, reducing container size ~70%, see #195
  * Use [Z3-TurnKey](https://github.com/tudo-aqua/z3-turnkey) instead of a
    bespoke Z3 build, see #219

test/tla/Rec10.tla

@@ -1,19 +1,27 @@
+--------------------------- MODULE Rec10 -------------------------------------
 (*
- * A regression test.
- * Recursive operators that are declared via instances should not fail.
+ * A test for unfolding recursive definitions.
+ *
+ * Igor Konnov, April 2020
  *)
--------------------------------- MODULE test -------------------------------
------------------------------ MODULE inner ---------------------------
-RECURSIVE A(_)
-A(x) == IF x = 1 THEN 1 ELSE A(1)
-======================================================================
+EXTENDS Integers
 
 VARIABLES f
-I == INSTANCE inner
 
-Init == f = I!A(0)
+RECURSIVE Fact(_)
 
-Next == UNCHANGED f
+Fact(n) ==
+  IF n <= 1
+  THEN 1
+  ELSE n * Fact(n - 1)
 
-Inv == TRUE
-============================================================================
+Init ==
+    f = Fact(4)
+
+Next ==
+    f' = Fact(7)
+
+Inv ==
+    f >= 1
+
+=============================================================================

test/tla/Rec11.tla

@@ -0,0 +1,33 @@
+--------------------------- MODULE Rec11 -------------------------------------
+(*
+ * A test for unfolding recursive definitions.
+ *
+ * Igor Konnov, April 2020
+ *)
+EXTENDS Integers
+
+VARIABLES f
+
+RECURSIVE Fact(_)
+
+Fact(n) ==
+  IF n <= 1
+  THEN 1
+  ELSE n * Fact(n - 1)
+
+\* define the default value
+UNROLL_DEFAULT_Fact == 0
+
+\* but keep UNROLL_TIMES_Fact undefined
+\*UNROLL_TIMES_Fact == 4
+
+Init ==
+    f = Fact(4)
+
+Next ==
+    f' = Fact(7)
+
+Inv ==
+    f >= 1
+
+=============================================================================

test/tla/Rec5.tla

@@ -4,11 +4,10 @@
  *
  * Igor Konnov, April 2020
  *)
-EXTENDS Integers
+EXTENDS Integers, FiniteSets
 
-CONSTANTS
-    MAX_POWER,  \* a maximal voting power
-    Procs       \* a set of processes
+MAX_POWER == 3              \* the maximal voting power
+Procs == {"a", "b", "c"}     \* the set of processes
 
 VARIABLES votingPower
 
@@ -24,8 +23,8 @@ Sum(S) ==
   ELSE LET x == CHOOSE y \in S: TRUE IN
     votingPower[x] + Sum(S \ {x})
 
-UNFOLD_TIMES_Sum == Cardinality(Procs)
-UNFOLD_DEFAULT_Sum == 0
+UNROLL_TIMES_Sum == 3
+UNROLL_DEFAULT_Sum == 0
 
 Init ==
     votingPower \in [Procs -> 0..MAX_POWER]

test/tla/cli-integration-tests.md

@@ -328,6 +328,27 @@ The outcome is: NoError
 ...
 ```
 
+### check Rec10.tla fails without UNROLL_DEFAULT_Fact
+
+```sh
+$ apalache-mc check Rec10.tla | sed 's/[IEW]@.*//'
+...
+Input error (see the manual): Recursive operator Fact requires an annotation UNROLL_DEFAULT_Fact. See: https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#recursion
+...
+EXITCODE: ERROR (99)
+```
+
+### check Rec11.tla fails without UNROLL_TIMES_Fact
+
+```sh
+$ apalache-mc check Rec11.tla | sed 's/[IEW]@.*//'
+...
+Input error (see the manual): Recursive operator Fact requires an annotation UNROLL_TIMES_Fact. See: https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#recursion
+...
+EXITCODE: ERROR (99)
+```
+
+
 ### check ExistsAsValue.tla succeeds
 
 ```sh

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala

@@ -8,7 +8,7 @@ import at.forsyte.apalache.tla.imp.SanyException
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir.{MalformedTlaError, TlaEx}
 import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
-import at.forsyte.apalache.tla.pp.{ConfigurationError, IrrecoverablePreprocessingError, NotInKeraError, TLCConfigurationError}
+import at.forsyte.apalache.tla.pp.{ConfigurationError, IrrecoverablePreprocessingError, NotInKeraError, TLCConfigurationError, TlaInputError}
 import com.typesafe.scalalogging.LazyLogging
 import javax.inject.{Inject, Singleton}
 
@@ -30,6 +30,9 @@ class CheckerExceptionAdapter @Inject()(sourceStore: SourceStore,
     case err: ConfigurationError =>
       NormalErrorMessage("Configuration error (see the manual): " + err.getMessage)
 
+    case err: TlaInputError =>
+      NormalErrorMessage("Input error (see the manual): " + err.getMessage)
+
     case err: AssignmentException =>
       logger.info("To understand the error, read the manual:")
       logger.info("  [https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#assignments]")

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

@@ -9,7 +9,6 @@ import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TlaModu
 import at.forsyte.apalache.tla.lir.values.TlaInt
 
 class Unroller( tracker : TransformationTracker ) extends TlaModuleTransformation {
-
   import Unroller._
 
   def unrollLetIn(
@@ -65,20 +64,22 @@ class Unroller( tracker : TransformationTracker ) extends TlaModuleTransformatio
     bodyMap.get( unrollLimitOperName ) match {
       case Some( unrollLimitDecl ) =>
         // The unrollLimit operator must not be recursive ...
+        val msg = s"Expected an integer bound in $unrollLimitOperName, found a recursive operator. See: " + MANUAL_LINK
         if ( unrollLimitDecl.isRecursive )
-          FailWith( new Exception( s"Unroll-limit operator $unrollLimitOperName is recursive." ) )
+          FailWith( new TlaInputError( msg ) )
         else
         // ... and must evaluate to a single integer
           ConstSimplifier( tracker )(
             InlinerOfUserOper( bodyMap, tracker )( unrollLimitDecl.body )
           ) match {
             case ValEx( TlaInt( n ) ) =>
               SucceedWith( n )
-            case _ =>
-              FailWith( new Exception( s"Unroll-limit operator $unrollLimitOperName body must be a single integer." ) )
+            case e =>
+              FailWith( new TlaInputError(s"Expected an integer bound in $unrollLimitOperName, found: " + e) )
           }
       case None =>
-        FailWith( new Exception( s"Unroll-limit operator $unrollLimitOperName for $name is not defined." ) )
+        val msg = s"Recursive operator $name requires an annotation $unrollLimitOperName. See: " + MANUAL_LINK
+        FailWith( new TlaInputError( msg ) )
     }
   }
 
@@ -87,13 +88,14 @@ class Unroller( tracker : TransformationTracker ) extends TlaModuleTransformatio
     bodyMap.get( defaultOperName ) match {
       case Some( defaultDecl ) =>
         // ... which must not be recursive ...
+        val msg = s"Expected a default value in $defaultOperName, found a recursive operator. See: " + MANUAL_LINK
         if ( defaultDecl.isRecursive )
-          FailWith( new Exception( s"Default body operator $defaultOperName is recursive." ) )
+          FailWith( new TlaInputError( msg ) )
         else
         // ... but may be defined using other operators, so we call transform on it
           SucceedWith( InlinerOfUserOper( bodyMap, tracker )( defaultDecl.body ) )
       case None =>
-        FailWith( new Exception( s"Default body operator $defaultOperName for $name is not defined." ) )
+        FailWith( new TlaInputError( s"Recursive operator $name requires an annotation $defaultOperName. See: " + MANUAL_LINK ) )
     }
   }
 
@@ -154,6 +156,7 @@ class Unroller( tracker : TransformationTracker ) extends TlaModuleTransformatio
 object Unroller {
   val UNROLL_TIMES_PREFIX   : String = "UNROLL_TIMES_"
   val UNROLL_DEFAULT_PREFIX : String = "UNROLL_DEFAULT_"
+  val MANUAL_LINK: String = "https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#recursion"
 
   def apply( tracker : TransformationTracker ) : Unroller = {
     new Unroller( tracker )

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

@@ -34,6 +34,15 @@ class IrrecoverablePreprocessingError(message: String) extends Exception(message
   */
 class ConfigurationError(message: String) extends Exception(message)
 
+/**
+  * An exception that should be thrown when the TLA+ code is not following the Apalache guidelines, e.g.,
+  * missing annotations for the recursive operators.
+  * This exception should be treated as the input error: no stack trace, normal messages.
+  *
+  * @param message the error message
+  */
+class TlaInputError(message: String) extends Exception(message)
+
 /**
  * An exception that should be thrown when a TLC configuration is wrong/not-found
  * @param message the error message