alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
100 commits 6 branches 0 tags 36 MiB
Commit graph

100 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
ad0aa705cf * src/tgbatest/ltl2tgba.cc: Handle the -o and -r options. 2003-06-19 13:48:51 +00:00
Alexandre Duret-Lutz
fc94d6c446 * src/tgbatest/tripprod.test, src/tgbatest/explprod.test, 
src/tgbatest/readsave.test: Adjust to reflect yesterday's
bddprint.cc change.
 2003-06-19 13:00:00 +00:00
Alexandre Duret-Lutz
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.
 2003-06-18 12:02:36 +00:00
Alexandre Duret-Lutz
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.
 2003-06-17 14:54:30 +00:00
Alexandre Duret-Lutz
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.
 2003-06-16 15:46:08 +00:00
Alexandre Duret-Lutz
b1d2b351fb more files to ignore 2003-06-16 15:23:22 +00:00
Alexandre Duret-Lutz
ab09c18597 Make sure we can multiply two tgba_explicit. 
* tgba/state.hh (state::translate, state::clone, state::as_bdd):
New virtual methods.
* tgba/stataebdd.cc (state::translate, state::clone): New methods.
* tgba/stataebdd.hh (state::translate, state::clone): New methods.
* tgba/tgbabddprod.cc (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
(tgba_bdd_product_succ_iterator::first): Reset right_
if any of left_ or right_ is already done (i.e., is empty).
(tgba_bdd_product_succ_iterator::done): Return true
if right_ is NULL.
(tgba_bdd_product_succ_iterator::current_state,
tgba_bdd_product::get_init_state): Work	directory with `state's.
* tgba/tgbabddprod.hh (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
* tgba/tgbabddtranslateproxy.cc
(tgba_bdd_translate_proxy_succ_iterator::
tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator.
(tgba_bdd_translate_proxy_succ_iterator::
~tgba_bdd_translate_proxy_succ_iterator): New method.
(tgba_bdd_translate_proxy_succ_iterator::current_state,
tgba_bdd_translate_proxy::get_init_state,
tgba_bdd_translate_proxy::succ_iter): Work on `state's and
`tgba_succ_iterator's directlry.
(tgba_bdd_translate_proxy::format_state): Delegate formating
to the proxied automata.
* tgba/tgbaexplicit.cc (state_explicit::clone): New method.
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(explprod_SOURCES): New variable.
(TESTS): Add explprod.test.
(CLEANFILES): Add input1 and input2.
 2003-06-16 15:18:20 +00:00
Alexandre Duret-Lutz
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.
 2003-06-12 15:21:33 +00:00
Alexandre Duret-Lutz
fe6ca2a7a4 * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G. 
* src/tgbatest/ltl2tgba.test: Use F and G.
 2003-06-10 10:52:04 +00:00
Alexandre Duret-Lutz
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.
 2003-06-06 13:53:01 +00:00
Alexandre Duret-Lutz
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.
 2003-06-06 13:23:04 +00:00
Alexandre Duret-Lutz
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.
 2003-06-06 12:45:11 +00:00
Alexandre Duret-Lutz
578fa26cf3 * src/ltltest/equals.cc, src/ltltest/readltl.cc, 
src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.
 2003-06-06 09:22:05 +00:00
Alexandre Duret-Lutz
42e079f64d whitespace changes 2003-06-05 16:24:55 +00:00
Alexandre Duret-Lutz
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.
 2003-06-05 16:22:30 +00:00
Alexandre Duret-Lutz
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.
 2003-06-05 15:22:42 +00:00
Alexandre Duret-Lutz
cebffb11e8 * src/ltlparse/ltlparse.yy: Typo in comment. 2003-06-05 12:20:02 +00:00
Alexandre Duret-Lutz
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.
 2003-06-05 12:15:03 +00:00
Alexandre Duret-Lutz
b8bb100521 * src/ltlparse/ltlparse.yy (result): Suppress unused definition. 2003-06-04 14:33:34 +00:00
Alexandre Duret-Lutz
27c83cce24 * src/Makefile.am (SUBDIRS): Build ltltest' after .'. 2003-06-04 14:08:51 +00:00
Alexandre Duret-Lutz
e766bb4b0d . 2003-06-04 14:04:25 +00:00
Alexandre Duret-Lutz
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.
 2003-06-04 14:03:30 +00:00
Alexandre Duret-Lutz
c4c90de3f6 typo 2003-06-03 17:02:33 +00:00
Alexandre Duret-Lutz
2f19a35e97 missing changelog entry 2003-06-03 16:54:14 +00:00
Alexandre Duret-Lutz
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.
 2003-06-02 11:39:55 +00:00
Alexandre Duret-Lutz
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.
 2003-05-28 15:13:56 +00:00
Alexandre Duret-Lutz
4034f9a3d6 whitespace 2003-05-27 16:04:08 +00:00
Alexandre Duret-Lutz
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.
 2003-05-27 15:18:32 +00:00
Alexandre Duret-Lutz
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.
 2003-05-27 14:42:58 +00:00
Alexandre Duret-Lutz
236a26ad66 typo 2003-05-27 13:06:58 +00:00
Alexandre Duret-Lutz
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.
 2003-05-27 13:05:22 +00:00
Alexandre Duret-Lutz
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.)
 2003-05-27 10:40:16 +00:00
Alexandre Duret-Lutz
d7e49255d3 * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. 
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
 2003-05-26 14:20:31 +00:00
Alexandre Duret-Lutz
53f8f29a9e * src/tgba/tgbabddtranslatefactory.cc 
(tgba_bdd_translate_factory::compute_pairs): Be quiet.
 2003-05-26 14:17:04 +00:00
Alexandre Duret-Lutz
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.
 2003-05-26 13:50:54 +00:00
Alexandre Duret-Lutz
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.
 2003-05-26 13:37:14 +00:00
Alexandre Duret-Lutz
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.
 2003-05-26 12:34:15 +00:00
Alexandre Duret-Lutz
c03934140f Initial code for TGBA (Transition Generalized Bchi Automata). 
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.
 2003-05-26 11:17:40 +00:00
Alexandre Duret-Lutz
5100c197a2 more files to ignore 2003-05-23 12:02:09 +00:00
Alexandre Duret-Lutz
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>.
 2003-05-23 11:51:20 +00:00
Alexandre Duret-Lutz
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.
 2003-05-22 15:07:56 +00:00
Alexandre Duret-Lutz
10f634d91d * src/pairs.c (bdd_mergepairs): New function. 
(bdd_copypair): Revert 2003-05-20's change.  Use bdd_addref
to copy result variables.
 2003-05-22 15:07:26 +00:00
Alexandre Duret-Lutz
039412ea35 * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. 2003-05-22 12:09:20 +00:00
Alexandre Duret-Lutz
4d6660835a * src/pairs.c (bdd_copypair): Use memcpy to copy from->result, 
and correctly copy p->last from from->last.
 2003-05-22 12:07:52 +00:00
Alexandre Duret-Lutz
2f6e476cba * src/pairs.c (bdd_copypair): Use memcpy to copy from->result. 2003-05-20 10:42:19 +00:00
Alexandre Duret-Lutz
42782f3a83 * src/pairs.c (bdd_setbddpair): Fix prototype in documentation. 2003-05-20 08:22:35 +00:00
Alexandre Duret-Lutz
ed8ae1ed55 * src/bdd.h: Declare bdd_copypair(). 
* src/pairs.c (bdd_copypair, bdd_pairalloc): New functions.
(bdd_newpair): Use bdd_pairalloc.
 2003-05-19 15:58:44 +00:00
Alexandre Duret-Lutz
38f7ae9a46 * src/ltlvisit/dotty.cc: Rewrite to display formulae as 
graphs rather than trees, to show how nodes are shared.
 2003-05-16 09:35:21 +00:00
Alexandre Duret-Lutz
e9b734f936 * src/ltlvisit/dump.hh (dump): Return the passed ostream. 
* 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.
 2003-05-16 08:39:11 +00:00
Alexandre Duret-Lutz
7685d3a5b8 * src/ltlvisit/dump.hh (dump): Take a formula* as argument, 
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.
 2003-05-16 08:10:58 +00:00