def test_ast_to_spec(self):
        queries = ["?",
                   "~?",
                   "'request' & ?",
                   "? | 'state = ready'",
                   "? -> '!request'",
                   "'state = busy' <-> ?",
                   "AX ?",
                   "AF ?",
                   "AG ?",
                   "EX ?",
                   "EF ?",
                   "EG ?",
                   "A[True U ?]",
                   "A[? W False]",
                   "E[? U True]",
                   "E[False W ?]",
                   "A[False oU ?]",
                   "A[? oW True]",
                   "A[True dU ?]",
                   "A[? dW False]",
                   "E[False oU ?]",
                   "E[? oW True]",
                   "E[True dU ?]",
                   "E[? dW False]"]

        for query in queries:
            init_nusmv()
            self.init_model()
            self.assertIsInstance(ast_to_spec(replace(parse_ctlq(query),
                                                      TrueExp())),
                                  Spec)
            deinit_nusmv()

 def setUp(self):
     init_nusmv()
     ret = cmd.Cmd_SecureCommandExecute("read_model -i"
                                        " tests/pynusmv/models/admin.smv")
     self.assertEqual(ret, 0)
     ret = cmd.Cmd_SecureCommandExecute("go")
     self.assertEqual(ret, 0)

 def setUp(self):
     init_nusmv()
     load_from_file(tests.current_directory(__file__)+"/models/flipflops_trans_invar_fairness.smv")
     go_bmc()
     
     self.fsm = BeFsm.global_master_instance()
     self.enc = self.fsm.encoding

    def test_bdd_to_set(self):
        set_ = {HashableDict({'state': 'ready', 'request': 'TRUE'}),
                HashableDict({'state': 'ready', 'request': 'FALSE'})}

        init_nusmv()
        fsm = self.init_model()
        self.assertEqual(bdd_to_set(fsm, fsm.init), set_)
        deinit_nusmv()

 def test_init(self):
     init_nusmv()
     # Should not produce error
     fsm = BddFsm.from_filename("tests/pynusmv/models/admin.smv")
     reset_nusmv()
     # Should not produce error
     fsm = BddFsm.from_filename("tests/pynusmv/models/admin.smv")
     deinit_nusmv()

 def __enter__(self):
     """Performs what one would usually do in setUp"""
     init_nusmv()
     load_from_file(self.model)
     go_bmc()
     self.testcase.sexpfsm = master_bool_sexp_fsm()
     self.testcase.befsm   = master_be_fsm()
     self.testcase.enc     = self.testcase.befsm.encoding
     self.testcase.mgr     = self.testcase.enc.manager

 def setUp(self):
     init_nusmv()
     load_from_file(tests.current_directory(__file__)+"/models/flipflops_vif.smv")
     go_bmc()
     self.enc = master_be_fsm().encoding
     self.v   = self.enc.by_name['v']
     self.f   = self.enc.by_name['f']
     self.i   = self.enc.by_name['i']
     self.n   = self.enc.by_name['next(v)']

 def setUp(self):
     init_nusmv()
     #config.debug = True
     config.partial.early.type = "full"
     config.partial.caching = True
     config.partial.filtering = True
     #config.partial.separation.type = "reach"
     #config.garbage.type = "step"
     #config.garbage.step = 4
     config.partial.alternate.type = {"univ", "strat"}

 def setUp(self):
     init_nusmv()
     glob.load(self.model())
     glob.flatten_hierarchy()
     glob.encode_variables()  # does it for BDD
     self.go_bmc()
     
     pd = _prop.PropPkg_get_prop_database()
     fsm= _prop.PropDb_master_get_be_fsm(pd)
     self._TEST = _be.BeFsm_get_fairness_list(fsm)

    def test_gc(self):
        """
        This test should not produce a segfault due to freed memory after
        deiniting NuSMV. This is thanks to the PyNuSMV GC system that keeps
        track of all wrapped pointers and free them when deiniting NuSMV, if
        needed.
        """
        init_nusmv()

        fsm = BddFsm.from_filename("tests/pynusmv/models/admin.smv")
        init = fsm.init

        deinit_nusmv()

def proceed(args):
    """Actually proceeds to the verification"""
    with init_nusmv():
        load(args.model)
        with BmcSupport():

            observable = mk_observable_names(args)

            if not args.quiet:
                with open(args.model) as m:
                    model = m.read()
                print_greeting(model, observable)

            if args.spec is not None:
                check(args, args.spec, observable)
            else:
                print("*" * 80)
                print("* DIAGNOSABILITY TESTS")
                print("*" * 80)
                print("Enter diagnosability condition, one per line in the format: 'c1 ; c2'")
                for line in sys.stdin:
                    check(args, line, observable)

 def setUp(self):
     init_nusmv()
     load_from_file(tests.current_directory(__file__)+"/models/flipflops_vif.smv")
     go_bmc()
     self._TESTED = BeEnc.global_singleton_instance()

    # Populate arguments: for now, only the model
    parser.add_argument('model', help='the NuSMV model with specifications')
    args = parser.parse_args(allargs)
    
    # Initialize the model
    fsm = BddFsm.from_filename(args.model)
    propDb = glob.prop_database()
    
    # Check all CTL properties
    for prop in propDb:
        #  Check type
        if prop.type == propTypes['CTL']:
            spec = prop.exprcore
    
            (satisfied, cntex) = check_ctl_spec(fsm, spec)
            # Print the result and the TLACE if any
            print('Specification',str(spec), 'is', str(satisfied),
                  file=sys.stderr)
        
            if not satisfied:
                print(xml_representation(fsm, cntex, spec))
            
            print()


if __name__ == '__main__': 
    # Initialize NuSMV
    init_nusmv()   
    check_and_explain(sys.argv[1:])
    # Quit NuSMV
    deinit_nusmv()

 def setUp(self):
     init_nusmv()
     load(self.model())

 def preloop(self):
     init_nusmv()

def cli(model_path, query, order):
    """Solve QUERY that belongs to fragment CTLQx for model in MODEL_PATH."""
    try:
        # Parse `query` and transform it in NNF.
        ast = negation_normal_form(parse_ctlq(query))

        # Check that `query` belongs to fragment CTLQx.
        if not check_ctlqx(ast):
            click.echo("Error: {query} does not belong to CTLQx".format(query=query))
            # Quit PyTLQ.
            sys.exit()

        # Initialize NuSMV.
        with init_nusmv():
            # Load model from `model_path`.
            load(model_path)
            # Enable dynamic reordering of the variables.
            enable_dynamic_reordering()
            # Check if an order file is given.
            if order:
                # Build model with pre-calculated variable ordering.
                compute_model(variables_ordering=order)
            else:
                # Build model.
                compute_model()
            # Retrieve FSM of the model.
            fsm = prop_database().master.bddFsm

            # Solve `query` in `fsm`.
            solution = solve_ctlqx(fsm, ast)

            # Display solution.
            click.echo("Solution states:")
            if not solution:
                click.echo("No solution")
                # Quit PyTLQ.
                sys.exit()
            elif solution.is_false():
                click.echo("False")
                # Quit PyTLQ.
                sys.exit()
            else:
                size = fsm.count_states(solution)
                if size > 100:
                    if click.confirm(
                        "The number of states is too large"
                        " ({size}). Do you still want to print"
                        " them?".format(size=size)
                    ):
                        pprint(bdd_to_set(fsm, solution))
                else:
                    pprint(bdd_to_set(fsm, solution))

            # Ask for further manipulations.
            while True:
                command = click.prompt(
                    "\nWhat do you want to do?"
                    "\n  1. Project the solution on a"
                    " subset of the variables"
                    "\n  2. Simplify the solution according"
                    " to Chan's approximate conjunctive"
                    " decomposition"
                    "\n  3. Quit PyTLQ"
                    "\nYour choice",
                    type=click.IntRange(1, 3),
                    default=3,
                )

                # Check if solution must be projected or simplified.
                if command == 1 or command == 2:

                    # Gather more information.
                    click.echo("")
                    if command == 2:
                        maximum = click.prompt(
                            "Please enter the maximum"
                            " number of variables that must"
                            " appear in the conjuncts of"
                            " the simplification",
                            type=int,
                            default=1,
                        )
                    variables = click.prompt(
                        "Please enter the list of" " variables of interest," " separated by commas",
                        type=str,
                        default="all the variables",
                    )
                    # Format `variables`.
                    if variables == "all the variables":
                        variables = None
                    else:
                        variables = variables.replace(" ", "").split(",")

                    if command == 1:
                        # Project solution and display projection.
                        click.echo("\nProjection:")
                        click.echo(project(fsm, solution, variables))
                    else:
                        # Simplify solution and display simplification.
                        click.echo("\nApproximate conjunctive decomposition:")
#.........这里部分代码省略.........

 def setUp(self):
     init_nusmv()
     load(self.model())
     go_bmc()
     self.fsm = BeFsm.global_master_instance()

 def setUp(self):
     init_nusmv()
     glob.load_from_file(tests.current_directory(__file__)+"/models/dummy_define_justice.smv")
     bmcGlob.go_bmc()
     self.fsm = glob.master_bool_sexp_fsm()

 def setUp(self):
     init_nusmv()
     load_from_file(tests.current_directory(__file__)+"/models/flipflops.smv")
     go_bmc()
     self.enc = BeEnc.global_singleton_instance()
     self.mgr = self.enc.manager

 def test_init_deinit_stats(self):
     init_nusmv()
     deinit_nusmv(ddinfo=True)