Add the operator Guess

UNRELEASED.md

@@ -12,4 +12,5 @@
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
 ### Features
 
+* Add the operator `Apalache!Guess`, see #1590 and #888
 * Extend the type parser to support ADR014 (experimental), see #1602

docs/src/lang/apalache-operators.md

@@ -43,6 +43,44 @@ True
 >> a = (b == "c") # a' := (b = "c")
 ```
 
+----------------------------------------------------------------------------
+
+<a name="Guess"></a>
+
+## Non-deterministically guess a value
+
+**Notation:** `Guess(S)`
+
+**LaTeX notation:** `Guess(S)`
+
+**Arguments:** One argument: a finite set `S`, possibly empty.
+
+**Apalache type:** `Set(a) => a`, for some type `a`.
+
+**Effect:** Non-deterministically pick a value out of the set `S`, if `S` is
+non-empty. If `S` is empty, return some value of the proper type.
+
+**Determinism:** Non-deterministic if `S` is non-empty, that is, two subsequent
+calls to `Guess(S)` may return `x, y \in S` that can differ (`x /= y`) or may
+be equal (`x = y`). Moreover, Apalache considers all possible combinations of
+elements of `S` in the model checking mode. If `S` is empty, `Guess(S)`
+produces the same value of proper type.
+
+**Errors:**
+If `S` is not a set, Apalache reports an error.
+
+**Example in TLA+:**
+
+```tla
+/\ 1 = Guess({ 1, 2, 3 })         \* TRUE or FALSE
+/\ 2 = Guess({ 1, 2, 3 })         \* TRUE or FALSE
+/\ 3 = Guess({ 1, 2, 3 })         \* TRUE or FALSE
+/\ 4 /= Guess({ 1, 2, 3 })        \* TRUE
+/\ Guess({ 1, 2, 3 }) \in Int     \* TRUE
+```
+
+
+
 ----------------------------------------------------------------------------
 
 <a name="Gen"></a>

src/tla/Apalache.tla

@@ -38,6 +38,19 @@ x := e == x = e
  *)
 Gen(size) == {}
 
+(**
+ * Non-deterministically pick a value out of the set `S`, if `S` is non-empty.
+ * If `S` is empty, return some value of the proper type.  This can be
+ * understood as a non-deterministic version of CHOOSE x \in S: TRUE.
+ *
+ * @type: Set(a) => a;
+ *)
+Guess(S) ==
+    \* Since this is not supported by TLC,
+    \* we fall back to the deterministic version for TLC.
+    \* Apalache redefines the operator `Guess` as explained above.
+    CHOOSE x \in S: TRUE
+
 (**
  * Convert a set of pairs S to a function F. Note that if S contains at least
  * two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,

test/tla/TestSets.tla

@@ -4,7 +4,7 @@
  * We introduce a trivial state machine and write tests as state invariants.
  *)
 
-EXTENDS Integers, FiniteSets
+EXTENDS Integers, FiniteSets, Apalache
 
 Init == TRUE
 Next == TRUE
@@ -175,19 +175,58 @@ TestChooseMin ==
     IN
     min = 1
 
+TestGuessMin ==
+    LET min == Guess({
+            i \in Set1357:
+                \A j \in Set1357: i <= j
+        })
+    IN
+    min = 1
+
 TestChooseSet ==
     LET S ==
         CHOOSE T \in { SetEmpty, Set263, Set1357 }:
             6 \in T
     IN
     S = Set263
 
+TestGuessSet ==
+    LET S ==
+        Guess({ T \in { SetEmpty, Set263, Set1357 }: 6 \in T })
+    IN
+    S = Set263
+
+TestChooseSetFromTwo ==
+    LET S ==
+        CHOOSE T \in { SetEmpty, Set263, Set1357 }:
+            3 \in T
+    IN
+    S \in { Set263, Set1357 }
+
+TestGuessSetFromTwo ==
+    LET S ==
+        Guess({ T \in { SetEmpty, Set263, Set1357 }: 3 \in T })
+    IN
+    S \in { Set263, Set1357 }
+
 TestChooseInSingleton ==
     LET x == CHOOSE i \in { 3 }: TRUE IN
     x = 3
 
+TestGuessInSingleton ==
+    LET x == Guess({ 3 }) IN
+    x = 3
+
 TestChooseEmpty ==
     LET x == CHOOSE i \in SetEmpty: TRUE IN
+    \* This expression is equivalent to TRUE.
+    \* We are using to avoid constant simplification of TRUE.
+    x <= 0 \/ x > 0
+
+TestGuessEmpty ==
+    LET x == Guess(SetEmpty) IN
+    \* This expression is equivalent to TRUE.
+    \* We are using to avoid constant simplification of TRUE.
     x <= 0 \/ x > 0
 
 TestForallSet ==
@@ -240,6 +279,10 @@ AllTests ==
     /\ TestChooseInSingleton
     /\ TestChooseEmpty
     /\ TestChooseSet
+    /\ TestGuessMin
+    /\ TestGuessInSingleton
+    /\ TestGuessEmpty
+    /\ TestGuessSet
     /\ TestIsFiniteSet
     /\ TestPowersetCardinality
     \* IGNORE UNTIL FIXED: /\ TestIsFiniteSetOnInfinite

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala

@@ -192,7 +192,9 @@ class SymbStateRewriterImpl(
         key(tla.forall(tla.name("x"), tla.name("S"), tla.name("p")))
           -> List(new QuantRule(this)),
         key(tla.choose(tla.name("x"), tla.name("S"), tla.name("p")))
-          -> List(new ChooseRule(this)),
+          -> List(new ChooseOrGuessRule(this)),
+        key(tla.guess(tla.name("S")))
+          -> List(new ChooseOrGuessRule(this)),
         // control flow
         key(tla.ite(tla.name("cond"), tla.name("then"), tla.name("else")))
           -> List(new IfThenElseRule(this)),

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/analyses/ExpansionMarker.scala

@@ -61,10 +61,15 @@ class ExpansionMarker @Inject() (tracker: TransformationTracker) extends TlaExTr
       OperEx(op, OperEx(TlaBoolOper.exists, name, transform(false)(set), transform(false)(pred))(tag))(tag)
 
     case ex @ OperEx(op @ TlaOper.chooseBounded, name, set, pred) =>
-      // CHOOSE is essentially a skolemizable existential with the constraint of uniqueness
+      // CHOOSE does not require the set to be expanded
       val tag = ex.typeTag
       OperEx(op, name, transform(false)(set), transform(false)(pred))(tag)
 
+    case ex @ OperEx(op @ ApalacheOper.guess, set) =>
+      // Guess does not require the set to be expanded
+      val tag = ex.typeTag
+      OperEx(op, transform(false)(set))(tag)
+
     case ex @ OperEx(op, name, set, pred) if op == TlaBoolOper.exists || op == TlaBoolOper.forall =>
       // non-skolemizable quantifiers require their sets to be expanded
       val tag = ex.typeTag

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/ChooseOrGuessRule.scala

@@ -0,0 +1,87 @@
+package at.forsyte.apalache.tla.bmcmt.rules
+
+import at.forsyte.apalache.tla.bmcmt._
+import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, OracleHelper}
+import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TlaType1}
+import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.convenience.tla
+import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaOper}
+
+/**
+ * <p>Rewriting rule for CHOOSE and Apalache!Guess. We implement a non-deterministic choice. It is not hard to add the
+ * requirement of determinism, but that will most likely affect efficiency.</p>
+ *
+ * <p>We will make CHOOSE deterministic when the issue #841 is solved.</p>
+ *
+ * @author
+ *   Igor Konnov
+ */
+class ChooseOrGuessRule(rewriter: SymbStateRewriter) extends RewritingRule {
+  private val pickRule = new CherryPick(rewriter)
+
+  override def isApplicable(state: SymbState): Boolean = {
+    state.ex match {
+      case OperEx(TlaOper.chooseBounded, _, _, _) =>
+        true
+
+      case OperEx(ApalacheOper.guess, _) =>
+        true
+
+      case _ =>
+        false
+    }
+  }
+
+  override def apply(state: SymbState): SymbState = {
+    state.ex match {
+      case OperEx(TlaOper.chooseBounded, varName, set, pred) =>
+        // This is a general encoding, handling both happy and unhappy scenarios,
+        // that is, when CHOOSE is defined on its arguments and not, respectively.
+        // Compute set comprehension and then pick an element from it.
+        val setT = set.typeTag.asTlaType1()
+        val filterEx = tla
+          .filter(varName, set, pred)
+          .typed(setT)
+        val nextState = rewriter.rewriteUntilDone(state.setRex(filterEx))
+        guess(setT, nextState)
+
+      case OperEx(ApalacheOper.guess, setEx) =>
+        val setT = setEx.typeTag.asTlaType1()
+        val nextState = rewriter.rewriteUntilDone(state.setRex(setEx))
+        guess(setT, nextState)
+
+      case _ =>
+        throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex)
+    }
+  }
+
+  private def guess(setT: TlaType1, state: SymbState): SymbState = {
+    // pick an arbitrary witness
+    val setCell = state.asCell
+    if (state.arena.getHas(setCell).isEmpty) {
+      setT match {
+        case SetT1(elemT) =>
+          val (newArena, defaultValue) = rewriter.defaultValueCache.getOrCreate(state.arena, elemT)
+          state.setArena(newArena).setRex(defaultValue.toNameEx)
+
+        case _ =>
+          throw new IllegalStateException(s"Expected a set, found: $setT")
+      }
+    } else {
+      val elems = state.arena.getHas(setCell)
+      // add an oracle \in 0..N, where the indices from 0 to N - 1 correspond to the set elements,
+      // whereas the index N corresponds to the default choice when the set is empty
+      val (oracleState, oracle) = pickRule.oracleFactory.newDefaultOracle(state, elems.size + 1)
+
+      // pick a cell
+      val nextState = pickRule.pickByOracle(oracleState, oracle, elems, oracleState.arena.cellTrue().toNameEx)
+      val pickedCell = nextState.asCell
+      // require the oracle to produce only the values for the set elements (or no elements, when it is empty)
+      OracleHelper.assertOraclePicksSetMembers(rewriter, nextState, oracle, setCell, elems)
+
+      // If oracle = N, the picked cell is not constrained. In the past, we used a default value here,
+      // but it sometimes produced conflicts (e.g., a picked record domain had to coincide with a default domain)
+      nextState.setRex(pickedCell.toNameEx)
+    }
+  }
+}

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala

@@ -10,7 +10,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestRewriterWithArrays
     extends TestCherryPick with TestSymbStateDecoder with TestSymbStateRewriter with TestSymbStateRewriterAction
     with TestSymbStateRewriterApalacheGen with TestSymbStateRewriterAssignment with TestSymbStateRewriterBool
-    with TestSymbStateRewriterChoose with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
+    with TestSymbStateRewriterChooseOrGuess with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
     with TestSymbStateRewriterFiniteSets with TestSymbStateRewriterFoldSeq with TestSymbStateRewriterFoldSet
     with TestSymbStateRewriterFun with TestSymbStateRewriterFunSet with TestSymbStateRewriterInt
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecFun with TestSymbStateRewriterRecord

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala

@@ -10,7 +10,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestRewriterWithOOPSLA19
     extends TestCherryPick with TestSymbStateDecoder with TestSymbStateRewriter with TestSymbStateRewriterAction
     with TestSymbStateRewriterApalacheGen with TestSymbStateRewriterAssignment with TestSymbStateRewriterBool
-    with TestSymbStateRewriterChoose with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
+    with TestSymbStateRewriterChooseOrGuess with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
     with TestSymbStateRewriterFiniteSets with TestSymbStateRewriterFoldSeq with TestSymbStateRewriterFoldSet
     with TestSymbStateRewriterFun with TestSymbStateRewriterFunSet with TestSymbStateRewriterInt
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecFun with TestSymbStateRewriterRecord