Index

A

add_bthread() (bppy.model.bprogram.BProgram method) advance_bthreads() (bppy.model.bprogram.BProgram method) All (class in bppy.model.event_set)

AllExcept (class in bppy.model.event_set) analysis_thread() (in module bppy.model.b_thread) assertion_failed() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method)

B

b_thread() (in module bppy.model.b_thread) b_thread_added() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) b_thread_done() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) b_thread_removed() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) BEvent (class in bppy.model.b_event) bp_state_to_gym_space() (bppy.gym.bp_observation_space.BPObservationSpace method) (bppy.gym.simple_bp_observation_space.SimpleBPObservationSpace method) BPActionSpace (class in bppy.gym.bp_action_space) BPAssertionError BPEnv (class in bppy.gym.bp_env) BPObservationSpace (class in bppy.gym.bp_observation_space) bppy module bppy.analysis module bppy.analysis.bprogram_converter module bppy.analysis.dfs_bprogram_verifier module bppy.analysis.symbolic_bprogram_verifier module bppy.execution module bppy.execution.listeners module bppy.execution.listeners.b_program_runner_listener module bppy.execution.listeners.print_b_program_runner_listener module bppy.gym module bppy.gym.bp_action_space module bppy.gym.bp_env module bppy.gym.bp_observation_space module bppy.gym.simple_bp_observation_space module

bppy.model module bppy.model.b_event module bppy.model.b_thread module bppy.model.bprogram module bppy.model.event_selection module bppy.model.event_selection.event_selection_strategy module bppy.model.event_selection.experimental_smt_event_selection_strategy module bppy.model.event_selection.priority_based_event_selection_strategy module bppy.model.event_selection.rich_event_selection_strategy module bppy.model.event_selection.simple_event_selection_strategy module bppy.model.event_selection.smt_event_selection_strategy module bppy.model.event_selection.solver_based_event_selection_strategy module bppy.model.event_set module bppy.model.sync_statement module bppy.utils module bppy.utils.dfs module bppy.utils.exceptions module bppy.utils.weighted_sampling module bppy.utils.z3helper module BProgram (class in bppy.model.bprogram) BProgramConverter (class in bppy.analysis.bprogram_converter) BProgramRunnerListener (class in bppy.execution.listeners.b_program_runner_listener)

C

choice (class in bppy.model.sync_statement) close() (bppy.gym.bp_env.BPEnv method) collect_structure() (bppy.analysis.bprogram_converter.BProgramConverter method)

compute_bthread_state_space() (bppy.gym.simple_bp_observation_space.SimpleBPObservationSpace method) contains() (bppy.gym.bp_action_space.BPActionSpace method) (bppy.gym.bp_observation_space.BPObservationSpace method)

D

DFSBProgram (class in bppy.utils.dfs)

DFSBProgramVerifier (class in bppy.analysis.dfs_bprogram_verifier) DFSBThread (class in bppy.utils.dfs)

E

EmptyEventSet (class in bppy.model.event_set) ended() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) enqueue_external_event() (bppy.model.bprogram.BProgram method) event_selected() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method)

EventSelectionStrategy (class in bppy.model.event_selection.event_selection_strategy) EventSet (class in bppy.model.event_set) EventSetList (class in bppy.model.event_set) execution_thread() (in module bppy.model.b_thread) ExperimentalSMTEventSelectionStrategy() (in module bppy.model.event_selection.experimental_smt_event_selection_strategy)

F

from_jsonable() (bppy.gym.bp_observation_space.BPObservationSpace method)

G

get_key() (bppy.utils.dfs.Node method) get_state() (bppy.gym.bp_env.BPEnv method) (bppy.utils.dfs.DFSBThread method)

getVariables() (in module bppy.utils.z3helper)

H

halted() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method)

I

is_satisfied() (bppy.model.event_selection.event_selection_strategy.EventSelectionStrategy method) (bppy.model.event_selection.rich_event_selection_strategy.RichEventSelectionStrategy method) (bppy.model.event_selection.simple_event_selection_strategy.SimpleEventSelectionStrategy method) (bppy.model.event_selection.smt_event_selection_strategy.SMTEventSelectionStrategy method) (bppy.model.event_selection.solver_based_event_selection_strategy.SolverBasedEventSelectionStrategy method)

L

load_new_bthreads() (bppy.model.bprogram.BProgram method)

M

module bppy bppy.analysis bppy.analysis.bprogram_converter bppy.analysis.dfs_bprogram_verifier bppy.analysis.symbolic_bprogram_verifier bppy.execution bppy.execution.listeners bppy.execution.listeners.b_program_runner_listener bppy.execution.listeners.print_b_program_runner_listener bppy.gym bppy.gym.bp_action_space bppy.gym.bp_env bppy.gym.bp_observation_space bppy.gym.simple_bp_observation_space bppy.model bppy.model.b_event bppy.model.b_thread bppy.model.bprogram bppy.model.event_selection bppy.model.event_selection.event_selection_strategy bppy.model.event_selection.experimental_smt_event_selection_strategy bppy.model.event_selection.priority_based_event_selection_strategy bppy.model.event_selection.rich_event_selection_strategy bppy.model.event_selection.simple_event_selection_strategy bppy.model.event_selection.smt_event_selection_strategy bppy.model.event_selection.solver_based_event_selection_strategy bppy.model.event_set bppy.model.sync_statement bppy.utils bppy.utils.dfs bppy.utils.exceptions bppy.utils.weighted_sampling bppy.utils.z3helper

N

next_event() (bppy.model.bprogram.BProgram method) Node (class in bppy.utils.dfs)

NodeList (class in bppy.utils.dfs) np_random (bppy.gym.bp_observation_space.BPObservationSpace property)

O

options() (bppy.model.sync_statement.choice method)

P

PrintBProgramRunnerListener (class in bppy.execution.listeners.print_b_program_runner_listener)

printVars() (in module bppy.utils.z3helper) PriorityBasedEventSelectionStrategy (class in bppy.model.event_selection.priority_based_event_selection_strategy)

R

render() (bppy.gym.bp_env.BPEnv method) reset() (bppy.gym.bp_env.BPEnv method) RichEventSelectionStrategy (class in bppy.model.event_selection.rich_event_selection_strategy)

run() (bppy.model.bprogram.BProgram method) (bppy.utils.dfs.DFSBProgram method) (bppy.utils.dfs.DFSBThread method)

S

sample() (bppy.gym.bp_action_space.BPActionSpace method) (bppy.gym.bp_observation_space.BPObservationSpace method) (bppy.model.sync_statement.choice method) seed() (bppy.gym.bp_observation_space.BPObservationSpace method) select() (bppy.model.event_selection.event_selection_strategy.EventSelectionStrategy method) (bppy.model.event_selection.simple_event_selection_strategy.SimpleEventSelectionStrategy method) (bppy.model.event_selection.smt_event_selection_strategy.SMTEventSelectionStrategy method) (bppy.model.event_selection.solver_based_event_selection_strategy.SolverBasedEventSelectionStrategy method) selectable_events() (bppy.model.event_selection.priority_based_event_selection_strategy.PriorityBasedEventSelectionStrategy method) (bppy.model.event_selection.simple_event_selection_strategy.SimpleEventSelectionStrategy method) sequence_probability_nr_s() (in module bppy.utils.weighted_sampling) setup() (bppy.model.bprogram.BProgram method) shape (bppy.gym.bp_observation_space.BPObservationSpace property)

SimpleBPObservationSpace (class in bppy.gym.simple_bp_observation_space) SimpleEventSelectionStrategy (class in bppy.model.event_selection.simple_event_selection_strategy) SMTEventSelectionStrategy (class in bppy.model.event_selection.smt_event_selection_strategy) SolverBasedEventSelectionStrategy (class in bppy.model.event_selection.solver_based_event_selection_strategy) started() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) starting() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) step() (bppy.gym.bp_env.BPEnv method) super_step_done() (bppy.execution.listeners.b_program_runner_listener.BProgramRunnerListener method) (bppy.execution.listeners.print_b_program_runner_listener.PrintBProgramRunnerListener method) SymbolicBProgramVerifier (class in bppy.analysis.symbolic_bprogram_verifier) sync (class in bppy.model.sync_statement)

T

thread() (in module bppy.model.b_thread) tickets_without_bt() (bppy.utils.dfs.DFSBProgram static method)

to_jsonable() (bppy.gym.bp_observation_space.BPObservationSpace method) to_prism() (bppy.analysis.bprogram_converter.BProgramConverter method) toFloat() (in module bppy.utils.z3helper)

V

verify() (bppy.analysis.dfs_bprogram_verifier.DFSBProgramVerifier method) (bppy.analysis.symbolic_bprogram_verifier.SymbolicBProgramVerifier method)

visitor() (in module bppy.utils.z3helper)

W

weighted_sample_without_replacement() (in module bppy.utils.weighted_sampling)