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

244 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
6b7f0399f4 Release Spot 1.99.8 
* NEWS, configure.ac, doc/org/setup.org: Update version number.
 2016-02-18 14:28:06 +01:00
Alexandre Duret-Lutz
dc93e13490 * NEWS, configure.ac: Bump version number. 2016-01-15 16:29:09 +01:00
Alexandre Duret-Lutz
f466320b4a Release Spot 1.99.7 
* NEWS, configure.ac, doc/org/setup.org: Bump version to 1.99.7.
 2016-01-15 11:30:16 +01:00
Alexandre Duret-Lutz
6e854b6d83 move the sanity tests in tests/sanity/ 
* spot/sanity/: Move ...
* tests/sanity/: ... here.
* spot/sanity/Makefile.am: Merge with...
* tests/Makefile.am: ... this.
* tests/run.in: Learn to run perl tests.
* README, configure.ac, spot/Makefile.am: Adjust.
* spot/tl/mark.hh: Add missing SPOT_API detected by
fixed private.test.

* spot/twaalgos/weight.cc, spot/twaalgos/weight.hh: Move...
* spot/priv/weight.cc, spot/priv/weight.hh: ... here, as
suggested by fixed private.test.
* spot/twaalgos/tau03opt.cc, spot/twaalgos/Makefile.am,
spot/priv/Makefile.am: Adjust.
 2016-01-05 17:20:51 +01:00
Alexandre Duret-Lutz
ddc424f5a3 move ltsmin tests to tests/ltsmin/ 
* spot/ltsmin/defs.in: Delete.
* spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve,
spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm,
spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test,
spot/ltsmin/finite2.test, spot/ltsmin/kripke.test,
spot/ltsmin/modelcheck.cc: Move...
* tests/ltsmin/: ... here.
* spot/ltsmin/README: Point to tests/ltsmin/README.
* README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore,
tests/Makefile.am, tests/core/defs.in: Adjust.
 2016-01-05 11:52:24 +01:00
Alexandre Duret-Lutz
5cb94a1a3f Merge the core and python tests in the tests/ directory 
* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
 2016-01-04 16:02:30 +01:00
Alexandre Duret-Lutz
134dfc73de move spot/bin/ and spot/tests/ up by one level 
* spot/bin/: Move...
* bin/: ... here.
* spot/tests/: Move...
* tests/: ... here.
* Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
Adjust.
 2015-12-27 20:10:59 +01:00
Alexandre Duret-Lutz
6fb4df4359 Move spot-if/ltsmin/ to spot/ltsmin/ 
* spot-if/ltsmin/: Rename as...
* spot/ltsmin/: ... this.
* spot-if/: Delete.
* Makefile.am, NEWS, README, configure.ac, debian/libspot-dev.install,
doc/Doxyfile.in, spot/Makefile.am, spot/sanity/80columns.test,
spot/sanity/style.test: Adjust.
 2015-12-25 13:45:42 +01:00
Alexandre Duret-Lutz
34c3c1cedc rename wrap/python/ to python/ 
* wrap/python/: Rename to...
* python/: ... this.
* wrap/: Delete.
* Makefile.am, README, configure.ac, debian/python3-spot.examples,
debian/rules, doc/org/.dir-locals.el.in, doc/org/init.el.in,
spot/sanity/ipynb.test: Adjust.
 2015-12-25 12:38:25 +01:00
Alexandre Duret-Lutz
b519c7d3dc rename iface/ as spot-if/ 
So that instead of having to do
  #incluce <spot/iface/ltsmin/ltsmin.hh>
for using installed the installed header, and
  #incluce <iface/ltsmin/ltsmin.hh>
for using the non-installed version, we now do
  #incluce <spot-if/ltsmin/ltsmin.hh>
in both cases.

* iface/: Rename as...
* spot-if/: ... this.
* doc/Doxyfile.in, README, configure.ac, Makefile.am,
spot/sanity/80columns.test, spot/sanity/style.test: Adjust.
* NEWS: Mention the change.
* spot-if/ltsmin/Makefile.am: Install headers in $includedir/spot-if.
* debian/libspot-dev.install: Distribute that directory as well.
 2015-12-07 22:29:18 +01:00
Alexandre Duret-Lutz
f120dd3206 rename src/ as spot/ and use include <spot/...> 
* NEWS: Mention the change.
* src/: Rename as ...
* spot/: ... this, adjust all headers to include <spot/...> instead of
"...", and adjust all Makefile.am to search headers from the top-level
directory.
* HACKING: Add conventions about #include.
* spot/sanity/style.test: Add a few more grep to catch cases
that do not follow these conventions.
* .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
debian/rules, doc/Doxyfile.in, doc/Makefile.am,
doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am,
iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
 2015-12-04 20:13:59 +01:00
Alexandre Duret-Lutz
47da953c74 * NEWS, configure.ac: Bump version number. 2015-12-04 11:13:41 +01:00
Alexandre Duret-Lutz
af96afac82 Release Spot 1.99.6 
* NEWS, configure.ac, doc/org/setup.org: Update version and date.
 2015-12-04 08:12:34 +01:00
Alexandre Duret-Lutz
afbaa54d92 rewrite explicit Kripke structures and their parser 
Fixes #4 and fixes #5.

* NEWS: Mention the change.
* src/kripkeparse/: Delete.
* README, src/Makefile.am, configure.ac: Adjust.
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: Delete.
* src/kripke/kripkegraph.hh: New file.
* src/kripke/Makefile.am: Adjust.
* src/parseaut/parseaut.yy, src/parseaut/public.hh: Add
an option to read kripke structures.
* src/tests/bad_parsing.test: Delete.
* src/tests/Makefile.am: Adjust.
* src/tests/kripke.test, src/tests/parse_print_test.cc: Rewrite.
* src/tests/ikwiad.cc, src/tests/parseaut.test,
iface/ltsmin/modelcheck.cc, wrap/python/spot_impl.i: Adjust.
 2015-11-28 02:18:39 +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
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
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
c43245e778 * NEWS, configure.ac: Bump version to 1.99.4a. 2015-10-01 10:10:11 +02:00
Alexandre Duret-Lutz
59685eada0 Spot 1.99.4 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
* doc/org/index.org: Better wording of a link.
 2015-10-01 07:39:02 +02:00
Alexandre Duret-Lutz
ae6cd92142 ltlparse: move in parsetl/, and declare in tl/parse.hh 
* src/ltlparse/public.hh: Rename as...
* src/tl/parse.hh: ... this.
* src/ltlparse/: Rename as...
* src/parsetl/: ... this.
* NEWS: Mention the change.
* README, configure.ac, doc/org/tut01.org, doc/org/tut02.org,
doc/org/tut03.org, doc/org/tut10.org, src/Makefile.am,
src/bin/common_finput.cc, src/bin/common_finput.hh, src/bin/ltl2tgta.cc,
src/kripkeparse/kripkeparse.yy, src/parseaut/parseaut.yy,
src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc,
src/tl/Makefile.am, src/twaalgos/lbtt.cc, wrap/python/spot_impl.i,
iface/ltsmin/modelcheck.cc: Adjust.
 2015-09-30 17:38:06 +02:00
Alexandre Duret-Lutz
6ded5e75c4 merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory 
The ltl prefix does not make a lot of sens anymore (since we
support psl as well).  ltlast/ and ltlenv/ were almost empty.
And ltlvisit/ did not contain any visitor anymore.

* src/ltlvisit/, src/ltlast/, src/ltlenv/: Merge into...
* src/tl/: ...this.
* NEWS: Mention the change.
* README, bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_r.hh, src/bin/common_trans.cc, src/bin/genltl.cc,
src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc,
src/bin/randltl.cc, src/kripke/kripkeexplicit.hh,
src/kripkeparse/public.hh, src/parseaut/public.hh, src/priv/accmap.hh,
src/ta/taexplicit.hh, src/ta/tgtaexplicit.hh, src/tests/equalsf.cc,
src/tests/ikwiad.cc, src/tests/length.cc, src/tests/ltlrel.cc,
src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc,
src/tests/syntimpl.cc, src/tests/taatgba.cc, src/tests/tostring.cc,
src/tests/twagraph.cc, src/twa/acc.hh, src/twa/bdddict.cc,
src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/taatgba.cc,
src/twa/taatgba.hh, src/twa/twa.hh, src/twa/twagraph.cc,
src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc,
src/twaalgos/isweakscc.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
src/twaalgos/randomgraph.hh, src/twaalgos/relabel.hh,
src/twaalgos/remprop.hh, src/twaalgos/stats.cc, src/twaalgos/stutter.cc,
src/twaalgos/translate.hh, wrap/python/spot_impl.i,
src/ltlparse/ltlparse.yy, src/ltlparse/public.hh: Adjust.
 2015-09-28 15:36:48 +02:00
Alexandre Duret-Lutz
209e89a94c parseaut: swallow the dstarparser 
Note that the parser is still not able to reader multiple dstar
automata.

* src/dstarparse/: Delete.
* configure.ac, src/Makefile.am, README: Adjust.
* src/parseaut/parseaut.yy, src/parseaut/scanaut.ll: Merge in the
dstarparser rules.
* src/bin/common_trans.cc, src/bin/common_trans.hh,
src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc,
src/tests/ikwiad.cc: Adjust usage.
* src/tests/parseaut.test: Adjust expected output.
 2015-09-08 00:59:50 +02:00
Alexandre Duret-Lutz
22974c7b7b * configure.ac, NEWS: Bump version to 1.99.3a. 2015-08-26 18:05:21 +02:00
Alexandre Duret-Lutz
5498f1335a Release Spot 1.99.3 
* NEWS, configure.ac, doc/org/setup.org: Update version.
 2015-08-26 08:14:53 +02:00
Alexandre Duret-Lutz
5b75ad5abd fix detection of ipython 
* configure.ac: Use AC_CHECK_PROGS instead of AC_CHECK_PROG.
 2015-08-08 16:44:52 +02:00
Alexandre Duret-Lutz
86e16af97c debian: Distribute the html version of the ipython notebooks 
* configure.ac: Check for ipython.
* wrap/python/tests/Makefile.am (nb-html): New rule, using ipython.
* debian/control: Depend on ipython.
* debian/rules: Run nb-html.
* debian/python3-spot.examples: Install the genrated html files.
 2015-08-07 15:09:29 +02:00
Alexandre Duret-Lutz
ed4629a2ad * NEWS, configure.ac: Bump version to 1.99.2a. 2015-07-18 09:12:35 +02:00
Alexandre Duret-Lutz
ff57e3ef4c Release Spot 1.99.2 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2015-07-18 00:37:45 +02:00
Alexandre Duret-Lutz
9ae2af209b * NEWS, configure.ac: Bump version to 1.99.1a 2015-06-23 10:01:12 +02:00
Alexandre Duret-Lutz
b8c6eb04b3 Release Spot 1.99.1 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2015-06-23 08:35:32 +02:00
Alexandre Duret-Lutz
a86391ab77 hoaparse: rename to parseaut 
Because this parser is not specific to HOA anymore.

* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
src/parseaut/public.hh, src/hoaparse/hoascan.ll,
src/tests/hoaparse.test: Rename to...
* src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
src/hoaparse/public.hh, src/parseaut/scanaut.ll,
src/tests/parseaut.test: ... these, and also adjust the name internally.
For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
automaton_stream_parser, and hoa_parse() has become parse_aut().
* NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh, src/bin/common_conv.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
src/tests/complementation.cc, src/tests/ltl2tgba.cc,
src/tests/readsave.test, wrap/python/ajax/spot.in,
wrap/python/spot.py, wrap/python/spot_impl.i,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
Adjust.
 2015-06-11 13:31:13 +02:00
Alexandre Duret-Lutz
8de524adb0 org: add a first code example 
The difficulty is not the example, but setting up org-mode to allow
Python and C++ example that use the local libraries, not those
installed system-wide.

* doc/org/.dir-locals.el: Rename as...
* doc/org/.dir-locals.el.in: ... this, so we can easily define
PYTHONPATH and other environment variables.
* doc/org/init.el.in: Enable C++, and make sure but Python
and C++ use the local libraries.
* doc/org/g++wrap.in, doc/org/tut01.org: New files.
* doc/Makefile.am, configure.ac: Adjust.
* wrap/python/spot.py (to_str): Take a parenth argument.
 2015-06-03 08:07:23 +02:00
Alexandre Duret-Lutz
eabed370bf bin: clear temporary files on termination signals 
This is particularly important for src/tests/satmin.test, where ltl2tgba
might be killed while writing a huge temporary file used for SAT-based
minimization.  Before this patch, the temporary files would remain in
src/tests/satmin.dir/, easily overflowing the 100GB limit of the docker
containers we use on the build farm.

* src/bin/common_setup.cc: Catch termination signals for all tools,
even those that do not yet clear temporary files.
* configure.ac: Check for sigaction.
 2015-06-01 17:50:02 +02:00
Etienne Renault
66bd8f34db Merge kripketest, graphtest and ltltest into tests 
* README, configure.ac, iface/ltsmin/Makefile.am,
src/tests/defs.in, src/tests/.gitignore, src/tests/Makefile.am,
src/Makefile.am: update references.
* src/kripketest/.gitignore, src/kripketest/Makefile.am,
src/kripketest/defs.in, src/graphtest/.gitignore,
src/graphtest/Makefile.am,
src/graphtest/defs.in, src/ltltest/.cvsignore,
src/ltltest/.gitignore, src/ltltest/Makefile.am,
src/ltltest/defs.in:: remove files.
* src/kripketest/bad_parsing.test, src/kripketest/kripke.test,
src/kripketest/origin, src/kripketest/parse_print_test.cc,
src/ltltest/bare.test, src/ltltest/consterm.cc,
src/ltltest/consterm.test, src/tests/defs.in,
src/ltltest/equals.test, src/ltltest/equalsf.cc,
src/ltltest/eventuniv.test, src/ltltest/exclusive-ltl.test,
src/graphtest/graph.cc, src/graphtest/graph.test,
src/ltltest/isop.test, src/ltltest/kind.cc,
src/ltltest/kind.test, src/ltltest/latex.test,
src/ltltest/lbt.test, src/ltltest/length.cc,
src/ltltest/length.test, src/ltltest/lenient.test,
src/ltltest/ltlcrossgrind.test, src/ltltest/ltlfilt.test,
src/ltltest/ltlgrind.test, src/ltltest/ltlrel.cc,
src/ltltest/ltlrel.test, src/ltltest/lunabbrev.test,
src/ltltest/nenoform.test, src/graphtest/ngraph.cc,
src/graphtest/ngraph.test, src/ltltest/parse.test,
src/ltltest/parseerr.test, src/ltltest/rand.test,
src/ltltest/readltl.cc, src/ltltest/reduc.cc,
src/ltltest/reduc.test, src/ltltest/reduc0.test,
src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
src/ltltest/remove_x.test, src/ltltest/stutter-ltl.test,
src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
src/graphtest/tgbagraph.test, src/ltltest/tostring.cc,
src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
src/ltltest/tunenoform.test, src/graphtest/twagraph.cc,
src/ltltest/unabbrevwm.test,src/ltltest/utf8.test,
src/ltltest/uwrm.test: rename as...
* src/tests/bad_parsing.test, src/tests/kripke.test,
src/tests/origin, src/tests/parse_print_test.cc,
src/tests/bare.test, src/tests/consterm.cc,
src/tests/consterm.test, src/tests/equals.test,
src/tests/equalsf.cc, src/tests/eventuniv.test,
src/tests/exclusive-ltl.test, src/tests/graph.cc,
src/tests/graph.test, src/tests/isop.test,
src/tests/kind.cc, src/tests/kind.test,
src/tests/latex.test, src/tests/lbt.test,
src/tests/length.cc, src/tests/length.test,
src/tests/lenient.test, src/tests/ltlcrossgrind.test,
src/tests/ltlfilt.test, src/tests/ltlgrind.test,
src/tests/ltlrel.cc, src/tests/ltlrel.test,
src/tests/lunabbrev.test, src/tests/nenoform.test,
src/tests/ngraph.cc, src/tests/ngraph.test,
src/tests/parse.test, src/tests/parseerr.test,
src/tests/rand.test, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/reduc.test,
src/tests/reduc0.test, src/tests/reduccmp.test,
src/tests/reducpsl.test, src/tests/remove_x.test,
src/tests/stutter-ltl.test, src/tests/syntimpl.cc,
src/tests/syntimpl.test, src/tests/tgbagraph.test,
src/tests/tostring.cc, src/tests/tostring.test,
src/tests/tunabbrev.test, src/tests/tunenoform.test,
src/tests/twagraph.cc, src/tests/unabbrevwm.test,
src/tests/utf8.test, src/tests/uwrm.test: ...these!
 2015-04-24 13:57:56 +02:00
Etienne Renault
bd57f7a991 Rename tgbatest into tests. 
* src/Makefile.am, README, configure.ac: update references.
* src/tgbatest/: rename as...
* src/tests/: ...this!
 2015-04-24 13:57:56 +02:00
Alexandre Duret-Lutz
de529df59f rename src/tgbaalgos/ as src/twaalgos/ 
Automatic mass renaming.

* src/tgbaalgos/: Rename as...
* src/twaalgos/: ... this.
* README, configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh, src/bin/common_output.hh,
src/bin/common_post.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc,
src/bin/ltlfilt.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
src/graphtest/twagraph.cc, src/kripke/kripkeprint.cc,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/exclusive.cc, src/taalgos/emptinessta.hh,
src/tgbatest/checkpsl.cc, src/tgbatest/checkta.cc,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc, src/twa/twa.cc,
src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
wrap/python/spot_impl.i: Adjust.
 2015-04-22 17:58:06 +02:00
Alexandre Duret-Lutz
703fbd0e99 rename tgba files as twa 
Automatic mass renaming.

* src/graphtest/tgbagraph.cc, src/tgba/acc.cc, src/tgba/acc.hh,
src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.hh, src/tgba/fwd.hh, src/tgba/Makefile.am,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgba.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/.cvsignore: Rename as...
* src/graphtest/twagraph.cc, src/twa/acc.cc, src/twa/acc.hh,
src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc,
src/twa/bddprint.hh, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
src/twa/fwd.hh, src/twa/Makefile.am, src/twa/taatgba.cc,
src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twagraph.cc,
src/twa/twagraph.hh, src/twa/twa.hh, src/twa/twamask.cc,
src/twa/twamask.hh, src/twa/twaproduct.cc, src/twa/twaproduct.hh,
src/twa/twaproxy.cc, src/twa/twaproxy.hh,
src/twa/twasafracomplement.cc, src/twa/twasafracomplement.hh,
src/twa/.cvsignore: ... these.
* README, bench/stutter/stutter_invariance_randomgraph.cc,
configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
src/bin/common_aoutput.cc, src/bin/common_conv.hh,
src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/public.hh, src/graphtest/Makefile.am,
src/graphtest/ngraph.cc, src/hoaparse/hoaparse.yy,
src/hoaparse/public.hh, src/kripke/fairkripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/exclusive.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/priv/accmap.hh, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/canonicalize.cc,
src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh,
src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.hh,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc,
src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh,
src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc,
src/tgbaalgos/product.hh, src/tgbaalgos/projrun.cc,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh,
src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.cc,
src/tgbaalgos/sccinfo.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh,
src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
src/tgbaalgos/weight.hh, src/tgbaalgos/word.cc, src/tgbatest/acc.cc,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/taatgba.cc,
wrap/python/spot_impl.i: Adjust.
 2015-04-22 16:57:22 +02:00
Etienne Renault
b8bc619ddf Fix mac OSX support for echo -n. 
* configure.ac: here.
 2015-03-23 10:19:55 +01:00
Alexandre Duret-Lutz
441d408b9e configure: disable Python when --disable-shared 
Fixes #68.

* configure.ac: Here.
 2015-03-21 13:22:01 +01:00
Alexandre Duret-Lutz
176a7bf199 debian: include the number of git patches in the version 
* configure.ac, debian/changelog.in: Adjust.
* debian/source/format: Distribute this.
* Makefile.am (deb): New target.
 2015-02-28 18:24:43 +01:00
Alexandre Duret-Lutz
b396f373fa debian: First attempt at creating Debian packages 
* debian/: New directory.
* Makefile.am, README: Add it.
* configure.ac: Generate debian/changelog.
 2015-02-28 00:06:00 +01:00
Alexandre Duret-Lutz
7bac775ad4 Bump version to 1.99b to celebrate support for generic acceptance 
* configure.ac: Bump version.
* NEWS: Update description of HOA support.
 2015-02-26 17:30:02 +01:00
Alexandre Duret-Lutz
2a3c126c15 Make the compiler requirement clearer. 
* configure.ac: Check for g++ 4.6 bugs, so we catch
the error at compile time, not make time.
* README: Mention the minimal g++ and clang++ versions.
 2015-02-04 15:57:58 +01:00
Alexandre Duret-Lutz
a246c3b8ba tgbaparse: remove this parser 
For issue #1 (nearly done).

* src/tgbaparse/: Delete.
* configure.ac, src/Makefile.am, README: Adjust.
* src/tgbatest/randtgba.cc: Remove useless #include.
 2015-01-31 21:22:10 +01:00
Thibaud Michaud
dd4b821d93 Adding support for promela models via SpinS. 
* configure.ac, iface/Makefile.am: Adjust.
* iface/dve2/finite.test, iface/dve2/.gitignore, iface/dve2/Makefile.am,
iface/dve2/README, iface/dve2/beem-peterson.4.dve,
iface/dve2/dve2check.test, iface/dve2/defs.in, iface/dve2/finite.dve,
iface/ltsmin/finite.test, iface/dve2/kripke.test, iface/dve2/dve2.cc,
iface/dve2/dve2.hh, iface/dve2/dve2check.cc: Move to iface/ltsmin.
* iface/ltsmin/.gitignore, iface/ltsmin/Makefile.am,
iface/ltsmin/README, iface/ltsmin/beem-peterson.4.dve,
iface/ltsmin/check.test, iface/ltsmin/defs.in, iface/ltsmin/finite.dve,
iface/ltsmin/finite.test, iface/ltsmin/kripke.test,
iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc: Factorize dve2 and spins interface in
iface/ltsmin/
* iface/ltsmin/elevator2.1.pm, iface/ltsmin/finite.pm: Test promela
models.
* README: Document iface/ltsmin/ directory.
 2014-12-07 00:09:48 +01:00
Alexandre Duret-Lutz
e1bba50047 hoa: swallow the neverclaim parser 
This way we can easily parse a stream of HOAs intermixed with
neverclaims.

* src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules
for neverclaims, adjusted from src/neverparse/neverclaimparse.yy
and src/neverparse/neverclaimparse.ll.
* src/hoaparse/public.hh, NEWS: Update documentation.
* src/neverparse/: Remove this directory.
* README, configure.ac, src/Makefile.am: Adjust accordingly.
* src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc: Use HOA
parser to read neverclaims.
* src/tgbatest/hoaparse.test, src/tgbatest/neverclaimread.test: Adjust.
 2014-12-04 12:19:17 +01:00
Alexandre Duret-Lutz
e55bcd95aa hoa: preliminary implementation of a parser 
* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
* src/Makefile.am, configure.ac, README: Adjust.
* src/tgbatest/ltl2tgba.cc: Add a -XH option.
* src/tgbatest/hoaparse.test: New file.
* src/tgbatest/Makefile.am: Adjust.
* buddy/src/bddx.h: Add a bdd_from_int() function.
 2014-11-19 19:29:29 +01:00
Thibaud Michaud
37bcb5d959 Adding tgba-based stutter-invariance checking 
* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
Add closure function.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
Add two implementations of "self-loopize" function.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
self-loopize.
* src/tgba/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
closure and sl.
* src/tgbatest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Modify stutter-invariant option to use
automaton-based checking rather than syntactic-based checking.
* src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
Remove is_stutter_insensitive function.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Check if a formula is
stutter-invariant using closure and sl.
* wrap/python/spot.i: Add closure and sl bindings.
* bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
given formulas.
* bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
from random automata.
* bench/stutter/Makefile.am: Add them.
* configure.ac: Add bench/stutter/Makefile.
* bench/Makefile.am: Add stutter subdirectory.
* README: Document bench/stutter directory.
 2014-11-14 11:11:39 +01:00