Skip to content

Commit

Permalink
documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmacedo
nmacedo committed Jun 3, 2016
1 parent d4031c3 commit fdce4be
Show file tree
Hide file tree
Showing 9 changed files with 1,163 additions and 1,121 deletions.
2,190 changes: 1,099 additions & 1,091 deletions src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java
View file

Large diffs are not rendered by default.

10 changes: 7 additions & 3 deletions src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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 {

Expand All @@ -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>();
Expand Down Expand Up @@ -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.");
Expand Down
20 changes: 14 additions & 6 deletions src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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 {

Expand Down Expand Up @@ -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
Expand All @@ -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");
}
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
}
Expand All @@ -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);
}
Expand Down
16 changes: 10 additions & 6 deletions src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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 {
Expand All @@ -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>();
Expand All @@ -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;
}
Expand All @@ -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". */
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 */
Expand Down
15 changes: 10 additions & 5 deletions src/edu/mit/csail/sdg/alloy4compiler/translator/TranslateAlloyToKodkod.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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> {

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down
5 changes: 4 additions & 1 deletion src/edu/mit/csail/sdg/alloy4viz/AlloyType.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand All @@ -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 {
Expand All @@ -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. */
Expand Down
12 changes: 7 additions & 5 deletions src/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java
View file
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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; }
Expand All @@ -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);
Expand Down Expand Up @@ -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; }
Expand All @@ -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();
Expand Down
Loading

0 comments on commit fdce4be

Please sign in to comment.