# Path: pynusmv/glob.py
# def global_compile_cmps():
# def global_compile_flathierarchy():
# def _reset_globals():
# def load(*model):
# def load_from_string(model):
# def load_from_modules(*modules):
# def load_from_file(filepath):
# def flatten_hierarchy(keep_single_enum=False):
# def symb_table():
# def encode_variables(layers=None, variables_ordering=None):
# def encode_variables_for_layers(layers=None, init=False):
# def bdd_encoding():
# def build_flat_model():
# def build_model():
# def build_boolean_model(force=False):
# def master_bool_sexp_fsm():
# def flat_hierarchy():
# def prop_database():
# def compute_model(variables_ordering=None, keep_single_enum=False):
# def is_cone_of_influence_enabled():
# 
# Path: pynusmv/prop.py
# class Prop(PointerWrapper):
# class PropDb(PointerWrapper):
# class Spec(PointerWrapper):
#     def type(self):
#     def status(self):
#     def name(self):
#     def expr(self):
#     def exprcore(self):
#     def bddFsm(self):
#     def beFsm(self):
#     def scalarFsm(self):
#     def booleanFsm(self):
#     def need_rewriting(self):
#     def master(self):
#     def get_prop_at_index(self, index):
#     def get_size(self):
#     def get_props_of_type(self, prop_type):
#     def __len__(self):
#     def __getitem__(self, index):
#     def __iter__(self):
#     def __init__(self, ptr, freeit=False):
#     def _free(self):
#     def type(self):
#     def car(self):
#     def cdr(self):
#     def __str__(self):
#     def __eq__(self, other):
#     def __hash__(self):
#     def __or__(self, other):
#     def __and__(self, other):
#     def __invert__(self):
# def true():
# def false():
# def not_(spec):
# def and_(left, right):
# def or_(left, right):
# def imply(left, right):
# def iff(left, right):
# def ex(spec):
# def eg(spec):
# def ef(spec):
# def eu(left, right):
# def ew(left, right):
# def ax(spec):
# def ag(spec):
# def af(spec):
# def au(left, right):
# def aw(left, right):
# def x(spec):
# def g(spec):
# def f(spec):
# def u(left, right):
# def atom(strrep, type_checking=True):
# 
# Path: pynusmv/init.py
# def init_nusmv(collecting=True):
#     """
#     Initialize NuSMV. Must be called only once before calling
#     :func:`deinit_nusmv`.
# 
#     :param collecting: Whether or not collecting pointer wrappers to free them
#                        before deiniting nusmv.
# 
#     .. warning: Deactivating the collection of pointer wrappers may provoke
#                 segmentation faults when deiniting nusmv without correctly
#                 freeing all pointer wrappers in advance.
#                 On the other hand, collection may blow memory.
# 
#     """
#     global __collector, __collecting
#     if __collector is not None:
#         raise NuSMVInitError("Cannot initialize NuSMV twice.")
#     else:
#         __collecting = collecting
#         __collector = set()
#         nscinit.NuSMVCore_init_data()
#         nscinit.NuSMVCore_init(None, 0)  # No addons specified
#         nscinit.NuSMVCore_init_cmd_options()
# 
#         # Set NuSMV in interactive mode to avoid fast termination when errors
#         # nsopt.unset_batch(nsopt.OptsHandler_get_instance())
# 
#         # Initialize option commands (set, unset)
#         # to be able to set parser_is_lax
#         nsopt.init_options_cmd()
#         nscmd.Cmd_SecureCommandExecute("set parser_is_lax")
# 
#         return _PyNuSMVContext()
# 
# def deinit_nusmv(ddinfo=False):
#     """
#     Quit NuSMV. Must be called only once, after calling :func:`init_nusmv`.
# 
#     :param ddinfo: Whether or not display Decision Diagrams statistics.
# 
#     """
#     global __collector
#     if __collector is None:
#         raise NuSMVInitError(
#             "Cannot deinitialize NuSMV before initialization.")
#     else:
#         # Apply Python garbage collection first,
#         # then collect every pointer wrapper
#         # that is not yet collected by Python GC
#         from . import glob
# 
#         # Print statistics on stdout about DDs handled by the main DD manager.
#         if ddinfo:
#             try:
#                 manager = glob.prop_database().master.bddFsm.bddEnc.DDmanager
#                 nsdd.dd_print_stats(manager._ptr, nscinit.cvar.nusmv_stdout)
#             except PyNuSMVError:
#                 pass
# 
#         glob._reset_globals()
# 
#         # First garbage collect with Python
#         gc.collect()
#         # Then garbage collect with PyNuSMV
#         for elem in __collector:
#             elem._free()
#         __collector = None
#         nscinit.NuSMVCore_quit()


import unittest
import sys
from pynusmv import glob
from pynusmv.prop import propStatuses
from pynusmv.init import init_nusmv, deinit_nusmv


class TestPropDb(unittest.TestCase):
    
    def setUp(self):
        init_nusmv()
        
    def tearDown(self):
        deinit_nusmv()
    
    def load_admin_model(self):
        glob.load("tests/pynusmv/models/admin.smv")
        glob.compute_model()
        
            
    def test_prop(self):
        self.load_admin_model()
        propDb = glob.prop_database()
        fsm = propDb.master.bddFsm
        
        prop1 = propDb[0]

# Path: pynusmv/glob.py
# def global_compile_cmps():
# def global_compile_flathierarchy():
# def _reset_globals():
# def load(*model):
# def load_from_string(model):
# def load_from_modules(*modules):
# def load_from_file(filepath):
# def flatten_hierarchy(keep_single_enum=False):
# def symb_table():
# def encode_variables(layers=None, variables_ordering=None):
# def encode_variables_for_layers(layers=None, init=False):
# def bdd_encoding():
# def build_flat_model():
# def build_model():
# def build_boolean_model(force=False):
# def master_bool_sexp_fsm():
# def flat_hierarchy():
# def prop_database():
# def compute_model(variables_ordering=None, keep_single_enum=False):
# def is_cone_of_influence_enabled():
# 
# Path: pynusmv/prop.py
# class Prop(PointerWrapper):
# class PropDb(PointerWrapper):
# class Spec(PointerWrapper):
#     def type(self):
#     def status(self):
#     def name(self):
#     def expr(self):
#     def exprcore(self):
#     def bddFsm(self):
#     def beFsm(self):
#     def scalarFsm(self):
#     def booleanFsm(self):
#     def need_rewriting(self):
#     def master(self):
#     def get_prop_at_index(self, index):
#     def get_size(self):
#     def get_props_of_type(self, prop_type):
#     def __len__(self):
#     def __getitem__(self, index):
#     def __iter__(self):
#     def __init__(self, ptr, freeit=False):
#     def _free(self):
#     def type(self):
#     def car(self):
#     def cdr(self):
#     def __str__(self):
#     def __eq__(self, other):
#     def __hash__(self):
#     def __or__(self, other):
#     def __and__(self, other):
#     def __invert__(self):
# def true():
# def false():
# def not_(spec):
# def and_(left, right):
# def or_(left, right):
# def imply(left, right):
# def iff(left, right):
# def ex(spec):
# def eg(spec):
# def ef(spec):
# def eu(left, right):
# def ew(left, right):
# def ax(spec):
# def ag(spec):
# def af(spec):
# def au(left, right):
# def aw(left, right):
# def x(spec):
# def g(spec):
# def f(spec):
# def u(left, right):
# def atom(strrep, type_checking=True):
# 
# Path: pynusmv/init.py
# def init_nusmv(collecting=True):
#     """
#     Initialize NuSMV. Must be called only once before calling
#     :func:`deinit_nusmv`.
# 
#     :param collecting: Whether or not collecting pointer wrappers to free them
#                        before deiniting nusmv.
# 
#     .. warning: Deactivating the collection of pointer wrappers may provoke
#                 segmentation faults when deiniting nusmv without correctly
#                 freeing all pointer wrappers in advance.
#                 On the other hand, collection may blow memory.
# 
#     """
#     global __collector, __collecting
#     if __collector is not None:
#         raise NuSMVInitError("Cannot initialize NuSMV twice.")
#     else:
#         __collecting = collecting
#         __collector = set()
#         nscinit.NuSMVCore_init_data()
#         nscinit.NuSMVCore_init(None, 0)  # No addons specified
#         nscinit.NuSMVCore_init_cmd_options()
# 
#         # Set NuSMV in interactive mode to avoid fast termination when errors
#         # nsopt.unset_batch(nsopt.OptsHandler_get_instance())
# 
#         # Initialize option commands (set, unset)
#         # to be able to set parser_is_lax
#         nsopt.init_options_cmd()
#         nscmd.Cmd_SecureCommandExecute("set parser_is_lax")
# 
#         return _PyNuSMVContext()
# 
# def deinit_nusmv(ddinfo=False):
#     """
#     Quit NuSMV. Must be called only once, after calling :func:`init_nusmv`.
# 
#     :param ddinfo: Whether or not display Decision Diagrams statistics.
# 
#     """
#     global __collector
#     if __collector is None:
#         raise NuSMVInitError(
#             "Cannot deinitialize NuSMV before initialization.")
#     else:
#         # Apply Python garbage collection first,
#         # then collect every pointer wrapper
#         # that is not yet collected by Python GC
#         from . import glob
# 
#         # Print statistics on stdout about DDs handled by the main DD manager.
#         if ddinfo:
#             try:
#                 manager = glob.prop_database().master.bddFsm.bddEnc.DDmanager
#                 nsdd.dd_print_stats(manager._ptr, nscinit.cvar.nusmv_stdout)
#             except PyNuSMVError:
#                 pass
# 
#         glob._reset_globals()
# 
#         # First garbage collect with Python
#         gc.collect()
#         # Then garbage collect with PyNuSMV
#         for elem in __collector:
#             elem._free()
#         __collector = None
#         nscinit.NuSMVCore_quit()


# Path: tests/pynusmv/testProp.py
import unittest
import sys
from pynusmv import glob
from pynusmv.prop import propStatuses
from pynusmv.init import init_nusmv, deinit_nusmv



class TestPropDb(unittest.TestCase):
    
    def setUp(self):
        init_nusmv()
        
    def tearDown(self):
        deinit_nusmv()
    
    def load_admin_model(self):
        glob.load("tests/pynusmv/models/admin.smv")
        glob.compute_model()
        
            
    def test_prop(self):
        self.load_admin_model()
        propDb = glob.prop_database()
        fsm = propDb.master.bddFsm
        
        prop1 = propDb[0]

        self.assertEqual(prop1.status, propStatuses["Unchecked"])