def todo(fn):
def skip(reason):
def _log(fn, message):
def canonical_cnf(be):
def current_directory(what):
    def __init__(self, testcase, location, model):
    def __enter__(self):
    def __exit__(self, type_, value, traceback):
class Configure: 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() def load(*model):
    """
    Load the given model. This model can be of several forms:

    * a file path; in this case, the model is loaded from the file;
    * NuSMV modelling code; in this case, `model` is the code for the model;
    * a list of modules (list of :class:`Module <pynusmv.model.Module>`
      subclasses); in this case, the model is represented by the set of
      modules.

    """
    if len(model) == 1 and isinstance(model[0], str):
        if os.path.isfile(model[0]):
            load_from_file(model[0])
        else:
            load_from_string(model[0])
    else:  # model must be a list of modules
        load_from_modules(*model) def master_bool_sexp_fsm():
    """
    Return the global boolean SEXP model.

    :rtype: :class:`BoolSexpFsm <pynusmv.sexp.BoolSexpFsm>`
    """
    global __bool_sexp_fsm

    if not nscompile.cmp_struct_get_build_bool_model(global_compile_cmps()):
        raise NuSMVNeedBooleanModelError("boolean model not initialized")

    if __bool_sexp_fsm is None:
        propdb  = nsprop.PropPkg_get_prop_database()
        fsm_ptr = nsprop.PropDb_master_get_bool_sexp_fsm(propdb)
        __bool_sexp_fsm = BoolSexpFsm(fsm_ptr, freeit=False)
    return __bool_sexp_fsm def parse_ltl_spec(spec):
    """
    Parse a LTL specification

    :param string spec: the specification to parse
    :raise: a :exc:`NuSMVParsingError <pynusmv.exception.NuSMVParsingError>`
            if a parsing error occurs

    .. warning:: Returned value is a SWIG wrapper for the NuSMV node_ptr.
       It is the responsibility of the caller to manage it.

    """
    node, err = nsparser.ReadCmdFromString("LTLWFF " + spec)
    if err:
        errors = nsparser.Parser_get_syntax_errors_list()
        raise NuSMVParsingError.from_nusmv_errors_list(errors)
    else:
        node = nsnode.car(node)  # Get rid of the top CTLWFF node
        if node.type is nsparser.CONTEXT and nsnode.car(node) is None:
            # Get rid of the top empty context if any
            return nsnode.cdr(node)
        else:
            return node def parse_simple_expression(expression):
    """
    Parse a simple expression.

    :param string expression: the expression to parse
    :raise: a :exc:`NuSMVParsingError
            <pynusmv.exception.NuSMVParsingError>`
            if a parsing error occurs

    .. warning:: Returned value is a SWIG wrapper for the NuSMV node_ptr.
       It is the responsibility of the caller to manage it.

    """
    node, err = nsparser.ReadSimpExprFromString(expression)
    if err:
        errors = nsparser.Parser_get_syntax_errors_list()
        raise NuSMVParsingError.from_nusmv_errors_list(errors)
    else:
        node = nsnode.car(node)  # Get rid of the top SIMPWFF node
        if node.type is nsparser.CONTEXT and nsnode.car(node) is None:
            # Get rid of the top empty context if any
            return nsnode.cdr(node)
        else:
            return node class Node(PointerWrapper):

    """A generic NuSMV node."""

    def __init__(self, left, right, type_=None):
        """
        Create a new node of `type_` with `left` and `right` as left and right
        branches.

        If `type_` is None, the type is infered from the instantiated class.

        :param left: the left branch
        :type left: :class:`Node` or `None`
        :param right: the right branch
        :type right: :class:`Node` or `None`
        :param type_: the type of the node
        :type type_: `int`

        """

        if type_ is None:
            type_ = class_to_type[type(self)]

        left_ptr = left._ptr if left is not None else left
        right_ptr = right._ptr if right is not None else right

        ptr = nsnode.find_node(type_, left_ptr, right_ptr)
        super().__init__(ptr, freeit=False)
        self.type = type_
        self._car = left
        self._cdr = right

    @property
    def car(self):
        """The left branch of this node."""
        if not hasattr(self, "_car"):
            # Create the node
            car = nsnode.car(self._ptr)
            if car is not None:
                self._car = Node.from_ptr(car)
            else:
                self._car = None
        return self._car

    @property
    def cdr(self):
        """The right branch of this node."""
        if not hasattr(self, "_cdr"):
            # Create the node
            cdr = nsnode.cdr(self._ptr)
            if cdr is not None:
                self._cdr = Node.from_ptr(cdr)
            else:
                self._cdr = None
        return self._cdr

    def _free(self):
        if self._freeit and self._ptr is not None:
            nsnode.node_free(self._ptr)
            self._freeit = False

    def __str__(self):
        return nsnode.sprint_node(self._ptr)

    def __repr__(self): # makes debugging easier
        return nsnode.sprint_node(self._ptr)

    def __eq__(self, other):
        """Return whether `self` is equals to `other`."""
        if isinstance(self, type(other)):
            return nsnode.node_equal(self._ptr, other._ptr) != 0
        else:
            return False

    def __hash__(self):
        return nsnode.node2int(self._ptr)

    def __deepcopy__(self, memo):
        # Does not need to deep copy since these are immutable
        # and pointers would be the same
        return self

    @staticmethod
    def from_ptr(ptr, freeit=False):
        if ptr is None:
            return None
        cls = type_to_class[ptr.type]
        new_node = cls.__new__(cls)
        new_node._freeit = freeit
        new_node._ptr = ptr
        new_node.type = ptr.type
        return new_node

    @staticmethod
    def _handle_next_expression(expression):
        """
        Return a node representation of the next `expression`.
        If `expression` is already an Expresssion, return it as it is.
        If `expression` is a string of an integer, it is parsed as a next
        expression.

        :param expression: the expression to handle
        :type expression: :class:`Expression` or :class:`str` or :class:`int`
        """
        if isinstance(expression, int):
            expression = str(expression)
        if isinstance(expression, str):
            parsed = parse_next_expression(expression)
            expression = Node.from_ptr(find_hierarchy(parsed))
            nsnode.free_node(parsed)
        return expression class NodeList(PointerWrapper, Iterable):
    """
    This class implements a pythonic interface to NuSMV's internal version of a
    doubly linked list
    
    .. note:: The following apis have not been exposed since they require pointer
      to function (in C) which are considered too low level for this pythonic
      interface. However, these apis are accessible using 
      pynusmv_lower_interface.nusmv.utils.utils.<TheAPI> and passing nodelst._ptr instead of 
      nodelist.
      
        - NodeList_remove_elems
        - NodeList_search
        - NodeList_foreach
        - NodeList_map
        - NodeList_filter
    """
    def __init__(self, ptr, conversion=NodeConversion(),freeit=False):
        """
        Creates a new instance from the given pointer and conversion
        :param ptr: the pointer to a NuSMV NodeList to be wrapped
        :param conversion: the conversion object allowing the transformation
           from pointer to object and vice versa
        :param freeit: a flag indicating whether or not this list should be 
           freed upon garbage collection
        """
        # super is PointerWrapper since it's the first in the mro order
        super().__init__(ptr, freeit=freeit)
        self._conv = conversion
        
    def _free(self):
        """Overrides PointerWrapper._free()"""
        if self._freeit and self._ptr is not None:
            _utils.NodeList_destroy(self._ptr)
            
    def __str__(self):
        return 'NodeList'+str(list(self))        
    
    @staticmethod
    def empty(conversion=NodeConversion(), freeit=True):
        """
        Creates a new empty list
        
        :param conversion: the conversion object allowing the transformation
           from pointer to object and vice versa
        :param freeit: a flag indicating whether or not this list should be 
           freed upon garbage collection
        """
        return NodeList(_utils.NodeList_create(), conversion, freeit)
    
    # from_list ~~> from node, not exposed => use NodeIter instead
    
    @staticmethod
    def from_list(lst, conversion=NodeConversion(), freeit=True):
        """
        :return: a NodeList equivalent to the pythonic list `lst`
        :param lst: the list which shall serve as basis for the created one
        :param conversion: the object encapsulating the conversion back and forth
          from and to pointer
        :param freeit: a flag indicating whether or not this list should be freed
          upon garbage collection
        """
        ret = NodeList.empty(conversion, freeit)
        for v in lst:
            ret.append(v)
            
        return ret
    
    def copy(self, freeit=True):
        """
        :param freeit: a flag indicating whether or not the copy shoudl be freed
          upon garbage collection
        :return: Returns a copy of this list
        """
        return self.__copy__(freeit)
    
    def __copy__(self, freeit=True):
        """
        :param freeit: a flag indicating whether or not the copy shoudl be freed
          upon garbage collection
        :return: Returns a copy of this list
        """
        pointer = _utils.NodeList_copy(self._ptr)
        return NodeList(pointer, self._conv, freeit)
    
    def append(self, node):
        """
        Adds the given node at the end of the list
        
        :param node: the node to append to the list
        """
        _utils.NodeList_append(self._ptr, self._conv.to_pointer(node))
        
    def prepend(self, node):
        """
        Adds the given node at the beginning of the list
        
        :param node: the node to append to the list
        """
        _utils.NodeList_prepend(self._ptr, self._conv.to_pointer(node))
        
    def __len__(self):
        """:return: the length of the list"""
        return _utils.NodeList_get_length(self._ptr)
    
    def reverse(self):
        """inverts the order of the items in the list"""
        _utils.NodeList_reverse(self._ptr)
        
    def extend(self, other, unique=False):
        """
        Appends all the iems of `other` to this list. If param unique is set to
        true, the items are only appended if not already present in the list.
        
        :param other: the other list to concatenate to this one
        :param unique: a flag to conditionally add the elements of the other list
        """
        if unique:
            _utils.NodeList_concat_unique(self._ptr, other._ptr)
        else:
            _utils.NodeList_concat(self._ptr, other._ptr)
        
    def __contains__(self, node):
        """
        :return: True iff node belongs to this list
        :param node: the node whose appartenance is being tested
        """ 
        return _utils.NodeList_belongs_to(self._ptr, self._conv.to_pointer(node))
    
    def count(self, node):
        """
        :return: the number of occurences of `node`
        :param node: the node whose number of occurrences is being counted
        """
        return _utils.NodeList_count_elem(self._ptr, self._conv.to_pointer(node))
    
    def __getitem__(self, idx):
        """
        :return: the idx-th item of the list
        :raise: KeyError when the idx is not one of the possible indices of the
          list
        .. warning:: This implementation is O(idx) despite the syntax sugar making
          it look like O(1) 
        """
        counter = 0
        for node in self:
            if idx == counter: 
                return node
            counter += 1
        raise KeyError("Index {} is out of the list bounds".format(idx))

    def __delitem__(self, idx):
        """
        .. warning:: This implementation is O(idx) despite the syntax sugar making
          it look like O(1) 
          
        .. warning:: In case no value corresponds to idx, no warning is issued
        """
        iterator = iter(self)
        for _ in range(idx):
            iterator.__next__()
        _utils.NodeList_remove_elem_at(self._ptr, iterator._ptr) 
    
    def __iter__(self):
        """:return: an iterator to walk through this list"""
        return NodeListIter(self)
    
    def insert_before(self, iterator, node):
        """
        inserts `node` right before the position pointed by iterator
        :param iterator: the iterator pointing the position where to insert
        :param node: the node to insert in the list
        """
        _utils.NodeList_insert_before(self._ptr, iterator._ptr, self._conv.to_pointer(node))
        
    def insert_after(self, iterator, node):
        """
        inserts `node` right after the position pointed by iterator
        :param iterator: the iterator pointing the position where to insert
        :param node: the node to insert in the list
        """
        if _utils.ListIter_is_end(iterator._ptr):
            raise ValueError("impossible to add after an end iterator")
        else:
            _utils.NodeList_insert_after(self._ptr, iterator._ptr, self._conv.to_pointer(node))
        
    def insert_at(self, idx, node):
        """
        inserts `node` right before the node at position `idx`
        :param idx: the the position where to insert
        """
        iterator = iter(self)
        for _ in range(idx):
            iterator.__next__()
        _utils.NodeList_insert_before(self._ptr, iterator._ptr, self._conv.to_pointer(node))
    
    def print_nodes(self, stdio_file):
        """
        Prints the list node to the given stream.
        :param stdio_file: an instance of StdioFile wrapping an open C stream
        """
        _utils.NodeList_print_nodes(self._ptr, stdio_file.handle) class BmcSupport:
    """
    This class implements a context manager (an object that can be used with a 
    'with' statement) that initializes and deinitialises BMC and its submodules.
    
    .. note::
        
        The 'support' part in the name of this class does not bear the 
        sometimes used signification of 'what makes a formula true'. Instead, 
        it is present to make the code read easily (and be easily understood
        when read)
    
    Example::
    
        with init_nusmv():
            load(model)
             
            with BmcSupport():
                # do something smart like verifying LTL properties.
    """
    def __enter__(self):
        """Magic method for the initialisation"""
        go_bmc()
    
    def __exit__(self, typ, value, traceback):
        """Magic method for the de-initialisation"""
        bmc_exit() def master_be_fsm():
    """
    :return: the boolean FSM in BE stored in the master prop. 
    :raises NuSMVBeFsmMasterInstanceNotInitializedError:
         when the global BE FSM is null in the global properties database 
         (ie when coi is enabled).
    """
    global __be_fsm
    if __be_fsm is None:
        __be_fsm = BeFsm.global_master_instance()
    return __be_fsm def generate_counter_example(fsm, problem, solver, k, descr="BMC counter example"):
    """
    Generates a counter example for `problem` evaluated against `fsm` as 
    identified by `solver` (problem has a length `k`) but prints nothing.
    
    .. note::
        
        If you are looking for something more advanced, you might want to look
        at :func:`pynusmv.be.encoder.BeEnc.decode_sat_model` which does the same
        thing but is more complete.
    
    :param fsm: the FSM against which problem was evaluated
    :param problem: the SAT problem used to identify a counter example
    :param solver: the SAT solver that identified a counter example
    :param k: the length of the generated problem (length in terms of state)
    :param descr: a description of what the generated counter example is about
    :raises ValueError: whenever the problem or the solver is None or when the 
        problem bound `k` is negative.
    """
    if problem is None:
        raise ValueError("a problem must be given")
    if solver is None:
        raise ValueError("a solver must be given")
    if k < 0:
        raise ValueError("the problem bound `k` must be non negative")
    
    ptr = _bmc.Bmc_Utils_generate_cntexample(
            fsm.encoding._ptr, solver._as_SatSolver_ptr(),
            problem._ptr, k, descr,
            glob.master_bool_sexp_fsm().symbols_list._ptr)
    return Trace(ptr) def generate_ltl_problem(fsm, prop_node, bound=10, loop=utils.all_loopbacks()):
    """
    Generates a (non-incremental) Be expression corresponding to the SAT problem
    denoted by :math:`[[fsm, prop\\_node]]_{bound}^{loop}`
    
    That is to say it generates the problem that combines both the formula and
    and the model to perform the verification. Put another way, this problem
    can be read as: 
    
    .. math::
    
        [[fsm]]_{bound} \\wedge \\neg ( (\\neg L_k \\wedge [[ \\neg prop\\_node]]_{k}) \\vee {}_{l}[[ \\neg prop\\_node]]_{k}^{l} )
     
    :param fsm: the BeFsm object that represents the model against which the 
        property will be verified. (if in doubt, it can be obtained via 
        :func:`pynusmv.bmc.glob.master_be_fsm()` )
    :param prop_node: the property for which to generate a verification problem
        represented in a 'node' format (subclass of :class:`pynusmv.node.Node`)
        which corresponds to the format obtained from the ast. (remark: if you
        need to manipulate [ie negate] the formula before passing it, it is
        perfectly valid to pass a node decorated by `Wff.decorate`).
    :param bound: the bound of the problem, that is to say the maximum number of 
        times the problem will be unrolled. This parameter corresponds to the 
        value `k` used in the formal definitions of a bmc problem.
    :param loop: a loop definition. This is an integer value corresponding to 
        the moment in time where the loop might be starting (the parameter `l`
        in the formal definitions). However, this value is not as 'crude' as an
        absolute moment in time since it may indicate:
        
            - an absolute moment in time (obviously) when the value is positive
            - indicate a relative moment in time (when it is a negative number
              (for instance value -2 indicates that the loops are supposed to
              start 2 states ago)
            - that NO loop at all must be considered (ignore infinite behaviors)
              when this parameter takes the special value defined in 
              :func:`pynusmv.bmc.utils.no_loopback()`
            - that ALL possible loops in the model must be taken into account
              when this parameter takes the special value defined in
              :func:`pynusmv.bmc.utils.all_loopback()` (this is the default)
              
    :return: a Be boolean expression representing the satisfiability problem of
        for the verification of this property.
    :raises ValueError: when the bound is infeasible (negative value) or when
        the loop and bound values are inconsistent (loop is greater than the
        bound but none of the special values described above)
    """
    utils.check_consistency(bound, loop)
    
    ltl_wff = utils.make_negated_nnf_boolean_wff(prop_node)
    be_ptr  = _bmc.Bmc_Gen_LtlProblem(fsm._ptr, ltl_wff._ptr, bound, loop)
    return Be(be_ptr, fsm.encoding.manager) class SatSolverFactory():
    # =========================================================================
    # ========== Utility functions ============================================
    # =========================================================================
    @staticmethod
    def normalize_name(name):
        """
        :return: a normalized solver name corresponding to the given `name`.
          (Only case should be changed)
        :param name: the name (string) of the solver to normalize.
        :raise: ValueError whenever the name corresponds to none of the 
          available solvers
        """
        normalized = _sat.Sat_NormalizeSatSolverName(name)
        if normalized is None:
            raise ValueError("No such SAT solver available : {}".format(name))
        else:
            return normalized

    @staticmethod
    def available_solvers():
        """
        :return: a list with the name of the solvers that can be instantiated
        """
        return set(_sat.Sat_GetAvailableSolversString().split())
    
    @staticmethod 
    def print_available_solvers(stdio_file=utils.StdioFile.stdout()):
        """
        prints the list of available SAT solvers to the given stdio file 
        """
        _sat.Sat_PrintAvailableSolvers(stdio_file.handle)
        
    @staticmethod
    def create(name='MiniSat', incremental=True, proof=True):
        """
        Creates a new sat solver corresponding to the given name and capabilities
        :param name: the name of the solver to instanciate 
        :param incremental: a flag indicating whether the instanciated solver
        should have incremental capabilities
        :param proof: a flag indicating whether the instanciated solver should
        have proof logging capability.
        :return: a new sat solver corresponding to the given name and capabilities
        
        :raise: Given that ZChaff does not support proof logging, this method
          raises a ValueError when prooflogging is turned on and zchaff is passed
          as name parameter.
        """
        if SatSolverFactory.normalize_name(name) == 'ZChaff' and proof:
            raise ValueError("""
                Proof logging not supported when using the zchaff  SAT Solver. 
                Please retry using MiniSat
                """)
        
        if incremental:
            if proof:
                return SatIncProofSolver(
                                _sat.Sat_CreateIncProofSolver(name))
            else:
                return SatIncSolver(_sat.Sat_CreateIncSolver(name))
        else:
            if proof:
                return SatProofSolver(
                                _sat.Sat_CreateNonIncProofSolver(name))
            else:
                return SatSolver(
                                _sat.Sat_CreateNonIncSolver(name))
        raise Exception("Could not create solver") class Polarity(IntEnum):
    """
    In general, a polarity is assigned to a formula and its variables. If this
    were not done, this would potentially slow down the solver because the 
    solver would unnecessarily try to assign values to many variables.
    """
    POSITIVE =  1
    NEGATIVE = -1
    NOT_SET  =  0 class Trace(PointerWrapper, Iterable):
    """
    Encapsulates the details of a counter example trace.
    """
    
    def __init__(self, ptr, freeit=False):
        super().__init__(ptr, freeit=freeit)
        
    def _free(self):
        if self._freeit and self._ptr is not None:
            _trace.Trace_destroy(self._ptr)
            self._ptr = None
            self._freeit = False
            
    @staticmethod
    def create(description, trace_type, symb_table, symbols_list, is_volatile):
        """
        Creates a new (empty trace)
        
        :param description: a text describing what the trace is describing
        :param trace_type: an enumeration value (:class:`TraceType`) describing
            how the trace should be interpreted
        :param symb_table: the symbol table used to associate an human
            meaningful symbol to the internal representation of the trace
        :param symb_list: a NodeList (:class:`pynusmv.collections.NodeList`) 
            containing the various symbols that may appear in the trace.
            Note, this is not a regular python list but you can obtain a NodeList
            using `NodeList.from_list` if you need to. In case you just use
            SexpFsm (:func:`pynusmv.sexp.fsm.SexpFsm.symbols_list`) then no
            conversion is required as it already yields a NodeList
        :param is_volatile: a flag indicating whether or not the created insrance
            should be responsible of the symbol table reference it owns
        """
        ptr = _trace.Trace_create(symb_table._ptr, 
                                  description, 
                                  trace_type, 
                                  symbols_list._ptr, 
                                  is_volatile)
        return Trace(ptr, freeit=True)
    
    def concat(self, other):
        """
        Concatenates all the content from `other` to self and destroys other.
        
        .. warning::
            
            The initial state of `other` is not copied over to self.
        
        :param other: the other trace to append to self 
        """
        if other.is_registered:
            raise NuSmvIllegalTraceStateError("Cannot concat a registered trace")
        _trace.Trace_concatenate(self._ptr, other._ptr)
        # This function is DESTRUCTIVE !
        other._ptr = None
        other._freeit = False
        return self
    
    @property
    def id(self):
        """
        An unique identifier for this trace (a non-negative number)
        
        :return: an unique identifier for this trace
        """
        return _trace.Trace_get_id(self._ptr) 
    
    @property
    def description(self):
        """:return: this trace description in a human friendly format"""
        return _trace.Trace_get_desc(self._ptr)
    
    @description.setter
    def description(self, desc):
        """
        Sets a new description to explain what this trace is about
        
        :param desc: the new description value
        """
        _trace.Trace_set_desc(self._ptr, desc)
    
    @property
    def type(self):
        """
        Returns the TraceType (:class:`TraceType`) explaining how this
        trace should be interpreted
        
        :return: the trace type of this trace
        """
        return TraceType(_trace.Trace_get_type(self._ptr))
    
    @type.setter
    def type(self, trace_type):
        """
        Sets the type of this trace (a value explaining how to interpret this
        trace (:class:`TraceType`).
        
        :param trace_type: the new trace type
        """
        _trace.Trace_set_type(self._ptr, trace_type)
        
    @property
    def length(self):
        """
        Length for a trace is defined as the number of the transitions in it. 
        Thus, a trace consisting only of an initial state is a 0-length trace. 
        A trace with two states is a 1-length trace and so forth.
               
        :return: the length of this trace
        """
        return _trace.Trace_get_length(self._ptr)
    
    def __len__(self):
        """:return: the length of this trace (using the built in function)"""
        return self.length
    
    @property
    def is_empty(self):
        """
        Tests this trace for emptiness
        
        :return: True iff this trace is empty (that is to say it has length==0)
        """
        return bool(_trace.Trace_is_empty(self._ptr))
        
    @property
    def is_volatile(self):
        """
        A trace is volatile if it is not the owner of its symbol table reference
        
        :return: a flag indicating whether or not the trace is volatile
        """
        return bool(_trace.Trace_is_volatile(self._ptr)) 
        
    @property
    def is_registered(self):
        """
        :return: true iff the trace is registered with a trace manager
        """
        return bool(_trace.Trace_is_registered(self._ptr))
    
    def register(self, identifier):
        """
        sets the id of the trace (to be called by the trace manager when the
        trace gets registered in that context)
        
        :param identifier: an id for this trace
        """
        _trace.Trace_register(self._ptr, identifier)
        
    def unregister(self):
        """
        De-associates this trace from the trace manager it was previously 
        registered with
        """
        _trace.Trace_unregister(self._ptr)
        
    @property
    def is_frozen(self):
        """
        A frozen trace holds explicit information about loopbacks and can not 
        be appended a step, or added a variable value.

        .. warning::
        
            After freezing no automatic looback calculation will be performed: 
            it is up to the owner of the trace to manually add loopback 
            information.
            
        :return: True iff this trace is frozen.
        """
        return bool(_trace.Trace_is_frozen(self._ptr))
    
    def freeze(self):
        """
        Forces this trace to enter the frozen state so as to be able to add
        loopback information on this trace.
        
        A frozen trace holds explicit information about loopbacks. Its length 
        and assignments are immutable, that is it cannot be appended more steps,
        nor can it accept more values that those already stored in it.

        Still it is possible to register/unregister the trace and to change its
        type or description.
        
        .. warning::
        
            After freezing no automatic looback calculation is performed: it is
            up to the owner of the trace to manually add loopback information.
        """
        _trace.Trace_freeze(self._ptr)
    
    @property
    def is_thawed(self):
        """
        A thawed trace holds no explicit information about loopbacks and can be 
        appended a step or added a variable value.
        
        .. note::
            
            As the name suggests, thawed <-> ! frozen.

        .. warning:: 
        
            After thawing the trace will not persistently retain any loopback 
            information. In particular it is *illegal* to force a loopback on 
            a thawed trace.
        """
        return bool(_trace.Trace_is_thawed(self._ptr))
    
    def thaw(self):
        """
        Forces this trace to enter the thawed state so as to enable the 
        addition of steps or variables.
        
        .. note::
            
            As the name suggests, thawed <-> ! frozen.
            
        
        .. warning:: 
        
            After thawing the trace will not persistently retain any loopback 
            information. In particular it is *illegal* to force a loopback on 
            a thawed trace.
        """
        _trace.Trace_thaw(self._ptr)
    
    def equals(self, other):
        """
        Two traces are equals iff:

        1. They're the same object or None.
        2. They have exactly the same language, length, assignments for all 
           variables in all times and the same loopbacks.

                 (Defines are not taken into account for equality.)

        .. note:: 
        
            In order to be considered equal, the two traces need not be both 
            frozen/thawed, and to both have the same registration status. 
            (Of course two traces *cannot* have the same ID).
            
        .. warning::
        
            This test implements an 'equals logic', not an 'is same' logic 
            since the id field of the trace is not considered in the comparison.
            
            Hence, this equality test is inconsistent with the result of __hash__
        """
        if other is None: 
            return False
        return bool(_trace.Trace_equals(self._ptr, other._ptr))
    
    def __eq__(self, other):
        """
        Magic method to perform an equality test
        
        .. warning::
        
            This test implements an 'equals logic', not an 'is same' logic 
            since the id field of the trace is not considered in the comparison.
            
            Hence, this equality test is inconsistent with the result of __hash__
        """
        return self.equals(other)
    
    def append_step(self):
        """
        Creates and return a new step which is appended to the current trace
        
        :return: a new trace step which corresponds to the last step of the 
            trace.
        """
        return TraceStep(self, _trace.Trace_append_step(self._ptr))
    
    @property
    def symbol_table(self):
        """:return the symbol table associated to this trace"""
        return SymbTable(_trace.Trace_get_symb_table(self._ptr))
    
    @property
    def symbols(self):
        """
        Returns a NodeList (:class:`pynusmv.collections.NodeList`)
        exposing the symbols of the trace language.
        
        :returns: a NodeList exposing the symbols of the trace language
        """
        return NodeList(_trace.Trace_get_symbols(self._ptr))
    
    @property
    def state_vars(self):
        """
        Returns a NodeList  (:class:`pynusmv.collections.NodeList`)
        exposing the state variables that exist in the trace language
        
        :return: a NodeList containing the state variables of the trace language
        """
        return NodeList(_trace.Trace_get_s_vars(self._ptr))
    
    @property
    def state_frozen_vars(self):
        """
        Returns a NodeList  (:class:`pynusmv.collections.NodeList`)
        exposing the state and frozen variables that exist in the trace language
        
        :return: a NodeList containing the state and frozen variables of the 
            trace language
        """
        return NodeList(_trace.Trace_get_sf_vars(self._ptr))
    
    @property
    def input_vars(self):
        """
        Returns a NodeList  (:class:`pynusmv.collections.NodeList`)
        exposing the input variables that exist in the trace language
        
        :return: a NodeList containing the input variables of the trace language
        """
        return NodeList(_trace.Trace_get_i_vars(self._ptr))
    
    def language_contains(self, symbol_node):
        """
        Tests whether the given symbol represented by `symbol_node` 
        (:class:`pynusmv.node.Node`) belongs to the trace language.
        
        .. note::
        
            A more pythonic accessor is foreseen for the same purpose. If you
            prefer, you may perfectly use `symb_node` in `self` to get the
            exact same result. 
            
        :returns: True iff this symbol_node belongs to the trace language.
        """
        return bool(_trace.Trace_symbol_in_language(self._ptr, symbol_node._ptr))
    
    def __contains__(self, symbol_node):
        """
        Tests whether the given symbol represented by `symbol_node` 
        (:class:`pynusmv.node.Node`) belongs to the trace language.
        
        :returns: True iff this symbol_node belongs to the trace language.
        """
        return self.language_contains(symbol_node)
    
    def is_complete(self, vars_nlist, report=False):
        """
        Checks if a Trace is complete on the given set of vars
        
        A Trace is complete iff in every node, all vars are given a value

        .. note::

                * Only input and state section are taken into account.
                  Input vars are not taken into account in the first
                  step. Defines are not taken into account at all.
                * If result is false and parameter 'report' is true
                  then a message will be output in nusmv_stderr with
                  some explanation of why the trace is not complete
                
        :param vars_nlist: a NodeList of variable symbols that need to have a
            value in order for the trace to be considered complete.
            (:class:`pynusmv.collections.NodeList`)
            
        :return: True iff the trace has a value associated to each of the vars
            in vars_nlist.
        """
        return bool(_trace.Trace_is_complete(self._ptr, vars_nlist._ptr, report))

    def __iter__(self):
        """Iterator that permits an easy navigation in the steps of the trace"""
        for i in range(1, len(self)+2):
            yield self.steps[i]
    
    @indexed.getter
    def steps(self, i):
        """
        Returns the ith step of the trace
        
        .. warning::
        
            the indices start at 1
        
        :param i: the index/time of the step to fetch
        :return: the ith step of this trace
        """
        if i < 1 or i > self.length+1:
            raise KeyError("step index not in the range [0; {}]".format(len(self)+1))
        return TraceStep(self, _trace.Trace_ith_iter(self._ptr, i))
    
    def __repr__(self):
        """
        Returns a string representation of this object.
        """
        text ="""******************************************************\n"""
        text+= "{} : {}\n".format(str(self.type), self.description)
        for step in self:
            text+= str(step)
        return text
    # NOTE: covers language does not exist in the C code.
    #       public api for symbol_is_assigned not found in C code either class TraceType(IntEnum):
    """
    The possible types of traces
    """
    UNSPECIFIED     = _trace.TRACE_TYPE_UNSPECIFIED,
    COUNTER_EXAMPLE = _trace.TRACE_TYPE_CNTEXAMPLE,
    SIMULATION      = _trace.TRACE_TYPE_SIMULATION,
    EXECUTION       = _trace.TRACE_TYPE_EXECUTION,
    END             = _trace.TRACE_TYPE_END
    
    def __str__(self):
        """:return: a string representation of this trace type"""
        return _trace.TraceType_to_string(self) class TraceStep:
    """
    Encapsulates the details of what step is in a trace. In the context of a 
    trace, a step is considered to be a container for incoming input and next
    state (i.e. it has the form <i, S>)
    """
    
    def __init__(self, trace, step_ptr):
        """
        Creates a new instance
        
        :param trace: the parent trace (the one to which this step belongs to)
        :param step_ptr: a swig wrapper to the unerlying NuSMV pointer 
            representing this step (:type: `TraceIter`)
        """
        self.trace = trace
        self._ptr  = step_ptr
        
    @property
    def is_loopback(self):
        """
        Tests whether the state denoted by this step is a loopback state w.r.t 
        the last state in the parent trace.
        
        This function behaves accordingly to two different modes a trace  can 
        be: frozen or thawed(default).

        If the trace is frozen, permanent loopback information is used to 
        determine if this step has a loopback state and no further loopback 
        computation is made.
        
        If the trace is thawed, dynamic loopback calculation takes place, using
        a variant of Rabin-Karp pattern matching algorithm.
        
        .. note::
        
            No matter the configuration, the last step of a trace is always 
            seen as *NOT* being a loopback step.
        """
        return bool(_trace.Trace_step_is_loopback(self.trace._ptr, self._ptr))
    
    def force_loopback(self):
        """
        Forces this step to be considered as a loopback step using explicit 
        loopback information (trace must be frozen)
        
        Use this function to store explicit loopback information in a frozen 
        trace. The trace will retain loopback data until it is thawed again.
        
        :raises NuSmvIllegalTraceStateError: if the parent trace is not frozen
        """
        if not self.trace.is_frozen :
            raise NuSmvIllegalTraceStateError(
                    """
                    The parent trace must be frozen before explicit loopback 
                    information can be used
                    """)
        
        _trace.Trace_step_force_loopback(self.trace._ptr, self._ptr)
    
    def assign(self, symbol_node, value_node):
        """
        Stores an assignment into a trace step
        
        .. warning::
        
            Assignments to symbols not in trace language are silently ignored.
        
        
        :param symbol_node: a Node (:class:`pynusmv.node.Node`) 
            representing the symbol to which a value is assigned
        :param value_node: a Node (:class:`pynusmv.node.Node`)
            representing the value being assigned to the symbol
        
        :return: true iff the assignment worked smoothly.
        
        :raises NuSmvIllegalTraceStateError: if the parent trace is frozen
        """   
        if self.trace.is_frozen:
            raise NuSmvIllegalTraceStateError(
                        """
                        The parent trace must be thawed before any assignment
                        can be added to this trace step.
                        """)
        return bool(_trace.Trace_step_put_value(self.trace._ptr,
                                                self._ptr, 
                                                symbol_node._ptr, 
                                                value_node._ptr))
        
    def __iadd__(self, assignment):
        """
        Stores an assignment into a trace step
        
        .. note::
        
            Assignments to symbols not in trace language are silently ignored.
        
        :param assignment: is a tuple composed of a symbol_node (:class:`pynusmv.node.Node`)
            representing the symbol to which an assignment is made and a
            value_node (:class:`pynusmv.node.Node`) representing the value being
            assigned to the symbol.
            
        :raises NuSmvIllegalTraceStateError: if the parent trace is frozen
        """
        self.assign(assignment[0], assignment[1])
        return self
        
    @indexed.getter
    def value(self, symbol_node):
        """
        Retrieves the value that was assigned to `symbol_node` in the current
        trace step.
        
        :param symbol_node: a Node (:class:`pynusmv.node.Node`) 
            representing the symbol to which a value is assigned
        :return: a value_node, that is to say a Node (:class:`pynusmv.node.Node`)
            representing the value being assigned to the requested symbol.   
        """
        return Node.from_ptr(_trace.Trace_step_get_value(
                                            self.trace._ptr, 
                                            self._ptr, 
                                            symbol_node._ptr))
        
    def __iter__(self):
        """
        :return: an iterator to iterate over the variables symbols of this step
        """
        # NuSMV advises not to use Trace_step_iter. This implementation is safer
        # and works well
        for sym in self.trace.symbols:
            value = self.value[sym]
            if value is not None:
                yield (sym, value)
    
    def __repr__(self):
        """
        Returns a string representation of this object.
        """
        text = """****** Step ******* is_loopback : [{}] ****************\n""".\
                                        format("V" if self.is_loopback else " ")
                                        
        for symbol, value in self:
            text += "{} = {}\n".format(symbol, value)
        text +="""******************************************************\n"""
        return text

    def __eq__(self, other):
        """
        Equality test between two objects. 
        
        .. warning::
        
            Beware it uses the pointer to implement the hashing function.  
            So it is IDENTITY dependent (in C) and not value dependant.
        
        :return: True iff the two object are the same
        """
        return self._ptr == other._ptr
    
    def __hash__(self):
        """
        Makes this object hashable. 
        
        .. warning::
        
            Beware it uses the pointer to implement the hashing function.  
            So it is IDENTITY dependent (in C) and not value dependant.
        
        :return: an object that can serve as key to perform the lookup in a dict.
        """
        return self._ptr
import unittest
from tests                 import utils as tests 
from pynusmv.init          import init_nusmv, deinit_nusmv
from pynusmv.glob          import load,                \
                                  master_bool_sexp_fsm                    
from pynusmv.parser        import parse_ltl_spec,      \
                                  parse_simple_expression
from pynusmv.node          import Node 
from pynusmv.collections   import NodeList 
from pynusmv.bmc.glob      import BmcSupport, master_be_fsm
from pynusmv.bmc.utils     import generate_counter_example
from pynusmv.bmc.ltlspec   import generate_ltl_problem 
from pynusmv.sat           import SatSolverFactory, Polarity
from pynusmv.trace         import Trace, TraceType , TraceStep
                         is_volatile=True)
            
            trace.freeze()
            self.assertTrue (trace.is_frozen)
            self.assertFalse(trace.is_thawed)
            
            trace.thaw()
            self.assertFalse(trace.is_frozen)
            self.assertTrue (trace.is_thawed)
            
            # it may be called two times in a row
            trace.thaw()
            self.assertFalse(trace.is_frozen)
            self.assertTrue (trace.is_thawed)
            
    def test_append_step(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            self.assertEquals(0, len(trace))
            step = trace.append_step()
            self.assertIsNotNone(step)
            self.assertEquals(TraceStep, type(step))
            self.assertEquals(1, len(trace))
    
    def test_state_vars(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            self.assertEquals("NodeList[v, w]", str(trace.state_vars))
            
    def test_state_frozen_vars(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            self.assertEquals("NodeList[v, w, f]", str(trace.state_frozen_vars))
            
    def test_input_var(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            self.assertEquals("NodeList[i]", str(trace.input_vars))
            
    def test_language_contains(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            be_fsm   = master_be_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            v = be_fsm.encoding.by_name['v']
            w = be_fsm.encoding.by_name['w']
            f = be_fsm.encoding.by_name['f']
            i = be_fsm.encoding.by_name['i']
            
            self.assertTrue(v.name in trace)
            self.assertTrue(w.name in trace)
            self.assertTrue(f.name in trace)
            self.assertTrue(i.name in trace)
            
            x = parse_simple_expression("x")
            self.assertFalse(Node.from_ptr(x) in trace)
    
    def test_is_complete(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            be_fsm   = master_be_fsm()
            
            trace    = Trace.create("Dummy example", 
                         TraceType.COUNTER_EXAMPLE, 
                         sexp_fsm.symbol_table,
                         sexp_fsm.symbols_list,
                         is_volatile=True)
            
            # vacuously true
            self.assertTrue(trace.is_complete(NodeList.from_list([])))
            

            v = be_fsm.encoding.by_name['v'].name
            self.assertFalse(trace.is_complete(NodeList.from_list([v])))
            
            step = trace.steps[1]
            yes  = Node.from_ptr(parse_simple_expression("TRUE"))
            step+= (v, yes)
            
            self.assertTrue (trace.is_complete(NodeList.from_list([v])))             

    def test_iter(self):
        with BmcSupport():
            sexp_fsm = master_bool_sexp_fsm()
            
            trace    = Trace.create("Dummy example", 

                         TraceType.COUNTER_EXAMPLE, 