possible-exec-analysis

a, b = 0, 0
p, q = 1, 1

states = set()

new = 'NEW'
visited = 'VISITED'
no_steps = 'NO_STEPS'


def checker(a, b, p, q, thread_finished):
    state_str = f'[P{p},Q{q},{a},{b}]'

    if thread_finished:
        return None, no_steps, a, b, p, q
    if states.issuperset([state_str]):
        return state_str, visited, a, b, p, q
    states.add(state_str)
    return state_str, new, a, b, p, q


def p_step(a, b, p, q):
    if p == 1:
        a = 1
        p = 2
    elif p == 2:
        if b == 0:
            p = 3
    elif p == 3:
        p = 4
    elif p == 4:
        a = 0
        p = 1
    return checker(a, b, p, q, False)


def q_step(a, b, p, q):
    thread_finished = False
    if q == 1:
        b = 1
        q = 2
    elif q == 2:
        if a == 0:
            q = 4
        else:
            q = 3
    elif q == 3:
        b = 0
        q = 1
    elif q == 4:
        thread_finished = True
    return checker(a, b, p, q, thread_finished)


def bfs(a, b, p, q, state_from):
    global states, new, visited
    state_to, cont, p_res, q_res, a_res, b_res = p_step(a, b, p, q)
    append = ''

    if cont == visited:
        if state_from == state_to:
            append = ', loop'
        else:
            append = ', cycle in graph'
    if cont != no_steps:
        print(f'{state_from} -> {state_to} # P step{append}')
    else:
        print(f'# P terminated')

    if cont == new:
        bfs(p_res, q_res, a_res, b_res, state_to)

    state_to, cont, p_res, q_res, a_res, b_res = q_step(a, b, p, q)
    append = ''
    if cont == visited:
        if state_from == state_to:
            append = ', loop'
        else:
            append = ', cycle in graph'
    if cont != no_steps:
        print(f'{state_from} -> {state_to} # Q step{append}')
    else:
        print(f'# Unable to perform Q step from {state_from} - thread terminated')

    if cont == new:
        bfs(p_res, q_res, a_res, b_res, state_to)


states.add(f'[P{p},Q{q},{a},{b}]')
bfs(a, b, p, q, f'[P{p},Q{q},{a},{b}]')