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

3664 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
a5ca9dbc43 sat: rename dtgbasat as dtwasat 
* src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Rename as...
* src/twaalgos/dtwasat.cc, src/twaalgos/dtwasat.hh: ... these.
* src/bin/autfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
src/twaalgos/postproc.cc, wrap/python/spot_impl.i: Adjust.
* NEWS: Mention the renamings.
 2015-11-24 05:44:51 +01:00
Alexandre Duret-Lutz
6237bf4cd6 org: more language tooltips in HTML output 
* doc/org/spot.css: add tooltips for Python and C++.
 2015-11-20 14:50:25 +01:00
Alexandre Duret-Lutz
5aba246ff0 org: syntax-highlight the HOA outputs 
* elisp/hoa-mode.el, elisp/Makefile.am, elisp/README: New files.
* debian/copyright, configure.ac, README, Makefile.am: Adjust.
* doc/org/init.el.in: Adjust to load hoa-mode.el.
* doc/org/spot.css: Add entries for HOA mode.
* doc/org/hoa.org, doc/org/ltldo.org, doc/org/oaut.org,
doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org,
doc/org/tut30.org: Make the HOA outputs as HOA.
 2015-11-20 14:28:51 +01:00
Alexandre Duret-Lutz
d46da963d5 python: better interface for sat_minimize() 
* NEWS: Mention it.
* wrap/python/spot.py: Rewrite the sat_minimize() function.
* wrap/python/tests/satmin.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
 2015-11-17 18:37:23 +01:00
Alexandre Duret-Lutz
c1bfc5d59b doc: two typos 
* doc/mainpage.dox, doc/org/tut01.org: Here.
 2015-11-17 18:18:50 +01:00
Alexandre Duret-Lutz
b3ff5655fb dot: add support for option +N 
* src/twaalgos/dot.cc: Here.
* NEWS, src/bin/common_aoutput.cc: Document it.
* wrap/python/tests/automata.ipynb: Test it.
 2015-11-14 14:49:31 +01:00
Alexandre Duret-Lutz
f86beb3c68 workaround bad interactions between magit and whitespace-mode 
* .dir-locals.el: Use global-whitespace-mode instead of whitespace-mode.
 2015-11-14 14:15:49 +01:00
Alexandre Duret-Lutz
6b516df34a dot: display pairs of states for products 
* src/twaalgos/dot.cc: Here.
* wrap/python/tests/automata.ipynb: Test it.
* NEWS: Document this.
 2015-11-14 10:22:59 +01:00
Alexandre Duret-Lutz
e3b8ed7bb5 python: add a show_default option to setup() 
* wrap/python/spot.py: Here.
* wrap/python/tests/decompose.ipynb: Use it to simplify the code.
 2015-11-13 18:18:13 +01:00
Alexandre Duret-Lutz
d23eaec7ef make sure --dot=Bb is the same as --dot=b 
* NEWS: Mention the fixed bug.
* src/twaalgos/dot.cc: Fix.
* wrap/python/tests/decompose.ipynb: Use it.
 2015-11-13 17:50:12 +01:00
Alexandre Duret-Lutz
5a7abe8582 rename tgba_run as twa_run 
Fixes #122.

* src/twaalgos/word.cc, src/twaalgos/word.hh: Here.
* src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust.
* NEWS: Mention the renaming.
 2015-11-11 12:45:59 +01:00
Alexandre Duret-Lutz
d14f0998e0 hide trim() from the public interface 
* src/misc/escape.cc, src/misc/escape.hh (trim): Move...
* src/priv/trim.cc, src/priv/trim.hh: ... in these new files.
* src/priv/Makefile.am: Add them.
* src/parseaut/scanaut.ll, src/parsetl/scantl.ll: Adjust.
 2015-11-11 11:33:15 +01:00
Alexandre Duret-Lutz
86abd6c1c0 Use -Bsymbolic-functions and -Bsymbolic 
This avoids dynamic lookups to resolve symbols inside the library, but
disallows symbol interposition.

* m4/symbolic.m4: New file.
* buddy/m4/symbolic.m4: New link.
* configure.ac, buddy/configure.ac: Add AX_SYMBOLIC.
* buddy/src/Makefile.am, iface/ltsmin/Makefile.am, src/Makefile.am,
wrap/python/Makefile.am: Link with $(SYMBOLIC_LDFLAGS).
 2015-11-10 15:10:11 +01:00
Alexandre Duret-Lutz
0553842347 activate c11 for gnulib tests 
* configure.ac: Here.
 2015-11-10 13:36:21 +01:00
Alexandre Duret-Lutz
1396b7f710 * src/parsetl/.gitignore: Adjust to no-that-recent renamings. 2015-11-10 11:19:37 +01:00
Alexandre Duret-Lutz
622422226f * tools/.gitignore: Ignore ar-lib. 2015-11-10 11:16:59 +01:00
Alexandre Duret-Lutz
4a7733823e Update gnulib. 
* lib/Makefile.am, lib/alloca.in.h, lib/argmatch.c, lib/argmatch.h,
lib/argp-ba.c, lib/argp-eexst.c, lib/argp-fmtstream.c,
lib/argp-fmtstream.h, lib/argp-fs-xinl.c, lib/argp-help.c,
lib/argp-namefrob.h, lib/argp-parse.c, lib/argp-pin.c, lib/argp-pv.c,
lib/argp-pvh.c, lib/argp-xinl.c, lib/argp.h, lib/asnprintf.c,
lib/basename-lgpl.c, lib/c-ctype.c, lib/c-ctype.h, lib/c-strcase.h,
lib/c-strcasecmp.c, lib/c-strcaseeq.h, lib/c-strncasecmp.c,
lib/config.charset, lib/dirname-lgpl.c, lib/dirname.h, lib/dosname.h,
lib/errno.in.h, lib/error.c, lib/error.h, lib/exitfail.c,
lib/exitfail.h, lib/fcntl.in.h, lib/float+.h, lib/float.c,
lib/float.in.h, lib/getopt.c, lib/getopt.in.h, lib/getopt1.c,
lib/getopt_int.h, lib/gettext.h, lib/gettimeofday.c, lib/intprops.h,
lib/isatty.c, lib/itold.c, lib/localcharset.c, lib/localcharset.h,
lib/lstat.c, lib/malloc.c, lib/mbrtowc.c, lib/mbsinit.c, lib/memchr.c,
lib/mempcpy.c, lib/mkstemp.c, lib/mkstemps.c, lib/msvc-inval.c,
lib/msvc-inval.h, lib/msvc-nothrow.c, lib/msvc-nothrow.h, lib/pathmax.h,
lib/printf-args.c, lib/printf-args.h, lib/printf-parse.c,
lib/printf-parse.h, lib/progname.c, lib/progname.h, lib/quote.h,
lib/quotearg.c, lib/quotearg.h, lib/rawmemchr.c, lib/ref-add.sin,
lib/ref-del.sin, lib/secure_getenv.c, lib/size_max.h, lib/sleep.c,
lib/stat.c, lib/stdalign.in.h, lib/stdbool.in.h, lib/stddef.in.h,
lib/stdint.in.h, lib/stdio.in.h, lib/stdlib.in.h, lib/stpcpy.c,
lib/strcasecmp.c, lib/strchrnul.c, lib/streq.h, lib/strerror-override.c,
lib/strerror-override.h, lib/strerror.c, lib/string.in.h,
lib/strings.in.h, lib/stripslash.c, lib/strncasecmp.c, lib/strndup.c,
lib/strnlen.c, lib/strverscmp.c, lib/sys_stat.in.h, lib/sys_time.in.h,
lib/sys_types.in.h, lib/sys_wait.in.h, lib/sysexits.in.h,
lib/tempname.c, lib/tempname.h, lib/time.in.h, lib/unistd.c,
lib/unistd.in.h, lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h,
lib/vsnprintf.c, lib/wchar.in.h, lib/wctype.in.h, lib/xalloc-die.c,
lib/xalloc-oversized.h, lib/xalloc.h, lib/xmalloc.c, lib/xsize.h,
m4/00gnulib.m4, m4/absolute-header.m4, m4/alloca.m4, m4/argp.m4,
m4/codeset.m4, m4/configmake.m4, m4/dirname.m4, m4/double-slash-root.m4,
m4/errno_h.m4, m4/error.m4, m4/exponentd.m4, m4/extensions.m4,
m4/extern-inline.m4, m4/fcntl-o.m4, m4/fcntl_h.m4, m4/float_h.m4,
m4/getopt.m4, m4/gettimeofday.m4, m4/glibc21.m4, m4/gnulib-cache.m4,
m4/gnulib-common.m4, m4/gnulib-comp.m4, m4/gnulib-tool.m4,
m4/include_next.m4, m4/intmax_t.m4, m4/inttypes_h.m4, m4/isatty.m4,
m4/largefile.m4, m4/localcharset.m4, m4/locale-fr.m4, m4/locale-ja.m4,
m4/locale-zh.m4, m4/longlong.m4, m4/lstat.m4, m4/malloc.m4,
m4/math_h.m4, m4/mbrtowc.m4, m4/mbsinit.m4, m4/mbstate_t.m4,
m4/memchr.m4, m4/mempcpy.m4, m4/mkstemp.m4, m4/mkstemps.m4,
m4/mmap-anon.m4, m4/msvc-inval.m4, m4/msvc-nothrow.m4, m4/multiarch.m4,
m4/nocrash.m4, m4/off_t.m4, m4/pathmax.m4, m4/printf.m4, m4/quote.m4,
m4/quotearg.m4, m4/rawmemchr.m4, m4/secure_getenv.m4, m4/size_max.m4,
m4/sleep.m4, m4/ssize_t.m4, m4/stat.m4, m4/stdalign.m4, m4/stdbool.m4,
m4/stddef_h.m4, m4/stdint.m4, m4/stdint_h.m4, m4/stdio_h.m4,
m4/stdlib_h.m4, m4/stpcpy.m4, m4/strcase.m4, m4/strchrnul.m4,
m4/strerror.m4, m4/string_h.m4, m4/strings_h.m4, m4/strndup.m4,
m4/strnlen.m4, m4/strverscmp.m4, m4/sys_socket_h.m4, m4/sys_stat_h.m4,
m4/sys_time_h.m4, m4/sys_types_h.m4, m4/sys_wait_h.m4, m4/sysexits.m4,
m4/tempname.m4, m4/time_h.m4, m4/unistd_h.m4, m4/vasnprintf.m4,
m4/vsnprintf.m4, m4/warn-on-use.m4, m4/wchar_h.m4, m4/wchar_t.m4,
m4/wctype_h.m4, m4/wint_t.m4, m4/xalloc.m4, m4/xsize.m4,
tools/snippet/arg-nonnull.h, tools/snippet/c++defs.h,
tools/snippet/warn-on-use.h: Update.
 2015-11-10 11:14:38 +01:00
Alexandre Duret-Lutz
e206b5ef33 * wrap/python/tests/decompose.ipynb: Typos. 2015-11-09 10:01:03 +01:00
Alexandre Duret-Lutz
458fc53b71 * src/bin/man/autfilt.x: Fix description. 2015-11-09 08:25:58 +01:00
Alexandre Duret-Lutz
104a372c41 Add a notebook illustrating decompose_strength() 
* wrap/python/tests/decompose.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
* src/twaalgos/strength.cc: Fix corner cases.
* src/tests/strength.test: Adjust corner case.
* NEWS, doc/org/tut.org: Mention the notebook.
 2015-11-08 22:07:43 +01:00
Alexandre Duret-Lutz
a7db0b5435 Add a decompose_strength() function. 
* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(decompose_stregth): New function.
* src/bin/autfilt.cc: Add a --decompose-strength option.
* src/bin/man/autfilt.x: Add bibliography.
* src/tests/strength.test: Test it.
* NEWS: Mention it.
 2015-11-08 22:07:43 +01:00
Alexandre Duret-Lutz
3428fb32cd Add support for --check=strength 
* src/twaalgos/strength.cc, src/twaalgos/strength.hh (check_strength):
New function.
* src/bin/common_aoutput.cc: Add --check=strength.
* src/tests/strength.test: New file.
* src/tests/Makefile.am: Add it.
* doc/org/hoa.org, NEWS: Document it.
 2015-11-07 21:40:04 +01:00
Alexandre Duret-Lutz
f4cf0f4078 autfilt: Add --is-terminal and --is-weak. 
Fixes #47.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(is_weak_automaton): New function.
(is_terminal_automaton): Generalize slightly.
* src/bin/autfilt.cc: Add options --is-terminal and --is-weak.
* src/tests/readsave.test: Add a test.
* NEWS: Update.
 2015-11-07 16:40:26 +01:00
Alexandre Duret-Lutz
81cfa05aef rename safety.hh as strength.hh 
* src/twaalgos/safety.cc, src/twaalgos/safety.hh: Rename as ...
* src/twaalgos/strength.cc, src/twaalgos/strength.hh: ... these.
* src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
src/twaalgos/compsusp.cc, src/twaalgos/minimize.cc,
wrap/python/spot_impl.i: Adjust.
 2015-11-07 14:28:40 +01:00
Alexandre Duret-Lutz
8a8ec21de7 rename is_guarantee_automaton() as is_terminal_automaton() 
* src/twaalgos/safety.hh, src/twaalgos/safety.cc: Here.
* src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
wrap/python/ajax/spotcgi.in: Adjust.
* NEWS: Mention the change.
 2015-11-07 14:05:01 +01:00
Alexandre Duret-Lutz
0c5f87b442 add support for the "terminal" property 
* src/twa/twa.hh: Store the terminal property.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O for "terminal".
* src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/minimize.cc: Set terminal
as apropriate.
* src/twaalgos/safety.cc: Use it.
* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/tests/complement.test, src/tests/monitor.test,
wrap/python/tests/automata-io.ipynb: Adjust.
 2015-11-07 14:04:44 +01:00
Alexandre Duret-Lutz
654888718c add support for the weak property 
This fixes #119.

* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/twa/twa.hh: Support it in automata.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O support.
* src/twaalgos/minimize.cc, src/twaalgos/totgba.cc: Set weak
automata on output.
* src/tests/complement.test, src/tests/parseaut.test,
src/tests/readsave.test, src/tests/remfin.test, src/tests/sccsimpl.test,
src/tests/wdba2.test, wrap/python/tests/automata-io.ipynb: Adjust.
 2015-11-06 21:51:48 +01:00
Alexandre Duret-Lutz
eecd201273 org: more examples of accessing properties 
For the first part of #118.

* doc/org/tut21.org: Here.
 2015-11-06 16:15:34 +01:00
Alexandre Duret-Lutz
33c234da11 hoa: output "unambiguous" only for non-deterministic automata by default 
* src/twaalgos/hoa.cc: Output do not output "unambiguous" if the
automaton is deterministic.  Add option "v" to cancel this restriction,
and also output "no-univ-branch".
* src/twaalgos/hoa.hh: Document the "v" option.
* src/tests/readsave.test: Test it.
* src/tests/unambig.test: Adjust for unambiguous not being output
if the automaton is deterministic.
* src/bin/common_aoutput.cc, NEWS: Document it.
* doc/org/hoa.org: Add a summary table about how properties are handled.
* src/twa/twa.hh (prop_deterministic): Setting this should also
set the unambiguous property.
* src/twaalgos/isunamb.cc: Simplify the property check.
 2015-11-05 19:42:08 +01:00
Alexandre Duret-Lutz
30037b9905 org: update description of support for HOA properties 
* doc/org/hoa.org: Here.  Also mention --trust-hoa.
 2015-11-05 17:16:54 +01:00
Alexandre Duret-Lutz
19cd2cda6f python: add binding for is_unambiguous 
Fixes #117.

* wrap/python/spot.py, wrap/python/spot_impl.i: Add binding.
* wrap/python/tests/remfin.py: Add a small test case.
* NEWS: Mention it.
 2015-11-05 13:43:02 +01:00
Alexandre Duret-Lutz
cbb2e64e7c twa: rename the is_* getters as prop_* 
This fixes #116.

* src/twa/twa.hh: Rename those methods.
* NEWS: Document the renamings.
* doc/org/hoa.org, doc/org/tut21.org, src/parseaut/parseaut.yy,
src/tests/ikwiad.cc, src/twa/twagraph.hh,
src/twaalgos/are_isomorphic.cc, src/twaalgos/complete.cc,
src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isdet.cc,
src/twaalgos/isunamb.cc, src/twaalgos/lbtt.cc,
src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
src/twaalgos/product.cc, src/twaalgos/randomgraph.cc,
src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
src/twaalgos/totgba.cc: Adjust.
 2015-11-05 09:51:53 +01:00
Alexandre Duret-Lutz
8ea5f73c1a twa: no default argument for property setters 
This is a preliminary for the renaming suggested in #116.

* src/twa/twa.hh (prop_state_based_acc, prop_inherently_weak,
prop_deterministic, prop_unambiguous, prop_stutter_invariant,
prop_stutter_sensitive): Do not default the argument to true.
* src/parseaut/parseaut.yy, src/twaalgos/degen.cc,
src/twaalgos/dtbasat.cc, src/twaalgos/dtgbasat.cc,
src/twaalgos/minimize.cc, src/twaalgos/randomgraph.cc,
src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
src/twaalgos/simulation.cc, src/twaalgos/totgba.cc,
wrap/python/tests/remfin.py: Adjust.
 2015-11-04 18:25:49 +01:00
Alexandre Duret-Lutz
bf5749189e parseaut: do not ignore the "unambiguous" property 
Fixes #115.

* src/parseaut/parseaut.yy: Set the property on the output automaton.
* src/tests/unambig.test: Add a test case.
* NEWS: Mention the fix.
 2015-11-04 17:11:25 +01:00
Alexandre Duret-Lutz
cbaa94f911 * NEWS, configure.ac: Bump version to 1.99.5a. 2015-11-03 17:17:48 +01:00
Alexandre Duret-Lutz
f08b658f04 Release Spot 1.99.5 
* NEWS, configure.ac, doc/org/setup.org: Update version.
 2015-11-03 13:42:27 +01:00
Alexandre Duret-Lutz
a28ead2dce org: simply calls to parse_aut() 
* doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org: Simplify
the calls to parse_aut.
 2015-11-03 11:58:40 +01:00
Alexandre Duret-Lutz
7b3fdebc6e * debian/control: Build-Depends on libltdl-dev. 2015-10-29 18:05:11 +01:00
Alexandre Duret-Lutz
aaff42ee22 python: fix output of twa_run 
* src/twaalgos/emptiness.hh, src/twaalgos/emptiness.cc: Declare the
operator<< for twa_run, not for twa_run_ptr (the shared_ptr
automatically forward operator<<).
* wrap/python/spot_impl.i: Add __str__ to twa_run, not twa_run_ptr.
 2015-10-29 17:24:10 +01:00
Alexandre Duret-Lutz
f6af2a84cb twa_succ_iterator: rename accessors 
* src/twa/twa.hh, src/ta/ta.hh (current_state,
current_acceptance_conditions, current_condition): Rename as...
(dst, acc, cond): ... these.
* iface/ltsmin/ltsmin.cc, src/kripke/fairkripke.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.cc,
src/kripke/kripke.hh, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
src/ta/taproduct.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/dot.cc, src/taalgos/emptinessta.cc,
src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
src/taalgos/tgba2ta.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
src/twa/twagraph.hh, src/twa/twaproduct.cc,
src/twa/twasafracomplement.cc, src/twaalgos/bfssteps.cc,
src/twaalgos/bfssteps.hh, src/twaalgos/compsusp.cc,
src/twaalgos/copy.cc, src/twaalgos/emptiness.cc,
src/twaalgos/gtec/gtec.cc, src/twaalgos/gv04.cc,
src/twaalgos/lbtt.cc, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
src/twaalgos/ndfs_result.hxx, src/twaalgos/reachiter.cc,
src/twaalgos/se05.cc, src/twaalgos/stats.cc,
src/twaalgos/stutter.cc, src/twaalgos/tau03.cc,
src/twaalgos/tau03opt.cc, wrap/python/tests/interdep.py: Adjust.
* NEWS: Mention the renamings.
 2015-10-28 21:16:21 +01:00
Alexandre Duret-Lutz
1b5b9e4a65 * src/bin/common_post.cc: Fix description of --any. 2015-10-27 08:01:18 +01:00
Alexandre Duret-Lutz
71979840cb bin: factor handling of -B/-C/-D/... output options 
* src/bin/common_post.cc: Handle the options
for BA/TGBA/Monitor as well as Complete/SBAcc here,
and in the same group.  Rename "Translation intent"
and "Optimization level" to "Simplification goal" and
"Simplification level" so that it makes sense even
in autfilt.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc: Remove common code.
* doc/org/autfilt.org, doc/org/dstar2tgba.org,
doc/org/ltl2tgba.org: Adjust sed invocations.
 2015-10-26 20:28:06 +01:00
Alexandre Duret-Lutz
dee73ee342 parse_aut: simplify the interface 
* src/parseaut/public.hh, src/parseaut/parseaut.yy,
src/parseaut/fmterror.cc: Add a raise_errors options.  Remove the
parse_strict() method.  Store parse errors and filename in the output
parsed_aut to simplify usage.
* doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
src/bin/autfilt.cc, src/bin/common_hoaread.cc, src/bin/dstar2tgba.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltlcross3.test, src/tests/ltldo.test,
wrap/python/spot.py, wrap/python/tests/parsetgba.py: Adjust usage.
* NEWS: Mention the changes.
 2015-10-26 20:28:06 +01:00
Alexandre Duret-Lutz
3d5d160635 * lrde-upload.sh: Delete. 2015-10-25 14:19:52 +01:00
Alexandre Duret-Lutz
99c967f021 twa_run: swallow reduce_run, replay_twa_run, twa_run_to_tgba 
These now become twa_run::reduce, twa_run::replay, and
twa_run::as_twa.

* src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh,
src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh: Delete.
* src/twaalgos/Makefile.am: Adjust.
* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh: Move
the above functions here, as method of twa_run.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
wrap/python/ajax/spotcgi.in, iface/ltsmin/modelcheck.cc: Adjust.
* NEWS: List the renamings.
 2015-10-25 14:13:56 +01:00
Alexandre Duret-Lutz
63917def2d twa_run: keep a pointer to the automaton 
This simplify all laters invocations, because we do not have to pass
the automaton the run was generated on.

This fixes #113 by allowing the __str__ function to be implemented on
runs.

* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (twa_run):
Store the automaton.
(prin_twa_run): Rewrite as an overloaded <<.
* src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh (reduce_run):
Do not like the automaton as a parameter.
* src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh (replay_twa_run):
Likewise.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/complementation.cc, src/tests/ikwiad.cc,
src/tests/randtgba.cc, src/twaalgos/gtec/ce.cc, src/twaalgos/gv04.cc,
src/twaalgos/magic.cc, src/twaalgos/ndfs_result.hxx,
src/twaalgos/se05.cc, src/twaalgos/projrun.cc: Adjust.
* wrap/python/ajax/spotcgi.in: Add a __str__ function to twa_run_ptr.
* wrap/python/spot_impl.i: Adjust.
 2015-10-25 11:58:14 +01:00
Alexandre Duret-Lutz
e7cc89264a * src/tests/satmin2.test: Adjust for previous patch. 2015-10-25 09:16:33 +01:00
Alexandre Duret-Lutz
4221e68d44 rename tgba_run as twa_run 
Part of #113.

* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (tgba_run):
Rename as ...
(twa_run): ... this.
* NEWS: Mention it.
* iface/ltsmin/modelcheck.cc, src/tests/complementation.cc,
src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
src/twa/twa.hh, src/twaalgos/bfssteps.cc, src/twaalgos/bfssteps.hh,
src/twaalgos/gtec/ce.cc, src/twaalgos/gtec/ce.hh,
src/twaalgos/gv04.cc, src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
src/twaalgos/ndfs_result.hxx, src/twaalgos/projrun.cc,
src/twaalgos/projrun.hh, src/twaalgos/reducerun.cc,
src/twaalgos/reducerun.hh, src/twaalgos/replayrun.cc,
src/twaalgos/replayrun.hh, src/twaalgos/se05.cc, src/twaalgos/word.cc,
src/twaalgos/word.hh, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i: Adjust.
 2015-10-24 19:23:59 +02:00
Alexandre Duret-Lutz
4a91fccc33 stats: rename structures and attribute for concistency 
* src/taalgos/stats.cc, src/taalgos/stats.hh
(tgba_statistics::transitions, tgba_sub_statistics::sub_transitions):
Rename ...
(twa_statistics::edges, twa_sub_statistics::transitions): ... to
these.
* NEWS: Mention it.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltl2tgba.test,
src/tests/neverclaimread.test, src/tests/randtgba.cc,
src/tests/renault.test, src/tests/wdba2.test, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, wrap/python/ajax/spotcgi.in: Adjust.
 2015-10-24 19:23:59 +02:00
Alexandre Duret-Lutz
f7c4ca816b * src/tests/ltldo2.test: Honor $LTL2BA. 2015-10-24 19:23:52 +02:00