1. 01 Aug, 2003 5 commits
  2. 31 Jul, 2003 6 commits
  3. 30 Jul, 2003 6 commits
  4. 29 Jul, 2003 6 commits
  5. 28 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc · 860d085b
      Alexandre Duret-Lutz authored
      (tgba_tba_proxy::state_is_accepting): New method.
      * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files.
      * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
      tgbaalgos_HEADERS): Add them.
      * src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files.
      * src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES,
      check_PROGRAMS): Add them.
  6. 25 Jul, 2003 4 commits
  7. 24 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * configure.ac: Output iface/gspn/defs. · 664e49e0
      Alexandre Duret-Lutz authored
      * iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS).
      (TESTS, check_SCRIPTS, distclean-local): New.
      * iface/gspn/dcswave.test, iface/gspn/simple.test,
      iface/gspn/defs.in: New files.
      * iface/gspn/dottygspn.cc (main): Take the list of properties
      of interest in argument.
  8. 23 Jul, 2003 2 commits
  9. 22 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a. · 94a9543f
      Alexandre Duret-Lutz authored
      * iface/gspn/Makefile.am: Adjust, build dottygspn-rg and
      dottygspn-srg instead of dottygspn.
      * iface/gspn/gspn.cc (EVENT_TRUE): Undefine.
      (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes.
      * iface/gspn/dottygspn.cc (main): Destroy the automaton before
      its dictionnary.
  10. 17 Jul, 2003 4 commits
    • Alexandre Duret-Lutz's avatar
      Rename gspnlin.m4 to gspnlib.m4 · 44993317
      Alexandre Duret-Lutz authored
    • 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_variables_output_): New attributes.
      * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
      Handle the two new arguments.
      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_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_variables): Implement them.
      * src/tgba/tgbaproduct.hh: Adjust.
      * iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
      (tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
      (tgba_gspn_private_::~tgba_gspn_private_): Delete
      (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_variables): New functions.
      * iface/gspn/gspn.hh: Adjust.
    • Alexandre Duret-Lutz's avatar
      * rsc/bdd.h (bdd_existcomp, bdd_forallcomp, · 4bf6c52b
      Alexandre Duret-Lutz authored
      bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp,
      bdd_appunicomp): Declare for C and C++.
      CACHEID_APPUNCC): New macros.
      (quatvarsetcomp): New variables.
      (varset2vartable): Take a second argument to indicate negation,
      set quatvarsetcomp.
      (INVARSET): Honor quatvarsetcomp.
      (quantify): New function, extracted from bdd_exist, bdd_forall,
      and bdd_appunicomp.
      (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify.
      (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions.
      (appquantify): New function, extracted from bdd_appex, bdd_appall,
      and bdd_appuni.
      (bdd_appex, bdd_appall, bdd_appuni): Use appquantify.
      (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions.
      * src/bddop.c (bdd_support): Return bddtrue when the support
      is empty, because variable sets are conjunctions.
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily.. · f63c67b5
      Alexandre Duret-Lutz authored
      (tgba_gspn::succ_iter): Fix usage of cube.
  11. 16 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * m4/gspnlib.m4: New file. · 4ac192ac
      Alexandre Duret-Lutz authored
      * configure.ac: Call AX_CHECK_GSPNLIB.
      * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4.
      * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS).
      (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES,
      dottygspn_LDADD): New variables.
      * iface/gspn/gspn.hh (gspn_interface): New class.
      (gspn_exeption): Take a string argument and adjust all callers.
      (operator<<): Define for gspn_exeption.
      * iface/gspn/gspn.cc (gspn_interface::gspn_interface,
      gspn_interface::~gspn_interface): New.
      * iface/gspn/gspnlib.h: Delete, it belongs to GSPN.
      * iface/gspn/dottygspn.cc: New file.
  12. 15 Jul, 2003 3 commits
    • Alexandre Duret-Lutz's avatar
      * m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE · 49fd9579
      Alexandre Duret-Lutz authored
      when using an already installed lbtt.
    • Alexandre Duret-Lutz's avatar
      more files to ignore · 9791182f
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      Homogenize passing of automata as pointers, not references. · 66b1630c
      Alexandre Duret-Lutz authored
      Disallow copy for security.
      * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
      * src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
      tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
      * src/tgba/tgbabddconcreteproduct.cc
      product): Take operand automata as pointers.
      * src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
      * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
      (tgba_product): Disallow copy.
      (tgba_product::tgba_product): Take operand automata as pointers.
      * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
      Take tgba arguments as pointer.
      * src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
      * src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
      * src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
      * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
      * src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
      * src/tgbaalgos/save.hh (save): Likewise.
      * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltl2tgba.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: Likewise.