#! /usr/bin/python
import numpy as np
import math
import sys
import os
import fractions
import copy
import subprocess
import string
import shutil

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

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

#output : file resultsN with TA verified and results (UPPAAL log)

#graph example :
#	
#p 0 48.1540811791 78.4171121718
#p 1 22.3034450305 86.8491780822
#p 2 73.2186900176 90.7916104965
#p 3 41.5013633282 49.1759685779
#p 4 46.5326056803 78.3737165383
#0 1 2 3 4 
#1 0 4 
#2 0 4 
#3 0 4 
#4 0 1 2 3 

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'


graph=[]
nMax=30
indMax=9
STEP=1.0
data=[]
dataBorder=[]
graph2=[]


class Node:
	def __init__(self):
		self.neighbors=[]
		self.interferers=[]
	ID=0
	rank=100
	coordinate=0
	mts=1
	x=0.0
	y=0.0	
	alphaKids=[0,0.0]#alarms considered as kid traffic for now
	alphaInt=[0,0.0]
	alphaOut=[0,0.0]
	checked=0
	bestNeighbor=-1
	toCheck=1


class Data:
	A=0
	B=0
	C=0

def parseGraph(graphFile):#retreiving the graph from the file (parse 2 times)
	ifi=open(graphFile,'r')
	l=ifi.readline()
	i=0
	while l!="":#creates nodes
		ls=l.split()
		if ls[0]=="p":
			graph.append(Node())
			graph[i].ID=int(ls[1])
			if int(ls[4])==1:
				graph[i].alphaKids=[1,1000.0]
			i+=1
		l=ifi.readline()
	ifi=open(graphFile,'r')
	l=ifi.readline()
	
	i=0
	while l!="":#assigns neighbors to nodes
		ls=l.split()
		if ls[0]!="p":
			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()

	ifi=open(graphFile,'r')
	l=ifi.readline()

	i=0
	while l!="":#assigns locations to nodes
		ls=l.split()
		if ls[0]=="p":
			graph[i].x=float(ls[2])
			graph[i].y=float(ls[3])
			i+=1
		l=ifi.readline()

def neighb2():#to be used on a copy of the graph: it is the 2hop connection graph
	for i in range(len(graph)):
		for j in range(len(graph[i].neighbors)):
			for k in range(len(graph)):
				if graph[k].ID==graph[i].neighbors[j].ID:
					for l in range(len(graph[k].neighbors)):
						if graph[k].neighbors[l].ID!=graph[i].ID:
							graph2[i].neighbors.append(copy.copy(graph[k].neighbors[l]))


def setRank(node):#recursive algorithm to set ranks, call 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 F(theta, cn, ci, R):
	inter=0.0
	ret=0.0
	inter=math.sqrt(pow(R,2)-pow((cn-1)*R+ci,2)*pow(math.cos(theta),2))
	ret=(((cn-1)*R+ci)/2)*(-math.cos(theta)*inter-(pow(R,2)*math.atan(((cn-1)*R+ci)*math.cos(theta)/inter))/((cn-1)*R+ci));
	return ret

#init RTXP coordinates data 
def initData():
	
		
	for i in range(nMax+1):
		c=[]
		d=[]
		for j in range(indMax+1):
			c.append(Data())
			d.append(Data())
		data.append(c)
		dataBorder.append(d)


	xc1=0.0
	yc1=0.0
	xc2=0.0
	yc2=0.0
	i=0.0
	A=0.0
	C=0.0
	B=0.0
	pA=0.0
	pC=0.0
	pB=0.0
	R=10.0
	n=1
	
	while n<nMax:
		i=0.0
		while i<R:
			if not (n==1 and i==0.0):
				if n!=1:
					yc1=(pow((n-1)*R,2)-pow(R,2)+pow((n-1)*R+i,2))/(2*((n-1)*R+i))
					xc1=np.sqrt(pow((n-1)*R,2)-pow(yc1,2))
					#deduces the angles for A
					theta1=math.atan(yc1/xc1)
					theta2=math.atan(-yc1/xc1)+math.pi

				#computes the intersection points for zone C
				yc2=(pow(n*R,2)-pow(R,2)+pow((n-1)*R+i,2))/(2*((n-1)*R+i))
				xc2=np.sqrt(pow(n*R,2)-pow(yc2,2))

				#deduces the angles for C
				theta1p=math.atan(yc2/xc2)
				theta2p=math.atan(-yc2/xc2)+math.pi

				#computes the actual surface of A	and of C depending on the current i which is the "offset"	
				if n!=1:
					A=n*(n-2)*pow(R,2)*(theta2-theta1)/2+(pow((n-1)*R+i,2)*(math.sin(theta2)*math.cos(theta2)-math.sin(theta1)*math.cos(theta1))/2)+F(theta2,n,i,R)-F(theta1,n,i,R)
				C=(1-pow(n,2))*pow(R,2)*(theta2p-theta1p)/2-(pow((n-1)*R+i,2)*(math.sin(theta2p)*math.cos(theta2p)-math.sin(theta1p)*math.cos(theta1p))/2)+F(theta2p,n,i,R)-F(theta1p,n,i,R)
			
			#transforms i in an integer in order to store computed value with i and n as indexes
			ind=int(i/STEP)

			if n>1:
				#general case
				pA=A/(math.pi*pow(R,2))
				pC=C/(math.pi*pow(R,2))

				pB=1-pA-pC

				data[n][ind].A=pA
				data[n][ind].B=pB
				data[n][ind].C=pC

				#border data
				pB=1-pA;
				dataBorder[n][ind].A=pA
				dataBorder[n][ind].B=pB
				dataBorder[n][ind].C=0
			else:#n=1 => there is no surface A
				if n==1 and i==0.0:
					pB=1.0
					pC=0.0
				else:
					pC=C/(math.pi*pow(R,2))
					pB=1-pC
				data[n][ind].A=0
				data[n][ind].B=pB
				data[n][ind].C=pC

			i+=STEP
		n+=1


def setCoordinate():
	for i in range(len(graph)):
		if graph[i].rank==0:
			graph[i].coordinate=1
		else:
			up=0
			lev=0
			down=0
			for j in range(len(graph[i].neighbors)):
				if graph[i].neighbors[j].rank < graph[i].rank:
					down+=1
				elif graph[i].neighbors[j].rank == graph[i].rank:
					lev+=1
				elif graph[i].neighbors[j].rank > graph[i].rank:
					up+=1
			tot=up+lev+down
			pup=float(up)/float(tot)
			plev=float(lev)/float(tot)
			pdown=float(down)/float(tot)
			r=graph[i].rank
			mini=100.0
			res=0
			current=0.0

			for k in range(len(data[r])):
				if pup>0.0:
					current=math.sqrt(pow(((data[r][k].A)-pdown),2)+pow(((data[r][k].B)-plev),2)+pow(((data[r][k].C)-pup),2))
				else:
					#Border case
					current=math.sqrt(pow(((dataBorder[r][k].A)-pdown),2)+pow(((dataBorder[r][k].B)-plev),2))

				if current < mini:
					mini=current
					res=float(k*STEP)


			graph[i].coordinate=int((res+mini)*10.0)


def findDuplicate():
	for i in range(len(graph)):
		for j in range(len(graph[i].neighbors)):
			for k in range(len(graph[i].neighbors)):
				if graph[i].neighbors[j].rank==graph[i].neighbors[k].rank and graph[i].neighbors[j].coordinate==graph[i].neighbors[k].coordinate and j!=k:
					return [graph[i].neighbors[j].ID,graph[i].neighbors[k].ID]
	return [0,0]

def maxRank():
	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
	return maxRank

def findNoInt(n):
	for i in range(len(graph)):
		if graph[i].rank==n and graph[i].checked==0:
			found=0
			for j in range(len(graph[i].neighbors)):
				if graph[i].neighbors[j].rank==graph[i].rank and graph[i].neighbors[j].coordinate<graph[i].coordinate and graph[i].neighbors[j].checked==0:
					found=1
			if found==0:
				return i
	return -1


def sumCurve(a,b):
	c=[0,0.0]
	c[0]=a[0]+b[0]#sum of the bursts
	g=fractions.gcd(a[1],b[1])
	if g==0:
		g=1
	period=(a[1]*b[1])/g#resulting period of the main pattern
	if a[1]==0 and b[1]!=0:
		return b
	elif a[1]!=0 and b[1]==0:
		return a
	elif a[1]!=0 and b[1]!=0:
		o=(period/a[1])+(period/b[1])#resulting offset of the main pattern
	else:
		o=0.0
	if o!=0:
		c[1]=period/o#
	return c

#d shoold be a delay (because we assume a node can serve all the traffic after a delay)
def deconv(a,d):
	c=[0,0.0]
	if a[1]!=0.0:
		c[0]=a[0]+math.floor(d/a[1])
	c[1]=a[1]
	return c

def sumKids(i):
	for j in range(len(graph[i].neighbors)):
		if graph[i].neighbors[j].bestNeighbor==i:
			graph[i].alphaKids=sumCurve(graph[i].alphaKids,graph[i].neighbors[j].alphaOut)

def sumInt(i):
	for j in graph[i].interferers:
		graph[i].alphaInt=sumCurve(graph[i].alphaInt,graph[j].alphaOut)

def setBestNeighbor():
	for i in range(len(graph)):
		coord=1000
		for j in range(len(graph[i].neighbors)):
			if graph[i].neighbors[j].rank<graph[i].rank:
				if graph[i].neighbors[j].coordinate < coord:
						graph[i].bestNeighbor=graph[i].neighbors[j].ID
						coord=graph[i].neighbors[j].coordinate

def setInterferers():
	for i in range(len(graph)):
			for j in range(len(graph2[i].neighbors)):
				if graph2[i].neighbors[j].rank==graph[i].rank and graph2[i].neighbors[j].coordinate<graph[i].coordinate:
					if graph2[i].neighbors[j].ID not in graph[i].interferers:
						graph[i].interferers.append(graph2[i].neighbors[j].ID)

def setAutomata(inFileName, outFileName, node):
	docO = ElementTree.parse(inFileName)#the new templates will be added to this tree (O is for ouput)
	ntaO = docO.getroot()
	for child in ntaO:
		if(child.find("name"))!=None:
			if child.find("name").text=="UTAint":
				dec=child.find("declaration")
				dec.text="clock x,y;\n"
				dec.text=dec.text+"const int BMAX="+str(int(graph[node].alphaInt[0]))+";\n"
				dec.text=dec.text+"const int delta="+str(int(graph[node].alphaInt[1]*10000))+";\n"
				dec.text=dec.text+"const int delta2=(backoffD+rcvSlot+backoffD)*3+buzz;\n"
				dec.text=dec.text+"int[0,BMAX] b=BMAX;\n"
			if child.find("name").text=="UTAalarm":
				dec2=child.find("declaration")
				dec2.text="clock x,y;\n"
				dec2.text=dec2.text+"const int BMAX="+str(int(graph[node].alphaKids[0]))+";\n"
				dec2.text=dec2.text+"const int delta="+str(int(graph[node].alphaKids[1]*10000))+";\n"
				dec2.text=dec2.text+"const int delta2=(backoffD+rcvSlot+backoffD)*3+buzz;\n"
				dec2.text=dec2.text+"int[0,BMAX] b=BMAX;\n"
	sys="N0=Node("+str(graph[node].rank)+","+str(graph[node].coordinate)+",1,1);\n"
	if graph[node].alphaInt[1]==0 and graph[node].alphaKids[1]!=0:
		sys=sys+"Ua = UTAalarm();\n\n\n"
		sys=sys+"system N0, Ua;\n"
	elif graph[node].alphaInt[1]==0 and graph[node].alphaKids[1]!=0:
		sys=sys+"inter=interferers("+str(graph[node].rank)+",1,2);\n"
		sys=sys+"Ui = UTAint();\n\n\n"
		sys=sys+"system N0,inter,Ui;\n"
	elif graph[node].alphaInt[1]!=0 and graph[node].alphaKids[1]!=0:
		sys=sys+"inter=interferers("+str(graph[node].rank)+",1,2);\n"
		sys=sys+"Ua = UTAalarm();\n"
		sys=sys+"Ui = UTAint();\n\n\n"
		sys=sys+"system N0,inter,Ui,Ua;\n"
	elif graph[node].alphaInt[1]==0 and graph[node].alphaKids[1]==0:
		sys=sys+"\n\nsystem N0;\n"
	system=ntaO.find("system")
	system.text=sys
	docO.write(outFileName)


def main():
	delay=2.2
	parseGraph(sys.argv[1])
	graph[0].rank=0
	setRank(graph[0])
	initData()
	setCoordinate()


	res=findDuplicate()
	while not (res[0]==0 and res[1]==0):
	 	graph[res[0]].coordinate+=1
	 	res=findDuplicate()

	for i in range(len(graph)):
		graph2.append(Node())
		graph2[i].ID=graph[i].ID
	neighb2()
	setBestNeighbor()
	setInterferers()
	Nmax=maxRank()

	for i in range(Nmax,0,-1):
		node=findNoInt(i)
		while node!=-1:
			sumKids(node)
			sumInt(node)
			graph[node].alphaOut=deconv(graph[node].alphaKids,delay)
			graph[node].checked=1
			node=findNoInt(i)


	#if there is a node with alphaKids and alphaInt greater (burst greater and delta smaller) than those of node i, then there is no need to check i. (because "its traffic will be generated by the other node".) 
	for i in range(len(graph)):
		for j in range(len(graph)):
			if graph[i].alphaKids[0]<=graph[j].alphaKids[0] and graph[i].alphaKids[1]>=graph[j].alphaKids[1] and graph[i].alphaInt[0]<=graph[j].alphaInt[0] and graph[i].alphaInt[1]>=graph[j].alphaInt[1] and graph[j].toCheck!=0 and i!=j:
				graph[i].toCheck=0
				break
		if graph[i].alphaKids[1]==0:#no traffic to forward so no need to check it
			graph[i].toCheck=0

	for i in range(len(graph)):
		print i, graph[i].rank, graph[i].alphaKids, graph[i].alphaInt, graph[i].alphaOut, graph[i].toCheck 


	logFile=open("log","a")

	n=1
	while os.path.exists("results"+str(n)):
		n+=1
	os.makedirs("results"+str(n))#create resuktsn
	for i in range(1,len(graph)):
		if graph[i].toCheck!=0:
			print "node ", i, "being checked"
			setAutomata(sys.argv[2],"out"+str(i)+".xml",i)
			logFile.write("Check node "+str(i)+":\n")
			output=subprocess.Popen(["/home/alex/uppaal-4.1.11/bin-Linux/verifyta", "-t", "1", "-S", "2", "-f", str(i), "-s", "out"+str(i)+".xml", "query.q"], stdout=subprocess.PIPE).communicate()[0]
			if string.find(output,"-- Property is satisfied.") == -1:
				print "node ", i, "cannot handle its trafic"
			else:
				logFile.write(output)
				logFile.write("\n\n\n")
			shutil.move("out"+str(i)+".xml","results"+str(n))
	shutil.move("log","results"+str(n))
if __name__ == '__main__':
    main()