Explanation of caseAssertions behavior (#2707)

apalache-mc · Aug 24, 2023 · 80ee397 · 80ee397
1 parent d783788
commit 80ee397
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala
@@ -49,8 +49,12 @@ trait Oracle extends Serializable {
       assertions: Seq[TBuilderInstruction],
       elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = {
     size match {
+      // If the oracle has no candidate values, then caseAssertions should return a no-op for SMT, i.e. TRUE.
       case 0 => state.arena.cellTrue().toBuilder
 
+      // If the oracle has a single candidate value, then the chosen value will always equal to the (sole) candidate value.
+      // In other words, for such an oracle, whenEqualTo(..., 0) will always hold.
+      // Therefore, we don't need an ITE (and don't need to consider elseAssertions), we just take the first assertion.
       case 1 => assertions.head
 
       case _ =>