Utils.scala 5.55 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.{TSGraphEncoding, WFGraphEncoding}
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.invariants.{InvProperties, InvariantChecker}
12 13
import org.checkerframework.checker.units.qual.s
import scalax.collection.edge.Implicits.+
Christian Müller's avatar
Christian Müller committed
14

15
object Utils extends LazyLogging {
16

Christian Müller's avatar
Christian Müller committed
17
  val RESULTSFOLDER = "results"
Christian Müller's avatar
src  
Christian Müller committed
18
  val DEBUG_MODE = true
19
  val Z3CONTEXTELIM = false
Christian Müller's avatar
Christian Müller committed
20
  val APPROXELIM_MINSIZE = 50
Christian Müller's avatar
Christian Müller committed
21

22
  def mkString[T](string: Iterable[T], start: String, mid: String, end: String): String = {
Christian Müller's avatar
Christian Müller committed
23 24
    if (string.isEmpty) "" else string.mkString(start, mid, end)
  }
25

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

35
  def allchoices(w: Workflow): Set[Fun] = {
36
    w.steps.flatMap(collectChoices).toSet
Christian Müller's avatar
Christian Müller committed
37
  }
38

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

43
  def time[R](block: => R): (Long, R) = {
Christian Müller's avatar
Christian Müller committed
44
    val t0 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
45
    val result = block // call-by-name
Christian Müller's avatar
Christian Müller committed
46
    val t1 = System.nanoTime()
Christian Müller's avatar
Christian Müller committed
47 48 49
    ((t1 - t0) / 1000000, result)
  }

Christian Müller's avatar
Christian Müller committed
50 51 52
  private def recclear(folder: File) {
    for (fol <- folder.listFiles() if fol.isDirectory()) {
      recclear(fol)
Christian Müller's avatar
Christian Müller committed
53
    }
Christian Müller's avatar
Christian Müller committed
54 55 56 57
    folder.listFiles().foreach(_.delete())
  }

  def clear() {
Christian Müller's avatar
Christian Müller committed
58 59 60 61
    val fol = new File(RESULTSFOLDER)
    fol.mkdirs()
    recclear(fol)
  }
Christian Müller's avatar
Christian Müller committed
62 63 64 65 66
  def clear(name:String) {
    val fol = new File(RESULTSFOLDER, name)
    fol.mkdirs()
    recclear(fol)
  }
Christian Müller's avatar
Christian Müller committed
67
  
68 69
  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
70 71 72
    if (file.exists()) {
      file.delete()
    }
Christian Müller's avatar
Christian Müller committed
73 74 75 76
    file.getParentFile.mkdirs()
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
77
    logger.info(s"Written $file")
Christian Müller's avatar
Christian Müller committed
78
  }
Christian Müller's avatar
Christian Müller committed
79

Christian Müller's avatar
Christian Müller committed
80 81 82

  def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
    clear(name)
Christian Müller's avatar
Christian Müller committed
83
    infer(name, desc, spec, properties)
Christian Müller's avatar
Christian Müller committed
84 85 86 87 88 89 90
  }

  def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
    val spec = Examples.parseExampleWF(name).get
    check(name, desc, inv, spec, properties)
  }

Christian Müller's avatar
Christian Müller committed
91
  def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = {
92

Christian Müller's avatar
Christian Müller committed
93 94
    clear(name)

95 96 97 98 99 100 101 102
    val basename = name.split("/").last
    val filenames = s"$basename${if (desc.isEmpty) "" else s"_$desc"}"

    // initial wf graph
    val graph = WFGraphEncoding.toGraph(spec.w)
    val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
    Utils.write(name, s"${filenames}_workflow.dot", elabdot)

Christian Müller's avatar
Christian Müller committed
103

Christian Müller's avatar
Christian Müller committed
104
    val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
Christian Müller's avatar
Christian Müller committed
105 106 107
    val tsgraph = TSGraphEncoding.toGraph(invspec.ts)
    val elabtsdot = TSGraphEncoding.toDot(tsgraph)(Map(), Set())
    Utils.write(name, s"${filenames}_ts.dot", elabtsdot)
108
    infer(name, desc, invspec, properties)
Christian Müller's avatar
Christian Müller committed
109
  }
Christian Müller's avatar
Christian Müller committed
110
  
Christian Müller's avatar
Christian Müller committed
111
  private def infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
Christian Müller's avatar
Christian Müller committed
112
    val model = if (properties.stubborn) "stubborn" else "causal"
113 114

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

Christian Müller's avatar
Christian Müller committed
117 118 119 120
    val fixspec = properties.universe.map(u =>
      InvSpecInstantiator.instantiate(spec, u)
    ).getOrElse(spec)

121
    val (res, graph, labelling, provens, strategies, dot, time) =
Christian Müller's avatar
Christian Müller committed
122
      InvariantChecker.checkInvariantFPLabelling(fixspec, properties)
Christian Müller's avatar
Christian Müller committed
123

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

Christian Müller's avatar
Christian Müller committed
127 128
    if (!res) {
      val headinv = labelling.last(graph.nodes.head)
129
      val satq = And(spec.axioms, Neg(headinv))
Christian Müller's avatar
Christian Müller committed
130 131 132
      logger.info(s"Initial state violating the invariant: ${Z3BSFO.debugmodelBS(satq)}")
    }

Christian Müller's avatar
Christian Müller committed
133
    for ((s, i) <- dot.zipWithIndex) {
134
      Utils.write(name,s"${filenames}_$i.dot", s)
Christian Müller's avatar
Christian Müller committed
135
    }
136
    val strengthenings = for (List(a, b) <- labelling.sliding(2) if a != b) yield {
Christian Müller's avatar
Christian Müller committed
137 138
      true
    }
139

140
    // .invariants
141
    val labels = (for ((node, inv) <- labelling.last) yield {
Christian Müller's avatar
Christian Müller committed
142
      s"Node ${node}:\n${inv.pretty}\n"
143
    }).mkString("\n")
144
    Utils.write(name, s"$filenames.invariants", labels)
Christian Müller's avatar
Christian Müller committed
145

146 147 148 149 150 151 152
    // .strategies
    val strats = strategies.last.values.foldLeft("")(_ + _)
    val stratfile = s"Strategies:\n${Utils.indentLines(strats)}"
    Utils.write(name, s"$filenames.strategies", stratfile)

    // .metrics

Christian Müller's avatar
Christian Müller committed
153
    val wfsize = graph.edges.size - 1
Christian Müller's avatar
Christian Müller committed
154
    val invsizes = labelling.last.map(_._2.opsize)
Christian Müller's avatar
Christian Müller committed
155 156
    val maxsize = invsizes.max
    val avgsize = invsizes.sum / invsizes.size
157
    Utils.write(name, s"$filenames.metrics",
158 159 160 161 162 163 164 165 166 167 168 169 170 171
    s"""Name: $name
       |Description: $desc
       |  Invariant:
       |${spec.inv.pretty.linesIterator.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
       |  Properties: $properties
       |  """.stripMargin
Christian Müller's avatar
Christian Müller committed
172
    )
Christian Müller's avatar
Christian Müller committed
173 174
    res
  }
175 176 177 178 179

  // Will be obsolete in Scala 2.13
  def using[A, B <: {def close(): Unit}] (closeable: B) (f: B => A): A =
    try { f(closeable) } finally { closeable.close() }

Christian Müller's avatar
Christian Müller committed
180
}