Utils.scala 3.29 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
9
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
10

11
object Utils extends LazyLogging {
12

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

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

  def collectChoices(w: Block): List[Fun] = {
    w match {
Christian Müller's avatar
Christian Müller committed
21
      case Loop(steps)                     => steps.flatMap(collectChoices)
22 23 24 25 26 27
      case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
      case b: ForallBlock                  => List()
      case NondetChoice(l, r)              => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
    }
  }

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

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

  def time[R](block: => R) = {
Christian Müller's avatar
Christian Müller committed
37
    val t0 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
38
    val result = block // call-by-name
Christian Müller's avatar
Christian Müller committed
39
    val t1 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
    ((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
55
  
Christian Müller's avatar
Christian Müller committed
56 57
  def write(name: String, prop: String) {
    val file = new File(s"$RESULTSFOLDER/$name")
Christian Müller's avatar
Christian Müller committed
58 59 60
    if (file.exists()) {
      file.delete()
    }
Christian Müller's avatar
Christian Müller committed
61 62 63 64
    file.getParentFile.mkdirs()
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
65
    logger.info(s"Written $name")
Christian Müller's avatar
Christian Müller committed
66
  }
Christian Müller's avatar
Christian Müller committed
67 68 69
  
  def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
    val model = if (properties.stubborn) "stubborn" else "causal"
Christian Müller's avatar
Christian Müller committed
70
		val filenames = s"${name}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
71
		
Christian Müller's avatar
Christian Müller committed
72
    // do not blow up the formula with auxilliary elimination
Christian Müller's avatar
Christian Müller committed
73
    val (res, graph, labelling, provens, dot, time, headlabel) =
Christian Müller's avatar
Christian Müller committed
74 75
      InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
    for ((s, i) <- dot.zipWithIndex) {
Christian Müller's avatar
Christian Müller committed
76
      Utils.write(s"${filenames}_$i.dot", s)
Christian Müller's avatar
Christian Müller committed
77 78 79 80
    }
    val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
      true
    }
81 82 83 84 85 86 87
    
    val labels = (for ((node, inv) <- labelling.last) yield {
      s"Node ${node.value}:\n${inv.pretty()}\n"
    }).mkString("\n")
    
    Utils.write(s"$filenames.invariants", labels)
    
Christian Müller's avatar
Christian Müller committed
88 89 90 91
    val wfsize = graph.edges.size - 1
    val invsizes = labelling.last.map(_._2.opsize())
    val maxsize = invsizes.max
    val avgsize = invsizes.sum / invsizes.size
Christian Müller's avatar
Christian Müller committed
92
    Utils.write(s"$filenames.metrics",
Christian Müller's avatar
Christian Müller committed
93 94 95 96 97 98 99 100 101
        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}
Christian Müller's avatar
Christian Müller committed
102 103
         Largest Inv: $maxsize
         Average Inv: $avgsize""")
Christian Müller's avatar
Christian Müller committed
104 105 106 107 108 109 110
    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
111
}