changed importing ordering module for aldb actions to be 'as aldb_ord…

…er', which caused renamings of first/last/next; this is to make the code more general in case the user also uses the ordering module
WatForm · May 21, 2024 · 58cc41c · 58cc41c
1 parent f6ef9cc
commit 58cc41c
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 22 deletions.
diff --git a/src/alloy/AlloyUtils.java b/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, sprime: s.next { %s[s, sprime] } }" + "\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,

diff --git a/test/alloy/TestAlloyInterface.java b/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 {}",
             "",
@@ -181,9 +181,9 @@ private File createModelForTesting() throws IOException {
             "    s.switch = Off implies sprime.switch = On",
             "}",
             "",
-            "fact { init[first] }",
+            "fact { init[aldb_order/first] }",
             "",
-            "fact { all s: State, sprime: s.next { next[s, sprime] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             ""
         );
 

diff --git a/test/alloy/TestAlloyUtils.java b/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, sprime: s.next { next[s, sprime] } }",
+            "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, sprime: s.next { trans[s, sprime] } }",
+            "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, sprime: s.next { next[s, sprime] } }",
+            "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, sprime: s.next { next[s, sprime] } }",
+            "fact { all s: State, sprime: s.(aldb_order/next) { next[s, sprime] } }",
             "",
             "run {  } for exactly 6 State"
         );