WFCLI.scala 2.23 KB
Newer Older
1 2 3 4
package de.tum.niwo

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

import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.WorkflowParser

Christian Müller's avatar
Christian Müller committed
13
object WFCLI extends App with LazyLogging {
14 15

  lazy val usage = """
Christian Müller's avatar
Christian Müller committed
16 17
    Usage niwo-wf.jar [--stubborn] [--elimChoice] FILE
    
18
    FILE should be a path to a Workflow Description File.
Christian Müller's avatar
Christian Müller committed
19
    If --stubborn is given, all agents are assumed to be stubborn.
Christian Müller's avatar
Christian Müller committed
20 21 22 23
    If --approxChoice is given, all A predicates will be eliminated only after termination
      of the fixpoint algorithm. (may sometimes improve performance)
      immediately eliminated from the precondition.
      Turning approxChoice on corresponds to A predicates not changing over time.
Christian Müller's avatar
Christian Müller committed
24 25
    If --approxElim is given, second order quantifier elimination is further approximated by not computing CNF for formulas that are too large.
      This achieves a tremendous speed boost at the cost of accuracy.
26 27 28 29 30 31
  """

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

Christian Müller's avatar
Christian Müller committed
32
    var causal = true
Christian Müller's avatar
Christian Müller committed
33
    var elimA = true
Christian Müller's avatar
Christian Müller committed
34
    var approxelim = false
35
    args.collect {
Christian Müller's avatar
Christian Müller committed
36
      case "--stubborn"   => causal = false
Christian Müller's avatar
Christian Müller committed
37
      case "--approxChoice" => elimA = false
Christian Müller's avatar
Christian Müller committed
38
      case "--approxElim" => approxelim = true
39
    }
Christian Müller's avatar
Christian Müller committed
40
    val properties = InvProperties(stubborn = !causal, eliminateA = elimA, approxElim = approxelim)
41 42 43 44

    val file = args.last

    logger.info(s"Using $file")
Christian Müller's avatar
Christian Müller committed
45

46 47 48 49
    val source = Utils.using(Source.fromFile(file)) { source => source.mkString }
    val spec = WorkflowParser.parseSpec(source)
    if (!spec.successful) {
      logger.error(s"Parsing of $file unsuccessful: $spec")
Christian Müller's avatar
Christian Müller committed
50
      None
51
    } else {
Christian Müller's avatar
Christian Müller committed
52
      if (!spec.get.isSane()) {
53
        logger.error(s"Sanity check of $file failed. Skipping file.")
Christian Müller's avatar
Christian Müller committed
54
        None
55
      } else {
Christian Müller's avatar
Christian Müller committed
56
        Some(spec.get)
57 58
      }
    }
Christian Müller's avatar
Christian Müller committed
59 60

    spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
61
  }
Christian Müller's avatar
Christian Müller committed
62 63 64 65 66 67 68 69 70 71

  def generate(name: String, spec: NISpec, properties: InvProperties) {
    logger.info(s"Encoding Spec:\n$spec")

    def invariant = InvariantGenerator.invariantNoninterSingleBS _

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

}