# Path: pynusmv/exception.py
# class NuSMVParsingError(PyNuSMVError):
# 
#     """
#     A :class:`NuSMVParsingError` is a NuSMV parsing exception. Contains several
#     errors accessible through the :attr:`errors` attribute.
# 
#     """
# 
#     def __init__(self, errors):
#         """
#         Initialize this exception with errors.
# 
#         :param errors: a tuple of errors
#         :type errors: tuple(:class:`Error`)
#         """
#         super(NuSMVParsingError, self).__init__(self)
#         self._errors = errors
# 
#     @staticmethod
#     def from_nusmv_errors_list(errors):
#         """
#         Create a new NuSMVParsingError from the given list of NuSMV errors.
# 
#         :param errors: the list of errors from NuSMV
#         """
#         errlist = []
#         while errors is not None:
#             error = nsnode.car(errors)
#             err = nsparser.Parser_get_syntax_error(error)
#             errlist.append(_Error(*err[1:]))
#             errors = nsnode.cdr(errors)
#         return NuSMVParsingError(tuple(errlist))
# 
#     def __str__(self):
#         return "\n".join([str(err) for err in self._errors])
# 
#     def __repr__(self):
#         return repr(self._errors)
# 
#     @property
#     def errors(self):
#         """
#         The tuple of errors of this exception. These errors are tuples
#         `(line, token, message)` representing the line, the token and the
#         message of the error.
# 
#         """
#         return self._errors
# 
# 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_lower_interface.nusmv.node import node as nsnode
from pynusmv_lower_interface.nusmv.parser import parser as nsparser
from pynusmv.parser import *
from pynusmv.exception import NuSMVParsingError
from pynusmv.init import init_nusmv, deinit_nusmv
    def test_good_simple_expressions(self):
        exprs = ["a.car = 3",
                 "e <= 56",
                 "a[4] & t[v]",
                 "inn | outt -> TRUE",
                 "AA + B = C - D",
                 "a -- b = c" # OK because b = c is commented so the expr is 'a'
                ]
        
        for expr in exprs:
            node = parse_simple_expression(expr)
            self.assertIsNotNone(node)
            self.assertIsNotNone(nsnode.sprint_node(node))
            
            
    def test_bad_simple_expressions(self):
        exprs = ["a =",
                 "e <=> 56",
                 "--",
                 "a[4] % t[v]", # The lexer prints an error message at stderr
                                # cannot be avoided
                 "in | outt -> TRUE",
                 "A + B = C - D",
                 "b + 1 -",
                 "next(i) = 3",
                 "init(d) + 5",
                 "a := b"
                ]
        
        for expr in exprs:

# Path: pynusmv/exception.py
# class NuSMVParsingError(PyNuSMVError):
# 
#     """
#     A :class:`NuSMVParsingError` is a NuSMV parsing exception. Contains several
#     errors accessible through the :attr:`errors` attribute.
# 
#     """
# 
#     def __init__(self, errors):
#         """
#         Initialize this exception with errors.
# 
#         :param errors: a tuple of errors
#         :type errors: tuple(:class:`Error`)
#         """
#         super(NuSMVParsingError, self).__init__(self)
#         self._errors = errors
# 
#     @staticmethod
#     def from_nusmv_errors_list(errors):
#         """
#         Create a new NuSMVParsingError from the given list of NuSMV errors.
# 
#         :param errors: the list of errors from NuSMV
#         """
#         errlist = []
#         while errors is not None:
#             error = nsnode.car(errors)
#             err = nsparser.Parser_get_syntax_error(error)
#             errlist.append(_Error(*err[1:]))
#             errors = nsnode.cdr(errors)
#         return NuSMVParsingError(tuple(errlist))
# 
#     def __str__(self):
#         return "\n".join([str(err) for err in self._errors])
# 
#     def __repr__(self):
#         return repr(self._errors)
# 
#     @property
#     def errors(self):
#         """
#         The tuple of errors of this exception. These errors are tuples
#         `(line, token, message)` representing the line, the token and the
#         message of the error.
# 
#         """
#         return self._errors
# 
# 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/testPyNuSMVParsing.py
import unittest
import sys
from pynusmv_lower_interface.nusmv.node import node as nsnode
from pynusmv_lower_interface.nusmv.parser import parser as nsparser
from pynusmv.parser import *
from pynusmv.exception import NuSMVParsingError
from pynusmv.init import init_nusmv, deinit_nusmv

    def test_good_simple_expressions(self):
        exprs = ["a.car = 3",
                 "e <= 56",
                 "a[4] & t[v]",
                 "inn | outt -> TRUE",
                 "AA + B = C - D",
                 "a -- b = c" # OK because b = c is commented so the expr is 'a'
                ]
        
        for expr in exprs:
            node = parse_simple_expression(expr)
            self.assertIsNotNone(node)
            self.assertIsNotNone(nsnode.sprint_node(node))
            
            
    def test_bad_simple_expressions(self):
        exprs = ["a =",
                 "e <=> 56",
                 "--",
                 "a[4] % t[v]", # The lexer prints an error message at stderr
                                # cannot be avoided
                 "in | outt -> TRUE",
                 "A + B = C - D",
                 "b + 1 -",
                 "next(i) = 3",
                 "init(d) + 5",
                 "a := b"
                ]
        
        for expr in exprs:

            with self.assertRaises(NuSMVParsingError):