-
Notifications
You must be signed in to change notification settings - Fork 122
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[recursion] Fixes the infinite recursion in the check for integers an… (
#22) * [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)
- Loading branch information
Showing
51 changed files
with
171 additions
and
16 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
File renamed without changes
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
138 changes: 138 additions & 0 deletions
138
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<T> extends VisitQuery<T> { | ||
| final Set<Expr> 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); | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
5 changes: 5 additions & 0 deletions
5
org.alloytools.alloy.core/src/test/resources/test-recursion.als
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |