build niwo-ltl.jar

assembly/README.md

 # Invariants Tool
 
-This is an implementation accompanying the anonymous submission 47.
-It can be used to verify and infer universal invariants for workflows.
+This is NIWO, an implementation for automatic verification of multi-agent workflows.
+It can be used to verify and infer universal invariants for workflows as well as directly solve non-omitting workflows.
 
 ## Prerequisites
 

build.sbt

-name := "LoopingWorkflows"
+name := "loopingWorkflows"
 
 version := "0.1"
 

src/main/scala/META-INF/MANIFEST.MF

+Manifest-Version: 1.0
+Main-Class: de.tum.workflows.LTLCLI
+

src/main/scala/de/tum/workflows/LTLCli.scala → src/main/scala/de/tum/workflows/LTLCLI.scala

@@ -2,17 +2,10 @@ package de.tum.workflows
 
 import scala.io.Source
 import com.typesafe.scalalogging.LazyLogging
-import de.tum.workflows.blocks.Spec
 import java.io.File
 
-import de.tum.workflows.foltl.Properties
-import de.tum.workflows.ltl.FOTransformers
-import de.tum.workflows.owl.OwlTransformer
-
 object LTLCLI extends App with LazyLogging {
 
-  val MAXAGENTS = 8
-
   lazy val usage = """
     Usage niwo-ltl.jar [--stubborn] FILE
 
@@ -46,43 +39,6 @@ object LTLCLI extends App with LazyLogging {
       }
     }
 
-    spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, stubborn))
-  }
-
-  def generate(name: String, spec: Spec, onlystubborn: Boolean) {
-    logger.info(s"Encoding Spec:\n$spec")
-
-    if (spec.w.isomitting) {
-      logger.info("Omitting spec - no embedding in LTL possible")
-    } else {
-      logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
-      val foltlprop = if (onlystubborn || spec.causals.isEmpty) {
-        logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
-        Properties.noninterStubborn(spec)
-      } else {
-        logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
-        Properties.noninterCausal(spec)
-      }
-      logger.info(s"Built FOLTL prop with size ${foltlprop.opsize()}")
-
-      val (agents, res) = FOTransformers.eliminateExistentials(foltlprop)
-      val universe = agents.map(_.withType()).mkString(", ")
-      logger.info(s"Using universe $universe")
-
-      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 = FOTransformers.eliminateUniversals(res, agents)
-      val ltlprop = FOTransformers.eliminatePredicates(quantfree)
-
-      logger.info(s"Built LTL property with size ${ltlprop.opsize()}")
-
-      val owlprop = OwlTransformer.toOwl(ltlprop)
-
-    }
-
+    spec.map(MainLTL.generate(new File(file).getName.stripSuffix(".spec"), _, stubborn))
   }
-
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/MainLTL.scala

 package de.tum.workflows
 
 import foltl.FOLTL._
-import blocks.Workflow._
-import Implicits._
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.workflows.ltl.FOTransformers
 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.FormulaFunctions
-import de.tum.workflows.toz3.InvariantChecker
+import de.tum.workflows.owltransformer.OwlTransformer
+import owl.ltl.algorithms.LanguageAnalysis
+import owl.ltl.rewriter.SimplifierFactory
 
-object MainLTL extends App with LazyLogging {
 
-  val MAXAGENTS = 8
+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())
@@ -31,47 +28,63 @@ object MainLTL extends App with LazyLogging {
       return
     }
 
-    // Do FOLTL to LTL
-    if (spec.w.isomitting) {
-      logger.info("Omitting spec - no embedding in LTL possible")
-    } else {
-      logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
-      val (agents, res) = FOTransformers.eliminateExistentials(prop)
+    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")
+    val universe = agents.map(_.withType()).mkString(", ")
+    logger.info(s"Using universe $universe")
 
-      if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
-        logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
-        return
-      }
+    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"
 
-      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())
 
-      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())
+      write(s"${name}.owlltl", simped.toString)
+      logger.info("Simplified owl formula")
+      // check owl sat
+      logger.info("Checking satisfiability")
+      LanguageAnalysis.isSatisfiable(simped)
     }
 
-    write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
+    logger.info(s"Found LTL formula to be satisfiable: $sat in $t ms")
 
-    logger.info(s"Written all files for $name")
+    metrics :+= s"Satisfiable: $sat"
+    metrics :+= s"Owl runtime: $t ms"
+
+    write(s"${name}.metrics", metrics.mkString("", "\n", "\n"))
   }
 
-  def generate(name: String, spec: Spec) {
+  def generate(name: String, spec: Spec, onlystubborn:Boolean) {
     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", spec, 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"${name}_causal", spec, cprop)
+    // 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)
+      }
     }
   }
 
@@ -83,7 +96,7 @@ object MainLTL extends App with LazyLogging {
       logger.error(s"Not a valid spec: $name")
     }
 
-    spec.map(generate(name, _))
+    spec.foreach(generate(name, _, false))
   }
 
   def generateAllExamples() {
@@ -95,7 +108,9 @@ object MainLTL extends App with LazyLogging {
   }
 
   //  clear()
-    generateExample("nonomitting/conference")
-  //    generateExample("tests/declasstest")
+//    generateExample("nonomitting/conference")
+//      generateExample("tests/declasstest")
+  generateExample("tests/simpleChoice")
+//  generateExample("tests/simpleChoiceNoOracle")
 //  generateAllExamples()
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/owl/OwlTransformer.scala → src/main/scala/de/tum/workflows/owltransformer/OwlTransformer.scala

-package de.tum.workflows.owl
+package de.tum.workflows.owltransformer
 
 import scala.collection.JavaConversions._
 import com.typesafe.scalalogging.LazyLogging

src/test/scala/de/tum/workflows/ltl/tests/OwlTest.scala

@@ -5,7 +5,7 @@ import java.util.EnumSet
 
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.workflows.foltl.FOLTL._
-import de.tum.workflows.owl.OwlTransformer
+import de.tum.workflows.owltransformer.OwlTransformer
 import org.scalatest.FlatSpec
 import org.scalatest.Matchers._
 import org.scalatest.Inspectors._