Main.scala 3.79 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 {
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
24
  
Christian Müller's avatar
Christian Müller committed
25
26
27
28
29
  def clear() {
    def recclear(folder:File) {
      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()
  }
  
46
  def writeExample(name: String, spec:Spec, prop: Formula) {
47
48
    
    var metrics = List[String]()
49

Christian Müller's avatar
Christian Müller committed
50
    write(s"${name}.foltl", prop.pretty())
51
    metrics :+= s"${name}.foltl: ${prop.opsize()}"
Christian Müller's avatar
Christian Müller committed
52
    
53
    if (!FormulaFunctions.checkSanity(prop)) {
Christian Müller's avatar
Christian Müller committed
54
55
56
      logger.error("Property didn't pass sanity check")
      return
    }
Christian Müller's avatar
Christian Müller committed
57
    
Christian Müller's avatar
Christian Müller committed
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
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)
      
      val universe = agents.map(_.withType()).mkString(", ")
      logger.info(s"Using universe $universe")
      
      if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
        logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
        return
      }
      
      val quantfree = LTL.eliminateUniversals(res, agents)
      val ltlprop = LTL.eliminatePredicates(quantfree)
      metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
      metrics :+= s"Universe: $universe" 
  
      write(s"${name}.ltl", ltlprop.toString())
      write(s"${name}.ppltl", ltlprop.pretty())
80
81
    }
    
82
83
    write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
    
Christian Müller's avatar
Christian Müller committed
84
85
    logger.info(s"Written all files for $name")
  }
86

Christian Müller's avatar
Christian Müller committed
87
  def generate(name: String, spec:Spec) {
88
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
89
90
91
92
93
    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
94
    writeExample(s"results/${name}_stubborn", spec, prop)
Christian Müller's avatar
Christian Müller committed
95
96
97
    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
98
      writeExample(s"$FOLDER/${name}_causal", spec, cprop)
Christian Müller's avatar
Christian Müller committed
99
    }
Christian Müller's avatar
Christian Müller committed
100
101
102
103
    
    if (checkinvariants) {
      
    	val inv = InvariantChecker.invariantNoninterStubborn(spec)
Christian Müller's avatar
Christian Müller committed
104
       val (t,(safe, msg)) = time {
Christian Müller's avatar
Christian Müller committed
105
106
         InvariantChecker.checkStubborn(spec.w, inv)
       }
Christian Müller's avatar
Christian Müller committed
107
       val noninter = s"Noninterference Invariant (took $t ms):\n$msg"
Christian Müller's avatar
Christian Müller committed
108
       
Christian Müller's avatar
Christian Müller committed
109
       write(s"$FOLDER/${name}.inv", noninter)
Christian Müller's avatar
Christian Müller committed
110
    }
111
  }
Christian Müller's avatar
Christian Müller committed
112
  
Christian Müller's avatar
Christian Müller committed
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
  def generateExample(name: String) {
      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, _))
  }
  
  def generateAllExamples() {
    clear()
    // Fill results alphabetically
    for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
       generateExample(k)
    }
130
  }
Christian Müller's avatar
Christian Müller committed
131
  
Christian Müller's avatar
Christian Müller committed
132
133
134
//  clear()
//  generateExample("omitting/conference")
  generateAllExamples()
Christian Müller's avatar
Christian Müller committed
135
}