Package il.ac.bgu.cs.bp.bpjs.execution.jsproxy

Class BProgramJsProxy

java.lang.Object
il.ac.bgu.cs.bp.bpjs.execution.jsproxy.SyncStatementBuilder
il.ac.bgu.cs.bp.bpjs.execution.jsproxy.BProgramJsProxy
All Implemented Interfaces:
Serializable
public class BProgramJsProxy extends SyncStatementBuilder implements Serializable
An object representing the BProgram context for JavaScript code. Methods in this object allow JavaScript code to register new BThreads, create events,write messages to the log etc.

Methods in the class are available to JavaScript code via the bp object, like so: 


 bp.log.info("I'm a log message!");
 var myEvent = bp.Event("My Event");
 bp.registerBThread(...);
Author:
michael
See Also:

  • Field Details

    • log

      public final BpLog log

    • all

      @Deprecated(forRemoval=true) public final EventSet all
      Deprecated, for removal: This API element is subject to removal in a future version.
      Deprecated - use eventSets.all

    • none

      @Deprecated(forRemoval=true) public final EventSet none
      Deprecated, for removal: This API element is subject to removal in a future version.
      Deprecated - use eventSets.none

    • eventSets

      public final EventSetsJsProxy eventSets

    • random

      public RandomProxy random
      Facility for creating random numbers. BPjs code should not use JavaScript's random facility, as it won't play well with model checking.

  • Constructor Details

    • BProgramJsProxy

      public BProgramJsProxy(BProgram aBProgram)

    • BProgramJsProxy

      public BProgramJsProxy(BProgram aBProgram, BpLog log)

  • Method Details

    • setCurrentBThread

      public static void setCurrentBThread(BProgramSyncSnapshot bpss, BThreadSyncSnapshot btss)

    • clearCurrentBThread

      public static void clearCurrentBThread()

    • getCurrentChanges

      public static MapProxy getCurrentChanges()

    • Event

      public BEvent Event(String name)
      Event constructor, called from JavaScript, hence the funny capitalization.
      Parameters:
      name - name of the event
      Returns:
      an event with the passed name.

    • Event

      public BEvent Event(String name, Object jsData)
      Event constructor, called from JavaScript, hence the funny capitalization.
      Parameters:
      name - name of the event
      jsData - Additional data for the object.
      Returns:
      an event with the passed name.

    • EventSet

      public JsEventSet EventSet(String name, Object predicateObj)

    • allExcept

      public EventSet allExcept(EventSet es)

    • registerBThread

      public void registerBThread(String name, Object data, org.mozilla.javascript.Function func)
      Called from JS to add BThreads with data.
      Parameters:
      name - Name of the registered BThread (useful for debugging).
      data - Data object for the b-thread.
      func - Script entry point of the BThread.
      See Also:

    • registerBThread

      public void registerBThread(String name, org.mozilla.javascript.Function func)
      Called from JS to add BThreads running function as their runnable code.
      Parameters:
      name - Name of the registered BThread (useful for debugging).
      func - Script entry point of the BThread.
      See Also:

    • registerBThread

      public void registerBThread(org.mozilla.javascript.Function func)
      Registers a BThread and gives it a unique name. Use when you don't care about the added BThread's name.
      Parameters:
      func - the BThread to add.
      See Also:

    • ASSERT

      public void ASSERT(boolean value, String message) throws FailedAssertionException
      If value is false, puts the entire program in an invalid state. This, in turn, would terminate it when it's being run, or discover a specification violation when it's being verified.

      note: I'd rather call it assert too, but that's a Java keyword, which complicates stuff.

      Parameters:
      value - The value of the assertion. When false, the program is declared in invalid state.
      message - Textual information about what caused the violation.
      Throws:
      FailedAssertionException - if value is false.

    • fork

      public void fork() throws org.mozilla.javascript.ContinuationPending
      Throws:
      org.mozilla.javascript.ContinuationPending

    • setInterruptHandler

      public void setInterruptHandler(Object aPossibleHandler)

    • sync

      public void sync(org.mozilla.javascript.NativeObject jsRWB, Object data)
      Specified by:
      sync in class SyncStatementBuilder

    • hot

      public SyncStatementBuilder hot(boolean isHot)
      Specified by:
      hot in class SyncStatementBuilder

    • synchronizationPoint

      protected void synchronizationPoint(org.mozilla.javascript.NativeObject jsRWB, Boolean hot, Object data)
      Where the actual Behavioral Programming synchronization point is done.
      Parameters:
      jsRWB - The JavaScript object {request:... waitFor:...}
      hot - True if this should be a "hot" synchronization point.
      data - Optional extra data the synchronizing b-thread may want to add.

    • convertToEventSet

      protected EventSet convertToEventSet(Object jsObject)

    • enqueueExternalEvent

      public BEvent enqueueExternalEvent(BEvent evt)
      Push a new event to the external event queue.
      Parameters:
      evt - The event to be pushed.
      Returns:
      the event being pushed.

    • setWaitForExternalEvents

      public void setWaitForExternalEvents(boolean newDaemonMode)
      Sets whether the BProgram will wait for external events when there's no internal event to choose.
      Parameters:
      newDaemonMode - true for making this a daemon; false otherwise.

    • isWaitForExternalEvents

      public boolean isWaitForExternalEvents()

    • getTime

      public long getTime()
      Returns:
      Returns the current time in milliseconds since 1/1/1970.

    • getThread

      public BThreadDataProxy getThread()

    • getStore

      public MapProxy getStore()

    • getJavaThreadName

      public String getJavaThreadName()
      Gets the name of the Java thread executing this b-thread at the moment. Useful for debugging Java runtime issues.
      Returns:
      the name of the Java thread executing this b-thread at the moment.

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • equals

      public boolean equals(Object obj)
      Proxies contain no state of their own, and provide a gateway to the Java environment the BProgram runs in. When comparing sync snapshots, we can encounter JS proxies when traversing the JS heap and stack. To prevent leaking the equality evaluation outside of the JavaScript, we do not check the equality of the BProgram this is a proxy of. Rather, we just check that the other object is a proxy too.
      Overrides:
      equals in class Object
      Parameters:
      obj - The object we compare to.
      Returns:
      true iff the other object is a BProgramJsProxy.