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

2691 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
261b073ae7 * doc/org/ltlcross.org: Typos. 2014-08-31 17:01:49 +02:00
Alexandre Duret-Lutz
359e0c6fb4 remove wdbacomp.cc and wdbacomp.hh 
The weak complementation is now implemented by dtgba_complement(), with
dispatch based on the automaton property.

* src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh: Remove.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/dtgbacomp.cc: Implement the weak version.
* src/tgbaalgos/dtgbacomp.hh: Document it.
* src/tgbaalgos/minimize.cc: Use dtgba_complement() instead.
 2014-08-31 00:58:10 +02:00
Alexandre Duret-Lutz
c8b399c02a Remove futurecondcol and tgbascc. 
They are not used in Spot, and their interface is really horrible.  They
are used in SOG-ITS to implement the SLAP product from TACAS'11, so we
should support the functionality eventually, but maybe using the new
kind of properties that can be attached to automata.  In the meantime,
these classes are making refactoring harder.

* src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh: Delete.
* src/tgba/Makefile.am, src/tgbatest/ltl2tgba.cc,
src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc: Adjust.
 2014-08-31 00:57:29 +02:00
Alexandre Duret-Lutz
baf644a93a python: add an SVG printer for automata 
* wrap/python/spot.i (tgba._repr_svg_): Call dot to
output SVG using the same logic as in Vaucanson 2.
 2014-08-24 17:25:57 +02:00
Alexandre Duret-Lutz
ae35cc29f5 Better formula I/O for ipython. 
* src/ltlparse/public.hh, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll (parse_error): New class.
(parse_formula): New function that raises a parse_error
exception on error.
* src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc:
(to_sclatex_string): New method.
* wrap/python/spot.i: Catch the parser_error exception,
and use the to_sclatex_string for MathJax rendering.
* wrap/python/tests/run.in: Start ipython on demand.
 2014-08-24 14:00:59 +02:00
Alexandre Duret-Lutz
6d7c258fd7 Use shared_ptr for the emptiness check interfaces. 
At the same time, this adds a is_empty() method to the tgba class,
simplifying many places that ran emptiness checks.

* iface/dve2/dve2check.cc, src/bin/ltlcross.cc,
src/dstarparse/dra2ba.cc, src/ltlvisit/contain.cc, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/gv04.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/powerset.cc,
src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/word.cc, src/tgbaalgos/word.hh,
src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc, wrap/python/ajax/spot.in,
wrap/python/spot.i: Use shared_ptr.
 2014-08-23 18:35:43 +02:00
Alexandre Duret-Lutz
803e17bb8d apcollect: Fix prototype. 
* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: Take automaton
by reference.
 2014-08-23 18:33:10 +02:00
Alexandre Duret-Lutz
c3c02bfb44 Remove useless forward declarations of class tgba. 
* src/tgbaalgos/compsusp.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoaf.hh,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/simulation.hh: Here.
 2014-08-23 13:10:24 +02:00
Alexandre Duret-Lutz
4d82ca7055 * src/tgbaalgos/hoaf.hh: Typos in comments. 2014-08-22 17:38:55 +02:00
Alexandre Duret-Lutz
92848f73af * src/tgbaalgos/hoaf.hh: Typos in comments. 2014-08-22 17:38:18 +02:00
Alexandre Duret-Lutz
700cf88b06 Merge branch master (Spot 1.2.5) into next. 
* src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/randltl.cc,
src/ltltest/reduccmp.test, src/neverparse/neverclaimparse.yy,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlcross.test, src/tgbatest/neverclaimread.test,
wrap/python/ajax/ltl2tgba.html: Fix conflicts.
 2014-08-22 16:45:41 +02:00
Alexandre Duret-Lutz
3152c1a6cb * NEWS, configure.ac: Bump version to 1.2.5a. 2014-08-22 00:11:00 +02:00
Alexandre Duret-Lutz
290106b0a4 Release Spot 1.2.5. 
* configure.ac, doc/org/tools.org, NEWS: Bump version to 1.2.5.
 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
a72b84b0b4 * src/tgbatest/ltlcross.test: More formulas from Joachim. 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
408dc878e5 ltl2tgba_fm: fix translation of !{f} as done last year for {f} 
* src/tgbaalgos/ltl2tgba_fm.cc: Fix.
* src/tgbatest/randpsl.test: Rewrite using ltlcross and add a testcase.
* NEWS: Mention it.
 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
d3ddd724c9 * doc/org/satmin.org: Tweak so org-mode does not botch the output. 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
bab579cf9d ltl2tgba.html: Separate the ltl3ba tabs from the others. 
Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: Name the tab.
* wrap/python/ajax/css/ltl2tgba.css: Give it some space.
 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
85beeec2e4 ltl2tgba.html: Add option to output LBT format. 
Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: New option.
* wrap/python/ajax/protocol.txt, NEWS: Document it.
* wrap/python/ajax/spot.in: Implement it.
* wrap/python/spot.i: Export src/ltlvisit/lbt.hh.
 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
d9d9837e55 * wrap/python/ajax/ltl2tgba.html: Update tooltips. 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
829012fe43 ltlcross: implement a --save-bogus=FILENAME option 
Suggested by Joachim Klein.

* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/ltlcross3.test: Test it.
* doc/org/ltlcross.org, NEWS: Document it.
 2014-08-21 23:16:39 +02:00
Alexandre Duret-Lutz
2227ad60cf randltl: do not reset the seed between formulas 
Reported by Joachim Klein.

* src/bin/randltl.cc: Here.
* NEWS: Mention the fix.
 2014-08-21 13:23:36 +02:00
Alexandre Duret-Lutz
44fc323e7b randltl: accept a number of atomic propositions 
Suggested by Joachim Klein.

* src/bin/randltl.cc: Implement it.
* src/ltltest/rand.test: Test it.
* doc/org/randltl.org, NEWS: Document it.
 2014-08-21 13:17:18 +02:00
Alexandre Duret-Lutz
310a98c15a hoaf: first implementation of the HOA Format output. 
The specifications are at http://adl.github.io/hoaf/

* src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/tgbatest/ltl2tgba.cc: Add option to output HOA.
* NEWS: Mention it.
 2014-08-20 23:10:01 +02:00
Alexandre Duret-Lutz
e997676c3e Support LBT formula in ltl2tgba.html. 
Suggested by Joachim Klein.

* wrap/python/ajax/spot.in: Try parse_lbt() when parse() fails.
* NEWS: Mention it.
 2014-08-20 23:10:01 +02:00
Alexandre Duret-Lutz
e78548ebae ltlcross: display formulas in blue instead of white 
So that people using white-background terminal can still read them...
Reported by Joachim Klein.

* src/bin/ltlcross.cc: Adjust.
* NEWS: Mention it.
 2014-08-20 23:10:01 +02:00
Alexandre Duret-Lutz
795c2f1720 ltl2tgba_fm: Fix incorrect simplification of promises for M 
The bug was reported by Joachim Klein.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Reduce P(a M b) to P(a & b), not to P(a).
* src/tgbatest/ltlcross.test: Test Joachim's formula.
* src/tgbatest/ltl2ta.test: Adjust some expected values.
* NEWS: Mention the bug.
 2014-08-20 23:10:01 +02:00
Alexandre Duret-Lutz
edb220af6a dtbasat,dtgbasat: rewrite using the tgba_digraph interface 
This gets rid of many state*/int conversions.  We now use scc_info
instead of scc_map.  Finally the loops are now all 0-based.

* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh (weak_sccs): New
method.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh: Use the
tgba_digraph interface.
* src/tgbatest/ltl2tgba.cc: Adjust calls.
 2014-08-20 16:18:35 +02:00
Alexandre Duret-Lutz
99d28c3cc2 * src/tgbaalgos/complete.cc: Introduce a sink state only if needed. 2014-08-20 16:11:00 +02:00
Alexandre Duret-Lutz
d28e7f9c5c graph: Add a is_dead_transition method. 
* src/graph/graph.hh, src/tgba/tgbagraph.hh (is_dead_transition): New
method.
 2014-08-20 16:10:41 +02:00
Alexandre Duret-Lutz
73e74c0ad3 * src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Cleanup. 2014-08-20 10:33:10 +02:00
Alexandre Duret-Lutz
5c9a5403fe use scc_info instead of scc_map in a couple of easy places 
* src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/simulation.cc: Use scc_info instead of scc_map.
* src/tgbaalgos/stats.hh, src/bin/common_output.hh: Change parameters
types to be tgba_digraph_ptr instead tgba_ptr, so that scc_info can be
used.
 2014-08-20 10:27:43 +02:00
Alexandre Duret-Lutz
14570f62d0 bivect: workaround flexible arrays not being standard C++ 
This is a -pedantic warning from gcc.

* src/misc/bitvect.cc, src/misc/bitvect.hh (storage_): Remove.
(storage): New method to access past the end of the struct.
 2014-08-19 22:50:08 +02:00
Alexandre Duret-Lutz
52ce449bbc tgba: merge succiter.hh, state.hh, and tgba.hh 
It makes it easier to browse tgba/.

* src/tgba/state.hh, src/tgba/succiter.hh: Delete, and
move the contents...
* src/tgba/tgba.hh: ... here.
* src/tgba/Makefile.am: Adjust.
* src/graphtest/ngraph.cc, src/kripke/fairkripke.hh,
src/saba/sabacomplementtgba.cc, src/ta/ta.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/bfssteps.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/rundotdec.cc, wrap/python/spot.i: Adjust includes.
 2014-08-19 21:48:32 +02:00
Alexandre Duret-Lutz
a5bc7c3ff6 * src/misc/bitvect.hh (bitvect_array): Make as SPOT_DELETED. 2014-08-19 16:15:02 +02:00
Alexandre Duret-Lutz
e7dc62e3c8 * NEWS: Add more news. 2014-08-19 14:57:35 +02:00
Alexandre Duret-Lutz
e5124faa13 man: more doc about TGBA and monitors 
This was prompted by an exchange of emails with Caroline Lemieux.

* src/bin/man/ltl2tgba.x: Add notes and references.
* NEWS, THANKS: Update.
 2014-08-19 14:52:51 +02:00
Alexandre Duret-Lutz
06a0c498a4 * src/bin/common_setup.cc: Disable sync_with_stdio to boost I/O. 2014-08-19 10:01:29 +02:00
Alexandre Duret-Lutz
bc2e68f85c tgbatest: rewrite emptchk.test in C++ 
So that its run time goes from 10min+ to ~5s.

* src/tgbatest/emptchk.cc: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbatest/emptchk.test: Use it.
 2014-08-18 23:59:59 +02:00
Alexandre Duret-Lutz
b360b02290 tgbatest: speed ltl2ta.test up! 
Again instead of calling ltl2tgba dozen of times with different options
for various formulas, this implements a single executable that reads
formulas from a file, translate them using the different setups, and
dump statistics for comparison.  Valgrind now only has to be started
once.

* src/tgbatest/checkta.cc: New file.
* src/tgbatest/Makefile.am: Use it.
* src/tgbatest/ltl2ta.test: Rewrite using checkta.
* src/tgbatest/ltl2tgba.cc: Remove a unused variable.
 2014-08-18 20:23:15 +02:00
Alexandre Duret-Lutz
9502266f95 tgbatest: implement a large part of ltl2tgba.test in c++ 
So that running valgrind is a lot more efficient.  Running
ltl2tgba.test using to take more than 15min.  We are now down to
25sec.

* src/tgbatest/checkpsl.cc: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.test: Adjust.
 2014-08-17 19:46:14 +02:00
Alexandre Duret-Lutz
6a741189bc ltltest: speedup more tests 
This generalizes the previous patch.

* src/ltltest/equalsf.cc: Allow escaped '\,' and
negated result.
* src/ltltest/Makefile.am: Use equalsf.cc for
almost all tests that used equals.cc.
(nequals): New.
* src/ltltest/equals.test, src/ltltest/eventuniv.test,
src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
src/ltltest/parseerr.test, src/ltltest/tunabbrev.test,
src/ltltest/tunenoform.test: Adjust.
 2014-08-17 12:29:12 +02:00
Alexandre Duret-Lutz
7b9f695265 Speedup reduccmp.test 
This test used to take more than 10min because an instance of valgrind
was launched for each separate equivalence check.  The list of
equivalences to checks are not given in a file, and only two valgrind
instances are run.  The test takes less than 15sec.

* src/ltltest/equalsf.cc: New file.
* src/ltltest/Makefile.am (reduccmp, reductaustr): Build using
equalsf.cc.
* src/ltltest/reduccmp.test: Rewrite.
* src/ltltest/uwrm.test: Also rewrite, and use valgrind.
 2014-08-17 11:26:33 +02:00
Alexandre Duret-Lutz
b43f75e917 tgba: move boolean properties from tgba_digraph to tgba 
* src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
* src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
setting/querying/copying the following properties: single_acc_set,
state_based_acc, inherently_weak, deterministic.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
it to bypass some useless work.
 2014-08-15 16:10:39 +02:00
Alexandre Duret-Lutz
e3b5119f25 degen: return input if it is already degeneralized 
* src/tgbaalgos/degen.cc (degeneralize, degeneralize_tba): Shortcut
degeneralization if the automaton is already degeneralized.
 2014-08-15 11:24:41 +02:00
Alexandre Duret-Lutz
bf6c906772 Fix some bdd_dict_ptr not being passed by const reference. 
* iface/dve2/dve2.cc, iface/dve2/dve2.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
src/tgba/tgbagraph.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/translate.cc,
src/tgbaalgos/translate.hh, src/tgbaalgos/word.cc,
src/tgbaalgos/word.hh: Pass shared_ptr to functions by const ref.
 2014-08-15 11:07:05 +02:00
Alexandre Duret-Lutz
51151ab271 Handle all automata through shared_ptr. (monstro patch) 
A type such as 'const tgba_digraph*' and 'tgba_digraph*' are replaced
by 'const_tgba_digraph_ptr' and 'tgba_digraph_ptr'.  Additionally 'new
tgba_digraph(...)' is replaced by 'make_tgba_digraph(...)'.

This convention is followed by all automata types. Those smart
pointers should normally be passed by const reference as input of
function to avoid the atomic increments/decrements, but I probably
missed a few, as this huge patch took me nearly 12h.

* src/kripke/fwd.hh, src/tgba/fwd.hh: New files.
* src/kripke/Makefile.am, src/tgba/Makefile.am: Adjust.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/common_output.hh, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
src/bin/ltlfilt.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/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/neverparse/neverclaimparse.yy,
src/neverparse/public.hh, src/priv/accmap.hh,
src/priv/countstates.cc, src/priv/countstates.hh, src/saba/saba.hh,
src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/sabacomplementtgba.cc, src/ta/ta.hh,
src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
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/dotty.cc, src/taalgos/dotty.hh,
src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
src/taalgos/tgba2ta.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
src/tgba/formula2bdd.hh, src/tgba/futurecondcol.cc,
src/tgba/futurecondcol.hh, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.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/tgbascc.cc,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh,
src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.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/dotty.hh, src/tgbaalgos/dottydec.cc,
src/tgbaalgos/dottydec.hh, 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/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/isdet.cc,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.cc,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.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/rundotdec.cc,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/safety.cc,
src/tgbaalgos/safety.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.cc, 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.cc, src/tgbaalgos/stripacc.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/maskacc.cc, src/tgbatest/powerset.cc,
src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
wrap/python/ajax/spot.in, wrap/python/spot.i,
wrap/python/tests/interdep.py: Use shared pointers for automata.
 2014-08-15 11:07:05 +02:00
Alexandre Duret-Lutz
ca85d4184d tgba_union: Remove this unused class. 
* src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh: Delete.
* src/tgba/Makefile.am: Adjust.
 2014-08-14 20:17:45 +02:00
Alexandre Duret-Lutz
dc5ad78b3e Make bdd_dict a shared pointer. 
* src/tgba/bdddict.hh (bdd_dict_ptr): New type.
(make_bdd_dict): New function.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/dstarparse/dstarparse.yy, src/dstarparse/public.hh,
src/graphtest/tgbagraph.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/neverparse/neverclaimparse.yy, src/neverparse/public.hh,
src/priv/accmap.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/sabatest/sabacomplementtgba.cc,
src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/taalgos/dotty.cc, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.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/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh,
src/tgba/wdbacomp.cc, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaalgos/word.cc, src/tgbaalgos/word.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/maskacc.cc,
src/tgbatest/powerset.cc, src/tgbatest/randtgba.cc,
src/tgbatest/taatgba.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/parsetgba.py: Update to use bdd_dict_ptr and
make_bdd_dict().
 2014-08-13 20:23:09 +02:00
Alexandre Duret-Lutz
10e5c62386 Simplify copying of atomic propositions in new tgba_digraph. 
* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(register_all_propositions_of): New method.
* src/tgba/tgbagraph.hh (copy_ap_of): New method.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/dstarparse/nsa2tgba.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stripacc.cc: Simplify using copy_ap_of.
 2014-08-13 16:05:09 +02:00
Alexandre Duret-Lutz
917f70073f tgba_digraph: add a set_single_acceptance_set() method. 
* src/tgba/tgbagraph.cc: New file.
* src/tgba/Makefile.am: Adjust.
* src/tgba/tgbagraph.hh (set_single_acceptance_set,
new_acc_transition): New methods.
(set_acceptance_conditions, merge_transitions): Move body
to tgbagraph.cc.
* src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbacomp.cc,
src/neverparse/neverclaimparse.yy, src/dstarparse/dra2ba.cc,
src/dstarparse/nra2nba.cc: Simplify using these new methods.
 2014-08-13 14:31:11 +02:00