MainLTL.scala 3.53 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 com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
6
import de.tum.workflows.Utils._
7
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
8
import de.tum.workflows.blocks.Spec
9
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
10
11
12
import de.tum.workflows.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory
Christian Müller's avatar
Christian Müller committed
13
import de.tum.workflows.ltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
14

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

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

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

Christian Müller's avatar
Christian Müller committed
20
21
    val MAX_AGENTS = 8

22
    var metrics = List[String]()
23

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

27
    if (!FormulaFunctions.checkSanity(prop)) {
Christian Müller's avatar
Christian Müller committed
28
29
30
      logger.error("Property didn't pass sanity check")
      return
    }
Christian Müller's avatar
Christian Müller committed
31

Christian Müller's avatar
Christian Müller committed
32
33
    logger.info("Embedding FOLTL formula in LTL")
    val (agents, res) = FOTransformers.eliminateExistentials(prop)
Christian Müller's avatar
Christian Müller committed
34

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

Christian Müller's avatar
Christian Müller committed
38
39
40
41
42
43
44
    if (agents.groupBy(_.typ).exists(_._2.size > MAX_AGENTS)) {
      logger.error(s"Universe has more than $MAX_AGENTS agents for a single type. Aborting.")
      return
    }

    val quantfree = FOTransformers.eliminateUniversals(res, agents)
    val ltlprop = FOTransformers.eliminatePredicates(quantfree)
Christian Müller's avatar
Christian Müller committed
45
    metrics :+= s"$name.ltl: ${ltlprop.opsize()}"
Christian Müller's avatar
Christian Müller committed
46
    metrics :+= s"Universe: $universe"
Christian Müller's avatar
Christian Müller committed
47

Christian Müller's avatar
Christian Müller committed
48
49
    write(s"$name.ltl", ltlprop.toString())
    write(s"$name.ppltl", ltlprop.pretty())
Christian Müller's avatar
Christian Müller committed
50

Christian Müller's avatar
Christian Müller committed
51
52
53
54
55

    val owlform = OwlTransformer.toOwl(ltlprop)

    val (t, sat) = time {
      // simplify owl
Christian Müller's avatar
Christian Müller committed
56
57
      val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
      write(s"$name.owlltl", simped.toString)
Christian Müller's avatar
Christian Müller committed
58
59
60
61
      logger.info("Simplified owl formula")
      // check owl sat
      logger.info("Checking satisfiability")
      LanguageAnalysis.isSatisfiable(simped)
62
    }
Christian Müller's avatar
Christian Müller committed
63

Christian Müller's avatar
Christian Müller committed
64
    logger.info(s"Found LTL formula to be satisfiable: $sat in $t ms")
Christian Müller's avatar
Christian Müller committed
65

Christian Müller's avatar
Christian Müller committed
66
67
68
    metrics :+= s"Satisfiable: $sat"
    metrics :+= s"Owl runtime: $t ms"

Christian Müller's avatar
Christian Müller committed
69
    write(s"$name.metrics", metrics.mkString("", "\n", "\n"))
Christian Müller's avatar
Christian Müller committed
70
  }
71

Christian Müller's avatar
Christian Müller committed
72
  def generate(name: String, spec: Spec, onlystubborn:Boolean) {
73
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
74
75
    val t1 = "pi1"
    val t2 = "pi2"
Christian Müller's avatar
Christian Müller committed
76
77
78
79
80
81
82
83
84
85
86
87
88
    // Do FOLTL to LTL
    if (spec.w.isomitting) {
      logger.info("Omitting spec - no embedding in LTL possible")
    } else {
      if (onlystubborn || spec.causals.isEmpty) {
        logger.info (s"Computing noninterference for target ${spec.target} using only stubborn agents")
        val prop = Properties.noninterStubborn (spec)
        writeExample (s"${name}_stubborn", spec, prop)
      } else {
        logger.info (s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
        val cprop = Properties.noninterCausal (spec)
        writeExample (s"${name}_causal", spec, cprop)
      }
Christian Müller's avatar
Christian Müller committed
89
    }
90
  }
Christian Müller's avatar
Christian Müller committed
91

Christian Müller's avatar
Christian Müller committed
92
  def generateExample(name: String) {
Christian Müller's avatar
Christian Müller committed
93
94
95
    logger.info(s"Generating $name")
    val spec = ExampleWorkflows.parseExample(name)

Christian Müller's avatar
Christian Müller committed
96
    if (spec.isEmpty) {
Christian Müller's avatar
Christian Müller committed
97
98
99
      logger.error(s"Not a valid spec: $name")
    }

Christian Müller's avatar
Christian Müller committed
100
    spec.foreach(generate(name, _, false))
Christian Müller's avatar
Christian Müller committed
101
  }
Christian Müller's avatar
Christian Müller committed
102

Christian Müller's avatar
Christian Müller committed
103
104
105
106
  def generateAllExamples() {
    clear()
    // Fill results alphabetically
    for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
Christian Müller's avatar
Christian Müller committed
107
      generateExample(k)
Christian Müller's avatar
Christian Müller committed
108
    }
109
  }
Christian Müller's avatar
Christian Müller committed
110
111

  //  clear()
Christian Müller's avatar
Christian Müller committed
112
113
//    generateExample("nonomitting/conference")
//      generateExample("tests/declasstest")
Christian Müller's avatar
Christian Müller committed
114
115
//  generateExample("tests/simpleChoice")
  generateExample("tests/simpleChoiceNoOracle")
Christian Müller's avatar
Christian Müller committed
116
//  generateAllExamples()
Christian Müller's avatar
Christian Müller committed
117
}