Fix deadlock log message (#2760)

apalache-mc · Oct 19, 2023 · ada2323 · ada2323
1 parent 2c336c1
commit ada2323
Showing 1 changed file with 8 additions and 5 deletions.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala
@@ -1,13 +1,14 @@
 package at.forsyte.apalache.tla.bmcmt.passes
 
+import at.forsyte.apalache.infra.passes.DerivedPredicates
 import at.forsyte.apalache.infra.passes.Pass.PassResult
+import at.forsyte.apalache.infra.passes.options.OptionGroup
 import at.forsyte.apalache.tla.bmcmt.VCGenerator
 import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
 import at.forsyte.apalache.io.lir.TlaWriterFactory
 import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
 import com.google.inject.Inject
 import com.typesafe.scalalogging.LazyLogging
-import at.forsyte.apalache.infra.passes.DerivedPredicates
 
 /**
  * The pass that generates verification conditions.
@@ -16,7 +17,8 @@ import at.forsyte.apalache.infra.passes.DerivedPredicates
  *   Igor Konnov
  */
 class VCGenPassImpl @Inject() (
-    derivedPreds: DerivedPredicates,
+    options: OptionGroup.HasChecker,
+    derivedPredicates: DerivedPredicates,
     tracker: TransformationTracker,
     writerFactory: TlaWriterFactory)
     extends VCGenPass with LazyLogging {
@@ -25,14 +27,15 @@ class VCGenPassImpl @Inject() (
 
   override def execute(tlaModule: TlaModule): PassResult = {
     val newModule =
-      derivedPreds.invariants match {
+      derivedPredicates.invariants match {
         case List() =>
-          logger.info("  > No invariant given. Only deadlocks will be checked")
+          val deadlockMsg = if (options.checker.noDeadlocks) "" else " Only deadlocks will be checked"
+          logger.info(s"  > No invariant given.${deadlockMsg}")
           tlaModule
         case invariants =>
           invariants.foldLeft(tlaModule) { (mod, invName) =>
             logger.info(s"  > Producing verification conditions from the invariant $invName")
-            val optView = derivedPreds.view
+            val optView = derivedPredicates.view
             optView.foreach { viewName => logger.info(s"  > Using state view ${viewName}") }
             new VCGenerator(tracker).gen(mod, invName, optView)
           }