1. 24 Jan, 2010 1 commit
    • Guillaume Sadegh's avatar
      Fix copyrights. · 3a974d61
      Guillaume Sadegh authored
      * bench/Makefile.am, bench/gspn-ssp/Makefile.am,
      bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am,
      bench/split-product/Makefile.am, configure.ac,
      iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh,
      iface/nips/Makefile.am, iface/nips/common.cc,
      iface/nips/common.hh, iface/nips/dottynips.cc,
      iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am,
      src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
      src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc,
      src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am,
      src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh,
      src/evtgba/product.cc, src/evtgba/product.hh,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am,
      src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
      src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
      src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
      src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc,
      src/ltlast/atomic_p...
      3a974d61
  2. 28 May, 2009 1 commit
  3. 23 Feb, 2009 1 commit
  4. 18 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/ltl2tgba.cc: Simplify using · 3b3a1965
      Alexandre Duret-Lutz authored
      emptiness_check_instantiator.
      * src/tgba/tgba.cc, src/tgba/tgba.hh
      (tgba::number_of_acceptance_conditions): Return an unsigned.
      * bench/emptchk/algorithms, bench/emptchk/README,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust
      references to algorithms.
      * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote
      variables properly.
      3b3a1965
  5. 17 Nov, 2004 3 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh, · 32117733
      Alexandre Duret-Lutz authored
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos.
      32117733
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh, · c3e399c8
      Alexandre Duret-Lutz authored
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
      src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
      src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
      src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.
      c3e399c8
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, · 2cd298e4
      Alexandre Duret-Lutz authored
      src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
      src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
      src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
      groups in the documentation.  Presently this only covers the
      tgba/ directory, and the emptiness-check algorithms.
      * doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
      in src/evtgbaparse/.
      2cd298e4
  6. 04 Nov, 2004 1 commit
  7. 29 Oct, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      A tgba can now annotate a transition (i.e., the position of a · 754d7064
      Alexandre Duret-Lutz authored
      tgba_succ_iterator) with some string.  This comes handy to
      associate that transition to its high-level name.
      * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
      New method.
      * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
      (tgba_product::transition_annotation): Implement it.
      * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
      (tgba_tba_proxy::transition_annotation): Likewise.
      * src/tgbaalgos/replayrun.cc (print_annotation): New function.
      (replay_tgba_run): Use it.
      754d7064
  8. 20 Apr, 2004 1 commit
  9. 28 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/gspn.cc, · e341cc9a
      Alexandre Duret-Lutz authored
      iface/gspn/gspn.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.hh, src/tgba/succiter.hh,
      src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/save.cc, src/tgbatest/explicit.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbaparse/tgbaparse.yy,
      wrap/python/tests/ltl2tgba.py:
      Rewrite `accepting condition' as `acceptance condition'.
      The symbols which have been renamed are:
      tgba::all_accepting_conditions
      tgba::neg_accepting_conditions
      succ_iterator::current_accepting_conditions
      bdd_dict::register_accepting_variable
      bdd_dict::register_accepting_variables
      bdd_dict::is_registered_accepting_variable
      tgba_bdd_concrete_factory::declare_accepting_condition
      tgba_bdd_core_data::accepting_conditions
      tgba_bdd_core_data::all_accepting_conditions
      tgba_explicit::declare_accepting_condition
      tgba_explicit::complement_all_accepting_conditions
      tgba_explicit::has_accepting_condition
      tgba_explicit::get_accepting_condition
      tgba_explicit::add_accepting_condition
      tgba_explicit::all_accepting_conditions
      tgba_explicit::neg_accepting_conditions
      state_tba_proxy::acceptance_cond
      accepting_cond_splitter
      e341cc9a
  10. 21 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * COPYING: New file. · 43a91a15
      Alexandre Duret-Lutz authored
      * Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
      iface/gspn/Makefile.am, iface/gspn/common.cc,
      iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
      iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
      iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
      src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
      src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltltest/Makefile.am,
      src/ltltest/defs.in, src/ltltest/equals.cc,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
      src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
      src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
      src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
      src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.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/tgba.cc, 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/tgbabddfactory.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
      src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, src/tgbaparse/Makefile.am,
      src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/defs.in,
      src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
      wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
      wrap/python/spot.i, wrap/python/cgi/Makefile.am,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
      wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/run.in: Add Copyright license.
      43a91a15
  11. 30 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh, src/tgba/tgba.cc · 24099078
      Alexandre Duret-Lutz authored
      (tgba::project_state): New method.
      * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
      (tgba_product::project_state): New method.
      * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
      (tgba_bta_proxy::project_state): New method.
      * src/tgbaalgos/magic.cc (magic_search::print_result): Take
      a restrict argument.
      24099078
  12. 25 Jul, 2003 1 commit
  13. 17 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Now succ_iter() can fetch extra information from · 1d9c3d64
      Alexandre Duret-Lutz authored
      the root of a product to reduce its number of successors.
      * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc.
      * src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and
      global_automaton arguments.
      (tgba::support_conditions, tgba::support_variables,
      tgba::compute_support_conditions, tgba::compute_support_variables):
      New functions.
      (tgba::last_support_conditions_input_,
      tgba::last_support_conditions_output_,
      tgba::last_support_variables_input_,
      tgba::last_support_variables_output_): New attributes.
      * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
      Handle the two new arguments.
      (tgba_bdd_concrete::compute_support_conditions,
      tgba_bdd_concrete::compute_support_variables): Implement them.
      * src/tgba/tgbabddconcrete.hh: Adjust.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter):	Ignore
      the two new arguments.
      (tgba_explicit::compute_support_conditions,
      tgba_explicit::compute_support_variables): Implement them.
      * src/tgba/tgbaexplicit.hh: Adjust.
      * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
      two new arguments.
      (tgba_product::compute_support_conditions,
      tgba_product::compute_support_variables): Implement them.
      * src/tgba/tgbaproduct.hh: Adjust.
      * iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
      tgba_gspn_private_::last_state_cond_output,
      (tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
      (tgba_gspn_private_::~tgba_gspn_private_): Delete
      last_state_cond_input.
      (tgba_gspn_private_::state_conds): New function, eved out
      from tgba_gspn::succ_iter.
      (tgba_gspn::succ_iter): Use it.  Use the two new arguments.
      (tgba_gspn::compute_support_conditions,
      tgba_gspn::compute_support_variables): New functions.
      * iface/gspn/gspn.hh: Adjust.
      1d9c3d64
  14. 14 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Before this change, all automata would construct their own · cab3be97
      Alexandre Duret-Lutz authored
      dictionaries (map of BDD variables to LTL formulae).  This was
      cumbersome, because to multiply two automata we had to build a
      common dictionary (the union of the two LTL formula spaces), and
      install wrappers to translate each automaton's BDD answers into
      the common dictionary.  This translation, that had to be repeated
      when several products were nested, was time consuming and was a
      hindrance for some optimizations.
      In the new scheme, all automata involved in a product must
      share the same dictionary.  An empty dictionary should be
      constructed by the user and passed to the automaton' constructors
      as necessary.
      This huge change removes most code than it adds.
      
      * src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
      * src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files.  These
      partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
      * src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
      * src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
      src/tgba/dictunion.hh, src/tgba/dictunion.cc,
      src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
      src/tgba/tgbabddtranslatefactory.hh,
      src/tgba/tgbabddtranslatefactory.cc,
      src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
      Delete.
      * src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files.  These
      replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
      bddfactory.hh and bddfactory.cc.
      * src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
      use bdd_dict* instead of tgba_bdd_dict&.
      * src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
      Get next_to_now from the dictionary.
      * src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
      not a const tgba_bdd_dict*.
      * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
      Adjust to use the new dictionary, stored in data_.
      * src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh: Likewise.  Plus
      now_to_next_ is now also stored in the dictionary.
      * src/tgba/tgbabddconcreteproduct.cc: Likewise.  Now
      that both operand share the same product, there is not
      point in using tgba_bdd_translate_factory.
      * src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
      Store a bdd_dict (taken as constructor argument).
      (tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
      (tgba_bdd_core_data::translate): Remove.
      (tgba_bdd_core_data::next_to_now): Remove (now in dict).
      (tgba_bdd_core_data::dict): New pointer.
      * src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
      Adjust to use the new dictionary.
      * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise.  Do
      not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
      * src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
      use bdd_dict* instead of tgba_bdd_dict&.
      * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
      (ltl_to_tgba): Take a dict argument.
      * src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
      * src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
      * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
      src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
      a dictionary, and pass it to the automata' constructors.
      * src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
      option.
      * iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
      (tgba_gspn::get_dict): Adjust return type.
      * iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
      use the new dictionary instead.
      cab3be97
  15. 26 Jun, 2003 1 commit
  16. 23 Jun, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Switch from "promises" to "accepting set". Fix the definitions · 25e6cca4
      Alexandre Duret-Lutz authored
      of these accepting set so that they are really usable.  Provide
      a all_accepting_conditions() method for use in the emptyness
      check, and a neg_accepting_conditions() for products.
      Predeclare TGBA accepting conditions is the i/o.
      
      * src/tgba/bddprint.cc (want_prom): Rename as ...
      (want_prom): ... this.
      (print_handler): Adjust to display Acc[].
      (print_acc_handler, bdd_print_acc): New functions.
      * src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
      New functions.
      * src/tgba/succiter.hh (current_promise): Rename as ...
      (current_accepting_conditions): ... this.
      * src/tgba/succiterconcrete.cc (current_state):
      Rename next to now.
      (current_promise): Rename as ...
      (current_accepting_conditions): ... this, and compute
      the accepting conditions.
      * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
      src/tgba/succiterconcrete.hh,
      src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
      src/tgba/tgbabddtranslatefactory.cc,
      src/tgbaalgos/dotty.cc: Adjust to new names.
      * src/tgba/tgba.hh (all_accepting_conditions,
      neg_accepting_conditions): New functions.
      * src/tgba/tgbabddconcretefactory.cc: Adjust to new
      names, and record accepting conditions instead of promises.
      * src/tgba/tgbabddcoredata.hh (accepting_conditions,
      all_accepting_conditions, negacc_set): New variables.
      (notnow_set, notprom_set, declare_promise): Rename as ...
      (notnext_set, notacc_set, declare_accepting_condition): ... these.
      * src/tgba/tgbaexplicit.hh
      (tgba_explicit_succ_iterator::current_promise): Rename as ...
      (tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
      (tgba_explicit::add_promise): Rename as ...
      (tgba_explicit::add_accepting_condition): ... this.
      (tgba_explicit::declare_accepting_condition,
      tgba_explicit::has_accepting_condition): New variables.
      (tgba_explicit::get_promise): Rename as ...
      (tgba_explicit::get_accepting_condition): ... this.
      (tgba_explicit::all_accepting_conditions,
      tgba_explicit::neg_accepting_conditions): Implement them.
      (all_accepting_conditions, neg_accepting_conditions,
      all_accepting_conditions): New variables.
      (tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
      * src/tgba/tgbaexplicit.cc: Likewise.
      * src/tgba/tgbaproduct.hh
      (tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
      (tgba_product::all_accepting_conditions,
      tgba_product::neg_accepting_conditions): Implement them.
      * src/tgba/tgbatranslateproxy.hh:
      (tgba_translate_proxy::all_accepting_conditions,
      tgba_translate_proxy::neg_accepting_conditions): Implement them.
      * src/tgba/tgbatranslateproxy.cc: Likewise.
      * src/tgbaalgos/save.cc (save_rec): Call bdd_print
      (tgba_save_reachable): Output the `acc =' line.
      * src/tgbaparse/tgbaparse.yy: Support the for
      accepting conditions definitions using an "acc =" line
      at the start.  Later, use has_accepting_condition while
      parsing	accepting conditions to ensure they were declared.
      Disallow !cond in accepting conditions.
      * src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
      * src/tgbatest/explicit.cc (main): Declare accepting conditions.
      * src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
      and -R new options.
      * src/tgbatest/tgbaread.cc (main): Really exit on parse error.
      * src/tgbatest/explicit.test, src/tgbatest/explprod.test,
      src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
      recent changes.
      25e6cca4
  17. 28 May, 2003 1 commit
  18. 27 May, 2003 2 commits
    • 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
  19. 26 May, 2003 2 commits
    • 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