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

3 4
import de.tum.niwo.blocks._
import de.tum.niwo.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

Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.toz3.Z3BSFO
9
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
10
import de.tum.niwo.graphs.WFGraphEncoding
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.invariants.{InvProperties, InvariantChecker}
Christian Müller's avatar
Christian Müller committed
12

13
object Utils extends LazyLogging {
14

Christian Müller's avatar
Christian Müller committed
15
  val RESULTSFOLDER = "results"
Christian Müller's avatar
src  
Christian Müller committed
16
  val DEBUG_MODE = true
Christian Müller's avatar
Christian Müller committed
17

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

22
  def collectChoices(w: WFBlock): List[Fun] = {
23
    w match {
24 25
      case l:WFLoop                           => l.steps.flatMap(collectChoices)
      case nd:WFNondetChoice                   => nd.left.flatMap(collectChoices) ++ nd.right.flatMap(collectChoices)
26
      case ForallMayWFBlock(agents, pred, _) => List(Fun(pred, agents))
27
      case _: ForallWFBlock                  => List()
28 29 30
    }
  }

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

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

  def time[R](block: => R) = {
Christian Müller's avatar
Christian Müller committed
40
    val t0 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
41
    val result = block // call-by-name
Christian Müller's avatar
Christian Müller committed
42
    val t1 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
    ((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
58
  
59 60
  def write(dir: String, filename:String, prop: String) {
    val file = new File(s"$RESULTSFOLDER/$dir/$filename")
Christian Müller's avatar
Christian Müller committed
61 62 63
    if (file.exists()) {
      file.delete()
    }
Christian Müller's avatar
Christian Müller committed
64 65 66 67
    file.getParentFile.mkdirs()
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
68
    logger.info(s"Written $file")
Christian Müller's avatar
Christian Müller committed
69
  }
Christian Müller's avatar
Christian Müller committed
70 71 72 73 74

  def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = {
    val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
    check(name, desc, invspec, properties)
  }
Christian Müller's avatar
Christian Müller committed
75
  
Christian Müller's avatar
Christian Müller committed
76
  def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
Christian Müller's avatar
Christian Müller committed
77
    val model = if (properties.stubborn) "stubborn" else "causal"
78 79 80 81

    val basename = name.split("/").last
		val filenames = s"${basename}_$model${if (desc.isEmpty()) "" else s"_$desc"}"

Christian Müller's avatar
Christian Müller committed
82
    val (res, graph, labelling, provens, dot, time) =
Christian Müller's avatar
Christian Müller committed
83
      InvariantChecker.checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
84

Christian Müller's avatar
Christian Müller committed
85
    logger.info(s"Invariant was ${spec.inv}")
Christian Müller's avatar
Christian Müller committed
86 87
    logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $time ms)\n")

Christian Müller's avatar
Christian Müller committed
88 89
    if (!res) {
      val headinv = labelling.last(graph.nodes.head)
90
      val satq = And(spec.axioms, Neg(headinv))
Christian Müller's avatar
Christian Müller committed
91 92 93
      logger.info(s"Initial state violating the invariant: ${Z3BSFO.debugmodelBS(satq)}")
    }

Christian Müller's avatar
Christian Müller committed
94
    for ((s, i) <- dot.zipWithIndex) {
95
      Utils.write(name,s"${filenames}_$i.dot", s)
Christian Müller's avatar
Christian Müller committed
96 97 98 99
    }
    val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
      true
    }
100

Christian Müller's avatar
Christian Müller committed
101 102 103
    // FIXME move this
//    val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
//    Utils.write(name, s"${filenames}_elaborated.dot", elabdot)
104

105
    val labels = (for ((node, inv) <- labelling.last) yield {
Christian Müller's avatar
Christian Müller committed
106
      s"Node ${node}:\n${inv.pretty}\n"
107 108
    }).mkString("\n")
    
109
    Utils.write(name, s"$filenames.invariants", labels)
110
    
Christian Müller's avatar
Christian Müller committed
111
    val wfsize = graph.edges.size - 1
Christian Müller's avatar
Christian Müller committed
112
    val invsizes = labelling.last.map(_._2.opsize)
Christian Müller's avatar
Christian Müller committed
113 114
    val maxsize = invsizes.max
    val avgsize = invsizes.sum / invsizes.size
115
    Utils.write(name, s"$filenames.metrics",
Christian Müller's avatar
Christian Müller committed
116
        s"""Name: $name
Christian Müller's avatar
Christian Müller committed
117 118 119 120 121 122 123 124 125 126 127 128
        |Description: $desc
        |  Invariant:
        |${spec.inv.pretty.lines.map(s => "            " + s).mkString("\n")}
        |  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""".stripMargin
    )
Christian Müller's avatar
Christian Müller committed
129 130 131
    res
  }
  
Christian Müller's avatar
Christian Müller committed
132
  def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
133
    val spec = Examples.parseExampleWF(name).get
Christian Müller's avatar
Christian Müller committed
134 135
    check(name, desc, inv, spec, properties)
  }
Christian Müller's avatar
Christian Müller committed
136
}