From c87725605f7d9feeee157445fa6cdc9bb0f0b932 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 16 Oct 2023 15:32:11 +0200 Subject: [PATCH] Continue simulation on SMT timeout in enabledness check (#2758) * Continue simulation on SMT timeout * Update changelog --- .unreleased/bug-fixes/2758-sim-timeout.md | 1 + .../at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala | 8 ++++++-- 2 files changed, 7 insertions(+), 2 deletions(-) create mode 100644 .unreleased/bug-fixes/2758-sim-timeout.md diff --git a/.unreleased/bug-fixes/2758-sim-timeout.md b/.unreleased/bug-fixes/2758-sim-timeout.md new file mode 100644 index 0000000000..6710887e62 --- /dev/null +++ b/.unreleased/bug-fixes/2758-sim-timeout.md @@ -0,0 +1 @@ +Continue simulation on SMT timeout in enabledness check, see #2758 diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala index e725879794..e7360504ff 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala @@ -262,8 +262,12 @@ class SeqModelChecker[ExecutorContextT]( logger.info(s"Step ${trex.stepNo}: Transition #$no is disabled") case None => - searchState.onResult(RuntimeError()) - return (Set.empty, Set.empty) // UNKNOWN or timeout + if (params.isRandomSimulation) { + logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled") + } else { + searchState.onResult(RuntimeError()) + return (Set.empty, Set.empty) // UNKNOWN or timeout + } } // recover from the snapshot trex.recover(snapshot.get)