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

3082 commits

This branch
This branch
All branches
Author SHA1 Message Date
Etienne Renault
8c4a3c0125 Ensure that all tests have different names. 
* src/ltltest/Makefile.am, src/tgbatest/Makefile.am: update references.
* src/ltltest/exclusive.test, src/ltltest/stutter.test,
src/tgbatest/exclusive.test, src/tgbatest/stutter.test: rename as...
* src/ltltest/exclusive-ltl.test, src/ltltest/stutter-ltl.test,
src/tgbatest/exclusive-tgba.test,
src/tgbatest/stutter-tgba.test: ...these
 2015-04-24 13:57:55 +02:00
Alexandre Duret-Lutz
7757d44ee9 bddprint: remove some never used functions 
* src/twa/bddprint.cc, src/twa/bddprint.hh (bdd_print_acc,
bdd_print_dot, bdd_print_table): Remove.
 2015-04-24 09:11:25 +02:00
Alexandre Duret-Lutz
65c0cb48fc tmpfile: fix out-of-memory check 
another catch by cppcheck

* src/misc/tmpfile.cc: Here.
 2015-04-24 08:43:22 +02:00
Alexandre Duret-Lutz
340557a12d remove some unused variables 
as reported by cppcheck

* src/taalgos/emptinessta.cc, src/taalgos/tgba2ta.cc, src/twa/acc.cc,
src/twaalgos/minimize.cc, src/twaalgos/neverclaim.cc,
src/twaalgos/remprop.cc, src/twaalgos/sccinfo.cc: Here.
 2015-04-24 08:39:23 +02:00
Alexandre Duret-Lutz
967f9e8cf1 fix some cppcheck errors 
* src/twaalgos/hoa.cc, src/twaalgos/ltl2tgba_fm.cc: Remove some
useless declarations of iterators, as detected by cppcheck.
 2015-04-23 23:46:26 +02:00
Alexandre Duret-Lutz
c829cbbadf get rid of tgta.cc 
Fixes #76.

* src/ta/tgta.cc: Delete, and move the empty
constructor and destructor...
* src/ta/tgta.hh: ... here.
* src/ta/Makefile.am: Adjust.
 2015-04-23 23:21:56 +02:00
Alexandre Duret-Lutz
a06ae1e97e get rid of the deprecated std::auto_ptr 
Fixes #77.  g++ 5.1 warns about auto_ptr.

* src/twaalgos/ltl2tgba_fm.cc: replace auto_ptr by unique_ptr.
 2015-04-23 18:20:06 +02:00
Alexandre Duret-Lutz
e201c3c9da ltsmin: do not install the library 
For some reason, we used to install the library (causing the warning
from Lintian while building the Debian packages) and not the binary.
Let's not install any of these: the user interface is not nice enough.

* iface/ltsmin/Makefile.am: Do not install libspotltsmin.la.
 2015-04-23 17:29:36 +02:00
Alexandre Duret-Lutz
7770572c89 debian: fix two lintian errors 
* debian/control (libspot-dev): Do not depend on an exact version of
spot.
(spot-doc): depend on libjs-mathjax.
* debian/rules: Patch doc/userdoc/ to use the local version of MathJax.
 2015-04-23 17:29:27 +02:00
Alexandre Duret-Lutz
e07c70577a * NEWS: Update to mention TωA. 2015-04-22 19:27:08 +02:00
Alexandre Duret-Lutz
5e67d28c8f * HACKING: Update paragraph about LTO. 2015-04-22 19:26:45 +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
Alexandre Duret-Lutz
8839f50a0f rename Doxygen groups 
Automatic mass renaming.

* src/dstarparse/public.hh, src/hoaparse/public.hh,
src/kripke/fairkripke.hh, src/kripke/kripkeprint.hh,
src/tgba/bdddict.hh, src/tgba/tgba.hh, src/tgba/tgbamask.cc,
src/tgba/tgbamask.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/canonicalize.hh, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoa.hh,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.hh,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.hh,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.hh,
src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh:
Rename all documention group starting with tgba_ as
group starting with twa_.
 2015-04-22 16:57:22 +02:00
Alexandre Duret-Lutz
03f78ee85a Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep 
Automatic mass renaming.

* src/dstarparse/dra2ba.cc, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh:
Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep.
 2015-04-22 16:57:22 +02:00
Alexandre Duret-Lutz
5301fce3bf rename tgba_proxy into twa_proxy 
Automatic mass renaming.

* src/tgba/tgbamask.cc, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh:
Rename tgba_proxy into twa_proxy.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
2648ea170f rename tgba_graph_state and tgba_graph_trans_data as twa_... 
Automatic mass renaming.

* src/tgba/tgbagraph.hh, src/tgbaalgos/powerset.cc: Rename
tgba_graph_state and tgba_graph_trans_data as twa_graph_state and
twa_graph_trans_data.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
8520c4c330 rename tgba_ptr into twa_ptr 
Automatic mass renaming.

* iface/ltsmin/modelcheck.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/nra2nba.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh,
src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgba/fwd.hh,
src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.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/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc,
src/tgbaalgos/hoa.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
src/tgbaalgos/stutter.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/tau03opt.hh, src/tgbatest/checkta.cc,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2tgba.cc, wrap/python/spot_impl.i: Rename tgba_ptr as
twa_ptr.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
5d9778474f rename tgba_succ_iterator as twa_succ_iterator 
Automatic mass renaming.

* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeprint.cc, src/ta/ta.hh, src/ta/taproduct.hh,
src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/emptinessta.cc, src/taalgos/reachiter.hh,
src/taalgos/tgba2ta.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbamask.cc, 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/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/stats.cc, src/tgbaalgos/stutter.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Rename
tgba_succ_iterator as twa_succ_iterator.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
c856933099 rename tgba_product as twa_product 
Automatic mass renaming.

* iface/ltsmin/finite.test, src/ta/tgtaproduct.cc,
src/ta/tgtaproduct.hh, src/tgba/fwd.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, wrap/python/spot_impl.i: Rename tgba_product
as twa_product.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
e0bd0ad4c0 rename tgba_digraph as twa_graph 
Automatic mass renaming.

* src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh, src/bin/common_conv.cc,
src/bin/common_conv.hh, src/bin/common_output.hh, src/bin/dstar2tgba.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/randaut.cc,
src/dstarparse/dra2ba.cc, src/dstarparse/dstar2tgba.cc,
src/dstarparse/dstarparse.yy, src/dstarparse/nra2nba.cc,
src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh,
src/graphtest/tgbagraph.cc, src/hoaparse/hoaparse.yy,
src/hoaparse/public.hh, src/ltlvisit/contain.hh,
src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh,
src/priv/accmap.hh, src/taalgos/minimize.cc, src/tgba/fwd.hh,
src/tgba/tgba.cc, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh,
src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh,
src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc,
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/hoa.cc,
src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/product.cc, src/tgbaalgos/product.hh,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh,
src/tgbaalgos/relabel.cc, src/tgbaalgos/relabel.hh,
src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh,
src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh,
src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh,
src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh,
src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh,
src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc, wrap/python/spot_impl.i,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb,
wrap/python/tests/piperead.ipynb, wrap/python/tests/testingaut.ipynb:
Rename tgba_digraph as twa_graph.
 2015-04-22 16:57:21 +02:00
Alexandre Duret-Lutz
c2ae99e779 rename the spot::tgba class as spot::twa 
Now that we support any type of omega-accetpance, not just "Generalized
Büchi", it is time to move away from GB and replace it by "ω", written
just w in ASCII.

This just change the name of the tgba class.  This part has to be done
by hand because the word "tgba" occurs in many contexts and a mass
replacement would be wrong.

This will be followed by some automatic renaming of all the derived
types and more.

* src/bin/autfilt.cc, src/bin/randaut.cc, src/kripke/fairkripke.hh,
src/ta/tgta.cc, src/ta/tgta.hh, src/tgba/fwd.hh, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbagraph.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/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/cleanacc.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/dupexp.hh, src/tgbaalgos/hoa.cc,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stutter.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.py,
wrap/python/spot_impl.i: Rename the tgba class into twa.
 2015-04-22 16:53:52 +02:00
Alexandre Duret-Lutz
8248072057 ltlfilt: add a --define option 
* src/bin/ltlfilt.cc: Implement it.
* src/bin/common_output.cc, src/bin/common_output.hh: export the
stream_formula function.
* src/ltltest/ltlfilt.test: Test it.
* src/ltlvisit/relabel.hh: Make it possible to clear the
relabeling map.
* NEWS, doc/org/ltlfilt.org: Mention --define.
 2015-04-22 16:47:01 +02:00
Etienne Renault
65a729ab3d Add remove_fin Python binding. 
* wrap/python/spot_impl.i: here.
* wrap/python/tests/automata.ipynb: tests here.
 2015-04-21 09:09:04 +02:00
Etienne Renault
f067dd7871 Add setup method for spot. 
* wrap/python/spot.py: here.
* wrap/python/tests/automata.ipynb: tests here.
 2015-04-20 13:05:58 +02:00
Etienne Renault
d55c15baf2 Use bdd dictionnary during translation. 
* wrap/python/spot.py: here
* wrap/python/tests/automata.ipynb: tests here.
 2015-04-20 13:05:58 +02:00
Etienne Renault
0ab745be9c Ignore difference in graphviz versions. 
* wrap/python/tests/ipnbdoctest.py: here.
 2015-04-20 13:05:58 +02:00
Etienne Renault
dc7ca7d8d2 Force Clang and GCC to have the same behaviour. 
* src/ltlvisit/remove_x.cc, src/ltltest/remove_x.test: here.
 2015-04-20 13:05:58 +02:00
Alexandre Duret-Lutz
439517736f autfilt: --remove-unreachable-states, --remove-dead-states 
Add these two options as an answer to comments in
https://github.com/adl/hoaf/issues/39

* src/bin/autfilt.cc: Add those options.  Also
make --keep-state use --remove-unreachable-states
instead of the less efficient --remove-dead-states
by default.
* src/tgbatest/readsave.test: Test them.
 2015-04-19 19:41:09 +02:00
Alexandre Duret-Lutz
a83bde72b3 hoa: diagnose undefined states that appear as destination 
This was discussed in the comments of
https://github.com/adl/hoaf/issues/39

* src/hoaparse/hoaparse.yy: Rename defined_states as info_states
and keep additional information about states in this vector to
diagnose undefined states.
* src/tgbatest/hoaparse.test: Add a test case.
 2015-04-19 19:40:57 +02:00
Alexandre Duret-Lutz
9e959cdc7e stutter: new variant of Etessami's check 
* src/tgbaalgos/stutter.cc: Add a new variant of Etessami's check,
closer to his original paper in IPL.
* src/ltltest/stutter.test: Add more tests.
* bench/stutter/user.sh: Include this new variant in the benchmark.
 2015-04-17 15:18:47 +02:00
Alexandre Duret-Lutz
ecfd9b7776 dot: add option to number transitions 
* src/tgbaalgos/dotty.cc: Add option 'o'.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it.
* src/taalgos/dotty.cc: Ignore this option.
* src/tgbatest/readsave.test: Test it.
 2015-04-16 12:42:40 +02:00
Alexandre Duret-Lutz
dfd080e005 acc: add a parser for string -> acc_code 
* src/tgba/acc.cc, src/tgba/acc.hh (parse_acc_code): New function.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
 2015-04-15 00:16:17 +02:00
Alexandre Duret-Lutz
c65bf731fd acc: more helper functions 
* src/tgba/acc.hh: Make it possible to call acc_cond::mark_t({1,2,3}),
and acc_code::fin({1,2,3}).
 2015-04-14 20:27:15 +02:00
Alexandre Duret-Lutz
39b92a6dea python: fix non-determinism in the test suite. 
Some tests calling spot.automaton('non-existing|') where failing either
with a "process returned 127", or, under heavier load, with "failed to
read from...".  The latter occur if we poll() the exit status before the
children has had the tame to finish.

* wrap/python/spot.py: Make sure we wait for the child process if we
reach EOF, so that we can report the error status.
* wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
Update.
 2015-04-14 17:57:06 +02:00
Alexandre Duret-Lutz
ebdb5b7c90 python: avoid some locking errors with the history 
* wrap/python/tests/ipnbdoctest.py: Store all the history
in memory.
 2015-04-14 17:56:23 +02:00
Alexandre Duret-Lutz
98e4d99b24 more final keywords 
For #42.

* src/graph/graph.hh, src/ltlast/multop.hh, src/ltlenv/defaultenv.hh,
src/misc/tmpfile.hh, src/tgba/taatgba.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbaproduct.hh, src/tgbaalgos/gtec/gtec.hh: Declare more
classes as final.
 2015-04-13 18:28:31 +02:00
Alexandre Duret-Lutz
ab7ee2c460 python: fix error handling while reading automata 
* wrap/python/tests/run.in: Make it easier to run python with gdb.
* wrap/python/tests/automata-io.ipynb: Add test case.
* wrap/python/spot.py (spot.automata): Make sure p is defined in all
cases.
* src/hoaparse/hoascan.ll: Make sure we do not close a file that
hasn't been opened.
 2015-04-13 16:45:05 +02:00
Alexandre Duret-Lutz
a637e23d84 debian: ship the ipython notebooks as examples 
Fixes #73.

* debian/python3-spot.examples: New file.
* Makefile.am: Distribute it.
 2015-04-03 14:41:08 +02:00
Alexandre Duret-Lutz
57b0586400 totgba: fix conversion of false acceptance 
* src/tgbaalgos/totgba.cc: false must become true...
* src/tgbatest/remfin.test: adjust.
 2015-04-03 08:16:52 +02:00
Alexandre Duret-Lutz
e589e208bd new transformation from Fin-less to TGBA 
Fixes #72.

* src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add
a Generic output type, and call to_generalized_buchi() if
this type is not selected.
* src/tgbatest/remfin.test: Add some tests.
* src/bin/autfilt.cc: Add a --generic option, and set it
by default.
 2015-04-02 23:19:12 +02:00
Alexandre Duret-Lutz
16204e8e61 python: better bindings for testing automata 
* src/taalgos/dotty.cc, src/taalgos/dotty.hh: Add an interface
similar to that of tgba/dotty.hh, even if we have to ignore
most options.
* src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh: Add an option
to display the intermediate automaton with explicit stuttering
transitions, for the purpose of making demonstrations.
* src/tgba/tgbagraph.hh: Tweak the file so that SWIG can
read it.
* wrap/python/spot.py: Add wrappers for testing automata.
* wrap/python/spot_impl.i: Fix support for
atomic_prop_collect_as_bdd, and include a few more files.
* wrap/python/tests/testingaut.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
 2015-04-02 18:33:16 +02:00
Alexandre Duret-Lutz
7bb183b929 degen: add a lowinit option 
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New argument
to disable the "jump to the accepting level if the entering
state as an accepting self-loop" optimization.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Check
the degen-lowinit option and pass it on to degeneralize().
* src/bin/spot-x.cc: Document it.
* src/tgbatest/degenlskip.test: Add some tests.
* src/tgbatest/ltl2ta.test: Update value.  We output less
accepting states now.
 2015-04-01 17:33:15 +02:00
Alexandre Duret-Lutz
6e8170e386 degen: do not mark initial trivial SCCs as accepting 
Doing so is not wrong, but it's superfluous, and the extra accepting
state will cause additional work in emptiness checks based on NDFS.
Report from Jan Strejček.

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case.
 2015-04-01 15:26:05 +02:00
Alexandre Duret-Lutz
54a8ce502d python: LRU cache for the dot->svg conversion 
* wrap/python/spot.py: Here.
 2015-04-01 14:44:10 +02:00
Alexandre Duret-Lutz
31b3862f48 python 2 is no longer supported 
* m4/pypath.m4: Check for Python 3.2+.
* README, NEWS, HACKING: Reflect this change.
 2015-04-01 14:01:26 +02:00
Alexandre Duret-Lutz
a18327d488 stutter: improve closure 
if a transition with the same label already exist, reuse it

* src/tgbaalgos/stutter.cc: Here.
* src/tgbatest/stutter.test: Add a test case.
 2015-03-31 19:18:41 +02:00
Alexandre Duret-Lutz
2f42c1c9bf randaut: add option --acc-type=random 
Fixes #71.

* src/bin/randaut.cc: Implement option --acc-type.
* src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh (random_acceptance): New function.
* src/tgbatest/randaut.test, wrap/python/tests/randaut.ipynb: Test it.
 2015-03-31 13:50:56 +02:00
Alexandre Duret-Lutz
d3ee61979c python: binding and example for cleanup_acceptance 
* wrap/python/spot_impl.i: Include cleanacc.hh.
* wrap/python/tests/randaut.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
 2015-03-31 11:25:32 +02:00
Alexandre Duret-Lutz
df981a0676 rename cleanup_acceptance() as cleanup_acceptance_here() 
And add a cleanup_acceptance() version that copies.

* src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh: Rename
and add the second version.
* src/bin/autfilt.cc, src/bin/ltlcross.cc,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/remfin.cc: Use
cleanup_acceptance_here.
 2015-03-31 10:44:53 +02:00