Main.scala

package de.tum.workflows

import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.TermFunctions

object Main extends App with LazyLogging {
  
  val MAXAGENTS = 5
  val FOLDER = "results"
  
  def generateExample(name: String) {
      logger.info(s"Generating $name")
      val spec = ExampleWorkflows.examples(name)
      
      generate(name, spec)
  }
  
  def write(name: String, prop:String) {
    val file = new File(name)
    val writer = new PrintWriter(file)
    writer.print(prop)
    writer.close()
  }
  
  def writeExample(name: String, prop: Term) {

    write(s"${name}.foltl", prop.pretty())

    if (!TermFunctions.checkSanity(prop)) {
      logger.error("Property didn't pass sanity check")
      return
    }
    
    val (agents, res) = LTL.eliminateExistentials(prop)
    
    logger.info(s"Using universe ${agents.map(_.withType())}")
    
    if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
      logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
      return
    }
    
    val quantfree = LTL.eliminateUniversals(res, agents)
    val ltlprop = LTL.eliminatePredicates(quantfree)

    write(s"${name}_size${agents.size}.ltl", ltlprop.toString())
    write(s"${name}_size${agents.size}.ppltl", ltlprop.pretty())
    
    logger.info(s"Written all files for $name")
  }

  def generate(name: String, spec:Spec) {
    logger.info(s"Encoding Spec:\n$spec")
    val t1 = "pi1"
    val t2 = "pi2"

    logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
    val prop = Properties.noninterStubborn(spec)
    writeExample(s"results/${name}_stubborn", prop)
    
    if (!spec.causals.isEmpty) {
      logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
      val cprop = Properties.noninterCausal(spec)
      writeExample(s"$FOLDER/${name}_causal", cprop)
    }
  }

  // Clear results folder
  val folder = new File(FOLDER)
  folder.mkdirs()
  folder.listFiles().foreach(_.delete())
  
  // Fill results
  for ((k, value) <- ExampleWorkflows.examples) {
     generateExample(k)
  }
}