From ada23233afca38b59c3599f264fa527e9aabb9bd Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 19 Oct 2023 16:09:12 +0200 Subject: [PATCH] Fix deadlock log message (#2760) --- .../apalache/tla/bmcmt/passes/VCGenPassImpl.scala | 13 ++++++++----- 1 file changed, 8 insertions(+), 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 index 93b3863229..710d3c9d4a 100644 --- 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) }