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

static void translateFormula ( const class Ltl formula  )  [static]

Translate a formula and output the automaton to standard output

Parameters:
formula the formula to be translated

The generalized Büchi automaton

acceptance set number and proposition

number of states

iterator to states

flag: does the state belong to the acceptance set?

Definition at line 131 of file lbt.C.

References LtlGraph::begin(), LtlGraph::end(), Ltl::fetch(), BitVector::findNext(), Ltl::getKind(), BitVector::nonzero(), and printGates().

{
  /** The generalized Büchi automaton */
  class LtlGraph gba (formula);
  /** acceptance set number and proposition */
  typedef std::pair<unsigned, const class Ltl*> acceptance_set_t;
  typedef std::map<const class Ltl*, acceptance_set_t> acceptance_map_t;
  acceptance_map_t acceptance_sets;

  /** number of states */
  unsigned numStates = 0;
  /** iterator to states */
  LtlGraph::const_iterator s;

  // construct the acceptance sets
  for (s = gba.begin (); s != gba.end (); s++) {
    numStates++;
    const class BitVector& temporal = s->second.m_old;
    for (unsigned i = temporal.nonzero (); i; ) {
      const class Ltl& f = Ltl::fetch (i - 1);
      switch (f.getKind ()) {
      case Ltl::Until:
      if (!static_cast<const class LtlUntil&>(f).isRelease ())
        acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t>
                          (&f, acceptance_set_t
                           (acceptance_sets.size (),
                            &static_cast<const class LtlUntil&>
                            (f).getRight ())));
      break;
      case Ltl::Future:
      if (static_cast<const class LtlFuture&>(f).getOp () ==
          LtlFuture::finally)
        acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t>
                          (&f, acceptance_set_t
                           (acceptance_sets.size (),
                            &static_cast<const class LtlFuture&>
                            (f).getFormula ())));
      break;
      default:
      break;
      }
      if (i) i = temporal.findNext (i);
    }
  }

  if (numStates) {
    printf ("%u %u", numStates + 1, acceptance_sets.size ());
    puts ("\n0 1 -1");
    printGates (gba, 0);
  }
  else
    puts ("0 0");

  for (s = gba.begin (); s != gba.end (); s++) {
    printf ("%u 0", s->first);
    const class BitVector& temporal = s->second.m_old;

    // determine and display the acceptance sets the state belongs to
    for (acceptance_map_t::iterator a = acceptance_sets.begin ();
       a != acceptance_sets.end (); a++) {
      /** flag: does the state belong to the acceptance set? */
      bool accepting = true;

      for (unsigned i = temporal.nonzero (); i; ) {
      const class Ltl* f = &Ltl::fetch (i - 1);
      if (f == a->second.second) {
        accepting = true;
        break;
      }
      else if (f == a->first)
        accepting = false;
      if (i) i = temporal.findNext (i);
      }

      if (accepting)
      printf (" %u", a->second.first);
    }

    puts (" -1");
    printGates (gba, s->first);
  }
}


Generated by  Doxygen 1.6.0   Back to index