tests

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

@@ -160,7 +160,7 @@ object FormulaFunctions extends LazyLogging {
         val eqs = for (x <- vars; y <- otherthan) yield {
           Neg(Eq(x,y))
         }
-        Forall(vars, And(And.make(eqs), fp))
+        Forall(vars, Implies(And.make(eqs), fp))
       }
     })
   }

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 = f.removeOTQuantifiers()
+    res2 should be(
+      Forall(List("x","y"), Implies(And(Neg(Eq("x", "y")), Neg(Eq("y", "z"))), Globally("x")))
+    )
+  }
+}
\ No newline at end of file