plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/scripts/check_diagnosability.py

import sys
import os
import re
import subprocess

import _paths


def handle_options():
    """Returns options values as map."""

    from xsap.utils.options import (
      MC_ENGINE_BDD,
      MC_ENGINE_BMC,
      MC_ENGINE_MSAT_BMC,
      MC_ENGINE_IC3)

    import argparse
    parser = argparse.ArgumentParser(description="")

    parser.add_argument("--engine", "-E",
                        dest="engine",
                        choices=[MC_ENGINE_BDD, MC_ENGINE_BMC, MC_ENGINE_MSAT_BMC, MC_ENGINE_IC3],
                        default=MC_ENGINE_IC3,
                        help="Use given engine (default: %(default)s)")

    parser.add_argument("--bmc-length", "-k",
                        dest="bmc_len",
                        action="store",
                        type=int,
                        default=10,
                        help="Maximum path length for BMC")

    parser.add_argument("--smv-file", "-m",
                        dest="smv",
                        action="store",
                        default=None,
                        help="SMV file")

    parser.add_argument("--diagnosis-condition", "-c",
                        dest="diag_cond",
                        action="store",
                        default=None,
                        help="Diagnosis condition")

    parser.add_argument("--alarm-pattern", "-a",
                        dest="alarm_pattern",
                        choices=['exact', 'bounded', 'finite'],
                        default=None,
                        help="Alarm pattern (default: %(default)s)")

    parser.add_argument("--delay-bound", "-d",
                        dest="delay_bound",
                        action="store",
                        type=int,
                        default=None,
                        help="Alarm pattern delay bound")

    parser.add_argument("--context-expression", "-x",
                        dest="ltl_context",
                        action="store",
                        default=None,
                        help="LTL context expression")

    parser.add_argument("--observables-file", "-o",
                        dest="obs_file",
                        action="store",
                        default=None,
                        help="File specifying observable variables")

    parser.add_argument("--asl-file", "-f",
                        dest="asl_file",
                        action="store",
                        default=None,
                        help="File containing the alarms specification")

    parser.add_argument("--verbosity-level", "-v",
                        dest="verbose_level",
                        action="store",
                        type=int,
                        default=0,
                        help="Sets the output verbosity level")

    args = parser.parse_args()

    # check arguments

    if args.smv is None or not os.path.exists(args.smv):
        parser.error("The SMV model was not specified.")

    if args.bmc_len < 0:
        parser.error("Illegal BMC length.")

    if args.obs_file is None or not os.path.exists(args.obs_file):
        parser.error("The observables file was not specified.")

    if args.asl_file is None:
        if args.diag_cond is None:
            parser.error("The diagnosis condition was not specified.")

        if args.alarm_pattern is None:
            parser.error("The alarm pattern was not chosen.")

        if args.alarm_pattern in ['exact', 'bounded'] and args.delay_bound is None:
            parser.error("For the chosen alarm pattern a delay bound needs to be specified.")

        if args.alarm_pattern in ['finite'] and args.delay_bound is not None:
            parser.error("A delay bound cannot be specified for finite-delay.")

        if args.delay_bound is not None and int(args.delay_bound) < 0:
            parser.error("Illegal delay bound.")
    else:
        if not os.path.exists(args.asl_file):
            parser.error("The ASL file does not exist")
        if args.diag_cond is not None:
            parser.error("Cannot specify both a diagnosis condition and an ASL file")

    return args


if __name__ == "__main__":

    _paths.setup_path()

    # setup logging
    import xsap.utils.misc.log
    xsap.utils.misc.log.init()
    args = handle_options()

    from xsap.utils.options import MC_ENGINE_MSAT_BMC
    from xsap.utils.processes.xsap_process import XsapProcess

    need_msat = XsapProcess.has_infinite_domain_vars(args.smv) or MC_ENGINE_MSAT_BMC == args.engine

    xsap_process = XsapProcess(args.smv, fail_obs_alm_fname=None,
                               ord_fname=None, need_msat=need_msat,
                               args=["-v", "%d" % args.verbose_level], stdout=subprocess.PIPE,
                               stderr=subprocess.STDOUT,
                               dumpers=[])

    delay_bound = -1 if args.delay_bound is None else int(args.delay_bound)

    results = xsap_process.check_diagnosability_ASL(args.diag_cond,
        args.alarm_pattern, delay_bound, args.ltl_context, args.obs_file,
        args.engine, args.bmc_len, args.asl_file)

    xsap_process.kill_and_close_streams()

    for i, (res, traceA, traceB) in enumerate(results):
        if len(results) > 1:
            print("Specification %d" % i)
        if "Error" == res:
            print "--------------------------------------------------"
            print "Result: An error has occurred during the analysis."
            print "--------------------------------------------------"

        elif "Unknown" == res:
            print "------------------------------------------------------"
            print "Result: No counterexample found within analysis bound."
            print "------------------------------------------------------"

        elif "True" == res:
            print "-------------------------------------------------------"
            print "Result: The specification is diagnosable in the system."
            print "-------------------------------------------------------"

        elif "False" == res:
            print "--------------------------------------------------------------------------------"
            print "Result: The specification is not diagnosable in the system. A pair of traces has"
            print "been generated that show non-diagnosability:"
            print "Trace A:", traceA
            print "Trace B:", traceB
            print "--------------------------------------------------------------------------------"

        else:
            assert False, "BUG: unexpected result of diagnosability verification."