Main.scala 2.44 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
Christian Müller's avatar
Christian Müller committed
15
import de.tum.workflows.foltl.TermFunctions
Christian Müller's avatar
Christian Müller committed
16

Christian Müller's avatar
Christian Müller committed
17
object Main extends App with LazyLogging {
18
  
19
  val MAXAGENTS = 5
Christian Müller's avatar
Christian Müller committed
20
  val FOLDER = "results"
21
  
22
23
  def generateExample(name: String) {
      logger.info(s"Generating $name")
Christian Müller's avatar
Christian Müller committed
24
25
26
      val spec = ExampleWorkflows.examples(name)
      
      generate(name, spec)
27
  }
Christian Müller's avatar
Christian Müller committed
28
  
29
  def write(name: String, prop:String) {
Christian Müller's avatar
Christian Müller committed
30
31
32
33
34
35
36
    val file = new File(name)
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
  }
  
  def writeExample(name: String, prop: Term) {
37

Christian Müller's avatar
Christian Müller committed
38
    write(s"${name}.foltl", prop.pretty())
Christian Müller's avatar
Christian Müller committed
39
40
41
42
43

    if (!TermFunctions.checkSanity(prop)) {
      logger.error("Property didn't pass sanity check")
      return
    }
Christian Müller's avatar
Christian Müller committed
44
    
45
    val (agents, res) = LTL.eliminateExistentials(prop)
46
    
Christian Müller's avatar
Christian Müller committed
47
48
49
50
    logger.info(s"Using universe ${agents.map(_.withType())}")
    
    if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
      logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
51
52
53
      return
    }
    
54
55
56
    val quantfree = LTL.eliminateUniversals(res, agents)
    val ltlprop = LTL.eliminatePredicates(quantfree)

Christian Müller's avatar
Christian Müller committed
57
58
    write(s"${name}_size${agents.size}.ltl", ltlprop.toString())
    write(s"${name}_size${agents.size}.ppltl", ltlprop.pretty())
59
    
Christian Müller's avatar
Christian Müller committed
60
61
    logger.info(s"Written all files for $name")
  }
62

Christian Müller's avatar
Christian Müller committed
63
  def generate(name: String, spec:Spec) {
64
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
65
66
67
68
69
70
71
    val t1 = "pi1"
    val t2 = "pi2"

    logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
    val prop = Properties.noninterStubborn(spec)
    writeExample(s"results/${name}_stubborn", prop)
    
Christian Müller's avatar
Christian Müller committed
72
73
74
75
76
    if (!spec.causals.isEmpty) {
      logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
      val cprop = Properties.noninterCausal(spec)
      writeExample(s"$FOLDER/${name}_causal", cprop)
    }
77
78
  }

Christian Müller's avatar
Christian Müller committed
79
80
81
82
83
84
  // Clear results folder
  val folder = new File(FOLDER)
  folder.mkdirs()
  folder.listFiles().foreach(_.delete())
  
  // Fill results
85
86
  for ((k, value) <- ExampleWorkflows.examples) {
     generateExample(k)
87
  }
Christian Müller's avatar
Christian Müller committed
88
}