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

void LtlFuture::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 187 of file Ltl.C.

References BitVector::assign_true(), m_formula, LtlGraphNode::m_new, LtlGraphNode::m_next, Ltl::m_num, LtlGraphNode::m_old, and m_op.

{
  switch (m_op) {
  case next:
    node.m_next.assign_true (m_formula.m_num);
    return;
  case finally:
    {
      class BitVector new_set (node.m_new);
      if (!node.m_old[m_formula.m_num])
      new_set.assign_true (m_formula.m_num);
      to_expand.push (new class LtlGraphNode (node.m_incoming,
                                    new_set,
                                    node.m_old,
                                    node.m_atomic,
                                    node.m_next));
    }
    break;
  case globally:
    if (!node.m_old[m_formula.m_num])
      node.m_new.assign_true (m_formula.m_num);
    break;
#ifndef NDEBUG
  default:
    assert (false);
#endif // NDEBUG
  }
  node.m_next.assign_true (m_num);
}


Generated by  Doxygen 1.6.0   Back to index