# takes: fei (either xml or text) and smv,
# and produces smv and fault modes files

import sys
import os.path
import logging
import subprocess

import _paths
import _utils


# WARNING! ordering is important here!
FT_ENGINES = "bdd bmc bddbmc msat ic3".split()
(FT_ENGINE_BDD,
 FT_ENGINE_BMC,
 FT_ENGINE_BDD_BMC,
 FT_ENGINE_MSAT,
 FT_ENGINE_IC3, ) = FT_ENGINES


def handle_options():
    """returns (options, input_file):
    values (as a map) and the name of the input file"""

    import argparse
    parser = argparse.ArgumentParser(description="Produces an extend smv file"
                                     " out of given nominal smv file and fei")

    parser.add_argument("--smv-file",
                        metavar="SMV-FILE",
                        help="The input extended smv file name")

    parser.add_argument("--fms-file",
                        metavar="FMS-FILE",
                        help="The input fault mode xml file name")

    parser.add_argument("--faults-bound", "-N",
                        type=int,
                        metavar="BOUND",
                        help="Sets a bound to the maximum number of faults")

    parser.add_argument("--prop-index", "-n",
                        type=int,
                        metavar="INDEX",
                        help="Property index to be used as TLE")

    parser.add_argument("--prop-name", "-P",
                        metavar="NAME",
                        help="Property name to be used as TLE")

    parser.add_argument("--prop-text", "-p",
                        metavar="PROPERTY",
                        help="Textual property to be used as TLE")

    parser.add_argument('--verbose', '-v',
                        action='store_true',
                        default=False,
                        help='Sets verbosity to high level')

    parser.add_argument('--engine', '-E',
                        choices=FT_ENGINES,
                        default=FT_ENGINE_BDD,
                        help='Use given engine (default: %(default)s)')

    parser.add_argument('--dynamic',
                        action='store_true',
                        default=False,
                        help='Generates dynamic fault tree')

    parser.add_argument('--gen-trace', "-e",
                        action='store_true',
                        default=False,
                        help='Generates xml trace from fault tree')

    parser.add_argument('--bmc-length', "-k",
                        type=int,
                        default=10,
                        help='Specify BMC length (integer)')

    parser.add_argument('--show', '-s',
                        action='store_true',
                        default=False,
                        help='Show the generated fault tree')

    parser.add_argument("--probability",
                        action='store_true',
                        default=False,
                        help="Computes probability when generating FT")

    parser.add_argument("--symbolic", '-S',
                        action='store_true',
                        default=False,
                        help="Generates symbolic probability as well "
                        "when computing probability",)

    parser.add_argument("--quick", '-Q',
                        action='store_true',
                        default=False,
                        help="For quick computation, avoid ordering the "
                        "FT and when computing probability avoid computing"
                        "probability of intermediate nodes. Use to"
                        "speedup computation.",)

    parser.add_argument(
        "-d", "--outdir",
        default="out",
        metavar="PATH",
        help="Output directory, where all generated file should be "
        "put into (default:%(default)s)")

    args = parser.parse_args()

    for fn in (args.smv_file, args.fms_file):
        if fn and not os.path.isfile(fn):
            parser.error("File not found: " + fn)

    if os.path.exists(args.outdir) and not os.path.isdir(args.outdir):
        parser.error("Not a directory: " + args.outdir)

    prop = [p for p in (args.prop_index, args.prop_name, args.prop_text)
            if p is not None]
    if len(prop) > 1:
        parser.error("Only one property can be specified")

    if args.symbolic and not args.probability:
        parser.error("Option -S (--symbolic) requires --probability")

    return args


if "__main__" == __name__:

    _paths.setup_path()

    import xsap.utils.misc.log
    from xsap.utils.processes.xsap_process import XsapProcess
    xsap.utils.misc.log.init()

    opts = handle_options()

    if not os.path.exists(opts.outdir):
        os.makedirs(opts.outdir)

    if opts.verbose:
        logging.getLogger().setLevel(logging.INFO)


    # automatically searches for inputs when not explicitly provided
    smv_fname = _utils.get_suitable_smv_file(opts.smv_file, opts.outdir)
    if smv_fname is None:
        sys.exit(1)

    fms_fname = _utils.get_suitable_fms_file(opts.fms_file,
                                             smv_fname,
                                             opts.outdir)
    if fms_fname is None:
        sys.exit(1)

    stdouterr_fname = os.path.join(opts.outdir, "xsap_compute_ft.out")
    if os.path.exists(stdouterr_fname):
        os.remove(stdouterr_fname)

    stdouterr_file = open(stdouterr_fname, "w")

    # instantiate the process
    logging.info("Invoking xsap to compute fault tree")

    need_msat = XsapProcess.has_infinite_domain_vars(smv_fname) or opts.engine == FT_ENGINE_MSAT
    with  XsapProcess(smv_fname, fms_fname,
                      ord_fname=None, need_msat=need_msat,
                      args=["-v", "%d" % (5 if opts.verbose else 0)],
                      stdout=subprocess.PIPE,
                      stderr=subprocess.STDOUT,
                      dumpers=[stdouterr_file]) as xsap_process:

        # set the prefix
        full_base, _ext = os.path.splitext(smv_fname)
        base = os.path.basename(full_base)
        xsap_process.set_tmp_filename_prefix(opts.outdir + "/" + base)

        stdouterr_file.write("\n" + "-" * 70)
        stdouterr_file.write("\nInvoking: %s %s\n" % (xsap_process.get_path(),
                                                  " ".join(xsap_process.get_args())))
        stdouterr_file.write("\n" + "-" * 70)
        stdouterr_file.write("\n")

        prop = (('-n %d' % opts.prop_index) if opts.prop_index is not None
                else
                ('-P "%s"' % opts.prop_name) if opts.prop_name is not None
                else
                ('"%s"' % opts.prop_text) if opts.prop_text is not None
                else "")

        ev_file, gates_file, xml_file = xsap_process.compute_fault_tree(
            prop, opts.dynamic, opts.bmc_length,
            use_bdd=opts.engine==FT_ENGINE_BDD,
            use_bdd_bmc=opts.engine==FT_ENGINE_BDD_BMC,
            compute_probabilities=opts.probability,
            use_param=opts.engine==FT_ENGINE_IC3,
            fails_nbr=opts.faults_bound,
            symbolic=opts.symbolic,
            quick=opts.quick,
            gen_trace=opts.gen_trace,
            gen_random_prefix=False)

    stdouterr_file.close()

    logging.info("xsap produced fault tree in: ")
    logging.info("  events: '%s'" % ev_file)
    logging.info("  gates: '%s'" % gates_file)

    if ev_file is not None and gates_file is not None and opts.show:
        logging.info("Now showing result fault tree")
        import fault_tree_viewer.ftv as ftv
        ftv.run(ev_file, gates_file, xml_file, None, None)