InvariantCLI.scala 1.91 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
package de.tum.workflows

import scala.io.Source

import com.typesafe.scalalogging.LazyLogging

import de.tum.workflows.Utils._
import de.tum.workflows.blocks.Spec
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
cleanup    
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
58
59
60
  """

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

  def generate(name: String, spec: Spec, properties: InvProperties) {
    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)
  }

}