import sys


def generate_players(f, N: int):
    for i in range(1, N+1):
        f.write(f"""
player p{i}
    girl{i}
endplayer
""")


def generate_secrets(f, N: int):
    for g in range(1, N+1):
        f.write(f'\n// Girl{g}\'s secrets\n')
        for s in range(1, N+1):
            f.write(f'global g{g}s{s} : bool init {str(g == s).lower()};\n')


def generate_shorthands(f, N: int):
    f.write('\n// Handy shorthands\n')
    for g in range(1, N+1):
        for s in range(1, N+1):
            f.write(f'formula g{g}g{(g%N)+1}s{s} = g{g}s{s} | g{(g%N)+1}s{s};\n')
        if g != N:
            f.write('\n')


def generate_labels(f, N: int):
    f.write('\n// Labels\n')
    for g in range(1, N+1):
        f.write(f'label "omniscient{g}" = ')
        for s in range(1, N+1):
            f.write(f'g{g}s{s}')
            if s != N:
                f.write(' & ')
        f.write(';\n')
    f.write('label "allomniscient" = ')
    for g in range(1, N+1):
        for s in range(1, N+1):
            f.write(f'g{g}s{s}')
            if g != N or s != N:
                f.write(' & ')
    f.write(';\n')


def generate_round_counter(f, N: int):
    f.write("""\n// Round counting
const int roundmax = 20;
global round : [0..roundmax] init 0;

module counter
	[] round<=roundmax -> (round'=min(round+1,roundmax));
endmodule
""")


def generate_modules(f, N: int):
    for g in range(1, N+1):
        if g == 1:
            f.write(f"""
// Modules
module girl1
    [_1call_left] round <= roundmax -> true;
    [_1call_right] round <= roundmax -> true;
endmodule

""")
        else:
            f.write(f'module girl{g} = girl1 [_1call_left =_{g}call_left,_1call_right = _{g}call_right] endmodule\n')


def generate_specific_synchronization(sync, f, N: int):
    f.write('\t')
    f.write(str([(f'_{i+1}call_right', f'_{i+1}call_left')[int(sync[i])] for i in range(N)]).replace('\'', ''))
    f.write(' true ->')
    updates = [i for i in range(N) if not sync[i] and sync[(i+1)%N]]
    if len(updates) == 0:
        f.write(' true')
    else:
        f.write('\n')
        for i in updates:
            f.write('\t\t')
            g1 = i+1
            g2 = (i+1)%N + 1
            for g in [g1, g2]:
                for s in range(1, N+1):
                    f.write(f'(g{g}s{s}\' = g{g1}g{g2}s{s})')
                    if s != N:
                        f.write(' & ')
                if g != g2:
                    f.write(' &\n\t\t')
            if i != updates[-1]:
                f.write(' &\n')
    f.write(';\n')


def gen_sync_rec(sync, n: int, f, N: int):
    if n == 0:
        generate_specific_synchronization(sync, f, N)
    else:
        gen_sync_rec(sync + [True], n-1, f, N)
        gen_sync_rec(sync + [False], n-1, f, N)

def generate_synchronizations(f, N: int):
    f.write('\n// Synchronizations\nmodule channel\n')
    gen_sync_rec([], N, f, N)
    f.write('endmodule\n')


if __name__ == '__main__':
    if len(sys.argv) != 2:
        print('Usage: python generate-circ.py <N>')
        exit(1)
    N = int(sys.argv[1])
    if N <= 1:
        print('N must be greater than 1')
        exit(1)
    print(f'Generating circular network of {N} girls...')
    file_name = f'gossipping_girls_circular_{N}.prism'

    with open(file_name, 'w') as f:
        f.write("""// Gossipping Girls circular
// Generated by generate-circ.py

csg
""")
        generate_players(f, N)
        generate_secrets(f, N)
        generate_shorthands(f, N)
        generate_labels(f, N)
        generate_round_counter(f, N)
        generate_modules(f, N)
        generate_synchronizations(f, N)

        print(f'Successfully generated {file_name}')
