fix

Author: myfreess

counter_test.mbt

@@ -3,7 +3,7 @@
 // The model is the single integer value that a correct mutable counter should
 // contain after each prefix of the command program. `CounterIncr` advances that
 // model by one, while `CounterGet` observes it. The property under test is the
-// basic state-machine lockstep property from the blogs: after each concrete
+// basic state-machine lockstep property : after each concrete
 // command, the observed response must match the response predicted by the pure
 // model.
 fn case_config(
@@ -188,9 +188,22 @@ test "counter passes against faithful implementation" {
     counter_script_spec(commands),
     config=case_config(max_commands=commands.length()),
   )
-  assert_eq(summary.cases_run, 1)
-  assert_eq(summary.commands_run, 4)
-  assert_eq(summary.command_distribution.length(), 2)
+  inspect(summary.cases_run, content="1")
+  inspect(summary.commands_run, content="4")
+  inspect(
+    @debug.to_string(summary.command_distribution),
+    content="[(\"incr\", 2), (\"get\", 2)]",
+  )
+  inspect(
+    @quickcheck_statemachine.format_commands(summary.commands),
+    content=(
+      #|0: CounterIncr -> CounterIncrDone
+      #|1: CounterGet -> CounterGot(1)
+      #|2: CounterIncr -> CounterIncrDone
+      #|3: CounterGet -> CounterGot(2)
+      #|
+    ),
+  )
 }
 
 ///|
@@ -215,15 +228,19 @@ test "counter catches value 42 increment bug" {
         model~,
         next_model~,
         commands~,
+        logic~,
         ..
       )
     ) else {
     fail("expected counter postcondition failure")
   }
-  assert_eq(step_index, 43)
-  assert_true(command is CounterGet)
-  assert_true(response is CounterGot(42))
-  assert_eq(model, 43)
-  assert_eq(next_model, 43)
-  assert_eq(commands.length(), 44)
+  inspect(
+    "\{step_index}: \{@debug.to_string(command)} -> \{@debug.to_string(response)}, model=\{model}, next=\{next_model}",
+    content="43: CounterGet -> CounterGot(42), model=43, next=43",
+  )
+  inspect(commands.length(), content="44")
+  inspect(
+    @quickcheck_statemachine.format_counterexample(logic.counterexample()),
+    content="counter response matches model",
+  )
 }

filesystem_test.mbt

@@ -835,7 +835,7 @@ fn fs_sym_name(command : FsSymCommand) -> String {
 
 ///|
 // Labels used as coverage diagnostics:
-// The file-system example in the blog uses labels to make sure generated
+// The file-system example uses labels to make sure generated
 // programs cover meaningful behaviors, not just arbitrary command names. These
 // labels identify multi-open scenarios, successful reads, closed-handle writes,
 // and busy reads.
@@ -954,7 +954,7 @@ fn fs_unknown_handle_probe_spec() -> @quickcheck_statemachine.StateMachine[
 // exist, reified at execution time, and still satisfy the pure model. The
 // required labels assert that the scenario covers both multiple open handles and
 // at least one successful read.
-test "qsm blog filesystem open-write-read examples pass with symbolic handles" {
+test "qsm filesystem open-write-read examples pass with symbolic handles" {
   let root = fs_root_dir()
   let z = fs_dir(["z"])
   let a = fs_file(root, "a")
@@ -980,7 +980,29 @@ test "qsm blog filesystem open-write-read examples pass with symbolic handles" {
       "OpenTwo", "SuccessfulRead",
     ]),
   )
-  assert_eq(summary.commands_run, commands.length())
+  inspect(summary.commands_run, content="12")
+  inspect(
+    @debug.to_string(summary.labels),
+    content="[\"OpenTwo\", \"SuccessfulRead\"]",
+  )
+  inspect(
+    @quickcheck_statemachine.format_commands(summary.commands),
+    content=(
+      #|0: FsSymOpen({ dir: { parts: [] }, name: "a" }) -> FsSymSucceeded(FsSymHandle({ id: 0 }))
+      #|1: FsSymOpen({ dir: { parts: [] }, name: "b" }) -> FsSymSucceeded(FsSymHandle({ id: 1 }))
+      #|2: FsSymWrite(Symbolic({ id: 0 }), "Hi") -> FsSymSucceeded(FsSymUnit)
+      #|3: FsSymWrite(Symbolic({ id: 1 }), "Bye") -> FsSymSucceeded(FsSymUnit)
+      #|4: FsSymClose(Symbolic({ id: 0 })) -> FsSymSucceeded(FsSymUnit)
+      #|5: FsSymRead({ dir: { parts: [] }, name: "a" }) -> FsSymSucceeded(FsSymText("Hi"))
+      #|6: FsSymClose(Symbolic({ id: 1 })) -> FsSymSucceeded(FsSymUnit)
+      #|7: FsSymRead({ dir: { parts: [] }, name: "b" }) -> FsSymSucceeded(FsSymText("Bye"))
+      #|8: FsSymMkDir({ parts: ["z"] }) -> FsSymSucceeded(FsSymUnit)
+      #|9: FsSymOpen({ dir: { parts: ["z"] }, name: "b" }) -> FsSymSucceeded(FsSymHandle({ id: 2 }))
+      #|10: FsSymClose(Symbolic({ id: 2 })) -> FsSymSucceeded(FsSymUnit)
+      #|11: FsSymRead({ dir: { parts: ["z"] }, name: "b" }) -> FsSymSucceeded(FsSymText(""))
+      #|
+    ),
+  )
 }
 
 ///|
@@ -989,7 +1011,7 @@ test "qsm blog filesystem open-write-read examples pass with symbolic handles" {
 // introduced that variable. The property checks that generation exhausts its
 // retries and reports a deadlock at step zero instead of producing a program
 // that would fail later during reification.
-test "qsm blog precondition rejects handles that were never created" {
+test "qsm precondition rejects handles that were never created" {
   let result = @quickcheck_statemachine.check(
     fs_unknown_handle_probe_spec(),
     config=case_config(max_commands=1, max_tries=3),
@@ -1000,9 +1022,12 @@ test "qsm blog precondition rejects handles that were never created" {
     ) else {
     fail("expected unknown handle to exhaust generation attempts")
   }
-  assert_eq(step_index, 0)
-  assert_eq(model.created_handles.length(), 0)
-  assert_eq(commands.length(), 0)
+  inspect(step_index, content="0")
+  inspect(
+    @debug.to_string(model),
+    content="{ dirs: [{ parts: [] }], files: [], handles: [], created_handles: [] }",
+  )
+  inspect(@quickcheck_statemachine.format_commands(commands), content="")
 }
 
 ///|
@@ -1012,7 +1037,7 @@ test "qsm blog precondition rejects handles that were never created" {
 // the intentionally liberal precondition: closed-handle writes remain legal test
 // commands so the model can verify the expected `HandleClosed` response and the
 // label can record that coverage.
-test "qsm blog precondition still allows closed handle errors" {
+test "qsm precondition still allows closed handle errors" {
   let root = fs_root_dir()
   let a = fs_file(root, "a")
   let commands : Array[FsSymCommand] = [
@@ -1026,7 +1051,23 @@ test "qsm blog precondition still allows closed handle errors" {
       "ClosedHandleWrite",
     ]),
   )
-  assert_eq(summary.commands_run, 3)
+  inspect(summary.commands_run, content="3")
+  inspect(@debug.to_string(summary.labels), content="[\"ClosedHandleWrite\"]")
+  inspect(
+    @quickcheck_statemachine.format_history(summary.history),
+    content=(
+      #|Invocation(
+      #|  pid={ id: 0 },
+      #|  command=FsOpen({ dir: { parts: [] }, name: "a" }),
+      #|)
+      #|Response(pid={ id: 0 }, response=FsSucceeded(FsHandle(0)))
+      #|Invocation(pid={ id: 1 }, command=FsClose(0))
+      #|Response(pid={ id: 1 }, response=FsSucceeded(FsUnit))
+      #|Invocation(pid={ id: 2 }, command=FsWrite(0, "late write"))
+      #|Response(pid={ id: 2 }, response=FsFailed(FsHandleClosed))
+      #|
+    ),
+  )
 }
 
 ///|
@@ -1036,7 +1077,7 @@ test "qsm blog precondition still allows closed handle errors" {
 // The property verifies that the postcondition catches this mismatch and that
 // the recorded history contains the full three-command prefix needed to explain
 // the failure.
-test "qsm blog filesystem catches missing busy read check" {
+test "qsm filesystem catches missing busy read check" {
   let root = fs_root_dir()
   let a = fs_file(root, "a")
   let commands : Array[FsSymCommand] = [
@@ -1057,17 +1098,50 @@ test "qsm blog filesystem catches missing busy read check" {
         model~,
         next_model~,
         history~,
+        logic~,
         ..
       )
     ) else {
     fail("expected busy read mismatch")
   }
-  assert_eq(step_index, 2)
-  assert_true(command is FsRead(_))
-  assert_true(response is FsSucceeded(FsText("Hi")))
-  assert_true(fs_postcondition(model, command, response).eval() == false)
-  assert_true(next_model == model)
-  assert_eq(@quickcheck_statemachine.make_operations(history).length(), 3)
-  assert_eq(model.handles.length(), 1)
-  assert_true(model.handles[0].file == a)
+  inspect(
+    "\{step_index}: \{@debug.to_string(command)} -> \{@debug.to_string(response)}, postcondition=\{fs_postcondition(model, command, response).eval()}",
+    content=(
+      #|2: FsRead({ dir: { parts: [] }, name: "a" }) -> FsSucceeded(FsText("Hi")), postcondition=false
+    ),
+  )
+  inspect(
+    @debug.to_string(model),
+    content=(
+      #|{
+      #|  dirs: [{ parts: [] }],
+      #|  files: [{ file: { dir: { parts: [] }, name: "a" }, content: "Hi" }],
+      #|  handles: [{ handle: 0, file: { dir: { parts: [] }, name: "a" } }],
+      #|  next_handle: 1,
+      #|}
+    ),
+  )
+  inspect(next_model == model, content="true")
+  inspect(
+    @quickcheck_statemachine.format_history(history),
+    content=(
+      #|Invocation(
+      #|  pid={ id: 0 },
+      #|  command=FsOpen({ dir: { parts: [] }, name: "a" }),
+      #|)
+      #|Response(pid={ id: 0 }, response=FsSucceeded(FsHandle(0)))
+      #|Invocation(pid={ id: 1 }, command=FsWrite(0, "Hi"))
+      #|Response(pid={ id: 1 }, response=FsSucceeded(FsUnit))
+      #|Invocation(
+      #|  pid={ id: 2 },
+      #|  command=FsRead({ dir: { parts: [] }, name: "a" }),
+      #|)
+      #|Response(pid={ id: 2 }, response=FsSucceeded(FsText("Hi")))
+      #|
+    ),
+  )
+  inspect(
+    @quickcheck_statemachine.format_counterexample(logic.counterexample()),
+    content="filesystem response matches model",
+  )
 }

jug_test.mbt

@@ -143,14 +143,18 @@ fn jug_solution_spec() -> @quickcheck_statemachine.StateMachine[
 test "die hard jug model covers alternate commands" {
   let model = JugModel::{ big_jug: 1, small_jug: 2 }
   let fill_small = jug_next(model, JugFillSmall)
-  assert_eq(fill_small.big_jug, 1)
-  assert_eq(fill_small.small_jug, 3)
   let empty_big = jug_next(model, JugEmptyBig)
-  assert_eq(empty_big.big_jug, 0)
-  assert_eq(empty_big.small_jug, 2)
   let small_into_big = jug_next(model, JugSmallIntoBig)
-  assert_eq(small_into_big.big_jug, 3)
-  assert_eq(small_into_big.small_jug, 0)
+  inspect(
+    @debug.to_string([fill_small, empty_big, small_into_big]),
+    content=(
+      #|[
+      #|  { big_jug: 1, small_jug: 3 },
+      #|  { big_jug: 0, small_jug: 2 },
+      #|  { big_jug: 3, small_jug: 0 },
+      #|]
+    ),
+  )
 }
 
 ///|
@@ -174,18 +178,51 @@ test "die hard jug reports the 4 liter solution" {
         model~,
         next_model~,
         commands~,
+        history~,
+        logic~,
         ..
       )
     ) else {
     fail("expected jug solution to be reported as a postcondition failure")
   }
-  assert_eq(step_index, 5)
-  assert_true(command is JugBigIntoSmall)
-  assert_true(response is JugDone)
-  assert_eq(model.big_jug, 5)
-  assert_eq(model.small_jug, 2)
-  assert_eq(next_model.big_jug, 4)
-  assert_eq(next_model.small_jug, 3)
-  assert_eq(commands.length(), 6)
-  assert_true(commands.commands[4].command is JugFillBig)
+  inspect(
+    "\{step_index}: \{@debug.to_string(command)} -> \{@debug.to_string(response)}, model=\{@debug.to_string(model)}, next=\{@debug.to_string(next_model)}",
+    content=(
+      #|5: JugBigIntoSmall -> JugDone, model={ big_jug: 5, small_jug: 2 }, next={ big_jug: 4, small_jug: 3 }
+    ),
+  )
+  inspect(
+    @quickcheck_statemachine.format_commands(commands),
+    content=(
+      #|0: JugFillBig -> JugDone
+      #|1: JugBigIntoSmall -> JugDone
+      #|2: JugEmptySmall -> JugDone
+      #|3: JugBigIntoSmall -> JugDone
+      #|4: JugFillBig -> JugDone
+      #|5: JugBigIntoSmall -> JugBigJugIs4
+      #|
+    ),
+  )
+  inspect(
+    @quickcheck_statemachine.format_history(history),
+    content=(
+      #|Invocation(pid={ id: 0 }, command=JugFillBig)
+      #|Response(pid={ id: 0 }, response=JugDone)
+      #|Invocation(pid={ id: 1 }, command=JugBigIntoSmall)
+      #|Response(pid={ id: 1 }, response=JugDone)
+      #|Invocation(pid={ id: 2 }, command=JugEmptySmall)
+      #|Response(pid={ id: 2 }, response=JugDone)
+      #|Invocation(pid={ id: 3 }, command=JugBigIntoSmall)
+      #|Response(pid={ id: 3 }, response=JugDone)
+      #|Invocation(pid={ id: 4 }, command=JugFillBig)
+      #|Response(pid={ id: 4 }, response=JugDone)
+      #|Invocation(pid={ id: 5 }, command=JugBigIntoSmall)
+      #|Response(pid={ id: 5 }, response=JugDone)
+      #|
+    ),
+  )
+  inspect(
+    @quickcheck_statemachine.format_counterexample(logic.counterexample()),
+    content="jug reports 4 liter solution",
+  )
 }