MainLTL.scala 3.52 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

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

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

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

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

21
    var metrics = List[String]()
22

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

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

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

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

Christian Müller's avatar
Christian Müller committed
37
38
39
40
41
42
43
    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
44
    metrics :+= s"$name.ltl: ${ltlprop.opsize()}"
Christian Müller's avatar
Christian Müller committed
45
    metrics :+= s"Universe: $universe"
Christian Müller's avatar
Christian Müller committed
46

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

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

    val owlform = OwlTransformer.toOwl(ltlprop)

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

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

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

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

Christian Müller's avatar
Christian Müller committed
71
  def generate(name: String, spec: Spec, onlystubborn:Boolean) {
72
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
73
74
    val t1 = "pi1"
    val t2 = "pi2"
Christian Müller's avatar
Christian Müller committed
75
76
77
78
79
80
81
82
83
84
85
86
87
    // 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
88
    }
89
  }
Christian Müller's avatar
Christian Müller committed
90

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

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

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

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

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