"""

This module provides a wrapper to generate SMV models from Verilog benchmarks using EBMC,
inject temporal properties, and then invoke nuXmv with BDD or IC3 backends.

Function:
  runNuXmv(name, module_name, nuXmvSpec, idtext, SVSpec=None, ifIC3=False)

Workflow:
 1. Record start time.
 2. Read the original Verilog file from `Benchmarks/{name}.sv`.
 3. If `SVSpec` is provided:
    - Inject an `assert property` block before `endmodule`.
    - Write the modified Verilog to `Tools/nuXmv/SMV/{name}.sv`.
    - Run EBMC with `--smv-netlist`, producing `{name}.smv`.
    - Clean up the temporary `.sv` file.
 4. If no `SVSpec`, 
    - run EBMC directly on the original `.sv` to generate the SMV netlist.
    - Read the generated SMV file, strip everything before the EBMC header, append `nuXmvSpec` if
    no `SVSpec` was given.
    - Overwrite `Tools/nuXmv/SMV/{name}.smv` with the final content.
 7. Invoke nuXmv or `nuXmv_IC3.sh` based on `ifIC3` flag.
 8. Measure and print total elapsed time.

Returns:
    nuXT (float):     Elapsed wall-clock time (seconds) for the nuXmv run.
"""

import os
import time
import re


def runNuXmv(name, module_name, nuXmvSpec, idtext, SVSpec = None, ifIC3 = False):
	begin = time.time()
	#os.system(f"rm ../../Tools/nuXmv/SMV/{name}.smv")
	with open(f"../../Benchmarks/{name}.sv", 'r') as file:
	    data = file.read()
	if SVSpec is not None:
		prop = f"\tp1: assert property  ({SVSpec}) ;\nendmodule"
		data = re.sub("endmodule", prop, data)
		with open(f"../../Tools/nuXmv/SMV/{name}.sv", "w") as file:
			file.write(data)
		#print(data)
		os.system(f"ebmc ../../Tools/nuXmv/SMV/{name}.sv --smv-netlist > ../../Tools/nuXmv/SMV/{name}.smv")
		os.system(f"rm ../../Tools/nuXmv/SMV/{name}.sv")
	else:
		os.system(f"ebmc ../../Benchmarks/{name}.sv --smv-netlist > ../../Tools/nuXmv/SMV/{name}.smv")
	
	data = ""
	with open(f"../../Tools/nuXmv/SMV/{name}.smv", 'r') as file:
		data = file.read()
	data = data[data.find('-- Generated by EBMC') :]
	if SVSpec is None:
		data += "\n\n"+ nuXmvSpec
	with open(f"../../Tools/nuXmv/SMV/{name}.smv", "w") as file:
		file.write(data)
	if ifIC3:
		os.system(f"../../Tools/nuXmv/nuXmv_IC3.sh ../../Tools/nuXmv/SMV/{name}.smv")
	else:
		os.system(f"../../Tools/nuXmv/nuXmv ../../Tools/nuXmv/SMV/{name}.smv")
	end = time.time()
	nuXT = end - begin
	if ifIC3:
		print(f"\n\nnuXmv IC3 TIME: {nuXT}\n")
	else:
		print(f"\n\nnuXmv TIME: {nuXT}\n")
	return nuXT

