Merge branch 'master' of https://versioncontrolseidl.in.tum.de/mueller/loopingworkflows

src/main/scala/de/tum/workflows/foltl/FOLTL.scala

@@ -15,6 +15,8 @@ object FOLTL {
     def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore)
     def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
     def opsize() = FormulaFunctions.opsize(this)
+    
+    def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
 
     def bracketed(): String = this match {
       case _: BinOp => "(" + this + ")"

src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala

@@ -153,4 +153,15 @@ object FormulaFunctions extends LazyLogging {
 
     frees.isEmpty
   }
+  
+  def removeOTQuantifiers(f: Formula) = {
+    f.everywhere({
+      case ForallOtherThan(vars, otherthan, fp) => {
+        val eqs = for (x <- vars; y <- otherthan) yield {
+          Neg(Eq(x,y))
+        }
+        Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
+      }
+    })
+  }
 }
\ No newline at end of file

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

+package de.tum.workflows.ltl.tests
+
+import org.scalatest.FlatSpec
+import org.scalatest.Matchers._
+import org.scalatest.Inspectors._
+
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.Implicits._
+
+class FOLTLTest extends FlatSpec {
+
+  "Formula functions" should "generate inequalities" in {
+
+    val f = ForallOtherThan("x", List("y", "z"), Globally("x"))
+    val res = f.removeOTQuantifiers()
+    res should be(
+      Forall("x", Implies(And(Neg(Eq("x", "y")), Neg(Eq("x", "z"))), Globally("x")))
+    )
+    
+    val f2 = ForallOtherThan(List("x","y"), "z", Globally("x"))
+    val res2 = f2.removeOTQuantifiers()
+    res2 should be(
+      Forall(List("x","y"), Implies(And(Neg(Eq("x", "z")), Neg(Eq("y", "z"))), Globally("x")))
+    )
+  }
+}
\ No newline at end of file