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 21 22 23 24 25 26 27

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

28 29
  def allchoices(w: Workflow) = {
    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"
70 71
		val filenames = s"${name}_${model}${if (desc.isEmpty()) "" else s"_$desc"}"
		
Christian Müller's avatar
Christian Müller committed
72 73 74 75 76 77 78 79 80
    // 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
    }
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 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
    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
111
}