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

#!/usr/bin/env python

import sys
import os.path
from argparse import ArgumentParser, RawTextHelpFormatter

import _paths
_paths.setup_path()

from xsap.data_structure.tfpg.tfpg_errors import UnsupportedInfinitySemantics
from xsap.data_structure.tfpg.tfpg import OPEN_INFINITY
from xsap.data_structure.tfpg.tfpg import Tfpg
from xsap.features.tfpg_smt.utils import parse_scenario_file, print_model
from xsap.features.tfpg_smt.reasoner import TFPGReasoner
from xsap.features.tfpg_smt.encoding import node_state_symbol


def main():
    parser = ArgumentParser(formatter_class=RawTextHelpFormatter,
                            description="""
TFPG Check (SMT): Checks multiple properties of the given TFPG.
""")

    parser.add_argument('inputTFPG', metavar='inputTFPG',
                        type=str,
                        help='The TFPG model to use')

    parser.add_argument('--scenario', metavar='scenario',
                        type=str,
                        help='The scenario to be used for checking')

    parser.add_argument('--possibility', '-p', action='store_true',
                        help='Checks the possibility of the given scenario ' \
                        'in the given TFPG')

    parser.add_argument('--necessity', '-n', action='store_true',
                        help='Checks the necessity of the given scenario ' \
                        'in the given TFPG')

    parser.add_argument('--consistency', '-x', action="store_true",
                        help='Checks if a scenario exists for the given TFPG')

    parser.add_argument('--activability', action="store_true",
                        help='Checks if all nodes can be activated')

    parser.add_argument('--all-modes', action="store_true",
                        help='Enumerates the modes compatible with the scenario.')

    parser.add_argument('--open-infinity', action='store_true',
                        help='Force the usage of Open Infinity semantics')

    args = parser.parse_args()


    # Command line handling
    tfpg = Tfpg.parse_tfpg(args.inputTFPG)
    if tfpg is None:
        sys.exit(1)

    if args.open_infinity:
        tfpg.set_infinity_semantics(OPEN_INFINITY)

    try:
        reasoner = TFPGReasoner(tfpg, include_health=False)
    except UnsupportedInfinitySemantics:
        print("The current version of the algorithm only supports Open Infinity Semantics.")
        print("To force the implicit conversion, use the option --open-infinity")
        sys.exit(1)

    if args.possibility:
        scenario_f = args.scenario
        if scenario_f is None:
            print("You must specify the scenario to check by using the --scenario option")
            print("See help for further details.")
            sys.exit(1)

        scenario = parse_scenario_file(scenario_f)
        if scenario is None:
            print("The given scenario is invalid")
            sys.exit(1)

        print("Checking the possibility of the given scenario...")
        res, model = reasoner.check_scenario(scenario)
        if res:
            print("The scenario is possible!")
            print("A model is:")
            print_model(model)
        else:
            print("The scenario is NOT possible!")

    elif args.consistency:
        res, model = reasoner.check_consistency()
        if res:
            print("The TFPG is consistent!")
            print("A model is:")
            print_model(model)
        else:
            print("The TFPG is NOT consistent!")

    elif args.necessity:
        scenario_f = args.scenario
        if scenario_f is None:
            print("You must specify the scenario to check by using the --scenario option")
            print("See help for further details.")
            sys.exit(1)

        scenario = parse_scenario_file(scenario_f)
        if scenario is None:
            print("The given scenario is invalid")
            sys.exit(1)

        print("Checking the necessity of the given scenario...")
        res, model = reasoner.check_scenario_necessity(scenario)
        if res:
            print("The scenario is necessary!")
        else:
            print("The scenario is NOT necessary!")
            print("A counterexample scenario is:")
            print_model(model)

    elif args.activability:
        print("Checking if all nodes can be activated...")
        invalid_nodes = reasoner.check_activability()
        if len(invalid_nodes) == 0:
            print("All nodes can be activated!")
        else:
            print("The following nodes CANNOT be activated!")
            print([str(n) for n in invalid_nodes])

    elif args.all_modes:
        scenario_f = args.scenario
        if scenario_f is None:
            print("You must specify the scenario to check by using the --scenario option")
            print("See help for further details.")
            sys.exit(1)

        scenario = parse_scenario_file(scenario_f)
        if scenario is None:
            print("The given scenario is invalid")
            sys.exit(1)

        print("Checking Modes compatible with the scenario...")
        scenario = reasoner.scenario_to_formula(scenario)
        modes = reasoner.get_all_modes(scenario)
        if len(modes) == 0:
            print("NO mode compatible with the scenario!")
        else:
            print("The following modes are ALL the compatible modes:")
            for mode in modes:
                print(mode)

    else:
        print "Invalid command line parameters."
        print "See help for further details."
        sys.exit(1)


if __name__ == "__main__":
    main()