MainLTL.scala

package de.tum.workflows

import foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory
import de.tum.workflows.ltl.FOTransformers


object MainLTL extends App with LazyLogging {

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

    val MAX_AGENTS = 8

    var metrics = List[String]()

    write(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(s"$name.ltl", ltlprop.toString())
    write(s"$name.ppltl", ltlprop.pretty())


    val owlform = OwlTransformer.toOwl(ltlprop)

    val (t, sat) = time {
      // simplify owl
      val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
      write(s"$name.owlltl", simped.toString)
      logger.info("Simplified owl formula")
      // check owl sat
      logger.info("Checking satisfiability")
      LanguageAnalysis.isSatisfiable(simped)
    }

    logger.info(s"Found LTL formula to be satisfiable: $sat in $t ms")

    metrics :+= s"Satisfiable: $sat"
    metrics :+= s"Owl runtime: $t ms"

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

  def generate(name: String, spec: Spec, onlystubborn:Boolean) {
    logger.info(s"Encoding Spec:\n$spec")
    val t1 = "pi1"
    val t2 = "pi2"
    // 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)
      }
    }
  }

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

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

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

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

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