InvariantCLI.scala 1.91 KB
Newer Older
1
package de.tum.niwo
Christian Müller's avatar
Christian Müller committed
2 3 4

import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
5 6
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.NISpec
Christian Müller's avatar
Christian Müller committed
7
import de.tum.niwo.invariants.InvariantChecker
Christian Müller's avatar
Christian Müller committed
8 9
import java.io.File

Christian Müller's avatar
Christian Müller committed
10
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
11 12
import de.tum.niwo.parser.WorkflowParser

Christian Müller's avatar
Christian Müller committed
13 14 15 16 17 18 19 20
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
21
      With elimChoice turned off, that corresponds to choice predicates not changing over time.
Christian Müller's avatar
Christian Müller committed
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
  """

  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 {
Christian Müller's avatar
Christian Müller committed
46
      if (!spec.get.isSane()) {
Christian Müller's avatar
Christian Müller committed
47 48 49 50 51 52 53 54 55 56
        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
57
  def generate(name: String, spec: NISpec, properties: InvProperties) {
Christian Müller's avatar
Christian Müller committed
58 59
    logger.info(s"Encoding Spec:\n$spec")

Christian Müller's avatar
Christian Müller committed
60
    def invariant = InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
61 62 63 64 65

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

}