MainLTLWorkflows.scala 3.65 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

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

14
object MainLTLWorkflows extends App with LazyLogging {
Christian Müller's avatar
Christian Müller committed
15

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

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

20
    var metrics = List[String]()
21

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

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

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

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

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

46 47 48 49
    // So aalta doesnt throw up
    val ltlstring = ltlprop.toString.replace("#","_")

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

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

    val owlform = OwlTransformer.toOwl(ltlprop)

Christian Müller's avatar
Christian Müller committed
55
    // simplify owl
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
//    val (t1,simped) = time {
//      SimplifierFactory.apply(owlform.formula(), SimplifierFactory.Mode.SYNTACTIC_FIXPOINT)
//    }
//    write(name, s"$name.owlltl",simped.toString)
//    logger.info(s"Simplified owl formula in $t1 ms")
//    val (t2, sat) = time {
//      // check owl sat
//      logger.info("Checking satisfiability")
////      LanguageAnalysis.isSatisfiable(simped)
//
//      OwlTransformer.isSatisfiable(simped)
//    }
//    logger.info(s"Found LTL formula to be satisfiable: $sat in $t2 ms")
//
//    metrics :+= s"Satisfiable: $sat"
//    metrics :+= s"Owl simplification $t1 ms"
//    metrics :+= s"Owl runtime: $t2 ms"
Christian Müller's avatar
Christian Müller committed
73

74
    write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
Christian Müller's avatar
Christian Müller committed
75
  }
76

Christian Müller's avatar
Christian Müller committed
77
  def generate(name: String, spec: NISpec, onlystubborn:Boolean) {
78
    logger.info(s"Encoding Spec:\n$spec")
Christian Müller's avatar
Christian Müller committed
79 80 81 82 83 84 85 86 87 88 89 90 91
    // 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
92
    }
93
  }
Christian Müller's avatar
Christian Müller committed
94

Christian Müller's avatar
Christian Müller committed
95
  def generateExample(name: String) {
Christian Müller's avatar
Christian Müller committed
96
    logger.info(s"Generating $name")
97
    val spec = Examples.parseExampleWF(name)
Christian Müller's avatar
Christian Müller committed
98

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

Christian Müller's avatar
Christian Müller committed
103
    spec.foreach(generate(name, _, false))
Christian Müller's avatar
Christian Müller committed
104
  }
Christian Müller's avatar
Christian Müller committed
105

Christian Müller's avatar
Christian Müller committed
106 107 108
  def generateAllExamples() {
    clear()
    // Fill results alphabetically
109
    for (k <- Examples.wfexamples.keys.toList.sorted) {
Christian Müller's avatar
Christian Müller committed
110
      generateExample(k)
Christian Müller's avatar
Christian Müller committed
111
    }
112
  }
Christian Müller's avatar
Christian Müller committed
113 114

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