#! /bin/python

def joinstr(listofthings):
    return "".join(map(str,listofthings))

def encoder(V,A,E):
    nodes = E[0].split("_")
    startObject = "".join(("o",nodes[0],"L0_",nodes[1],"L1X"))
    counter = str(len(V)-1)
    return "".join(("/* Initial (and input) multiset */\n    @ms(in) = c",counter,", ",startObject, ";\n\n"))
   
def membraneStructure(V,A,E):
    structure = "[]'in " #inital membrane 
    for (v,i) in [ (v,i) for i in range(len(V)-1, 0, -1) for v in V if v != "0"]:
        # i is counting down from |V|-1 to 1 
        # v is each node not equal to 0, note the membranes appear in oposite order than the paper, but it doesnt matter.
        structure += joinstr(("]'n",v,"L",i," ]'eval "))
        structure = "[["+ structure 

    structure = "[ ["+ structure + "]'fin ]'skn" 
    return " /* membrane structure */\n    @mu = " + structure + ";\n/* note, this assumes that 0 is the start node */\n\n"


def semimakeRules(V, A, E):
    rules = "/* counter to dissolve the input membrane after |V| time steps. */\n"

    #get us out of i after V time steps
    for i in range(len(V)-1,0,-1):
        rules += joinstr(("[ c",i," --> c",i-1," ]'in;\n"))  #F2 \label{rule:agap:fcounter}
    rules += "[ c0 ]'in --> d2;\n" #F3 \label{rule:agap:fdisolver}
    
    
    rules += "/* traverse all paths in the graph starting from 0. (start node, s) */\n"
    #F1 \label{rule:agap:init_out2}
    for l in range(0,len(V)-1):
        i = str(l)
        j = str(l+1)
        k = str(l+2)
        for u in V:
            for v in V:
                if u+"_"+v in E :
                    rules += "[ o"+ u + "L"+i+"_"+v+"L"+j+"X --> o"+ u + "L"+i+"_"+v+"L"+j+", " #first make a copy that is not primed
                    for w in V: #then for all edges leaving v make an edge
                        if v+"_"+w in E:
                            rules += "o"+v+"L"+j+"_"+w+"L"+k+"X, "
                    rules = rules[:-2] #cut off the ", " from the end 
                    rules += " ]'in;\n" 

    rules += "/* The second phase we assume 2 is the Terminal node. */\n"
    rules += "/* First the rules for if any edge reaches the terminal node 1, make a yes object. */\n"
    for l in range(0,len(V)-1):
        i = str(l)
        j = str(l+1)
        for u in V:
            rules += "[ o"+u+"L"+i+"_2L"+j+" --> Y"+u+"L"+i+ "]'n2L"+j+";\n" #S4 \label{rule:agap:sMeetsAt}
        
    rules += "/* now the rules to evaluate a universal node. */\n"
    for l in range(1,len(V)):
        i = str(l-1)
        j = str(l)
        for u in V:
            for v in V:
                if v not in ["2"]: #the t node in the graph
                    rules += "[ o"+u+"L"+i+"_"+v+"L"+j+"_preN --> N"+u+"L"+i+" ]'eval;\n" #rule S5 \label{rule:first_prepN}
                    rules += "[ o"+u+"L"+i+"_"+v+"L"+j+"_preY --> Y"+u+"L"+i+" ]'eval;\n" #rule S6 \label{rule:evalpos_to_pos}
                    rules += "[ o"+u+"L"+i+"_"+v+"L"+j+"_preY --> o"+u+"L"+i+"_"+v+"L"+j+"_preN ]'n"+v+"L"+j+";\n" #rule S7  \label{rule:dissolveM}

                if v in A and v not in ["2"]:  #unversal node and not t
                    rules += "/* rule to evaluate when node is universal */\n"
                    rules += "[ o"+ u+"L"+i+"_"+v+"L"+j+" --> o"+u+"L"+i+"_"+v+"L"+j+"_preN ]'n"+v+"L"+j+";\n" #rule S8 \label{rule:first_prepN}
                    rules += "[ o"+u+"L"+i+"_"+v+"L"+j+"_preN --> o"+u+"L"+i+"_"+v+"L"+j+"_preY ]'n"+v+"L"+j+";\n" #rule S9  \label{rule:negPre_goto_yes}
                    rules += "[ Y"+v+"L"+j+" --> Y"+v+"L"+j+"W ]'n"+v+"L"+j+";\n" #rule S10 {rule:yes_wait} 
                    rules += "[ N"+v+"L"+j+" ]'n"+v+"L"+j+" --> #;\n" #rule S10 \label{rule:disovleN}
                    rules += "[ Y"+v+"L"+j+"W ]'n"+v+"L"+j+" --> #;\n" #rule S11 \label{rule:dissolveY}

                elif v not in A and v not in ["2"]: #existential rules and not t
                    rules += "/* rule to evaluate when node is universal */\n"
                    rules += "[ o"+ u+"L"+i+"_"+v+"L"+j+" --> o"+u+"L"+i+"_"+v+"L"+j+"_preY ]'n"+v+"L"+j+";\n" #rule S16 \label{rule:first_prepN:ext}
                    rules += "[ N"+v+"L"+j+" --> N"+v+"L"+j+"W ]'n"+v+"L"+j+";\n" #rule S17 {rule:yes_wait:ext}
                    rules += "[ Y"+v+"L"+j+" ]'n"+v+"L"+j+" --> #;\n" #rule S18 \label{rule:disovleN:ext}
                    rules += "[ N"+v+"L"+j+"W ]'n"+v+"L"+j+" --> #;\n" #rule S19 \label{rule:disovleY:ext} #hmm names got confused with all the editing 
   
    for l in range(0,len(V)):
        i = str(l)
        for u in V:
            rules += "/* counter rules */\n"
            rules += "[ d2 --> d1 ]'n"+u+"L"+i+";\n" #rule S13 \label{rule:counterDown} 
            rules += "[ d1 --> d0 ]'n"+u+"L"+i+";\n" #rule S13 \label{rule:counterDown}
            rules += "[ d0 ]'n"+u+"L"+i+" --> d0;\n" #rule S14 \label{rule:last_counter_disolve}
    
    rules += "[ d1 ]'eval --> d2;\n" #rule S15 \label{rule:finaldissrule}
    rules += "[ d0 ]'eval --> d2;\n" #rule S15 \label{rule:finaldissrule}

    ###
    ###
    ###
    rules += "/* the start vertex is existential */\n"
    rules += "[ N0L0 --> N0L0W ]'fin;\n" #rule S20  \label{rule:endnowait:ext}
    rules += "[ Y0L0 ]'fin --> yes;\n" #rule S21 \label{rule:yesdiss:ext}
    rules += "[ N0L0W ]'fin --> no;\n" #rule S22 \label{rule:nodiss:ext}


    return rules
   
   
if __name__ == "__main__":
    # note sigma is 0, 1 is S and 2 is T
    #also the 0_1 edge must be first in the list of edges
    
    #example that tests for propper foralls
    #YES
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ("3", "6" )
    #E = ("0_1", "1_3", "3_5", "3_6", "5_2", "5_7", "4_7", "1_4", "6_2")
    
    #example that tests for propper foralls 
    #NO
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ("1", "3", "6")
    #E = ("0_1", "1_3", "3_5", "3_6", "5_2", "5_7", "4_7", "1_4", "6_2")
    
    #niall example that tests for propper foralls and testing if different length paths affect it 
    #YES
    V = ("0", "1", "2", "3", "4", "5", "6", "7", "8")
    A = ("3", "6" )
    E = ("0_1", "1_3", "3_5", "3_6", "5_2", "5_7", "4_7", "1_4", "6_2", "7_8")
    
    #Marios example (variation1)
    #YES
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ("6")
    #E = ("0_1", "1_6", "1_3", "6_4", "6_5", "6_2", "6_3", "3_4", "3_5", "4_2", "2_5")
    
    #Marios example (variation2)
    #NO
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ("1", "6" )
    #E = ("0_1", "1_6", "1_3", "6_4", "6_5", "6_2", "6_3", "3_4", "3_5", "4_2", "2_5")
 
    #Example to test that dead ends work ok existential
    #YES
    #V = ("0", "1", "2", "3", "4", "5", "6", "7", "8")
    #A = ("1")
    #E = ("0_1", "1_2", "2_4", "4_5", "4_6", "4_7") 
    
    #Example to test that dead ends work ok existential
    #YES  
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ( "1" )
    #E = ("0_1", "1_3", "3_4", "2_5", "3_6", "3_2") 
    
    #Example to test that dead ends work ok universal
    #NO
    #V = ("0", "1", "2", "3", "4", "5", "6", "7")
    #A = ("1", "3", "4", "5")
    #E = ("0_1","1_3", "3_4", "3_5", "3_6", "3_2") 
 
    import cv
    import os.path
    import sys

    
    if len(sys.argv) < 2:
        sys.exit("usage: %s <output pli file> " %(sys.argv[0],))

    plifilePath = os.path.normpath(os.path.expanduser(sys.argv[1]))

    plifile = open ( plifilePath, 'w' )

    plifile.write("@model<transition>\n\n\n")
    plifile.write("/* semi uniform solution for the AGAP instance\n")
    plifile.write("V = "+ str(V) +"\n")
    plifile.write("E = "+ str(E) +"*/\n\n")
    plifile.write("def AGAP(n){\n\n") 
    plifile.write(membraneStructure(V,A,E))
    plifile.write(encoder(V,A,E))
    plifile.write(semimakeRules(V,A,E))
    plifile.write("}\n\n/* Main module */\n def main(){\n\n    call AGAP(%d);\n }" %len(V))
    plifile.close()