Main.scala 4.39 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
package de.tum.workflows

import foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
4
import blocks.Workflow._
Christian Müller's avatar
Christian Müller committed
5
import Implicits._
Christian Müller's avatar
Christian Müller committed
6
7
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
Christian Müller's avatar
Christian Müller committed
8
9
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
10
11
12
13
import de.tum.workflows.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
Christian Müller's avatar
Christian Müller committed
14
import de.tum.workflows.blocks.Spec
15
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
16
import de.tum.workflows.toz3.InvariantChecker
Christian Müller's avatar
Christian Müller committed
17

Christian Müller's avatar
Christian Müller committed
18
object Main extends App with LazyLogging {
Christian Müller's avatar
Christian Müller committed
19

20
  val MAXAGENTS = 8
Christian Müller's avatar
Christian Müller committed
21
  val FOLDER = "results"
Christian Müller's avatar
Christian Müller committed
22
23

  val checkinvariants = true
Christian Müller's avatar
Christian Müller committed
24

Christian Müller's avatar
Christian Müller committed
25
  def clear() {
Christian Müller's avatar
Christian Müller committed
26
    def recclear(folder: File) {
Christian Müller's avatar
Christian Müller committed
27
28
29
      for (fol <- folder.listFiles() if fol.isDirectory()) {
        recclear(fol)
      }
Christian Müller's avatar
Christian Müller committed
30

Christian Müller's avatar
Christian Müller committed
31
32
33
34
35
      folder.listFiles().foreach(_.delete())
    }
    val fol = new File(FOLDER)
    fol.mkdirs()
    recclear(fol)
36
  }
Christian Müller's avatar
Christian Müller committed
37
38

  def write(name: String, prop: String) {
Christian Müller's avatar
Christian Müller committed
39
    val file = new File(name)
Christian Müller's avatar
Christian Müller committed
40
    file.getParentFile.mkdirs()
Christian Müller's avatar
Christian Müller committed
41
42
43
44
45
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
  }
  
Christian Müller's avatar
Christian Müller committed
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
  def timeNoninter(spec:Spec) = {
      val inv = InvariantChecker.invariantNoninterStubborn(spec)
      val (t, (safe, msg)) = time {
        InvariantChecker.checkInvariant(spec.w, inv, true)
      }
      s"Noninterference Invariant (took $t ms):\n$msg\n"
  }
  
  def timeAllEqual(spec:Spec) = {
      val inv = InvariantChecker.invariantAllEqual(spec)
      val (t, (safe, msg)) = time {
        InvariantChecker.checkInvariant(spec.w, inv, true)
      }
      s"All Equal Invariant (took $t ms):\n$msg\n"
  }

  def writeExample(name: String, spec: Spec, prop: Formula) {

64
    var metrics = List[String]()
65

Christian Müller's avatar
Christian Müller committed
66
    write(s"${name}.foltl", prop.pretty())
67
    metrics :+= s"${name}.foltl: ${prop.opsize()}"
Christian Müller's avatar
Christian Müller committed
68

69
    if (!FormulaFunctions.checkSanity(prop)) {
Christian Müller's avatar
Christian Müller committed
70
71
72
      logger.error("Property didn't pass sanity check")
      return
    }
Christian Müller's avatar
Christian Müller committed
73

Christian Müller's avatar
Christian Müller committed
74
75
76
77
78
79
    // Do FOLTL to LTL
    if (spec.w.isomitting) {
      logger.info("Omitting spec - no embedding in LTL possible")
    } else {
      logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
      val (agents, res) = LTL.eliminateExistentials(prop)
Christian Müller's avatar
Christian Müller committed
80

Christian Müller's avatar
Christian Müller committed
81
82
      val universe = agents.map(_.withType()).mkString(", ")
      logger.info(s"Using universe $universe")
Christian Müller's avatar
Christian Müller committed
83

Christian Müller's avatar
Christian Müller committed
84
85
86
87
      if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
        logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
        return
      }
Christian Müller's avatar
Christian Müller committed
88

Christian Müller's avatar
Christian Müller committed
89
90
91
      val quantfree = LTL.eliminateUniversals(res, agents)
      val ltlprop = LTL.eliminatePredicates(quantfree)
      metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
Christian Müller's avatar
Christian Müller committed
92
93
      metrics :+= s"Universe: $universe"

Christian Müller's avatar
Christian Müller committed
94
95
      write(s"${name}.ltl", ltlprop.toString())
      write(s"${name}.ppltl", ltlprop.pretty())
96
    }
Christian Müller's avatar
Christian Müller committed
97

98
    write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
Christian Müller's avatar
Christian Müller committed
99

Christian Müller's avatar
Christian Müller committed
100
101
    logger.info(s"Written all files for $name")
  }
102

Christian Müller's avatar
Christian Müller committed
103
  def generate(name: String, spec: Spec) {
104
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
105
106
107
108
109
    val t1 = "pi1"
    val t2 = "pi2"

    logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
    val prop = Properties.noninterStubborn(spec)
Christian Müller's avatar
Christian Müller committed
110
    writeExample(s"results/${name}_stubborn", spec, prop)
Christian Müller's avatar
Christian Müller committed
111
112
113
    if (!spec.causals.isEmpty) {
      logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
      val cprop = Properties.noninterCausal(spec)
Christian Müller's avatar
Christian Müller committed
114
      writeExample(s"$FOLDER/${name}_causal", spec, cprop)
Christian Müller's avatar
Christian Müller committed
115
    }
Christian Müller's avatar
Christian Müller committed
116

Christian Müller's avatar
Christian Müller committed
117
118
    if (checkinvariants) {
      
Christian Müller's avatar
Christian Müller committed
119
      def invariants = List(
Christian Müller's avatar
Christian Müller committed
120
121
          InvariantChecker.invariantNoninterStubborn _,
          InvariantChecker.invariantAllEqual _
Christian Müller's avatar
Christian Müller committed
122
123
      )

Christian Müller's avatar
Christian Müller committed
124
125
126
127
128
129
      def msgs = for (inv <- invariants) yield {
        val (t, (safe, msg)) = time {
          InvariantChecker.checkInvariant(spec.w, inv(spec), true)
        }
        s"Proving Invariant (took $t ms):\n$msg\n"
      }
Christian Müller's avatar
Christian Müller committed
130
131

      write(s"$FOLDER/${name}.inv", msgs.mkString("\n"))
Christian Müller's avatar
Christian Müller committed
132
    }
133
  }
Christian Müller's avatar
Christian Müller committed
134

Christian Müller's avatar
Christian Müller committed
135
  def generateExample(name: String) {
Christian Müller's avatar
Christian Müller committed
136
137
138
139
140
141
142
143
    logger.info(s"Generating $name")
    val spec = ExampleWorkflows.parseExample(name)

    if (!spec.isDefined) {
      logger.error(s"Not a valid spec: $name")
    }

    spec.map(generate(name, _))
Christian Müller's avatar
Christian Müller committed
144
  }
Christian Müller's avatar
Christian Müller committed
145

Christian Müller's avatar
Christian Müller committed
146
147
148
149
  def generateAllExamples() {
    clear()
    // Fill results alphabetically
    for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
Christian Müller's avatar
Christian Müller committed
150
      generateExample(k)
Christian Müller's avatar
Christian Müller committed
151
    }
152
  }
Christian Müller's avatar
Christian Müller committed
153
154

  //  clear()
Christian Müller's avatar
Christian Müller committed
155
    generateExample("omitting/conference")
Christian Müller's avatar
Christian Müller committed
156
  //    generateExample("tests/declasstest")
Christian Müller's avatar
Christian Müller committed
157
//  generateAllExamples()
Christian Müller's avatar
Christian Müller committed
158
}