fixed bug in NNF

nmacedo · Oct 16, 2024 · f861715 · f861715
1 parent 938b87d
commit f861715
Showing 1 changed file with 9 additions and 2 deletions.
diff --git a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/ltl2fol/NNFReplacer.java b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/ltl2fol/NNFReplacer.java
@@ -43,6 +43,7 @@
 import kodkod.ast.QuantifiedFormula;
 import kodkod.ast.RelationPredicate;
 import kodkod.ast.UnaryTempFormula;
+import kodkod.ast.operator.TemporalOperator;
 import kodkod.ast.visitor.AbstractReplacer;
 
 /**
@@ -266,8 +267,14 @@ public Formula visit(BinaryTempFormula tf) {
 
 		if (negated) {
 			switch (tf.op()) {
-			case UNTIL: case RELEASES: case SINCE: case TRIGGERED:
-				return cache(tf,tf.left().accept(this).compose(tf.op(),tf.right().accept(this)));
+			case UNTIL:
+				return cache(tf,tf.left().accept(this).compose(TemporalOperator.RELEASES,tf.right().accept(this)));
+			case RELEASES:
+				return cache(tf,tf.left().accept(this).compose(TemporalOperator.UNTIL,tf.right().accept(this)));
+			case SINCE:
+				return cache(tf,tf.left().accept(this).compose(TemporalOperator.TRIGGERED,tf.right().accept(this)));
+			case TRIGGERED:
+				return cache(tf,tf.left().accept(this).compose(TemporalOperator.SINCE,tf.right().accept(this)));
 			default:
 				negated = !negated;
 				Formula temp1 = tf.left().accept(this);