From 5baad82bf92e6873a2933a857337fc3dd76f0c69 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 20 Sep 2019 13:50:41 +0200
Subject: [PATCH] support tuple definitions in UNCHANGED
UNCHANGED can now contain definitions
which themselves are tuples
---
src/main/java/de/tla2b/analysis/BOperation.java | 17 +++++++++++++----
1 file changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index bc00f86..dd673d8 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -378,16 +378,20 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
OpApplNode var = (OpApplNode) k.getArgs()[i];
//findUnchangedVariablesInOpApplNode(var);
// System.out.println("var.getOperator() = " + var.getOperator().getName() + " at " + var.getOperator() + " of class " + var.getOperator().getClass().getSimpleName());
- // TO DO: support OpDefNode
if(var.getOperator() instanceof OpDefNode) {
+ // we have a definition
OpDefNode def = (OpDefNode) var.getOperator();
if(def.getParams().length > 0) {
+ // we do not support definitions with arguments yet
throw new RuntimeException("Declaration with parameters not supported for UNCHANGED: " + var.getOperator().getName() + " " + var.getLocation());
}
ExprNode body = def.getBody();
- //if(body instanceof OpApplNode)
- //System.out.println("Body = " + body + " of class " + body.getClass().getSimpleName());
- throw new RuntimeException("Declaration not yet supported for UNCHANGED: " + var.getOperator().getName() + " defined at " + body + " used at " + var.getLocation());
+ // System.out.println("Body = " + body + " of class " + body.getClass().getSimpleName());
+ if(body instanceof OpApplNode) {
+ OpApplNode obody = (OpApplNode) body;
+ // System.out.println("Operator = " + obody.getOperator()); // In module --TLA+ BUILTINS--
+ findUnchangedVariablesInOpApplNode(obody);
+ }
} else if(!(var.getOperator() instanceof OpDeclNode)) {
throw new RuntimeException("cannot convert to list of unchanged variables: " + var.getOperator().getName() + " " + var.getLocation());
} else {
@@ -403,6 +407,11 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
}
+
+
+ private void addUnchangedVariablesInOpApplNodeTuple(OpApplNode k) {
+
+ }
}
--
GitLab