bppy.model.event_selection package

Submodules

bppy.model.event_selection.event_selection_strategy module

class bppy.model.event_selection.event_selection_strategy.EventSelectionStrategy

Bases: 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.

abstract is_satisfied(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

eventBEvent

The event to be checked against the statement.

statementdict

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.

abstract select(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

statementslist

A list of bthread statements from which an event will be selected.

external_events_queuelist, 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

bppy.model.event_selection.experimental_smt_event_selection_strategy module

bppy.model.event_selection.experimental_smt_event_selection_strategy.ExperimentalSMTEventSelectionStrategy()

bppy.model.event_selection.priority_based_event_selection_strategy module

class bppy.model.event_selection.priority_based_event_selection_strategy.PriorityBasedEventSelectionStrategy(default_priority=0)

Bases: SimpleEventSelectionStrategy

Priority-based extension for SimpleEventSelectionStrategy, selecting the requested non-blocked event with the highest priority. If no priority is specified for an event, the default_priority attribute is used.

Attributes

default_priorityint

The default priority value to use if no priority is specified for an event.

selectable_events(statements)

Returns a set of possible events that can be selected from a list of bthread statements. Specifically, the method extracts requested non-blocked events, with the maximal priority value, from the provided bthreads statements.

Parameters

statementslist

A list of bthread statements from which to extract possible events.

Returns

set

A set of possible events that can be selected.

bppy.model.event_selection.rich_event_selection_strategy module

class bppy.model.event_selection.rich_event_selection_strategy.RichEventSelectionStrategy

Bases: SMTEventSelectionStrategy

A solver-based implementation of EventSelectionStrategy using z3 SMT solver. The strategy used is the one presented in the paper Executing Scenario-Based Specification with Dynamic Generation of Rich Events.

is_satisfied(event, statement)

Abstract method to check whether a given event satisfies the given sync statement, and the bthread should advance. For more information, see SMTEventSelectionStrategy.

bppy.model.event_selection.simple_event_selection_strategy module

class bppy.model.event_selection.simple_event_selection_strategy.SimpleEventSelectionStrategy

Bases: EventSelectionStrategy

A simple EventSelectionStrategy, which uniformly selects an event that is requested and not blocked. It advances all bthreads that requested or waited for the selected event.

is_satisfied(event, statement)

Checks whether a bthread should advance based on the selected event and its current sync statement. Specifically, It checks whether the statement requests or waits for the selected event.

Parameters

eventBEvent

The selected event to be checked against the statement.

statementdict

The bthread’s sync statement to check the selected event against.

Returns

bool

True if the statement requests or waits for the selected event while not blocking it, False otherwise.

select(statements, external_events_queue=[])

Selects the next event from the given statements and external events queue.

This method selects the next event uniformly at random from the set of selectable events If no events can be selected from the statements, an event from the external events queue will be selected (or None is returned if the queue is empty).

Parameters

statementslist

A list of bthreads sync statements from which an event will be selected.

external_events_queuelist, optional

A list of external events that may be selected.

Returns

BEvent or None

The selected event, or None if no event can be selected.

selectable_events(statements)

Returns a set of possible events that can be selected from a list of bthread statements. Specifically, the method extracts requested non-blocked events from the provided bthreads statements.

Parameters

statementslist

A list of bthreads sync statements from which to extract selectable events.

Returns

set

A set of events that can be selected.

bppy.model.event_selection.smt_event_selection_strategy module

class bppy.model.event_selection.smt_event_selection_strategy.SMTEventSelectionStrategy

Bases: SolverBasedEventSelectionStrategy

A solver-based implementation of EventSelectionStrategy using z3 SMT solver. The strategy used is the one presented in the paper Executing Scenario-Based Specification with Dynamic Generation of Rich Events, with the difference that b-threads are continued if the selected assignment is either requested or waited for. For the original strategy, see RichEventSelectionStrategy.

is_satisfied(event, statement)

Abstract method to check whether a given event satisfies the given sync statement, and the bthread should advance. For more information, see SMTEventSelectionStrategy.

select(statements, additional_statement=None)

Abstract method to select and return the bprogram’s next event. For more information, see SMTEventSelectionStrategy.

bppy.model.event_selection.solver_based_event_selection_strategy module

class bppy.model.event_selection.solver_based_event_selection_strategy.SolverBasedEventSelectionStrategy

Bases: EventSelectionStrategy

A base class used to represent a Solver based Event Selection Strategy. This is an abstract class that requires the implementation of select and is_satisfied methods.

abstract is_satisfied(event, statement)

Abstract method to check whether a given event satisfies the given sync statement, and the bthread should advance. For more information, see SMTEventSelectionStrategy.

abstract select(statements, external_events_queue=[])

Abstract method to select and return the bprogram’s next event. For more information, see SMTEventSelectionStrategy.

Module contents