From b145939afef2665dd4e89f9183985c214df47152 Mon Sep 17 00:00:00 2001 From: Peter Kriens Date: Fri, 17 Nov 2017 20:28:42 +0100 Subject: [PATCH] =?UTF-8?q?[recursion]=20Fixes=20the=20infinite=20recursio?= =?UTF-8?q?n=20in=20the=20check=20for=20integers=20an=E2=80=A6=20(#22)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * [recursion] Fixes the infinite recursion in the check for integers and strings * [recurs] More output and added hamcrest. * [recurs] Wrong project * [recurse] Tests need sat4j on the path * [recurse] Running in some problems with the split - Moved models to core - Application had wrong resource directory - Core gradle file was including a wrong dependency (all deps must go through bnd) --- org.alloytools.alloy.application/.classpath | 2 +- org.alloytools.alloy.application/bnd.bnd | 6 +- .../resources/images/24_execute.gif | Bin .../resources/images/24_execute_abort2.gif | Bin .../{ => main}/resources/images/24_graph.gif | Bin .../resources/images/24_history.gif | Bin .../{ => main}/resources/images/24_new.gif | Bin .../{ => main}/resources/images/24_open.gif | Bin .../resources/images/24_plaintext.gif | Bin .../{ => main}/resources/images/24_reload.gif | Bin .../{ => main}/resources/images/24_save.gif | Bin .../resources/images/24_settings.gif | Bin .../resources/images/24_settings_apply.gif | Bin .../resources/images/24_settings_apply2.gif | Bin .../resources/images/24_settings_apply3.gif | Bin .../resources/images/24_settings_close.gif | Bin .../resources/images/24_settings_close2.gif | Bin .../resources/images/24_settings_close3.gif | Bin .../resources/images/24_settings_close4.gif | Bin .../resources/images/24_settings_close5.gif | Bin .../resources/images/24_texttree.gif | Bin .../src/{ => main}/resources/images/cb0.gif | Bin .../src/{ => main}/resources/images/cb1.gif | Bin .../src/{ => main}/resources/images/logo.gif | Bin .../src/{ => main}/resources/images/menu0.gif | Bin .../src/{ => main}/resources/images/menu1.gif | Bin .../src/{ => main}/resources/images/tcb01.gif | Bin .../src/{ => main}/resources/images/tcb02.gif | Bin .../src/{ => main}/resources/images/tcb03.gif | Bin .../src/{ => main}/resources/images/tcb04.gif | Bin org.alloytools.alloy.core/.classpath | 3 +- org.alloytools.alloy.core/bnd.bnd | 8 +- org.alloytools.alloy.core/build.gradle | 4 - .../java/edu/mit/csail/sdg/ast/Command.java | 8 +- .../edu/mit/csail/sdg/ast/VisitQuery.java | 5 +- .../edu/mit/csail/sdg/ast/VisitQueryOnce.java | 138 ++++++++++++++++++ .../edu/mit/csail/sdg/parser/CompUtil.java | 3 +- .../src/{ => main}/resources/.gitignore | 0 .../main}/resources/models/util/boolean.als | 0 .../src/main}/resources/models/util/graph.als | 0 .../main}/resources/models/util/integer.als | 0 .../main}/resources/models/util/natural.als | 0 .../main}/resources/models/util/ordering.als | 0 .../main}/resources/models/util/relation.als | 0 .../main}/resources/models/util/seqrel.als | 0 .../main}/resources/models/util/sequence.als | 0 .../main}/resources/models/util/sequniv.als | 0 .../main}/resources/models/util/ternary.als | 0 .../src/main}/resources/models/util/time.als | 0 .../alloy/core}/AlloyModelsTest.java | 5 +- .../src/test/resources/test-recursion.als | 5 + 51 files changed, 171 insertions(+), 16 deletions(-) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_execute.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_execute_abort2.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_graph.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_history.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_new.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_open.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_plaintext.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_reload.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_save.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_apply.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_apply2.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_apply3.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_close.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_close2.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_close3.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_close4.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_settings_close5.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/24_texttree.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/cb0.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/cb1.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/logo.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/menu0.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/menu1.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/tcb01.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/tcb02.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/tcb03.gif (100%) rename org.alloytools.alloy.application/src/{ => main}/resources/images/tcb04.gif (100%) create mode 100644 org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java rename org.alloytools.alloy.core/src/{ => main}/resources/.gitignore (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/boolean.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/graph.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/integer.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/natural.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/ordering.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/relation.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/seqrel.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/sequence.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/sequniv.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/ternary.als (100%) rename {org.alloytools.alloy.application/src => org.alloytools.alloy.core/src/main}/resources/models/util/time.als (100%) rename {org.alloytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole => org.alloytools.alloy.core/src/test/java/org/alloytools/alloy/core}/AlloyModelsTest.java (91%) create mode 100644 org.alloytools.alloy.core/src/test/resources/test-recursion.als diff --git a/org.alloytools.alloy.application/.classpath b/org.alloytools.alloy.application/.classpath index aa743ce76..55864cdf7 100644 --- a/org.alloytools.alloy.application/.classpath +++ b/org.alloytools.alloy.application/.classpath @@ -2,7 +2,7 @@ - + diff --git a/org.alloytools.alloy.application/bnd.bnd b/org.alloytools.alloy.application/bnd.bnd index 152b19190..9c71999a4 100644 --- a/org.alloytools.alloy.application/bnd.bnd +++ b/org.alloytools.alloy.application/bnd.bnd @@ -1,5 +1,5 @@ -includeresource: \ - src/resources + src/main/resources -buildpath: \ lib/apple-osx-ui.jar;version=file,\ @@ -7,7 +7,9 @@ org.alloytools.kodkod.core;version=latest -testpath: \ - osgi.enroute.junit.wrapper + osgi.enroute.junit.wrapper, \ + osgi.enroute.hamcrest.wrapper, \ + org.sat4j.core Private-Package: \ edu.mit.csail.sdg.alloy4graph,\ diff --git a/org.alloytools.alloy.application/src/resources/images/24_execute.gif b/org.alloytools.alloy.application/src/main/resources/images/24_execute.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_execute.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_execute.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_execute_abort2.gif b/org.alloytools.alloy.application/src/main/resources/images/24_execute_abort2.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_execute_abort2.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_execute_abort2.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_graph.gif b/org.alloytools.alloy.application/src/main/resources/images/24_graph.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_graph.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_graph.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_history.gif b/org.alloytools.alloy.application/src/main/resources/images/24_history.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_history.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_history.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_new.gif b/org.alloytools.alloy.application/src/main/resources/images/24_new.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_new.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_new.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_open.gif b/org.alloytools.alloy.application/src/main/resources/images/24_open.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_open.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_open.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_plaintext.gif b/org.alloytools.alloy.application/src/main/resources/images/24_plaintext.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_plaintext.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_plaintext.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_reload.gif b/org.alloytools.alloy.application/src/main/resources/images/24_reload.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_reload.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_reload.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_save.gif b/org.alloytools.alloy.application/src/main/resources/images/24_save.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_save.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_save.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_apply.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_apply.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_apply.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_apply.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_apply2.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_apply2.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_apply2.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_apply2.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_apply3.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_apply3.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_apply3.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_apply3.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_close.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_close.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_close.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_close.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_close2.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_close2.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_close2.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_close2.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_close3.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_close3.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_close3.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_close3.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_close4.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_close4.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_close4.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_close4.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_settings_close5.gif b/org.alloytools.alloy.application/src/main/resources/images/24_settings_close5.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_settings_close5.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_settings_close5.gif diff --git a/org.alloytools.alloy.application/src/resources/images/24_texttree.gif b/org.alloytools.alloy.application/src/main/resources/images/24_texttree.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/24_texttree.gif rename to org.alloytools.alloy.application/src/main/resources/images/24_texttree.gif diff --git a/org.alloytools.alloy.application/src/resources/images/cb0.gif b/org.alloytools.alloy.application/src/main/resources/images/cb0.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/cb0.gif rename to org.alloytools.alloy.application/src/main/resources/images/cb0.gif diff --git a/org.alloytools.alloy.application/src/resources/images/cb1.gif b/org.alloytools.alloy.application/src/main/resources/images/cb1.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/cb1.gif rename to org.alloytools.alloy.application/src/main/resources/images/cb1.gif diff --git a/org.alloytools.alloy.application/src/resources/images/logo.gif b/org.alloytools.alloy.application/src/main/resources/images/logo.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/logo.gif rename to org.alloytools.alloy.application/src/main/resources/images/logo.gif diff --git a/org.alloytools.alloy.application/src/resources/images/menu0.gif b/org.alloytools.alloy.application/src/main/resources/images/menu0.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/menu0.gif rename to org.alloytools.alloy.application/src/main/resources/images/menu0.gif diff --git a/org.alloytools.alloy.application/src/resources/images/menu1.gif b/org.alloytools.alloy.application/src/main/resources/images/menu1.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/menu1.gif rename to org.alloytools.alloy.application/src/main/resources/images/menu1.gif diff --git a/org.alloytools.alloy.application/src/resources/images/tcb01.gif b/org.alloytools.alloy.application/src/main/resources/images/tcb01.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/tcb01.gif rename to org.alloytools.alloy.application/src/main/resources/images/tcb01.gif diff --git a/org.alloytools.alloy.application/src/resources/images/tcb02.gif b/org.alloytools.alloy.application/src/main/resources/images/tcb02.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/tcb02.gif rename to org.alloytools.alloy.application/src/main/resources/images/tcb02.gif diff --git a/org.alloytools.alloy.application/src/resources/images/tcb03.gif b/org.alloytools.alloy.application/src/main/resources/images/tcb03.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/tcb03.gif rename to org.alloytools.alloy.application/src/main/resources/images/tcb03.gif diff --git a/org.alloytools.alloy.application/src/resources/images/tcb04.gif b/org.alloytools.alloy.application/src/main/resources/images/tcb04.gif similarity index 100% rename from org.alloytools.alloy.application/src/resources/images/tcb04.gif rename to org.alloytools.alloy.application/src/main/resources/images/tcb04.gif diff --git a/org.alloytools.alloy.core/.classpath b/org.alloytools.alloy.core/.classpath index aa743ce76..76b65c0d5 100644 --- a/org.alloytools.alloy.core/.classpath +++ b/org.alloytools.alloy.core/.classpath @@ -2,7 +2,8 @@ - + + diff --git a/org.alloytools.alloy.core/bnd.bnd b/org.alloytools.alloy.core/bnd.bnd index f91f218ac..cf408c336 100644 --- a/org.alloytools.alloy.core/bnd.bnd +++ b/org.alloytools.alloy.core/bnd.bnd @@ -1,4 +1,7 @@ +-includeresource: \ + src/main/resources + -buildpath: \ org.alloytools.kodkod.core;version=latest, \ org.sat4j.core,\ @@ -9,7 +12,10 @@ org.alloytools.kodkod.nativesat.x86-windows;version=latest -testpath: \ - osgi.enroute.junit.wrapper + osgi.enroute.junit.wrapper, \ + osgi.enroute.hamcrest.wrapper, \ + src/main/resources;version=file + Export-Package: \ edu.mit.csail.sdg.alloy4,\ diff --git a/org.alloytools.alloy.core/build.gradle b/org.alloytools.alloy.core/build.gradle index 095f3b44c..dd26cd987 100644 --- a/org.alloytools.alloy.core/build.gradle +++ b/org.alloytools.alloy.core/build.gradle @@ -1,9 +1,5 @@ apply plugin: 'java' -dependencies { - testCompile group: 'junit', name: 'junit', version: '4.12' -} - task jflex(type: JavaExec) { inputs.files("src/main/java/edu/mit/csail/sdg/parser/Alloy.lex") outputs.files("src/main/java/edu/mit/csail/sdg/parser/CompLexer.java") diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java index 855ec54c1..73bcad5cc 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java @@ -20,12 +20,12 @@ import java.util.List; import java.util.Set; -import edu.mit.csail.sdg.alloy4.Err; -import edu.mit.csail.sdg.alloy4.Pos; import edu.mit.csail.sdg.alloy4.ConstList; -import edu.mit.csail.sdg.alloy4.Util; import edu.mit.csail.sdg.alloy4.ConstList.TempList; +import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.alloy4.ErrorSyntax; +import edu.mit.csail.sdg.alloy4.Pos; +import edu.mit.csail.sdg.alloy4.Util; /** * Immutable; reresents a "run" or "check" command. @@ -269,7 +269,7 @@ public ConstList getGrowableSigs() { */ public Set getAllStringConstants(Iterable sigs) throws Err { final Set set = new HashSet(); - final VisitQuery findString = new VisitQuery() { + final VisitQuery findString = new VisitQueryOnce() { @Override public final Object visit(ExprConstant x) throws Err { if (x.op == ExprConstant.Op.STRING) diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java index 894c88a28..5755d68ca 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java @@ -15,6 +15,9 @@ package edu.mit.csail.sdg.ast; +import java.util.HashSet; +import java.util.Set; + import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.ast.Sig.Field; @@ -30,7 +33,7 @@ */ public abstract class VisitQuery extends VisitReturn { - + /** Constructs a VisitQuery object. */ public VisitQuery() {} diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java new file mode 100644 index 000000000..ce0710aae --- /dev/null +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java @@ -0,0 +1,138 @@ +package edu.mit.csail.sdg.ast; + +import java.util.HashSet; +import java.util.Set; + +import edu.mit.csail.sdg.alloy4.Err; +import edu.mit.csail.sdg.ast.Sig.Field; + +/** + * Acts like VisitQuery but never traverses a node more than once. + * + */ +public class VisitQueryOnce extends VisitQuery { + final Set visited = new HashSet<>(); + + @Override + public T visit(ExprBinary x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprList node F[X1,X2,X3..] by calling accept() on X1, X2, + * X3... + */ + @Override + public T visit(ExprList x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprCall node F[X1,X2,X3..] by calling accept() on X1, X2, + * X3... + */ + @Override + public T visit(ExprCall x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprConstant node (this default implementation simply returns + * null) + */ + @Override + public T visit(ExprConstant x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprITE node (C => X else Y) by calling accept() on C, X, then + * Y. + */ + @Override + public T visit(ExprITE x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprLet node (let a=x | y) by calling accept() on "a", "x", + * then "y". + */ + @Override + public T visit(ExprLet x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits an ExprQt node (all a,b,c:X1, d,e,f:X2... | F) by calling accept() + * on a,b,c,X1,d,e,f,X2... then on F. + */ + @Override + public T visit(ExprQt x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** Visits an ExprUnary node (OP X) by calling accept() on X. */ + @Override + public T visit(ExprUnary x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** + * Visits a ExprVar node (this default implementation simply returns null) + */ + @Override + public T visit(ExprVar x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** Visits a Sig node (this default implementation simply returns null) */ + @Override + public T visit(Sig x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + /** Visits a Field node (this default implementation simply returns null) */ + @Override + public T visit(Field x) throws Err { + if (visited(x)) + return null; + else + return super.visit(x); + } + + private boolean visited(Expr x) { + return visited.add(x); + } + +} diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompUtil.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompUtil.java index 945aa2192..9f4209a3e 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompUtil.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompUtil.java @@ -44,6 +44,7 @@ import edu.mit.csail.sdg.ast.Module; import edu.mit.csail.sdg.ast.Sig; import edu.mit.csail.sdg.ast.VisitQuery; +import edu.mit.csail.sdg.ast.VisitQueryOnce; import edu.mit.csail.sdg.ast.ExprUnary.Op; import edu.mit.csail.sdg.ast.Sig.Field; import edu.mit.csail.sdg.ast.Type.ProductType; @@ -150,7 +151,7 @@ public static boolean areIntsUsed(Iterable sigs, Command cmd) { /* check expressions; look for CAST2SIGING (Int[]) */ try { Object intTriggerNode; - intTriggerNode = cmd.formula.accept(new VisitQuery() { + intTriggerNode = cmd.formula.accept(new VisitQueryOnce() { @Override public Object visit(ExprCall x) throws Err { // skip integer arithmetic functions, because their diff --git a/org.alloytools.alloy.core/src/resources/.gitignore b/org.alloytools.alloy.core/src/main/resources/.gitignore similarity index 100% rename from org.alloytools.alloy.core/src/resources/.gitignore rename to org.alloytools.alloy.core/src/main/resources/.gitignore diff --git a/org.alloytools.alloy.application/src/resources/models/util/boolean.als b/org.alloytools.alloy.core/src/main/resources/models/util/boolean.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/boolean.als rename to org.alloytools.alloy.core/src/main/resources/models/util/boolean.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/graph.als b/org.alloytools.alloy.core/src/main/resources/models/util/graph.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/graph.als rename to org.alloytools.alloy.core/src/main/resources/models/util/graph.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/integer.als b/org.alloytools.alloy.core/src/main/resources/models/util/integer.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/integer.als rename to org.alloytools.alloy.core/src/main/resources/models/util/integer.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/natural.als b/org.alloytools.alloy.core/src/main/resources/models/util/natural.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/natural.als rename to org.alloytools.alloy.core/src/main/resources/models/util/natural.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/ordering.als b/org.alloytools.alloy.core/src/main/resources/models/util/ordering.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/ordering.als rename to org.alloytools.alloy.core/src/main/resources/models/util/ordering.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/relation.als b/org.alloytools.alloy.core/src/main/resources/models/util/relation.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/relation.als rename to org.alloytools.alloy.core/src/main/resources/models/util/relation.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/seqrel.als b/org.alloytools.alloy.core/src/main/resources/models/util/seqrel.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/seqrel.als rename to org.alloytools.alloy.core/src/main/resources/models/util/seqrel.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/sequence.als b/org.alloytools.alloy.core/src/main/resources/models/util/sequence.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/sequence.als rename to org.alloytools.alloy.core/src/main/resources/models/util/sequence.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/sequniv.als b/org.alloytools.alloy.core/src/main/resources/models/util/sequniv.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/sequniv.als rename to org.alloytools.alloy.core/src/main/resources/models/util/sequniv.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/ternary.als b/org.alloytools.alloy.core/src/main/resources/models/util/ternary.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/ternary.als rename to org.alloytools.alloy.core/src/main/resources/models/util/ternary.als diff --git a/org.alloytools.alloy.application/src/resources/models/util/time.als b/org.alloytools.alloy.core/src/main/resources/models/util/time.als similarity index 100% rename from org.alloytools.alloy.application/src/resources/models/util/time.als rename to org.alloytools.alloy.core/src/main/resources/models/util/time.als diff --git a/org.alloytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole/AlloyModelsTest.java b/org.alloytools.alloy.core/src/test/java/org/alloytools/alloy/core/AlloyModelsTest.java similarity index 91% rename from org.alloytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole/AlloyModelsTest.java rename to org.alloytools.alloy.core/src/test/java/org/alloytools/alloy/core/AlloyModelsTest.java index b3c597e20..5998af385 100644 --- a/org.alloytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole/AlloyModelsTest.java +++ b/org.alloytools.alloy.core/src/test/java/org/alloytools/alloy/core/AlloyModelsTest.java @@ -1,4 +1,5 @@ -package edu.mit.csail.sdg.alloy4whole; +package org.alloytools.alloy.core; + import org.junit.Test; @@ -18,11 +19,13 @@ public void testRecursion() throws Exception { Module world = CompUtil.parseEverything_fromFile(A4Reporter.NOP, null, filename); A4Options options = new A4Options(); + options.unrolls = 10; for (Command command : world.getAllCommands()) { A4Solution ans = TranslateAlloyToKodkod.execute_command(A4Reporter.NOP, world.getAllReachableSigs(), command, options); while (ans.satisfiable()) { String hc = "Answer: " + ans.toString().hashCode(); + System.out.println(hc); ans = ans.next(); } return; diff --git a/org.alloytools.alloy.core/src/test/resources/test-recursion.als b/org.alloytools.alloy.core/src/test/resources/test-recursion.als new file mode 100644 index 000000000..dbe0f9fd9 --- /dev/null +++ b/org.alloytools.alloy.core/src/test/resources/test-recursion.als @@ -0,0 +1,5 @@ +sig Foo { n : lone Foo } +pred a[ f : Foo ] { some f.n implies b[f.n] } +pred b[ f : Foo ] { some f.n implies a[f.n] } + +run a for 4 \ No newline at end of file