ALDB updated for Alloy 6 (#66)

* updated jar and build.xml for Alloy 6

* updated README with dist/aldb.jar

* fixed typo in README about conf names

* removed ' from variables in all models

* changed s' to sprime in autogenerated code

* replaces s' with sprime in tests

* modifed .xml trace file example with new attributes from Alloy 6, which are ignored in aldb

* using Alloy jar from our Alloy build

* changed importing ordering module for aldb actions to be 'as aldb_order', which caused renamings of first/last/next; this is to make the code more general in case the user also uses the ordering module

* added alloy 6 jar from our Dash build

CONTRIBUTING.md

@@ -9,6 +9,7 @@ Prior to submitting a PR, please ensure that:
 
 * Java 8 or later
 * [Ant](https://ant.apache.org/) 1.10.7 or later
+* Note: org.alloytools.alloy.dist-6.0.0.jar is included in lib (from https://github.com/AlloyTools/org.alloytools.alloy/releases)
 
 ## Build and Run
 
@@ -18,7 +19,9 @@ Prior to submitting a PR, please ensure that:
 ## Running Tests
 
      $ ant test
-     
+
+Note: a tmp file is created in the model's directory by aldb during execution (and removed when execution is finished).  Examining this file can be helpful in debugging.
+
 ## Pull Request Process
 
 1. Ensure your code builds successfully.

README.md

@@ -27,7 +27,7 @@ This guide explains usage of ALDB, compatibility requirements for Alloy models,
 
 2. Run ALDB from the command line:
     ```sh
-    $ java -jar <path-to-aldb.jar>
+    $ java -jar dist/aldb.jar
     ```
 
 ## Model and Configuration Format
@@ -60,7 +60,7 @@ The Alloy code that conforms to the above configuration – with the configurati
 /*  BEGIN_ALDB_CONF
  *
  *  stateSigName: State
- *  transitionConstraintName: next
+ *  transitionRelationName: next
  *  initPredicateName: init
  *
  *  END_ALDB_CONF

build.xml

@@ -15,7 +15,7 @@
         <pathelement location="${lib}/junit-platform-console-standalone-1.5.2.jar"/>
         <pathelement location="${lib}/mockito-core-3.3.2.jar"/>
         <pathelement location="${lib}/objenesis.jar"/>
-        <pathelement location="${lib}/org.alloytools.alloy.dist-5.1.0.jar"/>
+        <pathelement location="${lib}/org.alloytools.alloy.dist.jar"/>
         <pathelement location="${lib}/snakeyaml-1.25.jar"/>
         <pathelement location="${lib}/system-rules-1.19.0.jar"/>
         <pathelement location="${bin.main}"/>

models/even_odd.als

@@ -16,6 +16,6 @@ pred init[s: State] {
     s.i = 0 || s.i = 1
 }
 
-pred next[s, s': State] {
-    s'.i = plus[s.i, 2]
+pred next[s, sprime: State] {
+    sprime.i = plus[s.i, 2]
 }

models/musical_chairs.als

@@ -50,85 +50,85 @@ pred pre_music_starts [s: State] {
   #s.players > 1
   s.mode = start
 }
-pred post_music_starts [s, s': State] {
-  s'.players = s.players
-  s'.chairs = s.chairs
+pred post_music_starts [s, sprime: State] {
+  sprime.players = s.players
+  sprime.chairs = s.chairs
   // no one is sitting after music starts
-  s'.occupied = none -> none
-  s'.mode= walking
+  sprime.occupied = none -> none
+  sprime.mode= walking
 }
-pred music_starts [s, s': State] {
+pred music_starts [s, sprime: State] {
   pre_music_starts[s]
-  post_music_starts[s,s']
+  post_music_starts[s,sprime]
 }
 
 pred pre_music_stops [s: State] {
   s.mode = walking
 }
-pred post_music_stops [s, s': State] {
-  s'.players = s.players
-  s'.chairs = s.chairs
+pred post_music_stops [s, sprime: State] {
+  sprime.players = s.players
+  sprime.chairs = s.chairs
   // no other chair/player than chairs/players
-  s'.occupied in s'.chairs -> s'.players
+  sprime.occupied in sprime.chairs -> sprime.players
   // forcing occupied to be total and
   //each chair mapped to only one player
-  all c:s'.chairs | one c.(s'.occupied)
+  all c:sprime.chairs | one c.(sprime.occupied)
   // each "occupying" player is sitting on one chair
-  all p:Chair.(s'.occupied) | one s'.occupied.p
-  s'.mode = sitting
+  all p:Chair.(sprime.occupied) | one sprime.occupied.p
+  sprime.mode = sitting
 }
-pred music_stops [s, s': State] {
+pred music_stops [s, sprime: State] {
   pre_music_stops[s]
-  post_music_stops[s,s']
+  post_music_stops[s,sprime]
 }
 
 pred pre_eliminate_loser [s: State] {
   s.mode = sitting
 }
-pred post_eliminate_loser [s, s': State] {
+pred post_eliminate_loser [s, sprime: State] {
   // loser is the player in the game not in the range of occupied
-  s'.players = Chair.(s.occupied)
-  #s'.chairs = (#s.chairs).minus[1]
-  s'.mode = start
+  sprime.players = Chair.(s.occupied)
+  #sprime.chairs = (#s.chairs).minus[1]
+  sprime.mode = start
 }
-pred eliminate_loser [s, s': State] {
+pred eliminate_loser [s, sprime: State] {
   pre_eliminate_loser[s]
-  post_eliminate_loser[s,s']
+  post_eliminate_loser[s,sprime]
 }
 
 pred pre_declare_winner [s: State] {
   #s.players = 1
   s.mode = start
 }
-pred post_declare_winner [s, s': State] {
-  s'.players = s.players
-  s'.chairs = s.chairs
-  s'.mode = end
+pred post_declare_winner [s, sprime: State] {
+  sprime.players = s.players
+  sprime.chairs = s.chairs
+  sprime.mode = end
 }
-pred declare_winner [s, s': State] {
+pred declare_winner [s, sprime: State] {
   pre_declare_winner[s]
-  post_declare_winner[s,s']
+  post_declare_winner[s,sprime]
 }
 
 pred pre_end_loop [s: State] {
   s.mode = end
 }
-pred post_end_loop [s, s': State] {
-  s'.mode = end
-  s'.players = s.players
-  s'.chairs = s.chairs
-  s'.occupied = s.occupied
+pred post_end_loop [s, sprime: State] {
+  sprime.mode = end
+  sprime.players = s.players
+  sprime.chairs = s.chairs
+  sprime.occupied = s.occupied
 }
-pred end_loop [s, s': State] {
+pred end_loop [s, sprime: State] {
   pre_end_loop[s]
-  post_end_loop[s,s']
+  post_end_loop[s,sprime]
 }
 
 // helper to define valid transitions
-pred trans [s,s': State] {
-    music_starts[s,s'] or
-    music_stops[s,s'] or
-    eliminate_loser[s,s'] or
-    declare_winner[s,s'] or
-    end_loop[s,s']
+pred trans [s,sprime: State] {
+    music_starts[s,sprime] or
+    music_stops[s,sprime] or
+    eliminate_loser[s,sprime] or
+    declare_winner[s,sprime] or
+    end_loop[s,sprime]
 }

models/river_crossing.als

@@ -16,16 +16,16 @@ pred init[s:State] {
 }
 
 /* At most one item to move from 'from' to 'to' */
-pred crossRiver [from, from', to, to': set Object] {
+pred crossRiver [from, fromprime, to, toprime: set Object] {
   one x: from | {
-    from' = from - x - Farmer - from'.eats
-    to' = to + x + Farmer
+    fromprime = from - x - Farmer - fromprime.eats
+    toprime = to + x + Farmer
   }
 }
 
-pred next[s, s':  State] {
+pred next[s, sprime:  State] {
   Farmer in s.near =>
-    crossRiver [s.near, s'.near, s.far, s'.far]
+    crossRiver [s.near, sprime.near, s.far, sprime.far]
   else
-    crossRiver [s.far, s'.far, s.near, s'.near]
+    crossRiver [s.far, sprime.far, s.near, sprime.near]
 }

models/switch.als

@@ -12,9 +12,9 @@ pred init[s: State] {
     s.b = Off
 }
 
-pred next[s, s': State] {
-    s.a = On implies s'.a = Off
-    s.a = Off implies s'.a = On
-    s.b = On implies s'.b = Off
-    s.b = Off implies s'.b = On
+pred next[s, sprime: State] {
+    s.a = On implies sprime.a = Off
+    s.a = Off implies sprime.a = On
+    s.b = On implies sprime.b = Off
+    s.b = Off implies sprime.b = On
 }

src/alloy/AlloyUtils.java

@@ -83,11 +83,11 @@ public static String annotatedTransitionSystem(String model, ParsingConf parsing
     }
 
     public static String annotatedTransitionSystemStep(String model, ParsingConf parsingConf, int steps) {
-        return annotatedTransitionSystem(model, parsingConf, steps, "path[first]");
+        return annotatedTransitionSystem(model, parsingConf, steps, "path[aldb_order/first]");
     }
 
     public static String annotatedTransitionSystemUntil(String model, ParsingConf parsingConf, int steps) {
-        return annotatedTransitionSystem(model, parsingConf, steps, "break[last]");
+        return annotatedTransitionSystem(model, parsingConf, steps, "break[aldb_order/last]");
     }
 
     /**
@@ -222,7 +222,7 @@ private static String annotatedTransitionSystem(String model, ParsingConf parsin
         Map<String, Integer> additionalSigScopes = parsingConf.getAdditionalSigScopes();
         String additionalConstraintFact = additionalConstraint.trim().isEmpty() ? "" : String.format("fact { %s }" + "\n\n", additionalConstraint);
         String transitionRelationFact = String.format(
-            "fact { all s: %s, s': s.next { %s[s, s'] } }" + "\n\n", stateSigName, transitionRelationName
+            "fact { all s: %s, sprime: s.(aldb_order/next) { %s[s, sprime] } }" + "\n\n", stateSigName, transitionRelationName
         );
         String sigScopes = String.format("run {  } for exactly %d %s", steps + 1, stateSigName);
         for (String sigScopeName : additionalSigScopes.keySet()) {
@@ -232,9 +232,9 @@ private static String annotatedTransitionSystem(String model, ParsingConf parsin
             sigScopes += String.format(scopeFormat, additionalSigScopes.get(sigScopeName), sigScopeName);
         }
         return String.format(
-            String.format("open util/ordering[%s]" + "\n\n", stateSigName) +
+            String.format("open util/ordering[%s] as aldb_order" + "\n\n", stateSigName) +
             model + "\n\n" +
-            String.format("fact { %s[first] }" + "\n\n", initPredicateName) +
+            String.format("fact { %s[aldb_order/first] }" + "\n\n", initPredicateName) +
             additionalConstraintFact +
             transitionRelationFact +
             sigScopes,

test/alloy/TestAlloyInterface.java

@@ -162,7 +162,7 @@ public void testGetSigFromA4Solution_sigNotFound() throws IOException {
 
     private File createModelForTesting() throws IOException {
         String modelString = String.join("\n",
-            "open util/ordering[State]",
+            "open util/ordering[State] as aldb_order",
             "",
             "abstract sig SwitchState {}",
             "",
@@ -176,14 +176,14 @@ private File createModelForTesting() throws IOException {
             "    s.switch = Off",
             "}",
             "",
-            "pred next[s, s': State] {",
-            "    s.switch = On implies s'.switch = Off",
-            "    s.switch = Off implies s'.switch = On",
+            "pred next[s, sprime: State] {",
+            "    s.switch = On implies sprime.switch = Off",
+            "    s.switch = Off implies sprime.switch = On",
             "}",
             "",
-            "fact { init[first] }",
+            "fact { init[aldb_order/first] }",
             "",
-            "fact { all s: State, s': s.next { next[s, s'] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             ""
         );
 

test/alloy/TestAlloyUtils.java

@@ -39,13 +39,13 @@ public void testAnnotatedTransitionSystem() {
         int steps = 5;
         boolean until = false;
         String expected = String.join("\n",
-            "open util/ordering[State]",
+            "open util/ordering[State] as aldb_order",
             "",
             "Some model",
             "",
-            "fact { init[first] }",
+            "fact { init[aldb_order/first] }",
             "",
-            "fact { all s: State, s': s.next { next[s, s'] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             "",
             "run {  } for exactly 6 State"
         );
@@ -76,13 +76,13 @@ public void testAnnotatedTransitionSystem_customParsingConf() {
         pc.setAdditionalSigScopes(sigScopes);
 
         String expected = String.join("\n",
-            "open util/ordering[Snapshot]",
+            "open util/ordering[Snapshot] as aldb_order",
             "",
             "Some model",
             "",
-            "fact { initialize[first] }",
+            "fact { initialize[aldb_order/first] }",
             "",
-            "fact { all s: Snapshot, s': s.next { trans[s, s'] } }",
+            "fact { all s: Snapshot, sprime: s.(aldb_order/next) { trans[s, sprime] } }",
             "",
             "run {  } for exactly 6 Snapshot, exactly 3 Chair, 6 Int, exactly 4 Player, 6 seq"
         );
@@ -100,15 +100,15 @@ public void testAnnotatedTransitionSystemStep() {
         int steps = 5;
         boolean until = false;
         String expected = String.join("\n",
-            "open util/ordering[State]",
+            "open util/ordering[State] as aldb_order",
             "",
             "Some model",
             "",
-            "fact { init[first] }",
+            "fact { init[aldb_order/first] }",
             "",
-            "fact { path[first] }",
+            "fact { path[aldb_order/first] }",
             "",
-            "fact { all s: State, s': s.next { next[s, s'] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             "",
             "run {  } for exactly 6 State"
         );
@@ -126,15 +126,15 @@ public void testAnnotatedTransitionSystemUntil() {
         int steps = 5;
         boolean until = false;
         String expected = String.join("\n",
-            "open util/ordering[State]",
+            "open util/ordering[State] as aldb_order",
             "",
             "Some model",
             "",
-            "fact { init[first] }",
+            "fact { init[aldb_order/first] }",
             "",
-            "fact { break[last] }",
+            "fact { break[aldb_order/last] }",
             "",
-            "fact { all s: State, s': s.next { next[s, s'] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             "",
             "run {  } for exactly 6 State"
         );

test/simulation/TestSimulationManager.java

@@ -74,7 +74,7 @@ public void testInitializeWithModel_nonexistantFile() {
     public void testInitializeWithModel_noInitPredicate() throws IOException {
         String noInitModel = String.join("\n",
             "sig State {}",
-            "pred next[s, s': State] {}",
+            "pred next[s, sprime: State] {}",
             ""
         );
         initializeTestWithModelString(noInitModel);
@@ -115,7 +115,7 @@ public void testInitializeWithModel_missingScopes() throws IOException {
             "sig Foo {}",
             "sig State { x: set Foo }",
             "pred init[s: State] {}",
-            "pred next[s, s': State] {}",
+            "pred next[s, sprime: State] {}",
             ""
         );
         initializeTestWithModelString(model);
@@ -129,7 +129,7 @@ public void testInitializeWithModel_unsat() throws IOException {
         String unsatModel = String.join("\n",
             "sig State { x: Int }",
             "pred init[s: State] { s.x = none }",
-            "pred next[s, s': State] {}",
+            "pred next[s, sprime: State] {}",
             ""
         );
         initializeTestWithModelString(unsatModel);

traces/fgs_counterexample.xml

@@ -1,6 +1,6 @@
 <alloy builddate="2018-04-08T17:20:06.754Z">
 
-<instance bitwidth="4" maxseq="4" command="Check Default_Lateral_Mode_Is_ROLL for 11 Snapshot, exactly 2 EventLabel" filename="/media/jis/TOSHIBA EXT/JIS/Estudio/UWaterloo/Research/Git/dash/Models/Optimisations/optimised/generated_optimised.als">
+<instance bitwidth="4" maxseq="4" mintrace="-1" maxtrace="-1" command="Check Default_Lateral_Mode_Is_ROLL for 11 Snapshot, exactly 2 EventLabel" filename="/media/jis/TOSHIBA EXT/JIS/Estudio/UWaterloo/Research/Git/dash/Models/Optimisations/optimised/generated_optimised.als" tracelength="1" backloop="0">
 
 <sig label="seq/Int" ID="0" parentID="1" builtin="yes">
 </sig>