import netverifcar
import libsverifcar
import time

#______________________PROPOSITIONS & HEURISTICS______________________

#___________Arrival Order___________

def arrival_i_before_j(state,i,j) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			pi = v.posX
		if v.id == j :
			pj = v.posX
	if pi == libsverifcar.LengthX and pi > pj :
		return True
	return False

#Heuristic for arrival_i_before_j
def distance_i_j(state,i,j) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			pi = v.posX
		if v.id == j :
			pj = v.posX
	return pi - pj

#Negation of arrival_i_before_j
def not_arrival_i_before_j(state,i,j) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			pi = v.posX
		if v.id == j :
			pj = v.posX
	if pi == libsverifcar.LengthX and pi > pj :
		return False
	return True

#___________Travel Time___________

#Travel time > n
def travel_time_i_sup_n(state,i,n) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i and v.posX == libsverifcar.LengthX :	
			return v.nb_updates > n
	return False

#Heuristic for travel_time_i_sup_n
def hestimated_travel_time(state,i,n) :#n for compilation
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i and v.nb_updates > 0:	
			return v.nb_updates+(((libsverifcar.LengthX-v.posX)/v.speed)*10)
	return 0

#Travel time < n
def travel_time_i_inf_n(state,i,n) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i and v.posX == libsverifcar.LengthX :	
			return v.nb_updates < n
	return False

#Heuristic for travel_time_i_inf_n
def hestimated_travel_time_inv(state,i,n) :#n for compilation
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i and v.nb_updates > 0:	
			return -(v.nb_updates+(((libsverifcar.LengthX-v.posX)/v.speed)*10))
	return 0

#___________Time-to-collision___________

#TTC < n
def ttc_i_j_inf_n(state,i,j,n) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			vi = v
			if v.posX == libsverifcar.LengthX :
				return False
		if v.id == j :
			vj = v
			if v.posX == libsverifcar.LengthX :
				return False
	return netverifcar.time_to_collision(vi, vj) < n

#Heuristic for ttc_i_j_inf_n
def time_to_overtake_i_j_inv(state,i,j,n) :#n for compilation
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			vi = v
			if v.posX == libsverifcar.LengthX :
				return -100*libsverifcar.scale
		if v.id == j :
			vj = v
			if v.posX == libsverifcar.LengthX :
				return -100*libsverifcar.scale
	if vi.posX > vj.posX :
		if vi.speed < vj.speed :
			return -(vi.posX-vj.posX)/(vj.speed-vi.speed)
		else :
			return -100*libsverifcar.scale
	elif vj.posX > vi.posX :
		if vj.speed < vi.speed :
			return -(vj.posX-vi.posX)/(vi.speed-vj.speed)
		else :
			return -100*libsverifcar.scale
	else :
		return 0
#TTC > n
def ttc_i_j_sup_n(state,i,j,n) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			vi = v
			if v.posX == libsverifcar.LengthX :
				return True
		if v.id == j :
			vj = v
			if v.posX == libsverifcar.LengthX :
				return True
	return netverifcar.time_to_collision(vi, vj) > n

#Heuristic for ttc_i_j_inf_n
def time_to_overtake_i_j(state,i,j,n) :#n for compilation
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.id == i :
			vi = v
			if v.posX == libsverifcar.LengthX :
				return 100*libsverifcar.scale
		if v.id == j :
			vj = v
			if v.posX == libsverifcar.LengthX :
				return 100*libsverifcar.scale
	if vi.posX > vj.posX :
		if vi.speed < vj.speed :
			return (vi.posX-vj.posX)/(vj.speed-vi.speed)
		else :
			return 100*libsverifcar.scale
	elif vj.posX > vi.posX :
		if vj.speed < vi.speed :
			return (vj.posX-vi.posX)/(vi.speed-vj.speed)
		else :
			return 100*libsverifcar.scale
	else :
		return 0

#______________________EXPLORATION ALGORITHMS______________________

#___________Sub-functions___________

def strong_equal(state1,state2) :
	v1 = list(state1["vehicles"].items())
	v2 = list(state2["vehicles"].items())
	for i in range(len(v1)):
		if not v1[i].strong_equal(v2[i]) :
			return False
	return True	

def final_state(state) :
	vehicles = list(state["vehicles"].items())
	for v in vehicles :
		if v.posX != libsverifcar.LengthX :
			return False
	return True

def next_border(init) :
	finals = set()
	exploring = set()
	exploring.add(init)
	while exploring :
		for i in exploring.copy() :
			itersucc = list(netverifcar.itersucc(i))
			exploring.remove(i)
			for s in itersucc :
				marking = i-s[2]+s[3]
				if s[0] == 'update' :
				#if s[0] == 'signal' :
					finals.add(marking)
				else :
					exploring.add(marking)
	return finals

def next_border_set(init_set) :
	finals = []
	exploring = init_set
	while exploring :
		for i in exploring.copy() :
			itersucc = list(netverifcar.itersucc(i))
			exploring.remove(i)
			for s in itersucc :
				marking = i-s[2]+s[3]
				if s[0] == 'update' :
				#if s[0] == 'signal' :
					state_added = False
					for aset in finals :
						if strong_equal(aset.copy().pop(),marking) :
							aset.add(marking)
							state_added = True
					if not state_added :
						finals.append({marking})
				else :
					exploring.add(marking)
	return finals

#___________Full Exploration Algorithms___________

#Standard width first exploration
def basic_width() :
	start_time = time.time()
	exploring = [netverifcar.init()]
	finals = set()
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ = netverifcar.succ(exploring.pop(0))
		state_counter = state_counter + 1
		for s in succ :
			if final_state(s) :
				finals.add(s)
				print("--- %s seconds ---" % (time.time() - start_time))
			elif s not in exploring :
				exploring.append(s)
			else :
				print("Found interliving")
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return finals

#Standard depth first exploration (no results to be expected)
def basic_depth() :
	start_time = time.time()
	exploring = [netverifcar.init()]
	finals = set()
	state_counter = 0
	while exploring :
		succ = netverifcar.succ(exploring.pop())
		state_counter = state_counter + 1
		for s in succ :
			if final_state(s) :
				finals.add(s)
				print(len(exploring))
				print("--- %s seconds ---" % (time.time() - start_time))
			else :
				exploring.append(s)
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return finals

#Layered depth first exploration without weak variables
def strong_explore_depth() :
	start_time = time.time()
	exploring = [netverifcar.init()]
	finals = set()
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border(exploring.pop())
		state_counter = state_counter + 1
		for s in succ_set :
			if final_state(s) :
				finals.add(s)
				print(len(exploring))
				print("--- %s seconds ---" % (time.time() - start_time))
			else :
				exploring.append(s)
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return finals

#Layered depth first exploration with weak variables
def explore_depth() :
	start_time = time.time()
	exploring = [{netverifcar.init()}]
	finals = set()
	state_counter = 0
	final_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border_set(exploring.pop())
		state_counter = state_counter + 1
		for aset in succ_set :
			explore_set = set()
			for s in aset :
				if final_state(s) :
					finals.add(s)
					final_counter = final_counter + 1
					print("Found %s th final state" % (final_counter))
					print("--- %s seconds ---" % (time.time() - start_time))
				else :
					explore_set.add(s)
			if explore_set :
				exploring.append(explore_set)
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return finals

#Width first exploration for paths extrema of a set of indicators (any number of indicator can be added)
def bounds_value(value1,value1_args,value2,value2_args,value3,value3_args) :
	start_time = time.time()
	init = netverifcar.init()
	v1 = value1(init,*value1_args)
	v2 = value2(init,*value2_args)
	v3 = value3(init,*value3_args)
	exploring = [(init,v1,v1,v2,v2,v3,v3)]
	finals = set()
	state_counter = 0
	while exploring :
		#print(len(exploring))
		explored = exploring.pop(0)
		succ = next_border(explored[0])
		state_counter = state_counter + 1
		for s in succ :
			state_value1 = value1(s,*value1_args)
			min_path_value1 = min(explored[1],state_value1)
			max_path_value1 = max(explored[2],state_value1)
			state_value2 = value2(s,*value2_args)
			min_path_value2 = min(explored[3],state_value2)
			max_path_value2 = max(explored[4],state_value2)
			state_value3 = value3(s,*value3_args)
			min_path_value3 = min(explored[5],state_value3)
			max_path_value3 = max(explored[6],state_value3)
			if final_state(s) :
				finals.add((s,min_path_value1,max_path_value1,min_path_value2,max_path_value2,min_path_value3,max_path_value3))
			elif (s,min_path_value1,max_path_value1,min_path_value2,max_path_value2,min_path_value3,max_path_value3) not in exploring :
				exploring.append((s,min_path_value1,max_path_value1,min_path_value2,max_path_value2,min_path_value3,max_path_value3))
			else :
				print("Found interliving")
	print("--- %s seconds ---" % (time.time() - start_time))
	print("Exploration is over. Number of states explored : ", state_counter)
	return finals

#___________Reachability Algorithms___________

#EF p in depth first with heuristic
def exist_state(prop,heuristic,func_args) :
	start_time = time.time()
	exploring = [({netverifcar.init()},heuristic(netverifcar.init(),*func_args))]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border_set(exploring.pop()[0])
		state_counter = state_counter + 1
		for s in succ_set :
			state=s.copy().pop()
			if prop(state,*func_args) :
				print("Exploration is over. Number of states explored : ", state_counter)
				print("--- %s seconds ---" % (time.time() - start_time))
				print(s)
				return True
			elif not final_state(state) :
				weight = heuristic(state,*func_args)
				index = len(exploring)
				if index == 0 :
					exploring.append((s,weight))
				elif exploring[0][1] > weight :
					exploring.insert(0,(s,weight))
				else :
					while exploring[index-1][1] > weight and index > 1 :#to improve with dichotomy
						index = index - 1
					exploring.insert(index,(s,weight))
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False

#EF p in width first 
def width_exist(func,func_args) :
	start_time = time.time()
	exploring = [netverifcar.init()]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border(exploring.pop(0))
		state_counter = state_counter + 1
		for s in succ_set :
			if func(s,*func_args) :
				print("Exploration is over. Number of states explored : ", state_counter)
				print("--- %s seconds ---" % (time.time() - start_time))
				print(s)
				return True
			if s not in exploring and not final_state(s):
				exploring.append(s)
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False

#EG p in depth first with heuristic
def exist_path(prop,heuristic,func_args) :
	start_time = time.time()
	exploring = [({netverifcar.init()},heuristic(netverifcar.init(),*func_args))]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border_set(exploring.pop()[0])
		state_counter = state_counter + 1
		for s in succ_set :
			state=s.copy().pop()
			if prop(state,*func_args) :
				if final_state(state) :
					print("Exploration is over. Number of states explored : ", state_counter)
					print("--- %s seconds ---" % (time.time() - start_time))
					print(s)
					return True
				else :
					weight = heuristic(state,*func_args)
					index = len(exploring)
					if index == 0 :
						exploring.append((s,weight))
					elif exploring[0][1] > weight :
						exploring.insert(0,(s,weight))
					else :
						while exploring[index-1][1] > weight and index > 1 :#to improve with dichotomy
							index = index - 1
						exploring.insert(index,(s,weight))
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False

#EG p in width first
def width_path(func,func_args) :
	start_time = time.time()
	exploring = [netverifcar.init()]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		succ_set = next_border(exploring.pop(0))
		state_counter = state_counter + 1
		for s in succ_set :
			if func(s,*func_args) :
				if final_state(s) :
					print("Exploration is over. Number of states explored : ", state_counter)
					print("--- %s seconds ---" % (time.time() - start_time))
					return True
				elif s not in exploring :
					exploring.append(s)
				else :
					print("Found interliving")
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False

#EF (p and EF q) in depth first
def EFpEFq(prop1,prop1_args,prop2,prop2_args) :
	start_time = time.time()
	exploring = [({netverifcar.init()},False)]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		main_succ = exploring.pop()
		succ_set = next_border_set(main_succ[0])
		state_counter = state_counter + 1
		for s in succ_set :
			state=s.copy().pop()
			mark = False
			if prop1(state,*prop1_args) or main_succ[1] :
				mark = True
			if mark and prop2(state,*prop2_args) :
				print("Exploration is over. Number of states explored : ", state_counter)
				print("--- %s seconds ---" % (time.time() - start_time))
				print(s)
				return True
			elif not final_state(state) :
				exploring.append((s,mark))
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False

#EF (p and EG q) in depth first
def EFpEGq(prop1,prop1_args,prop2,prop2_args) :
	start_time = time.time()
	exploring = [({netverifcar.init()},False)]
	state_counter = 0
	while exploring :
		#print(len(exploring))
		main_succ = exploring.pop()
		succ_set = next_border_set(main_succ[0])
		state_counter = state_counter + 1
		for s in succ_set :
			state=s.copy().pop()
			mark = False
			if (prop1(state,*prop1_args) or main_succ[1]) and prop2(state,*prop2_args) :
				mark = True
			if mark and final_state(state) :
				print("Exploration is over. Number of states explored : ", state_counter)
				print("--- %s seconds ---" % (time.time() - start_time))
				print(s)
				return True
			elif not final_state(state) :
				exploring.append((s,mark))
	print("Exploration is over. Number of states explored : ", state_counter)
	print("--- %s seconds ---" % (time.time() - start_time))
	return False