Reachability Analysis¶

libmc also offers graph search methods, central to explicit model checking.

BFS and DFS¶

libmc.bfs() and libmc.dfs() implement a generic way to perform graph search.

Consider this example graph:

# initial states
I = [1, 2]

# transitions
T = {
        1:  [2, 4],
        2:  [5, 6],
        3:  [7],
        4:  [3, 7],
        5:  [9],
        6:  [7, 8],
        7:  [3, 4],
        8:  [5, 8],
        9:  [10],
        10: [7]
    }

To perform breadth-first and depth-first search, some key components have to be defined:

a search node to keep track of the current path by storing a pointer to the parent node

class Node:
    def __init__ (self, ID, parent=None):
        self.id = ID
        self.parent = parent

a mandatory successors() function, generating the set of successors to the given node

def successors (current):
    for successor in sorted(T[current.id]):
        yield Node(successor, current)

an optional cache() function, adding a node’s id to the cache
```
def cache (successor): Cache.add(successor.id)
```
an optional cached() function, checking if a given node’s id has been cached already
```
def cached (successor): return successor.id in Cache
```

an optional quit() function, returning True iff the target has been found

def quit (current):
    global numVisited
    numVisited = numVisited + 1

    if current.id == target:
        buildTrace(current)
        return True
    else:
        return False

To simplify repeated initialization of the global variables Cache, Stack and numVisited, the following function is defined:

def initialize ():
    return (
        [ Node(i) for i in I ], # Stack
        set(I),                 # Cache
        0                       # numVisited
    )

Finally, the function generating the trace in quit() is given below:

def buildTrace (node):
    global trace
    trace = []
    while True:
        trace = [ node.id ] + trace
        node = node.parent
        if node is None: break

A search on the example graph can now be performed by using the previously defined components.

target = 7

Breadth-First Search

Stack, Cache, numVisited = initialize()

bfs(Stack, successors, cache=cache, cached=cached, quit=quit)

assert numVisited == 7
assert trace == [1, 4, 7]

Depth-First Search

Stack, Cache, numVisited = initialize()

dfs(Stack, successors, cache=cache, cached=cached, quit=quit)

assert numVisited == 4
assert trace == [2, 6, 7]

Tarjan’s Algorithm¶

Tarjan’s algorithm is implemented in libmc.tarjan() and can be used to find strongly connected components in a graph:

# example graph (undirected)
nodes = [ 'A', 'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K' ]
edges = [
            ('A', 'B'), ('A', 'E'),
            ('B', 'D'), ('B', 'F'),
            ('C', 'F'),
            ('D', 'A'), ('D', 'H'), ('D', 'I'),
            ('E', 'D'),
            ('F', 'G'), ('F', 'J'),
            ('G', 'C'), ('G', 'K'),
            ('H', 'E'), ('H', 'H'),
            ('I', 'E'), ('I', 'J'),
            ('J', 'G'), ('J', 'K')
        ]

scc = tarjan(nodes, edges)

assert scc == [
    ['A', 'B', 'D', 'E', 'H', 'I'],
    ['C', 'F', 'G', 'J'],
    ['K']