Kripke Module

Introduction

This module defines the Kripke structure used to represent the different branches of a potentially nested conditional expression. The labels for each state represent a single combination of evaluations for the conditional expression guards. For example, given the following simple function:

def example(x: int) -> int:
   if x <= 10:
      return x + 1  # s1
   else:
      return x - 5  # s2

the resulting Kripke structure will contain two states \(\{S_1, S_2\}\) representing the two possible outcomes of the evaluating the conditional statement with the labels, \(L(S_1)=\{x \leq 10\}\) and \(L(S_2) = \{x > 10\}\). For the more complex example:

def example2(x: int, y: int) -> int:
   if x <= 10:
      if y <= 20:
         return x + y  # s1
      else:
         return x - y  # s2
   else:
      if y >= 30:
         return y  # s3
      else:
         return x  # s4

the Kripke structure will have four states \(\{S_1, S_2, S_3, S_4\}\) with the labeling

• \(L(S_1)=\{x \leq 10, y \leq 20\}\)

• \(L(S_2)=\{x \leq 10, y > 20\}\)

• \(L(S_3)=\{x > 10, y \geq 30\}\)

• \(L(S_4)=\{x > 10, y < 30\}\)

An example of creating a Kripke structure can be seen below:

from bsa.kripke import Kripke, State

states = [State(), State(), State()]
initial = {
   state[0]: True,
   state[1]: False,
   state[2]: False,
}
labels = {
   state[0]: [
      "color = green",
      "timer <= 10"
   ],
   state[1]: [
      "color = yellow",
      "timer <= 5"
   ],
   state[2]: [
      "color = red",
      "timer <= 10"
   ],
}
edges = [
   (states[0], states[1]),
   (states[1], states[2]),
   (states[2], states[0]),
]

kripke = Kripke(states, initial, labels, edges)

Classes