diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d2fc696..3acfd69 100644 --- a/CONTRIBUTING.md +++ b/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. diff --git a/README.md b/README.md index fb4710a..e2801b5 100644 --- a/README.md +++ b/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 + $ 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 diff --git a/build.xml b/build.xml index ec43340..dcf1e34 100644 --- a/build.xml +++ b/build.xml @@ -15,7 +15,7 @@ - + diff --git a/lib/org.alloytools.alloy.dist-5.1.0.jar b/lib/org.alloytools.alloy.dist-5.1.0.jar deleted file mode 100644 index 5720727..0000000 Binary files a/lib/org.alloytools.alloy.dist-5.1.0.jar and /dev/null differ diff --git a/lib/org.alloytools.alloy.dist.jar b/lib/org.alloytools.alloy.dist.jar new file mode 100644 index 0000000..8f5dccf Binary files /dev/null and b/lib/org.alloytools.alloy.dist.jar differ diff --git a/models/even_odd.als b/models/even_odd.als index 90f4dc4..45ebf22 100644 --- a/models/even_odd.als +++ b/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] } diff --git a/models/musical_chairs.als b/models/musical_chairs.als index 70a486b..d6e1bac 100644 --- a/models/musical_chairs.als +++ b/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] } diff --git a/models/river_crossing.als b/models/river_crossing.als index 8271f15..0e3860c 100644 --- a/models/river_crossing.als +++ b/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] } diff --git a/models/switch.als b/models/switch.als index a47d59d..d506177 100644 --- a/models/switch.als +++ b/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 } diff --git a/src/alloy/AlloyUtils.java b/src/alloy/AlloyUtils.java index ab25eb2..2176b0e 100644 --- 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 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, diff --git a/test/alloy/TestAlloyInterface.java b/test/alloy/TestAlloyInterface.java index 85a4bdb..f4965ff 100644 --- 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 {}", "", @@ -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] } }", "" ); diff --git a/test/alloy/TestAlloyUtils.java b/test/alloy/TestAlloyUtils.java index c49384b..45888c3 100644 --- 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, 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" ); diff --git a/test/simulation/TestSimulationManager.java b/test/simulation/TestSimulationManager.java index d7ff813..a625ae3 100644 --- a/test/simulation/TestSimulationManager.java +++ b/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); diff --git a/traces/fgs_counterexample.xml b/traces/fgs_counterexample.xml index c67b5f2..ce8ffe2 100644 --- a/traces/fgs_counterexample.xml +++ b/traces/fgs_counterexample.xml @@ -1,6 +1,6 @@ - +