| # 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! |
| FMEA_ENGINES = "bdd bmc msat".split() |
| FMEA_ENGINE_BDD, FMEA_ENGINE_BMC, FMEA_ENGINE_MSAT = FMEA_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("--prop-indices", "-n", |
| type=int, |
| metavar="INDICES", |
| help="Property indices to be used as TLE " |
| "(separated by ':' or spaces, ranges like " |
| "'0-10' are allowed)") |
| |
| parser.add_argument("--props-text", "-p", |
| metavar="PROPERTIES", |
| help="Textual properties to be used as TLE, " |
| "separated by ':' or by spaces") |
| |
| parser.add_argument('--verbose', '-v', |
| action='store_true', |
| default=False, |
| help='Sets verbosity to high level') |
| |
| parser.add_argument('--engine', '-E', |
| choices=FMEA_ENGINES, |
| default=FMEA_ENGINE_BDD, |
| help='Use given engine (default: %(default)s)') |
| |
| parser.add_argument('--dynamic', |
| action='store_true', |
| default=False, |
| help='Generates dynamic fmea table') |
| |
| parser.add_argument('--compact', '-c', |
| action='store_true', |
| default=False, |
| help='Generates compact fmea table') |
| |
| parser.add_argument('--card', "-N", |
| type=int, |
| default=1, |
| help='Cut-Set cardinality (default: %(default)d)') |
| |
| 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 fmea table') |
| |
| 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_indices, args.props_text) |
| if p is not None] |
| if len(prop) > 1: |
| parser.error("Properties can be specified only " |
| "in one way (multiple used)") |
| |
| if args.engine in (FMEA_ENGINE_MSAT, FMEA_ENGINE_BMC) and args.dynamic: |
| parser.error("Dynamic fmea not available with engine %s" % args.engine) |
| |
| return args |
| |
| |
| def show_fmea_table(fmea_fname, card, show): |
| count = 0 |
| |
| import csv |
| with open(fmea_fname, 'rb') as csvfile: |
| reader = csv.reader(csvfile, delimiter='\t', quotechar="'") |
| reader.next() |
| for row in reader: |
| if show: |
| print "-" * 70 |
| print "ID: ", row[0] |
| print "TLE:", row[3] |
| print "FMS:", row[2] |
| count += 1 |
| |
| if show: |
| print "=" * 70 |
| print "Total cut sets with cardinality %d: %d" % (card, count) |
| |
| elif count == 0: |
| logging.warn("The FMEA table is empty with cardinality %d" % card) |
| |
| return |
| |
| |
| if "__main__" == __name__: |
| _paths.setup_path() |
| |
| import xsap.utils.misc.log |
| from xsap.utils.processes.xsap_process import XsapProcess |
| xsap.utils.misc.log.init() |
| |
| args = handle_options() |
| |
| if not os.path.exists(args.outdir): |
| os.makedirs(args.outdir) |
| |
| if args.verbose: |
| logging.getLogger().setLevel(logging.INFO) |
| |
| prop = [('-n %d' % args.prop_indices) if args.prop_indices is not None |
| else |
| ('%s' % args.props_text) if args.props_text is not None |
| else ""] |
| |
| # automatically searches for inputs when not explicitly provided |
| smv_fname = _utils.get_suitable_smv_file(args.smv_file, args.outdir) |
| if smv_fname is None: |
| sys.exit(1) |
| |
| fms_fname = _utils.get_suitable_fms_file(args.fms_file, |
| smv_fname, |
| args.outdir) |
| if fms_fname is None: |
| sys.exit(1) |
| |
| stdouterr_fname = os.path.join(args.outdir, "xsap_compute_fmea.out") |
| if os.path.exists(stdouterr_fname): |
| os.remove(stdouterr_fname) |
| stdouterr_file = open(stdouterr_fname, "w") |
| |
| logging.info("Invoking xsap to compute fmea table") |
| |
| need_msat = XsapProcess.has_infinite_domain_vars(smv_fname) or args.engine == FMEA_ENGINE_MSAT |
| with XsapProcess(smv_fname, fms_fname, |
| need_msat=need_msat, |
| stdout=subprocess.PIPE, |
| stderr=subprocess.STDOUT, |
| dumpers=[stdouterr_file]) as xsap_proc: |
| |
| # set the prefix of generated files |
| full_base, _ext = os.path.splitext(smv_fname) |
| base = os.path.basename(full_base) |
| xsap_proc.set_tmp_filename_prefix(args.outdir + "/" + base) |
| |
| stdouterr_file.write("\n" + "-" * 70) |
| stdouterr_file.write("\nInvoking: %s %s\n" % (xsap_proc.get_path(), |
| " ".join(xsap_proc.get_args()))) |
| stdouterr_file.write("\n" + "-" * 70) |
| stdouterr_file.write("\n") |
| |
| res = xsap_proc.compute_fmea_table( |
| prop, args.card, dynamic=args.dynamic, bmc_length=args.bmc_length, |
| compact=args.compact, engine=args.engine) |
| |
| logging.info("xsap produced fmea table in: '%s'" % res) |
| stdouterr_file.close() |
| |
| show_fmea_table(res, args.card, args.show) |
