| # 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) |
