#!/usr/bin/env python3
"""
Doeblin word avoidability check (OG4 detector).

Given a host instance and a forbidden word in template symbols, builds a memory automaton
and decides if the forbidden word is avoidable along an infinite legal path.

Outputs:
- AVOIDABLE with a finite cycle witness if avoidable
- UNAVOIDABLE with a finite bound B on the longest avoidance length otherwise
"""
from __future__ import annotations
import json, argparse
from collections import defaultdict, deque
from typing import Dict, Any, Tuple

def load(p: str) -> Dict[str, Any]:
    with open(p,"r",encoding="utf-8") as f:
        return json.load(f)

def build_suffix(prev: Tuple[str,...], sym: str, k: int) -> Tuple[str,...]:
    nxt = prev + (sym,)
    if len(nxt) <= k:
        return nxt
    return nxt[-k:]

def main()->int:
    ap=argparse.ArgumentParser()
    ap.add_argument("--host_instance", required=True)
    ap.add_argument("--forbidden", required=True)
    args=ap.parse_args()

    inst=load(args.host_instance)
    states=inst["constraint_graph"]["states"]
    edges=inst["constraint_graph"]["edges"]

    forbidden=[s.strip() for s in args.forbidden.split(",") if s.strip()]
    if not forbidden:
        print("Empty forbidden word")
        return 2
    L=len(forbidden)
    k=L-1

    out_edges=defaultdict(list)
    for e in edges:
        out_edges[e["from"]].append(e)

    start=[(s, tuple()) for s in states]
    adj=defaultdict(list)
    nodes=set(start)
    q=deque(start)
    while q:
        gstate, suf=q.popleft()
        for e in out_edges[gstate]:
            sym=e["template"]
            if k==0:
                if [sym]==forbidden:
                    continue
                suf2=tuple()
            else:
                if list(suf + (sym,)) == forbidden:
                    continue
                suf2=build_suffix(suf, sym, k)
            node2=(e["to"], suf2)
            adj[(gstate,suf)].append((node2, e["id"], sym))
            if node2 not in nodes:
                nodes.add(node2)
                q.append(node2)

    color={}
    parent={}
    parent_edge={}
    def dfs(u):
        color[u]=1
        for v,eid,sym in adj.get(u,[]):
            if v not in color:
                parent[v]=u
                parent_edge[v]=(eid,sym)
                res=dfs(v)
                if res:
                    return res
            elif color[v]==1:
                cycle=[]
                cur=u
                cycle.append((eid,sym))
                while cur!=v:
                    cycle.append(parent_edge[cur])
                    cur=parent[cur]
                cycle.reverse()
                return cycle
        color[u]=2
        return None

    for s in start:
        if s not in color:
            cyc=dfs(s)
            if cyc:
                print("AVOIDABLE")
                print("cycle_edge_ids:", ",".join(x[0] for x in cyc))
                print("cycle_templates:", ",".join(x[1] for x in cyc))
                return 0

    indeg=defaultdict(int)
    for u in nodes:
        for v,_,_ in adj.get(u,[]):
            indeg[v]+=1
    topo=deque([u for u in nodes if indeg[u]==0])
    dist={u:0 for u in nodes}
    while topo:
        u=topo.popleft()
        for v,_,_ in adj.get(u,[]):
            if dist[v] < dist[u]+1:
                dist[v]=dist[u]+1
            indeg[v]-=1
            if indeg[v]==0:
                topo.append(v)
    B=max(dist.values()) if dist else 0
    print("UNAVOIDABLE")
    print("max_avoid_length_B:", B)
    return 0

if __name__=="__main__":
    raise SystemExit(main())
