#!/usr/bin/python3

import spot
from collections import defaultdict
from pprint import pprint

def ba_to_dict(aut):
    assert aut.prop_state_acc() and aut.acc().is_buchi()
    # If AP={a,b,c}, the alphabet is 2^AP, but edges are
    # labeled by Boolean formulas over AP (e.g. "a&(b|c)")
    # representing not one letter but a subset of the alphabet.
    # Calling split_edges() replaces an edge labeled by a&(b|c)
    # replace edge labeled by three edges labeled a&b&!c, a&!b&c, and a&b&c,
    # effectively causing the edges to be labeled by elements of the
    # alphabet.
    aut = spot.split_edges(aut)
    ap = aut.ap_vars()
    trans = defaultdict(list)
    alphabet = set()
    for edge in aut.edges():
        letter = str(spot.bdd_to_formula(edge.cond))
        trans[(edge.src, letter)].append(edge.dst)
        alphabet.add(letter)
    n = aut.num_states()
    acc = [s for s in range(n) if aut.state_is_accepting(s)]
    return { 'trans' : trans,
             'alphabet': alphabet,
             'acc' : acc,
             'init' : aut.get_init_state_number() }

aut = spot.translate('(a U b & FGc) | Gb', 'BA')

print(aut.to_str('hoa'))

pprint(ba_to_dict(aut))