Skip to content

Commit

Permalink
Merge pull request #10 from bThink-BGU/0.0.6
Browse files Browse the repository at this point in the history
updating docs
  • Loading branch information
tomyaacov authored Jul 19, 2023
2 parents b02b1e9 + 8881872 commit b289338
Show file tree
Hide file tree
Showing 22 changed files with 615 additions and 21 deletions.
34 changes: 33 additions & 1 deletion bppy/execution/listeners/b_program_runner_listener.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,44 +2,76 @@


class BProgramRunnerListener(ABC):

"""
Abstract Base Class representing a listener for :class:`BProgram <bppy.model.bprogram.BProgram>` execution events.
"""
@abstractmethod
def starting(self, b_program):
"""
Abstract method to handle the start of the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def started(self, b_program):
"""
Abstract method to handle the start of the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def super_step_done(self, b_program):
"""
Abstract method to handle the completion of a super-step of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def ended(self, b_program):
"""
Abstract method to handle the end of the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def assertion_failed(self, b_program):
"""
Abstract method to handle assertion failures in the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def b_thread_added(self, b_program):
"""
Abstract method to handle the addition of a bthread in the :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def b_thread_removed(self, b_program):
"""
Abstract method to handle the removal of a bthread in the :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def b_thread_done(self, b_program):
"""
Abstract method to handle the termination of a bthread in the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def event_selected(self, b_program, event):
"""
Abstract method to handle the selection of event during the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

@abstractmethod
def halted(self, b_program):
"""
Abstract method to handle the halting of the execution of a :class:`BProgram <bppy.model.bprogram.BProgram>`.
"""
pass

18 changes: 17 additions & 1 deletion bppy/execution/listeners/print_b_program_runner_listener.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,15 @@


class PrintBProgramRunnerListener(BProgramRunnerListener):

"""
This class implements the :class:`BProgramRunnerListener
<bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener>` interface, providing basic print
statements for specific events in the BProgram's execution.
"""
def starting(self, b_program):
"""
Prints "STARTED" when the BProgram execution is about to start.
"""
print("STARTED")

def started(self, b_program):
Expand All @@ -13,6 +20,9 @@ def super_step_done(self, b_program):
pass

def ended(self, b_program):
"""
Prints "ENDED" when the BProgram execution is about to start.
"""
print("ENDED")

def assertion_failed(self, b_program):
Expand All @@ -28,12 +38,18 @@ def b_thread_done(self, b_program):
pass

def event_selected(self, b_program, event):
"""
Prints the selected event when an event has been selected during the BProgram's execution.
"""
print(event)

def halted(self, b_program):
pass

def __init__(self):
"""
Initializes the PrintBProgramRunnerListener.
"""
super().__init__()


21 changes: 20 additions & 1 deletion bppy/model/b_event.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,25 @@
class BEvent:

"""
A class to represent a Behavioral Event (BEvent) object.
Attributes
----------
name : str
The name of the event.
data : dict
Additional data associated with the event.
"""
def __init__(self, name="", data={}):
"""
Constructs all the necessary attributes for the BEvent object.
Parameters
----------
name : str
The name of the event.
data : dict
Additional data associated with the event.
"""
self.name = name
self.data = data

Expand Down
3 changes: 3 additions & 0 deletions bppy/model/b_thread.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@


def b_thread(func):
"""
A decorator to wrap bthread generator with, in order to handle data transmission and bthread termination.
"""
def wrapper(*args):
while True:
m = None
Expand Down
92 changes: 91 additions & 1 deletion bppy/model/bprogram.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,44 @@


class BProgram:

"""
A class to represent a Behavioral Program (BProgram) object.
Attributes
----------
source_name : str
A file name from which bthreads are imported.
new_bt : list
A list of new bthreads that have not been loaded yet.
bthreads : list
A list of bthreads to be run in the BProgram.
event_selection_strategy : :class:`EventSelectionStrategy <bppy.model.event_selection.event_selection_strategy.EventSelectionStrategy>`
A strategy object to select events and advance bthreads.
listener : :class:`BProgramRunnerListener <bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener>`
A listener object to be invoked at the start and end of the program, and at each event selection.
variables : dict
A dictionary of variables declared in the source module (for SMT based event selection startegy).
tickets : list
A list of bthread tickets (used in execution).
external_events_queue : list
A queue to handle external events introduced into the BProgram.
"""
def __init__(self, bthreads=None, source_name=None, event_selection_strategy=None, listener=None):
"""
Constructs all the necessary attributes for the BProgram object.
Parameters
----------
bthreads : list, optional
A list of bthreads to be run in the BProgram.
source_name : str, optional
The module from which bthreads are imported. If this is provided,
the bthreads and variables from the source module will be imported when setup() is called.
event_selection_strategy : :class:`EventSelectionStrategy <bppy.model.event_selection.event_selection_strategy.EventSelectionStrategy>`, optional
An event selection strategy object.
listener : :class:`BProgramRunnerListener <bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener>`, optional
A bprogram listener object.
"""
self.source_name = source_name
self.new_bt = []
self.bthreads = bthreads
Expand All @@ -19,6 +55,12 @@ def __init__(self, bthreads=None, source_name=None, event_selection_strategy=Non
self.external_events_queue = []

def setup(self):
"""
Sets up the BProgram.
If a source file is provided, this method imports all bthreads and variables
into the BProgram. All bthreads are then loaded.
"""
if self.source_name:
self.bthreads = [o[1]() for o in getmembers(import_module(self.source_name)) if
isfunction(o[1]) and o[1].__module__ == self.source_name]
Expand All @@ -31,6 +73,16 @@ def setup(self):


def advance_bthreads(self,tickets, m):
"""
Advances bthreads based on the selected event (m), using the event selection strategy satisfactions criteria (e.g., event was requested or waited for).
Parameters
----------
tickets : list
A list of bthread tickets.
m : :class:`BEvent <bppy.model.b_event.BEvent>`
The selected event to be sent as message to the bthreads.
"""
if len(self.new_bt) > 0:
warnings.warn("Some new bthreads are not loaded and are not affecting the bprogram. Use the load_new_bthreads method to load them.", RuntimeWarning)
for l in tickets:
Expand All @@ -47,23 +99,53 @@ def advance_bthreads(self,tickets, m):
pass

def add_bthread(self, bt):
"""
Adds a new bthread to the BProgram (should be loaded after using :func:`load_new_bthreads <bppy.model.bprogram.BProgram.load_new_bthreads>`).
Parameters
----------
bt : Any
The bthread to be added.
"""
self.new_bt.append(bt)

def load_new_bthreads(self):
"""
Loads all new bthreads into the BProgram.
The method uses :func:`advance_bthreads <bppy.model.bprogram.BProgram.advance_bthreads>` to load bthreads.
"""
while len(self.new_bt) > 0:
new_tickets = [{'bt': bt} for bt in self.new_bt]
self.new_bt.clear()
self.advance_bthreads(new_tickets, None)
self.tickets.extend(new_tickets)

def next_event(self):
"""
Selects the next event in the BProgram using the event selection strategy.
If there are new bthreads that haven't been loaded, a warning will be raised.
Returns
-------
event : :class:`BEvent <bppy.model.b_event.BEvent>`
The selected event to be processed.
"""
if len(self.new_bt) > 0:
warnings.warn(
"Some new bthreads are not loaded and are not affecting the bprogram. Use the load_new_bthreads method to load them.",
RuntimeWarning)
return self.event_selection_strategy.select(self.tickets, self.external_events_queue)

def run(self):
"""
Runs the BProgram.
It sets up the BProgram, selects events, and advance the bthreads until no event can be selected
or until interrupted by the listener. At the start and end of the run, and after each
event selection, the listener (if provided) is invoked.
"""
if self.listener:
self.listener.starting(b_program=self)

Expand All @@ -88,4 +170,12 @@ def run(self):
self.listener.ended(b_program=self)

def enqueue_external_event(self, event):
"""
Enqueues an external event into the BProgram.
Parameters
----------
event : :class:`BEvent <bppy.model.b_event.BEvent>`
The external event to be enqueued.
"""
self.external_events_queue.append(event)
46 changes: 45 additions & 1 deletion bppy/model/event_selection/event_selection_strategy.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,55 @@


class EventSelectionStrategy(ABC):

"""
A base class used to represent an Event Selection Strategy. This is an abstract class
that requires the implementation of `select` and `is_satisfied` methods.
"""
@abstractmethod
def select(self, statements, external_events_queue=[]):
"""
Abstract method to select and return the bprogram's next event.
This method needs to be implemented in child classes. It takes a list of statements
and an external events queue, and should return the next event to be selected based
on the strategy being implemented.
Parameters
----------
statements : list
A list of bthread statements from which an event will be selected.
external_events_queue : list, optional
A list of external events that may be selected.
Returns
-------
Abstract
Returns the next event to be selected based on the strategy being implemented,
or `None` if no event can be selected
"""
pass

@abstractmethod
def is_satisfied(self, event, statement):
"""
Abstract method to check whether a given event satisfies the given sync statement, and the bthread should
advance.
This method needs to be implemented in child classes. It takes an event and a
statement, and should return a boolean indicating whether the event satisfies
the statement and the bthread should advance according to the strategy being implemented.
Parameters
----------
event : :class:`BEvent <bppy.model.b_event.BEvent>`
The event to be checked against the statement.
statement : dict
The statement to check the event against.
Returns
-------
Abstract
Returns a boolean indicating whether the event satisfies the statement
and the bthread should advance according to the strategy being implemented.
"""
pass
Loading

0 comments on commit b289338

Please sign in to comment.