Event selection strategies now accept BProgramSyncSnapshot as a param…

…eter

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.

src/main/java/il/ac/bgu/cs/bp/bpjs/analysis/DfsCycleInspection.java

@@ -42,7 +42,7 @@ public interface DfsCycleInspection {
      * <code>
      * [a]-[b]-[c]-[d]--...
      *       \      |
-     *        +-----+
+     *        +-----+ (going from d back to b)
      * </code>
      * 
      * This methods will be called with trace={@code [a][b][c][d]} and 

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<String> 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<Violation> inspectCycle(List<DfsTraversalNode> currentTrace, int
         }
 
         private Set<String> getHotThreadNames( Set<BThreadSyncSnapshot> 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<String> getHotThreadNames( Set<BThreadSyncSnapshot> 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<DfsTraversalNode> trace) {

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<BEvent> 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();
     }

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();

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<BEvent> possibleEvents = bprog.getEventSelectionStrategy().selectableEvents(cur.getStatements(), cur.getExternalEvents());
+                Set<BEvent> 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<EventSelectionResult> res = bprog.getEventSelectionStrategy().select(cur.getStatements(), cur.getExternalEvents(), possibleEvents);
+                    Optional<EventSelectionResult> res = bprog.getEventSelectionStrategy().select(cur, possibleEvents);
 
                     if ( res.isPresent() ) {
                         EventSelectionResult esr = res.get();

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<BProgramRunnerListener> listeners, BProgram bprog, Context ctxt) {
         Set<BThreadSyncSnapshot> 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<BThreadSyncSnapshot> getBThreadSnapshots() {
     }
 
     public Set<SyncStatement> 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();
     }

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);

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<EventSelectionResult> select(Set<SyncStatement> statements, List<BEvent> externalEvents, Set<BEvent> selectableEvents) {
+    public Optional<EventSelectionResult> select(BProgramSyncSnapshot bpss, Set<BEvent> selectableEvents) {
         if (selectableEvents.isEmpty()) {
             return Optional.empty();
         }
         BEvent chosen = new ArrayList<>(selectableEvents).get(rnd.nextInt(selectableEvents.size()));
-        Set<BEvent> requested = statements.stream()
+        Set<BEvent> requested = bpss.getStatements().stream()
                                           .filter((SyncStatement stmt) -> stmt != null)
                                           .flatMap((SyncStatement stmt) -> stmt.getRequest().stream())
                                           .collect(Collectors.toSet());
@@ -85,7 +85,7 @@ public Optional<EventSelectionResult> select(Set<SyncStatement> 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))));
         }
     }
 

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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent> externalEvents) {
-        return getDecorated().selectableEvents(statements, externalEvents);
+    public Set<BEvent> selectableEvents(BProgramSyncSnapshot bpss) {
+        return getDecorated().selectableEvents(bpss);
     }
 
     @Override
-    public Optional<EventSelectionResult> select(Set<SyncStatement> statements, List<BEvent> externalEvents, Set<BEvent> selectableEvents) {
-        return getDecorated().select(statements, externalEvents, selectableEvents);
+    public Optional<EventSelectionResult> select(BProgramSyncSnapshot bpss, Set<BEvent> selectableEvents) {
+        return getDecorated().select(bpss, selectableEvents);
     }
 
 }

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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent> externalEvents);
+    Set<BEvent> 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. 
+     * 
+     * <strong>In normal BP, the selected event (if any) has
+     * to be a member of {@code selectableEvents}.</strong>
+     * 
+     * @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<EventSelectionResult> select(Set<SyncStatement> statements, 
-                                          List<BEvent> externalEvents,
+    Optional<EventSelectionResult> select(BProgramSyncSnapshot bpss,
                                           Set<BEvent> selectableEvents );
 
 }

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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent> externalEvents) {
-        final Set<BEvent> selectableEvents = getDecorated().selectableEvents(statements, externalEvents);
+    public Set<BEvent> selectableEvents(BProgramSyncSnapshot bpss) {
+        final Set<BEvent> 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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent>
     }
 
     @Override
-    public Optional<EventSelectionResult> select(Set<SyncStatement> statements, List<BEvent> externalEvents, Set<BEvent> selectableEvents) {
-        Optional<EventSelectionResult> selectedEvent = getDecorated().select(statements, externalEvents, selectableEvents);
+    public Optional<EventSelectionResult> select(BProgramSyncSnapshot bpss, Set<BEvent> selectableEvents) {
+        Optional<EventSelectionResult> selectedEvent = getDecorated().select(bpss, selectableEvents);
         out.println("== Actual Event Selection ======");
         out.println( selectedEvent.toString() );
         out.println("================================");

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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent> externalEvents) {
+    public Set<BEvent> selectableEvents(BProgramSyncSnapshot bpss) {
+        Set<SyncStatement> statements = bpss.getStatements();
+        List<BEvent> externalEvents = bpss.getExternalEvents();
+
         if ( statements.isEmpty() ) {
             // Corner case, not sure this is even possible.
             return externalEvents.isEmpty() ? emptySet() : singleton(externalEvents.get(0));

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<EventSelectionResult> select(Set<SyncStatement> statements, List<BEvent> externalEvents, Set<BEvent> selectableEvents) {
-        Optional<EventSelectionResult> res = getDecorated().select(statements, externalEvents, selectableEvents);
+    public Optional<EventSelectionResult> select(BProgramSyncSnapshot bpss, Set<BEvent> selectableEvents) {
+        Optional<EventSelectionResult> res = getDecorated().select(bpss, selectableEvents);
         lock.readLock().lock();
         listener.eventSelectionPaused(this);
         lock.writeLock().lock(); // blocks while the read lock is locked.

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<BEvent> selectableEvents(Set<SyncStatement> statements, List<BEvent> externalEvents) {
+    public Set<BEvent> selectableEvents(BProgramSyncSnapshot bpss) {
+
+        Set<SyncStatement> statements = bpss.getStatements();
+        List<BEvent> externalEvents = bpss.getExternalEvents();
 
         EventSet blocked = ComposableEventSet.anyOf(statements.stream()
                 .filter( stmt -> stmt!=null )