WFCLI.scala 1.94 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 20 21
    If --stubborn is given, all agents are assumed to be stubborn ignoring the model given in the specification file.
    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)
      With elimChoice turned off, that corresponds to choice predicates not changing over time.
22 23 24 25 26 27
  """

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

Christian Müller's avatar
Christian Müller committed
28 29
    var causal = true
    var elim = false
30
    args.collect {
Christian Müller's avatar
Christian Müller committed
31 32
      case "--stubborn"   => causal = false
      case "--elimChoice" => elim = true
33
    }
Christian Müller's avatar
Christian Müller committed
34
    val properties = InvProperties(!causal, elim)
35 36 37 38

    val file = args.last

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

40 41 42 43
    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
44
      None
45
    } else {
Christian Müller's avatar
Christian Müller committed
46
      if (!spec.get.isSane()) {
47
        logger.error(s"Sanity check of $file failed. Skipping file.")
Christian Müller's avatar
Christian Müller committed
48
        None
49
      } else {
Christian Müller's avatar
Christian Müller committed
50
        Some(spec.get)
51 52
      }
    }
Christian Müller's avatar
Christian Müller committed
53 54

    spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, properties))
55
  }
Christian Müller's avatar
Christian Müller committed
56 57 58 59 60 61 62 63 64 65

  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)
  }

}