import itertools


def dump_arbiter_spec(N):
    """Generate arbiter specification for case of N lines."""
    output = "ENV: "+" ".join(["r"+str(i) for i in range(1, N+1)])+";\n"
    output += "SYS: "+" ".join(["g"+str(i) for i in range(1, N+1)])+";\n\n"

    output += "ENVINIT: "+" & ".join(["!r"+str(i) for i in range(1, N+1)])+";\n"
    output += "ENVTRANS:\n  "+"\n& ".join(["[](((r"+str(i)+" & !g"+str(i)+") | (!r"+str(i)+" & g"+str(i)+")) -> ((r"+str(i)+"' & r"+str(i)+") | (!r"+str(i)+"' & !r"+str(i)+")))" for i in range(1, N+1)])+";\n"
    output += "ENVGOAL:\n  "+"\n& ".join(["[]<>!(r"+str(i)+" & g"+str(i)+")" for i in range(1, N+1)])+";\n"

    output += "\nSYSINIT: "+" & ".join(["!g"+str(i) for i in range(1, N+1)])+";\n"
    output += "SYSTRANS:\n  "
    if N > 1:
        output += "\n& ".join(["[](!g"+str(i)+"' | !g"+str(j)+"')" for (i, j) in itertools.combinations(range(1, N+1), 2)])+"\n& "
    output += "\n& ".join(["[](((r"+str(i)+" & g"+str(i)+") | (!r"+str(i)+" & !g"+str(i)+")) -> ((g"+str(i)+" & g"+str(i)+"') | (!g"+str(i)+" & !g"+str(i)+"')))" for i in range(1, N+1)])+";\n"
    output += "SYSGOAL:\n  "+"\n& ".join(["[]<>((r"+str(i)+" & g"+str(i)+") | (!r"+str(i)+" & !g"+str(i)+"))" for i in range(1, N+1)])+";\n"
    return output