Temporal Specification and Analysis (Electrum) (AlloyTools#136)

.gitignore

@@ -37,3 +37,5 @@ org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4compiler/
 *.out
 *.app
 
+.idea
+*.iml

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "org.alloytools.pardinus"]
+	path = org.alloytools.pardinus
+	url = https://github.com/haslab/Pardinus

.travis.yml

@@ -1,20 +1,12 @@
-dist: trusty
-sudo: false
+dist: focal
 language: java
-jdk:
-- oraclejdk8
-install: "./gradlew --version"
-script: ./gradlew --no-daemon -DGRADLE_OPTS="-Xms128m" --stacktrace build -i
-after_success:
-- git status
-- echo $REPOSITORY_USERNAME
-- echo $TRAVIS_PULL_REQUEST
-- echo $TRAVIS_BRANCH
-- if [ master == $TRAVIS_BRANCH -a $TRAVIS_PULL_REQUEST == false -a  ${REPOSITORY_USERNAME:=X}
-  != X ]; then ./gradlew -DGRADLE_OPTS="-Xms128m" release -i; fi
+before_install:
+  - curl -L "http://nusmv.fbk.eu/distrib/NuSMV-2.6.0-zchaff-linux64.tar.gz" | tar --extract --gzip --strip-components=2 -C $HOME/bin "NuSMV-2.6.0-Linux/bin/NuSMV" || true
+  - curl -N -L "http://es-static.fbk.eu/tools/nuxmv/downloads/nuXmv-2.0.0-linux64.tar.gz" | tar --extract --gzip --strip-components=2 -C $HOME/bin "nuXmv-2.0.0-Linux/bin/nuXmv" || true
+install: 
+  - "gradle --version"
+script: travis_wait gradle --no-daemon -DGRADLE_OPTS="-Xms128m" --stacktrace build -i
 cache:
   directories:
   - "$HOME/.gradle"
-env:
-  secure: "iMLby/ptj+UObydTJmFj2VO3QoYOiLmNC6kl7HOeSek7Jeo1LNV/+PXZ01o72t2QszFVux2gDcUBlaZKFXsvN585rT0JGRf7R9EA5qiRzetPmWJaA4vdY+GSZR4O0DiOuBcp+KGS5rBHmi3NoKlLAeO/CrHLFyAv2qjofsECUwmsRsS47aCepC7qllla+8PiQbyse6wytJKIqvk4n7BDXXOfQLM6Y5LZ/5uFs6PKyiLlXBmlG5LzdMtxlEED1nOEmLKak7ZjP2VwpJ3KSFGyu7/l9lf+IFnnXAIZaGvARbTDUhF3cyoZgP2Ab5yWJEB1uYzkoNwczmW5ARfalKkjBAV8DuZJFSe39K7XcWVvWRMGTpUSUKA20BpD+wW3q1x8s8Vw+CLuRzCO6QD3uG+JZX2URIBt4F50SpS07HHAd0c6hzv9M4cjd5l9wBYH2nFX1uUuza6znuk3DJ69bM9INMQ+8A5fkSUaXEw/7ym3a+GQINrFtYftcDm915wAznS5Sa86tK2icDtV4vCdTikXLtu6xmYJ4raliGN0E3yL9agW0J1dMjzK+D6l6zXo/qVT+qjwN8+KSFaaYpGYGotqYT4ZnzR9gE85LZWAYLKgsyOOvMopl9MxRVDSKPomUW48aLpG4G80r2NDG3paxA8xS7esDJTBPNCYKuh7Gn3Cp8s="
-
+  - "$HOME/bin"

README.md

@@ -2,11 +2,11 @@
 [![Build Status](https://travis-ci.org/AlloyTools/org.alloytools.alloy.svg?branch=master)](https://travis-ci.org/AlloyTools/org.alloytools.alloy)
 # Alloy
 
-Alloy 4 is a self-contained executable, which includes the Kodkod
-model finder and a variety of SAT solvers, as well as the standard
-Alloy library and a collection of tutorial examples. The same jar file
-can be incorporated into other applications to use Alloy as an API,
-and includes the source code. See the release notes for details of new
+Alloy 6 is a self-contained executable, which includes an extended version of 
+the Kodkod model finder and a variety of SAT solvers, as well as the standard
+Alloy library and a collection of tutorial examples. The same jar file can be
+incorporated into other applications to use Alloy as an API, and includes the
+source code. See the release notes for details of new
 features. 
 
 More documentation can be found at: http://alloytools.org/documentation.html.
@@ -28,12 +28,12 @@ Checkout the project and type `./gradlew build`. You find the executable JAR in
      java version "1.8.0_144"
      Java(TM) SE Runtime Environment (build 1.8.0_144-b01)
      Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed model
-     $ git clone https://github.com/AlloyTools/org.alloytools.alloy.git
+     $ git clone --recursive https://github.com/AlloyTools/org.alloytools.alloy.git
      $ cd org.alloytools.alloy
      $ ./gradlew build
      $ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar
      # opens GUI
-
+     
 Note: if you are behind a proxy, the call to `gradlew` is likely to fail, unless you pass it further options about the http and https proxies (and possibly your login and password on this proxy). There are several ways to pass these options, a simple one is to type (replace the `XXXXX`'s by the adequate settings):
 
      $ ./gradlew -Dhttps.proxyHost=XXXXX -Dhttp.proxyHost=XXXXX -Dhttp.proxyPort=XXXXX \
@@ -53,8 +53,8 @@ The workspace is divided into a number of projects:
 * [org.alloytools.alloy.application](org.alloytools.alloy.application) – Main application code includes the parser, ast, visualiser, and application code
 * [org.alloytools.alloy.dist](org.alloytools.alloy.dist) – Project to create the distribution executable JAR
 * [org.alloytools.alloy.extra](org.alloytools.alloy.extra) – Models and examples
-* [org.alloytools.kodkod.core](org.alloytools.kodkod.core) – Kodkod without native code
-* [org.alloytools.kodkod.nativesat](org.alloytools.kodkod.nativesat) – The native code libraries for kodkod
+* [org.alloytools.pardinus](org.alloytools.pardinus) – A Kodkod extension without native code
+* [org.alloytools.kodkod.nativesat](org.alloytools.kodkod.nativesat) – The native code libraries for Kodkod
 
 ### Relevant Project files
 
@@ -97,7 +97,9 @@ In the root of this workspace type `./gradlew`. This is a script that will downl
 
 ### Continuous Integration
 
-The workspace is setup to build after every commit using Travis. It releases snapshots to `https://oss.sonatype.org/content/repositories/snapshots/org/alloytools/` for every CI build on Travis.
+The workspace is setup to build after every commit using Travis. 
+
+It releases snapshots to `https://oss.sonatype.org/content/repositories/snapshots/org/alloytools/` for every CI build on Travis.
 
 ### Building the DMG file for OSX systems
 

cnf/.classpath

@@ -3,4 +3,4 @@
 	<classpathentry kind="src" path="src"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
 	<classpathentry kind="output" path="bin"/>
-</classpath>
+</classpath>

cnf/build.bnd

@@ -9,8 +9,8 @@ testbin:      			target/test-classes
 target-dir:   			target
 
 javac.source:           1.8
-javac.target:           ${javac.source}
-javac.compliance:       ${javac.source}
+javac.target:           1.8
+javac.compliance:       1.8
 javac.debug:            on
 
 Git-Descriptor:         	${system-allow-fail;git describe --dirty --always}
@@ -21,7 +21,7 @@ Bundle-Vendor:			AlloyTools at Github
 Bundle-DocURL: 			http://alloytools.org
 Bundle-License:			MIT
 
-base.version:           5.1.0
+base.version:           6.0.0
 Bundle-Version:         ${base.version}.${tstamp}
 
 # Remove -SNAPSHOT for release version

cnf/central.xml

@@ -8,6 +8,10 @@
 
 	<packaging>pom</packaging>
 
+	<properties>
+		<logback-version>1.1.7</logback-version>
+	</properties>
+
 	<dependencies>
 		<dependency>
 			<groupId>org.eclipse.jdt</groupId>
@@ -24,6 +28,18 @@
 			<artifactId>org.sat4j.core</artifactId>
 			<version>2.3.1</version>
 		</dependency>
+		<dependency>
+			<groupId>org.sat4j</groupId>
+			<artifactId>org.sat4j.maxsat</artifactId>
+			<version>2.3.1</version>
+			<scope>compile</scope>
+		</dependency>
+		<dependency>
+			<groupId>org.sat4j</groupId>
+			<artifactId>org.sat4j.pb</artifactId>
+			<version>2.3.1</version>
+			<scope>compile</scope>
+		</dependency>		
 		<dependency>
 			<groupId>de.jflex</groupId>
 			<artifactId>jflex</artifactId>
@@ -34,6 +50,16 @@
 			<artifactId>java-cup</artifactId>
 			<version>11b-20160615</version>
 		</dependency>
+		<dependency>
+			<groupId>org.slf4j</groupId>
+			<artifactId>slf4j-api</artifactId>
+			<version>1.7.28</version>
+		</dependency>
+		<dependency>
+			<groupId>org.slf4j</groupId>
+			<artifactId>slf4j-simple</artifactId>
+			<version>1.7.5</version>
+		</dependency>
 	</dependencies>
 
 </project>

org.alloytools.alloy.application/.classpath

@@ -1,9 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <classpath>
-	<classpathentry excluding="test/java/" kind="src" output="target/classes" path="src/main/java"/>
-	<classpathentry kind="src" output="target/test-classes" path="src/test/java"/>
-	<classpathentry kind="src" path="src/main/resources"/>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
 	<classpathentry kind="con" path="aQute.bnd.classpath.container"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
+	<classpathentry kind="src" output="target/classes" path="src/main/java"/>
+	<classpathentry kind="src" output="target/test-classes" path="src/test/java">
+		<attributes>
+			<attribute name="test" value="true"/>
+		</attributes>
+	</classpathentry>
 	<classpathentry kind="output" path="target/classes"/>
 </classpath>

org.alloytools.alloy.application/.settings/org.eclipse.jdt.core.prefs

@@ -133,12 +133,16 @@ org.eclipse.jdt.core.compiler.problem.unusedTypeParameter=ignore
 org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore
 org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
 org.eclipse.jdt.core.compiler.processAnnotations=disabled
+org.eclipse.jdt.core.compiler.release=disabled
 org.eclipse.jdt.core.compiler.source=1.8
 org.eclipse.jdt.core.compiler.taskCaseSensitive=enabled
 org.eclipse.jdt.core.compiler.taskPriorities=NORMAL,NORMAL
 org.eclipse.jdt.core.compiler.taskTags=TODO,FIXME
+org.eclipse.jdt.core.formatter.align_assignment_statements_on_columns=false
 org.eclipse.jdt.core.formatter.align_fields_grouping_blank_lines=4
 org.eclipse.jdt.core.formatter.align_type_members_on_columns=true
+org.eclipse.jdt.core.formatter.align_variable_declarations_on_columns=false
+org.eclipse.jdt.core.formatter.align_with_spaces=false
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=2
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=51
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=50
@@ -148,6 +152,7 @@ org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_e
 org.eclipse.jdt.core.formatter.alignment_for_assignment=2
 org.eclipse.jdt.core.formatter.alignment_for_binary_expression=2
 org.eclipse.jdt.core.formatter.alignment_for_compact_if=2
+org.eclipse.jdt.core.formatter.alignment_for_compact_loops=16
 org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=2
 org.eclipse.jdt.core.formatter.alignment_for_enum_constants=51
 org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=2
@@ -191,6 +196,8 @@ org.eclipse.jdt.core.formatter.brace_position_for_lambda_body=end_of_line
 org.eclipse.jdt.core.formatter.brace_position_for_method_declaration=end_of_line
 org.eclipse.jdt.core.formatter.brace_position_for_switch=end_of_line
 org.eclipse.jdt.core.formatter.brace_position_for_type_declaration=end_of_line
+org.eclipse.jdt.core.formatter.comment.align_tags_descriptions_grouped=false
+org.eclipse.jdt.core.formatter.comment.align_tags_names_descriptions=false
 org.eclipse.jdt.core.formatter.comment.clear_blank_lines_in_block_comment=true
 org.eclipse.jdt.core.formatter.comment.clear_blank_lines_in_javadoc_comment=false
 org.eclipse.jdt.core.formatter.comment.count_line_length_from_starting_position=true
@@ -242,13 +249,13 @@ org.eclipse.jdt.core.formatter.insert_new_line_before_closing_brace_in_array_ini
 org.eclipse.jdt.core.formatter.insert_new_line_before_else_in_if_statement=do not insert
 org.eclipse.jdt.core.formatter.insert_new_line_before_finally_in_try_statement=do not insert
 org.eclipse.jdt.core.formatter.insert_new_line_before_while_in_do_statement=insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_annotation_declaration=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_anonymous_type_declaration=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_block=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=do not insert
-org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=do not insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_annotation_declaration=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_anonymous_type_declaration=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_block=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert
+org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert
 org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert
 org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert
 org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert
@@ -415,6 +422,9 @@ org.eclipse.jdt.core.formatter.join_wrapped_lines=false
 org.eclipse.jdt.core.formatter.keep_else_statement_on_same_line=false
 org.eclipse.jdt.core.formatter.keep_empty_array_initializer_on_one_line=false
 org.eclipse.jdt.core.formatter.keep_imple_if_on_one_line=false
+org.eclipse.jdt.core.formatter.keep_simple_do_while_body_on_same_line=false
+org.eclipse.jdt.core.formatter.keep_simple_for_body_on_same_line=false
+org.eclipse.jdt.core.formatter.keep_simple_while_body_on_same_line=false
 org.eclipse.jdt.core.formatter.keep_then_statement_on_same_line=false
 org.eclipse.jdt.core.formatter.lineSplit=140
 org.eclipse.jdt.core.formatter.never_indent_block_comments_on_first_column=false

org.alloytools.alloy.application/.settings/org.eclipse.jdt.ui.prefs

@@ -31,7 +31,9 @@ cleanup.qualify_static_member_accesses_through_subtypes_with_declaring_class=tru
 cleanup.qualify_static_member_accesses_with_declaring_class=true
 cleanup.qualify_static_method_accesses_with_declaring_class=false
 cleanup.remove_private_constructors=true
-cleanup.remove_redundant_type_arguments=true
+cleanup.remove_redundant_modifiers=false
+cleanup.remove_redundant_semicolons=false
+cleanup.remove_redundant_type_arguments=false
 cleanup.remove_trailing_whitespaces=false
 cleanup.remove_trailing_whitespaces_all=true
 cleanup.remove_trailing_whitespaces_ignore_empty=false
@@ -60,7 +62,7 @@ cleanup_settings_version=2
 eclipse.preferences.version=1
 editor_save_participant_org.eclipse.jdt.ui.postsavelistener.cleanup=true
 formatter_profile=_Alloy
-formatter_settings_version=13
+formatter_settings_version=14
 org.eclipse.jdt.ui.exception.name=e
 org.eclipse.jdt.ui.gettersetter.use.is=true
 org.eclipse.jdt.ui.ignorelowercasenames=true
@@ -88,7 +90,7 @@ sp_cleanup.convert_functional_interfaces=false
 sp_cleanup.convert_to_enhanced_for_loop=false
 sp_cleanup.correct_indentation=false
 sp_cleanup.format_source_code=true
-sp_cleanup.format_source_code_changes_only=false
+sp_cleanup.format_source_code_changes_only=true
 sp_cleanup.insert_inferred_type_arguments=false
 sp_cleanup.make_local_variable_final=false
 sp_cleanup.make_parameters_final=false
@@ -105,6 +107,8 @@ sp_cleanup.qualify_static_member_accesses_through_subtypes_with_declaring_class=
 sp_cleanup.qualify_static_member_accesses_with_declaring_class=false
 sp_cleanup.qualify_static_method_accesses_with_declaring_class=false
 sp_cleanup.remove_private_constructors=true
+sp_cleanup.remove_redundant_modifiers=false
+sp_cleanup.remove_redundant_semicolons=false
 sp_cleanup.remove_redundant_type_arguments=false
 sp_cleanup.remove_trailing_whitespaces=true
 sp_cleanup.remove_trailing_whitespaces_all=true

org.alloytools.alloy.application/bnd.bnd

@@ -3,8 +3,8 @@
 
 -buildpath: \
 	lib/apple-osx-ui.jar;version=file,\
+	org.alloytools.pardinus;version=latest,\
 	org.alloytools.alloy.core;version=latest,\
-	org.alloytools.kodkod.core;version=latest
 
 -testpath: \
 	osgi.enroute.junit.wrapper, \
@@ -15,9 +15,8 @@
     org.alloytools.kodkod.nativesat.x86-linux, \
     org.alloytools.kodkod.nativesat.x86-mac, \
     org.alloytools.kodkod.nativesat.x86-windows
-	
+
 Private-Package: \
 	edu.mit.csail.sdg.alloy4graph,\
 	edu.mit.csail.sdg.alloy4viz,\
 	edu.mit.csail.sdg.alloy4whole,\
-

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/Graph.java

@@ -37,6 +37,9 @@
  * Mutable; represents a graph.
  * <p>
  * <b>Thread Safety:</b> Can be called only by the AWT event thread.
+ *
+ * @modified [electrum] changed so that nodes are sorted lexicographically
+ *           within each layer of the graph
  */
 
 public final strictfp class Graph {
@@ -313,7 +316,18 @@ private void layout_assignOrder() {
                 grOUT.get(n.pos()).remove(x);
             for (GraphNode n : grOUT.get(x.pos()))
                 grIN.get(n.pos()).remove(x);
-            for (GraphNode n : Util.fastJoin(grIN.get(x.pos()), grOUT.get(x.pos()))) {
+            // [electrum] hack to get nodes sorted lexicographically within each layer
+            // can't fast join since read-only
+            //          Iterable<GraphNode> aux = Util.fastJoin(grIN.get(x.pos()), );
+            List<GraphNode> aux = new ArrayList<GraphNode>(grIN.get(x.pos()));
+            aux.addAll(grOUT.get(x.pos()));
+            aux.sort(new Comparator<GraphNode>() {
+
+                public int compare(GraphNode o1, GraphNode o2) {
+                    return -o1.uuid.toString().compareTo(o2.uuid.toString());
+                }
+            });
+            for (GraphNode n : aux) {
                 int ni = n.pos(), out = grOUT.get(ni).size(), in = grIN.get(ni).size();
                 int b = (out == 0) ? 0 : (in == 0 ? (2 * num) : (out - in + num));
                 if (grBIN[ni] != b) {

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/GraphViewer.java

@@ -61,6 +61,9 @@
  * This class displays the graph.
  * <p>
  * <b>Thread Safety:</b> Can be called only by the AWT event thread.
+ *
+ * @modified [electrum] added the ability to update the scale (needed to be
+ *           preserved when navigating traces)
  */
 
 public final strictfp class GraphViewer extends JPanel {
@@ -695,6 +698,16 @@ public Dimension getPreferredSize() {
         return new Dimension((int) (graph.getTotalWidth() * scale), (int) (graph.getTotalHeight() * scale));
     }
 
+    /** Returns the zoom level of this graph. */
+    public double getScale() {
+        return scale;
+    }
+
+    /** Updates the zoom level of this graph. */
+    public void setScale(double scale) {
+        this.scale = scale;
+    }
+
     /**
      * This method is called by Swing to draw this component.
      */