documentation

Author: nmacedo

src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyright (c) 2014-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -49,7 +50,10 @@
 import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig;
 import edu.mit.csail.sdg.alloy4compiler.ast.Sig.SubsetSig;
 
-/** This helper class contains helper routines for reading an A4Solution object from an XML file. */
+/** This helper class contains helper routines for reading an A4Solution object from an XML file. 
+ * 
+ * @modified: nmm
+ * */
 
 public final class A4SolutionReader {
 
@@ -72,7 +76,7 @@ public final class A4SolutionReader {
     private final Map<String,Sig> id2sig = new LinkedHashMap<String,Sig>();
 
     /** Stores the set of all sigs. */
-    private final Set<Sig> allsigs = Util.asSet((Sig)UNIV, SIGINT, SEQIDX, STRING, NONE, TIME);  //pt.uminho.haslab
+    private final Set<Sig> allsigs = Util.asSet((Sig)UNIV, SIGINT, SEQIDX, STRING, NONE, TIME);  //pt.uminho.haslab: time sigs
 
     /** Mapes each expression we've seen to its TupleSet. */
     private final Map<Expr,TupleSet> expr2ts = new LinkedHashMap<Expr,TupleSet>();
@@ -138,7 +142,7 @@ private Sig parseSig(String id, int depth) throws IOException, Err {
            if (label.equals(SIGINT.label)) { id2sig.put(id, SIGINT); return SIGINT; }
            if (label.equals(SEQIDX.label)) { id2sig.put(id, SEQIDX); return SEQIDX; }
            if (label.equals(STRING.label)) { id2sig.put(id, STRING); return STRING; }
-           if (label.equals(TIME.label))   { id2sig.put(id, TIME);   return TIME; } // pt.uminho.haslab
+           if (label.equals(TIME.label))   { id2sig.put(id, TIME);   return TIME; } // pt.uminho.haslab: time sigs
            throw new IOException("Unknown builtin sig: "+label+" (id="+id+")");
         }
         if (depth > nmap.size()) throw new IOException("Sig "+label+" (id="+id+") is in a cyclic inheritance relationship.");

src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyright (c) 2015-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -37,7 +38,10 @@
 import edu.mit.csail.sdg.alloy4compiler.ast.Sig.SubsetSig;
 import edu.mit.csail.sdg.alloy4compiler.ast.Type;
 
-/** This helper class contains helper routines for writing an A4Solution object out as an XML file. */
+/** This helper class contains helper routines for writing an A4Solution object out as an XML file. 
+ * 
+ * @modified: nmm
+ * */
 
 public final class A4SolutionWriter {
 
@@ -108,6 +112,7 @@ private boolean writeExpr(String prefix, Expr expr) throws Err {
     }
 
     /** Write the given Sig. */
+    // pt.uminho.haslab: extended with time sigs
     private A4TupleSet writesig(final Sig x) throws Err {
        A4TupleSet ts = null, ts2 = null;
        if (x==Sig.NONE) return null; // should not happen, but we test for it anyway
@@ -130,7 +135,7 @@ private A4TupleSet writesig(final Sig x) throws Err {
        if (x.isEnum!=null) out.print("\" enum=\"yes");
        out.print("\">\n");
        try {
-           if (sol!=null && x!=Sig.UNIV && x!=Sig.SIGINT && x!=Sig.SEQIDX && x!=Sig.TIME) { // pt.uminho.haslab
+           if (sol!=null && x!=Sig.UNIV && x!=Sig.SIGINT && x!=Sig.SEQIDX && x!=Sig.TIME) { // pt.uminho.haslab: time sigs
               ts = (A4TupleSet)(sol.eval(x));
               for(A4Tuple t: ts.minus(ts2))  Util.encodeXMLs(out, "   <atom label=\"", t.atom(0), "\"/>\n");
            }
@@ -174,15 +179,16 @@ private void writeSkolem(ExprVar x) throws Err {
     }
 
     /** If sol==null, write the list of Sigs as a Metamodel, else write the solution as an XML file. */
+    // pt.uminho.haslab: extended with time scopes and sigs
     private A4SolutionWriter(A4Reporter rep, A4Solution sol, Iterable<Sig> sigs, int bitwidth, int maxseq, int time, int loop, String originalCommand, String originalFileName, PrintWriter out, Iterable<Func> extraSkolems) throws Err {
     	this.rep = rep;
         this.out = out;
         this.sol = sol;
         for (Sig s:sigs) if (s instanceof PrimSig && ((PrimSig)s).parent==Sig.UNIV) toplevels.add((PrimSig)s);
         out.print("<instance bitwidth=\""); out.print(bitwidth);
         out.print("\" maxseq=\""); out.print(maxseq);
-        out.print("\" time=\""); out.print(time); // pt.uminho.haslab
-        out.print("\" loop=\""); out.print(loop); // pt.uminho.haslab
+        out.print("\" time=\""); out.print(time); // pt.uminho.haslab: time scopes
+        out.print("\" loop=\""); out.print(loop); // pt.uminho.haslab: time scopes
         out.print("\" command=\""); Util.encodeXML(out, originalCommand);
         out.print("\" filename=\""); Util.encodeXML(out, originalFileName);
         if (sol==null) out.print("\" metamodel=\"yes");
@@ -223,11 +229,12 @@ private A4SolutionWriter(A4Reporter rep, A4Solution sol, Iterable<Sig> sigs, int
     }
 
     /** If this solution is a satisfiable solution, this method will write it out in XML format. */
+    // pt.uminho.haslab: extended with time scopes and sigs
     static void writeInstance(A4Reporter rep, A4Solution sol, PrintWriter out, Iterable<Func> extraSkolems, Map<String,String> sources) throws Err {
         if (!sol.satisfiable()) throw new ErrorAPI("This solution is unsatisfiable.");
         try {
             Util.encodeXMLs(out, "<alloy builddate=\"", Version.buildDate(), "\">\n\n");
-            new A4SolutionWriter(rep, sol, sol.getAllReachableSigs(), sol.getBitwidth(), sol.getMaxSeq(), sol.getTime(), sol.getLoop(), sol.getOriginalCommand(), sol.getOriginalFilename(), out, extraSkolems);  // pt.uminho.haslab
+            new A4SolutionWriter(rep, sol, sol.getAllReachableSigs(), sol.getBitwidth(), sol.getMaxSeq(), sol.getTime(), sol.getLoop(), sol.getOriginalCommand(), sol.getOriginalFilename(), out, extraSkolems);  // pt.uminho.haslab: time scopes
             if (sources!=null) for(Map.Entry<String,String> e: sources.entrySet()) {
                 Util.encodeXMLs(out, "\n<source filename=\"", e.getKey(), "\" content=\"", e.getValue(), "\"/>\n");
             }
@@ -239,9 +246,10 @@ static void writeInstance(A4Reporter rep, A4Solution sol, PrintWriter out, Itera
     }
 
     /** Write the metamodel as &lt;instance&gt;..&lt;/instance&gt; in XML format. */
+    // pt.uminho.haslab: extended with time scopes and sigs
     public static void writeMetamodel(ConstList<Sig> sigs, String originalFilename, PrintWriter out) throws Err {
         try {
-            new A4SolutionWriter(null, null, sigs, 4, 4, 4, 4, "show metamodel", originalFilename, out, null);  // pt.uminho.haslab
+            new A4SolutionWriter(null, null, sigs, 4, 4, 4, 4, "show metamodel", originalFilename, out, null);  // pt.uminho.haslab: time scopes
         } catch(Throwable ex) {
             if (ex instanceof Err) throw (Err)ex; else throw new ErrorFatal("Error writing the solution XML file.", ex);
         }

src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyrght (c) 2015-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -70,6 +71,8 @@
  * <br> we will give an error message.
  *
  * <p> Please see ScopeComputer.java for the exact rules for deriving the missing scopes.
+ * 
+ * @modified: nmm
  */
 
 final class ScopeComputer {
@@ -91,7 +94,7 @@ final class ScopeComputer {
     /** The number of STRING atoms to allocate; -1 if it was not specified. */
     private int maxstring = (-1);
 
-    private int time = (-1); // pt.uminho.haslab
+    private int time = (-1); // pt.uminho.haslab: time scopes
 
     /** The scope for each sig. */
     private final IdentityHashMap<PrimSig,Integer> sig2scope = new IdentityHashMap<PrimSig,Integer>();
@@ -110,7 +113,7 @@ public int sig2scope(Sig sig) {
         if (sig==SIGINT) return 1<<bitwidth;
         if (sig==SEQIDX) return maxseq;
         if (sig==STRING) return maxstring;
-        if (sig==TIME) return time;  // pt.uminho.haslab
+        if (sig==TIME) return time;  // pt.uminho.haslab: time scopes
         Integer y = sig2scope.get(sig);
         return (y==null) ? (-1) : y;
     }
@@ -129,7 +132,7 @@ private void sig2scope(Sig sig, int newValue) throws Err {
 
     /** Returns whether the scope of a sig is exact or not. */
     public boolean isExact(Sig sig) {
-        return sig==SIGINT || sig==SEQIDX || sig==STRING || sig==TIME || ((sig instanceof PrimSig) && exact.containsKey(sig)); // pt.uminho.haslab
+        return sig==SIGINT || sig==SEQIDX || sig==STRING || sig==TIME || ((sig instanceof PrimSig) && exact.containsKey(sig)); // pt.uminho.haslab: time scopes
     }
 
     /** Make the given sig "exact". */
@@ -271,6 +274,7 @@ private int computeLowerBound(final PrimSig sig) throws Err {
     //===========================================================================================================================//
 
     /** Compute the scopes, based on the settings in the "cmd", then log messages to the reporter. */
+    // pt.uminho.haslab: extended with time scopes
     private ScopeComputer(A4Reporter rep, Iterable<Sig> sigs, Command cmd) throws Err {
         this.rep = rep;
         this.cmd = cmd;
@@ -329,9 +333,9 @@ private ScopeComputer(A4Reporter rep, Iterable<Sig> sigs, Command cmd) throws Er
         for(Sig s:sigs) if (s.isTopLevel()) computeLowerBound((PrimSig)s);
         int max = max(), min = min();
         if (max >= min) for(int i=min; i<=max; i++) atoms.add(""+i);
-        time = cmd.time; // pt.uminho.haslab
-        sig2scope.put(TIME, time < 1 ? 0 : time); // pt.uminho.haslab
-        if (time > 0) for(int i=0; i<time; i++) atoms.add("Time$"+i); // pt.uminho.haslab
+        time = cmd.time; // pt.uminho.haslab: time scopes
+        sig2scope.put(TIME, time < 1 ? 0 : time); // pt.uminho.haslab: time scopes
+        if (time > 0) for(int i=0; i<time; i++) atoms.add("Time$"+i); // pt.uminho.haslab: time scopes
     }
 
     /** Whether or not Int appears in the relation types found in these sigs */

src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyright (c) 2015-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -75,7 +76,10 @@
 import edu.mit.csail.sdg.alloy4compiler.ast.Type;
 import edu.mit.csail.sdg.alloy4compiler.ast.VisitReturn;
 
-/** Translate an Alloy AST into Kodkod AST then attempt to solve it using Kodkod. */
+/** Translate an Alloy AST into Kodkod AST then attempt to solve it using Kodkod. 
+ * 
+ * @modifed: nmm
+ * */
 
 public final class TranslateAlloyToKodkod extends VisitReturn<Object> {
 
@@ -414,6 +418,7 @@ public static A4Solution execute_command (A4Reporter rep, Iterable<Sig> sigs, Co
      * <p> If the return value X is satisfiable, you can call X.next() to get the next satisfying solution X2;
      * and you can call X2.next() to get the next satisfying solution X3... until you get an unsatisfying solution.
      */
+    // pt.uminho.haslab: extended for timed iterations
     public static A4Solution execute_commandFromBook (A4Reporter rep, Iterable<Sig> sigs, Command cmd, A4Options opt) throws Err {
         if (rep==null) rep = A4Reporter.NOP;
         TranslateAlloyToKodkod tr = null;
@@ -599,10 +604,10 @@ private static Relation right(Expression x) {
           case MIN: return IntConstant.constant(min); //TODO
           case MAX: return IntConstant.constant(max); //TODO
           case NEXT: return A4Solution.KK_NEXT;
-          case NEXTTIME: return A4Solution.KK_TIMENEXT; // pt.uminho.haslab
-          case END: return A4Solution.KK_TIMEEND; // pt.uminho.haslab
-          case LOOP: return A4Solution.KK_TIMELOOP; // pt.uminho.haslab
-          case INIT: return A4Solution.KK_TIMEINIT; // pt.uminho.haslab
+          case NEXTTIME: return A4Solution.KK_TIMENEXT; // pt.uminho.haslab: time relations (deprecated)
+          case END: return A4Solution.KK_TIMEEND; // pt.uminho.haslab: time relations (deprecated)
+          case LOOP: return A4Solution.KK_TIMELOOP; // pt.uminho.haslab: time relations (deprecated)
+          case INIT: return A4Solution.KK_TIMEINIT; // pt.uminho.haslab: time relations (deprecated)
           case TRUE: return Formula.TRUE;
           case FALSE: return Formula.FALSE;
           case EMPTYNESS: return Expression.NONE;

src/edu/mit/csail/sdg/alloy4compiler/translator/TranslateAlloyToKodkod.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyright (c) 2015-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -20,6 +21,8 @@
 /** Immutable; represents an Alloy toplevel signature or an Alloy subsignature.
  *
  * <p><b>Thread Safety:</b> Can be called only by the AWT event thread.
+ * 
+ * @modified: nmm
  */
 
 public final class AlloyType extends AlloyNodeElement {
@@ -40,7 +43,7 @@ public final class AlloyType extends AlloyNodeElement {
    public static final AlloyType SET=new AlloyType("set", false, false, false, false, false, false);
 
 
-   public static final AlloyType TIME=new AlloyType("Time", false, false, true, false, false, false); // pt.uminho.haslab
+   public static final AlloyType TIME=new AlloyType("Time", false, false, true, false, false, false); // pt.uminho.haslab: time types (deprecated)
 
 
    /** Constructs an AlloyType object with that name. */

src/edu/mit/csail/sdg/alloy4viz/AlloyType.java

@@ -1,4 +1,5 @@
 /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
+ * Electrum -- Copyright (c) 2015-present, Nuno Macedo
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
  * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
@@ -94,7 +95,7 @@ private AlloyType makeType(String label, boolean isOne, boolean isAbstract, bool
 
    /** Create a new AlloySet whose label is unambiguous with any existing one. */
    private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, AlloyType type) {
-      while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab
+      while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab: time sigs
       while(true) {
          AlloySet ans = new AlloySet(label, isPrivate, isMeta, type);
          if (!sets.contains(ans)) return ans;
@@ -104,7 +105,7 @@ private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, AlloyT
 
    /** Create a new AlloyRelation whose label is unambiguous with any existing one. */
    private AlloyRelation makeRel(String label, boolean isPrivate, boolean isMeta, List<AlloyType> types) {
-      while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab
+      while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab: time sigs
       while(true) {
          AlloyRelation ans = new AlloyRelation(label, isPrivate, isMeta, types);
          if (!rels.containsKey(ans)) return ans;
@@ -212,6 +213,7 @@ private void setOrRel(A4Solution sol, String label, Expr expr, boolean isPrivate
    }
 
    /** Parse the file into an AlloyInstance if possible. */
+   // pt.uminho.haslab: extended with time sigs
    private StaticInstanceReader(XMLNode root) throws Err {
       XMLNode inst = null;
       for(XMLNode sub: root) if (sub.is("instance")) { inst=sub; break; }
@@ -224,7 +226,7 @@ private StaticInstanceReader(XMLNode root) throws Err {
          sig2type.put(Sig.SIGINT, AlloyType.INT);
          sig2type.put(Sig.SEQIDX, AlloyType.SEQINT);
          sig2type.put(Sig.STRING, AlloyType.STRING);
-         sig2type.put(Sig.TIME, AlloyType.TIME); // pt.uminho.haslab
+         sig2type.put(Sig.TIME, AlloyType.TIME); // pt.uminho.haslab: time sigs
          ts.put(AlloyType.SEQINT, AlloyType.INT);
          for(int i=sol.min(), max=sol.max(), maxseq=sol.getMaxSeq(); i<=max; i++) {
             AlloyAtom at = new AlloyAtom(i>=0 && i<maxseq ? AlloyType.SEQINT : AlloyType.INT, i, ""+i);
@@ -262,7 +264,7 @@ private StaticInstanceReader(XMLNode root) throws Err {
          AlloyAtom intAtom = sig2atom.get(Sig.SIGINT);
          AlloyAtom seqAtom = sig2atom.get(Sig.SEQIDX);
          AlloyAtom strAtom = sig2atom.get(Sig.STRING);
-         AlloyAtom timAtom = sig2atom.get(Sig.TIME); // pt.uminho.haslab
+         AlloyAtom timAtom = sig2atom.get(Sig.TIME); // pt.uminho.haslab: time sigs
          for(Set<AlloyTuple> t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(univAtom)) { univAtom=null; break; }
          for(Set<AlloyTuple> t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(intAtom)) { intAtom=null; break; }
          for(Set<AlloyTuple> t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(seqAtom)) { seqAtom=null; break; }
@@ -282,7 +284,7 @@ private StaticInstanceReader(XMLNode root) throws Err {
             }
             atom2sets.remove(strAtom);
          }
-         if (timAtom!=null) { // pt.uminho.haslab
+         if (timAtom!=null) { // pt.uminho.haslab: time sigs
              for(Iterator<AlloyTuple> it=exts.iterator(); it.hasNext();) {
                 AlloyTuple at=it.next();
                 if (at.getStart()==timAtom || at.getEnd()==timAtom) it.remove();