#! /usr/bin/python

###############################
# Author : Alexandre Mouradian
# year : 2013
###############################

#input : - infile.xml -> node TA
#		 - graph -> description of the topology

#output : outfile.xml -> NTA + query.q

#graph example :
#
#0 1 2 3 4 
#1 0 4 
#2 0 4 
#3 0 4 
#4 0 1 2 3

import sys
import copy

try:
	from lxml import etree as ElementTree
except ImportError, e:
	try:
		from elementtree import ElementTree
	except ImportError, e:
		print '***'
		print '*** Error: Must install either ElementTree or lxml.'
		print '***'
		raise ImportError, 'must install either ElementTree or lxml'

class Node:
	def __init__(self):
		self.neighbors=[]
		self.myCliques=[]
	ID=0
	rank=100
	mts=0

#global variables
V=0
graph=[]
cliques=[]

#Coen Bron and Joep Kerbosch. Algorithm 457 : Finding all cliques of an undirected graph. Commun. ACM, 16 :575{577, September 1973.
def BK(R, X, P, graph, cliques):
	if len(P) == 0 and len(X) == 0:
		cliques.append(tuple(R))
		return
	if len(P) == 0:
		return
	cP=copy.copy(P)
	for n in cP:
		sel = n
		P.remove(sel)
		newP = removeDisconnected(P[:], sel, graph)
		newX = removeDisconnected(X[:], sel, graph)
		cR=copy.copy(R)
		cR.append(sel)
		newR=cR
		BK(newR, newX, newP, graph, cliques)
		X.append(sel)
		if len(P) == 0:
			return
#remove the nodes that are not connected to sel and that are in N (it checks the connections in the graph)
def removeDisconnected(N, sel, graph):
	V=copy.copy(N)
	for j in V:
		found=False
		for k in range(len(graph[j].neighbors)):
			if graph[j].neighbors[k].ID==sel:
				found=True
		if found==False:
			N.remove(j)

	return N

def parseGraph(graphFile):#retreiving the graph from the file (parse two times)
	ifi=open(graphFile,'r')
	l=ifi.readline()
	i=0
	while l!="":#creates nodes
		ls=l.split()
		graph.append(Node())
		graph[i].ID=int(ls[0])
		i+=1
		l=ifi.readline()
	ifi=open(graphFile,'r')
	l=ifi.readline()
	i=0

	while l!="":#assigns neighbors to nodes
		ls=l.split()
		for j in range(1,len(ls)):
			for k in range(len(graph)):
				if graph[k].ID==int(ls[j]):
					graph[i].neighbors.append(graph[k])
		i+=1
		l=ifi.readline()

def setRank(node):#recursive algorithm that set the rank, call it with the sink as parameter
	for i in range(len(node.neighbors)):
		if node.neighbors[i].rank>node.rank+1:
			node.neighbors[i].rank=node.rank+1
			setRank(node.neighbors[i])

def setAutomata(inFileName, outFileName):
	V=len(graph)
	sysString1=""
	sysString2="system"
	docO = ElementTree.parse(inFileName)#the new templates will be added to this tree (O is for ouput)
	ntaO = docO.getroot()
	sol=ntaO.find("template")#find the original template
	ntaO.remove(sol) #remove the original template
	for i in range(0,V):#here the range will depend on the number of nodes in the network
		docC = ElementTree.parse(inFileName)
		ntaC = docC.getroot()
		children=ntaC.getchildren()
		for child in children:
			if child.tag!="template" and child.tag!="declaration":
				ntaC.remove(child)
			elif child.tag=="template":
				name=child.find("name")
				name.text=str(name.text)+str(i)#rename the template
				ntaO.insert(i+1,child)#insert it in the output tree
		if graph[i].mts==1:
			sysString1=sysString1+" n"+str(i)+" = "+"Template"+str(i)+"(1,"+str(graph[i].rank)+","+str(i)+")"+";"#strings which declare the system
		else:
			sysString1=sysString1+" n"+str(i)+" = "+"Template"+str(i)+"(0,"+str(graph[i].rank)+","+str(i)+")"+";"#strings which declare the system
		if i==0:
			sysString2=sysString2+" n"+str(i)
		else:
			sysString2=sysString2+", n"+str(i)
	sysString2=sysString2+";"
	system=ntaO.find("system")
	system.text=sysString1+sysString2
	declaration=ntaO.find("declaration")
	for j in range(len(cliques)):
		declaration.text=declaration.text+"broadcast chan chan"+str(j)+";\n"
	declaration.text=declaration.text+"int[0,"+str(V)+"] rank;"

	#in each template we have to search for synchronization transitions and replace each one by several group synchronization transitions. The group depend on the location of the node in the topology. We obtain the groups (maximal cliques) by applying BK algorithm on the network graph.  

	children=ntaO.getchildren()
	i=0
	for child in children:#search the first level (templates and co)
		if child.tag=="template":
			gchildren=child.getchildren()#search the edges and locations
			nbLoc=0
			for gchild in gchildren:
				if gchild.tag=="location":
					nbLoc+=1
				elif gchild.tag=="transition":#we are interessed in transitions
					tchildren=gchild.getchildren()
					for tchild in tchildren:
						if tchild.attrib.get('kind') is not None:
							if tchild.attrib.get('kind')=="synchronisation":#and in transitions
								if tchild.text[len(tchild.text)-1]=="?":
									gchild.remove(tchild)#remove tchild in order to remove the old channel name and put the new list
									for m in range(len(cliques)):
										for n in range(len(cliques[m])):
											if cliques[m][n]==i:
												newt=copy.copy(tchild)
												newt.text="chan"+str(m)+"?"
												newg=copy.copy(gchild)
												newg.append(newt)
												child.append(newg)
									child.remove(gchild) #remove the old transition
								elif tchild.text[len(tchild.text)-1]=="!":
									myCliques=[]
									for m in range(len(cliques)):
										for n in range(len(cliques[m])):
											if cliques[m][n]==i:
												myCliques.append(m);
									tchild.text="chan"+str(myCliques[0])+"!"
									if len(myCliques)>1:
										for k in range(1,len(myCliques)):#this loop creates the committed places
											loc=ElementTree.Element("location")
											loc.set('id',"id"+str(nbLoc-1+k))
											sloc=ElementTree.Element("committed")
											loc.insert(nbLoc-1+k+3,sloc)#uppaal don't like locations being in the middle of transitions declarations. The 3 is for name,  
											child.insert(nbLoc-1+k+3,loc)#declaration and parameter
										#here connect the transition to the first committed location
										trans=gchild.find("target")
										recTar=trans.get('ref')
										trans.set('ref',"id"+str(nbLoc))
										#then connecting the rest by adding transitions
										for k in range(1,len(myCliques)):
											trans=ElementTree.Element("transition")
											target=ElementTree.Element("target")
											if k<len(myCliques)-1:
												target.set('ref',"id"+str(nbLoc+k))
											else:
												target.set('ref',recTar)
											source=ElementTree.Element("source")
											source.set('ref',"id"+str(nbLoc-1+k))
											label=ElementTree.Element("label")
											label.set('kind',"synchronisation")
											label.text="chan"+str(myCliques[k])+"!"
											trans.append(source)
											trans.append(target)
											trans.append(label)
											child.append(trans)

			i+=1						
	docO.write(outFileName)#write the tree in the output file
	

def main():
	args = sys.argv[1:]
	if len(args) != 3:
		print 'usage: python test.py infile.xml outfile.xml graphFile.xml'
		sys.exit(-1)
	parseGraph(sys.argv[3])
	ofiQueries=open("testout-LB.q",'w')

	graph[0].rank=0
	V=len(graph)

	setRank(graph[0])

	nodeList=[]
	for i in range(len(graph)):
		nodeList.append(graph[i].ID)

	#these two loops aim at selecting the sender of the packet
	maxRank=0
	maxRankID=0
	for i in range(len(graph)):#search a node with a maximum rank value
		if maxRank<graph[i].rank:
			maxRank=graph[i].rank
			maxRankID=graph[i].ID

	for i in range(len(graph)):#then find the node and put mts value at one
		if maxRankID==graph[i].ID:
			graph[i].mts=1
	
	ofiQueries.write("A[] n0.m imply (z>"+str(maxRank*3)+" and z<="+str((maxRank+1)*5)+")\n")
	print "NB", V

	BK([],[],nodeList,graph,cliques)
	setAutomata(args[0],args[1])

if __name__ == '__main__':
    main()