MainLTL.scala 3.52 KB
Newer Older
1
package de.tum.niwo
Christian Müller's avatar
Christian Müller committed
2 3

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

Christian Müller's avatar
Christian Müller committed
18
  def writeExample(name: String, spec: NISpec, prop: Formula) {
Christian Müller's avatar
Christian Müller committed
19

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(name, 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
    val universe = agents.map(_.withType).mkString(", ")
Christian Müller's avatar
Christian Müller committed
36
    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

48
    write(name, s"$name.ltl", ltlprop.toString())
Christian Müller's avatar
Christian Müller committed
49
    write(name, 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
      val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
57
      write(name, 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"

69
    write(name, 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: NISpec, 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
}