Skip to content

Commit

Permalink
Update mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/opti…
Browse files Browse the repository at this point in the history
…ons.scala
  • Loading branch information
Shon Feder committed Sep 9, 2022
1 parent 559a71e commit 42ea3c4
Showing 1 changed file with 26 additions and 29 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -573,35 +573,32 @@ object OptionGroup extends LazyLogging {
extends OptionGroup

object Checker extends Configurable[Config.Checker, Checker] with LazyLogging {
def apply(checker: Config.Checker): Try[Checker] = {
val configured = for {
algo <- checker.algo.toTry("checker.algo")
discardDisabled <- checker.discardDisabled.toTry("checker.discardDisabled")
length <- checker.length.toTry("checker.length")
maxError <- checker.maxError.toTry("checker.maxError")
noDeadlocks <- checker.noDeadlocks.toTry("checker.noDeadlocks")
nworkers <- checker.nworkers.toTry("checker.nworkers")
smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding")
tuning <- checker.tuning.toTry("checker.tuning")
} yield Checker(
algo = algo,
discardDisabled = discardDisabled,
length = length,
maxError = maxError,
noDeadlocks = noDeadlocks,
nworkers = nworkers,
smtEncoding = smtEncoding,
tuning = tuning,
)
// do some validation
configured.foreach(c =>
if (checker.view.isEmpty && c.maxError > 1) {
throw new PassOptionException(s"Option maxError = ${c.maxError} requires a view. None specified.")
})
// produce the configured checker
configured
}
}
def apply(checker: Config.Checker): Try[Checker] = for {
algo <- checker.algo.toTry("checker.algo")
discardDisabled <- checker.discardDisabled.toTry("checker.discardDisabled")
length <- checker.length.toTry("checker.length")
noDeadlocks <- checker.noDeadlocks.toTry("checker.noDeadlocks")
nworkers <- checker.nworkers.toTry("checker.nworkers")
smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding")
tuning <- checker.tuning.toTry("checker.tuning")
maxError <- checker.maxError.toTry("checker.maxError").flatMap { n =>
if (n > 1 && checker.view.isEmpty) {
val msg = s"Option maxError = ${n} requires a view. None specified."
Failure(new PassOptionException(msg))
} else {
Success(n)
}
}
} yield Checker(
algo = algo,
discardDisabled = discardDisabled,
length = length,
maxError = maxError,
noDeadlocks = noDeadlocks,
nworkers = nworkers,
smtEncoding = smtEncoding,
tuning = tuning,
)

////////////////
// Interfaces //
Expand Down

0 comments on commit 42ea3c4

Please sign in to comment.