Utils.scala 2.97 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
package de.tum.workflows

3
import de.tum.workflows.blocks._
Christian Müller's avatar
Christian Müller committed
4
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
5 6
import java.io.File
import java.io.PrintWriter
Christian Müller's avatar
Christian Müller committed
7 8
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvProperties
Christian Müller's avatar
Christian Müller committed
9

Christian Müller's avatar
Christian Müller committed
10
object Utils {
11

Christian Müller's avatar
Christian Müller committed
12 13
  val RESULTSFOLDER = "results"

14
  def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = {
Christian Müller's avatar
Christian Müller committed
15 16
    if (string.isEmpty) "" else string.mkString(start, mid, end)
  }
17 18 19 20 21 22 23 24 25 26

  def collectChoices(w: Block): List[Fun] = {
    w match {
      case Loop(steps)                     => steps.flatMap(collectChoices _)
      case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
      case b: ForallBlock                  => List()
      case NondetChoice(l, r)              => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
    }
  }

27 28
  def allchoices(w: Workflow) = {
    w.steps flatMap (collectChoices _) toSet
Christian Müller's avatar
Christian Müller committed
29
  }
30 31 32 33

  def indentLines(s: String) = {
    s.lines.map("  " + _).mkString("\n")
  }
Christian Müller's avatar
Christian Müller committed
34 35

  def time[R](block: => R) = {
Christian Müller's avatar
Christian Müller committed
36
    val t0 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
37
    val result = block // call-by-name
Christian Müller's avatar
Christian Müller committed
38
    val t1 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
    ((t1 - t0) / 1000000, result)
  }

  def clear() {
    def recclear(folder: File) {
      for (fol <- folder.listFiles() if fol.isDirectory()) {
        recclear(fol)
      }

      folder.listFiles().foreach(_.delete())
    }
    val fol = new File(RESULTSFOLDER)
    fol.mkdirs()
    recclear(fol)
  }
Christian Müller's avatar
Christian Müller committed
54
  
Christian Müller's avatar
Christian Müller committed
55 56
  def write(name: String, prop: String) {
    val file = new File(s"$RESULTSFOLDER/$name")
Christian Müller's avatar
Christian Müller committed
57 58 59
    if (file.exists()) {
      file.delete()
    }
Christian Müller's avatar
Christian Müller committed
60 61 62 63
    file.getParentFile.mkdirs()
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
Christian Müller's avatar
Christian Müller committed
64
  }
Christian Müller's avatar
Christian Müller committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
  
  def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
    val model = if (properties.stubborn) "stubborn" else "causal"
		val filenames = s"${name}_${model}_${desc}"
    // do not blow up the formula with auxilliary elimination
    val (res, graph, labelling, provens, dot, time) = 
      InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
    for ((s, i) <- dot.zipWithIndex) {
      Utils.write(s"${filenames}_${i}.dot", s)
    }
    val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
      true
    }
    val wfsize = graph.edges.size - 1
    val invsizes = labelling.last.map(_._2.opsize())
    val maxsize = invsizes.max
    val avgsize = invsizes.sum / invsizes.size
    Utils.write(s"${filenames}.metrics",
        s"""Name: $name
         Description: $desc
         Invariant: $inv
         Model: $model
         Result: ${if (!res) "not " else ""}inductive
         WF size: $wfsize
         Time: $time ms
         Proof steps: ${dot.size}
         Strengthenings: ${strengthenings.size}
         Largest Inv: ${maxsize}
         Average Inv: ${avgsize}""")
    res
  }
  
  def check(name:String, desc:String, inv:Formula, properties:InvProperties):Boolean = {
    val spec = ExampleWorkflows.parseExample(name).get
    check(name, desc, inv, spec, properties)
  }
Christian Müller's avatar
Christian Müller committed
101
}