InvariantCLI.scala 1.92 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7
package de.tum.workflows

import scala.io.Source

import com.typesafe.scalalogging.LazyLogging

import de.tum.workflows.Utils._
Christian Müller's avatar
Christian Müller committed
8
import de.tum.workflows.blocks.NISpec
Christian Müller's avatar
Christian Müller committed
9 10 11 12 13 14 15 16 17 18 19 20 21
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
import java.io.File

object InvariantCLI extends App with LazyLogging {

  lazy val usage = """
    Usage invariants.jar [--causal] [--elimChoice] FILE
    
    FILE should be a path to a Workflow Description File.
    If --causal is given, all agents are assumed to be causal, otherwise all agents are assumed to be stubborn.
    If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
Christian Müller's avatar
Christian Müller committed
22
      With elimChoice turned off, that corresponds to choice predicates not changing over time.
Christian Müller's avatar
Christian Müller committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
  """

  if (args.length == 0) {
    logger.info(usage)
  } else {

    var causal = false
    var elim = false
    args.collect {
      case "--causal"     => causal = true
      case "--elimChoice" => elim = true
    }
    val properties = InvProperties(!causal, elim)

    val file = args.last

    logger.info(s"Using $file")

    val source = Source.fromFile(file).mkString
    val spec = WorkflowParser.parseSpec(source)
    if (!spec.successful) {
      logger.error(s"Parsing of $file unsuccessful: $spec")
      None
    } else {
      if (!spec.get.checkSanity()) {
        logger.error(s"Sanity check of $file failed. Skipping file.")
        None
      } else {
        Some(spec.get)
      }
    }

    spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
  }

Christian Müller's avatar
Christian Müller committed
58
  def generate(name: String, spec: NISpec, properties: InvProperties) {
Christian Müller's avatar
Christian Müller committed
59 60
    logger.info(s"Encoding Spec:\n$spec")

Christian Müller's avatar
Christian Müller committed
61
    def invariant = InvariantGenerator.invariantNoninterSingleBS(spec)
Christian Müller's avatar
Christian Müller committed
62 63 64 65 66

    Utils.check(name, "", invariant, spec, properties)
  }

}