alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • aaeb297aed * iface/gspn/gspnlib.h: Fit 80 columns. [__cplusplus]: Wrap everything under extern "C". Alexandre Duret-Lutz 2003-07-07 12:37:45 +00:00
  • 5f55663ad3 typo Alexandre Duret-Lutz 2003-07-07 11:01:30 +00:00
  • 50b6994298 * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_acc_): New attribute. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Set current_acc_. (tgba_succ_iterator_concrete::current_accepting_conditions): Simply return it. Alexandre Duret-Lutz 2003-07-07 10:59:46 +00:00
  • 24427cccdb * configure.ac: Output iface/Makefile and iface/gspn/Makefile. * iface/Makefile.am, iface/gspn/Makefile.am: New files. * Makefile.am (SUBDIRS): Add iface. * iface/gspn/gspnlib.h: New file, from Yann and Souheib. Alexandre Duret-Lutz 2003-07-07 09:55:30 +00:00
  • f754d1112d * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data, tgba_bdd_core_data::translate): Handle all_accepting_conditions. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions. Alexandre Duret-Lutz 2003-07-07 09:34:15 +00:00
  • bca9d83c44 * src/Config-parse.yy: Remove stray `,' in %token arguments. * src/Alloc.h (__INT_TO_PTR): Redefine to work around glibc 2.3. * doc/texinfo.tex: New upstream version. Alexandre Duret-Lutz 2003-07-04 16:32:14 +00:00
  • 88b6012502 * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare accepting conditions w.r.t. to Now variables, not Next. Alexandre Duret-Lutz 2003-07-04 09:35:29 +00:00
  • 4432b2388b * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first): Simplify, do not call next_non_false_() either side is done. Alexandre Duret-Lutz 2003-07-03 14:04:25 +00:00
  • c09f646e3f * src/tgba/succiter.hh (tgba_succ_iterator::current_condition): State that this is a boolean function. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::trans_dest_, tgba_succ_iterator_concrete::trans_set_, tgba_succ_iterator_concrete::trans_set_left_, tgba_succ_iterator_concrete::neg_trans_set_): Remove. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete, tgba_succ_iterator_concrete::first): Adjust to removed members. (tgba_succ_iterator_concrete::next): Simplify, transitions are no labelled by boolean functions, not only conjunctions. Suggested by Denis Poitrenaud. Alexandre Duret-Lutz 2003-07-03 14:02:23 +00:00
  • 3281b6e9b3 spacing Alexandre Duret-Lutz 2003-07-02 14:28:24 +00:00
  • 0fe98c6d18 * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New function. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_core_data::translate. Alexandre Duret-Lutz 2003-07-02 14:28:06 +00:00
  • 2ea7cbe0f5 * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle nownext_set. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Use nownext_set to simplify. Alexandre Duret-Lutz 2003-07-02 14:19:04 +00:00
  • 2ed074750d typo Alexandre Duret-Lutz 2003-07-02 13:20:33 +00:00
  • dfe74f3134 Rewrite tgba_succ_iterator_concrete::next for the fourth time (or is it the fifth?). Alexandre Duret-Lutz 2003-07-02 13:19:19 +00:00
  • 42680e82bf * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Translate varandnext_set. Alexandre Duret-Lutz 2003-07-01 11:41:17 +00:00
  • d3a9261816 * src/tgbaparse/tgbaparse.yy (lines): Expect at last one line. Alexandre Duret-Lutz 2003-06-30 16:47:56 +00:00
  • cd8090d66c typo Alexandre Duret-Lutz 2003-06-30 15:40:02 +00:00
  • e562620885 * doc/Doxyfile.in (HAVE_DOT): Set to YES to output collaboration diagrams. * doc/mainpage.dox: Typo. Alexandre Duret-Lutz 2003-06-30 15:38:41 +00:00
  • b53d8aac71 * doc/Doxygen.in: Enable LaTeX output. * doc/Makefile.am (spotref.pdf): New rule. (EXTRA_DIST): Add spotref.pdf. Alexandre Duret-Lutz 2003-06-30 12:07:30 +00:00
  • 12f66a3b18 * src/tgba/tgbabddconcretefactory.cc: (tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New. (tgba_bdd_concrete_factory::create_state): Update now_to_next_. (tgba_bdd_concrete_factory::finish): Constraint Next variables in the relation. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::now_to_next_): New variable. Alexandre Duret-Lutz 2003-06-30 08:15:06 +00:00
  • cf136e84bd * src/tgba/tgbabddconcretefactory.cc: (tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New. (tgba_bdd_concrete_factory::create_state): Update now_to_next_. (tgba_bdd_concrete_factory::finish): Constraint Next variables in the relation. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::now_to_next_): New variable. Alexandre Duret-Lutz 2003-06-30 08:15:05 +00:00
  • 6f2f4d0247 more files to ignore Alexandre Duret-Lutz 2003-06-30 07:48:20 +00:00
  • 692f78d663 Fix errors reported by ICC. Alexandre Duret-Lutz 2003-06-28 10:10:25 +00:00
  • 59c145a8fb * Makefile.am (EXTRA_DIST): Add HACKING. Alexandre Duret-Lutz 2003-06-26 16:46:13 +00:00
  • d874332e27 * configure.ac: Bump version to 0.0c. Alexandre Duret-Lutz 2003-06-26 16:45:43 +00:00
  • d852f2c882 * configure.ac: Bump version to 0.0b. Alexandre Duret-Lutz 2003-06-26 16:25:54 +00:00
  • 3d129932a8 * INSTALL: New file. Alexandre Duret-Lutz 2003-06-26 15:23:33 +00:00
  • 7fdd78614c * src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ... * src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here. * src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust. * src/tgba/public.hh: Do not include ltl2tgba.hh. * src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc, src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc, src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions. Alexandre Duret-Lutz 2003-06-26 15:15:39 +00:00
  • f4629246f7 * src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments. * src/ltlast/formula.hh: More Doxygen comments. * src/tgba/tgba.hh: Use <tt> in Doxygen comments. Alexandre Duret-Lutz 2003-06-26 15:06:18 +00:00
  • ecda9e2641 * doc/mainpage.dox: New file. * doc/Makefile.am (EXTRA_DIST): Add mainpage.dox. * doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox Alexandre Duret-Lutz 2003-06-26 14:57:09 +00:00
  • 8e3a24ad5c * src/tgba/succiter.hh: Adjust comments about promises to refer to accepting conditions. * src/tgba/tgbabddconcretefactory.hh: Likewise. * src/tgba/tgbabddcoredata.hh: Likewise. * src/tgba/dictunion.cc: Likewise. * src/tgba/tgba.hh: Likewise. Alexandre Duret-Lutz 2003-06-26 14:44:21 +00:00
  • 0b3d2c1325 * doc/Makefile.am (doc): Typo. * src/ltlvisit/tostring.hh (to_string): Add doxygen comments. * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments. * src/tgba/tgbaexplicit.hh (tgba_explicit::transtion, state_explicit, tgba_explicit_succ_iterator): Add doxygen comments. * src/ltlvisit/postfix.hh: Typo. Alexandre Duret-Lutz 2003-06-26 14:27:14 +00:00
  • 483507f16e * doc/Makefile.am (doc): Typo. * src/ltlvisit/tostring.hh (to_string): Add doxygen comments. * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments. * src/ltlvisit/postfix.hh: Typo. Alexandre Duret-Lutz 2003-06-26 14:26:23 +00:00
  • 05f724108d * src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables. (libltlast_la_SOURCES): Move all headers to ltlast_HEADERS. * src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables. (libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS. * src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New variables. (libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS. * src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New variables. (libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS. * src/misc/Makefile.am (include_HEADERS): Rename as .. (misc_HEADERS): ... this. (miscdir): New variable. * src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables. (libtgba_la_SOURCES): Move all headers to tgba_HEADERS. * src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS): New variables. (libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS. * src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New variables. (libtgbaparse_la_SOURCES): Move all public headers to tgbaparse_HEADERS. * src/tgbaparse/public.hh: Include ltlparse/location.hh, not location.hh. Alexandre Duret-Lutz 2003-06-26 14:16:29 +00:00
  • 7824dd7ada * doc/Makefile.am (stamp): Prefix $(srcdir) explicitely. Alexandre Duret-Lutz 2003-06-26 13:41:59 +00:00
  • 98a31af495 * m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir). * src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS). Alexandre Duret-Lutz 2003-06-26 12:53:29 +00:00
  • 5d26d6f01e * doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in or configure.ac changes. Distribute the html doc. * doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with useless Bison classes. (FILE_PATTERNS): Remove *.cc files. Alexandre Duret-Lutz 2003-06-26 12:34:08 +00:00
  • 510756cdb7 Distribute BuDDy. Compile and link with the included version if explicitely requested (--with-included-buddy) or if there is now stuitable version already installed. Alexandre Duret-Lutz 2003-06-26 11:53:17 +00:00
  • 832a504d8d * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Rewrite using bdd_satoneset. This time it's for real. (I hope.) * src/tgba/succiterconcrete.hh (current_base_, current_base_left_): Delete. * tgba/tgbabddcoredata.hh (next_set): New variable. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update next_set. Alexandre Duret-Lutz 2003-06-25 19:06:02 +00:00
  • 60bd2d17c9 * src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbaproduct.hh: Fix Doxygen comments. Alexandre Duret-Lutz 2003-06-25 15:23:10 +00:00
  • 6d0546c317 * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... (succ_set_left_): ... this. (current_base_, current_base_left_): New variables. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first): Reset current_. (tgba_succ_iterator_concrete::next): Rewrite. (tgba_succ_iterator_concrete::current_state): Simplify. (tgba_succ_iterator_concrete::current_accepting_conditions): Remove atomic proposition with universal quantification. * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state): Complete the initial state. (tgba_bdd_concrete::succ_iter): Do not remove Now variable from the BDD passed to the iterator. * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update notnow_set and var_set. Alexandre Duret-Lutz 2003-06-25 15:15:30 +00:00
  • 35be07c472 spacing Alexandre Duret-Lutz 2003-06-25 09:52:52 +00:00
  • 7cf57e2463 fix message Alexandre Duret-Lutz 2003-06-25 09:50:40 +00:00
  • 3e4497dc70 spacing Alexandre Duret-Lutz 2003-06-25 09:45:57 +00:00
  • f1af8f96bf * src/tgbatest/ltl2tgba.cc: Support -v. Alexandre Duret-Lutz 2003-06-25 09:44:29 +00:00
  • cdb17c5486 * src/tgbatest/ltl2tgba.cc (syntax): Fix usage message. Alexandre Duret-Lutz 2003-06-24 19:08:47 +00:00
  • a7d31e20b7 * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort accepting conditions. Alexandre Duret-Lutz 2003-06-24 19:01:58 +00:00
  • 2558e823a0 typo Alexandre Duret-Lutz 2003-06-24 13:59:52 +00:00
  • 0ae1a32a70 * src/ltlvisit/nenoform.cc (negative_normal_form): New const variant. * src/ltlvisit/nenoform.hh (negative_normal_form): New const variant. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic): New const variant. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic): New const variant. * src/ltlvisit/tunabbrev.cc (unabbreviate_ltl): New const variant. * src/ltlvisit/tunabbrev.hh (unabbreviate_ltl): New const variant. Alexandre Duret-Lutz 2003-06-24 13:52:44 +00:00
  • a889dd7dfd typo Alexandre Duret-Lutz 2003-06-24 08:55:44 +00:00
  • 25e6cca4b4 Switch from "promises" to "accepting set". Fix the definitions 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. Alexandre Duret-Lutz 2003-06-23 17:28:26 +00:00
  • fbbfda43f2 * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort out some possible inversions in the output. Alexandre Duret-Lutz 2003-06-22 20:08:30 +00:00
  • 725dacb4e8 * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the formulae used as keys in prom_. (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. (tgba_bdd_concrete_factory::prom_): New map. * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust the Fx and aUb cases to register promises with tgba_bdd_concrete_factory::declare_promise(). (ltl2tgba): Call tgba_bdd_concrete_factory::finish(). Alexandre Duret-Lutz 2003-06-19 15:01:53 +00:00
  • 8e51474fa2 * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Revert the change from 2003-06-12, it needs more work (the automaton generated on Xa&(b U !a) was bogus, with that patch). Alexandre Duret-Lutz 2003-06-19 14:26:42 +00:00
  • ad0aa705cf * src/tgbatest/ltl2tgba.cc: Handle the -o and -r options. Alexandre Duret-Lutz 2003-06-19 13:48:51 +00:00
  • fc94d6c446 * src/tgbatest/tripprod.test, src/tgbatest/explprod.test, src/tgbatest/readsave.test: Adjust to reflect yesterday's bddprint.cc change. Alexandre Duret-Lutz 2003-06-19 13:00:00 +00:00
  • bacd5a0ac2 * src/tgba/bddprint.cc (print_handler): Quote promises when !want_prom. * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or identifiers. Discard empty strings. * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod. (mixprod_SOURCES): New variable. (TESTS): Add mixprod.test. Alexandre Duret-Lutz 2003-06-18 12:02:36 +00:00
  • fd12c02345 * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): New constructor. * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product): New constructor. * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (tripprod_SOURCES): New variable. (CLEANFILES): Add input3. (TESTS): Add tripprod.test. Alexandre Duret-Lutz 2003-06-17 14:54:30 +00:00
  • 4db70160c9 * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these. (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ... (tgba_product, tgba_product_succ_iterator): ... these, and adjust all uses. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: Rename as ... * src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: ... these. (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator): Rename as ... (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these, and adjust all uses. Alexandre Duret-Lutz 2003-06-16 15:46:08 +00:00
  • b1d2b351fb more files to ignore Alexandre Duret-Lutz 2003-06-16 15:23:22 +00:00
  • ab09c18597 Make sure we can multiply two tgba_explicit. Alexandre Duret-Lutz 2003-06-16 15:18:20 +00:00
  • 5d2e0a4224 * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make sure to compute the status of the most Now variables possible. This helps to identify equivalant states. (tgba_bdd_concrete): Call set_init_state. Alexandre Duret-Lutz 2003-06-12 15:21:33 +00:00
  • fe6ca2a7a4 * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G. * src/tgbatest/ltl2tgba.test: Use F and G. Alexandre Duret-Lutz 2003-06-10 10:52:04 +00:00
  • 0233f31ee0 * src/tgbatest/bddprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod. (bddprod_SOURCES, bddprod_CXXFLAGS): New variables. (TESTS): Add bddprod.test. * src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT. Alexandre Duret-Lutz 2003-06-06 13:53:01 +00:00
  • 4472a29227 * src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae while building new dictionary. * src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod. (ltlprod_SOURCES): New variable. (TESTS): Add ltlprod.test. Alexandre Duret-Lutz 2003-06-06 13:23:04 +00:00
  • 3991a51a17 * src/ltlvisit/clone.cc (clone): New const version. * src/ltlvisit/clone.hh (clone): Likewise. * src/ltlvisit/destroy.cc (destroy): New const version. * src/ltlvisit/destroy.hh (destroy): Likewise. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::create_state, tgba_bdd_concrete_factory::create_atomic_prop, tgba_bdd_concrete_factory::promise): Clone new formulae. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods that clone and destroy formulae. * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. (ltl2tgba_SOURCES): New variable. (TESTS): Add ltl2tgba.test. Alexandre Duret-Lutz 2003-06-06 12:45:11 +00:00
  • 578fa26cf3 * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>. Alexandre Duret-Lutz 2003-06-06 09:22:05 +00:00
  • 42e079f64d whitespace changes Alexandre Duret-Lutz 2003-06-05 16:24:55 +00:00
  • 19e47ee6e4 * src/tgba/bddprint.cc (dict): Make this variable static. (want_prom): New global static variable. (print_handle): Honor want_prom. (print_sat_handler, bdd_print_sat, bdd_format_sat): New functions. (bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom. * src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions. * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add save.cc and save.hh. * src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave. (readsave_SOURCES): New variable. (TESTS): Add readsave.test. Alexandre Duret-Lutz 2003-06-05 16:22:30 +00:00
  • 6884a7f985 * configure.ac: Output src/tgbaparse/Makefile. * src/Makefile.am (SUBDIRS): Add tgbaparse. (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise, tgba_explicit::add_neg_condition, tgba_explicit::add_neg_promise): New methods. * src/tgba/tgbaexplicit.hh: Declare them. * 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/tgbaread.cc, src/tgbatest/tgbaread.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread. (TESTS): Add tgbaread.cc. (CLEANFILES): Add input. (tgbaread_SOURCES): New variable. Alexandre Duret-Lutz 2003-06-05 15:22:42 +00:00
  • cebffb11e8 * src/ltlparse/ltlparse.yy: Typo in comment. Alexandre Duret-Lutz 2003-06-05 12:20:02 +00:00
  • 80dd0ae140 * configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs. * src/Makefile.am (SUBDIRS): Add tgbatest. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc and tgbaexplicit.hh. * src/tgbatest/Makefile.am, src/tgbatest/defs.in, src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files. Alexandre Duret-Lutz 2003-06-05 12:15:03 +00:00
  • b8bb100521 * src/ltlparse/ltlparse.yy (result): Suppress unused definition. Alexandre Duret-Lutz 2003-06-04 14:33:34 +00:00
  • 27c83cce24 * src/Makefile.am (SUBDIRS): Build ltltest' after .'. Alexandre Duret-Lutz 2003-06-04 14:08:51 +00:00
  • e766bb4b0d . Alexandre Duret-Lutz 2003-06-04 14:04:25 +00:00
  • 3fb593e542 * src/ltlparse/ltlscan.ll: Use ltlyy as %prefix. * src/ltlparse/parsedecl.hh (YY_DECL): Rename yylex to ltlyylex. * src/ltlparse/ltlparse.yy: Define yylex as ltlyylex. Alexandre Duret-Lutz 2003-06-04 14:03:30 +00:00
  • c4c90de3f6 typo Alexandre Duret-Lutz 2003-06-03 17:02:33 +00:00
  • 2f19a35e97 missing changelog entry Alexandre Duret-Lutz 2003-06-03 16:54:14 +00:00
  • 1e6dbe40d6 * src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. Alexandre Duret-Lutz 2003-06-02 11:39:55 +00:00
  • 331738d644 * src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. Alexandre Duret-Lutz 2003-05-28 15:13:56 +00:00
  • 4034f9a3d6 whitespace Alexandre Duret-Lutz 2003-05-27 16:04:08 +00:00
  • 4146426bfc * src/tgba/bddprint.cc, src/tgba/bddprint.hh, 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. Alexandre Duret-Lutz 2003-05-27 15:18:32 +00:00
  • ddf05b5d47 * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add Doxygen comments. Alexandre Duret-Lutz 2003-05-27 14:42:58 +00:00
  • 236a26ad66 typo Alexandre Duret-Lutz 2003-05-27 13:06:58 +00:00
  • fb5ff901d0 * src/tgba/bddprint.hh (bdd_format_set): New function. * 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. Alexandre Duret-Lutz 2003-05-27 13:05:22 +00:00
  • 3f0e95f061 * src/tgba/succiter.hh (tgba_succ_iterator::current_state): 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.) Alexandre Duret-Lutz 2003-05-27 10:40:16 +00:00
  • d7e49255d3 * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them. Alexandre Duret-Lutz 2003-05-26 14:20:31 +00:00
  • 53f8f29a9e * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::compute_pairs): Be quiet. Alexandre Duret-Lutz 2003-05-26 14:17:04 +00:00
  • 0a698131e6 * src/Makefile.am (SUBDIRS): Add tgbaalgos. (libspot_la_LIBADD): Add tgba/libtgbaalgos. * src/tgbaalgos/Makefile.am: New file. * configure.ac: Output src/tgbaalgos/Makefile. Alexandre Duret-Lutz 2003-05-26 13:50:54 +00:00
  • 16c6219988 * src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/public.hh: Include bddprint.hh. Alexandre Duret-Lutz 2003-05-26 13:37:14 +00:00
  • 885143309a * src/tgba/tgba.hh: Rename as ... * 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. Alexandre Duret-Lutz 2003-05-26 12:34:15 +00:00
  • c03934140f Initial code for TGBA (Transition Generalized Büchi Automata). Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, a LTL-to-TGBA translator using Couvreur's algorithm. Alexandre Duret-Lutz 2003-05-26 11:17:40 +00:00
  • 5100c197a2 more files to ignore Alexandre Duret-Lutz 2003-05-23 12:02:09 +00:00
  • 557c86b65b * m4/gccwarn.m4: Do not use -Winline, this is inappropriate with STL. * src/ltlast/atomic_prop.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc: Include <cassert>. Alexandre Duret-Lutz 2003-05-23 11:51:20 +00:00
  • dc6efb0c40 * src/pairs.c (bdd_mergepairs): New function. (bdd_copypair): Revert 2003-05-20's change. Use bdd_addref to copy result variables. * src/bdd.h (BDD_INVMERGE): New error code. (bdd_mergepairs): Declare. * src/kernel.c (errorstrings): Add string of BDDINV. Alexandre Duret-Lutz 2003-05-22 15:07:56 +00:00
  • 10f634d91d * src/pairs.c (bdd_mergepairs): New function. (bdd_copypair): Revert 2003-05-20's change. Use bdd_addref to copy result variables. Alexandre Duret-Lutz 2003-05-22 15:07:26 +00:00
  • 039412ea35 * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. Alexandre Duret-Lutz 2003-05-22 12:09:20 +00:00
  • 4d6660835a * src/pairs.c (bdd_copypair): Use memcpy to copy from->result, and correctly copy p->last from from->last. Alexandre Duret-Lutz 2003-05-22 12:07:52 +00:00
  • 2f6e476cba * src/pairs.c (bdd_copypair): Use memcpy to copy from->result. Alexandre Duret-Lutz 2003-05-20 10:42:19 +00:00
  • 42782f3a83 * src/pairs.c (bdd_setbddpair): Fix prototype in documentation. Alexandre Duret-Lutz 2003-05-20 08:22:35 +00:00