fixed bug on var one sigs' bounds

haslab · Nov 10, 2016 · a435344 · a435344
1 parent 2032198
commit a435344
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 4 deletions.
diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/Expr.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/Expr.java
@@ -734,4 +734,13 @@ public final Decl setOf(String label) throws Err {
     * <p> this must be an integer expression
     */
    public final Expr cast2sigint() { return ExprUnary.Op.CAST2SIGINT.make(span(), this); }
+
+   // [HASLab]
+   public final Expr always() { return ExprUnary.Op.ALWAYS.make(span(), this); }
+   public final Expr eventually() { return ExprUnary.Op.EVENTUALLY.make(span(), this); }
+   public final Expr after() { return ExprUnary.Op.AFTER.make(span(), this); }
+   public final Expr previous() { return ExprUnary.Op.PREVIOUS.make(span(), this); }
+   public final Expr historically() { return ExprUnary.Op.HISTORICALLY.make(span(), this); }
+   public final Expr once() { return ExprUnary.Op.ONCE.make(span(), this); }
+
 }
diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java
@@ -454,11 +454,11 @@ Relation addRel(String label, TupleSet lower, TupleSet upper, Expr expr) throws
 		if (solved) throw new ErrorFatal("Cannot add a Kodkod relation since solve() has completed.");
 		Relation rel;
 		if (expr instanceof  Field){
-			if (((Field) expr).isVariable != null){rel = VarRelation.nary(label, upper.arity());}
+			if (((Field) expr).isVariable != null){rel = VarRelation.nary(label, upper.arity());} // [HASLab]
 			else{rel = Relation.nary(label, upper.arity());}
 		}  else {
 			if (expr instanceof  Sig){
-				if (((Sig) expr).isVariable != null){rel = VarRelation.nary(label, upper.arity());}
+				if (((Sig) expr).isVariable != null){rel = VarRelation.nary(label, upper.arity());} // [HASLab]
 				else{rel = Relation.nary(label, upper.arity());}
 			}else{
 				rel = Relation.nary(label, upper.arity());

diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/BoundsComputer.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/BoundsComputer.java
@@ -143,6 +143,8 @@ private Expression allocatePrimSig(PrimSig sig) throws Err {
             Expression relation = sol.addRel(sig.label+" remainder", lower, upper, sig);
             sum = sum.union(relation);
         }
+        if (sig.isOne != null) // [HASLab]
+        	sol.addFormula(sum.one().always(), sig.isOne);
         sol.addSig(sig, sum);
         return sum;
     }

diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java
@@ -308,8 +308,10 @@ private ScopeComputer(A4Reporter rep, Iterable<Sig> sigs, Command cmd) throws Er
             if (exact) makeExact(cmd.pos, s);
         }
         // Force "one" sigs to be exactly one, and "lone" to be at most one
-        for(Sig s:sigs) if (s instanceof PrimSig) {
-            if (s.isOne!=null) { makeExact(cmd.pos, s); sig2scope(s,1); } else if (s.isLone!=null && sig2scope(s)!=0) sig2scope(s,1);
+        for(Sig s:sigs) if (s instanceof PrimSig) { // [HASLab]
+            if (s.isOne!=null && s.isVariable==null) { makeExact(cmd.pos, s); sig2scope(s,1); } 
+            if (s.isOne!=null && s.isVariable!=null) { sig2scope(s,1); } 
+            else if (s.isLone!=null && sig2scope(s)!=0) sig2scope(s,1);
         }
         // Derive the implicit scopes
         while(true) {