from smt.z3solver import *
from smt.cvc5solver import *
import warnings

from dds.expr import has_propvars
from ltl.automaton import Automaton
from verification.constraint_graph import ConstraintGraph
from verification.product_construction import ProductConstruction
from verification.abstraction_equivalence import Equivalence

def check_LTL(dds, ltl_property, equiv, suffix, verbose):
  cg = ConstraintGraph(dds, equiv)
  nfa = Automaton(ltl_property)
  anames = [ t["name"] for t in dds._transitions]
  nfa._has_action_vars = has_propvars(ltl_property._property, anames)
  prod_nfa = ProductConstruction(dds, nfa, equiv)
  
  visualize_graphs(dds, cg, nfa, prod_nfa, suffix)

  witness = None
  if prod_nfa.has_final_state():
    if verbose:
      print("product automaton admits witness")
    prod_nfa.compute_witness(show=verbose)
    witness = True
  else:
    if verbose:
      print("product automaton admits no witness")
    witness = False
  return witness

def visualize_graphs(dds, cg, nfa, pc, suffix):
  # ignore warnings that graph output was scaled
  warnings.filterwarnings("ignore", message = ".*graph is too large.*Scaling.*")

  outdir = "out"
  dds.show(outdir + "/ddsa" + ("_" + suffix if suffix else "") + ".png")
  cg.show(outdir + "/cg" + ("_" + suffix if suffix else "") + ".png")
  nfa.show(outdir + "/nfa" + ("_" + suffix if suffix else "") + ".png")
  pc.show(outdir + "/pc" + ("_" + suffix if suffix else "") + ".png")

