Change the runtime behavior of then (#1304)

* fix the semantics of then * update the docs * update changelog * fix formatting * improve comments * add detailed docs * fix the throwing tests * Update quint/src/runtime/impl/compilerImpl.ts Co-authored-by: Shon Feder <[email protected]> --------- Co-authored-by: Shon Feder <[email protected]>
informalsystems · Dec 13, 2023 · 42d0174 · 42d0174
1 parent e61c083
commit 42d0174
Show file tree

Hide file tree

Showing 8 changed files with 164 additions and 61 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -12,6 +12,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Add a run operator `A.expect(P)` to test the state predicate `P` in the state resulting from applying action `A` (#1303)
 
 ### Changed
+
+- Change in `A.then(B)`: If `A` returns `false`, `A.then(B)` fails (#1304)
+
 ### Deprecated
 ### Removed
 ### Fixed

diff --git a/doc/builtin.md b/doc/builtin.md
@@ -851,7 +851,9 @@ run test = (x' = 0).then(a).then(assert(x == 3))
 
 `a` is true for a step from `s1` to `t` and `b` is true for a step from `t` to `s2`.
 
-This is the action composition operator.
+This is the action composition operator. If `a` evaluates to `false`, then
+`a.then(b)` reports an error. If `b` evaluates to `false` after `a`, then
+`a.then(b)` returns `false`.
 
 ### Examples
 

diff --git a/doc/lang.md b/doc/lang.md
@@ -1658,13 +1658,19 @@ then(A, B)
 
 The semantics of this operator is as follows. When `A.then(B)` is applied to a
 state `s_1`, the operator computes a next state `s_2` of `s_1` by applying
-action `A`, if such a state exists. If `A` returns `true`, then the operator
-`A.then(B)` computes a next state `s_3` of `s_2` by applying action `B`, if
-such a state exists. If `B` returns true, then the operator `A.then(B)` returns
-`true`, the old state is equal to `s_1`, and the new state is equal to `s_3`.
-In all other cases, the operator returns `false`.
-
-This operator is equivalent to `A \cdot B` of TLA+.
+action `A`, if such a state exists. Depending on the result of `A`, two scenarios
+are possible:
+
+ - When `A` returns `true`, then the operator `A.then(B)` computes a next state
+ `s_3` of `s_2` by applying action `B`, if such a state exists.
+  If `B` returns true, then the operator `A.then(B)` returns
+  `true`, the old state is equal to `s_1`, and the new state is equal to `s_3`.
+  Otherwise, the operator `A.then(B)` returns `false`.
+
+ - If `A` returns `false`, then it is impossible to continue. A runtime error
+  should be reported.
+
+This operator is equivalent to `A \cdot B` of TLA+ (except for the runtime errors).
 
 **Example.** Consider the specification `counters`:
 

diff --git a/examples/language-features/counters.qnt b/examples/language-features/counters.qnt
@@ -80,10 +80,10 @@ module counters {
   // this tests for a failing condition
   run failingTest = {
     init
-      .then(10.reps(_ => all {
+      .then(all {
          n == 0,
          step,
-       }))
+       })
       .fail()
   }
 

diff --git a/quint/src/builtin.qnt b/quint/src/builtin.qnt
@@ -780,7 +780,9 @@ module builtin {
   ///
   /// `a` is true for a step from `s1` to `t` and `b` is true for a step from `t` to `s2`.
   ///
-  /// This is the action composition operator.
+  /// This is the action composition operator. If `a` evaluates to `false`, then
+  /// `a.then(b)` reports an error. If `b` evaluates to `false` after `a`, then
+  /// `a.then(b)` returns `false`.
   ///
   /// ### Examples
   ///

diff --git a/quint/src/quintError.ts b/quint/src/quintError.ts
@@ -101,6 +101,8 @@ export type ErrorCode =
   | 'QNT511'
   /* QNT512: Simulation failure */
   | 'QNT512'
+  /* QNT513: Cannot continue in 'then' */
+  | 'QNT513'
 
 /* Additional data for a Quint error */
 export interface QuintErrorData {

diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts
@@ -1257,8 +1257,18 @@ export class CompilerVisitor implements IRVisitor {
     }
   }
 
-  // compute all { ... } or A.then(B)...then(E) for a chain of actions
-  private chainAllOrThen(actions: Computable[], kind: 'all' | 'then'): Maybe<EvalResult> {
+  /**
+   *  Compute all { ... } or A.then(B)...then(E) for a chain of actions.
+   * @param actions actions as computable to execute
+   * @param kind is it 'all { ... }' or 'A.then(B)'?
+   * @param actionId given the action index, return the id that produced this action
+   * @returns evaluation result
+   */
+  private chainAllOrThen(
+    actions: Computable[],
+    kind: 'all' | 'then',
+    actionId: (idx: number) => bigint
+  ): Maybe<EvalResult> {
     // save the values of the next variables, as actions may update them
     const savedValues = this.snapshotNextVars()
     const savedTrace = this.trace()
@@ -1270,14 +1280,27 @@ export class CompilerVisitor implements IRVisitor {
     for (const action of actions) {
       nactionsLeft--
       result = action.eval()
-      if (result.isNone() || !(result.value as RuntimeValue).toBool()) {
+      const isFalse = result.isJust() && !(result.value as RuntimeValue).toBool()
+      if (result.isNone() || isFalse) {
         // As soon as one of the arguments does not evaluate to true,
         // break out of the loop.
         // Restore the values of the next variables,
         // as evaluation was not successful.
         this.recoverNextVars(savedValues)
         this.resetTrace(just(rv.mkList(savedTrace)))
-        break
+
+        if (kind === 'then' && nactionsLeft > 0 && isFalse) {
+          // Cannot extend a run. Emit an error message.
+          const actionNo = actions.length - (nactionsLeft + 1)
+          this.errorTracker.addRuntimeError(
+            actionId(actionNo),
+            'QNT513',
+            `Cannot continue in A.then(B), A evaluates to 'false'`
+          )
+          return none()
+        } else {
+          return result
+        }
       }
 
       // switch to the next frame, when implementing A.then(B)
@@ -1302,7 +1325,7 @@ export class CompilerVisitor implements IRVisitor {
     const args = this.compStack.splice(-app.args.length)
 
     const kind = app.opcode === 'then' ? 'then' : 'all'
-    const lazyCompute = () => this.chainAllOrThen(args, kind)
+    const lazyCompute = () => this.chainAllOrThen(args, kind, idx => app.args[idx].id)
 
     this.compStack.push(mkFunComputable(lazyCompute))
   }
@@ -1384,7 +1407,8 @@ export class CompilerVisitor implements IRVisitor {
               },
             }
           })
-          return this.chainAllOrThen(actions, 'then')
+          // In case the case of reps, we have multiple copies of the same action. This is why all occurrences have the same id.
+          return this.chainAllOrThen(actions, 'then', _ => app.args[1].id)
         })
         .join()
     }

diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts
@@ -3,7 +3,7 @@ import { assert } from 'chai'
 import { Either, left, right } from '@sweet-monads/either'
 import { just } from '@sweet-monads/maybe'
 import { expressionToString } from '../../src/ir/IRprinting'
-import { Computable, ComputableKind, fail, kindName } from '../../src/runtime/runtime'
+import { Callable, Computable, ComputableKind, fail, kindName } from '../../src/runtime/runtime'
 import { noExecutionListener } from '../../src/runtime/trace'
 import {
   CompilationContext,
@@ -80,56 +80,84 @@ function assertVarExists(kind: ComputableKind, name: string, input: string) {
   res.mapLeft(m => assert.fail(m))
 }
 
+// compile a computable for a run definition
+function callableFromContext(ctx: CompilationContext, callee: string): Either<string, Callable> {
+  let key = undefined
+  const lastModule = ctx.compilationState.modules[ctx.compilationState.modules.length - 1]
+  const def = lastModule.declarations.find(def => def.kind === 'def' && def.name === callee)
+  if (!def) {
+    return left(`${callee} definition not found`)
+  }
+  key = kindName('callable', def.id)
+  if (!key) {
+    return left(`${callee} not found`)
+  }
+  const run = ctx.evaluationState.context.get(key) as Callable
+  if (!run) {
+    return left(`${callee} not found via ${key}`)
+  }
+
+  return right(run)
+}
+
 // Scan the context for a callable. If found, evaluate it and return the value of the given var.
-// Assumes the input has a single callable
-// `callee` is used for error reporting.
-function evalVarAfterCall(varName: string, callee: string, input: string): Either<string, string> {
+// Assumes the input has a single definition whose name is stored in `callee`.
+function evalVarAfterRun(varName: string, callee: string, input: string): Either<string, string> {
   // use a combination of Maybe and Either.
   // Recall that left(...) is used for errors,
   // whereas right(...) is used for non-errors in sweet monads.
   const callback = (ctx: CompilationContext): Either<string, string> => {
-    let key = undefined
-    const lastModule = ctx.compilationState.modules[ctx.compilationState.modules.length - 1]
-    const def = lastModule.declarations.find(def => def.kind === 'def' && def.name === callee)
-    if (!def) {
-      return left(`${callee} definition not found`)
-    }
-    key = kindName('callable', def.id)
-    if (!key) {
-      return left(`${callee} not found`)
-    }
-    const run = ctx.evaluationState.context.get(key)
-    if (!run) {
-      return left(`${callee} not found via ${key}`)
-    }
+    return callableFromContext(ctx, callee)
+      .mapRight(run => {
+        return run
+          .eval()
+          .map(res => {
+            if ((res as RuntimeValue).toBool() === true) {
+              // extract the value of the state variable
+              const nextVal = (ctx.evaluationState.context.get(kindName('nextvar', varName)) ?? fail).eval()
+              if (nextVal.isNone()) {
+                return left(`Value of the variable ${varName} is undefined`)
+              } else {
+                return right(expressionToString(nextVal.value.toQuintEx(idGen)))
+              }
+            } else {
+              const s = expressionToString(res.toQuintEx(idGen))
+              const m = `Callable ${callee} was expected to evaluate to true, found: ${s}`
+              return left<string, string>(m)
+            }
+          })
+          .or(just(left(`Value of ${callee} is undefined`)))
+          .unwrap()
+      })
+      .join()
+  }
 
-    return run
-      .eval()
-      .map(res => {
-        if ((res as RuntimeValue).toBool() === true) {
-          // extract the value of the state variable
-          const nextVal = (ctx.evaluationState.context.get(kindName('nextvar', varName)) ?? fail).eval()
-          // using if-else, as map-or-unwrap confuses the compiler a lot
-          if (nextVal.isNone()) {
-            return left(`Value of the variable ${varName} is undefined`)
-          } else {
-            return right(expressionToString(nextVal.value.toQuintEx(idGen)))
-          }
-        } else {
-          const s = expressionToString(res.toQuintEx(idGen))
-          const m = `Callable ${callee} was expected to evaluate to true, found: ${s}`
-          return left<string, string>(m)
-        }
+  return evalInContext(input, callback)
+}
+
+// Evaluate a run and return the result.
+function evalRun(callee: string, input: string): Either<string, string> {
+  // Recall that left(...) is used for errors,
+  // whereas right(...) is used for non-errors in sweet monads.
+  const callback = (ctx: CompilationContext): Either<string, string> => {
+    return callableFromContext(ctx, callee)
+      .mapRight(run => {
+        return run
+          .eval()
+          .map(res => {
+            return right<string, string>(expressionToString(res.toQuintEx(idGen)))
+          })
+          .or(just(left(`Value of ${callee} is undefined`)))
+          .unwrap()
       })
-      .or(just(left(`Value of ${callee} is undefined`)))
-      .unwrap()
+      .join()
   }
 
   return evalInContext(input, callback)
 }
 
 function assertVarAfterCall(varName: string, expected: string, callee: string, input: string) {
-  evalVarAfterCall(varName, callee, input)
+  evalVarAfterRun(varName, callee, input)
     .mapLeft(m => assert.fail(m))
     .mapRight(output => assert(expected === output, `Expected ${varName} == ${expected}, found ${output}`))
 }
@@ -933,7 +961,7 @@ describe('compiling specs to runtime values', () => {
   })
 
   describe('compile runs', () => {
-    it('then', () => {
+    it('then ok', () => {
       const input = dedent(
         `var n: int
         |run run1 = (n' = 1).then(n' = n + 2).then(n' = n * 4)
@@ -943,6 +971,30 @@ describe('compiling specs to runtime values', () => {
       assertVarAfterCall('n', '12', 'run1', input)
     })
 
+    it('then fails when rhs is unreachable', () => {
+      const input = dedent(
+        `var n: int
+        |run run1 = (n' = 1).then(all { n == 0, n' = n + 2 }).then(n' = 3)
+        `
+      )
+
+      evalRun('run1', input)
+        .mapRight(result => assert.fail(`Expected the run to fail, found: ${result}`))
+        .mapLeft(m => assert.equal(m, 'Value of run1 is undefined'))
+    })
+
+    it('then returns false when rhs is false', () => {
+      const input = dedent(
+        `var n: int
+        |run run1 = (n' = 1).then(all { n == 0, n' = n + 2 })
+        `
+      )
+
+      evalRun('run1', input)
+        .mapRight(result => assert.equal(result, 'false'))
+        .mapLeft(m => assert.fail(`Expected the run to return false, found: ${m}`))
+    })
+
     it('reps', () => {
       const input = dedent(
         `var n: int
@@ -958,14 +1010,26 @@ describe('compiling specs to runtime values', () => {
       assertVarAfterCall('hist', 'List(0, 1, 2)', 'run2', input)
     })
 
+    it('reps fails when action is false', () => {
+      const input = dedent(
+        `var n: int
+        |run run1 = (n' = 0).then(10.reps(i => all { n < 5, n' = n + 1 }))
+        `
+      )
+
+      evalRun('run1', input)
+        .mapRight(result => assert.fail(`Expected the run to fail, found: ${result}`))
+        .mapLeft(m => assert.equal(m, 'Value of run1 is undefined'))
+    })
+
     it('fail', () => {
       const input = dedent(
         `var n: int
         |run run1 = (n' = 1).fail()
         `
       )
 
-      evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+      evalVarAfterRun('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
     })
 
     it('assert', () => {
@@ -975,7 +1039,7 @@ describe('compiling specs to runtime values', () => {
         `
       )
 
-      evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected an error, found: ${m}`))
+      evalVarAfterRun('n', 'run1', input).mapRight(m => assert.fail(`Expected an error, found: ${m}`))
     })
 
     it('expect fails', () => {
@@ -985,7 +1049,7 @@ describe('compiling specs to runtime values', () => {
         `
       )
 
-      evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+      evalVarAfterRun('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
     })
 
     it('expect ok', () => {
@@ -1005,7 +1069,7 @@ describe('compiling specs to runtime values', () => {
         `
       )
 
-      evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+      evalVarAfterRun('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
     })
 
     it('expect and then expect fail', () => {
@@ -1015,7 +1079,7 @@ describe('compiling specs to runtime values', () => {
         `
       )
 
-      evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+      evalVarAfterRun('n', 'run1', input).mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
     })
 
     it('q::debug', () => {