For more information about Alloy, http://alloytools.org
" + +"Questions and comments about Alloy are welcome at the community forum:
" + +"Alloy Community Forum: https://groups.google.com/forum/#!forum/alloytools
" + +"Alloy experts also respond to https://stackoverflow.com questions tagged alloy.
Major contributions to earlier versions of Alloy were made by: Felix Chang (v4);
"
+ +"Jonathan Edwards, Eunsuk Kang, Joe Near, Robert Seater, Derek Rayside, Greg Dennis,
"
+ +"Ilya Shlyakhter, Mana Taghdiri, Mandana Vaziri, Sarfraz Khurshid (v3); Manu Sridharan
"
+ +"(v2); Edmond Lau, Vincent Yeung, Sam Daitch, Andrew Yip, Jongmin Baek, Ning Song,
"
+ +"Arturo Arizpe, Li-kuo (Brian) Lin, Joseph Cohen, Jesse Pavel, Ian Schechter, Uriel
"
+ +"Schafer (v1).
The development of Alloy was funded by part by the National Science Foundation under
"
+ +"Grant Nos. 0325283, 0541183, 0438897 and 0707612; by the Air Force Research Laboratory
"
+ +"(AFRL/IF) and the Disruptive Technology Office (DTO) in the National Intelligence
"
+ +"Community Information Assurance Research (NICIAR) Program; and by the Nokia
"
+ +"Corporation as part of a collaboration between Nokia Research and MIT CSAIL.
" + +"Build Date: " + Version.buildDate()+""); + // @formatter:on + ta.setEditable(false); + ta.addHyperlinkListener((e) -> { + if (e.getEventType() == EventType.ACTIVATED) { + if (Desktop.isDesktopSupported() && Desktop.getDesktop().isSupported(Desktop.Action.BROWSE)) { + try { + Desktop.getDesktop().browse(e.getURL().toURI()); + } catch (IOException | URISyntaxException e1) { + // ignore + } + } + } + }); + OurDialog.showmsg("About Alloy Analyzer " + Version.version(), ta); + return null; } @@ -1520,7 +1590,8 @@ public final void hyperlinkUpdate(HyperlinkEvent e) { // occur html2.setPage(e.getURL()); html2.requestFocusInWindow(); - } catch (Throwable ex) {} + } catch (Throwable ex) { + } } }; html1.setEditable(false); @@ -1970,11 +2041,13 @@ else if (height < 100) y = 30; } } - if (width < 100) - width = 100; - if (height < 100) - height = 100; } + + if (width < 500) + width = 500; + if (height < 500) + height = 500; + frame.setSize(width, height); frame.setLocation(x, y); frame.setVisible(true); @@ -2064,8 +2137,7 @@ private void finishInit(String[] args, int width) { windowmenu = menu(bar, "&Window", doRefreshWindow(false)); windowmenu2 = menu(null, "&Window", doRefreshWindow(true)); helpmenu = menu(bar, "&Help", null); - if (!Util.onMac()) - menuItem(helpmenu, "About Alloy...", 'A', doAbout()); + menuItem(helpmenu, "About Alloy...", 'A', doAbout()); menuItem(helpmenu, "Quick Guide", 'Q', doHelp()); menuItem(helpmenu, "See the Copyright Notices...", 'L', doLicense()); } finally { @@ -2128,7 +2200,7 @@ private void finishInit(String[] args, int width) { all.add(status, BorderLayout.SOUTH); // Generate some informative log messages - log.logBold("Alloy Analyzer " + Version.version() + " (build date: " + Version.buildDate() + " git " + Version.commit + ")\n\n"); + log.logBold("Alloy Analyzer " + Version.getShortversion() + " built " + Version.buildDate() + "\n\n"); // If on Mac, then register an application listener try { @@ -2155,7 +2227,8 @@ private void finishInit(String[] args, int width) { java.lang.reflect.Field old = ClassLoader.class.getDeclaredField("usr_paths"); old.setAccessible(true); old.set(null, newarray); - } catch (Throwable ex) {} + } catch (Throwable ex) { + } // Pre-load the preferences dialog prefDialog = new PreferencesDialog(log, binary); diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Version.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Version.java index ae27151c9..9d99120b0 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Version.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Version.java @@ -33,21 +33,30 @@ public final class Version { /** * The constructor is private, since this class never needs to be instantiated. */ - private Version() {} + private Version() { + } public static String version = "unknown"; public static long buildnumber = -1; public static Instant builddate = Instant.ofEpochMilli(0); public static String commit = "unknown"; public static boolean experimental = true; + private static String shortversion = ""; static { Manifest manifest = getManifest(); if (manifest != null) { String version = manifest.getMainAttributes().getValue("Bundle-Version"); - if (version != null) + if (version != null) { Version.version = version; + int lastIndexOf = version.lastIndexOf('.'); + if (lastIndexOf > 0) { + Version.shortversion = version.substring(0, lastIndexOf); + } else { + Version.shortversion = version; + } + } String commit = manifest.getMainAttributes().getValue("Git-SHA"); if (commit != null) @@ -100,4 +109,8 @@ public static String buildDate() { return builddate.toString(); } + public static String getShortversion() { + return shortversion; + } + } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/WorkerEngine.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/WorkerEngine.java index 0f9a3179d..0483f039b 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/WorkerEngine.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/WorkerEngine.java @@ -170,7 +170,8 @@ public void close() throws IOException { /** * Constructor is private since this class does not need to be instantiated. */ - private WorkerEngine() {} + private WorkerEngine() { + } /** * This terminates the subprocess, and prevent any further results from reaching @@ -241,8 +242,25 @@ public static void runLocally(final WorkerTask task, final WorkerCallback callba * to it */ public static void run(final WorkerTask task, int newmem, int newstack, String jniPath, String classPath, final WorkerCallback callback) throws IOException { - if (classPath == null || classPath.length() == 0) + String java = "java"; + String javahome = System.getProperty("java.home"); + if (javahome == null) + throw new IllegalArgumentException("java.home not set"); + + File jhome = new File(javahome); + + if (classPath == null || classPath.isEmpty()) classPath = System.getProperty("java.class.path"); + + if (classPath == null || classPath.isEmpty()) { + File dist = findInAncestors(jhome, "org.alloytools.alloy.dist.jar"); + if (dist == null) { + throw new IllegalArgumentException("cannot establish classpath. Neither set for this java nor \"org.alloytools.alloy.dist.jar\" in an ancestor directory of $JAVA_HOME (" + jhome + ")"); + } + System.out.println("Found jar in ancestors java_home " + dist); + classPath = dist.getAbsolutePath(); + } + synchronized (WorkerEngine.class) { final Process sub; if (latest_manager != null && latest_manager.isAlive()) @@ -252,21 +270,19 @@ public static void run(final WorkerTask task, int newmem, int newstack, String j latest_sub.exitValue(); latest_manager = null; latest_sub = null; - } catch (IllegalThreadStateException ex) {} + } catch (IllegalThreadStateException ex) { + } if (latest_sub == null) { - String java = "java", javahome = System.getProperty("java.home"); - if (javahome != null && javahome.length() > 0) { - // First try "[JAVAHOME]/bin/java" - File f = new File(javahome + File.separatorChar + "bin" + File.separatorChar + "java"); - // Then try "[JAVAHOME]/java" - if (!f.isFile()) - f = new File(javahome + File.separatorChar + "java"); - // All else, try "java" (and let the Operating System search - // the program path...) - if (f.isFile()) - java = f.getAbsolutePath(); - } + File f = new File(javahome + File.separatorChar + "bin" + File.separatorChar + "java"); + + if (!f.isFile()) + f = new File(javahome + File.separatorChar + "java"); + + if (f.isFile()) + java = f.getAbsolutePath(); + String debug = AlloyCore.isDebug() ? "yes" : "no"; + if (jniPath != null && jniPath.length() > 0) sub = Runtime.getRuntime().exec(new String[] { java, "-Xmx" + newmem + "m", "-Xss" + newstack + "k", "-Djava.library.path=" + jniPath, "-Ddebug=" + debug, "-cp", classPath, WorkerEngine.class.getName(), Version.buildDate(), "" + Version.buildNumber() @@ -375,13 +391,16 @@ public void uncaughtException(Thread t, Throwable e) { // prevent freezes try { System.loadLibrary("minisat"); - } catch (Throwable ex) {} + } catch (Throwable ex) { + } try { System.loadLibrary("minisatprover"); - } catch (Throwable ex) {} + } catch (Throwable ex) { + } try { System.loadLibrary("zchaff"); - } catch (Throwable ex) {} + } catch (Throwable ex) { + } // Now we repeat the following read-then-execute loop Thread t = null; while (true) { @@ -439,10 +458,12 @@ public void callback(Object x) { } @Override - public void done() {} + public void done() { + } @Override - public void fail() {} + public void fail() { + } }; task.run(y); x.writeObject(null); @@ -456,7 +477,8 @@ public void fail() {} System.gc(); x.writeObject(t); x.flush(); - } catch (Throwable ex2) {} finally { + } catch (Throwable ex2) { + } finally { halt("Error: " + e, 2); } } @@ -475,7 +497,8 @@ public void fail() {} System.gc(); x.writeObject(e); x.flush(); - } catch (Throwable t) {} finally { + } catch (Throwable t) { + } finally { halt("Error: " + e, 1); } } @@ -490,4 +513,18 @@ public void fail() {} private static void halt(String reason, int exitCode) { Runtime.getRuntime().halt(exitCode); } + + private static File findInAncestors(File rover, String fileName) { + while (true) { + if (rover == null) + return null; + + File f = new File(rover, fileName); + if (f.isFile()) + return f; + + rover = rover.getParentFile(); + } + } + } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java index 512657a30..5bb5ff747 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java @@ -421,7 +421,8 @@ public final Object visit(ExprCall x) { while (!todo.isEmpty()) { q.visitThis(todo.remove(todo.size() - 1).getBody()); } - } catch (Err ex) {} // Exception should not occur + } catch (Err ex) { + } // Exception should not occur return seen; } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprVar.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprVar.java index 229cd3208..964c2a63a 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprVar.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprVar.java @@ -15,6 +15,8 @@ package edu.mit.csail.sdg.ast; +import static edu.mit.csail.sdg.alloy4.TableView.clean; + import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -22,7 +24,6 @@ import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.alloy4.ErrorWarning; import edu.mit.csail.sdg.alloy4.Pos; -import edu.mit.csail.sdg.alloy4.TableView; /** * Immutable; represents a LET or QUANTIFICATION variable in the AST. @@ -101,6 +102,6 @@ public String getHTML() { @Override public String explain() { - return "var " + label + "\n" + TableView.toTable(type); + return clean(type.explain()) + " : " + label; } } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java index aeb234cf9..6518c9d30 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java @@ -21,14 +21,11 @@ import java.util.List; import java.util.NoSuchElementException; -import org.alloytools.util.table.Table; - import edu.mit.csail.sdg.alloy4.ConstList; import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.alloy4.ErrorSyntax; import edu.mit.csail.sdg.alloy4.ErrorType; import edu.mit.csail.sdg.alloy4.Pos; -import edu.mit.csail.sdg.alloy4.TableView; import edu.mit.csail.sdg.alloy4.Util; /** @@ -289,35 +286,41 @@ public String getHTML() { @Override public String explain() { + if (clean(label).contains("run$")) { + return null; + } + + StringBuilder sb = new StringBuilder(); if (isPred) sb.append("pred "); else sb.append("fun "); - sb.append(clean(label)).append(":\n"); + sb.append(clean(label)).append("["); if (decls.size() > 0 || !isPred) { - sb.append("\n"); - int n = 0; int count = (int) decls.stream().flatMap(decl -> decl.names.stream()).count(); - Table t = new Table(2, count + (isPred ? 0 : 1), 1); + String del = ""; for (Decl decl : decls) { + + String delName = ""; for (Expr e : decl.names) { - t.set(0, n, e); - t.set(1, n, TableView.toTable(decl.expr.type)); - n++; + sb.append(delName).append(e); + delName = ", "; } + sb.append(" : " + decl.expr.type.explain()); } - if (!isPred) { - t.set(0, n, "⟶"); - t.set(1, n, TableView.toTable(returnDecl.type)); - n++; - } - sb.append(t); + del = ", "; } + sb.append("]"); + if (!isPred) { + sb.append(" : "); + sb.append(returnDecl.type.explain()); + } + return sb.toString(); } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java index de776e653..b57b1d9d0 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java @@ -21,8 +21,6 @@ import java.util.Collection; import java.util.List; -import org.alloytools.util.table.Table; - import edu.mit.csail.sdg.alloy4.ConstList; import edu.mit.csail.sdg.alloy4.ConstList.TempList; import edu.mit.csail.sdg.alloy4.Err; @@ -32,7 +30,6 @@ import edu.mit.csail.sdg.alloy4.ErrorWarning; import edu.mit.csail.sdg.alloy4.Pos; import edu.mit.csail.sdg.alloy4.SafeList; -import edu.mit.csail.sdg.alloy4.TableView; import edu.mit.csail.sdg.alloy4.Util; import edu.mit.csail.sdg.alloy4.Version; import edu.mit.csail.sdg.ast.Attr.AttrType; @@ -757,7 +754,6 @@ public String getHTML() { public String explain() { StringBuilder sb = new StringBuilder(); - sb.append("relation "); if (isPrivate != null) { sb.append("private "); @@ -766,9 +762,7 @@ public String explain() { sb.append("meta "); } sb.append(clean(label)); - sb.append(":\n"); - Table table = TableView.toTable(type); - sb.append(table).append("\n"); + sb.append(" : ").append(clean(type.explain())); return sb.toString(); } @@ -912,8 +906,6 @@ public final Field addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, String la @Override public String explain() { - Table t = new Table(2, 1 + realFields.size(), 1); - StringBuilder sb = new StringBuilder(); if (builtin) sb.append("builtin "); @@ -933,20 +925,16 @@ public String explain() { sb.append("sig "); if (isSubset != null) sb.append("subset "); - t.set(0, 0, sb); - t.set(1, 0, clean(label)); - int n = 1; - for (Field f : realFields) { - t.set(0, n++, clean(f.label)); - } - n = 1; + sb.append(clean(label)).append(" { "); + String del = ""; for (Field f : realFields) { - String relation = clean(type.join(f.type).toString()); - Table table = TableView.toTable(relation, false); - t.set(1, n++, table); + String relation = clean(type.join(f.type).explain()); + sb.append(del).append(f.label).append(" : ").append(relation); + del = ", "; } + sb.append(" }"); - return t.toString(); + return sb.toString(); } } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java index 1d48cce76..85c23ae84 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java @@ -1866,7 +1866,7 @@ void addCommand(boolean followUp, Pos pos, Expr e, boolean check, int overall, i public void addDefaultCommand() { if (commands.isEmpty()) { addFunc(Pos.UNKNOWN, Pos.UNKNOWN, "$$Default", null, new ArrayList
" + +"Git Commit: " + Version.commit + +"