Python Branch Statement Analyzer

This library provides three main functionalities:

Decompose the conditional statements in the body of a python function into a BranchTree representing the heirarchy of conditional guards.
Transform the conditional expression tree into a set of kripke structures where the labels for each state contain one combination of guard expression evaluations.
Instrument a function to save the state of the variables used in each conditional guard expression during evaluation.

An example usage of this library can be seen in the two room thermostat system, which is designed to be used in conjunction with psy-taliro to search for test inputs to cover all thermostat controller branches.

Usage

The following is an example using this library to determine which branch was taken during the function exection without observing the return value.

from bsa import BranchTree, instrument_function, active_branches

def func(x, y):
   if x <= 5:
      if y <= 20:
         return 1
      else:
         return 2
   else:
      if y <= 30:
         return 3
      else:
         return 4

trees = BranchTree.from_function(func)

assert len(trees) == 1

tree = trees[0]
kripkes = tree.as_kripke()

assert len(kripkes) == 1

kripke = kripkes[0]
instrumented = instrument_function(func)
variables, _ = instrumented(11, 20)
states = active_states(kripke, variables)

assert len(states) == 1

state = states[0]
labels = kripke.labels_for(state)

assert len(labels) == 2
assert Comparison.gt("x", 5, strict=True) in labels
assert Comparison.lt("y", 30, strict=False) in labels

Installation

This project is available for installation on PyPI using the command pip install branch-statement-analyzer. For most cases, we suggest using a virtual environment manager like Poetry, Pipenv, Hatch, or a full installation manager like Conda or Mamba.

Repository

The source code for this repository can be found here. Pull requests are always welcome, please see the contribution guide for more information.

Modules: