Logo Search packages:      
Sourcecode: lbt version File versions  Download package

void LtlIff::expand ( class LtlGraphNode node,
std::stack< class LtlGraphNode * > &  to_expand 
) const [virtual]

Implements operator/operand specific details of the expansion algorithm.

Parameters:
node the node representing the formula
to_expand stack of nodes to be expanded

Implements Ltl.

Definition at line 129 of file Ltl.C.

References BitVector::assign_true(), m_iff, m_left, Ltl::m_num, m_right, and Ltl::negClone().

{
  class BitVector new_set (node.m_new);
  class Ltl& neg_left = m_left.negClone ();
  class Ltl& neg_right = m_right.negClone ();
  if (!node.m_old[m_left.m_num])
    node.m_new.assign_true (m_left.m_num);
  if (!new_set[neg_left.m_num])
    new_set.assign_true (neg_left.m_num);
  if (m_iff) {
    if (!node.m_old[m_right.m_num])
      node.m_new.assign_true (m_right.m_num);
    if (!new_set[neg_right.m_num])
      new_set.assign_true (neg_right.m_num);
  }
  else {
    if (!node.m_old[neg_right.m_num])
      node.m_new.assign_true (neg_right.m_num);
    if (!new_set[m_right.m_num])
      new_set.assign_true (m_right.m_num);
  }
  to_expand.push (new class LtlGraphNode (node.m_incoming, new_set,
                                node.m_old, node.m_atomic,
                                node.m_next));
}


Generated by  Doxygen 1.6.0   Back to index