def compute_potentials(pa):
'''Computes the potential function for each state of the product automaton.
The potential function represents the minimum distance to a self-reachable
final state in the product automaton.
'''
assert 'v' not in pa.g
# add virtual node which connects to all initial states in the product
pa.g.add_node('v')
pa.g.add_edges_from([('v', p) for p in pa.init])
# create strongly connected components of the product automaton w/ 'v'
scc = list(nx.strongly_connected_components(pa.g))
dag = nx.condensation(pa.g, scc)
# get strongly connected component which contains 'v'
for k, sc in enumerate(scc[::-1]):
if 'v' in sc:
start = len(scc) - k - 1
break
assert 'v' in scc[start]
assert map(lambda sc: 'v' in sc, scc).count(True) == 1
# get self-reachable final states
pa.srfs = self_reachable_final_states_dag(pa, dag, scc, start)
# remove virtual node from product automaton
pa.g.remove_node('v')
assert 'v' not in pa.g
if not pa.srfs:
return False
# add artificial node 'v' and edges from the set of self reachable
# states (pa.srfs) to 'v'
pa.g.add_node('v')
for p in pa.srfs:
pa.g.add_edge(p, 'v', **{'weight': 0})
# compute the potentials for each state of the product automaton
lengths = nx.shortest_path_length(pa.g, target='v', weight='weight')
for p in pa.g:
pa.g.node[p]['potential'] = lengths[p]
# remove virtual state 'v'
pa.g.remove_node('v')
return True
评论列表
文章目录
