1. 04 Jun, 2003 4 commits
  2. 03 Jun, 2003 2 commits
  3. 02 Jun, 2003 1 commit
  4. 28 May, 2003 1 commit
  5. 27 May, 2003 6 commits
    • Alexandre Duret-Lutz's avatar
      whitespace · 4034f9a3
      Alexandre Duret-Lutz authored
      4034f9a3
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.cc, src/tgba/bddprint.hh, · 4146426b
      Alexandre Duret-Lutz authored
      src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
      src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
      src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
      Add Doxygen comments.
      4146426b
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, · ddf05b5d
      Alexandre Duret-Lutz authored
      src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
      Doxygen comments.
      ddf05b5d
    • Alexandre Duret-Lutz's avatar
      typo · 236a26ad
      Alexandre Duret-Lutz authored
      236a26ad
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.hh (bdd_format_set): New function. · fb5ff901
      Alexandre Duret-Lutz authored
      * src/tgba/bddprint.cc (bdd_format_set): Likewise.
      * src/tgba/state.hh: Add Doxygen comments.
      (state::compare): Take a state*, not a state&.
      (state_ptr_less_than): New functor.
      * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
      state&.
      * src/tgba/statebdd.cc (state_bdd::compare): Likewise.
      * src/tgba/succiter.hh: Add Doxygen comments.
      * src/tgba/tgba.hh: Mention promises.
      (tgba::formate_state): New pure virtual method.
      * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
      New method.
      * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
      Likewise.
      * src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
      and tgba::formate_state.
      fb5ff901
    • Alexandre Duret-Lutz's avatar
      * src/tgba/succiter.hh (tgba_succ_iterator::current_state): · 3f0e95f0
      Alexandre Duret-Lutz authored
      Return a state*, not a state_bdd.
      * src/tgba/succiterconcrete.hh
      (tgba_succ_iterator_concrete::current_state): Return a state_bdd*,
      not a state_bdd.
      * src/tgba/state.hh (state::as_bdd): New abstract method.
      * src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ...
      * src/tgba/statebdd.cc (state_bdd::as_bdd): ... here.
      * src/tgba/tgba.hh: Add Doxygen comments.
      (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd.
      * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state):
      Return a state_bdd*, not a state_bdd.
      (tgba_bdd_concrete::get_init_bdd): New method.
      (tgba_bdd_concrete::succ_uter): Take a state* as argument.
      * src/tgba/tgbabddconcrete.cc: Likewise.
      * src/tgba/tgbabddtranslatefactory.cc
      (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
      tgba_bdd_concrete::get_init_bdd.
      * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust
      to use state* instead of state_bdd.
      * src/tgba/succlist.hh: Delete.  (Leftover from a previous
      draft.)
      3f0e95f0
  6. 26 May, 2003 6 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. · d7e49255
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
      d7e49255
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbabddtranslatefactory.cc · 53f8f29a
      Alexandre Duret-Lutz authored
      (tgba_bdd_translate_factory::compute_pairs): Be quiet.
      53f8f29a
    • Alexandre Duret-Lutz's avatar
      * src/Makefile.am (SUBDIRS): Add tgbaalgos. · 0a698131
      Alexandre Duret-Lutz authored
      (libspot_la_LIBADD): Add tgba/libtgbaalgos.
      * src/tgbaalgos/Makefile.am: New file.
      * configure.ac: Output src/tgbaalgos/Makefile.
      0a698131
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files. · 16c62199
      Alexandre Duret-Lutz authored
      * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
      * src/tgba/public.hh: Include bddprint.hh.
      16c62199
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh: Rename as ... · 88514330
      Alexandre Duret-Lutz authored
      * src/tgba/public.hh: .. this.
      * src/tgba/tgba.hh: New file.
      * src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh.
      * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba.
      (tgba_bdd_concrete::init_iter): Delete.
      (tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
      not a bdd.
      * src/tgba/tgbabddconcrete.cc: Likewise.
      88514330
    • Alexandre Duret-Lutz's avatar
      Initial code for TGBA (Transition Generalized Bchi Automata). · c0393414
      Alexandre Duret-Lutz authored
      Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
      a LTL-to-TGBA translator using Couvreur's algorithm.
      
      * src/Makefile.am (SUBDIRS): Add tgba.
      (libspot_la_LIBADD): Add tgba/libtgba.la.
      * src/tgba/Makefile.am, src/tgba/bddfactory.cc,
      src/tgba/bddfactory.hh, src/tgba/dictunion.cc,
      src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
      src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
      src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
      src/tgba/succiterconcrete.hh, src/tgba/succlist.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc,
      src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh,
      src/tgba/tgbabddtranslatefactory.cc,
      src/tgba/tgbabddtranslatefactory.hh: New files.
      c0393414
  7. 23 May, 2003 2 commits
  8. 22 May, 2003 4 commits
  9. 20 May, 2003 2 commits
  10. 19 May, 2003 1 commit
  11. 16 May, 2003 5 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/dotty.cc: Rewrite to display formulae as · 38f7ae9a
      Alexandre Duret-Lutz authored
      graphs rather than trees, to show how nodes are shared.
      38f7ae9a
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/dump.hh (dump): Return the passed ostream. · e9b734f9
      Alexandre Duret-Lutz authored
      * src/ltlvisit/dump.cc (dump): Likewise.
      * src/ltlvisit/dotty.hh (dotty): Likewise.
      * src/ltlvisit/dotty.cc (dotty): Likewise.
      * src/ltlvisit/tostring.hh (to_string): Likewise.
      * src/ltlvisit/tostring.cc (to_string): Likewise.
      e9b734f9
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/dump.hh (dump): Take a formula* as argument, · 7685d3a5
      Alexandre Duret-Lutz authored
      not a formula&.  This is more homogeneous.
      * src/ltlvisit/dump.cc (dump): Likewise.
      * src/ltlvisit/dotty.hh (dotty): Likewise.
      * src/ltlvisit/dotty.cc (dotty): Likewise.
      * src/ltlvisit/tostring.hh (to_string): Likewise.
      * src/ltlvisit/tostring.cc (to_string): Likewise.
      * src/ltltest/readltl.cc, src/ltltest/equals.cc,
      src/ltltest/tostring.cc: Adjust usage.
      7685d3a5
    • Alexandre Duret-Lutz's avatar
      typo · 35f77be6
      Alexandre Duret-Lutz authored
      35f77be6
    • Alexandre Duret-Lutz's avatar
      Check trivial multop equality at build time. The makes the · 1cdfea31
      Alexandre Duret-Lutz authored
      equal visitor useless, since two equals formulae will now
      share the same address.
      
      * src/ltlast/multop.hh (add_sorted): New function.
      (paircmp): New comparison functor.
      (map): Use paircmp, we want to compare the vectors' contents,
      not their addresses.
      * src/ltlast/multop.cc (add_sorted): New function.
      (add): Use it.
      * src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare
      pointers instead of calling equal.
      * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete.
      * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove
      equals.cc and equals.hh.
      * wrap/spot.i: Do not include equals.hh.
      1cdfea31
  12. 15 May, 2003 4 commits
    • Alexandre Duret-Lutz's avatar
      Implements spot::ltl::destroy() and exercise it. · 9123e56f
      Alexandre Duret-Lutz authored
      * src/ltlast/atomic_prop.hh: Declare instance_count().
      * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
      Likewise.  Also, really inherit for ref_formula this time.
      * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
      src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
      the instance from the instance map.  Implement instance_count().
      * src/ltlast/formula.cc, src/ltlast/formula.hh,
      src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
      destructors.
      * src/ltlparse/ltlparse.yy: Recover from binary operators with
      missing right hand operand (the point is just to destroy the
      the left hand operand).
      * src/ltltest/equals.cc, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc: Destroy used formulae.  Make sure
      instance_count()s are null are the end.
      * src/ltltest/parseerr.test: Adjust expected result, now
      that the parser lnows about missing right hand operands.
      * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
      * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
      * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
      occurring twice in the rewritten expression.
      9123e56f
    • Alexandre Duret-Lutz's avatar
      Massage the AST so that identical sub-formula share the same · 5f6d8b62
      Alexandre Duret-Lutz authored
      reference-counted formula*.  One can't call constructors for AST
      items anymore, everything need to be acquired through instance()
      class methods.
      
      * src/ltlast/formula.cc, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh: New files.
      * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them.
      * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor
      and destructor protected.  Define a static function `instance()'
      to get an instance with specific argument.  Use a map called
      `instances' to store all known instances.  Inherit from
      ref_formula.
      * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect
      the constructor and destructor.  Provide the false_instance()
      and true_instance() functions instead.
      * src/formula.hh (ref, unref, ref_, unref_): New methods.
      * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect
      the constructor, destructor, as well as the add() method.
      Provides the instance(), and add() class methods instead.
      Store children_ as a pointer.
      * src/ltlenv/defaultenv.cc (require): Adjust to
      call atomic_prop::instance.
      * src/ltlparse/ltlparse.yy: Adjust to call instance() functions
      instead of constructors.
      * src/ltltest/Makefile.am (LDADD): Tweak library ordering.
      * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor,
      not const_visitor, and adjust all prototypes appropriately.
      * src/ltlvisit/clone.cc (clone_visitor): Likewise.
      Call ref() or instance() methods instead of copy constructors.
      * src/ltlvisit/equals.cc: Simplify atomic_prop and constant
      cases.
      * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc,
      src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance()
      methods instead of constructor.  Make these children of visitor, not
      const_visitor.
      * src/ltltest/readltl.c (main): Do not delete the formula.
      5f6d8b62
    • Alexandre Duret-Lutz's avatar
      * src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to · f1838ab8
      Alexandre Duret-Lutz authored
      remove a warning with newer versions of Flex.
      f1838ab8
    • Alexandre Duret-Lutz's avatar
      * src/ltlparse/ltlparse.yy (error_list, parse_environment, result): · a92327d3
      Alexandre Duret-Lutz authored
      CVS Bison now supports %parse-param for the C++ skeleton; pass these
      variables as arguments to the Parser::Parser constructor instead of
      using globals.
      (parse): Adjust Parser::Parser call.
      a92327d3
  13. 12 May, 2003 2 commits