MainLTLTransitionSystems.scala 3.21 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
package de.tum.niwo

import foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.Utils._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.blocks.{InvariantSpec, NISpec}
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.owltransformer.OwlTransformer


object MainLTLTransitionSystems extends App with LazyLogging {

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

    val MAX_AGENTS = 8

    var metrics = List[String]()

    write(name, s"$name.foltl", prop.pretty)
    metrics :+= s"$name.foltl: ${prop.opsize}"

    if (!FormulaFunctions.checkSanity(prop)) {
      logger.error("Property didn't pass sanity check")
      return
    }

    logger.info("Embedding FOLTL formula in LTL")
    val (agents, res) = FOTransformers.eliminateExistentials(prop)

    val universe = agents.map(_.withType).mkString(", ")
    logger.info(s"Using universe $universe")

    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)
    metrics :+= s"$name.ltl: ${ltlprop.opsize}"
    metrics :+= s"Universe: $universe"

    write(name, s"$name.ltl", ltlprop.toString())
    write(name, s"$name.ppltl", ltlprop.pretty)


//    val owlform = OwlTransformer.toOwl(ltlprop)
//
//    // simplify owl
//    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"

    write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
  }

  def generate(name: String, spec: InvariantSpec) {
    logger.info(s"Encoding Spec:\n$spec")

    // TODO: Check if correct fragment
    logger.info (s"Computing invariant for target ${spec.inv} using only stubborn agents")
    val prop = Properties.singletrace (spec)
    writeExample (s"${name}_invspec", spec, prop)
  }

  def generateExample(name: String) {
    logger.info(s"Generating $name")
    val spec = Examples.parseExampleTS(name)

    if (spec.isEmpty) {
      logger.error(s"Not a valid spec: $name")
    }

    spec.foreach(generate(name, _))
  }

  def generateAllExamples() {
    clear()
    // Fill results alphabetically
    for (k <- Examples.tsexamples.keys.toList.sorted) {
      generateExample(k)
    }
  }

  //  clear()
  //    generateExample("nonomitting/conference")
  //      generateExample("tests/declasstest")
  generateExample("tstests/easychair_singletrace")
  //  generateExample("tests/simpleChoiceNoOracle")
  //  generateAllExamples()
}