From e16e074325d9f16ddbcba8157d6f37ab87a6162e Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Sun, 3 Feb 2019 22:48:04 +0200 Subject: [PATCH 01/11] API cleanup --- README.md | 1 + dependency-reduced-pom.xml | 2 +- pom.xml | 2 +- ...ner.java => PrintDfsVerifierListener.java} | 6 +++--- .../violations/HotBProgramCycleViolation.java | 2 +- .../bgu/cs/bp/bpjs/mains/BPJsCliRunner.java | 6 +++--- .../bp/bpjs/model/BProgramSyncSnapshot.java | 1 - .../cs/bp/bpjs/model/BThreadSyncSnapshot.java | 2 +- .../internal}/ContinuationProgramState.java | 2 +- .../bp/bpjs/TicTacToe/TicTacToeVerMain.java | 4 ++-- .../ContinuationProgramStateTest.java | 1 + .../analysis/DfsBProgramVerifierTest.java | 20 +++++++++---------- .../cs/bp/bpjs/analysis/examples/Mazes.java | 4 ++-- 13 files changed, 27 insertions(+), 26 deletions(-) rename src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/{BriefPrintDfsVerifierListener.java => PrintDfsVerifierListener.java} (92%) rename src/main/java/il/ac/bgu/cs/bp/bpjs/{analysis => model/internal}/ContinuationProgramState.java (99%) diff --git a/README.md b/README.md index a8b368ba..16fc9a3e 100644 --- a/README.md +++ b/README.md @@ -46,6 +46,7 @@ a link to this page somewhere in the documentation/system about section. ### 2019-01-19 * :sparkles: More tests. +* :arrow_up: `BriefPrintDfsVerifierListener` => `PrintDfsVerifierListener`, so that it's consistent with `PrintBProgramRunnerListener`. ### 2019-01-18 * :bug: Fixed a that cause equality tests of JS event sets to return false negatives. diff --git a/dependency-reduced-pom.xml b/dependency-reduced-pom.xml index 5af5d55c..ccdaf4c1 100644 --- a/dependency-reduced-pom.xml +++ b/dependency-reduced-pom.xml @@ -4,7 +4,7 @@ com.github.bthink-bgu BPjs BPjs - 0.9.7-SNAPSHOT + 0.9.7 Provides a runtime for behavioral programs written in Javascript. It can run stand-alone (from the commmandline) or be embedded in larger JVM-based systems. diff --git a/pom.xml b/pom.xml index 22c601e5..ecc3c560 100644 --- a/pom.xml +++ b/pom.xml @@ -5,7 +5,7 @@ com.github.bthink-bgu BPjs - 0.9.7-SNAPSHOT + 0.9.8-SNAPSHOT jar BPjs diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/BriefPrintDfsVerifierListener.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/PrintDfsVerifierListener.java similarity index 92% rename from src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/BriefPrintDfsVerifierListener.java rename to src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/PrintDfsVerifierListener.java index 12a7d53e..b5f45ece 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/BriefPrintDfsVerifierListener.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/listeners/PrintDfsVerifierListener.java @@ -32,15 +32,15 @@ * Logs the state of the verifier with short, not too-detailed messages. * @author michael */ -public class BriefPrintDfsVerifierListener implements DfsBProgramVerifier.ProgressListener { +public class PrintDfsVerifierListener implements DfsBProgramVerifier.ProgressListener { private final PrintStream out; - public BriefPrintDfsVerifierListener(PrintStream out) { + public PrintDfsVerifierListener(PrintStream out) { this.out = out; } - public BriefPrintDfsVerifierListener() { + public PrintDfsVerifierListener() { this(System.out); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java index 10e0200a..02870ec5 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java @@ -44,7 +44,7 @@ public HotBProgramCycleViolation(List counterExampleTrace, int @Override public String decsribe() { - return "Hot cycle violation: returning to index " + getCycleToIndex() + return "Hot b-program cycle violation: returning to index " + getCycleToIndex() + " in the trace because of event " + event.toString(); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java index de4d22c5..bf7151fb 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java @@ -28,7 +28,7 @@ import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; import il.ac.bgu.cs.bp.bpjs.analysis.HashVisitedStateStore; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; -import il.ac.bgu.cs.bp.bpjs.analysis.listeners.BriefPrintDfsVerifierListener; +import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; import il.ac.bgu.cs.bp.bpjs.model.BProgram; import il.ac.bgu.cs.bp.bpjs.execution.BProgramRunner; @@ -113,7 +113,7 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { bpp.setEventSelectionStrategy(sess); DfsBProgramVerifier vfr = new DfsBProgramVerifier(); vfr.setDebugMode( switchPresent("-v", args)); - vfr.setProgressListener( new BriefPrintDfsVerifierListener() ); + vfr.setProgressListener(new PrintDfsVerifierListener() ); if ( switchPresent("--full-state-storage", args) ) { println("Using full state storage"); @@ -139,7 +139,7 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { println("Max trace length: " + vfr.getMaxTraceLength() ); try { - println("Starting vberification"); + println("Starting verification"); VerificationResult res = vfr.verify(bpp); println("Verification completed."); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java index 15544822..18750ac9 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java @@ -361,7 +361,6 @@ public boolean equals(Object obj) { if ( ! getExternalEvents().equals(other.getExternalEvents()) ) { return false; } - // TODO return Objects.equals(threadSnapshots, other.threadSnapshots); } } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java index b4e34e6d..7cefd4a4 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java @@ -1,5 +1,6 @@ package il.ac.bgu.cs.bp.bpjs.model; +import il.ac.bgu.cs.bp.bpjs.model.internal.ContinuationProgramState; import java.io.Serializable; import java.util.Optional; @@ -7,7 +8,6 @@ import org.mozilla.javascript.NativeContinuation; import org.mozilla.javascript.Scriptable; -import il.ac.bgu.cs.bp.bpjs.analysis.ContinuationProgramState; import java.util.Objects; /** diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramState.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java similarity index 99% rename from src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramState.java rename to src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java index d0b80b9f..d0355380 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramState.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java @@ -21,7 +21,7 @@ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN * THE SOFTWARE. */ -package il.ac.bgu.cs.bp.bpjs.analysis; +package il.ac.bgu.cs.bp.bpjs.model.internal; import java.lang.reflect.Field; import java.util.ArrayList; diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java index 0379eb6e..d770d718 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java @@ -7,7 +7,7 @@ import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; -import il.ac.bgu.cs.bp.bpjs.analysis.listeners.BriefPrintDfsVerifierListener; +import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; /** * Verification of the TicTacToe strategy. @@ -47,7 +47,7 @@ public static void main(String[] args) throws InterruptedException { vfr.setMaxTraceLength(70); // vfr.setDebugMode(true); vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); - vfr.setProgressListener( new BriefPrintDfsVerifierListener() ); + vfr.setProgressListener(new PrintDfsVerifierListener() ); final VerificationResult res = vfr.verify(bprog); if (res.isViolationFound()) { diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramStateTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramStateTest.java index d53967e1..084c9953 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramStateTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ContinuationProgramStateTest.java @@ -23,6 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis; +import il.ac.bgu.cs.bp.bpjs.model.internal.ContinuationProgramState; import il.ac.bgu.cs.bp.bpjs.internal.ExecutorServiceMaker; import il.ac.bgu.cs.bp.bpjs.model.BProgram; import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java index b2538c8d..50cec996 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java @@ -37,7 +37,7 @@ import static org.junit.Assert.*; import il.ac.bgu.cs.bp.bpjs.model.StringBProgram; -import il.ac.bgu.cs.bp.bpjs.analysis.listeners.BriefPrintDfsVerifierListener; +import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; import il.ac.bgu.cs.bp.bpjs.analysis.violations.DeadlockViolation; import il.ac.bgu.cs.bp.bpjs.analysis.violations.FailedAssertionViolation; @@ -50,7 +50,7 @@ public class DfsBProgramVerifierTest { public void simpleAAABTrace_forgetfulStore() throws Exception { BProgram program = new ResourceBProgram("DFSVerifierTests/AAABTrace.js"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); sut.setVisitedNodeStore(new ForgetfulVisitedStateStore()); VerificationResult res = sut.verify(program); @@ -64,7 +64,7 @@ public void simpleAAABTrace() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setDebugMode(true); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); sut.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); VerificationResult res = sut.verify(program); @@ -77,7 +77,7 @@ public void simpleAAABTrace_hashedNodeStore() throws Exception { BProgram program = new ResourceBProgram("DFSVerifierTests/AAABTrace.js"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setDebugMode(true); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); program.appendSource(Requirements.eventNotSelected("B")); VisitedStateStore stateStore = new HashVisitedStateStore(); sut.setVisitedNodeStore(stateStore); @@ -146,7 +146,7 @@ public void testTwoSimpleBThreads() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.addInspector(DfsInspections.FailedAssertions); VerificationResult res = sut.verify(bprog); @@ -164,7 +164,7 @@ public void testTwoLoopingBThreads() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.setDebugMode(true); VerificationResult res = sut.verify(bprog); @@ -190,7 +190,7 @@ public void testVariablesInBT() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.setDebugMode(true); VerificationResult res = sut.verify(bprog); @@ -216,7 +216,7 @@ public void testVariablesEquailtyInBT() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.setDebugMode(true); VerificationResult res = sut.verify(bprog); @@ -244,7 +244,7 @@ public void testMaxTraceLength() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.setDebugMode(true); VerificationResult res = sut.verify(bprog); assertTrue(res.isViolationFound()); @@ -281,7 +281,7 @@ public void testJavaVariablesInBT() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); - sut.setProgressListener(new BriefPrintDfsVerifierListener()); + sut.setProgressListener(new PrintDfsVerifierListener()); sut.setDebugMode(true); VerificationResult res = sut.verify(bprog); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java index d8917902..3d180f2e 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java @@ -34,7 +34,7 @@ import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; import il.ac.bgu.cs.bp.bpjs.analysis.Requirements; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; -import il.ac.bgu.cs.bp.bpjs.analysis.listeners.BriefPrintDfsVerifierListener; +import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; import java.util.stream.Collectors; import org.mozilla.javascript.NativeArray; @@ -85,7 +85,7 @@ public void verify() throws InterruptedException { try { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); - vfr.setProgressListener(new BriefPrintDfsVerifierListener()); + vfr.setProgressListener(new PrintDfsVerifierListener()); vfr.setIterationCountGap(10); vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); // vfr.setVisitedNodeStore(new ForgetfulVisitedStateStore()); From 1f5c5489e5314dea88f5ff1f9672cfad58faec9a Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Sun, 3 Feb 2019 23:23:07 +0200 Subject: [PATCH 02/11] VisitedStateStore update --- README.md | 3 + .../BThreadSnapshotVisitedStateStore.java | 17 ++--- .../bp/bpjs/analysis/DfsBProgramVerifier.java | 4 +- .../analysis/ForgetfulVisitedStateStore.java | 6 +- .../bpjs/analysis/HashVisitedStateStore.java | 9 +-- .../bp/bpjs/analysis/VisitedStateStore.java | 6 +- .../cs/bp/bpjs/analysis/StateStoreTests.java | 70 +++++++++---------- 7 files changed, 60 insertions(+), 55 deletions(-) diff --git a/README.md b/README.md index 16fc9a3e..330bf370 100644 --- a/README.md +++ b/README.md @@ -48,6 +48,9 @@ a link to this page somewhere in the documentation/system about section. * :sparkles: More tests. * :arrow_up: `BriefPrintDfsVerifierListener` => `PrintDfsVerifierListener`, so that it's consistent with `PrintBProgramRunnerListener`. +### 2019-02-03 +* :arrow_up: `VisitedStateStore` now stores *states*, not DFS nodes. So it's more reusable that way. + ### 2019-01-18 * :bug: Fixed a that cause equality tests of JS event sets to return false negatives. * :bug: The `bp` object no longer collected by the state comparators. diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/BThreadSnapshotVisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/BThreadSnapshotVisitedStateStore.java index 14fd944e..ead21d06 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/BThreadSnapshotVisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/BThreadSnapshotVisitedStateStore.java @@ -23,6 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; import java.util.Collections; import java.util.HashSet; @@ -45,8 +46,8 @@ private static final class Snapshot { final Set bthreads; private final int hashCode; - Snapshot( Set snapshots ){ - bthreads = Collections.unmodifiableSet(snapshots); + Snapshot( BProgramSyncSnapshot bpss ){ + bthreads = Collections.unmodifiableSet(bpss.getBThreadSnapshots()); hashCode = bthreads.hashCode(); } @@ -68,19 +69,15 @@ public boolean equals(Object obj) { } @Override - public void store(DfsTraversalNode nd) { - visited.add(extractStatus(nd)); + public void store(BProgramSyncSnapshot bss) { + visited.add(new Snapshot(bss)); } @Override - public boolean isVisited(DfsTraversalNode nd) { - return visited.contains( extractStatus(nd) ); + public boolean isVisited(BProgramSyncSnapshot bss) { + return visited.contains(new Snapshot(bss)); } - private Snapshot extractStatus( DfsTraversalNode nd ) { - return new Snapshot(nd.getSystemState().getBThreadSnapshots()); - } - @Override public void clear() { visited.clear(); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java index d679de93..95b878a9 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java @@ -178,7 +178,7 @@ protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorSe final BEvent nextEvent = src.getEventIterator().next(); DfsTraversalNode possibleNextNode = src.getNextNode(nextEvent, execSvc); visitedEdgeCount++; - if (visited.isVisited(possibleNextNode) ) { + if (visited.isVisited(possibleNextNode.getSystemState()) ) { // Found a possible cycle if ( !cycleInspectors.isEmpty() ) { BProgramSyncSnapshot pns = possibleNextNode.getSystemState(); @@ -243,7 +243,7 @@ void printStatus(long iteration, List path) { } private void push(DfsTraversalNode n) { - visited.store(n); + visited.store(n.getSystemState()); currentPath.add(n); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ForgetfulVisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ForgetfulVisitedStateStore.java index 9dc6ed9b..13752122 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ForgetfulVisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ForgetfulVisitedStateStore.java @@ -23,6 +23,8 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; + /** * A VisitedNodeStore that does not remember any visited node. When the program * search graph is a tree, ensures that all the nodes are visited. When the program @@ -36,12 +38,12 @@ public class ForgetfulVisitedStateStore implements VisitedStateStore { private long visitedCount=0; @Override - public void store(DfsTraversalNode nd) { + public void store(BProgramSyncSnapshot bss) { visitedCount++; } @Override - public boolean isVisited(DfsTraversalNode nd) { + public boolean isVisited(BProgramSyncSnapshot bss) { return false; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java index f5251362..5bf35dcb 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java @@ -23,6 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; import java.util.Set; import java.util.TreeSet; @@ -35,13 +36,13 @@ public class HashVisitedStateStore implements VisitedStateStore { private final Set visited = new TreeSet<>(); @Override - public void store(DfsTraversalNode nd) { - visited.add( hash(nd.getSystemState().getBThreadSnapshots()) ); + public void store(BProgramSyncSnapshot bss) { + visited.add( hash(bss.getBThreadSnapshots()) ); } @Override - public boolean isVisited(DfsTraversalNode nd) { - return visited.contains( hash(nd.getSystemState().getBThreadSnapshots()) ); + public boolean isVisited(BProgramSyncSnapshot bss) { + return visited.contains( hash(bss.getBThreadSnapshots()) ); } private long hash( Set snapshots ) { diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VisitedStateStore.java index a048b352..4e5b21c5 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/VisitedStateStore.java @@ -23,14 +23,16 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; + /** * Objects that know which states were already visited. * * @author michael */ public interface VisitedStateStore { - void store( DfsTraversalNode nd ); - boolean isVisited( DfsTraversalNode nd ); + void store( BProgramSyncSnapshot bpss ); + boolean isVisited( BProgramSyncSnapshot bpss ); void clear(); long getVisitedStateCount(); } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java index 50130eb8..69bfc0a0 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/StateStoreTests.java @@ -19,11 +19,11 @@ public void ForgetfulStore() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); VisitedStateStore forgetful = new ForgetfulVisitedStateStore(); DfsTraversalNode initial = DfsTraversalNode.getInitialNode(program, execSvc); - forgetful.store(initial); - assertFalse(forgetful.isVisited(initial)); + forgetful.store(initial.getSystemState()); + assertFalse(forgetful.isVisited(initial.getSystemState())); DfsTraversalNode next = sut.getUnvisitedNextNode(initial, execSvc); - assertFalse(forgetful.isVisited(next)); + assertFalse(forgetful.isVisited(next.getSystemState())); } @Test @@ -43,17 +43,17 @@ private void TestAAABTraceStore(VisitedStateStore storeToUse) throws Exception { ExecutorService execSvc = ExecutorServiceMaker.makeWithName("StoreSvc"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); DfsTraversalNode initial = DfsTraversalNode.getInitialNode(program, execSvc); - storeToUse.store(initial); - assertTrue(storeToUse.isVisited(initial)); + storeToUse.store(initial.getSystemState()); + assertTrue(storeToUse.isVisited(initial.getSystemState())); DfsTraversalNode next = sut.getUnvisitedNextNode(initial, execSvc); - assertFalse(storeToUse.isVisited(next)); - storeToUse.store(next); - assertTrue(storeToUse.isVisited(next)); - assertTrue(storeToUse.isVisited(initial)); + assertFalse(storeToUse.isVisited(next.getSystemState())); + storeToUse.store(next.getSystemState()); + assertTrue(storeToUse.isVisited(next.getSystemState())); + assertTrue(storeToUse.isVisited(initial.getSystemState())); storeToUse.clear(); - assertFalse(storeToUse.isVisited(next)); - assertFalse(storeToUse.isVisited(initial)); + assertFalse(storeToUse.isVisited(next.getSystemState())); + assertFalse(storeToUse.isVisited(initial.getSystemState())); } @Test @@ -82,23 +82,23 @@ private void TestDiffJSVar(VisitedStateStore storeToUse) throws Exception { List snapshots = new ArrayList<>(); DfsTraversalNode initial = DfsTraversalNode.getInitialNode(program, execSvc); - storeToUse.store(initial); + storeToUse.store(initial.getSystemState()); snapshots.add(initial); - assertTrue(storeToUse.isVisited(initial)); + assertTrue(storeToUse.isVisited(initial.getSystemState())); DfsTraversalNode next = initial; //Iteration 1,starts already at request state A for (int i = 0; i < 4; i++) { next = sut.getUnvisitedNextNode(next, execSvc); - storeToUse.store(next); + storeToUse.store(next.getSystemState()); } snapshots.add(next); - assertTrue(storeToUse.isVisited(next)); + assertTrue(storeToUse.isVisited(next.getSystemState())); for (int i = 0; i < 4; i++) { next = sut.getUnvisitedNextNode(next, execSvc); - storeToUse.store(next); + storeToUse.store(next.getSystemState()); } snapshots.add(next); - assertTrue(storeToUse.isVisited(next)); + assertTrue(storeToUse.isVisited(next.getSystemState())); //now we want to compare specific states BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState(); BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState(); @@ -131,24 +131,24 @@ private void TestEqualJSVar(VisitedStateStore storeToUse) throws Exception { List snapshots = new ArrayList<>(); DfsTraversalNode initial = DfsTraversalNode.getInitialNode(program, execSvc); - storeToUse.store(initial); + storeToUse.store(initial.getSystemState()); snapshots.add(initial); - assertTrue(storeToUse.isVisited(initial)); + assertTrue(storeToUse.isVisited(initial.getSystemState())); DfsTraversalNode next = initial; //Iteration 1,starts already at request state A for (int i = 0; i < 4; i++) { next = sut.getUnvisitedNextNode(next, execSvc); - storeToUse.store(next); + storeToUse.store(next.getSystemState()); } snapshots.add(next); - assertTrue(storeToUse.isVisited(next)); + assertTrue(storeToUse.isVisited(next.getSystemState())); for (int i = 0; i < 4; i++) { next = sut.getUnvisitedNextNode(next, execSvc); - assertTrue(storeToUse.isVisited(next)); - storeToUse.store(next); + assertTrue(storeToUse.isVisited(next.getSystemState())); + storeToUse.store(next.getSystemState()); } snapshots.add(next); - assertTrue(storeToUse.isVisited(next)); + assertTrue(storeToUse.isVisited(next.getSystemState())); //now we want to compare specific BProgramSyncSnapshot state1 = snapshots.get(1).getSystemState(); BProgramSyncSnapshot state2 = snapshots.get(2).getSystemState(); @@ -191,12 +191,12 @@ private void testEqualRuns(VisitedStateStore storeToUse) throws Exception { DfsTraversalNode next1 = initial1; DfsTraversalNode next2 = initial2; - storeToUse.store(next1); - assertTrue(storeToUse.isVisited(next2)); + storeToUse.store(next1.getSystemState()); + assertTrue(storeToUse.isVisited(next2.getSystemState())); for (int i = 0; i < 4; i++) { next1 = sut.getUnvisitedNextNode(next1, execSvc); - storeToUse.store(next1); - assertTrue(storeToUse.isVisited(next2)); + storeToUse.store(next1.getSystemState()); + assertTrue(storeToUse.isVisited(next2.getSystemState())); } } @@ -226,22 +226,22 @@ private void testStateStoreJavaVars(VisitedStateStore storeToUse) throws Excepti DfsBProgramVerifier sut = new DfsBProgramVerifier(); DfsTraversalNode next = DfsTraversalNode.getInitialNode(bprog, execSvc); - storeToUse.store(next); - assertTrue(storeToUse.isVisited(next)); + storeToUse.store(next.getSystemState()); + assertTrue(storeToUse.isVisited(next.getSystemState())); //now we enter the loop and generate initial node //a is 7 next = sut.getUnvisitedNextNode(next, execSvc); - assertFalse(storeToUse.isVisited(next)); - storeToUse.store(next); + assertFalse(storeToUse.isVisited(next.getSystemState())); + storeToUse.store(next.getSystemState()); //Now loop again, this should also not exist next = sut.getUnvisitedNextNode(next, execSvc); //a should be -536870912 - assertFalse(storeToUse.isVisited(next)); - storeToUse.store(next); + assertFalse(storeToUse.isVisited(next.getSystemState())); + storeToUse.store(next.getSystemState()); //now a should be 7 again //and now we should see the node next = sut.getUnvisitedNextNode(next, execSvc); - assertTrue(storeToUse.isVisited(next)); + assertTrue(storeToUse.isVisited(next.getSystemState())); } } From f3cface7793a102170352db9d12f48f63d1a8730 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Sun, 3 Feb 2019 23:49:30 +0200 Subject: [PATCH 03/11] Removed daemon terminology (closes #75) --- docs/source/embed-bpjs.rst | 5 ++--- docs/source/images/bprogram-running.png | Bin 20837 -> 24303 bytes docs/source/images/bprogram-running.puml | 2 +- .../execution/jsproxy/BProgramJsProxy.java | 4 ++-- .../examples/ExternalEventsDaemonTest.java | 2 +- src/test/resources/ExternalEventsDaemon.js | 6 +++--- 6 files changed, 9 insertions(+), 10 deletions(-) diff --git a/docs/source/embed-bpjs.rst b/docs/source/embed-bpjs.rst index a9f265e8..eed48e9b 100644 --- a/docs/source/embed-bpjs.rst +++ b/docs/source/embed-bpjs.rst @@ -81,7 +81,7 @@ At Runtime * If the host Java program will push external events to the b-program, make the b-program wait for these events by calling ``bprog.setWaitForExternalEvents(true)``. * Instantiate a ``BProgramRunner`` object, and supply it with the ``BProgram`` instance. * Add listeners to the runner. -* In the common case when the program needs to wait for external events (such as GUI interactions), set the ``isDaemon`` property of the ``BProgram`` to ``true``. +* In the common case when the program needs to wait for external events (such as GUI interactions), set the ``isWaitForExternalEvents`` property of the ``BProgram`` to ``true``. * Call ``BProgramRunner::start()``. The BProgram will start running. Life-cycle and behavioral events will be passed to the listener objects. In case the host application would like to push an external event to the embedded b-program (e.g. because of a network request, or a user click), it should use the ``BProgram``'s `enqueueExternalEvent`_ method. @@ -98,8 +98,7 @@ External Events vs. Internal Events There is no difference between external and internal events -- both are instances of the Java ``BEvent`` class, or a subclass of it. However, there may be a difference in how these events are treated by the event selection strategy. External events are made available to the strategy using an "external event queue". An event selection strategy may choose to ignore this queue whenever it can choose an event requested by a b-thread. But a strategy can also decide to choose an event from the queue even when there are internal events that are requested and not blocked. -All event selection strategies currently included with BPjs ignore external events when there are choosable internal ones. This choice makes the system easier to reason about, as it gets to complete its reaction to one external event before it starts reacting to a new one. But this does not *have* to be the case. - +All event selection strategies currently included with BPjs ignore external events when there are internal ones available for selection. This choice makes the system easier to reason about, as it gets to complete its reaction to one external event before it starts reacting to a new one. But this does not *have* to be the case. .. _import directives: https://developer.mozilla.org/en-US/docs/Mozilla/Projects/Rhino/Scripting_Java diff --git a/docs/source/images/bprogram-running.png b/docs/source/images/bprogram-running.png index 7b61e995fc7778d130338ee96aee21da37a130eb..fefb4c9ff4b661182f8fc4897f740e5dfa0ec4d6 100644 GIT binary patch literal 24303 zcmaI71yqz#*ETF7pyVJ8BONL&-Q5z>-O}AiNq35bba!`mDBaz{&`39Y_n`0dyleg6 z_phbPQ+pLY%- zstyL$Hm(+*jU1kdeYW~+r|0n5kXYZ9*u=rXhLfJ&#zN1^!O_x!&cNCdoq+=ktZ;9t zsOs=P&!52n%eW+4Dtxk@X8?KD#Xj1szf#vjS66!bLr%oI;7z`X>6~`By>tmDYtPXEeL^i%6!7XBD;7JlvnDYVj*CAFwN7`+&Nl)^On z@<>MlW+KNaL*+x#%EMdPe_EK~-`oY`@-L+?gwC#nP_d>?8h)Md2|yf0u$H2#2&NOb zCKB{-aI9K^NkRWoo0ZEur&{zWfsA&>iOk{s!G&D#mP#;1s-k0s3P-->TcP&QsFy6U znWA{HEbkJL5{}TO_o`=2Easg!AT2NCk##5?jTS3WRlo7=*(KX&xVK+sb=0yM)wJJw zdjyRc5|IvPl%r;}|1o2dJTLR*#DEc1@!J0kNI#Es61oTbXfa9+(^A(|l)EB>6a z{>WF!G_+gcIP~>2ba)O=G1uC({^q3OJ2oXZJx;k0L;_o%7u-!osN)Qg>A<8wHV6{? zIi>V^rQPG^1=g~`Qdv>Y+BCoDxQykmUn-G2K`GBZU?_UO;jNtzXjKgD~8DB^hBQ`>-%*FA$)w&nQGXITWkt*4xYJ>- zqNI;SVmaj$OqmKLSFcT%i7NaVTqOu3Oa}HN9_m*wUMZ6)KhNATuQ^|`P*gtg~c&uAL5t)|9?mc zRSRm0QwwSiKE}+c@0k^PfL=tW^Jhfm{)2fcXKrZKKI5J*530j_g&*QbpQDrj8kXCVhym~5Sdcbuf<2bEeqE@4zE?_>Yn_2~+j&(r-a503|@ zI@-3nyk$VY5Hp12G(MRFU8jDI4e`Pe5(b)kLk}8A(=bDaQQ19?M%{S_@=wAH#9iCs zHhlQTM755@cDw9&-L0wTLeZyw1+hK0SJUsPZ0gC9<{$buIP6JV z%WJHcc&J3l|z=wUr z`TQ%c0t?|C=!<8iem3{fd!_e3-QO$I&=2!+DHW?SuDn(*RFwEsXC=+(v@a)h(cyS{xsmd-6xeI^iS+%aX_hHB z2bHBGD`lvnbik&f=u#ZfFPM4qs&lw?rWXHg9Ia=&Sruo~*%3Z=Ae_`ur5_jiHHpr- zYu2CUqtS7>{>VGp{dta5U^98&=gDmTC`nPP_t9X+@OvesMqm|1fbxKisZWe=_rVBl}@n9Fj>A6{*)!kV%q@+3E_K~ z#TZ69j=pSwIDw{$RM6vfQt6hxyuv@C*(Nb=*e&cW)X@uRcQraX2X=k?Mi5$}L4<6* z0k*e0d`Se!2(-eyzj4Iw11l(LI(*Wx-IhCSu|;y*{7w@cV^?SqzV@Z{+DN0jp=d@j zEfn2p*Z_1|zhq=zKm7aIxdXv4A&CaaY&lpG-^^Xlcx7PE32UI%NcBL;IMj)@Yl(c0 zzO34h>(f>qq=?rVGgU>KL-k|Imjd>~`uX)}v0O2~4Bh+tOCJ64Z1j`*5uW&4yQPXg zLNdvCItrtqM#<*0@z-iDY-WnG4hKIdQ(d2A z8UOL!sjQ@T5|^|4e@z0rjv|*g2TnD%+t$peBUWZR_{kW=JuX-CdN+a?uu4YdLC;Cc z1)NvbH+(6#Qn`Xmiox$+Jo{BVmfv#Aa#v*B@$6)auKVMphP>oj^V|4MkI0PKEQ*WR z@Oax6y><{za1;(g1J&3~-k=d`Qgz9x;_Kz5&NB;w2VE0ijhRmGzp$N6IbI7iCp(FxL{-sZAqOj$Y17(5Qod<+@jkft za$}z?RzW1@GPkGp27~NX%D(gBknJZURMEwy&5t;RbsT*}wK?@b>d9q-|B^c7-6~au z0oT*^=qb^BI*d4H*z3izh-BSlsVQ8=fe*_tImKzb-7E%i=3E({6NRXzq;22HLEuCU z-zYd9j$P*s&p0@-_>+|Fa6)$OBq2qdBdq>SIhL9Bp~EYVty!mfDG1eGJ?YWI(wvW@ zu5!kY&G-EDDNPO!Ij2l1REeDth)x$RojIE}U(D=H2Ph=tKvFttpIp0d`V z_J-lnAPtQ0E?}Y(uolPDY|CvYPGm&6?N{KfSvpj#HV-cG2?bt&-f-1o%5vL=QhdZh zu-9HasM8^vNVSv1_*5Vd7s`%%JO&rg99~KqMytC(g9>^bgdnUx5Qjh-fgueZgurDm zhx%$IjD>t%#TUkjS!y6aZil>vbsF~V=@F#5tYGIaX5whC$xAclO6rQ(LI|4=x+#y0 zd%Rs?swBc1GME$}HSB$iCcD*G7tNY`)xz*h$U_K1l7h$Sw(YJ1x#ZNDoD+j^($+Ds zGN?iLQ`o1OIO`HSqh|Ox*>=I{r*J7v(rYrNQakPn5YH4IN2k&2$~bc>P+*LD=_o(9 z`d+gXB>ux^t9fe&-t?-9IBL=B+P4`g9@gw+OSXe+#h%822e+k4muj6Uf01&?;{*Y< zIOdx75C5U+SB{T4>iroD2&Ot-JY3CXN=1f@Hmh@XG|%<6L;D`mygZdB%e;!S*o)Qd z^Jw~=58V~5vXZt;x;yFv2zlm115oxPA3vP)1yRV*9F7xT^Hg_8b*o*mutNxIgR)3 z=Bm+LGvIY7t#9FJ>nPF%r5CgZczW|~kfobwtciw;ESJ54kk(OuEm%e4JTwfqa4H!7 za`#K|=t5NqZ&}vQTK#j3<8Rr#5_C%1NjQ5Iw88%3q^b&lvMOU8+GP(mvD(*B^hR`e zdfGi}w@1$X-gBR_;Dd-fXW!*@XRflWgT36}j8$&_w4262bPK~B05E|1#2!ip})*%aXZ0hAjG6%*LpZ*-DNC`I}ZsvriJB2GBS0h+qca=7X zM+mXkL`0`)4a~Zrr5pZ?8K)aXF-2ush)Z;$HJbdfH(Bs*1c?=8fz{~G{_=f2I7$=; zsZm?*tA0pj4U1jv4=!m9a%9; zgi*n`c37ucv*Vehc>~06T7WHOvwD#(CqVtsRe(8SMontqO;jr%+uT^!aI3&zYFFqF zr>f)jimKjF1G6_6B*^CkZ>Zw9t+g~>U1OeEa90~Wo~AMV#`Qa9t;MJMg!dOb`U*Bd zdmmBdEIDwi=y`8US~m3nEmqVJw;rUb*werJxHGWl6VAA6J5>pO_+a&YeU+J-d>$I! zyL;+~&&pteVBvjH5_(|#&!(FX(i~*Qu9M=pnqJDC;^%D!z>baU*UF1Sq&RVQo7Dy^ z;c!ig?E~YI2s4j;hg;PTSDB0y^@xlFET`2}a{Ccx=jsHSy?k+4QkFMhh!!4V>n)GD zZ65=~X!OJb&-~YT2*V5vKMzGaMTEqUEeXS~+XusNL2U8ugMdiOkKoY#igcY`u1u7h z!hV&KlO6)Aj(inqMS1qPoKF%?7BABcc)E(<_ZZcK6Ci0+Rr>P zT>4;Or*OIL0o3r+9_+0@8$az{ur7;Y;E`D3H=#-V#8J|}DIc`4c3q18b z!+TztQLizq&6ixatQc@yW)Ci(Fpf6zoy^66GOqNEGP7!!2c0UAX-~MJLd7~*wr~GR zpSw!JhfHbEg0s&y!p`t`$t2am-2^jaIT+KvPlg4($LgW_EQ%O*KI9X zFEVS5B#wC!S`=2|&;Sv-d7bgreCb1|<-QpEI@TF3>`qG0EX2pZM+3*iD3jhw?`@D-rkrAh$T@@vLqcbwlz%(qz$u1r_MqPoH_nosbMNa` zXm1`6=M=%QINh3(aM|*@+J-F;8M}zUA$|n0ZFcKYGK6x+p0V?%>*BQX3HP@RmeP{! zn1COTU-`E$F`wJMqP~aPA zgJRoG)IppItwS+dGVdaxui`$vYP)&~K1mD6;AG6s$y`~+eyOm*wA8k9hTS#MhzpMR znACKCxHPS1Yp5T!4kBCZhWQ=8dJ@k(sS7IEw9#GTc0Kypz3~8dx@})U{DU3$H(T~; zAcHcXW9L8uti(9Py|aj2d~0Z{z0Pi?RuYGLH;v5t=GV zi;ODs?1?Vir%MXC@h}30}0IHX{WD3gxn=;gXm{JP|m4GqGJYL#jJyLMq4FrG{e$Qy8)H2 zd@iKNA^I;;s9Li#dU2|)V}Qh%J&CLpTCDr5^LHL?+cSQx;y?@l-c4r+?z&t#0ugys zYd7E7OW>p*&Dp3b7H4)YAL%*b?f`UGy;}w1P*!IXn_Jf&2ruih~(Vq1F8z5Cg zudDbYR7mZ8w_mZ*nR;D~>j?&hA#x@Wi)?0-&oZcRfX)pjkoHF1!Xs~!;aJE{xgfMY!lx5;YiD-|g5J;l!>wAAg-Tjr z&T19xJMooLEqiD=-ecXyV=ZypOCTk3zNq=5)MZAJP6*b0aM=vJRx z(j4T;qGKJJ`}^xzNQ(vi?a;M^Ry^voiZz_;>bHI%WfR{$+@_YZ16A`{0=A&dyr~5G z8VFU10kA3%En~@ngHORje{tW1#?>>#rt_}v)u0y7*7FBwwq>^&Qh94KmYGDe{?*1l zb*nldMX}1LCddX^+Q=t>Hua&hIHJyow~b!z&+s!ydwRS3~lk(HNW82=?j@d`d;iY9UeRsL>t86zA^! zcT{%~yg0B|sX`r50r*717zmiVxIw*NnH%F+EgR{L?70(#bJW-7@}Sn_%TG?|)iDqo;?l{T6w5^BX+3g&gcx|8@uxw&c- z(*e4~xx~99xNLDcn3tY{2!P)-hX`?BO{r+~AP^O!kMLaj{XHD+g7Wh68jIDbJZ=$U z9sUFo@Is3^i^hxAiD(10hA`Yq#v#P;D2K(OimAK}+c!k! zOL9nmXs;a#(wK>nk)#byrTDown`? zNF`^AhrkMeYG2wFUfk~(@D7cS(=6ew#=L*LzFi}XcQ43&S3J1Gu~m0}8XrU!h!%Q} z#1v_$vS)V{tsU>d;kC>ywU{X^Lqzqm6I(!L$}{_LF0Ck2mm%xpLYp=B<2Z`hkIrA4 zj*X9}6AK9b-a5;ViWVQ=9FN3ojNIGq`e#iS9ET!ucq9|Q)JP{F$uF3flFYd;4e{yd z$r<-l+Q3nc*qOaeRq8wE#8eL8PRBa#9Ta;UD?5!Ofkjx#&ZS2DeP-)JY=J(hcn~Th zP7tp~x+$xKiM*`A>zMZ=x7Z%PdOlKeI^d3D>gbE9M){KWZo0tw6R#U_^t-r z((Wu@!ougr#~oeyDj-kjGpddmR>30id}b7+Ou) zMK_IquPH@cr?g^`9e_hM2)s%m?=?8eIV0co3SbQ0Y*gn8oe_Ofr#`0jbfoNljhv_+ zc=JVSCltAa1rB(jGb}33Y5Fzo=AOj7#QpgYQ_YLl2*e6f9*S)UZ27mq8n3ZI@L`PG zaOA=;;_SBlt#=-EH5Zu`?55DE5^AB;)?yxDPcgPQnLUh04Z(2RkCMFpG*-1l%Rh_s@bbF>h(y|CG$%0;d zA{Wr>C!(1iFI=Z~nNx4t`1>B*%jfh(aACz-qies!OM_r>TZQ_R{AqgKmQ*@PVKgdhU+~${_UeO>c}j5raH`ldGGsDNPn%baqC1v#t8w2VduL_^d~aZ} ztQmfMuU9&nHWFrDgAs4W3!K5|`nOqCrNc}$xINxl61D;wDQ$c1a*%M&$4OTaVPxZ2 zqI?z;US+A9oML4=^jgPh1u|fZSrSUybcSveb4M#yOWBF*?{U}fAuU9~jJtSCy(QYWg-+Ty1ro#kKw zn`&SY^DKp}tWW8*_*yIQ#b=hF+Uho?KQLS?-oH_@6u zTk1$x!q+CtRL$%l1+~}nf%lU@_iupKVw5P{66q~6T);SI+k|VVsg5ilY>Lr5kU0X>p~utUs%=VEFp1C9?Rr)Vh&F^Cxq<+6|&x&=LcOkz~(>d7E%(p-w9 zI=~p!J?iRHG_+X$GB3^qvzuBU(>~vn;frFvjF?EwK0HIxdPz7mE>D?sxifMtamotd zmO2W~u0L$!w@!X3n6w|+448a|=I?0Fjc+BOD17MDgx`p=S^^yMATMt^iYj*8&aV~l z_S~7<0_^Ss0$#06A8M){?q|Q20PdLw z*RjsyeJYgAd~wnk%PX+PulKgKe|-FAXXL_*Q$^p^vH3LWc5#Ak!VB$*2jv%+(h7Vq z!bHUkSVw8uj4I^YSh1&mUXT`0UF~>tROdSKv>F|-nxWoWCm#c4bU_Zvz!<0Er&Hn( z>^PGW{2eTxBfB)qUqoBRCA}0cNd=;3a?X57;X$E%=jF7Re(SHe74Gr8(v@FKy1Wn| ze|v`iyS5qsx8D7wwZ|>Ty)!#p#ue;@>bY@C(z={qg}k}i8(4qx#5B#!oO59$0h|D| zvjaF14~=kz*o2ar(%c(VbO3kFg4X4PVY*b3yvQX)D;bcpai&5vhK>GFTY*) z@xQ0<$L($NTH`)Gzo3aBmtJhs)y_ai=u(l8|4e*giVFs>^+(4`#4sNhS*mq#q{)_( ziWMSPp9tC#OBmy?GqeiKS7XzvJ4i`Nnk|&;bs4dkO`4=P$tq2y`MmJ>u83!{=?^a! zGt8WP^nd4rH%=35VgJ5Jk%4mfhxhn++T!@^J6p&mZD7d$7oOkYs8a_dakaSbSv488 znp;d8*d0vLSZEVL%*ob9WqJz%Xhghi#v`d4Bp{nkZiFy`*Yhe88u03_5{kaJE(W=( zt~a{Tjv>S5Tfw6zw4{4;9;9av9g8{^d$;JVXOkW4=gCnNXq8tJHm(1Q7fuG%RL|F# zvnk!b6Tdo9YFR(+*xl4$DBscVk-!PcVHx>8+1z}JaB5)()B0Wit>z-kB#+GCaM zKB2wuOO{j(!QD1#hiBJfTO(ZwG|*MaDtVOC~|8j3ybXJobUA9!GonmRk@giA~>i?h;hCC4h|r=yz;p z)8h>apoK)d&XCCx*`BH^Azc;a@r+Bg`aCnX4uT`qQ;qG0xo9!CQjFHBD^q3hOvLmx z5$5g|iXXvgc z<*(c_Q&D%KBY&`|x!~n{G~#JitgU(ITMjtPFa|U^?}vckZ3dg+;#^|B@D9ij4R$oY z&`lqPV92!I%msXm)+#GgJ}zKen~yTE@apS$gPfnElHrR82g13WdEcwoa;tq{IcH`x z9e;VeU_G)BfPyzJ-FzZ>>_I8w57lAzrchfz&EuDDA7cQjX$#GFLf<~cGRxpd_b4K2 zUJ+mK`Mi=2ET&d&y%1Ga+ti$|Y*ijdyyJQ@7ITtkgdCC&WomV$6xsA@II;qu8-vP+l8$idRy@P=H5)RoM!bg0e+%?JS#kFI{d?Yl zAIPEq<7eP=v#%u+90jvWJ?vF zlPFrVQ&$S(glPKgHon4W36G?{*?e?f843m=*yGOTN;8e+NQKD_ZWh8+B2n+Mqk>n_566hDzwuSZLg-4DlPe)Xe8lVXe}H^n?!|8pSqba zvsY#u+H{mkL)UV~%?Q-C=%~8gE7d!^uEn>9Nu-x#_gE^(F|I{3YRS0yr`LWdWrq!R zg{q8Ks8TRxc5B7wdP#&V?g12wAAbkBPr1QhUm~KGW+<2J#@&~-;=exKk}lt8vp<+` z>K@JDp}F-nOusNSw&@9{-b*199BHwjT|H%YUg|C12x~gE;s9A%L^khWOSwz%wBr(D8OgX zyID#9r7OU#3*vuuzB?6jJi^!3G`P2D&(&{map;lDJp%B!9d;!>e?#$lcYY!;C|Scv z718CpXScwXbE8L3UcHKq4a!ne9g=mC>nfi*78)CopBe4Am=Sdw+C{M~UMp_J!B9Uo0^coRSO*=YEBS(`Spj$5@uZ;jWn zgOSZ&qs?t{290tZsUcl)M_jcLbVW=&o=`gq)T_nPDTrF-0er)29r+RZA`66pisY*y zwgp4a&%a{h+J=(S-nKq^iV3Sm5*~b(F4FHgkrxJCOvsM(KX>W$L+WyEIiI$B2Vd3_ z$F&7xAPAnc7!B+5B0~<)02)ZgR~u{#TRD~TIf&!$hWc7B=GRVet(z+pQz6M58;0z{ z$O|hTICC%PWoY)-%bT6pDz;kLXyKYA`PRQaorm^y?T!wXyOqcAYE8Bi{-Wm(ldT>| zu1iQb+SHUXVC>dqgNTCnJ)q0gtjOt5C}W3BD-#1z&6APFTS?aOg?BXMuvzox+2jz= z1!2>sT+hSS$a48oTWKn-v~1dl#?$HbeNxN0VIQlUg_}N>#ns# zlgN7_(itXG<*2W&A;w)hPWvvx0RsGC9=-@^7^TtP`5XezMq`PXx4~mI=IZSG2X!j_ zXK!Z@P6SbqdIPuq?Br4X{1dM;oKlk6J2KcTO$a$^(}`I?!q%ilS?n)je}Zi;9h4oc z*cw?6i+8I^H|PjY2jbHrH2?%OI=p@6=xeopxi?33q$f$I@zuPH$I)+xNM; z-|UFGE?2i1q!~na>*yM{f~8<#TD6I30=F&zO;RIq-JmO;cyprcC>nq`yklGW(kR> z5ZTxoyi;Cw3Nz(i)*t6Ky(4@pH0FX`ftRR(ORf-dQwtD?g&uc>15%9zOut|Q1oZ2S zQShfy%{iM>^)KY0`0JjK1r zwC&W%>e+Tfql z{svJ+a!Fx|-^3?$`5Bhfc}w!L_W_AY7EsJ02dB@~OYfyeqDimk^(MAjkpRkSoJOx- z*Pus@QRdcHo6}aSrTL$N_^uhbV}(kU2_GoxoV+Pbml_+SKb_6Qy;qWVI9%*yEu(Lp zB`rg%dBctYu2ieS07s%2i%u-f@@~dbuIDC|2C>(z_wuKVQ0==r`f3Zj(jSDmF1!>h z>Bg)>jF`}^{(%tjD!M>ECkAZa&Ko8$S*%72hJ-Q2^aP=M(74WR1|Gwcm83c7{)4)N zxVj66TW9Qmj|sR=KN`&0{4R}mX+uJk3j6PAA18jsSgBPx^zC>$SuEDK4kBefgROtK z3GIXrW5_B~ra;uiEpc55rKgMY$Tx}ewIOHbKo8*6m^7KM<pRYz_ndk^=6FzS^}3kjxcJDT@B{HfD9|U5+(; z5*yD6Z{Xfd>A>RJWpkatgYC%`i&I6s-g?6&xlyQC@*{cN4Ap$J$inv|+U;3?BY#dn~NjgEJXuZJ>jIeYY@R-qdjD+5|`|o*sT6_#N(-IS4KL0)*pl{l=AWuGmjx8Be z>v6v@9ozKvUN@V1ABx7SN~XaGdiUEKTU37hcui27hbkzWk$2-i5lB9*tiDtouX;V7 zgzf#OM`ii-K+;*aq5V! zqeleez#w2x*1CcsHM@@2y@M*|&>b*Og}wnpJPena*&8lew)4D3R>PM%*WGo|u%cl> zykgSoA{vMAiobZ@E^(I4sgmNTlYi2W!5aUxp0NtH2E>B86AASiJCJ|8FT%g91?bn3 z7ek`B?f4<=#5^bO`a{sD*&l#I#0eZC@;I{PDYxv|Or-8#Y{@FdHJe4&p;N|@uesd9 ze^>Ut>V}$j(H#pb?fi|{o2kNL@ksZ{<_!sDn>$9iTL-54b#csno3AX=ZozLtu|xMS z$@=j26Haw=fmuK6#E8x)RpiNQ_s$`e@Q{(-$L;48+gj#pN1{By%qGu4lgYm|J~F4U z0p#7D1~Mj>RlSmhTHU8&&j*U=`woGMlj|1!rQLA-iSxQ(mZ6EyL>2<9H9vg}pgHE4 z`&9l_vDLT+HxHR177PI?;d<4&0yB`NiZa#f4|U!CE=K;iu#o&gwb*J@YuV&ZpWt@0 zIQ$txU4Q2gRI}!r!cWI)&gzY`j7AZ&PBY3CI~6K9xT}AMQw@6Zwm-<-o|)N@Ck8#~ z5nooh{tW~qtsZz_2})d8N8YsbvY7Y4^@0zU;ADa(<2UaMfbTFPAGUY8p74`PJPZJ{ zyKoS9UIANTrA|@UD%q}8@fZgqVnF`l{^<9xCCz>)hY<~xqJlBM+W03!$i1wZ^|Hdo81we&Gi2kaOZx})w5yX zzT@^Vgf#An_D9a;-})GG%gF~o&hlcti{M}W21^yC(I-@om~AP7MqN;czQi#hxC<)~yYLuU7`Mun5kUy8X z9SfVNietmjaq1lE@pPxg);}HaiV5stgx9m6+-qxq#dsmI(| z<0=BlU5|z}El%70MYEz8_n%i7bg@K~f%&UKi(YpXR2KY4ZEd2l^g7C0C8=Z*U-Y06 zukAinsy_+j9KvuYSZs>b$?F8)E1>B(pIM}h`v9I^mMBV8t15Ib*TDo$ZB9t!=o*rC z=0I1-KHCFx@ZNK`VriUSn_DWE>wGd7%1Plu4|IpKMO5z7o4}i; zX(JCyyhy$fdNIl=F3G8FXt;>K-1g->CG*Sq`=`2r0A9Y);ob2;-2zW=*K!NqS~I{H zMwya)*fPlK0dfE}+c6OjiXz1V@;JH_a}KeXvreelGp`F3dS2ciXfBJ4WZU{5gc;A512fj6|uPlawXkCr*w zdc8%x*~Ns(Mr|%5oc0?SdjL^L#l@oOU?I5kDFb7K3YaW-LG2@ad<3?O2!sjm-zyao zPZu{RKxxYC8E>i>MJSRBGwV1O;$~R4C>F$=I0LMsu;j0T(qj}aCUw~S$v4iL2Y+ne zE50?}nRf+-7Av1wjjfYI@0zSF6dk9K4aH-H$b(qV)2-W_XSfC!TUHeIITL6k;uS%X zqrf@K!UJzZDZyy3Qw35IA1$t!o-Eimt=L%wah>XbdX1U(ePNPmO@gqIg zs@k4*3@y7M=*$X+eR=GClz}uLwJc+s3=NZ%@r|3&9K&qJP*@|vsp9LSD_@n&+d>1e z+mlk_Cxm5}OUW?I#mDLP?VEj$=;Aaus>@Mp64_;z)3ddFg}mHk5pV3!FA?NBPnDDKsZw1C zdZX&7S7cms#mGBPX502>)r@YC^O-6r6B+$DwkziO$C=)htH-wRs-VwF63x4vkr>g$ zBiVUbP0yA;2lKLH@qNQa#Gc`0;(}M$nC^5;bZ$8SoMA>bVnTTWMBKt>aD}%5SvvAd zN5Xl{Q3#DiVaF&jVNU|M94qC8psOF`3v1c-q~{+`{hFPxaTb~EHU_4fxBOf0=Bmo# zw7L>ZgMKY{2Y0z|TH+wwro8vuGHA*Xi-hw7*@{K%6ESM+#7N!vBm5R{XjpPuVDEdZ zcgFqWx#pkOX^M#S1S4WG!G96yrf?-BdgY23J|w)u7}>53n9sc)_QfCh=a#31sh`uL zvG5Gz_ztAG$8fdcg>Oet7b~m-3zY$Vz2JW68QU(p7W){^(%6-G+yF@}-+#hyQycP~ z!M~pZSINOQc$I2bt>l@4V1I#R1CZ-HLEY!?a!&1irJ|vckAq5(ZlsLGP-}2*+^EdAICe{pj^*ABfMN3LnFehG#8Pw6lN0R#vBv8RJxTdaGA_-CcPhRa}jM&<5Fy_bj6i^5G8R zPI>A&sOZ#W>3rgwuipJ4>V=inbBKuXWM>2tlgdBt$7cuw-6LMS^j;MQ7 z*+~CLb9tHqFSI4Kvc!N$+3eyQZ@@q;$b;jzP;#&D%x#di^o7;x5~j}{BanDzit$7t zjn-va?cK>TE+j~u{G_Ley0NbUBY!rR{*^yVA`vN-fyPAes(QlZ7 z-Ua4!b9Do*gCI2fhy3V-84X56iNVjJgrdAwp$~Z1i8vQbCp$~G9}{u5Bnf7mhgfjL zz1wTna=;rDeCL|U)1DPvsTCtuJOuQY9Xsy6nks!eb3U?s_vv5^h7+M8&_K>$3YYel zx4o?!rIp^+o>OCl$>reT&Hj@QaCB-g%(*@}W60R&^w5=j!=?K5A1#V_o6@c%tQiw7 z^$2dK>eJ_3*M2*N{vkn~R`Y@Bv}H_d0LrXxk4x!j`bpf0zSdi-reg0*e$mw4@pjRN zAOp{w<+tP&FK2z=W+e677Bam=J-7Vt!`zLA!DL7{r|TXGUP~E5QfgTu;r;Fh+W#~$ zeVc&UYS8J2%vd|d1tbmi0%tA-l?Jv5sN+A5OKFA3qiXn2*^cvBINh}QY~ z^WV^A`qAMnHeuIZyF}`~8bz{X7>{gbJ1a_?{X5{=Iv8?nh`-^Ps?hJwFf-{LB*QXqjIv zn?FQa7H>pYItY+cvBj}Ck|B$haMruFVC4ypTaNLu@YT7uR~Q8TqC>@{2Y=q1M(EP} zYpTW(O%vA!G%Emf7#XQY0`eT<|9a$0u*wJ2axwL%ppCzw6Gs)}xZr zJ+ImBh9%SVzva?KMm=NF_{s1gjHrDy8G8+|o-8j1lRm+4m?iF;#ss;E{e`-3CiB(a z+jCV0!Vf{l+W!uh><}9BNk^<4J3>&$l2Q@2BvrfWtM#EoCYfoQaQazSwcDOUmtEe| zFRa>!z7yA^9&&rT^*kD9Vp#*7{np(Ax~MQ!84t8tJAT{MfYDAL)kuFGs*IugZTi z$!sl#!M<$lUmyZH`~XfrAu&*Zd{a#lSt_$B#Cp!f2#=xnAApQDBz=-K^RTGrU+h)o z6M!Y)fBqN3tB8>gIU_@JUBe-9@X{8@;~99xy%ax9pa7Cd?Eal*5zuPG(nf}fRPjqV zBo;pO`h0Ij4K?A7+dd<@{g%Wy^;5V9md(>9;DkGw*7s|>1Et{?7Ir=bwWaNv(M$Z1 zcPP2bdWflvUbjPR@oMYe44I!iKBW>Fu=_(?J3se2G;|;6?Lgt_^!7D4$Qh^n0dY&g z;9aP4NzA5a&1ht8{f`MBOBrCq)0Ir;x9MeT*Tn(a0L}r!CBFS4qa5~urVZ+qcIi?B zdkKpWw#UDSii|T8IPy2cr>n%_`-uLst3C&H!SsOn=w4o0znxmZ! zu&Jxj3u~U3X!>>TLM+qE%spvlL#Ijy-eG)$X1`;=gOgWdH0dUYE&Xr#gZJ-6H+xMf z)brp@lTYlWd=1vxCLGkM?4ny{p*CP-Z$mmNQDxM@4`M`^*Q{c|S=Gi-5yC}uH0WTp zXevQ5I1Kp$q<1H?s)S(sa+3G#0oRt&4Ab_u>gJ*?REA@Q|7z5NO#RuiCCO?lq%Dq3 zNL&D5t$6QwV`g92`&w|=cja))<^oeHROsRft{trVr&X-TH@wHc_~IBu!(aJxEKjra z1w#S(2O~rpTMH^a`jAS>`}YC&^CiN2wYsSao>ot;`d$J zn*fPT(}21|=LvF#(^uvsRSPgZF1GUm#nVS#-=YYyz`JG9mKxRRCdJq2F}Q^N;9DnI z3C0NYA3^c)i9;|G#5H!gTms8Nd>E0>HTeOT^k*a5uFxP9i2YzAjntado;Dk?In;Snqo(GCeb#&o7<`KOmXHMMk$FUS#0YkSHzaV3jj7D0&F7kb5;Dq zGIW2RR>?x(?4kH_mD{9pgCt@e?H+wxp>!=U=JvgOtbKoifjx#i1uqCF?R&fx@o;R} zZTd7#9iSZpSR@Gizm7q#2-w7i-1IXvl+KjoKc`xH&LpK)C;rXJC(}mEjIPcMx znGS^P_^SALBDDE4s&bEUWb(Dwiu#Q-qXO9T=I!5Aw_wsw$-u0pHW6_Fl#SF)x4% zP8_(~e&kjcy`8qs^jcwq!m-aEr7V7F2@WMXxnRfG^7PG;x`^*mYX(!wG?hD>25JZM zEI8IJHH)WWmCb|;@583*MDWjk}7HcXgJEuW^2Hs)23L4HjHtg(H8vRu>y@jWF3#S zOxyMF9kzkfF6*dA6fTzcubh`TB&G|)Z+(BTVsD(DR1~+kJ!<`&156-VpJvdssgxne zAypT%!2~5axd2)t~xF9v$xDjNYLi2l`D`#ERAnkL5?o&5ka)!Py*;i zrJ2tWAKK<(Z))XUG%Q=m?lI=psF94jt$4xKTK1J7!t$*r@Uv9SNGvJ*yiO;`uvktf zK`#uMPldq!)PqD`bGSL%WtwOc5iGnz^osXafi+(NQC{}cBzEApn%HB3!L8B;?+okg ztGLk4Z$LN@gNNxdtyEpoe;zYw#eXsNe5&B<#YqKC6+62JHEA5w7G>HcHUla{BQ&Ug z<&Bj^Kr8+BxJI@WC(R8+Xd_;-f=;UKx0IVh;72)8*gIk0)rZnB9XOR~Ov5^BosXC{ z=TEkam`h*j!+G=TkRT)I1a^7Wc#Xfa-k2Y{&$GIO?RG9YZVBGsU+B__s=`1xcV~=m zl#0i^CbAu^UaF%f+ijRj3H;)*Tj!Z_!hGnO>G>3607;G#5+IG|TlF@5gu62H&x^}P0elN|QdOIZouy9s+3Wt3dP1KM_V!o2Y_Ne@@IDcKp^_L-Oxqp^!TtWj8 zQ3z7Qb^5vNUY4c|;~2nP5hHpYmslVVx^l4Poiga8-IVC$aihoeuUw-1?V2JX9q`6& zip~}<0TN~?Xy+$nd`|DJ%UZbR@@RX`T-Uwp(KL}4}^ zidDzi9VfoJ)aOfQ;eC0^IS2jo6qa{ue1Wv-zMa=S26IW^?JD|+1bBZKhZdolcvPN| zS9 ziZY*sEOA*rfAnYS9K8P~1JJ>!g|~y328WBsq#O+uAJO!LxU0#VLtq;rf26gUO~XAE z%OJTSzSlRC*7uy7!R5jat=3SevTBv2qOar_ z7lcEv0$>=3H#-70n*5r64aXa}TSiqRz5{ufo((zBjRrk+qj$Rb_n9=zwP-b@b_{LY zeXC7p>JBSRpkq3RZ&;3rQ6+n$@5?x2lv=a;TW^faan*E@X}^4Ud}<+df`o327{$jO<(12&3#v5($;;yTlM<-y+7ot8TIlk)>qcw`5C< zokFq=#+rSN^j^QY@1FO4j`w(u_n-GT{DJw+wVuE0IeoZrzi4%rY#{vcKQO8+!P z>|Ke)&C~(S?)PqZ`SX|?TN)D72F_I9!Nn9m|63uIcMvv&GKC3?q0TZt6Z*(w&P?E! zzIE#al0Fno8$oSQ;^o>j(>1y(j(nF%0OO4646>L8w(_`^iLtommgSe(hMw!%HOcF}{l$wO8nVr|`+Oh{x^Xs~u9sLT zB$28&M$@>3)SR*;q9Ib_!Iwv|6xV7FwoAp{9zC!St*NnIK3`stC!3qgKHK*(y-)s~ zQl_);BCf?dAwpyHlmmP5AknyB-lgt=AW}v(9w~sbXbSB*J)m#FX=nAMUNl_Z56{cx zp2d10SOKlcWMKI1P8|%c8=|<-$1e1PMAk1YB^0p8e0TzW%?^@AIl^#@o<@BxhpxXDWwI?m8Ip}qCZyiYg)5M*ca~CPS5doOsKnohOQ&!Y?N5C9& zlq#SgJrlu91SlHDpbbPw*vKjQsKFm9Ox$i?A~`s|L0o%Kfb1d!&#?iyFXfVu%;$-gp23Wa_}iX z%>H;c{1()~TbeHi3?42dUm~Oqqb+Twf{_JtV!Xk8pV5gdn}yi&w#j!Uw&% zG?2cL1Z%lnd_=3fPZVxQP{^_IQW8`!%-WuR1YdP|kQ!gf@$tN} z;q8YK!VsRW&~HQ$a4bN@zrNyU5<@UACN~|g12fbu-#ZKK_Hf7$n&Y$6ja3;#TY-Is z0p5MyN9b+Zr7);q1#3HgBNwvldr$7Sf;Li62~;M25wEOD2QOw-qNJvi>~YZB_x4N| zfMyvmprg$&GDKGb zr^pLyB?xr{)>A^<9;j*kpBYEB2Vcy{IV`~J(Itl>jHl{4vYt%TnIr?g5|ftp{VWk! z3~Y*`HMoRv9Moa^5qG6*qS6`fG77v1i_EF)?Q!fHk$EU6zeH5(y-2m`u}6VgbV{w@ zy2y48^=b?`S~b%e*0(-ZzTgFk)OZ(?0kb(HM4eIC2b1nZt9s0`TefG0SnhVSSnf6! zM^z?gU;&R9;E~O4Id*m-Y9vFShnlqtul!uG|33)cK&^+pM8HpMGe%tx&so|vez5#< zV53WwMYE~oeiV6bX{g;SK!2O7^Z1dMg3r%m&h3T10N3M#&DT3SJ4=scGm+}Mj6t`U z&ahL%Li6h5Xt72n!e3?fFsf(1haX@KP1*HwOxRCy72;370B;^Oxf0y;k}Fz&;HOKe zM`vDQ%M{(N8!S8qooleg(|ODVUI%#m6mDZ4&u!_Amb2{1{>spr?06JT%YA#a?9)|u z4jhMU-K)u7eS2wAbvz?K^_iJxeiy=8kJ^4REOFQd{bEuMt1vy#D-())YdTKLY6Zil zP}78+|51LqAbxAZ!fD~>N^xIA*yTDMzwI7L4SkEukrlpWuzmy+Z{34`n53bV=FKyr z@J5Rl1>824Jmwi_TF5Wqt8g4LS!4DclhN=KtsgMo^zU`Smfm0cewhDwY-^6(^y%(l zqL<=E{d!dth#J8Qd$$W2x|nZadJ*eR z@2(3cZ#jL)PhG6}isS1!BXa=f2&Yxb2~uZ=_LT&u)>>|`;Fc_gggSJkUGYph1$yqK zKw-pUZK`RIRz$wWW&Az!S zc+{vX8}`ubT!i;Fk3R13^^kjh#}+pG4l5U743FukyVtdzLly5#~ zO2!ChHl6tBFr+}IsofP;f!w>SLRAjl3Z@-E%|Nij0}JvJfAIH78_GEEF5hSmKFb&h zu~i@nW-lEkHD$~oXU5qBP(d5)QVJ5}VaV0s zHTwQ^-x{@)vk+lWUPMuCzB*WMBGQ8KbIE0r^~rp7!?Qt#wXLTsg%jh2OAL3dUnyGQ zED~b)Gxi0`>6~A`@8{+`d$^g6C?*hpLzGpuQg2(FI)M&0C9q5{-_=A}7Jf1lWP9zmd>OHgy@x&7<8 zp7oOuPS|Gwq;kqqsTQPwY?8MSZ<@0)VlqX-GjjP$L3r_pZ-Hj z`i(2U!il%ASB9Eh1jPrO;u@fs_-tVHXhi#mHrbOfYTJK%x>mzat=)@QTGo;~rNqX)&uOBt(Ku^%MW%JDsPiwvX z4rabN`yV*T^+Kt-CiS_UB_{Qkx6_)88k*64G{S@-_du5-<(Wc? z@Gu%Fy*~!YCm*@dF2cXh9yoNVlSiN<}}OZU`zUPwg_ zH@pt31-ERSQ`sy?QOKhqo6AF(R}J=F{b&6+UH%uQ$@1O2{v%6s#&QSISaaCK#hV8a zypk^`#24wL_Hyz(FT^m9B$+VrP51N05s_Qqn=N7JY`#;QtmwkU6s4K{lOv?HCz<^? z;xdKsPDl25EAr&YCMmUy(cTZMe&z}OS4HnI=oGW+CqGm`&Pu@SDs>+E`Wg&>E%}0BDdizLoBB`^CnzaCpmJD6=q# zCKm<~G0$G|ob*oTyO&!b*e1Fd8MK*`lz7lJC3Ly&0YsUEzMcXvyleeP_rgXq8Iohm z7hE8^d_Ofy&1R2d;?<5reh{vJr4@k%k#xM;iM_8BD8iII>-e3A>0)u!9sYIM)DRODXk|*BVpDg;`92Z z<4$dMF1Q#SUj5>gIdVLKd%8E48=eSzEJyZNe!_STDjOPaESuq#PXWeJ-f3;ZjT5^m zLjWu_i@fmZQc29VJ)msTgppdV6@PEG58$zLMTHf)b|R$`u1z^5Y66PoG^8b=9Mt+o zXOY*~<#(B^H#rT@J+9mVA%s}7%$(qTc(k+Tk}9KtKb2CdI>G9y5zj>8QU$9#SokGF zd%|1sLwx zy7cO@tgcKUW!u;H#9v#cLJlyk%M}Bbw#6DYKynXc*bv$q1S5ly+<>$Kef&*B^;yd( z0=srcL@pFu+GRNUq?Icgk79?62e?yAZLgYh^_DE3ZU^GVP}LE(mq$4y<@X}>GkztH zZuBE9u`Pv`EBWK?DUX&ct*~yfSL0Cx!-G{IZe5<_&8x-9hWGHJ+m}fva+Glp9Jaw` z%boCsg|MX6gcGYX=n|%mo=hx(Fb>-A&ni4n_2%KNfg#&(vg55eP~ZX>a$?c!)LhA* zp-u!jV`l*Qg^b{$iy&j@%>n;nLEsg5#0Dx=z-Ti6s}zDq3k?v^an!W__o_BzL8YDh zkk{hZ7YKO|7N@6Nfd>r!VuOFY3OQKu2x&sgj_uSQN3W3HkhLk0o}c70o^$6$$>#^ez4J6nJ9W= z(z%t}vh(>^;xCXEZCkuJQe2+@pr8)1H)^EcLRwyLuCJ3ju^1lz~`M+uB5&(O&A32UWEw`eySkka{z0*?M7GMAESQjve=NMWk%i zlYnqN9-KpLb_uNYQ4;9_AvI`^ntSRE2>V3DmBzGffR@4Js!$>szH4Vo0f?M$+8Fst zV&xrCeTPWH#!GIkYlMCev|0SSP=l72JVnNATrsB>5QXysa(^xvhKTX@)74G^`e_0F zo;rnwHUpW8ESpdweZCH{^|v~AWaMjQ-_Ks)5|#$I4|Edt_vrxT&Wws)8dAe5ZB-0C zS9yeY#Kf)NcXkK&vZ$vuYpGA_TCTFfDLa}V0mPU0Qa*3YV;8WZ^~lotxX;8Rp+&6Q zwJNialpeDa{KBN%%6t0KCleDiC@6^o>`_j&TK#K2tG#30Kzxw1_`-R@6KZp-FtWGkYB&sNeA!}y8HyUG3i^7L!6a+0G#$tLxH{QOi_Es zKb+cLYAU5|9%AvPVj#kzB?Je#9T2Anxg0L?I0ry-y-&v>KnBfc1VkpRB>*{#(73=L zAl>#byw&6$~0H5Nk@!6NVXY8Ubf7Qi0z*{iGclxnJEkG0RPVcOa(M1OVYtovS*+a1;%sC7-<067ctk1yIbqoA;0Q91;W zb+r5Et?2ZPeJ0z-#oj1-K_X6J;Y!(7lY}Ns=S-23*NK$g;t%(ANE`aOyC3fHBPHr< z;awWAH%Hg-dJvW#psAweIjA0^^5>fWz|^4t&yLrx-xI#uAw^M?EZ%WzpjmDXE%#eD z=XTc=WqULL><(8mYd>xpHS|=4JuWfMhc%0aBm%sGD7sIU$_zb<6|^*s;p_cImNO1nVXQqq2d4faKQkx86E z%ejB1_f!_F2@rBNJ-v%vUekeZvp^0<*&z-W*#r?EIpo)Y4YoH{<_Zw! ztY^`VXEVEjQfQ_`dF_p4kj@zrG&0MQ#tHRE$aI5BLu9Ygb zsUb-xjQ78b8&qiyBS;CWm=x*&@aHaH|annp_rJ`}7uXhC@m47>$V-KH2Pv$|RG(M@ zsrdAdetQ3cjUh+;(GdMS$?WH2f-j-{s!h@4mQcRx5)}=fAmyh75;bT80y0XYLQG`W zg1k>FWSt=&RrPJa>FN8Q?v%5teX>{yB23UvOJR6ETNaADCbCY5r+unI;c6F zohZbv8BqqbgMimw6M-HILJct7Mk5gIn{^we@lk^pIkcG=qd8|apt?TZfh*LL%r*$V z#M5`IwD>9t-?m-TYw@r!5RHwN|7WP34MlsgN_JYP2H^(Axh%IwC_buxwHB1{ogsR= zOgqH{zPewwak&a@__9~VrczXpNsR&i-?L>!9%5b*GMI+*GVnSd;;tPvIM172G!Ua! zZw^nEC#-}G;mV57qXrWcpF<;1r=rXfLEtebMcV?o z=#s%iX~%=K=)}StH!%d1v%F%ouYaw4q{MMQHpL63rTn}-{k7^{Xj;xWQy|FF&h*k! zgv0_rDjt*~45WTkrC1(Pv MyitGQGA+uLOdj0Wx@Pfv1O0cFFdFD#sH>|x>L8b) zJ39o0z3%^bh9FS$3wq}9ZC(&J2tsF)hVV$L^AK6Am-vp#A7>JTX->dpCFOA9G*iCx zYrAu{pc`zfEFR~N`j8U$A3$Hf_&~=h$ThR?LafsB2!+ubt8&Hdr!4sLu9JbQ)qj5I cS&!viyBzXhg*g>Kdj6EUs+LNTl6la70f;Pc4gdfE literal 20837 zcmbrlbyQYS_b$45NeM}%Ln-O*ZV&;bySuyN1pz^61f*NKyHSu1>F)0Cx*Namcg`7i zjC23FW5^KJ`|h>YoO{Kb&-2XCkMdGz$OOm$0HDc8iz@;E3>5rvMM3~u%up4Y!2f8R zCDfgb?Cd?PO-!8uDHB^0M+0XQV=_YzGIM8VdtN3cdusz*XBQi5Mk6~LOlBS;0DvHQ zDyuvHPdfm(r`RaX+0HSe`rt16k)5tPmt#=xP2!7v%;{y62taU3Isu9z}(Fpi*HIZTpc%OWJAQ4KiD|!XK|4& zXzQCe$KYpw+*WE;royHj96Xekcqr;3z-<%IWEeM8SQI7VWSDDJ#I~n)41E3mlfhx` z2u;I@I!T1?Ty+mlEj_N|(3clE+d@OL1J!246^u`X{X6=yJN$w}kh?|oYDgruCssCN zns|zs3B730<04MPs!^3MOnV9akwAK@wlE~_Z8 z0|{n_IOe11wnUOMjVhe=G)A%d32xk78{14>v-P4^Q*vW(+L_OmtgBvnYQxr0>YXXk z%K$Q@|L=cKQUTev(JB!kR229}NHhblMKECC*zeV)enc5JlUK87!HK|S04W|Wh2C}4 z@u&5m9Wvh~*?prySo)Zl$T-V~L4h4QX!adh0 zcd_`+u3ejT^P^vud{q=bqL+s+2rry;Htyt%9#5#TbKDcL`j++l)-G6$`|K0jtU|-S z;#0?2D%TQWx8JBA(EvQE!178)OgEyInM|>l>vwCUop*#qwJ}VpLna$Wk^y>?cHA`i z-KJec2zpo7caeU)GqoyqWfeqt5oKe#Lv|YRt5>BTGpli!bj5938=|VsM}%u_zRA>< zh=(Rm)N0w%yvdfl7;?SP@C*JOgz{cpogp;TBLWgNR!M3d*6^Wuit=ODG!?$6%@ulL2t%BN~3AHV^_P&3Uc)57)MSgqD;LzFq~3}YGf(__t< z`R0Uui^*?q+xxcFE(lj-Cq8o&)X9-HtG#F+{9|`n(3*|d+^T6M3mf{h}#)e3%zlh$E44d#f=s8nWe!T9S(ZH#`-C9cX^e+*dKx! z*%ySuH*sRphm$a+OK5qEs^?Rq5<1;<)YVYSW&Tksf>>+iHq2>%fp5trwX<_-Tp*5K zLpjZ3Gt>A=zvduTfwL#oZBnJ><@}mm8?m%&%3W3EV6Gyd>{~4nAK1;#V`h#7?l&M@ z2)y53~FA(o4@?CdYn zkM}q0XTw|tHXN49F|;auv}FWcxCo853j}@Yepd^Oq2H3}x#m9#N0936uoky?)y1Xz zEmAkR4XcO(zgYNiTeVv6C2r2g!gsZqPrtlma9BuaecGK+`d%UF(H>>DK#*OE0&{zJ zR2M7I(M?MIzD(C<{c`SejDXN@F}s$UzZdvh3(X$Ed%PR{2{AKOQoSSD{o`kT*DC~( zb7TQZc`xHh{pPbD^{UN9zj|>A(#>hp!U1-?T^hzR?x|E;`!B2uXX1?@IKUGoa8MQZ z#_qITppX%l;nO%5%wKa#;8>MTm7ZKKIk?X(-R48B+|}=uK}H>3mc%!oPsW5g{;st; z`vZhrFQffon|hhr_7j>t&hkkDS`SK_c6(EJvgL+1Uv{BX_T_G=Paj6sruvPsuwQz%I+o}G7=mv_dO{~ zBl%CECJhyXxva8~vL>xR_df4q$LgJS=x1=o`}XKVdt=ib3Vb9_)BPff4k-vCND?mM z%(=gyGY!6nQ7=5P2*>6~n{wAS;s{^h@GU<1-lZD+P;sP1;P>LKgQV5H;+ja^ zfopgCXua;50)c`hQPGJ_higuK>BMza*BC)EK`qC4eMbY@6hoql05l?)1sW%{I+lx= z@kLtK_XeLvd0X<;;Yb}C@vN-J60>#Jntsn@ncu{P$3mkyC03UY#%qy$MA-hrxq0|@ zcSaS2Spk=wQBlphR@n={bO6u5!)Crpx7*?95W?*D$UVXL?jxDrSJyomAZ)5Yug#Pd zhIua7XoOJM?tLD~ZiS~RGBgqm4%^T`9%t-Vsd7%Qzm_OpvZ>6Ek!$j#hYX92qc+m- z`T1XRl?x2}?)<6YnXG%FNCeaSr~g(;1DEE_84h7x?+MV&@5R@U!#UW8#@)xu{k+0m z*f*!@wT+7B8d@i=8@uLG5WG^+yALPv*4dX|$bT+{4PY6LKChgMC0OFJ{`{9en}n|JB~9-x>Bo<5Q!X}pGWhjaV0fcx>Xp^F02 z%=XfPpC9?oRM}@_7qZLJFZ{~`?MAg&P;6>dTBGoCG(j$_*J)HRf74egx=EA~@FU_r z0hjxUd5==lNH&ZN5UBmf!}+ORt|jZM!ufYVfjQX^v=Lg_w>1`yO_B;xb$6(j8UV)D z-O^LU&)($@Y4XhiKS_x{&>3{0eFvW}l4l2Xd{sq2C!U~!qv!Gzk5JvD`^@SzHM{Sj zYiV5Ya0`d;#-9q2A>NVM@|MpcKp}Ts-GqBl7a#j$QAM@WonZJJyXrvLtc8iR?>EmNf%fEQ5UswXXZ%%*80HxYIRCSA*8bPg(_h;p^ z!4Bxi!n~XqAA+nl-sE!1+3wB4S5jX48w;U|GHnOEMJFJCs4@-za6)dVtVhay#(rxT z&%x}vzgE~Ef~?o#De+1ysIJ=YNmQ2HCc(zvi`i5wFmOKU1F(O{0t>I-ymI!9V2Rz^ zc7qB)H|Nhf35?yc9tvU}ozf-pN*HTTsK9{!96I=tB7l?X##^W691MLN;npzn4=Y}B zN7wf$sf~AWX%F--jBqDhg*$otHsJ*@dmi6^vJ3M#ZAAh?c)uCZsx(UcS?CVi*_*w5 zygMnB`kN!;qtV2vIUy^M-SeP*+{u#v?G~-$>lHc%!YJZ*B|3nti{Lm1cc;~U-RXg5V*ltVIUj#n~imc7B{h$1rjH~H_#kYf~Dre?&P=$RlW zfB0jv30nJ^up1s4y3YE+oLNDa%|y}hcN_l%kK3!GVuYqz>%@Xi+2Pt_=SW{NU?N4b zw&CoITo4JmP%*_$My)a{ zOui;t&uI&83RBf0oFqCVt$f0DTq{sUK26)ii)8%MgP)Ndcgu?rX)C71uqD5?xd{~g zRS7B+nH*lZAqH7U!!PdPQXQve0@!2I^CjABU@?jW@>?&ZyRdTFL@T2ob-4dJ>l+K) z`VPs1FhIZ??rvgsZIY;!vM3Mm6E}&h@ezB2qM-A;O!i$2Qja_bN(#XP%5imKN zazj3-fB`{DH+|6P2f&;7!3`I9@N;&FhA|j$;v8k1gS?>(j0|fS3c1>YJkKbf^)(wR z*3!1ICu!4fp7OnjfT8c7+~$q9F}YdAfaBm>tr9OfOm#QrG`mJ6;2n@w2~|v{+Dd~D z#QV9ZB0-OyKAgT}Km)W!JQBhKpDW0vbd$|dcGB?P3EJyN@9}99viK;>yvF+=ng0UT zqNlR{q-#&d2uM3*`J&ckFa$IIg?(u1`b(D=+pb|n#BGfsaVB{@-|zlhRlpfjSOK6( z;d?!J-gjMerD<8ap{<4k1-#M8;w&6Zk6@b5|_IMlZ|4)K^fMq8Pw! zyK8a|zebcfm@*dqgnfk6#>N5B2ZQJSugR8m2@4&P{Shiolq=J`YS&l->f9{(-P4hF zwMu|vG2rfrJw3(FqhJRi=aWj;q7aaJ3h%sGU?X0xNEd98_r0|!1AS0mdzYNNxJXWC zErS4K-?8hp(J7}FzYvGuJ_C1aTTS7mM ze7~<|QFxp3;7E^v>mx9|IlZZvNSRrNSbhmqQH)lxYGSs1xo9`rCfQs2-K9l}+uCzm z|5vJbPjdQtT$_nJqJz!dVcwuMBv@0IqN2K zv2!3?H}7x6KYRpm6~3|7PB?(7WWe+1vU0En@o;Qd?*IyTGU!@9#eaXr@B#*6^d%u) z^%PzU=TXw0_m!FY1lJxLb>7&8NGG z!dDdEUd!1N>ovJ@Xq4+WD;KGX5Zk$0hZDqoUzv(bWHAa9mqIs4*8k_oN>)>qhsU$w z4#o0iw9|*HCY?+IAFV{zKd~MsU~E& z>bUjCCyr)zv{+;R$N#Eb#l=g5$x_nNJtdCI?ODc4O(^Z)SzZ$Mlp_P1E9~#x3%5Mq zFc{wrrVrVof?WqkEx75TIMTH|$N(LAbngXWW+E8l(_{0l!n+$JFA^QBU#d~`2bbr@SDfk8>Bte!* z(E``K0RMMDx?igdt@1ktFgqxOSv2Zat*;$S;SnuVrYS<@IK5i=(@`!)aad2Tj(~n> zO9ONno#21|)t}I|{T@B&M+$FEJlI=QO^90{PJ~+^=OjLex9lHB#ebu!-L2sJc@*XJ zj-B-Zzs{V7E}Jxn+hBRH_35Avwv+^tkA7~*zkIcXKASe?z8^=|o#S;SeRDDOK>PU} zrz>kX8+`lI$2|Ge*95oEkc#Is5b}cig%cVtp8*MBi7j10)Y^su(0NMyE?OQ=JF#7$8@wZ1d^UN?5f)Jf1o&lQvC zrV%Q7EN&2m5i1GvpXXfu`sw>ZAKs%f43Xu60A7hMIFjO;=u2aGUqaosq?8jNoy>hq|z!&_QnJ2&kpDm>m& zaH_e-sCnwt8(&}eY((LfQK|ZVysY^e6OKk2S3iSNdb=R-(;o*2K+-ohO**TlQBs%* zqEN-Ly{~J_rD8%pI6Xte-qd-8rbj>b)=GBqYUzGRA=PY`Lj+@nBr$Q5|2DHVS#2}? zdhR{&I^O)W1$?S|as1jZVUdT9_p$Lfd*AYLT!^l)_QpZH%$M+oryPcOt%T`Mp2++$ z!yK_VNtk-|J9=tQH)``IJNq@eX{45OC-6UYvEiZ_q7yBK zV!sA5X~yu~H^%|ZAKCBG{NBq>9=h!u)($_uqq?RtD5Ga^p33{sLWT5}k9=%2Wo!MV zMg_gvcHSlg!_%c*j)U|Z9OzGjD7sIr`nX{{XBzc+5D|BOZmDV2!D+vB z+xwa$rj?_&Qn8Rn$1*P>xzpveMPkl19X1&0ca!(S?o#GDkA-j|7`no2`MB(lwSAbb z5^T2#HBT%g<@}SFi!Qn3IrVJ|Wv0urR#$ZnP8Sh*Pxrg4PtI#kdpk~*rN;toq7>If zSm2;LpRBr`jKbGe1k7+@3AT_9NYe9u1x1>5`N6_)3z#%mzgwd6Z=)5#2vl2ib`LSV zZj-eiXNVCv5~_CgZk5z>8$Y@@h$l!bEoHR7>bO^V5kR&dtwzKoacQr7twA&_khnmK z&;oOAtjhaa_9TxIDWJUTf{VxTNqfejBYpNMi$w}=5Kb!gZ4#1qcWA>yxT5?^R!apl<^3jqAN_GkMvArKr1`K+a9xU z)jCK0xdK@5Qgrf~sE`7Vk??%*{OWL9kiP7tLIvr;_vA=~ap-@dw}WKUJIag=Ezi4_ z2ShM`^w5k42Ej4lp+}7uAIi7F|M}0=@!t` z9ZNjVpt1;auPnRqUfhxEO+= z8!{MydayiuNheGB_(e1H;pebjiWu^1d@yh#*A;mLoamq9*_H7XYmbT@#n}y>9k|$2 zR1w|vi2x;cNLJ-+`b?q>bq_vJFkplA+2kDR(y8m%uGoki_$k@k-+Vq_={!B)7C+-< zo=}FnU3->ux0Z4Be%f=3XA!~J3DqW8shRo^4sffT-@>3ImcL{8B(jzuzb5o?t&ZU6 zV&$s0?Br02_?1E?_40iS=z&o*K@=cN5P_OUFI=iQ(;;)^%!pv=>U7$YKxmxXv~lec zo`Z<%;pfBBH;MNc;_)w_PDuey+c4$Z{1C~emKCQLW*SR}9Xx452j(~0&E)%1m$l$4 zWQF;wcfQ*EsGC_|rQNa6+Lm=9!ZZvM=~vhl&p@2Jxb^H1<4}Ox=>gqI*RKrIc;z5l z?eAE>)B2cuwpi-+9&;%+xJ=`bpiZA~e|mXF5~gf;Cag5g4;>}tZU+7!3^{@WomT*9 z_jphWkK`cOk|@kRAq_WCbYd;eD-LZ(eoY5DWF=GAks^p<-BaptsiqBAE=*|i;_1!e z2w8~4CR^04$9yzSAIxj+C=o9-j4zm+>0lUpVLRe!@bri8koH#=CDPl44E%Vtg*I7& zbF`-XP+>UPcPjNm7U#nj_rhx;;ar5ZM}M!Q2hFfCk%X%IFq8ImAYmwEeBb`aVFV7_ z53SQ2(tRv(952gz(UCw%{D!Oi`)FVc!Pp;RtF|%m4{a-xvV@%$*)Ia5UzMNYzyVbX zyGwugL}jg(d34Q@z$q&stjb=<+Zds%EKjZ6SW zEo=M?l`o9@z04|6t%@I_@LkDEeIh^r&U);cMi$&yaSpWqj1o9K~|z~k1`+RkM!+zpBCz|2t_ai$!YGW&lLtU?wtmw^|DRX zTRC5%VrwjDeRCJS6DY;=CBL`z%bMyMeS`E{s!VZk=P5LKsKE;Ev+Ym82X3CxNObpjTlqp^25HtOO*LcU%X)dheSp7VJaY63R4t@8zh{3~ zU8?h;5k_MN$&aS0jPxIy78jo;EUl#jca4P?Et7_bD%GdXB6HgZUV}!w>=q`|^*N{3 z(*g2m#NR()L)psYvH+cjHeTlXc z`4Sl(I#BU{CESWJ_Sj?)gCN42#|WJKIU8B888pw)(b13ah=}I#-hM3C|AkdNOhJr; z44rB|y?Wun#UfvOPC{8^Bx-l7dx)iroyzD#P{v2gCnGL6n zJO_IiFzoDR)!^G7gwzqt$u!cr>;?_8YKSk20!WOPmLOubcK6%?R$FcXTc57fcp zGYsyW@KT>twPi>z`O*FUkQ$BtIb`h!Mw1Oh%EAI>)GnX(I?emH4?QQhztgKaD*M07n;i$UtLX%sOn~YH$CZtiGK)#{VA^RxAjUsbDh zE&Y*5?@i*n?cWUPeg`Q|$AO-&o&=$&Om`2Rm0>C_Q34)kTL~L^Lq9IzCgJN6p1HT& zJmAOV78hxlVi#%Gy!rgx{MC;l--as7T+OLVoyRyV|I`wMQ#Z4R93Us|>Cs1fm1Wrq z`%Lfl7fo*}b);pO#QX0b{krM33>xk3N6{)XE$Lp)egYK7w}#_~Vkb=Il06@FQJ_`S z<&C0JE`pDj&(mT*?g)2~nGxhGC1Ha^BD9!Pe2YpSA30 zWi1jrSL}<|E5w)kR4-nPt+zeN=S*K7cSN(=Y6~^EpU80*T2le`NLaMh6=65S>Aups z_~~TX2*Ympk6(CSep+gIJbgLF0+SLMfv`snPlh(XXlATfm=_N4AG-@pkR5q1i|h!j zcwG2hc)F>hwCC@fx~BiqUFrycU!#1N-)s${#^MqJ#Y2Ag*L}uwU_vPNQ_f5ED=yR9 zg~l4=>^?BiHRwjx&}sPA&HWVf1Dg>BPtd;hpw+6-ZHg#-17=5g8K2k1l2NUcNcQpp zSI_#>fta7_qyjROVQTy^>HC%)IiO>awh0S&r1r#4Z1`?6dZjryzY`7U`t{suYoc>^LDf>~#**p~ME4rXM1Bf*{A2{uf zYd)vkw}*RWb(Ew>e=j2=NZxAI4t$TLR_lFyKw%gL2@;W*(ygZP7|Ecq2EDv4jN*JbIH68tmI8#wzObLj3>zUDA_0Ob2wK8*B)ci=-?p6>6 z`;fv7g$ToN(}0;#Y0J9F?;z@>SnVmDJc7U9tgwwYW)vv({2{w%PAIPvN!>2lE{wdq z&@nOVih{4f|Db? ztgNOV^eh%`8EG^s^ZT1RJo@4p3it(6>Yhp9C)F*_)zFAOuM`ltUms3acoFQYH!Z|^ zD(@1$*fK{u;<*w8Gg@n-v@@C;gu|fu1EQZlOlalu$>VW{25?s(t9U;Lb*4Q=HO9p-8~KFoKBq`IV2U#{fix7zt$_&Kv@or!)$op{#B=FIJI6jB{T8#@6@|L8>Kr)xAkMGq2cW*3poh1|p zFcat}b~vCcbH)OU;WQ?yQVx}uHI;sf=epabh~W}y7g8kaJB2lL~r=zT8=i=Cqz4%;}bnrHF(e)q3y_UGL*St!H8D z+os6lXYk|fisCj&fG|qh36Q>2OHWV zxV*2)X&Ei~{Tdu|zvrFpR|(`gZCTCvK6<2k2A^%Y{YXQZuVs+rFm>0gN7vz>zglW? zYqh+-bzr8du~IWaZ+{2On%Ox%_+SCyrWf>ie6McVwgm{LgqzNYKrAU%=#e`ojhLkI z&ZYl54P%q*;HM`svQP5n=+~$YqkldLk@memDp+pBz_g2C69nI%0=&M@0%NTauu-Ju zmg}dQ|4FPu`38BHFEIFZnmgAYmSoO@?+m&TFl6x_dnIu?>7Ql@IE#%M2Yce^sAU!! zIbwVenc#zUpY9jEP85sP4JHl_L3aKt{N5a=U0NnVz(m8}1)H%=+l_+^LNs#yX4e+a zU!}v_j~!zpLg*mRN#b)3gDm{|0&r|p@;8Gzbf4i5ANaluY|t-v5NP50>eW$Uj(r_w zR=*MqDGU?FJA8qi#xAf_w{+-Cyw~r50|>o_*4>7e4?vQ<&g+X<-r}s^KK8IoU5S~t zM6cHCtmS#6!W)Nm|JKib`=^uNjG%}E>s7fzx@&K%m>X_|w!5@B(ZMW797xTtTlSa> z<6VpKb8y$k&>imiG7?4hp(!B85x)uKJ1VyFunEMK4BtJt^&S?;ES!^jJ~Qej_fp;% z0fa>Yc=qx^6F~V42R62z(v(PQx7oRTp-R#6>|(J-J(gI}Df1$B#GmB`uI`2<#An9? zJ02$-gG;dPrnjhSMk#*##+5cEv}&qLb^9Z1H{bNrQ)6vbbXt7Tfr=0AG~4gLe3?>Q z{JOZn-eq}Um|E&aAgG<)jOi>lBIkG7E6>OTm-gB)k$F8tC+p3wsF5qfYoueTxg&y-{4Tv2?N_pd!E=QH0CzcxJuq+j(B8!nSugd7t(osQHLD1$^q-;&GCcHQ%-=HNrp;ejP;20g zNgulex2RqdXH8J`Mh8y+tbTCUJ8{F@SSk;)#nms~;Z(0j__?v`1jBCU;NMCF;z%x! zg*ChqF03<1!k?(q`;w!5)<3E}C8Obx5E_Ys4cVAT^6(%m4=0QZ!~VB(7ybS37#9+>r=(%Qga@n1p7^=h z0tA`0VT8>B!R(0UiN-o>+v6YBy7rT1!+!k>58LMDzKQ^==LdbGk90HkUQ#oHhLzUp zEq^X5@k9mq>Z}u5uz&Vm9y40DC!9T1`QIp}yGX&(q%`U29>tw3v6+0fZjAd+05Vqj zIjX_`yoLCJPewZpY07Yc`L^dw3IQQ+%>-7~#wU0U+E`tnDm63b_jNz5R*tibJAu8Y zX;s$4>DG4UZosONBZrO{4GbUvnN13qjO<^xGB6oH6bwB;0R}iwwBQ^dsyN-B0Wi}` zEkyoG;j@uwp+xh{O7NioGC$)UDFA14X+P(W_jQQJvp5?Z(K%($lt&vj5OXet7-R%c zG)+63_W&+n$W8$dy+~Zg1K^>?utq*qG|#Ftw6KfBoM$Z=C-bBk$Xy_aRr+sa+=hAF zw>^3$tKCI_H;C2A`M@%$9&lseDmaT2dg;+(AC~vWTwSQD0w8LrDW$XkWRRhMw8e&U z$$pUtXcpw6ROGDM)Tvy!TW5-L^(E-p$|YENb*y!(y^o_c(Mf-LxT-%tTu=>-=jt}H zfzW>#zD*Q^Z%;UKkx%7SFZuSBL$c21n}bgq2+tR&&`GOs({n%UHVxqxvJbzvDt?k&)DHXAfKAGFBanNB^ zAuirRx8|w0eov1t^yS1G8G%w{Z&UX#K5+U05a^MvlgwZdc`saEnj@Y znIsU_zm#e4icy>SPryvQZf}f)$#T2xSCjtu?+Z;l>EL}i%LA>L@=CU+I``R6c`@GI z)5EvXbmZDgXcrcLcWAZTDF2V$SvdwF!Mkrvf*X#({HcTx{kq7+vo&9vrnM2q2ojy2 zf}rjRMmQN2nfAy@V7k)er}MTw6S%CGHS6pz_dgYi4kdF%uTlHHVv1%!{XD4RRG+E!-f*+^-G%H-EmRC%7IYHAXbuY>F11ioy|a6k5>%7^v>- zMXD|Pr}OQ0Z3_jz6~Jiwr~gmD{eZ|BlqgM1Tpk=nU+n2!)VEa#{{HKU1svz4Uly)i z9;O~mG?ZLcIQq_)*|^*{x{UO8QHDXFd#Yu+BU_%(iWWpt>)*G%^ck_IH(SX$qCumh z)fV{#NP@1`K~{uez9*{^%Bpa*TXS|yZZ=}5*st&$WSnI|xsW!f?C`KP_dYgf)SfPA zm4Xfa`yAZ`Wrm&Tu-e175Ai^^B0ayb6w;|hc+4-!1AqG`T0Bz36y)3W#$|KlJe_Qd ze2P;@tE`fVBh%#lAvfR2gPqVwAEhf3yx?yM3jk2i)#2` zz{zn;j;pWbDp=;>mcwMV6Gkv~?%!*22iHsm@zCqA2atTH!Uj;unDidA_M9pVgC@AY zOgxzzxwk6iO;&>Ewlp%-FVFvWmnf$zvAsT?1VJL^S@V|^Y~9RLHzBAx6nQf1+MO+x zb>$k?>DDuJHi@rQZ646sC2tC5y-_$oD`FIOh`&QfFxOogPi#B5VaWcSgkY+U0StuP zXtH{}#CztaG5}-g&nKHMm!MRr@B^7K`!dsM*+ntL&rEa6s<+rl5x9@#@qlnn4iixU zgu}((%Nts9k7d!{A817O?4l=lz7jiUH%EZs_Ti;5!)K}q!#m0M#1&2#4FHeX_(Vul zd>D&-d)I9uIXuwSwrjOuJiKK!zSW^eSvZ^~4mjm5*ElwXu7p7{%t*;<(2js*w#~<1 z4$>}SKmGG~l=AF!I+<4UfPVS8zlr+=a@CzwiuU@sLZiD zdhrWaLJLpZ0;k<3w1O79>Fy_BJV0TY0u6^mt-%9nZMOF=qHwm!GaYnxleUK3ZZLnT zH+R7h_ZB>=*W%2Acx3g*o53@B$Lhx?oD=5{ziUhfm1~IKLe-WJsB+HOyT3igSGJON z!e2%GxK8qHkn`hgI`e9*&EwG@=<6KwQ3CeO3OJI*2j$Jft419moXElvuc3xabsP_m zU7;l{FU@|)p_)+wHglYDFtEH$zeSmynZLU`jU?Y_oKJ7ZP%=sHO}gn|SC(rQ{+gAO z-m-|mZL&wxt^L(-FmyCnbMVhDy+ghzaLMC4q__T(H(xNz-GH;k0WJY+)SQ`4ds7HB z*dO6*DYLE;lUnI_&sZ#_rQNQfxf=~K;5J8B5~e&kYG{lwEe#I1`RlrMbvdg#Y_3Ap zI`5Wo1r(=Xy1|rVYpxYnKYOj61t5gA;9yB<0>~aCx!*PZ=0c+{WHRLx7M{7}wcOuqw# zFYSAwEBv1#YqDfZnQ#+HVq0cFw;mLodTP&D>$?7XzR0Ya7W=3F?35XwStoaBQk|%k zD?PP-_J869A$iyuN6C4xUkP&_7{cdx#Ta%ixgAF6fBpcW!e@YJT){Iwsdr>P^4Id* zl%AcD5g6fs?SP*-^Wu<4Y*K?mSoit%$a|AHaq;;y`lmDyo!X+XO}P%gU?Uq9_DMu# zEP@Aarn;J~*tt28kcBmO1izqD`x-s0f77QDrzN6&D5+D8e|+Gh_8J>8pB9jdFy&ZD zn$TvrZ9pg1%-V$9f_Es*AsW-wc!83R4mMNT&No-DBnsP|(a@h)h8$NYgm~~!?6wMD zgn4C*WBc-UPAUO0;Iw2aG5`+HYt2J59INF6Qs?pzW zT`%etotRvm+RFWJ(t+tg3M-D}!iE1DAcZ1qN%dLm`j7ed1p%@JX)ivWq`N??v`tGE zlFv78`o~(e*7*d)o(MrGxF1eVRV|PH*sgMNGCzTfhpkt0@TVn5DB-iM#^~*VNEKw~ zYcha$;*UY@m83GKn)~xH-HV6CmNS#3R(Qp%&cR+!xWn)0 zb3ATu=UM+A9X|K}=*^W%V@>=0e|sB-_CZcfSh)i=nd^i$*SpCWMp*`%ofZC9f7`_K z&ST;4-!Yr>IjjOxV9*w>N*9?K-J#TEZ;+>UHCm>JIM%yVyy?G=a&?Wp8qHD|Ch*oS;SN>&_!E^=FZ&m%6$iEVXc9>UuRaa7bAaJ67RuBJXo) zN~Li%qkKT+u-0k!yuh#*eXfW{D~#AU$|u46)PmR4)zDSDJQcD$M_=Sxozxlr{LU2t z`Yss3d;4%JgX?{HpMikzuSz2J&)x!W0r0|^9NuU8zs29rdY>pAFQ82BQ+O~KozJM{ zfw43)(ES`xBLlt9x62F&XUxPDXav#-On%6C-aE*^p402U*N>u}%||gwG*$oZA5b@x z(%Xr%P3lt}0m5(kM&Pwn@MaP#B+^ep4&I+9hnWjw^XKpV44tOM1Zz>QCipL}>G8^b zM*Pi-JvPmJV^?P5TKZo>&-m4kG*MjOgQHn3W5B}0T!|mE%dUQnyOOhXd$M{&BJ)Wg~~x&%zo&KZHe~nhWKnK^&itFP$AO!Rh9# z>(*~?i9-RP$OUu%aLMuk_QMzd7iXCsrb&@cekZmk2?bXTYK1azV{Zf7nFo*%K^x{W;L0dVC&ieL+)+{xd8 z*MQy;SILR4-Q>@UY7z!7pw~|dZ-vw5P~ITWN5{TrE-1LU;lJIfD*x+FxJ>LB>YGa9 zvZMC`W@LcT#^6E+5%(6lLWPB}_Y+`>F=v&#iAVSOYe8lOUi0A!neJD7*^<>v*Wp8w zvKl&c1(a#61*S<}=B^KVpt@acxP5Br&;HH))Xy5;yamr{9N;Ld9JB}@zWsm3KlUQ@ zdaVl4cYAW(BPFA71_RKkB!v7i5OI48;8z3}x@t_Z*AsHdCp-f(UM1s1*@VisJP+ui)T3!<`r;yilwD3;FVn{lPuEf+qt$eUp7v^(av5{u=K-SJ8LMD zvvQMfx-h2!7V!=2UK2SEx1RiGvAC2bvPtD%7BF!d)jcl~trEZE|0DKv3;=6JL|}Rt zK?1`ne-_`V=-Ceo8Ck!xx}pAbYfdh^*_N(F30#XMd)Vfi+i=@q?bH-nBuxOq6m0rPXvhVG`RYgZ3Qgv>3V7&F4+#kHHpI_ zL(`FkJhr?T~oFxl92hWQ+>Vwiy=D%qNs4L(~A|bSV%5G#dvULMJX=L&-Pl1$5z^hgj zr77W^gHxqX*vUt`^aUjk_bO=1!o%;gZgpe?dzT|xj<#1AGTvhi`r)|HZRw#{`vqN_@(Iq2?xeC{IuX4}l8b0hj_5^#Lc-YlB z{BKx1cHdMllzul`ZMt<1F4Sj9;QBH9-|FH_%S+Ar1@7nF7BF|` zVLP68-lkS#jp<|HCiP_ri;5cj`SV8y z&74ugmxI%fJalkQc-8iZ;-tv148c2b`tK5f`g4h(`Swzk+3>bOM=<5;V^2HfF0c#P zh1-?vjiD?W-L3ki?x+!`+P0_D^D2lyFY#=7ZEGf~QUMkP8Tl&|Lqbwga;23_-gp_y z1#p3Jfw*Lwk7R9_U(D!#xH%QjL2vBFR9m;Zo(j=@;4Eh`i9`q{k+!$DH=0Kme<6U) zY9GoAZG`grH-36%LaT4BnQ5k50^-1 zBX%MQV9gWa*NYPi>jBIR0r&^X;E2-%5%eB^1e1@mBvb8>_M_~rlKImUv0-vnj z0(dx!B^Bthp=3yJzq}p7d~6K`=tG?XZ5GzdW4=&|gJK0S%p)X*68!uAsW88Hl>x2l zhe&3-c%WA0rI>DbID3R6HzHG6P{42e+c%(uBJ;n+Ih_QZx#ws@AOCivK45@jepnw> z7dDb}gRu_|2+Sk}r70=lI1oS>P-h2~E1<*;tRDr-J>kIG&F4Z=WKd-TCj#?aRC-Uu zW!{`~!UfXcg(q*}q2Ns0|9z4HfM5CleDoavegW?Jk%0eyU#9qvsiW#4&vV4Y`>&CK z6-*M(b3{V@k9E(p7T5oe9bg*w&zgU8_3d%HGv!!6q1JT*R@W3~XBuGV%lYuTOPIvO%B$!Wl2x z4Yt(Vt>Y0yFcOj7Q>FPRs=^c~f}n3nOf`&&*NEQ)S)heL#YU@POS#!)5GdA&GsB-- zUi~k{g0b+kKpS)?1lnbPu`3gU`c8MASQdutxs;VP3ZAS``+Az!Ww#m$+`M2_u;^fx z#JBjdB&j!=&+99OM;i$KQms7>wmz<`tPp?x{FzV;4*4~`dcbRNjpRf>>F_Y>*=SNW zk&@8teQtWMy(n4wt8QXrwtte7e7)t5)%sCCwfXlRdQ50&iRV5@$Cx=A8yn+@0|GE+ zOi*wh1si6vTfL2^HpVWwjFqKlR+R?#$(0T}xRn+Y9y8VVbTZx!>BU~|@x`T+I;;Ks zWZil?^kBOCG8{Xx0D=LYd=1Yhl_=a_Y+>$vq7s`ym0PZH~ zppzvZJv|MrrZVdkuUWdaqt&co<3ZvF%1m9-uORY37P3zTAU2{Y|1TCFPqmfRWa52I z=|R&y9VLYD2*1-FM7d!2{hQsG@Z|y%88g~e}J-kS8`w{V?nDGpHf9E#T|MK>z4ZG6oO1r`P1__M? z+_IHzfcA8S=;YM)I?GTS#b%%^5R9H;)5KKySx|fTW>N5w`xCEoJr_PmEV}>1iw1F~ ze>mahAbE~%i~i0;Q8??dYj=u3lkO?l=JyaM2ss7?@6Q#mBxT8q!_Q|3GITXGFSs{e zcVveakj7kCoUD4I_bfaw)m8;7*|t{m(rpJYvQLKiDp;R0i7lB}g!jpuZvBaDFHSG# z`b|JMkz}~Saf8Cdcx;b^49aE}AwA}#A@Jp{X4JC`T&F$$kaB^XSZlmCHXV52=tVKZ z($HEBBIBc(4if}p zq)&LErQ3XG)Y0rAc7y8&1J|CLGrsj;LgXH>QfEM7Wc7Yna8Bv=++xc?sHG0-<-QRo z0s=EBI9K*7zvZVMcDq4Qw<=i2_y#2Rzn8TwZk{wef_V6j)3nasXLQw~Gov=ygvA(Q zKGXhci{ZXspTFq{AXcpj2rvy16AOrgg;X@pfyTofZr@6W>_$o5YpOZBts$=Q8yWy^ z1rdUgK)pIEtGh!1^dS9y@Mv@u?>t~Nd9VESNYDF(#$u|pV2=&;eU0TS<$dBeSqNyB zbi;KZ-dG6&I#a&SOg#v+$iz}zs_BMMTbDo+++8SVgd7W3Lr!WTz|ean$_jsX;nU8rm@yiQngZn z6$U!6W#I%9DoZ|354I-4&lL15!W#Tq_K{k>y$C-0_L~IiZ)Y7pR-RZ*zBUb&c{NNF zsVN5&=rXsSZQg@qbJfC8H|bT+AQ!IU=Rb$T*3FGKUd&+9GP~{2{3hLN=GNhEO_0V<{Ebd?>v`pxai&bhy}(o`9;4W3pmar zY5!@m#oB^+eAwg=L#M`gvyt$9kt~d$dH$K?7R3PT?;1s!kv#P0fxu76%qucuFtg9t z^H3x+qNw2QQ`g@8s`eEQ^l3XL)Et78OBntRNi7N zF_!GIW?D=%i6qOUkSvLaL?qiVMhF?SXpu}x_N6S@$-YfB$dX-6mMk;2F(Ko7PJQ3| zd%yY3AM=}Y&U4N@bIyHT&wbt3y@&dpu(M?u!e-+w6 zV7SMTk2Ktn_Zo?=k^po5rLSW79X{$*YW%nuirvcC)|ep9*9zlpNI+aN+%zpx3c6UC z0GB!EKI;ubl5@{jUa7y0ZUZ)N99fRrcrm2d<*UZ!rZoE#0Dmj0@;*4XzYry6-X8OhMj@$QMS`im{pzwAdhWhKO*OtQn%ex2Q)1!e; z*F7hds+5a~tA3)-a^ROz939`iKK-aj!^hdH-#0&13AF`wjE5l8k8@OCi5~yx zwD5&qF-LBs+XVgGA&zM<+m%GvJObJ2O|WtC@yYSg|RnG*-KR!np-MF!zsl2`_ zs3MYeqYvo0NnHB7*s?I-?lhj~FFL#`YT-oxoLpyGkl$qo`Xtc7Oc#0tkdMTvPq&KW z%>&~WJeZ7oTzi1LGaNu;&Zz1)cn}36{Er4MX%@`w4S3b&9_Alwz74B<2nc1O+4V*a zpS;Q>xFNadRRQju`{6*Kqbtzi2BQJBJ9TZ-uu9YOb=KdIBW*Sqp&-NG_eKixoPm5M zVe^?rkgvpkUOej)8UudEZtaE&6bdQdvI%MorUv8hA%hTZ`+lawcIk8T!bTCJdwNdu zn>r*P;2@&I`mH?jKPBS=$B~J@Kz+!ueaoydFAC%+4y?;Gdt)qnAR8p43DLc@BbKa7 z22CFd6I4~hK*Y|xCXAO$-KceG#VZO$6rg0*tvRrPyYB2&vj2t$&wT<%DwV6Gq9wfO z`l7;^3;bZxUSGQj{=v0L?~dCrRD=1c<))voAeHGj)WrF*c(Pv5j$fc(iBvcOrZc?h zHZbsW_dxB^!ye(S35WLe1-S{mOt@A&92=3XMkJ|+U!llm1Y~m1IMyk6fEx==aP!#u z61vLKHfxPMOceEoR3fX=+&*db{~{Wu1CVg@ZOmL!5XVkv4u(xP->xVc|CnK z(@_dUxBHw3Jt{x;uKXx44PFj#LiV4tFueM00hF_WTDl^>kE@bK-~n(BgWUt`JivBj zz)1jG2l*=A235rPT&~4=Cse!Mx8HIxpx!c^Nqb;YZ+~a198nMWWXK`6KtX9L>;@n4 zwMy0LV31V!j5%85{^*O*n$cfZq$=3AQ7$z>Z^_fK`VLa*pF+e?E%= zUtT;MtQr1X0z~n^+XP!nT-@XoFA12gzy*Fr@@9bHn6s=>7u(r$r$m?q|0Jx{WHxYzJh=ga+2vyn9@ zK^~9Bix=bl(7$4Zbl;F~HQ#-5mKVlu^}4&%mZKpKpwg{R*>-jQq8=cqCEHD}#oZ%2+nNpceMldBd1G$%2eY_8cNR3D*&1{~*TXpy!0 z@T%NpS%B2du|nP>$>{zl@7wA#WABUk_6<_@+WZ)bi!b+Ie$-C8u73C9)~u7 zdZws_2&d&ruP-k~7nZr*EVH7nLv;<3LM!L;$jy0T zWu9@kuVM~d<29^rHG=#)(ulGvlsg?yhcF2nm^87@6ZM43fTYOJlT-;gh-Wfyj0VbS zQ#!t!S_!7tpwB$2Qg?=y!V;j71gE#1R%zgJOAf;l=;%7yTBlMLI!WAL+$DUe#);(v z6ACul>MCv~_trtutfKRGBN%Y_EzGR@E&hP`Es(_1LpJcvo9k9J1j~`=0b#jfpQb{< zk5(?gO1)mBHyj(KZ+$ky_twxsUzydwVTLe``=Oj}8ulotH@&%Iq4F=HI0vYtdjk5{ zXi++>r$Cb$2+Ozas4@9Qb12*=p8*4r<}bJ&+SY63YRPmrZ3`kdSP>wsmx@Ka8{~=G zZTAa^6@HN%zUq29R;*v+n1=Ait!XaMo@Z$9frf*-xa+qVwW3cxh_3pE9Hk-N?4fN( z+E)8aJng5tyF4dRFQ1P`VJ{k}N8oxe_PJZ${79EgWQ57eMsLi9!L-rNM@Eb@`=cnJl2Lsx(K4TY_Un^8d8d&DX{~7QmtVfL+h5_ufj~zDUQ+g& zY&K|Pq;*{+r;^ngpMT0F>(V(9t*m^k==wOhu-<0A*zbDDcCJ))t9%>NgSNrCHz#=y zs`1h8SZh{0Y55?}G^KWxGq2S(o?x*jlmE(Y@pMtkD`1dcMI%e;=}!*WoiT`?OUVAIR^_?`82^MmnKvzj|nMRS~pkbv!ig~YEpgq5}amM5@NkEWT3E*WUWRXe}2fD z*gB;?TAWlE(OJFH{n>q?PadW=d5FJ8Af)qfF~!;pAL-=SR|Uenz9LpHwb%HxngP)9 z-Dce`%!eD~_%Dydk<@#LE7%Yn7&%MaxDRu&xDesM=o$*X=|H8im0c!yRm*{?^z(6B zO)1e1`2fF&On%1j2b2wTx4O!HP9r68pWgLD8Rpy~aGSev>SOJ?HBUP_Y}^0iLy#VHXYy+ZvcAPI^6jdLKgkqwuzl_HhlLS6ZRTO(ZZq5e|2VzfbpEUZu+H_efF} z2;$%A(C+_W9E8BpVv;b|43qP5VKSUCSuB9KQ24Md*Q<4qu=y1!iy#YN-|0IFqX{`e#S`JFCW829bINF_qzyu<)0~&QQv`N7^(vo? tFt2`yVU2$fTaCTu#t$V5|GdW*L(>XAIJDiZy95I-qm!ok1=vfs{{s@-2*LmW diff --git a/docs/source/images/bprogram-running.puml b/docs/source/images/bprogram-running.puml index f50a2ad5..5d535dc4 100644 --- a/docs/source/images/bprogram-running.puml +++ b/docs/source/images/bprogram-running.puml @@ -9,7 +9,7 @@ class BProgramRunner { abstract class BProgram { - source - + isDaemon:boolean + + isWaitForExternalEvents:boolean + globalScope enqueueExternalEvent(e) diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxy.java index c72674e1..4109ea4b 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/BProgramJsProxy.java @@ -274,11 +274,11 @@ public BEvent enqueueExternalEvent( BEvent evt ) { * @param newDaemonMode {@code true} for making {@code this} a daemon; * {@code false} otherwise. */ - public void setDaemonMode( boolean newDaemonMode ) { + public void setWaitForExternalEvents( boolean newDaemonMode ) { program.setWaitForExternalEvents( newDaemonMode ); } - public boolean isDaemonMode() { + public boolean isWaitForExternalEvents() { return program.isWaitForExternalEvents(); } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/examples/ExternalEventsDaemonTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/examples/ExternalEventsDaemonTest.java index 1c520b51..0df31aa3 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/examples/ExternalEventsDaemonTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/examples/ExternalEventsDaemonTest.java @@ -36,7 +36,7 @@ public void superStepTest() throws InterruptedException { sut.run(); - assertTrue( sut.getBProgram().getFromGlobalScope("internalDaemonMode", Boolean.class).get() ); + assertTrue( sut.getBProgram().getFromGlobalScope("internalWaitForExternalEvents", Boolean.class).get() ); eventLogger.getEvents().forEach(e->System.out.println(e) ); diff --git a/src/test/resources/ExternalEventsDaemon.js b/src/test/resources/ExternalEventsDaemon.js index 6ae9f85a..56f9ec18 100644 --- a/src/test/resources/ExternalEventsDaemon.js +++ b/src/test/resources/ExternalEventsDaemon.js @@ -2,7 +2,7 @@ // Waits for three external events, handle each one. Then quits. -bp.setDaemonMode( true ); +bp.setWaitForExternalEvents( true ); var in1a = bp.Event("in1a"); var in1b = bp.Event("in1b"); @@ -14,7 +14,7 @@ bp.registerBThread("handler", function() { bp.sync( {request:in1a} ); bp.sync( {request:in1b} ); } - bp.setDaemonMode( false ); + bp.setWaitForExternalEvents( false ); }); -var internalDaemonMode = bp.isDaemonMode(); \ No newline at end of file +var internalWaitForExternalEvents = bp.isWaitForExternalEvents(); \ No newline at end of file From c85ced95cf764ff020b7638ea557572695d5f583 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Mon, 4 Feb 2019 00:16:01 +0200 Subject: [PATCH 04/11] Tips is now part of the docs (closes #73) --- README.md | 1 + docs/bpjs-tips.md | 88 ----------------------------------- docs/source/index.rst | 1 + docs/source/tips.rst | 106 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 108 insertions(+), 88 deletions(-) delete mode 100644 docs/bpjs-tips.md create mode 100644 docs/source/tips.rst diff --git a/README.md b/README.md index 330bf370..3f07fee1 100644 --- a/README.md +++ b/README.md @@ -47,6 +47,7 @@ a link to this page somewhere in the documentation/system about section. ### 2019-01-19 * :sparkles: More tests. * :arrow_up: `BriefPrintDfsVerifierListener` => `PrintDfsVerifierListener`, so that it's consistent with `PrintBProgramRunnerListener`. +* :arrow_up: Incorporated the "BPjs Tips" file to the central documentation. ### 2019-02-03 * :arrow_up: `VisitedStateStore` now stores *states*, not DFS nodes. So it's more reusable that way. diff --git a/docs/bpjs-tips.md b/docs/bpjs-tips.md deleted file mode 100644 index 6b78390a..00000000 --- a/docs/bpjs-tips.md +++ /dev/null @@ -1,88 +0,0 @@ -# BPjs tips -Mainly for commands that are useful, but not in frequent use. - -## Build jar with tests -Useful for running long verifications outside of NetBeans - -``` -mvn jar:test-jar -``` - -NOTE: The build must use jdk8 for now. Execution can be done on any jdk (at least, worked for us with jdk11). - - -## Running verifications that live in the tests directory from the terminal -to run the actual test, also build the uber-jar: - -``` -mvn package -P uber-jar -``` - -Now both live in the `target` directory. You can now run the test using Java, as usual, with both jars in the `-cp` parameter: - -``` -java -cp target/BPjs-0.9.2-SNAPSHOT.uber.jar:target/BPjs-0.9.2-SNAPSHOT-tests.jar il.ac.bgu.cs.bp.bpjs.TicTacToe.TicTacToeVerMain -``` - -## Event comparison -Better to use non-strict JavaScript object comparison for now. So prefer - -```javascript - var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)}); - if ( evt.name == ADD_WETS.name ) { - ... -``` - -over - -```javascript - var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)}); - if ( evt === ADD_WETS ) { - ... -``` - -as the latter may return a false negative, especially during verification. - -## Implementing Custom Events and Using Custom Objects as Event Data - -ALWAYS make sure that you have state-based, meaningful `equals()` and `hashCode()`. Or verification fails. - -## State minimization -(yes, this is informed by the "data minimization" directive of privacy by design) -It's better to store least amount of data. E.g. in the fruitRatio.js file, this verison of the b-threads yields three states: - -```JavaScript -bp.registerBThread( "RaspberryAdder", function(){ - var fruitIndex=0; - while (true) { - var evt = null; - if ( fruitIndex > 0 ) { - evt = bp.hot(true).sync({request:ADD_RASPB, - waitFor:ADD_FRUIT}); - } else { - evt = bp.sync({waitFor:ADD_FRUIT}); - } - fruitIndex = fruitIndex + - evt.data.blueberries-evt.data.raspberries; - } -}); -``` - -Where this version yields 4: -```JavaScript -bp.registerBThread( "RaspberryAdder", function(){ - var fruitIndex=0; - var evt = null; - while (true) { - if ( fruitIndex > 0 ) { - evt = bp.hot(true).sync({request:ADD_RASPB, - waitFor:ADD_FRUIT}); - } else { - evt = bp.sync({waitFor:ADD_FRUIT}); - } - fruitIndex = fruitIndex + - evt.data.blueberries-evt.data.raspberries; - } -}); -``` -That's because the former does not store the event from the previous iteration. \ No newline at end of file diff --git a/docs/source/index.rst b/docs/source/index.rst index ed077d93..2f5b1e29 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -46,6 +46,7 @@ Topics: extendBPjs/index glossary examples + tips diff --git a/docs/source/tips.rst b/docs/source/tips.rst new file mode 100644 index 00000000..31d30165 --- /dev/null +++ b/docs/source/tips.rst @@ -0,0 +1,106 @@ +BPjs tips +========= + +Mainly for commands that are useful, but not in frequent use. + +Build jar with tests +-------------------- + +Useful for running long verifications outside of NetBeans + +:: + + mvn jar:test-jar + +NOTE: The build must use jdk8 for now. Execution can be done on any jdk +(at least, worked for us with jdk11). + +Running verifications that live in the tests directory from the terminal +------------------------------------------------------------------------ + +to run the actual test, also build the uber-jar: + +:: + + mvn package -P uber-jar + +Now both live in the ``target`` directory. You can now run the test +using Java, as usual, with both jars in the ``-cp`` parameter: + +:: + + java -cp target/BPjs-0.9.2-SNAPSHOT.uber.jar:target/BPjs-0.9.2-SNAPSHOT-tests.jar il.ac.bgu.cs.bp.bpjs.TicTacToe.TicTacToeVerMain + +Event comparison +---------------- + +Better to use non-strict JavaScript object comparison for now. So prefer + +.. code:: javascript + + var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)}); + if ( evt.name == ADD_WETS.name ) { + ... + +over + +.. code:: javascript + + var evt = bp.sync({waitFor:ANY_ADDITION, block:chooseBlock(bias)}); + if ( evt === ADD_WETS ) { + ... + +as the latter may return a false negative, especially during +verification. + +Implementing Custom Events and Using Custom Objects as Event Data +----------------------------------------------------------------- + +ALWAYS make sure that you have state-based, meaningful ``equals()`` and +``hashCode()``. Or verification fails. + +State minimization +------------------ + +(yes, this is informed by the “data minimization” directive of privacy +by design) It’s better to store least amount of data. E.g. in the +fruitRatio.js file, this version of the b-threads yields three states: + +.. code:: javascript + + bp.registerBThread( "RaspberryAdder", function(){ + var fruitIndex=0; + while (true) { + var evt = null; + if ( fruitIndex > 0 ) { + evt = bp.hot(true).sync({request:ADD_RASPB, + waitFor:ADD_FRUIT}); + } else { + evt = bp.sync({waitFor:ADD_FRUIT}); + } + fruitIndex = fruitIndex + + evt.data.blueberries-evt.data.raspberries; + } + }); + +Where this version yields 4 (note different location of ``var evt``) : + +.. code:: javascript + + bp.registerBThread( "RaspberryAdder", function(){ + var fruitIndex=0; + var evt = null; + while (true) { + if ( fruitIndex > 0 ) { + evt = bp.hot(true).sync({request:ADD_RASPB, + waitFor:ADD_FRUIT}); + } else { + evt = bp.sync({waitFor:ADD_FRUIT}); + } + fruitIndex = fruitIndex + + evt.data.blueberries-evt.data.raspberries; + } + }); + +That’s because the former does not store the event from the previous +iteration. From b43bca4ce0eeeddc112873f525582bdfe261b521 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Tue, 5 Feb 2019 23:10:55 +0200 Subject: [PATCH 05/11] Event selection strategies now accept BProgramSyncSnapshot as a parameter --- README.md | 13 +- .../bp/bpjs/analysis/DfsCycleInspection.java | 2 +- .../cs/bp/bpjs/analysis/DfsInspections.java | 6 +- .../cs/bp/bpjs/analysis/DfsTraversalNode.java | 5 +- .../bprogramio/BProgramSyncSnapshotIO.java | 2 +- .../cs/bp/bpjs/execution/BProgramRunner.java | 4 +- .../bp/bpjs/model/BProgramSyncSnapshot.java | 8 +- .../cs/bp/bpjs/model/BThreadSyncSnapshot.java | 4 +- .../AbstractEventSelectionStrategy.java | 10 +- ...stractEventSelectionStrategyDecorator.java | 11 +- .../EventSelectionStrategy.java | 28 +++-- ...oggingEventSelectionStrategyDecorator.java | 15 ++- .../OrderedEventSelectionStrategy.java | 6 +- ...ausingEventSelectionStrategyDecorator.java | 7 +- ...rioritizedBSyncEventSelectionStrategy.java | 6 +- ...ritizedBThreadsEventSelectionStrategy.java | 8 +- .../SimpleEventSelectionStrategy.java | 5 +- .../internal/ContinuationProgramState.java | 12 +- .../java/il/ac/bgu/cs/bp/bpjs/TestUtils.java | 22 ++++ .../analysis/examples/DiningPhilTest.java | 2 +- .../jsproxy/SyncStatementTempTest.java | 7 +- .../bpjs/mocks/MockBProgramSyncSnapshot.java | 39 ++++++ .../bpjs/mocks/MockBThreadSyncSnapshot.java | 74 +++++++++++ .../bpjs/model/BProgramSyncSnapshotTest.java | 40 +++--- .../bpjs/model/BThreadSyncSnapshotTest.java | 12 +- .../OrderedEventSelectionStrategyTest.java | 34 +++--- ...itizedBSyncEventSelectionStrategyTest.java | 55 +++++---- ...zedBThreadsEventSelectionStrategyTest.java | 71 ++++++----- .../SimpleEventSelectionStrategyTest.java | 115 ++++++++++-------- 29 files changed, 405 insertions(+), 218 deletions(-) create mode 100644 src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBProgramSyncSnapshot.java create mode 100644 src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBThreadSyncSnapshot.java diff --git a/README.md b/README.md index 3f07fee1..f47fe1b0 100644 --- a/README.md +++ b/README.md @@ -44,14 +44,21 @@ a link to this page somewhere in the documentation/system about section. ## Change Log for the BPjs Library. +### 2019-02-04 +* :arrow_up: :tada: Event selection strategies now accept `BProgramSyncSnapshot`, rather than a set of sync statements and external events. + +### 2019-02-04 +* :sparkles: Testing infrastructure for execution traces. +* :arrow_up: More terminology cleanups in the api (e.g. "bsync" converted to "sync") + +### 2019-02-03 +* :arrow_up: `VisitedStateStore` now stores *states*, not DFS nodes. So it's more reusable that way. + ### 2019-01-19 * :sparkles: More tests. * :arrow_up: `BriefPrintDfsVerifierListener` => `PrintDfsVerifierListener`, so that it's consistent with `PrintBProgramRunnerListener`. * :arrow_up: Incorporated the "BPjs Tips" file to the central documentation. -### 2019-02-03 -* :arrow_up: `VisitedStateStore` now stores *states*, not DFS nodes. So it's more reusable that way. - ### 2019-01-18 * :bug: Fixed a that cause equality tests of JS event sets to return false negatives. * :bug: The `bp` object no longer collected by the state comparators. diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java index 760cca8c..66ec4856 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java @@ -42,7 +42,7 @@ public interface DfsCycleInspection { * * [a]-[b]-[c]-[d]--... * \ | - * +-----+ + * +-----+ (going from d back to b) * * * This methods will be called with trace={@code [a][b][c][d]} and diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java index cc6a0695..f18ba4a6 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java @@ -81,7 +81,7 @@ public final class DfsInspections { if ( curNode.getSystemState().isHot() && curNode.getSelectableEvents().isEmpty() ) { Set hotlyTerminated = curNode.getSystemState().getBThreadSnapshots().stream() - .filter( s -> s.getBSyncStatement().isHot() ).map( s->s.getName() ).collect( toSet() ); + .filter( s -> s.getSyncStatement().isHot() ).map( s->s.getName() ).collect( toSet() ); return Optional.of( new HotTerminationViolation(hotlyTerminated, trace) ); } else return Optional.empty(); }; @@ -123,7 +123,7 @@ public Optional inspectCycle(List currentTrace, int } private Set getHotThreadNames( Set bts ) { - return bts.stream().filter( bt -> bt.getBSyncStatement().isHot() ) + return bts.stream().filter( bt -> bt.getSyncStatement().isHot() ) .map( bt -> bt.getName() ) .collect( toSet() ); } @@ -139,7 +139,7 @@ private Set getHotThreadNames( Set bts ) { // Utility methods. private static boolean hasRequestedEvents(BProgramSyncSnapshot bpss) { - return bpss.getBThreadSnapshots().stream().anyMatch(btss -> (!btss.getBSyncStatement().getRequest().isEmpty())); + return bpss.getBThreadSnapshots().stream().anyMatch(btss -> (!btss.getSyncStatement().getRequest().isEmpty())); } private static DfsTraversalNode peek(List trace) { diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java index e2188306..bcdbefbd 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java @@ -48,8 +48,7 @@ protected DfsTraversalNode(BProgram bp, BProgramSyncSnapshot systemState, BEvent this.lastEvent = e; if (bp != null) { - selectableEvents = bp.getEventSelectionStrategy().selectableEvents(systemState.getStatements(), - systemState.getExternalEvents()); + selectableEvents = bp.getEventSelectionStrategy().selectableEvents(systemState); ArrayList eventOrdered = new ArrayList<>(selectableEvents); Collections.shuffle(eventOrdered); iterator = eventOrdered.iterator(); @@ -64,7 +63,7 @@ private String stateString() { StringBuilder str = new StringBuilder(); systemState.getBThreadSnapshots().forEach( - s -> str.append("\t").append(s.toString()).append(" {").append(s.getBSyncStatement()).append("} \n")); + s -> str.append("\t").append(s.toString()).append(" {").append(s.getSyncStatement()).append("} \n")); return str.toString(); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogramio/BProgramSyncSnapshotIO.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogramio/BProgramSyncSnapshotIO.java index fe36ed2a..5ff25aa6 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogramio/BProgramSyncSnapshotIO.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/bprogramio/BProgramSyncSnapshotIO.java @@ -181,7 +181,7 @@ private void writeBThreadSnapshot(BThreadSyncSnapshot bss, ObjectOutputStream ou try (BThreadSyncSnapshotOutputStream btos = new BThreadSyncSnapshotOutputStream(bthreadBytes, scope)) { btos.writeObject(bss.getEntryPoint()); btos.writeObject(bss.getInterrupt().orElse(null)); - btos.writeObject(bss.getBSyncStatement()); + btos.writeObject(bss.getSyncStatement()); btos.writeObject(bss.getContinuation()); btos.flush(); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunner.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunner.java index 4bd4d1ef..030f988a 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunner.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunner.java @@ -94,7 +94,7 @@ public void run() { while ( (!cur.noBThreadsLeft()) && go.get() ) { // see which events are selectable - Set possibleEvents = bprog.getEventSelectionStrategy().selectableEvents(cur.getStatements(), cur.getExternalEvents()); + Set possibleEvents = bprog.getEventSelectionStrategy().selectableEvents(cur); if ( possibleEvents.isEmpty() ) { // Superstep done: No events available for selection. @@ -115,7 +115,7 @@ public void run() { } else { // we can select some events - select one and advance. - Optional res = bprog.getEventSelectionStrategy().select(cur.getStatements(), cur.getExternalEvents(), possibleEvents); + Optional res = bprog.getEventSelectionStrategy().select(cur, possibleEvents); if ( res.isPresent() ) { EventSelectionResult esr = res.get(); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java index 18750ac9..89a43237 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java @@ -142,7 +142,7 @@ public BProgramSyncSnapshot triggerEvent(BEvent anEvent, ExecutorService exSvc, // Split threads to those that advance this round and those that sleep. threadSnapshots.forEach( snapshot -> { - (snapshot.getBSyncStatement().shouldWakeFor(anEvent) ? resumingThisRound : sleepingThisRound).add(snapshot); + (snapshot.getSyncStatement().shouldWakeFor(anEvent) ? resumingThisRound : sleepingThisRound).add(snapshot); }); } finally { Context.exit(); @@ -183,7 +183,7 @@ public BProgramSyncSnapshot triggerEvent(BEvent anEvent, ExecutorService exSvc, private void handleInterrupts(BEvent anEvent, Iterable listeners, BProgram bprog, Context ctxt) { Set interrupted = threadSnapshots.stream() - .filter(bt -> bt.getBSyncStatement().getInterrupt().contains(anEvent)) + .filter(bt -> bt.getSyncStatement().getInterrupt().contains(anEvent)) .collect(toSet()); if (!interrupted.isEmpty()) { threadSnapshots.removeAll(interrupted); @@ -211,7 +211,7 @@ public Set getBThreadSnapshots() { } public Set getStatements() { - return getBThreadSnapshots().stream().map(BThreadSyncSnapshot::getBSyncStatement) + return getBThreadSnapshots().stream().map(BThreadSyncSnapshot::getSyncStatement) .collect(toSet()); } @@ -256,7 +256,7 @@ public FailedAssertion getFailedAssertion() { */ public boolean isHot() { return getBThreadSnapshots().stream() - .map(BThreadSyncSnapshot::getBSyncStatement) + .map(BThreadSyncSnapshot::getSyncStatement) .filter(SyncStatement::isHot) .findAny().isPresent(); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java index 7cefd4a4..73a2594a 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshot.java @@ -88,11 +88,11 @@ public BThreadSyncSnapshot copyWith(Object aContinuation, SyncStatement aStateme return retVal; } - public SyncStatement getBSyncStatement() { + public SyncStatement getSyncStatement() { return bSyncStatement; } - public void setBSyncStatement(SyncStatement stmt) { + public void setSyncStatement(SyncStatement stmt) { bSyncStatement = stmt; if (bSyncStatement.getBthread() != this) { bSyncStatement.setBthread(this); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategy.java index ec677b46..2c3f2717 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategy.java @@ -25,6 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSet; import java.util.ArrayList; import static java.util.Collections.singleton; @@ -65,18 +66,17 @@ public long getSeed() { /** * Randomly select an event from {@code selectableEvents}, or a non-blocked event from {@code externalEvents}, in case {@code selectableEvents} is empty. * - * @param statements Statements at the current {@code bsync}. - * @param externalEvents List of events that are not requested by b-threads (at least, not directly). + * @param bpss a b-program at synchronization point. * @param selectableEvents Set of events that can be selected. * @return An optional event selection result. */ @Override - public Optional select(Set statements, List externalEvents, Set selectableEvents) { + public Optional select(BProgramSyncSnapshot bpss, Set selectableEvents) { if (selectableEvents.isEmpty()) { return Optional.empty(); } BEvent chosen = new ArrayList<>(selectableEvents).get(rnd.nextInt(selectableEvents.size())); - Set requested = statements.stream() + Set requested = bpss.getStatements().stream() .filter((SyncStatement stmt) -> stmt != null) .flatMap((SyncStatement stmt) -> stmt.getRequest().stream()) .collect(Collectors.toSet()); @@ -85,7 +85,7 @@ public Optional select(Set statements, List return Optional.of(new EventSelectionResult(chosen)); } else { // that was an external event, need to find the first index - return Optional.of(new EventSelectionResult(chosen, singleton(externalEvents.indexOf(chosen)))); + return Optional.of(new EventSelectionResult(chosen, singleton(bpss.getExternalEvents().indexOf(chosen)))); } } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategyDecorator.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategyDecorator.java index fecfbd4f..c34b4f0c 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategyDecorator.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/AbstractEventSelectionStrategyDecorator.java @@ -24,8 +24,7 @@ package il.ac.bgu.cs.bp.bpjs.model.eventselection; import il.ac.bgu.cs.bp.bpjs.model.BEvent; -import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; -import java.util.List; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import java.util.Optional; import java.util.Set; @@ -50,13 +49,13 @@ public ESS getDecorated() { } @Override - public Set selectableEvents(Set statements, List externalEvents) { - return getDecorated().selectableEvents(statements, externalEvents); + public Set selectableEvents(BProgramSyncSnapshot bpss) { + return getDecorated().selectableEvents(bpss); } @Override - public Optional select(Set statements, List externalEvents, Set selectableEvents) { - return getDecorated().select(statements, externalEvents, selectableEvents); + public Optional select(BProgramSyncSnapshot bpss, Set selectableEvents) { + return getDecorated().select(bpss, selectableEvents); } } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/EventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/EventSelectionStrategy.java index e3178c7d..5eadc761 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/EventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/EventSelectionStrategy.java @@ -2,6 +2,7 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import java.util.List; import java.util.Optional; import java.util.Set; @@ -19,25 +20,32 @@ public interface EventSelectionStrategy { /** - * Creates the set of selectable events, given the {@link SyncStatement}s from - * all participating BThreads. - * @param statements statements of all participating BThreads. - * @param externalEvents events queued by external processes. + * Creates the set of selectable events, given a b-program's + * synchronization point. + * + * @param bpss a {@link BProgram} at a synchronization point. * @return A set of events that may be selected for execution. */ - Set selectableEvents(Set statements, List externalEvents); + Set selectableEvents(BProgramSyncSnapshot bpss); /** * Selects an event for execution from the parameter {@code selectableEvents}, * or returns {@link Optional#empty()} in case no suitable event is found. * - * @param statements statements of all participating BThreads. - * @param externalEvents events queued by external processes. - * @param selectableEvents A set of events to select from + * The {@code selectableEvents} set is Normally the set of + * events returned by {@code this}' {@link #selectableEvents(il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot)} + * method on the previous call on the same synchronization point. This is + * an optimization that allows most strategies to select events only once + * per synchronization point. + * + * In normal BP, the selected event (if any) has + * to be a member of {@code selectableEvents}. + * + * @param bpss a {@link BProgram} at a synchronization point. + * @param selectableEvents A set of events to select from. * @return An event selection result, or no result. */ - Optional select(Set statements, - List externalEvents, + Optional select(BProgramSyncSnapshot bpss, Set selectableEvents ); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/LoggingEventSelectionStrategyDecorator.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/LoggingEventSelectionStrategyDecorator.java index afb3eb4b..aca90629 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/LoggingEventSelectionStrategyDecorator.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/LoggingEventSelectionStrategyDecorator.java @@ -23,11 +23,10 @@ */ package il.ac.bgu.cs.bp.bpjs.model.eventselection; -import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import java.io.PrintStream; import java.io.PrintWriter; -import java.util.List; import java.util.Optional; import java.util.Set; @@ -53,19 +52,19 @@ public LoggingEventSelectionStrategyDecorator(ESS decorated) { } @Override - public Set selectableEvents(Set statements, List externalEvents) { - final Set selectableEvents = getDecorated().selectableEvents(statements, externalEvents); + public Set selectableEvents(BProgramSyncSnapshot bpss) { + final Set selectableEvents = getDecorated().selectableEvents(bpss); out.println("== Choosing Selectable Events =="); out.println("BThread Sync Statements:"); - statements.forEach( stmt -> { + bpss.getStatements().forEach( stmt -> { out.println("+ " + stmt.getBthread().getName() + ":" + (stmt.isHot()?" HOT":"")); out.println(" Request: " + stmt.getRequest()); out.println(" WaitFor: " + stmt.getWaitFor()); out.println(" Block: " + stmt.getBlock()); out.println(" Interrupt: " + stmt.getInterrupt()); }); - out.println("+ ExternalEvents: " + externalEvents); + out.println("+ ExternalEvents: " + bpss.getExternalEvents()); out.println("-- Selectable Events -----------"); if ( selectableEvents.isEmpty() ){ @@ -80,8 +79,8 @@ public Set selectableEvents(Set statements, List } @Override - public Optional select(Set statements, List externalEvents, Set selectableEvents) { - Optional selectedEvent = getDecorated().select(statements, externalEvents, selectableEvents); + public Optional select(BProgramSyncSnapshot bpss, Set selectableEvents) { + Optional selectedEvent = getDecorated().select(bpss, selectableEvents); out.println("== Actual Event Selection ======"); out.println( selectedEvent.toString() ); out.println("================================"); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategy.java index 32a0ce7b..107b7efa 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategy.java @@ -25,6 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.eventsets.ComposableEventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSets; @@ -50,7 +51,10 @@ public class OrderedEventSelectionStrategy extends AbstractEventSelectionStrategy { @Override - public Set selectableEvents(Set statements, List externalEvents) { + public Set selectableEvents(BProgramSyncSnapshot bpss) { + Set statements = bpss.getStatements(); + List externalEvents = bpss.getExternalEvents(); + if ( statements.isEmpty() ) { // Corner case, not sure this is even possible. return externalEvents.isEmpty() ? emptySet() : singleton(externalEvents.get(0)); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PausingEventSelectionStrategyDecorator.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PausingEventSelectionStrategyDecorator.java index 7a75a699..af3584ca 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PausingEventSelectionStrategyDecorator.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PausingEventSelectionStrategyDecorator.java @@ -25,8 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.model.BEvent; import il.ac.bgu.cs.bp.bpjs.model.BProgram; -import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; -import java.util.List; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import java.util.Optional; import java.util.Set; import java.util.concurrent.locks.ReadWriteLock; @@ -61,8 +60,8 @@ public PausingEventSelectionStrategyDecorator(ESS decorated) { } @Override - public Optional select(Set statements, List externalEvents, Set selectableEvents) { - Optional res = getDecorated().select(statements, externalEvents, selectableEvents); + public Optional select(BProgramSyncSnapshot bpss, Set selectableEvents) { + Optional res = getDecorated().select(bpss, selectableEvents); lock.readLock().lock(); listener.eventSelectionPaused(this); lock.writeLock().lock(); // blocks while the read lock is locked. diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategy.java index 5de024b0..498cd662 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategy.java @@ -25,6 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.eventsets.ComposableEventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSets; @@ -57,7 +58,10 @@ public PrioritizedBSyncEventSelectionStrategy() { } @Override - public Set selectableEvents(Set statements, List externalEvents) { + public Set selectableEvents(BProgramSyncSnapshot bpss) { + + Set statements = bpss.getStatements(); + List externalEvents = bpss.getExternalEvents(); EventSet blocked = ComposableEventSet.anyOf(statements.stream() .filter( stmt -> stmt!=null ) diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategy.java index 22316ac5..5afde4ed 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategy.java @@ -6,7 +6,6 @@ import static java.util.stream.Collectors.toSet; import java.util.HashMap; -import java.util.List; import java.util.Map; import java.util.Set; import java.util.stream.Collectors; @@ -15,12 +14,14 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.eventsets.ComposableEventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSets; import java.util.Collection; import java.util.Collections; import java.util.Comparator; +import java.util.List; import java.util.stream.Stream; /** @@ -46,7 +47,10 @@ public PrioritizedBThreadsEventSelectionStrategy() { } @Override - public Set selectableEvents(Set statements, List externalEvents) { + public Set selectableEvents(BProgramSyncSnapshot bpss) { + Set statements = bpss.getStatements(); + List externalEvents = bpss.getExternalEvents(); + if ( statements.isEmpty() ) { // Corner case, not sure this is even possible. return externalEvents.isEmpty() ? emptySet() : singleton(externalEvents.get(0)); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategy.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategy.java index c4128c97..e90212d7 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategy.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategy.java @@ -2,6 +2,7 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.eventsets.ComposableEventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSet; import il.ac.bgu.cs.bp.bpjs.model.eventsets.EventSets; @@ -36,7 +37,9 @@ public SimpleEventSelectionStrategy() {} @Override - public Set selectableEvents(Set statements, List externalEvents) { + public Set selectableEvents(BProgramSyncSnapshot bpss) { + Set statements = bpss.getStatements(); + List externalEvents = bpss.getExternalEvents(); if ( statements.isEmpty() ) { // Corner case, not sure this is even possible. return externalEvents.isEmpty() ? emptySet() : singleton(externalEvents.get(0)); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java index d0355380..ef63b432 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java @@ -56,15 +56,19 @@ * @author michael */ public class ContinuationProgramState { - private final Map variables = new HashMap<>(); - private int programCounter = -1; - private int frameIndex = -1; + protected final Map variables = new HashMap<>(); + protected int programCounter = -1; + protected int frameIndex = -1; public ContinuationProgramState( NativeContinuation nc ) { collectStatus(nc.getImplementation()); collectScopeValues(nc); } + protected ContinuationProgramState(){ + // extra C'tor for subclasses. + } + private void collectScopeValues(NativeContinuation nc ){ ScriptableObject current = nc; ScriptableObject currentScope = nc; @@ -189,7 +193,7 @@ public boolean equals(Object obj) { if (obj == null) { return false; } - if (getClass() != obj.getClass()) { + if ( ! (obj instanceof ContinuationProgramState) ) { return false; } final ContinuationProgramState other = (ContinuationProgramState) obj; diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java index 7d14b004..20bd82e8 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java @@ -26,8 +26,18 @@ import il.ac.bgu.cs.bp.bpjs.model.BEvent; import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBProgramSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.BProgram; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.StringBProgram; +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; import java.util.List; import java.util.Objects; +import java.util.Set; import java.util.concurrent.ExecutionException; import java.util.concurrent.Future; import static java.util.stream.Collectors.joining; @@ -71,4 +81,16 @@ public static T safeGet( Future f ) { throw new RuntimeException(ex); } } + + public static BProgramSyncSnapshot makeBPSS( BThreadSyncSnapshot... snapshots ) { + Set bts = new HashSet<>(); + bts.addAll(Arrays.asList(snapshots)); + return makeBPSS( bts ); + } + + public static BProgramSyncSnapshot makeBPSS( Collection snapshots ) { + BProgram bprog = new StringBProgram(""); + Set bts = new HashSet<>(snapshots); + return new MockBProgramSyncSnapshot(new BProgramSyncSnapshot(bprog, bts, Collections.emptyList(), null)); + } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java index 25cff583..00a08eae 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java @@ -38,7 +38,7 @@ private static void printCounterExample(VerificationResult res) { .sorted((s1, s2) -> s1.getName().compareTo(s2.getName())) .forEach(s -> { System.out.println(s.getName()); - System.out.println(s.getBSyncStatement()); + System.out.println(s.getSyncStatement()); System.out.println(); }); } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/SyncStatementTempTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/SyncStatementTempTest.java index 138769d4..e94b4fbf 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/SyncStatementTempTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/jsproxy/SyncStatementTempTest.java @@ -28,6 +28,7 @@ import il.ac.bgu.cs.bp.bpjs.execution.listeners.PrintBProgramRunnerListener; import il.ac.bgu.cs.bp.bpjs.model.BEvent; import il.ac.bgu.cs.bp.bpjs.model.BProgram; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.eventselection.AbstractEventSelectionStrategyDecorator; @@ -55,9 +56,9 @@ public TemperatureLoggingESS(EventSelectionStrategy decorated) { } @Override - public Set selectableEvents(Set statements, List externalEvents) { - isHotRecord.add(statements.stream().filter(SyncStatement::isHot).findAny().isPresent()); - return decorated.selectableEvents(statements, externalEvents); + public Set selectableEvents(BProgramSyncSnapshot bpss) { + isHotRecord.add(bpss.getStatements().stream().filter(SyncStatement::isHot).findAny().isPresent()); + return decorated.selectableEvents(bpss); } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBProgramSyncSnapshot.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBProgramSyncSnapshot.java new file mode 100644 index 00000000..40d61c76 --- /dev/null +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBProgramSyncSnapshot.java @@ -0,0 +1,39 @@ +/* + * The MIT License + * + * Copyright 2019 michael. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package il.ac.bgu.cs.bp.bpjs.mocks; + +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import java.util.ArrayList; + +/** + * + * @author michael + */ +public class MockBProgramSyncSnapshot extends BProgramSyncSnapshot { + + public MockBProgramSyncSnapshot(BProgramSyncSnapshot bpss) { + super(bpss.getBProgram(), bpss.getBThreadSnapshots(), new ArrayList<>(bpss.getExternalEvents()), bpss.getFailedAssertion()); + } + +} diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBThreadSyncSnapshot.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBThreadSyncSnapshot.java new file mode 100644 index 00000000..e513db75 --- /dev/null +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mocks/MockBThreadSyncSnapshot.java @@ -0,0 +1,74 @@ +package il.ac.bgu.cs.bp.bpjs.mocks; + + +import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; +import il.ac.bgu.cs.bp.bpjs.model.internal.ContinuationProgramState; +import java.util.concurrent.atomic.AtomicInteger; + +/* + * The MIT License + * + * Copyright 2019 michael. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ + +/** + * + * @author michael + */ +public class MockBThreadSyncSnapshot extends BThreadSyncSnapshot { + + private static final AtomicInteger NEXT_ID = new AtomicInteger(0); + + public static class MockContinuationProgramState extends ContinuationProgramState { + + public void setFrameIndex(int frameIndex) { + this.frameIndex = frameIndex; + } + + public void setProgramCounter(int programCounter) { + this.programCounter = programCounter; + } + + public void setVariable( String name, Object value ) { + variables.put(name, value); + } + } + + public MockBThreadSyncSnapshot(String aName, SyncStatement stmt ) { + super(aName, null); + setSyncStatement(stmt); + stmt.setBthread(this); + } + + public MockBThreadSyncSnapshot(SyncStatement stmt ) { + this( "mock-btss_" + NEXT_ID.incrementAndGet(), stmt ); + } + + @Override + public ContinuationProgramState getContinuationProgramState() { + return super.getContinuationProgramState(); + } + + + + +} diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshotTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshotTest.java index 2c9a488c..66e4beb5 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshotTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshotTest.java @@ -75,8 +75,8 @@ public void testDoubleTriggerEvent() throws InterruptedException { BProgramSyncSnapshot setup = bprog.setup(); ExecutorService execSvcA = ExecutorServiceMaker.makeWithName("BProgramSnapshotTriggerTest"); BProgramSyncSnapshot stepa = setup.start(execSvcA); - Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(stepa.getStatements(), stepa.getExternalEvents()); - EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(stepa.getStatements(), stepa.getExternalEvents(), possibleEvents_a).get(); + Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(stepa); + EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(stepa, possibleEvents_a).get(); stepa.triggerEvent(event_a.getEvent(), execSvcA, listeners); exception.expect(IllegalStateException.class); stepa.triggerEvent(event_a.getEvent(), execSvcA, listeners); @@ -92,8 +92,8 @@ public void testHotnessDetection() throws InterruptedException { ExecutorService execSvcA = ExecutorServiceMaker.makeWithName("BProgramSnapshotTriggerTest"); BProgramSyncSnapshot bpss = setup.start(execSvcA); assertFalse(bpss.isHot()); - Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(bpss.getStatements(), bpss.getExternalEvents()); - EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(bpss.getStatements(), bpss.getExternalEvents(), possibleEvents_a).get(); + Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(bpss); + EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(bpss, possibleEvents_a).get(); bpss = bpss.triggerEvent(event_a.getEvent(), execSvcA, listeners); assertTrue(bpss.isHot()); @@ -133,20 +133,20 @@ public void testEqualsSingleStep() throws InterruptedException { assertNotEquals(setup2, stepb); //run second step - Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(stepa.getStatements(), stepa.getExternalEvents()); - Set possibleEvents_b = bprog2.getEventSelectionStrategy().selectableEvents(stepb.getStatements(), stepb.getExternalEvents()); - EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(stepa.getStatements(), stepa.getExternalEvents(), possibleEvents_a).get(); - EventSelectionResult event_b = bprog2.getEventSelectionStrategy().select(stepa.getStatements(), stepb.getExternalEvents(), possibleEvents_b).get(); + Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(stepa); + Set possibleEvents_b = bprog2.getEventSelectionStrategy().selectableEvents(stepb); + EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(stepa, possibleEvents_a).get(); + EventSelectionResult event_b = bprog2.getEventSelectionStrategy().select(stepa, possibleEvents_b).get(); BProgramSyncSnapshot step2a = stepa.triggerEvent(event_a.getEvent(), execSvcA, listeners); BProgramSyncSnapshot step2b = stepb.triggerEvent(event_b.getEvent(), execSvcB, listeners); assertEquals(step2a, step2b); assertNotEquals(stepa, step2a); assertNotEquals(stepb, step2b); - possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step2a.getStatements(), step2a.getExternalEvents()); - possibleEvents_b = bprog2.getEventSelectionStrategy().selectableEvents(step2b.getStatements(), step2b.getExternalEvents()); - event_a = bprog.getEventSelectionStrategy().select(step2a.getStatements(), step2a.getExternalEvents(), possibleEvents_a).get(); - event_b = bprog2.getEventSelectionStrategy().select(step2b.getStatements(), step2b.getExternalEvents(), possibleEvents_b).get(); + possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step2a); + possibleEvents_b = bprog2.getEventSelectionStrategy().selectableEvents(step2b); + event_a = bprog.getEventSelectionStrategy().select(step2a, possibleEvents_a).get(); + event_b = bprog2.getEventSelectionStrategy().select(step2b, possibleEvents_b).get(); BProgramSyncSnapshot step3a = step2a.triggerEvent(event_a.getEvent(), execSvcA, listeners); BProgramSyncSnapshot step3b = step2b.triggerEvent(event_b.getEvent(), execSvcB, listeners); assertEquals(step3a, step3b); @@ -188,10 +188,10 @@ public void testEqualsSingleStepAssert() throws InterruptedException { assertNotEquals(setup2, postStart2); // Run second step - Set possibleEvents1 = bprog1.getEventSelectionStrategy().selectableEvents(postStart1.getStatements(), postStart1.getExternalEvents()); - Set possibleEvents2 = bprog2.getEventSelectionStrategy().selectableEvents(postStart2.getStatements(), postStart2.getExternalEvents()); - EventSelectionResult event1_1 = bprog1.getEventSelectionStrategy().select(postStart1.getStatements(), postStart1.getExternalEvents(), possibleEvents1).get(); - EventSelectionResult event1_2 = bprog2.getEventSelectionStrategy().select(postStart1.getStatements(), postStart2.getExternalEvents(), possibleEvents2).get(); + Set possibleEvents1 = bprog1.getEventSelectionStrategy().selectableEvents(postStart1); + Set possibleEvents2 = bprog2.getEventSelectionStrategy().selectableEvents(postStart2); + EventSelectionResult event1_1 = bprog1.getEventSelectionStrategy().select(postStart1, possibleEvents1).get(); + EventSelectionResult event1_2 = bprog2.getEventSelectionStrategy().select(postStart1, possibleEvents2).get(); BProgramSyncSnapshot postSync1_1 = postStart1.triggerEvent(event1_1.getEvent(), execSvcA, listeners); BProgramSyncSnapshot postSync1_2 = postStart2.triggerEvent(event1_2.getEvent(), execSvcB, listeners); assertTrue(postSync1_1.isStateValid()); @@ -199,10 +199,10 @@ public void testEqualsSingleStepAssert() throws InterruptedException { assertNotEquals(postStart1, postSync1_1); assertNotEquals(postStart2, postSync1_2); - possibleEvents1 = bprog1.getEventSelectionStrategy().selectableEvents(postSync1_1.getStatements(), postSync1_1.getExternalEvents()); - possibleEvents2 = bprog2.getEventSelectionStrategy().selectableEvents(postSync1_2.getStatements(), postSync1_2.getExternalEvents()); - EventSelectionResult event2_1 = bprog1.getEventSelectionStrategy().select(postSync1_1.getStatements(), postSync1_1.getExternalEvents(), possibleEvents1).get(); - EventSelectionResult event2_2 = bprog2.getEventSelectionStrategy().select(postSync1_2.getStatements(), postSync1_2.getExternalEvents(), possibleEvents2).get(); + possibleEvents1 = bprog1.getEventSelectionStrategy().selectableEvents(postSync1_1); + possibleEvents2 = bprog2.getEventSelectionStrategy().selectableEvents(postSync1_2); + EventSelectionResult event2_1 = bprog1.getEventSelectionStrategy().select(postSync1_1, possibleEvents1).get(); + EventSelectionResult event2_2 = bprog2.getEventSelectionStrategy().select(postSync1_2, possibleEvents2).get(); assertEquals("B", event2_1.getEvent().name); BProgramSyncSnapshot postSync2_1 = postSync1_1.triggerEvent(event2_1.getEvent(), execSvcA, listeners); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java index 04f6063a..84022a5a 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/BThreadSyncSnapshotTest.java @@ -58,14 +58,14 @@ public void testJSVarState() throws InterruptedException { snapshots.add(step); //Iteration 1, starts already at request state A for (int i = 0; i < 4; i++) { - Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step.getStatements(), step.getExternalEvents()); - EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(step.getStatements(), step.getExternalEvents(), possibleEvents_a).get(); + Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step); + EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(step, possibleEvents_a).get(); step = step.triggerEvent(event_a.getEvent(), execSvc, listeners); } snapshots.add(step); for (int i = 0; i < 4; i++) { - Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step.getStatements(), step.getExternalEvents()); - EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(step.getStatements(), step.getExternalEvents(), possibleEvents_a).get(); + Set possibleEvents_a = bprog.getEventSelectionStrategy().selectableEvents(step); + EventSelectionResult event_a = bprog.getEventSelectionStrategy().select(step, possibleEvents_a).get(); step = step.triggerEvent(event_a.getEvent(), execSvc, listeners); } snapshots.add(step); @@ -86,8 +86,8 @@ public void testJavaVarState() throws InterruptedException { BProgramSyncSnapshot postSetup = bprog.setup(); ExecutorService execSvcA = ExecutorServiceMaker.makeWithName("BProgramSnapshotTriggerTest"); BProgramSyncSnapshot postSync1 = postSetup.start(execSvcA); - Set possibleEvents = bprog.getEventSelectionStrategy().selectableEvents(postSync1.getStatements(), postSync1.getExternalEvents()); - EventSelectionResult esr = bprog.getEventSelectionStrategy().select(postSync1.getStatements(), postSync1.getExternalEvents(), possibleEvents).get(); + Set possibleEvents = bprog.getEventSelectionStrategy().selectableEvents(postSync1); + EventSelectionResult esr = bprog.getEventSelectionStrategy().select(postSync1, possibleEvents).get(); BProgramSyncSnapshot postSync2 = postSync1.triggerEvent(esr.getEvent(), execSvcA, listeners); assertNotEquals(postSync1.getBThreadSnapshots(), postSync2.getBThreadSnapshots()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategyTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategyTest.java index b7b0bd06..a673453b 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategyTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/OrderedEventSelectionStrategyTest.java @@ -23,8 +23,11 @@ */ package il.ac.bgu.cs.bp.bpjs.model.eventselection; +import il.ac.bgu.cs.bp.bpjs.TestUtils; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import java.util.Arrays; import java.util.Collections; import java.util.HashSet; @@ -38,13 +41,10 @@ */ public class OrderedEventSelectionStrategyTest { - public OrderedEventSelectionStrategyTest() { - } - - private static final BEvent evt1 = new BEvent("evt1"); - private static final BEvent evt2 = new BEvent("evt2"); - private static final BEvent evt3 = new BEvent("evt3"); - private static final BEvent evt4 = new BEvent("evt4"); + private static final BEvent EVT_1 = new BEvent("evt1"); + private static final BEvent EVT_2 = new BEvent("evt2"); + private static final BEvent EVT_3 = new BEvent("evt3"); + private static final BEvent EVT_4 = new BEvent("evt4"); /** * Test of selectableEvents method, of class OrderedEventSelectionStrategy. @@ -54,11 +54,12 @@ public void testSelectableEvents_noBlocking() { OrderedEventSelectionStrategy sut = new OrderedEventSelectionStrategy(); - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make().request(Arrays.asList(evt1, evt2, evt3, evt4))); - stmts.add(SyncStatement.make().request(Arrays.asList(evt2, evt3, evt4))); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_1, EVT_2, EVT_3, EVT_4))), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_2, EVT_3, EVT_4))) + ); - assertEquals( new HashSet<>(Arrays.asList(evt1, evt2)), sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals( new HashSet<>(Arrays.asList(EVT_1, EVT_2)), sut.selectableEvents(bpss)); } @Test @@ -66,12 +67,13 @@ public void testSelectableEvents_withBlocking() { OrderedEventSelectionStrategy sut = new OrderedEventSelectionStrategy(); - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make().request(Arrays.asList(evt1, evt2, evt3, evt4))); - stmts.add(SyncStatement.make().request(Arrays.asList(evt2, evt3, evt4))); - stmts.add(SyncStatement.make().request(Arrays.asList(evt3, evt4)).block(evt1)); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_1, EVT_2, EVT_3, EVT_4))), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_2, EVT_3, EVT_4))), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_3, EVT_4)).block(EVT_1)) + ); - assertEquals( new HashSet<>(Arrays.asList(evt3, evt2)), sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals( new HashSet<>(Arrays.asList(EVT_3, EVT_2)), sut.selectableEvents(bpss)); } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategyTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategyTest.java index 0ec58d59..9ab9c0b7 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategyTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBSyncEventSelectionStrategyTest.java @@ -1,5 +1,7 @@ package il.ac.bgu.cs.bp.bpjs.model.eventselection; +import il.ac.bgu.cs.bp.bpjs.TestUtils; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; import static org.junit.Assert.assertEquals; import java.util.Arrays; @@ -11,54 +13,53 @@ import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; public class PrioritizedBSyncEventSelectionStrategyTest { - private static final BEvent evt1 = new BEvent("evt1"); - private static final BEvent evt2 = new BEvent("evt2"); - private static final BEvent evt3 = new BEvent("evt3"); - private static final BEvent evt4 = new BEvent("evt4"); + private static final BEvent EVT_1 = new BEvent("evt1"); + private static final BEvent EVT_2 = new BEvent("evt2"); + private static final BEvent EVT_3 = new BEvent("evt3"); + private static final BEvent EVT_4 = new BEvent("evt4"); @Test public void testSelectableEvents_noBlocking() throws InterruptedException { PrioritizedBSyncEventSelectionStrategy sut = new PrioritizedBSyncEventSelectionStrategy(); - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make().request(Arrays.asList(evt4))); - stmts.add(SyncStatement.make().request(Arrays.asList(evt1)).data(5)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt2)).data(10)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt3)).data(10)); - - assertEquals(new HashSet<>(Arrays.asList(evt2, evt3)), - sut.selectableEvents(stmts, Collections.emptyList())); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_4))), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_1)).data(5)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_2)).data(10)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_3)).data(10)) + ); + assertEquals(new HashSet<>(Arrays.asList(EVT_2, EVT_3)), sut.selectableEvents(bpss)); } @Test public void testSelectableEvents_withBlocking() { PrioritizedBSyncEventSelectionStrategy sut = new PrioritizedBSyncEventSelectionStrategy(); - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make().request(Arrays.asList(evt4))); - stmts.add(SyncStatement.make().request(Arrays.asList(evt1)).data(5)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt2)).data(1)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt3)).data(10).block(evt2)); - - assertEquals(new HashSet<>(Arrays.asList(evt3)), - sut.selectableEvents(stmts, Collections.emptyList())); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_4))), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_1)).data(5)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_2)).data(1)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_3)).data(10).block(EVT_2)) + ); + assertEquals(new HashSet<>(Arrays.asList(EVT_3)), sut.selectableEvents(bpss)); } @Test public void testSelectableEvents_allBlocked() { PrioritizedBSyncEventSelectionStrategy sut = new PrioritizedBSyncEventSelectionStrategy(); - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make().request(Arrays.asList(evt4)).block(evt1)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt1)).data(5).block(evt2)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt2)).data(1).block(evt3)); - stmts.add(SyncStatement.make().request(Arrays.asList(evt3)).data(10).block(evt4)); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_4)).block(EVT_1)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_1)).data(5).block(EVT_2)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_2)).data(1).block(EVT_3)), + new MockBThreadSyncSnapshot(SyncStatement.make().request(Arrays.asList(EVT_3)).data(10).block(EVT_4)) + ); - assertEquals(Collections.emptySet(), - sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals(Collections.emptySet(), sut.selectableEvents(bpss)); } } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategyTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategyTest.java index dff8a2e7..b324cd18 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategyTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PrioritizedBThreadsEventSelectionStrategyTest.java @@ -1,16 +1,18 @@ package il.ac.bgu.cs.bp.bpjs.model.eventselection; +import il.ac.bgu.cs.bp.bpjs.TestUtils; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; import static org.junit.Assert.*; import java.util.Arrays; import java.util.Collections; import java.util.HashSet; -import java.util.Set; import org.junit.Test; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import org.junit.Before; public class PrioritizedBThreadsEventSelectionStrategyTest { @@ -33,64 +35,61 @@ public void setup() { @Test public void testSelectableEvents_noBlocking() throws InterruptedException { - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))); - stmts.add(SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))); - stmts.add(SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3))); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot("bt1", SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))), + new MockBThreadSyncSnapshot("bt2", SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))), + new MockBThreadSyncSnapshot("bt3", SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3))) + ); - assertEquals(new HashSet<>(Arrays.asList(EVT_3)), - sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals(new HashSet<>(Arrays.asList(EVT_3)), sut.selectableEvents(bpss)); } @Test public void testSelectableEvents_noBlocking_double() throws InterruptedException { - Set stmts = new HashSet<>(); - stmts.add(SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))); - stmts.add(SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))); - stmts.add(SyncStatement.make(bt("2a")).request(Arrays.asList(EVT_2A))); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot("bt1", SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))), + new MockBThreadSyncSnapshot("bt2", SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))), + new MockBThreadSyncSnapshot("bt2a", SyncStatement.make(bt("2a")).request(Arrays.asList(EVT_2A))) + ); + assertEquals(new HashSet<>(Arrays.asList(EVT_2, EVT_2A)), - sut.selectableEvents(stmts, Collections.emptyList())); + sut.selectableEvents(bpss)); } @Test public void testSelectableEvents_withBlocking() { - Set stmts = new HashSet<>(); - - stmts.add(SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))); - stmts.add(SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2)).block(EVT_3)); - stmts.add(SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3))); - + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot("bt1", SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))), + new MockBThreadSyncSnapshot("bt2", SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2)).block(EVT_3)), + new MockBThreadSyncSnapshot("bt3", SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3))) + ); assertEquals(new HashSet<>(Arrays.asList(EVT_2)), - sut.selectableEvents(stmts, Collections.emptyList())); + sut.selectableEvents(bpss)); } @Test public void testSelectableEvents_allBlocked() { - Set stmts = new HashSet<>(); - - stmts.add(SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1)).block(EVT_2)); - stmts.add(SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2)).block(EVT_3)); - stmts.add(SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3)).block(EVT_1)); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot("bt1", SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1)).block(EVT_2)), + new MockBThreadSyncSnapshot("bt2", SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2)).block(EVT_3)), + new MockBThreadSyncSnapshot("bt3", SyncStatement.make(bt("3")).request(Arrays.asList(EVT_3)).block(EVT_1)) + ); - - assertEquals( Collections.emptySet(), - sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals( Collections.emptySet(), sut.selectableEvents(bpss)); } - @Test public void testSelectableEvents_withBlocking_double() { - Set stmts = new HashSet<>(); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot("bt1", SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))), + new MockBThreadSyncSnapshot("bt2", SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))), + new MockBThreadSyncSnapshot("bt2a", SyncStatement.make(bt("2a")).request(Arrays.asList(EVT_2A))), + new MockBThreadSyncSnapshot("bt3", SyncStatement.make(bt("3")).block(EVT_2A)) + ); - stmts.add(SyncStatement.make(bt("1")).request(Arrays.asList(EVT_1))); - stmts.add(SyncStatement.make(bt("2")).request(Arrays.asList(EVT_2))); - stmts.add(SyncStatement.make(bt("2a")).request(Arrays.asList(EVT_2A))); - stmts.add(SyncStatement.make(bt("3")).block(EVT_2A)); - - assertEquals(new HashSet<>(Arrays.asList(EVT_2)), - sut.selectableEvents(stmts, Collections.emptyList())); + assertEquals(new HashSet<>(Arrays.asList(EVT_2)), sut.selectableEvents(bpss)); } @Test diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategyTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategyTest.java index 8c631496..c599af01 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategyTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/SimpleEventSelectionStrategyTest.java @@ -1,12 +1,15 @@ package il.ac.bgu.cs.bp.bpjs.model.eventselection; +import il.ac.bgu.cs.bp.bpjs.TestUtils; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import il.ac.bgu.cs.bp.bpjs.model.eventsets.ExplicitEventSet; import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; -import static java.util.Collections.emptyList; import static java.util.Collections.emptySet; import static java.util.Collections.singleton; import java.util.HashSet; @@ -38,109 +41,125 @@ public void setUp() { @Test public void testEmptySet() { + BProgramSyncSnapshot bpss = TestUtils.makeBPSS(); assertEquals(Optional.empty(), - sut.select(Collections.emptySet(), Collections.emptyList(), Collections.emptySet()) ); + sut.select(bpss, Collections.emptySet()) ); } @Test public void testNoStatementsWithExternalEvents() { List externals = Arrays.asList(BEvent.named("a"), BEvent.named("b")); EventSelectionStrategy ess = new SimpleEventSelectionStrategy(700); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS(); + bpss.getExternalEvents().addAll(externals); assertEquals(Collections.singleton(externals.get(0)), - ess.selectableEvents(Collections.emptySet(), externals) ); + ess.selectableEvents(bpss) ); } @Test public void testUnanimousCase() { BEvent expected = eventOne; - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).request(eventOne), - SyncStatement.make(null).request(eventOne).waitFor(eventTwo), - SyncStatement.make(null).request(eventOne) - )); - assertEquals(singleton(expected), sut.selectableEvents(sets, Collections.emptyList())); - assertEquals(Optional.of(new EventSelectionResult(expected)), sut.select(sets, Collections.emptyList(),singleton(eventOne))); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne).waitFor(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne)) + ); + assertEquals(singleton(expected), sut.selectableEvents(bpss)); + assertEquals(new EventSelectionResult(expected), + sut.select(bpss,singleton(eventOne)).get()); } @Test public void testWithBlockingCase() { BEvent expected = eventOne; - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).request(eventOne), - SyncStatement.make(null).request(eventTwo), - SyncStatement.make(null).block(eventTwo) - )); - assertEquals(singleton(expected), sut.selectableEvents(sets, Collections.emptyList())); - assertEquals(Optional.of(new EventSelectionResult(expected)), - sut.select(sets, Collections.emptyList(), singleton(expected))); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventTwo)) + ); + assertEquals(singleton(expected), sut.selectableEvents(bpss)); + assertEquals(new EventSelectionResult(expected), + sut.select(bpss, singleton(expected)).get()); } @Test public void testDeadlock() { ExplicitEventSet setOfEvt2 = new ExplicitEventSet(); setOfEvt2.add(eventTwo); - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).request(eventOne), - SyncStatement.make(null).request(setOfEvt2), - SyncStatement.make(null).block(eventTwo), - SyncStatement.make(null).block(eventOne) - )); - assertEquals(emptySet(), sut.selectableEvents(sets, Collections.emptyList())); - assertEquals(Optional.empty(), sut.select(sets, Collections.emptyList(), emptySet())); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(setOfEvt2)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventOne)) + ); + assertEquals(emptySet(), sut.selectableEvents(bpss)); + assertEquals(Optional.empty(), sut.select(bpss, emptySet())); } @Test public void testNoRequests() { - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).waitFor(eventOne), - SyncStatement.make(null).waitFor(eventTwo), - SyncStatement.make(null).block(eventTwo), - SyncStatement.make(null).block(eventOne) - )); - assertEquals(emptySet(), sut.selectableEvents(sets, Collections.emptyList())); - assertEquals(Optional.empty(), sut.select(sets, Collections.emptyList(), emptySet())); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).waitFor(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).waitFor(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventOne)) + ); + assertEquals(emptySet(), sut.selectableEvents(bpss)); + assertEquals(Optional.empty(), sut.select(bpss, emptySet())); } @Test public void testDeadlockWithExternals() { - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).request(eventOne), - SyncStatement.make(null).request(eventTwo), - SyncStatement.make(null).block(eventTwo), - SyncStatement.make(null).block(eventOne) - )); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).request(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventTwo)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).block(eventOne)) + ); List externals = Arrays.asList(eventOne, eventTri, eventTri, eventTwo); - assertEquals( singleton(eventTri), sut.selectableEvents(sets, externals)); - assertEquals( Optional.of(new EventSelectionResult(eventTri, singleton(1))), - sut.select(sets, externals, singleton(eventTri))); + bpss.getExternalEvents().addAll(externals); + assertEquals( singleton(eventTri), sut.selectableEvents(bpss)); + assertEquals( new EventSelectionResult(eventTri, singleton(1)), + sut.select(bpss, singleton(eventTri)).get()); } @Test public void testNoInternalRequests() { - Set sets = new HashSet<>(Arrays.asList(SyncStatement.make(null).waitFor(eventOne), - SyncStatement.make(null).waitFor(eventTri), - SyncStatement.make(null).waitFor(eventTwo) - )); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS( + new MockBThreadSyncSnapshot(SyncStatement.make(null).waitFor(eventOne)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).waitFor(eventTri)), + new MockBThreadSyncSnapshot(SyncStatement.make(null).waitFor(eventTwo)) + ); List externals = Arrays.asList(eventOne, eventTwo, eventTri, eventTwo); + bpss.getExternalEvents().addAll(externals); - assertEquals( singleton(eventOne), sut.selectableEvents(sets, externals)); - assertEquals(Optional.of( new EventSelectionResult(eventOne, singleton(0))), - sut.select(sets, externals, singleton(eventOne))); + assertEquals( singleton(eventOne), sut.selectableEvents(bpss)); + assertEquals( new EventSelectionResult(eventOne, singleton(0)), + sut.select(bpss, singleton(eventOne)).get()); } @Test public void testSeed() { Set events = IntStream.range(0, 1000).mapToObj( i -> BEvent.named("evt"+i) ).collect( toSet() ); - Set stmts = events.stream().map(e -> SyncStatement.make().request(e)).collect(toSet()); + Set btssSet = new HashSet<>(); + events.stream().map(e -> SyncStatement.make().request(e)) + .map( s->new MockBThreadSyncSnapshot(s)) + .forEach(btssSet::add); + BProgramSyncSnapshot bpss = TestUtils.makeBPSS(btssSet); // See what sut does List selectedBySut = new ArrayList<>(1000); for ( int i=0; i<1000; i++ ) { - selectedBySut.add( sut.select(stmts, emptyList(), events).get().getEvent() ); + selectedBySut.add( sut.select(bpss, events).get().getEvent() ); } // replicate with a strategy with the same seed EventSelectionStrategy sameSeedEss = new SimpleEventSelectionStrategy(sut.getSeed()); List selectedBySameSeed = new ArrayList<>(1000); for ( int i=0; i<1000; i++ ) { - selectedBySameSeed.add( sameSeedEss.select(stmts, emptyList(), events).get().getEvent() ); + selectedBySameSeed.add( sameSeedEss.select(bpss, events).get().getEvent() ); } assertEquals( selectedBySut, selectedBySameSeed ); From e082e4272baa1511fcd44186f147b066ba285e73 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 13:20:30 +0200 Subject: [PATCH 06/11] Refactor verification parts for re-usabilty --- README.md | 5 +- .../bp/bpjs/analysis/ArrayExecutionTrace.java | 116 +++++++++++++ .../bp/bpjs/analysis/DfsBProgramVerifier.java | 82 +++++---- .../bp/bpjs/analysis/DfsCycleInspection.java | 58 ------- .../cs/bp/bpjs/analysis/ExecutionTrace.java | 156 ++++++++++++++++++ ...ion.java => ExecutionTraceInspection.java} | 42 ++++- ...ns.java => ExecutionTraceInspections.java} | 137 +++++++-------- .../violations/DeadlockViolation.java | 12 +- .../violations/FailedAssertionViolation.java | 5 +- .../violations/HotBProgramCycleViolation.java | 18 +- .../violations/HotBThreadCycleViolation.java | 19 +-- .../violations/HotTerminationViolation.java | 5 +- .../bpjs/analysis/violations/Violation.java | 11 +- .../bgu/cs/bp/bpjs/mains/BPJsCliRunner.java | 18 +- .../java/il/ac/bgu/cs/bp/bpjs/TestUtils.java | 13 +- .../bp/bpjs/TicTacToe/TicTacToeVerMain.java | 8 +- .../analysis/DfsBProgramVerifierTest.java | 4 +- .../analysis/ExecutionTraceEntryTest.java | 95 +++++++++++ .../TemperatureVerificationsTest.java | 18 +- .../analysis/examples/DiningPhilTest.java | 15 +- .../cs/bp/bpjs/analysis/examples/Mazes.java | 16 +- .../bpjs/mains/CaseofTheHotFruitBProgram.java | 12 +- .../StateStorePerformanceComparison.java | 2 +- 23 files changed, 603 insertions(+), 264 deletions(-) create mode 100644 src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTrace.java delete mode 100644 src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java create mode 100644 src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTrace.java rename src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/{DfsTraceInspection.java => ExecutionTraceInspection.java} (54%) rename src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/{DfsInspections.java => ExecutionTraceInspections.java} (54%) create mode 100644 src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceEntryTest.java diff --git a/README.md b/README.md index f47fe1b0..fbe570ac 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,10 @@ a link to this page somewhere in the documentation/system about section. ## Change Log for the BPjs Library. -### 2019-02-04 +### 2019-02-06 +* :arrow_up::arrow_up::sparkles: Verification areas refactored and generalized towards code reuse. Inspectors and traces are now general, and do not assume they were created from the DFS verifier. + +### 2019-02-05 * :arrow_up: :tada: Event selection strategies now accept `BProgramSyncSnapshot`, rather than a set of sync statements and external events. ### 2019-02-04 diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTrace.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTrace.java new file mode 100644 index 00000000..da1f8dfe --- /dev/null +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ArrayExecutionTrace.java @@ -0,0 +1,116 @@ +/* + * The MIT License + * + * Copyright 2019 michael. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package il.ac.bgu.cs.bp.bpjs.analysis; + +import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgram; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** + * + * An {@link ArrayList}-backed {@link ExecutionTrace} implementation. Allows for + * relatively efficient runs in stack-based traversals. + * + * @author michael + */ +public class ArrayExecutionTrace implements ExecutionTrace { + + private final ArrayList stack = new ArrayList<>(); + + private int cycleToIndex = -1; + + private final BProgram bprogram; + + public ArrayExecutionTrace( BProgram aBProgram ) { + bprogram = aBProgram; + } + + @Override + public BProgram getBProgram() { + return bprogram; + } + + @Override + public int getStateCount() { + return stack.size(); + } + + @Override + public BProgramSyncSnapshot getLastState() { + return stack.get(stack.size()-1).getState(); + } + + @Override + public List getNodes() { + return Collections.unmodifiableList(stack); + } + + @Override + public boolean isCyclic() { + return cycleToIndex != -1; + } + + @Override + public int getCycleToIndex() { + return cycleToIndex; + } + + @Override + public List getFinalCycle() { + if ( isCyclic() ) { + return stack.subList(cycleToIndex, stack.size()); + } else { + return Collections.emptyList(); + } + } + + public void push( BProgramSyncSnapshot aState ) { + stack.add( new Entry(aState) ); + } + + public Entry pop() { + cycleToIndex = -1; + return stack.remove(stack.size()-1); + } + + public void advance( BEvent anEvent, BProgramSyncSnapshot nextState ){ + stack.get(stack.size()-1).setEvent(anEvent); + push( nextState ); + cycleToIndex = -1; + } + + public void cycleTo( BEvent anEvent, int aCycleToIndex ) { + stack.get(stack.size()-1).setEvent(anEvent); + cycleToIndex = aCycleToIndex; + } + + public void clear() { + stack.clear(); + cycleToIndex=-1; + } + +} diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java index 95b878a9..d9f48f5e 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java @@ -90,19 +90,19 @@ public ViolatingCycleFoundException(Violation v) { private long iterationCountGap = DEFAULT_ITERATION_COUNT_GAP; private BProgram currentBProgram; private boolean debugMode = false; - private final Set traceInspectors = new HashSet<>(); - private final Set cycleInspectors = new HashSet<>(); + private final Set inspections = new HashSet<>(); + private ArrayExecutionTrace trace; public VerificationResult verify(BProgram aBp) throws Exception { currentBProgram = aBp; visitedEdgeCount = 0; currentPath.clear(); visited.clear(); + trace = new ArrayExecutionTrace(currentBProgram); // in case no verifications were specified, use the defauls set. - if ( traceInspectors.isEmpty() && cycleInspectors.isEmpty() ) { - traceInspectors.addAll( DfsInspections.ALL_TRACE ); - cycleInspectors.add(DfsInspections.HotBThreadCycles ); + if ( inspections.isEmpty() ) { + inspections.addAll( ExecutionTraceInspections.DEFAULT_SET ); } ExecutorService execSvc = ExecutorServiceMaker.makeWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet()); @@ -127,8 +127,8 @@ protected Violation dfsUsingStack(DfsTraversalNode aStartNode, ExecutorService e DfsTraversalNode curNode = peek(); if (curNode != null) { - Optional res = traceInspectors.stream() - .map(v->v.inspectTrace(currentPath)) + Optional res = inspections.stream() + .map(v->v.inspectTrace(trace)) .filter(o->o.isPresent()).map(Optional::get) .findAny(); if ( res.isPresent() ) { @@ -179,23 +179,22 @@ protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorSe DfsTraversalNode possibleNextNode = src.getNextNode(nextEvent, execSvc); visitedEdgeCount++; if (visited.isVisited(possibleNextNode.getSystemState()) ) { - // Found a possible cycle - if ( !cycleInspectors.isEmpty() ) { - BProgramSyncSnapshot pns = possibleNextNode.getSystemState(); - final AtomicInteger idx = new AtomicInteger(); - for ( DfsTraversalNode nd : currentPath ){ - if ( pns.equals(nd.getSystemState()) ) { - // found an actual cycle - Optional res = cycleInspectors.stream().map(i->i.inspectCycle(currentPath, idx.intValue(), nextEvent)) - .filter(o->o.isPresent()).map(Optional::get) - .findAny(); - if ( res.isPresent() ) { - throw new ViolatingCycleFoundException(res.get()); - } + // Found a possible cycle + BProgramSyncSnapshot pns = possibleNextNode.getSystemState(); + + for ( int idx=0; idx res = inspections.stream().map(i->i.inspectTrace(trace)) + .filter(o->o.isPresent()).map(Optional::get) + .findAny(); + if ( res.isPresent() ) { + throw new ViolatingCycleFoundException(res.get()); } - idx.incrementAndGet(); - } - } + } + } } else { // advance to this newly discovered node return possibleNextNode; @@ -245,6 +244,16 @@ void printStatus(long iteration, List path) { private void push(DfsTraversalNode n) { visited.store(n.getSystemState()); currentPath.add(n); + if ( trace.getStateCount() == 0 ) { + trace.push( n.getSystemState() ); + } else { + trace.advance(n.getLastEvent(), n.getSystemState()); + } + } + + private void pop() { + currentPath.remove(currentPath.size() - 1); + trace.pop(); } private int pathLength() { @@ -259,10 +268,6 @@ private DfsTraversalNode peek() { return isPathEmpty() ? null : currentPath.get(currentPath.size() - 1); } - private DfsTraversalNode pop() { - return currentPath.remove(currentPath.size() - 1); - } - public boolean isDebugMode() { return debugMode; } @@ -271,27 +276,16 @@ public void setDebugMode(boolean debugMode) { this.debugMode = debugMode; } - public void addInspector( DfsTraceInspection ins ) { - traceInspectors.add(ins); + public void addInspection( ExecutionTraceInspection ins ) { + inspections.add(ins); } - public Set getTraceInspectors() { - return traceInspectors; + public Set getInspections() { + return inspections; } - public boolean removeInspector( DfsTraceInspection ins ) { - return traceInspectors.remove(ins); + public boolean removeInspection( ExecutionTraceInspection ins ) { + return inspections.remove(ins); } - public void addInspector( DfsCycleInspection ins ) { - cycleInspectors.add(ins); - } - - public Set getCycleInspectors() { - return cycleInspectors; - } - - public boolean removeInspector( DfsCycleInspection ins ) { - return cycleInspectors.remove(ins); - } } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java deleted file mode 100644 index 66ec4856..00000000 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java +++ /dev/null @@ -1,58 +0,0 @@ -/* - * The MIT License - * - * Copyright 2018 michael. - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in - * all copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN - * THE SOFTWARE. - */ -package il.ac.bgu.cs.bp.bpjs.analysis; - -import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; -import il.ac.bgu.cs.bp.bpjs.model.BEvent; -import java.util.List; -import java.util.Optional; - -/** - * - * a DFS inspection that verifies cycles in the b-program state graph. - * - * @author michael - */ -public interface DfsCycleInspection { - /** - * Inspects a cycle in the program graph for possible violations. - * - * For example, in the following graph: - * - * [a]-[b]-[c]-[d]--... - * \ | - * +-----+ (going from d back to b) - * - * - * This methods will be called with trace={@code [a][b][c][d]} and - * cycleToIdx={@code 1}. - * - * @param currentTrace Program trace up to this point. - * @param cycleToIdx The index of the node in the trace where the cycle returns - * @param event The event leading to the cycle at index {@code cycleToIdx}, from the end of {@code currentTrace}. - * @return A non-empty optional with the violation details, or an empty - * optional, if everything is fine. - */ - Optional inspectCycle( List currentTrace, int cycleToIdx, BEvent event); -} diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTrace.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTrace.java new file mode 100644 index 00000000..a2feb773 --- /dev/null +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTrace.java @@ -0,0 +1,156 @@ +/* + * The MIT License + * + * Copyright 2019 michael. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package il.ac.bgu.cs.bp.bpjs.analysis; + +import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgram; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import java.util.List; +import java.util.Objects; +import java.util.Optional; + +/** + * A trace of a single execution of a b-program. Contains the ordered sequence of + * states and events, and some methods for making common queries about it. + * + * @author michael + */ +public interface ExecutionTrace { + + /** + * A single entry in the trace. Contains a state, and an optional event. + * The event may be missing, if the node is the last in the trace (e.g. a + * run that got to a dead-end. + */ + public class Entry { + private final BProgramSyncSnapshot state; + private BEvent event; + + public Entry(BProgramSyncSnapshot state, BEvent event) { + this.state = state; + this.event = event; + } + + public Entry( BProgramSyncSnapshot aState ) { + this(aState, null); + } + + public BProgramSyncSnapshot getState() { + return state; + } + + public Optional getEvent() { + return Optional.ofNullable(event); + } + + public void setEvent(BEvent event) { + this.event = event; + } + + @Override + public String toString() { + return "[Trace.Entry state:" + state + ", event:" + event + ']'; + } + + @Override + public int hashCode() { + int hash = 7; + hash = 79 * hash + Objects.hashCode(this.event); + return hash; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) { + return true; + } + if (obj == null) { + return false; + } + if (getClass() != obj.getClass()) { + return false; + } + final Entry other = (Entry) obj; + if (!Objects.equals(this.event, other.event)) { + return false; + } + return Objects.equals(this.state, other.state); + } + + } + + /** + * @return The b-program {@code this} trace belongs to. + */ + BProgram getBProgram(); + + /** + * Number of states in the trace. Note that the trace can be inifinite, so + * no point calling this {@code length} or {@code size}. + * + * @return number of states in the trace. + */ + int getStateCount(); + + /** + * Returns the last state in the node list. Note that when a trace is cyclic, + * this will not be the last state in the actual execution, but rather the last + * event before returning to a previously visited state. + * + * @return last state in the node list. + * @see #isCyclic() + */ + BProgramSyncSnapshot getLastState(); + + /** + * Ordered list of all nodes in the state. In case of cycles, the last node + * in the list is the last before returning to a previously visited node. + * + * @return list of all nodes in the trace, by order. + */ + List getNodes(); + + /** + * @return {@code true} iff the trace ends with a cycle. + */ + boolean isCyclic(); + + /** + * The index of the node in {@link #getNodes} to which the cycle (if any) + * returns. In case the trace is a-cyclic, returns -1. + * + * @return the index of the return-to node, or -1. + * @see #isCyclic() + */ + int getCycleToIndex(); + + /** + * A list of the nodes in the final cycle, or an empty list if the trace + * is a-cyclic. + * + * @return A list of the nodes in the final cycle. + */ + List getFinalCycle(); +} + diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraceInspection.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspection.java similarity index 54% rename from src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraceInspection.java rename to src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspection.java index f2f226f5..1f0a1cc0 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraceInspection.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspection.java @@ -1,7 +1,7 @@ /* * The MIT License * - * Copyright 2018 michael. + * Copyright 2019 michael. * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal @@ -24,19 +24,47 @@ package il.ac.bgu.cs.bp.bpjs.analysis; import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; -import java.util.List; import java.util.Optional; +import java.util.function.Function; /** - * A class inspecting a b-program trace during DFS. + * A single inspection, detects violations in {@link ExecutionTrace}s. + * * @author michael */ -public interface DfsTraceInspection { +public interface ExecutionTraceInspection { + /** - * Inspects the current trace for violations. - * @param currentTrace The trace of the b-program, up to the current point. + * Utility method for composing inspections on the fly. + * @param aTitle title of the inspection + * @param f actual inspection function + * @return an inspection with the title and implementation passed. + */ + static ExecutionTraceInspection named(String aTitle, Function> f ) { + return new ExecutionTraceInspection() { + @Override + public String title() { + return aTitle; + } + + @Override + public Optional inspectTrace(ExecutionTrace aTrace) { + return f.apply(aTrace); + } + }; + } + + /** + * A human-readable title, used for listing and logs. + * @return inspection title. + */ + String title(); + + /** + * Inspects a trace for violations. + * @param aTrace The trace of the b-program execution. May be cyclic. * @return A non-empty optional with the violation details, or an empty * optional, if everything is fine. */ - Optional inspectTrace( List currentTrace ); + Optional inspectTrace( ExecutionTrace aTrace ); } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java similarity index 54% rename from src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java rename to src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java index f18ba4a6..eefe2593 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsInspections.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java @@ -1,7 +1,7 @@ /* * The MIT License * - * Copyright 2018 michael. + * Copyright 2019 michael. * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal @@ -25,14 +25,14 @@ import il.ac.bgu.cs.bp.bpjs.analysis.violations.DeadlockViolation; import il.ac.bgu.cs.bp.bpjs.analysis.violations.FailedAssertionViolation; -import il.ac.bgu.cs.bp.bpjs.analysis.violations.HotBThreadCycleViolation; import il.ac.bgu.cs.bp.bpjs.analysis.violations.HotBProgramCycleViolation; +import il.ac.bgu.cs.bp.bpjs.analysis.violations.HotBThreadCycleViolation; import il.ac.bgu.cs.bp.bpjs.analysis.violations.HotTerminationViolation; import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation; -import il.ac.bgu.cs.bp.bpjs.model.BEvent; import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BThreadSyncSnapshot; import java.util.Arrays; +import java.util.Collections; import java.util.HashSet; import java.util.List; import java.util.Optional; @@ -41,72 +41,91 @@ import static java.util.stream.Collectors.toSet; /** - * + * * A static collection of commonly used inspections. These objects can detect - * problems in a b-program, during a DFS traversal of its state space. + * problems in a b-program, during a traversal of its state space. * - * @see DfsBProgramVerifier * @author michael */ -public final class DfsInspections { - +public class ExecutionTraceInspections { + /** * Detects a deadlock in a b-program: where there are requested events, but * non of them is selectable. */ - public static final DfsTraceInspection Deadlock = (List trace) -> { - DfsTraversalNode curNode = peek(trace); - if (hasRequestedEvents(curNode.getSystemState()) && - curNode.getSelectableEvents().isEmpty()) { - return Optional.of(new DeadlockViolation(trace)); - } else return Optional.empty(); - }; - + public static final ExecutionTraceInspection DEADLOCKS = ExecutionTraceInspection.named( + "Deadlocks", + trace -> { + if ( trace.isCyclic() ) return Optional.empty(); + BProgramSyncSnapshot curState = trace.getLastState(); + if (hasRequestedEvents(curState) && + trace.getBProgram().getEventSelectionStrategy().selectableEvents(curState).isEmpty()) { + return Optional.of(new DeadlockViolation(trace)); + } else return Optional.empty(); + }); + /** * Detects when a b-thread calls an assertion which evaluates to {@code false}. - */ - public static final DfsTraceInspection FailedAssertions = (List trace) -> { - DfsTraversalNode curNode = peek(trace); - if (!curNode.getSystemState().isStateValid()) { - return Optional.of(new FailedAssertionViolation(curNode.getSystemState().getFailedAssertion(), trace)); - } else return Optional.empty(); - }; - + */ + public static final ExecutionTraceInspection FAILED_ASSERTIONS = ExecutionTraceInspection.named( + "Failed Assertions", + trace -> { + if ( trace.isCyclic() ) return Optional.empty(); + BProgramSyncSnapshot curState = trace.getLastState(); + if (!trace.getLastState().isStateValid()) { + return Optional.of(new FailedAssertionViolation(trace.getLastState().getFailedAssertion(), trace)); + } else return Optional.empty(); + }); + /** * Detects a case where a b-program ends, while one of its b-threads is in a * hot sync. */ - public static final DfsTraceInspection HotTermination = (List trace) -> { - DfsTraversalNode curNode = peek(trace); - if ( curNode.getSystemState().isHot() && - curNode.getSelectableEvents().isEmpty() ) { - Set hotlyTerminated = curNode.getSystemState().getBThreadSnapshots().stream() - .filter( s -> s.getSyncStatement().isHot() ).map( s->s.getName() ).collect( toSet() ); - return Optional.of( new HotTerminationViolation(hotlyTerminated, trace) ); - } else return Optional.empty(); - }; + public static final ExecutionTraceInspection HOT_TERMINATIONS = ExecutionTraceInspection.named( + "Hot Terminations", + trace -> { + if ( trace.isCyclic() ) return Optional.empty(); + BProgramSyncSnapshot curState = trace.getLastState(); + if ( curState.isHot() && + trace.getBProgram().getEventSelectionStrategy().selectableEvents(curState).isEmpty() ) { + Set hotlyTerminated = curState.getBThreadSnapshots().stream() + .filter( s -> s.getSyncStatement().isHot() ).map( s->s.getName() ).collect( toSet() ); + return Optional.of( new HotTerminationViolation(hotlyTerminated, trace) ); + } else return Optional.empty(); + } + ); /** * Detects a case where a b-program can get into an infinite loop where, at * each sync point, at least one of the b-threads is in a hot sync. This does * not mean that individually b-threads are hot all along the loop. */ - public static final DfsCycleInspection HotBProgramCycles = (List currentTrace, int cycleToIdx, BEvent event) -> { - if ( currentTrace.subList(cycleToIdx, currentTrace.size()).stream().allMatch(s -> s.getSystemState().isHot()) ){ - return Optional.of(new HotBProgramCycleViolation(currentTrace, cycleToIdx, event)); - } else return Optional.empty(); - }; + public static final ExecutionTraceInspection HOT_BPROGRAM_CYCLES = ExecutionTraceInspection.named( + "Hot B-Program Cycles", + trace -> { + if ( trace.isCyclic() && + trace.getFinalCycle().stream().allMatch(s -> s.getState().isHot()) ){ + return Optional.of(new HotBProgramCycleViolation(trace)); + } else return Optional.empty(); + } + ); /** * Detects a case where a b-thread can get into an infinite loop where all * its sync points are hot. - */ - public static final DfsCycleInspection HotBThreadCycles = new DfsCycleInspection() { + */ + public static final ExecutionTraceInspection HOT_BTHREAD_CYCLES = new ExecutionTraceInspection(){ @Override - public Optional inspectCycle(List currentTrace, int cycleToIdx, BEvent event) { - if ( peek(currentTrace).getSystemState().isHot() ) { - List cycle = currentTrace.subList(cycleToIdx, currentTrace.size()); - List> hots = cycle.stream().map( nd -> nd.getSystemState().getBThreadSnapshots() ) + public String title() { + return "Hot B-Program Cycles"; + } + + @Override + public Optional inspectTrace(ExecutionTrace trace) { + if ( trace.isCyclic() && + trace.getLastState().isHot() ) { + List cycle = trace.getFinalCycle(); + List> hots = cycle.stream().map( nd -> nd.getState().getBThreadSnapshots() ) .map( this::getHotThreadNames ) .collect( toList() ); @@ -117,41 +136,29 @@ public Optional inspectCycle(List currentTrace, int }); return alwaysHotOpt.filter( ahs -> ahs.size()>0 ) - .map( alwaysHots -> new HotBThreadCycleViolation(currentTrace, cycleToIdx, event, alwaysHots) ); + .map( alwaysHots -> new HotBThreadCycleViolation(trace, alwaysHots) ); } else return Optional.empty(); } - private Set getHotThreadNames( Set bts ) { + private Set getHotThreadNames( Set bts ) { return bts.stream().filter( bt -> bt.getSyncStatement().isHot() ) .map( bt -> bt.getName() ) .collect( toSet() ); } }; + + + static final Set DEFAULT_SET = Collections.unmodifiableSet( + new HashSet( + Arrays.asList( + DEADLOCKS, FAILED_ASSERTIONS, HOT_TERMINATIONS, HOT_BTHREAD_CYCLES + ))); - public static final List ALL_TRACE = Arrays.asList( - DfsInspections.Deadlock, - DfsInspections.FailedAssertions, - DfsInspections.HotTermination - ); - ///////////////////////// // Utility methods. private static boolean hasRequestedEvents(BProgramSyncSnapshot bpss) { return bpss.getBThreadSnapshots().stream().anyMatch(btss -> (!btss.getSyncStatement().getRequest().isEmpty())); } - - private static DfsTraversalNode peek(List trace) { - return trace.isEmpty() ? null : trace.get(trace.size()-1); - } - - - // / Utility methods. - ///////////////////////// - - - // Prevent instantiation. - private DfsInspections(){} - } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/DeadlockViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/DeadlockViolation.java index 56521ffc..f5447272 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/DeadlockViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/DeadlockViolation.java @@ -23,13 +23,13 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.internal.Pair; import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; import java.util.HashMap; import java.util.HashSet; -import java.util.List; import java.util.Map; import java.util.Set; import java.util.TreeSet; @@ -46,14 +46,14 @@ public class DeadlockViolation extends Violation { private final String description; - public DeadlockViolation(List counterExampleTrace) { + public DeadlockViolation(ExecutionTrace counterExampleTrace) { super(counterExampleTrace); - DfsTraversalNode last = counterExampleTrace.get(counterExampleTrace.size()-1); + BProgramSyncSnapshot last = counterExampleTrace.getLastState(); Map> requestedBy = new HashMap<>(); Map> blockedBy; // collect who requested what - last.getSystemState().getStatements().forEach( syncs -> { + last.getStatements().forEach( syncs -> { syncs.getRequest().forEach( evt -> { if ( ! requestedBy.containsKey(evt) ) { requestedBy.put(evt, new HashSet<>()); @@ -67,7 +67,7 @@ public DeadlockViolation(List counterExampleTrace) { // collect who blocked what blockedBy = requestedBy.keySet().stream().map( evt -> Pair.of( evt, - last.getSystemState().getStatements().stream().filter(s->isBlocking(s,evt)).map(s->s.getBthread().getName()).collect(toSet())) + last.getStatements().stream().filter(s->isBlocking(s,evt)).map(s->s.getBthread().getName()).collect(toSet())) ).collect( Collectors.toMap(p->p.getLeft(), p->p.getRight(), (s1, s2)->{ Set mergedSet = new TreeSet<>(); mergedSet.addAll(s1); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/FailedAssertionViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/FailedAssertionViolation.java index 0fa6fd75..5570c698 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/FailedAssertionViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/FailedAssertionViolation.java @@ -23,9 +23,8 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.model.FailedAssertion; -import java.util.List; /** * @@ -35,7 +34,7 @@ public class FailedAssertionViolation extends Violation { private final FailedAssertion assertion; - public FailedAssertionViolation(FailedAssertion assertion, List counterExampleTrace) { + public FailedAssertionViolation(FailedAssertion assertion, ExecutionTrace counterExampleTrace) { super(counterExampleTrace); this.assertion = assertion; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java index 02870ec5..5cc3b91c 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBProgramCycleViolation.java @@ -23,7 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.model.BEvent; import java.util.List; @@ -33,27 +33,23 @@ */ public class HotBProgramCycleViolation extends Violation { - private final int cycleToIndex; - private final BEvent event; - - public HotBProgramCycleViolation(List counterExampleTrace, int cycleToIndex, BEvent event) { - super(counterExampleTrace); - this.cycleToIndex = cycleToIndex; - this.event = event; + public HotBProgramCycleViolation(ExecutionTrace trace) { + super(trace); } @Override public String decsribe() { return "Hot b-program cycle violation: returning to index " + getCycleToIndex() - + " in the trace because of event " + event.toString(); + + " in the trace because of event " + getCycleToEvent(); } public int getCycleToIndex() { - return cycleToIndex; + return getCounterExampleTrace().getCycleToIndex(); } public BEvent getCycleToEvent() { - return event; + List nodes = getCounterExampleTrace().getNodes(); + return nodes.get(nodes.size()-1).getEvent().get(); } } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBThreadCycleViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBThreadCycleViolation.java index 525f5a2a..084c3bf2 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBThreadCycleViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotBThreadCycleViolation.java @@ -23,7 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.model.BEvent; import java.util.List; import java.util.Set; @@ -38,14 +38,10 @@ */ public class HotBThreadCycleViolation extends Violation { - private final int cycleToIndex; - private final BEvent event; private final Set bthreads; - public HotBThreadCycleViolation(List counterExampleTrace, int cycleToIndex, BEvent event, Set bthreads) { - super(counterExampleTrace); - this.cycleToIndex = cycleToIndex; - this.event = event; + public HotBThreadCycleViolation(ExecutionTrace trace, Set bthreads) { + super(trace); this.bthreads = bthreads; } @@ -53,16 +49,17 @@ public HotBThreadCycleViolation(List counterExampleTrace, int public String decsribe() { return "Hot b-thread cycle violation: b-threads " + (bthreads.stream().collect(joining(" ,"))) - + " can get to an infinite hot loop. Cycle returns to index " + cycleToIndex - + " because of event " + event; + + " can get to an infinite hot loop. Cycle returns to index " + getCounterExampleTrace().getCycleToIndex() + + " because of event " + getCycleToEvent(); } public int getCycleToIndex() { - return cycleToIndex; + return getCounterExampleTrace().getCycleToIndex(); } public BEvent getCycleToEvent() { - return event; + List nds = getCounterExampleTrace().getNodes(); + return nds.get(nds.size()-1).getEvent().get(); } public Set getBThreads() { diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotTerminationViolation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotTerminationViolation.java index c562b558..3f0ddfe6 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotTerminationViolation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/HotTerminationViolation.java @@ -23,8 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; -import java.util.List; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import java.util.Set; import static java.util.stream.Collectors.joining; @@ -36,7 +35,7 @@ public class HotTerminationViolation extends Violation { private final Set hotlyTerminated; - public HotTerminationViolation(Set hotlyTerminated, List counterExampleTrace) { + public HotTerminationViolation(Set hotlyTerminated, ExecutionTrace counterExampleTrace) { super(counterExampleTrace); this.hotlyTerminated = hotlyTerminated; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java index 59447dfb..8a01b3c7 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/violations/Violation.java @@ -23,8 +23,7 @@ */ package il.ac.bgu.cs.bp.bpjs.analysis.violations; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; -import java.util.List; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; /** * @@ -34,9 +33,9 @@ */ public abstract class Violation { - private List counterExampleTrace; + private ExecutionTrace counterExampleTrace; - public Violation(List counterExampleTrace) { + public Violation(ExecutionTrace counterExampleTrace) { this.counterExampleTrace = counterExampleTrace; } @@ -48,11 +47,11 @@ public Violation(List counterExampleTrace) { */ public abstract String decsribe(); - public List getCounterExampleTrace() { + public ExecutionTrace getCounterExampleTrace() { return counterExampleTrace; } - public void setCounterExampleTrace(List counterExampleTrace) { + public void setCounterExampleTrace(ExecutionTrace counterExampleTrace) { this.counterExampleTrace = counterExampleTrace; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java index bf7151fb..11454613 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java @@ -25,7 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.analysis.BThreadSnapshotVisitedStateStore; import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTraceInspections; import il.ac.bgu.cs.bp.bpjs.analysis.HashVisitedStateStore; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; @@ -43,8 +43,8 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.ArrayList; import java.util.Arrays; +import java.util.Optional; import java.util.logging.Level; import java.util.logging.Logger; import org.mozilla.javascript.EvaluatorException; @@ -122,9 +122,9 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { vfr.setVisitedNodeStore( new HashVisitedStateStore() ); } if ( switchPresent("--liveness", args) ) { - vfr.addInspector(DfsInspections.HotBProgramCycles); - vfr.addInspector(DfsInspections.HotBThreadCycles); - vfr.addInspector(DfsInspections.HotTermination); + vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); + vfr.addInspection(ExecutionTraceInspections.HOT_BTHREAD_CYCLES); + vfr.addInspection(ExecutionTraceInspections.HOT_TERMINATIONS); } String maxDepthStr = keyForValue("--max-trace-length", args); if ( maxDepthStr != null ) { @@ -152,9 +152,11 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { println(vio.decsribe()); println("Counter example trace:"); - vio.getCounterExampleTrace().stream() - .skip(1) // the first node has no previous event. - .forEach(nd -> println(nd.getLastEvent().toString())); + vio.getCounterExampleTrace().getNodes().stream() + .map( n -> n.getEvent() ) + .filter(Optional::isPresent) + .map(Optional::get) + .forEach(evt -> println(evt.toString())); } println("General statistics:"); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java index 20bd82e8..8ccdbfa3 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/TestUtils.java @@ -24,7 +24,7 @@ package il.ac.bgu.cs.bp.bpjs; import il.ac.bgu.cs.bp.bpjs.model.BEvent; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; import il.ac.bgu.cs.bp.bpjs.mocks.MockBProgramSyncSnapshot; import il.ac.bgu.cs.bp.bpjs.model.BProgram; @@ -36,7 +36,7 @@ import java.util.Collections; import java.util.HashSet; import java.util.List; -import java.util.Objects; +import java.util.Optional; import java.util.Set; import java.util.concurrent.ExecutionException; import java.util.concurrent.Future; @@ -59,10 +59,11 @@ public static String traceEventNamesString( VerificationResult res, String delim return res.getViolation().map(v->traceEventNamesString(v.getCounterExampleTrace(), delimiter)).orElse(""); } - public static String traceEventNamesString( List trace, String delimiter ) { - return trace.stream() - .map(DfsTraversalNode::getLastEvent) - .filter(Objects::nonNull) + public static String traceEventNamesString( ExecutionTrace trace, String delimiter ) { + return trace.getNodes().stream() + .map(ExecutionTrace.Entry::getEvent) + .filter(Optional::isPresent) + .map(Optional::get) .map(BEvent::getName) .collect(joining(delimiter)); } diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java index d770d718..343066fa 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/TicTacToe/TicTacToeVerMain.java @@ -5,7 +5,8 @@ import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; import il.ac.bgu.cs.bp.bpjs.model.eventselection.PrioritizedBSyncEventSelectionStrategy; import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTraceInspection; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTraceInspections; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; @@ -42,7 +43,7 @@ public static void main(String[] args) throws InterruptedException { // bprog.appendSource(infiBThread); try { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); - vfr.addInspector(DfsInspections.FailedAssertions); + vfr.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); vfr.setMaxTraceLength(70); // vfr.setDebugMode(true); @@ -54,7 +55,8 @@ public static void main(String[] args) throws InterruptedException { System.out.println("Found a counterexample"); res.getViolation().get() .getCounterExampleTrace() - .forEach(nd -> System.out.println(" " + nd.getLastEvent())); + .getNodes() + .forEach(nd -> System.out.println(" " + nd.getEvent())); } else { System.out.println("No counterexample found."); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java index 50cec996..1e361654 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifierTest.java @@ -118,7 +118,7 @@ public void deadlockTrace() throws Exception { public void testDeadlockSetting() throws Exception { BProgram program = new ResourceBProgram("DFSVerifierTests/deadlocking.js"); DfsBProgramVerifier sut = new DfsBProgramVerifier(); - sut.addInspector(DfsInspections.FailedAssertions); + sut.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); VerificationResult res = sut.verify(program); assertFalse(res.isViolationFound()); } @@ -147,7 +147,7 @@ public void testTwoSimpleBThreads() throws Exception { DfsBProgramVerifier sut = new DfsBProgramVerifier(); sut.setIterationCountGap(1); sut.setProgressListener(new PrintDfsVerifierListener()); - sut.addInspector(DfsInspections.FailedAssertions); + sut.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); VerificationResult res = sut.verify(bprog); assertFalse(res.isViolationFound()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceEntryTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceEntryTest.java new file mode 100644 index 00000000..34b0492e --- /dev/null +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceEntryTest.java @@ -0,0 +1,95 @@ +/* + * The MIT License + * + * Copyright 2019 michael. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package il.ac.bgu.cs.bp.bpjs.analysis; + +import static il.ac.bgu.cs.bp.bpjs.TestUtils.makeBPSS; +import il.ac.bgu.cs.bp.bpjs.mocks.MockBThreadSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.BEvent; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; +import il.ac.bgu.cs.bp.bpjs.model.SyncStatement; +import java.util.HashSet; +import java.util.Set; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertNotEquals; +import static org.junit.Assert.assertTrue; +import org.junit.Test; + +/** + * + * @author michael + */ +public class ExecutionTraceEntryTest { + + @Test + public void testSanity() { + BProgramSyncSnapshot bpss1 = makeBPSS(new MockBThreadSyncSnapshot(SyncStatement.make())); + BProgramSyncSnapshot bpss2 = makeBPSS(new MockBThreadSyncSnapshot(SyncStatement.make())); + BEvent evt1 = new BEvent("EVT1"); + BEvent evt2 = new BEvent("EVT2"); + + ExecutionTrace.Entry sut1 = new ExecutionTrace.Entry(bpss1, evt1); + ExecutionTrace.Entry sut2 = new ExecutionTrace.Entry(bpss2, evt2); + ExecutionTrace.Entry sut3 = new ExecutionTrace.Entry(bpss2, null); + + assertTrue( sut1.equals(sut1) ); + assertFalse( sut3.getEvent().isPresent() ); + assertEquals( bpss1, sut1.getState() ); + assertEquals( evt1, sut1.getEvent().get() ); + + Set evts = new HashSet<>(); + evts.add( sut1 ); + evts.add( sut1 ); + evts.add( sut2 ); + + assertEquals( 2, evts.size() ); + assertTrue( evts.contains(sut1) ); + assertTrue( evts.contains(sut2) ); + } + + @Test + public void testSetter() { + BProgramSyncSnapshot bpss1 = makeBPSS(new MockBThreadSyncSnapshot(SyncStatement.make())); + + BEvent evt1 = new BEvent("EVT1"); + BEvent evt2 = new BEvent("EVT2"); + + ExecutionTrace.Entry sut1 = new ExecutionTrace.Entry(bpss1, evt1); + ExecutionTrace.Entry sut2 = new ExecutionTrace.Entry(bpss1, evt2); + + assertNotEquals( sut1, sut2 ); + sut2.setEvent(evt1); + assertEquals( sut1, sut2 ); + } + + @Test + public void testToString() { + BProgramSyncSnapshot bpss = makeBPSS(new MockBThreadSyncSnapshot(SyncStatement.make())); + BEvent evt = new BEvent("EVT"); + ExecutionTrace.Entry sut = new ExecutionTrace.Entry(bpss, evt); + + assertTrue( sut.toString().contains("EVT") ); + + } +} diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java index 5a38a5df..53834131 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/TemperatureVerificationsTest.java @@ -50,7 +50,7 @@ public void testHotTermination() throws Exception{ final ResourceBProgram bprog = new ResourceBProgram("statementtemp/hotTerminationExample.js"); DfsBProgramVerifier vfr = new DfsBProgramVerifier(); - vfr.addInspector(DfsInspections.HotTermination); + vfr.addInspection(ExecutionTraceInspections.HOT_TERMINATIONS); final VerificationResult res = vfr.verify(bprog); assertTrue(res.isViolationFound()); @@ -68,7 +68,7 @@ public void testHotBProgramCycle_onHotBThreadCycle() throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default set will not be used. - vfr.addInspector(DfsInspections.HotBProgramCycles ); + vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); final VerificationResult res = vfr.verify(bprog); assertTrue(res.isViolationFound()); @@ -83,7 +83,7 @@ public void testHotBProgramCycle_onHotBThreadCycle() throws Exception { // The expected index is the length of the path, minus the cycle length // (which is 3 in our case) plus 1. - int expectedCycleToIndex = hcv.getCounterExampleTrace().size()-3; + int expectedCycleToIndex = hcv.getCounterExampleTrace().getStateCount()-3; assertEquals(expectedCycleToIndex, hcv.getCycleToIndex() ); } @@ -92,7 +92,7 @@ public void testHotBProgramCycle_withJsEventSets() throws Exception { BProgram bprog = new ResourceBProgram("DFSVerifierTests/fruitRatio.js"); DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default set will not be used. - vfr.addInspector(DfsInspections.HotBProgramCycles); + vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() ); final VerificationResult res = vfr.verify(bprog); @@ -107,7 +107,7 @@ public void testHotBThreadCycle() throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default is to run them all. - vfr.addInspector(DfsInspections.HotBThreadCycles ); + vfr.addInspection(ExecutionTraceInspections.HOT_BTHREAD_CYCLES); final VerificationResult res = vfr.verify(bprog); assertTrue(res.isViolationFound()); @@ -123,7 +123,7 @@ public void testHotBThreadCycle() throws Exception { // The expected index is the length of the path, minus the cycle length // (which is 3 in our case) plus 1. - int expectedCycleToIndex = htv.getCounterExampleTrace().size()-3; + int expectedCycleToIndex = htv.getCounterExampleTrace().getStateCount()-3; assertEquals(expectedCycleToIndex, htv.getCycleToIndex() ); } @@ -133,14 +133,14 @@ public void testHotBProgramCycle_onHotBProgramCycle() throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default is to run them all. - vfr.addInspector(DfsInspections.HotBProgramCycles ); + vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); final VerificationResult res = vfr.verify(bprog); assertTrue(res.isViolationFound()); assertTrue(res.getViolation().get() instanceof HotBProgramCycleViolation); HotBProgramCycleViolation hcv = (HotBProgramCycleViolation) res.getViolation().get(); assertEquals( "e", hcv.getCycleToEvent().getName() ); - int expectedCycleToIndex = hcv.getCounterExampleTrace().size()-3; + int expectedCycleToIndex = hcv.getCounterExampleTrace().getStateCount()-3; assertEquals(expectedCycleToIndex, hcv.getCycleToIndex() ); } @@ -150,7 +150,7 @@ public void testHotBThreadCycle_onHotBProgramCycle() throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default is to run them all. - vfr.addInspector(DfsInspections.HotBThreadCycles ); + vfr.addInspection(ExecutionTraceInspections.HOT_BTHREAD_CYCLES); final VerificationResult res = vfr.verify(bprog); assertFalse(res.isViolationFound()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java index 00a08eae..4d39230c 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/DiningPhilTest.java @@ -1,10 +1,10 @@ package il.ac.bgu.cs.bp.bpjs.analysis.examples; import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; -import java.util.List; +import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot; import static org.junit.Assert.fail; import org.junit.Test; @@ -29,12 +29,13 @@ public void testCounterexampleFound() throws InterruptedException { private static void printCounterExample(VerificationResult res) { System.out.println("Found a counterexample"); - final List trace = res.getViolation().get().getCounterExampleTrace(); - trace.forEach(nd -> System.out.println(" " + nd.getLastEvent())); + final ExecutionTrace trace = res.getViolation().get().getCounterExampleTrace(); + trace.getNodes().forEach(nd -> System.out.println(" " + nd.getEvent())); - DfsTraversalNode last = trace.get(trace.size() - 1); - System.out.println("selectableEvents: " + last.getSelectableEvents()); - last.getSystemState().getBThreadSnapshots().stream() + BProgramSyncSnapshot last = trace.getLastState(); + System.out.println("selectableEvents: " + trace.getBProgram().getEventSelectionStrategy() + .selectableEvents(last)); + last.getBThreadSnapshots().stream() .sorted((s1, s2) -> s1.getName().compareTo(s2.getName())) .forEach(s -> { System.out.println(s.getName()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java index 3d180f2e..454136e5 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/analysis/examples/Mazes.java @@ -29,9 +29,9 @@ import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; import il.ac.bgu.cs.bp.bpjs.execution.listeners.PrintBProgramRunnerListener; import il.ac.bgu.cs.bp.bpjs.model.BEvent; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode; import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTraceInspections; import il.ac.bgu.cs.bp.bpjs.analysis.Requirements; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; import il.ac.bgu.cs.bp.bpjs.analysis.listeners.PrintDfsVerifierListener; @@ -90,17 +90,17 @@ public void verify() throws InterruptedException { vfr.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); // vfr.setVisitedNodeStore(new ForgetfulVisitedStateStore()); - vfr.addInspector(DfsInspections.FailedAssertions); // prevent from detecting cases where we ust hit a wall. + vfr.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); // We only want failed assertions, deadlocks are OK here, in the greateer program(!) final VerificationResult res = vfr.verify(bprog); char[][] maze = getMaze(bprog); printMaze(maze); if (res.isViolationFound()) { System.out.println("Found a counterexample"); - for (DfsTraversalNode nd : res.getViolation().get().getCounterExampleTrace()) { - System.out.println(" " + nd.getLastEvent()); - if (nd.getLastEvent() != null) { - String name = nd.getLastEvent().getName(); + for (ExecutionTrace.Entry nd : res.getViolation().get().getCounterExampleTrace().getNodes()) { + System.out.println(" " + nd.getEvent()); + nd.getEvent().ifPresent( e -> { + String name = e.getName(); if (name.startsWith("Enter")) { String loc = name.split("\\(")[1].replace(")", "").trim(); String coord[] = loc.split(","); @@ -108,7 +108,7 @@ public void verify() throws InterruptedException { int row = Integer.parseInt(coord[1]); maze[row][col] = '•'; } - } + }); } printMaze(maze); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java index 9d19acb9..fb780949 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/CaseofTheHotFruitBProgram.java @@ -25,7 +25,7 @@ import il.ac.bgu.cs.bp.bpjs.analysis.BThreadSnapshotVisitedStateStore; import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier; -import il.ac.bgu.cs.bp.bpjs.analysis.DfsInspections; +import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTraceInspections; import il.ac.bgu.cs.bp.bpjs.analysis.VerificationResult; import il.ac.bgu.cs.bp.bpjs.analysis.violations.HotBProgramCycleViolation; import il.ac.bgu.cs.bp.bpjs.execution.BProgramRunner; @@ -33,6 +33,7 @@ import il.ac.bgu.cs.bp.bpjs.model.BProgram; import il.ac.bgu.cs.bp.bpjs.model.ResourceBProgram; import java.util.Objects; +import java.util.Optional; import static java.util.stream.Collectors.joining; /** @@ -58,7 +59,7 @@ public static void verify(BProgram bprog) throws Exception { DfsBProgramVerifier vfr = new DfsBProgramVerifier(); // Adding the inspector means it will be the only inspector run, as the default set will not be used. - vfr.addInspector(DfsInspections.HotBProgramCycles); + vfr.addInspection(ExecutionTraceInspections.HOT_BPROGRAM_CYCLES); vfr.setVisitedNodeStore( new BThreadSnapshotVisitedStateStore() ); final VerificationResult res = vfr.verify(bprog); @@ -68,9 +69,10 @@ public static void verify(BProgram bprog) throws Exception { System.out.println(v.decsribe()); System.out.println("Trace:"); HotBProgramCycleViolation hcv = (HotBProgramCycleViolation) v; - System.out.println(hcv.getCounterExampleTrace().stream() - .map(nd->nd.getLastEvent()) - .map(e -> Objects.toString(e)) + System.out.println(hcv.getCounterExampleTrace().getNodes().stream() + .map(nd->nd.getEvent()) + .filter( Optional::isPresent ) + .map(e -> Objects.toString(e.get())) .collect(joining("\n"))); System.out.println("Cycle-to Index:" + hcv.getCycleToIndex()); System.out.println("Cycle-to Event:" + hcv.getCycleToEvent()); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java index 2ba4caec..072a5c6e 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java @@ -58,7 +58,7 @@ public static void main(String[] args) throws Exception { // prepare verifier DfsBProgramVerifier verifier = new DfsBProgramVerifier(); - verifier.addInspector(DfsInspections.FailedAssertions); + verifier.addInspection(ExecutionTraceInspections.FAILED_ASSERTIONS); // test verifier.setVisitedNodeStore(new BThreadSnapshotVisitedStateStore()); From 9d14b67066da887030ef7a1d0a02b479799449f7 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 15:21:03 +0200 Subject: [PATCH 07/11] Comments and cleanup --- .../java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java | 3 ++- .../bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java index f910c882..2af80bfb 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/ContinuationGames.java @@ -45,7 +45,8 @@ import org.mozilla.javascript.ScriptRuntime; /** - * Playing around with continuations. + * Playing around with Rhino continuations. This file is for technical tests, + * and can be safely ignored by anyone not doing anything Rhino-related. * * @author michael */ diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java index 072a5c6e..6677febb 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/mains/StateStorePerformanceComparison.java @@ -85,7 +85,9 @@ private static void runVerifier(DfsBProgramVerifier vfr) throws Exception { for (int i = 0; i < HEAT_UP_ITERATIONS; i++) { vfr.verify(makeBProgram()); } + System.out.println("Iterating"); for (int i = 0; i < ITERATIONS; i++) { + System.out.println(" " + i + " of " + ITERATIONS ); VerificationResult res = vfr.verify(makeBProgram()); System.out.println(res.getTimeMillies()); } From 58ff82a99ab79bb5cecbe7f246a58eae2e594e37 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 15:37:40 +0200 Subject: [PATCH 08/11] More tests and cleanups --- README.md | 1 + .../bp/bpjs/analysis/DfsBProgramVerifier.java | 2 +- .../cs/bp/bpjs/analysis/DfsTraversalNode.java | 1 + .../bpjs/model/eventsets/EventSetsTest.java | 41 +++++++++++++++---- 4 files changed, 37 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index fbe570ac..78d31f3c 100644 --- a/README.md +++ b/README.md @@ -46,6 +46,7 @@ a link to this page somewhere in the documentation/system about section. ### 2019-02-06 * :arrow_up::arrow_up::sparkles: Verification areas refactored and generalized towards code reuse. Inspectors and traces are now general, and do not assume they were created from the DFS verifier. +* :arrow_up: More tests. ### 2019-02-05 * :arrow_up: :tada: Event selection strategies now accept `BProgramSyncSnapshot`, rather than a set of sync statements and external events. diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java index d9f48f5e..7223b8b3 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsBProgramVerifier.java @@ -108,7 +108,7 @@ public VerificationResult verify(BProgram aBp) throws Exception { ExecutorService execSvc = ExecutorServiceMaker.makeWithName("DfsBProgramRunner-" + INSTANCE_COUNTER.incrementAndGet()); long start = System.currentTimeMillis(); listenerOpt.ifPresent(l -> l.started(this)); - Violation vio = dfsUsingStack(DfsTraversalNode.getInitialNode(aBp, execSvc), execSvc); + Violation vio = dfsUsingStack(new DfsTraversalNode(currentBProgram, currentBProgram.setup().start(execSvc), null), execSvc); long end = System.currentTimeMillis(); listenerOpt.ifPresent(l -> l.done(this)); execSvc.shutdown(); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java index bcdbefbd..6a03115a 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsTraversalNode.java @@ -29,6 +29,7 @@ public class DfsTraversalNode { * @param exSvc The executor service that will run the threads * @return Initial node for the BProgram run * @throws Exception in case there's an error with the executed JavaScript code. + * @deprecated Use the inside code, this whole class might be going away soon. */ public static DfsTraversalNode getInitialNode(BProgram bp, ExecutorService exSvc) throws Exception { BProgramSyncSnapshot seed = bp.setup().start(exSvc); diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSetsTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSetsTest.java index 1c7798fa..f8978914 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSetsTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventsets/EventSetsTest.java @@ -34,20 +34,47 @@ */ public class EventSetsTest { - public EventSetsTest() { - } + private static final BEvent EVT_1 = new BEvent("EVT_1"); + private static final BEvent EVT_2 = new BEvent("EVT_2"); + private static final BEvent EVT_3 = new BEvent("EVT_3"); + private static final BEvent EVT_4 = new BEvent("EVT_4"); + private static final BEvent EVT_4_SAME = new BEvent("EVT_4"); /** * Test of allExcept method, of class EventSets. */ @Test public void testAllExcept() { - BEvent evtIn = new BEvent("In"); - BEvent evtOut = new BEvent("Out"); - EventSet es = EventSets.allExcept(evtOut); + EventSet es = EventSets.allExcept(EVT_4); + + assertFalse( es.contains(EVT_4) ); + assertFalse( es.contains(EVT_4_SAME) ); + assertTrue( es.contains(EVT_1) ); + assertTrue( es.contains(EVT_2) ); + assertTrue( es.contains(EVT_3) ); - assertFalse( es.contains(evtOut) ); - assertTrue( es.contains(evtIn) ); + assertTrue( es.toString().contains(EVT_4.getName()) ); + } + + @Test + public void testAll() { + assertTrue( EventSets.all.contains(EVT_1) ); + assertTrue( EventSets.all.contains(EVT_2) ); + assertTrue( EventSets.all.contains(EVT_3) ); + assertTrue( EventSets.all.contains(EVT_4) ); + assertTrue( EventSets.all.contains(EVT_4_SAME) ); + assertTrue( EventSets.all.toString().contains("All") ); + } + + @Test + public void testNone() { + // OK, quite anecdotal, but still. + assertFalse( EventSets.none.contains(EVT_1) ); + assertFalse( EventSets.none.contains(EVT_2) ); + assertFalse( EventSets.none.contains(EVT_3) ); + assertFalse( EventSets.none.contains(EVT_4) ); + assertFalse( EventSets.none.contains(EVT_4_SAME) ); + assertTrue( EventSets.none.toString().contains("none") ); } } From 88786029050045651c002ff9db2c5cca9450cd29 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 16:21:12 +0200 Subject: [PATCH 09/11] Fixed tests --- .../il/ac/bgu/cs/bp/bpjs/execution/BProgramRunnerTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunnerTest.java b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunnerTest.java index c4eb1c54..38a49945 100644 --- a/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunnerTest.java +++ b/src/test/java/il/ac/bgu/cs/bp/bpjs/execution/BProgramRunnerTest.java @@ -65,14 +65,14 @@ public void testRun() { public void testImmediateAssert() { BProgram bprog = new ResourceBProgram( "ImmediateAssert.js"); BProgramRunner runner = new BProgramRunner(bprog); - runner.run(); InMemoryEventLoggingListener listener = new InMemoryEventLoggingListener(); runner.addListener(listener); + + runner.run(); + FailedAssertion expected = new FailedAssertion("failRightAWay!", "forward"); assertEquals(expected, runner.getFailedAssertion()); assertEquals(0, listener.getEvents().size()); - - } From affd77821e4a1b136cb60e010cf82578b8d81a3e Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 16:35:18 +0200 Subject: [PATCH 10/11] Fixed a rejected execution error --- README.md | 1 + .../java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 78d31f3c..01ce877e 100644 --- a/README.md +++ b/README.md @@ -47,6 +47,7 @@ a link to this page somewhere in the documentation/system about section. ### 2019-02-06 * :arrow_up::arrow_up::sparkles: Verification areas refactored and generalized towards code reuse. Inspectors and traces are now general, and do not assume they were created from the DFS verifier. * :arrow_up: More tests. +* :bug: Fixed a corner case where b-programs with immediate failed assertions would still attempt running certain machines. ### 2019-02-05 * :arrow_up: :tada: Event selection strategies now accept `BProgramSyncSnapshot`, rather than a set of sync statements and external events. diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java index 89a43237..117a546d 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/BProgramSyncSnapshot.java @@ -282,7 +282,8 @@ private void executeAllAddedBThreads(Set nextRound, Executo // if any new bthreads are added, run and add their result Set addedBThreads = bprog.drainRecentlyRegisteredBthreads(); Set addedForks = bprog.drainRecentlyAddedForks(); - while ( ! (addedBThreads.isEmpty() && addedForks.isEmpty()) ) { + while ( ((!addedBThreads.isEmpty()) || (!addedForks.isEmpty())) + && !exSvc.isShutdown() ) { Stream threadStream = addedBThreads.stream() .map(bt -> new StartBThread(bt, listener)); Stream forkStream = addedForks.stream().flatMap( f -> convertToTasks(f, listener) ); From e4a7854a07d6f6160bd1783bd033692ea81ab797 Mon Sep 17 00:00:00 2001 From: Michael Bar-Sinai Date: Wed, 6 Feb 2019 17:36:07 +0200 Subject: [PATCH 11/11] Better hashing algorithm for visited state store. Documentation and POM upgrades. --- README.md | 3 +++ dependency-reduced-pom.xml | 4 ++-- docs/source/Examples_code/DfsVerifierSample.java | 7 ++++--- docs/source/verification/index.rst | 4 +++- pom.xml | 2 +- .../bpjs/analysis/ExecutionTraceInspections.java | 2 +- .../bp/bpjs/analysis/HashVisitedStateStore.java | 4 ++-- .../ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java | 16 +++++++++++----- .../model/internal/ContinuationProgramState.java | 6 +++--- 9 files changed, 30 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 01ce877e..b0240caa 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,10 @@ a link to this page somewhere in the documentation/system about section. ### 2019-02-06 * :arrow_up::arrow_up::sparkles: Verification areas refactored and generalized towards code reuse. Inspectors and traces are now general, and do not assume they were created from the DFS verifier. +* :arrow_up: Improved state hashing algorithm in the hash-based visited state storage. +* :arrow_up: Updated documentation of the verification parts. * :arrow_up: More tests. +* :arrow_up: Updated maven compiler plugin. * :bug: Fixed a corner case where b-programs with immediate failed assertions would still attempt running certain machines. ### 2019-02-05 diff --git a/dependency-reduced-pom.xml b/dependency-reduced-pom.xml index ccdaf4c1..151bd8b9 100644 --- a/dependency-reduced-pom.xml +++ b/dependency-reduced-pom.xml @@ -4,7 +4,7 @@ com.github.bthink-bgu BPjs BPjs - 0.9.7 + 0.9.8-SNAPSHOT Provides a runtime for behavioral programs written in Javascript. It can run stand-alone (from the commmandline) or be embedded in larger JVM-based systems. @@ -32,7 +32,7 @@ maven-compiler-plugin - 3.1 + 3.8.0 ${java.version} ${java.version} diff --git a/docs/source/Examples_code/DfsVerifierSample.java b/docs/source/Examples_code/DfsVerifierSample.java index 02e95f46..77ec5881 100644 --- a/docs/source/Examples_code/DfsVerifierSample.java +++ b/docs/source/Examples_code/DfsVerifierSample.java @@ -4,6 +4,7 @@ vrf.setProgressListener(new BriefPrintDfsVerifierListener()); // add a listener to print progress VerificationResult res = vrf.verify(program); // this might take a while -res.isCounterExampleFound(); // true iff a counter example was found -res.getViolationType(); // Failed assertion, or a deadlock -res.getCounterExampleTrace(); // trace of events leading to the violation. +res.isViolationFound(); // true iff a counter example was found +res.getViolation(); // an Optional +res.getViolation().ifPresent( v -> v.getCounterExampleTrace() ); + // ExecutionTrace leading to the violation. diff --git a/docs/source/verification/index.rst b/docs/source/verification/index.rst index a05c662f..1194a9f2 100644 --- a/docs/source/verification/index.rst +++ b/docs/source/verification/index.rst @@ -72,9 +72,11 @@ A more in-depth discussion of verification in BPjs, including some techniques, c From the Command Line ~~~~~~~~~~~~~~~~~~~~~ -To verify a b-program from the commandline, simply add the ``--verify`` switch. Use ``--full-state-storage`` to force the verification to use the full state data when determining whether a state was visited (requires more memory). +To verify a b-program from the commandline, simply add the ``--verify`` switch. Use ``--full-state-storage`` to force the verification to use the full state data when determining whether a state was visited (requires more memory). To concentrate on liveness violations, add the ``--liveness`` switch. To limit the (possibly infinite) depth of the scan, use ``--mac-trace-length``. $ java -jar bpjs.jar --verify hello-possibly-broken-world.js + $ java -jar bpjs.jar --verify --full-state-storage hello-possibly-broken-world.js + $ java -jar bpjs.jar --verify --liveness --full-state-storage hello-possibly-broken-world.js Assertions During Runtime diff --git a/pom.xml b/pom.xml index ecc3c560..28e73040 100644 --- a/pom.xml +++ b/pom.xml @@ -105,7 +105,7 @@ org.apache.maven.plugins maven-compiler-plugin - 3.1 + 3.8.0 ${java.version} ${java.version} diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java index eefe2593..394e4ee2 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/ExecutionTraceInspections.java @@ -149,7 +149,7 @@ private Set getHotThreadNames( Set bts ) { }; - static final Set DEFAULT_SET = Collections.unmodifiableSet( + public static final Set DEFAULT_SET = Collections.unmodifiableSet( new HashSet( Arrays.asList( DEADLOCKS, FAILED_ASSERTIONS, HOT_TERMINATIONS, HOT_BTHREAD_CYCLES diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java index 5bf35dcb..04f40857 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/HashVisitedStateStore.java @@ -46,9 +46,9 @@ public boolean isVisited(BProgramSyncSnapshot bss) { } private long hash( Set snapshots ) { - long hash = 0; + long hash = 1; for ( BThreadSyncSnapshot snp : snapshots ) { - hash = hash ^ snp.getContinuationProgramState().hashCode(); + hash = hash * snp.getContinuationProgramState().hashCode();// * (snp.getName().hashCode()+1); } return hash; } diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java index 11454613..18ca1118 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/mains/BPJsCliRunner.java @@ -138,15 +138,18 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { } println("Max trace length: " + vfr.getMaxTraceLength() ); + if ( vfr.getInspections().isEmpty() ) { + ExecutionTraceInspections.DEFAULT_SET.forEach(vfr::addInspection); + } + println("Inspections:"); + vfr.getInspections().forEach( ins -> println( " * " + ins.title())); + try { println("Starting verification"); VerificationResult res = vfr.verify(bpp); println("Verification completed."); - if ( ! res.getViolation().isPresent() ) { - println("No violations found"); - - } else { + if ( res.getViolation().isPresent() ) { Violation vio = res.getViolation().get(); println("Found Violation:"); println(vio.decsribe()); @@ -157,8 +160,11 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) { .filter(Optional::isPresent) .map(Optional::get) .forEach(evt -> println(evt.toString())); - + + } else { + println("No violations found"); } + println("General statistics:"); println(String.format("Time:\t%,d (msec)", res.getTimeMillies())); println(String.format("States scanned:\t%,d", res.getScannedStatesCount())); diff --git a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java index ef63b432..2dd56218 100644 --- a/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java +++ b/src/main/java/il/ac/bgu/cs/bp/bpjs/model/internal/ContinuationProgramState.java @@ -179,10 +179,10 @@ private Object getValue( Object instance, String fieldName ) throws NoSuchFieldE @Override public int hashCode() { - return Objects.hash(programCounter, frameIndex, - variables.entrySet().stream() + return 37 * (programCounter+1) * (frameIndex+1) * + (variables.entrySet().stream() .map( es->Objects.hash(es.getKey(), es.getValue()) ) - .collect( Collectors.reducing(0, (x,y)->x^y)) ); + .collect( Collectors.reducing(0, (x,y)->x*y))+1); } @Override