def test_globally_no_loop(self):
     with Configure(self, __file__, "/models/flipflops.smv"):
         fsm     = self.befsm
         formula = self.nnf("G (a <-> !b)")
         
         #  bound 0
         ref_expr= ltlspec.bounded_semantics_without_loop(fsm, formula, 0)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 0, 0)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         # bound 1
         ref_expr= ltlspec.bounded_semantics_without_loop(fsm, formula, 1)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 1, 0)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         # ---- other offset ----
         #  bound 0
         offset  = 1
         ref_expr= Be.false(fsm.encoding.manager)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 0, offset)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         #  bound 1
         offset  = 1
         ref_expr= Be.false(fsm.encoding.manager)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 1, offset)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))

 def test_false(self):
     with self.assertRaises(Exception):
         Be.false(None)
     expr = Be.false(self._manager)
     self.assertFalse(expr.is_true())
     self.assertTrue(expr.is_false())
     self.assertTrue(expr.is_constant())

    def bounded_semantics(self, fsm, k, fairness=True):
        """
        Returns a boolean expression corresponding to the bounded semantics of
        the formula denoted by `self` on a path of length k. This combines both
        the semantics in case of a loopy path and the case of a non-loopy path.

        .. note::
            This function takes the same approach as NuSMV and does not enforce
            the absence of loop when using the more restrictive semantic_no_loop.

        :param fsm: the FSM representing the model. It is used to gain access
            to the encoder (-> shift variables) and to obtain the list of
            fairness constraints.
        :param k: the last time that exists in the universe of this expression
        :param fairness: a flag indicating whether or not the fairness constraints
            should be taken into account while generating the formula.
        :return: a boolean expression translating the bounded semantics of this
            formula.
        """
        enc = fsm.encoding
        noloop = self.semantic_no_loop(enc, 0, k)

        w_loop = Be.false(enc.manager)
        for l in range(k):  # [0; k-1]
            fairness_cond = fairness_constraint(fsm, k, l) if fairness else Be.true(enc.manager)

            w_loop |= loop_condition(enc, k, l) & fairness_cond & self.semantic_with_loop(enc, 0, k, l)

        return noloop | w_loop

 def test_constant_with_loop(self):
     with tests.Configure(self, __file__, "/example.smv"):
         expr = ast.Constant("TRUE")
         self.assertEqual(Be.true(self.mgr), expr.semantic_with_loop(self.enc, 0, 5, 2))
         
         expr = ast.Constant("FALSE")
         self.assertEqual(Be.false(self.mgr), expr.semantic_with_loop(self.enc, 0, 5, 2))

 def test_bounded_semantics_without_loop(self):
     # parse the ltl property
     spec = Node.from_ptr(parse_ltl_spec("G ( y <= 7 )"))
     
     # it must raise exception when the bound is not feasible
     with self.assertRaises(ValueError):
         ltlspec.bounded_semantics_without_loop(self.fsm, spec, bound=-1)
     
     # verify that the generated expression corresponds to what is announced
     no_loop = ltlspec.bounded_semantics_without_loop(self.fsm, spec, 10)
     
     # globally w/o loop is false (this is just a test)
     self.assertEqual(no_loop, Be.false(self.fsm.encoding.manager)) 
     
     # an other more complex generation
     spec = Node.from_ptr(parse_ltl_spec("F (y <= 7)"))
     no_loop = ltlspec.bounded_semantics_without_loop(self.fsm, spec, 10)
     
     #
     # The generated expression is [[f]]^{0}_{k} so (! L_{k}) is not taken 
     # care of. And actually, NuSMV does not generate that part of the 
     # formula: it only enforce the loop condition when the semantics with 
     # loop is used 
     # 
     handcrafted = Be.false(self.fsm.encoding.manager)
     y_le_seven  = Wff(parse_ltl_spec("y <= 7")).to_boolean_wff().to_be(self.fsm.encoding)
     for time_x in reversed(range(11)): # 11 because range 'eats' up the last step
         handcrafted |= self.fsm.encoding.shift_to_time(y_le_seven, time_x)
     
     #### debuging info #####
     #print("noloop  = {}".format(no_loop.to_cnf()))
     #print("hancraft= {}".format(handcrafted.to_cnf()))
     #print(self.fsm.encoding)
     self.assertEqual(no_loop, handcrafted)

    def test_add_(self):
        # using the algebraic notation
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertTrue((true + false).is_true())
        self.assertFalse((true + false).is_false())
        self.assertTrue((true + false).is_constant())

    def test_and(self):
        # using the function
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertFalse(true.and_(false).is_true())
        self.assertTrue(true.and_(false).is_false())
        self.assertTrue(true.and_(false).is_constant())

    def test__and_(self):
        # using the keyword
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertFalse((true and false).is_true())
        self.assertTrue((true and false).is_false())
        self.assertTrue((true and false).is_constant())

    def test_sub_(self):
        # and not
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertTrue((true - false).is_true())
        self.assertFalse((true - false).is_false())
        self.assertTrue((true - false).is_constant())

def bounded_semantics_at_offset(fsm, formula, bound, offset, fairness=True):
    """
    Generates the Be [[formula]]_{bound} corresponding to the bounded semantic 
    of `formula` but encodes it with an `offset` long shift in the timeline of the encoder.

    .. note:: 

        This function plays the same role as `bounded_semantics_all_loops` but allows to 
        position the time blocks at some place we like in the encoder timeline. This is mostly
        helpful if you want to devise verification methods that need to have multiple parallel
        verifications. (ie. diagnosability).

        Note however, that the two implementations are different.

    .. warning::

        So far, the only supported temporal operators are F, G, U, R, X

    :param fsm: the BeFsm for which the property will be verified. Actually, it is only used to 
        provide the encoder used to assign the variables to some time blocks. The api was kept 
        this ways to keep uniformity with its non-offsetted counterpart.
    :param formula: the property for which to generate a verification problem
        represented in a 'node' format (subclass of :see::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 logical time bound to the problem. (Leave out the offset for this param: if you
        intend to have a problem with at most 10 steps, say bound=10)
    :param offset: the time offset in the encoding block where the sem of this formula will be 
        generated.
    :param fairness: a flag indicating whether or not to take the fairness 
        constraint into account.
    :return: a Be corresponding to the semantics of `formula` for a problem with a maximum of `bound` 
        steps encoded to start at time `offset` in the `fsm` encoding timeline.
    """
    if bound< 0:
        raise ValueError("Bound must be a positive integer")
    if offset<0:
        raise ValueError("The offset must be a positive integer")
    
    enc = fsm.encoding
    straight = bounded_semantics_without_loop_at_offset(fsm, formula, 0, bound, offset)
    k_loop   = Be.false(enc.manager)
    for i in range(bound): 
        fairness_cond = utils.fairness_constraint(fsm, offset+bound, offset+i) \
                                 if fairness \
                                 else Be.true(enc.manager)
        k_loop |= ( utils.loop_condition(enc, offset+bound, offset+i) \
                  & fairness_cond \
                  & bounded_semantics_with_loop_at_offset(fsm, formula, 0, bound, i, offset))
    
    # this is just the sem of the formula
    return straight | k_loop    

    def test__mul_(self):
        # using algebraic notation
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertFalse((true * false).is_true())
        self.assertTrue((true * false).is_false())
        self.assertTrue((true * false).is_constant())

        self.assertFalse((true & false).is_true())
        self.assertTrue((true & false).is_false())
        self.assertTrue((true & false).is_constant())

    def test_imply(self):
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        # antecedent always true
        self.assertFalse(true.imply(false).is_true())
        self.assertTrue(true.imply(false).is_false())
        self.assertTrue(true.imply(false).is_constant())

        # antecedent always false
        self.assertTrue(false.imply(true).is_true())
        self.assertFalse(false.imply(true).is_false())
        self.assertTrue(false.imply(true).is_constant())

 def test_reset(self):
     """
     Verifies that resetting the cache provokes no error
     -> verifies only the absence of runtime errors since it is who RBC does 
        the heavy lifting, not the manager
     """
     mgr = BeRbcManager.with_capacity(10)
     # test it doesn't hurt to call this method even though nothing is to
     # be done.
     mgr.reset()
     # conversion to CNF populates the hashes which are being reset so 
     # using this manager to perform cnf conversion makes sense if we want
     # to test the reset works when it actually does something.
     (Be.true(mgr) and Be.false(mgr)).to_cnf(Polarity.POSITIVE)
     mgr.reset()

 def test_next_no_loop(self):
     with Configure(self, __file__, "/models/flipflops.smv"):
         fsm     = self.befsm
         formula = self.nnf("X (a <-> !b)")
         
         #  bound 0
         ref_expr= ltlspec.bounded_semantics_without_loop(fsm, formula, 0)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 0, 0)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         # bound 1
         ref_expr= ltlspec.bounded_semantics_without_loop(fsm, formula, 1)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 1, 0)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         # ---- other offset ----
         #  bound 0
         offset  = 1
         ref_expr= Be.false(fsm.encoding.manager)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 0, offset)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))
         
         #  bound 1
         offset  = 1
         ref_expr= Wff.decorate(ltlspec.car(formula)).to_be(fsm.encoding)
         ref_expr= fsm.encoding.shift_to_time(ref_expr, offset+1)
         expr    = ltlspec.bounded_semantics_without_loop_at_offset(fsm, formula, 0, 1, offset)
         self.assertEqual(canonical_cnf(expr), canonical_cnf(ref_expr))

def loop_condition(enc, k, l):
    """
    This function generates a Be expression representing the loop condition
    which is necessary to determine that k->l is a backloop.

    Formally, the returned constraint is denoted _{l}L_{k}

    Because the transition relation is encoded in Nusmv as formula (and not as
    a relation per-se), we determine the existence of a backloop between
    l < k and forall var, var(i) == var(k)

    That is to say: if it is possible to encounter two times the same state
    (same state being all variables have the same value in both states) we know
    there is a backloop on the path

    .. note::
        An other implementation of this function (w/ the same semantics) exists
        in :mod:`pynusmv.bmc.utils`. This version is merely re-implemented to
        1. show that it can be easily done
        2. stick closely to the definition given in the paper by Biere et al.
            (see other note)


    :param fsm: the fsm on which the condition will be evaluated
    :param k: the highest time
    :param l: the time where the loop is assumed to start
    :return: a Be expression representing the loop condition that verifies that
        k-l is a loop path.
    """
    cond = Be.true(enc.manager)
    for v in enc.curr_variables:  # for all untimed variable
        vl = v.at_time[l].boolean_expression
        vk = v.at_time[k].boolean_expression
        cond = cond & (vl.iff(vk))
    return cond

 def test_fairness_list(self):
     self.assertEqual(1, len(self._TESTED.fairness_list))   
     # returned items are boolean expressions
     fairness = self._TESTED.fairness_list[0]
     # manually recoding v = True
     v        = self._TESTED.encoding.by_name['v'].boolean_expression
     manual   = Be.true(self._TESTED.encoding.manager).iff(v)
     self.assertEqual(fairness, manual)

 def _semantic(time, cnt):
     """auxiliary function to stop recursing after k steps"""
     # at infinity, it is false: psi MUST happen at some time
     if cnt == k:
         return Be.false(enc.manager)
     psi = self.rhs.semantic_with_loop(enc, time, k, l)
     phi = self.lhs.semantic_with_loop(enc, time, k, l)
     return psi | (phi & _semantic(successor(time, k, l), cnt + 1))

    def semantic_no_loop(self, enc, i, k):
        """The semantics when there is no loop:: [[lhs W rhs]]_{bound}^{time}"""
        # k is not infinity when there is no loop
        if i > k:
            return Be.false(enc.manager)

        psi = self.rhs.semantic_no_loop(enc, i, k)
        phi = self.lhs.semantic_no_loop(enc, i, k)
        return psi | (phi & self.semantic_no_loop(enc, i + 1, k))

    def test_inline(self):
        true = Be.true(self._manager)
        self.assertIsNotNone(true.inline(True))
        self.assertIsNotNone(true.inline(False))

        # with a non constant expression
        v = self._fsm.encoding.by_name["v"].boolean_expression
        self.assertIsNotNone(v.inline(True))
        self.assertIsNotNone(v.inline(False))

    def test_iff(self):
        true = Be.true(self._manager)
        false = Be.false(self._manager)

        self.assertFalse(true.iff(false).is_true())
        self.assertTrue(true.iff(false).is_false())
        self.assertTrue(true.iff(false).is_constant())

        self.assertFalse(false.iff(true).is_true())
        self.assertTrue(false.iff(true).is_false())
        self.assertTrue(false.iff(true).is_constant())

        self.assertTrue(true.iff(true).is_true())
        self.assertFalse(true.iff(true).is_false())
        self.assertTrue(true.iff(true).is_constant())

        self.assertTrue(false.iff(false).is_true())
        self.assertFalse(false.iff(false).is_false())
        self.assertTrue(false.iff(false).is_constant())