Commit graph

143 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
bc61ca73c6 * wrap/python/cgi-bin/ltl2tgba.in: Reword description of svg_output. 2010-02-02 18:28:43 +01:00
Alexandre Duret-Lutz
72ae820b0c Add SVG output and language containment options to the cgi script.
* wrap/python/cgi-bin/ltl2tgba.in (new): Mark new options as new.
(svg_output, reduce_langcout): Add these new options.
(render_dot): Support svg_output.
2010-02-02 16:58:14 +01:00
Alexandre Duret-Lutz
a4766f2f82 Add SCC pruning options to the CGI script.
* wrap/python/cgi-bin/ltl2tgba.in: Add options to symbolically
prune unaccepting SCCs in LaCIM, and explicitely pruns unaccepting
SCCs in all algorithms.
* src/tgbaalgos/reductgba_sim.hh: Conceal most of the file to
SWIG.
* wrap/python/spot.i: Include reductgba_sim.hh.
2010-01-30 14:52:16 +01:00
Alexandre Duret-Lutz
4efde0d3d3 Make it possible to use the cgi script without installing a web
server.

* wrap/python/cgi-bin/ltl2tgba.in: Starts a web server if the
script is not called as a CGI.  Arrange to load libraries from
the build directory.  Create the spotimg/ if needed when run as
a web server.
* wrap/python/cgi-bin/Makefile.am: Adjust build rule and clean
the spotimg directory.
* wrap/python/cgi-bin/README, NEWS: Update.
2010-01-30 14:15:03 +01:00
Alexandre Duret-Lutz
85532dc8f8 Do not recognize "*" as "and". This leaves room for an
implementation of rational operators in a future version.

* src/ltlparse/ltlscan.ll: Do not recognize "*".
* wrap/python/cgi-bin/ltl2tgba.in: Undocument it.
* NEWS: Mention this.
* src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/reductgba.test: Replace "*" by "&".
2010-01-30 12:27:20 +01:00
Alexandre Duret-Lutz
7d5f493fb2 Rename wrap/python/cgi/ as wrap/python/cgi-bin/.
* wrap/python/cgi/: Rename as ...
* wrap/python/cgi-bin/: ... this.
* configure.ac, spot/wrap/python/Makefile.am, README: Adjust.
2010-01-29 15:48:56 +01:00
Damien Lefortier
58d6b7912c * wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new
translation algorithm: Tauriainen/TAA.
2010-01-25 18:37:19 +01:00
Damien Lefortier
d9b8fcddd6 * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead
of the UNIQUE_ID environment variable to avoid being
Apache-specific.
2010-01-25 18:33:31 +01:00
Guillaume Sadegh
3a974d61f0 Fix copyrights.
* bench/Makefile.am, bench/gspn-ssp/Makefile.am,
bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am,
bench/split-product/Makefile.am, configure.ac,
iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh,
iface/nips/Makefile.am, iface/nips/common.cc,
iface/nips/common.hh, iface/nips/dottynips.cc,
iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am,
src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc,
src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am,
src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh,
src/evtgba/product.cc, src/evtgba/product.hh,
src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am,
src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in,
src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc,
src/ltlast/atomic_prop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlenv/environment.hh,
src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
src/ltltest/Makefile.am, src/ltltest/defs.in,
src/ltltest/equals.cc, src/ltltest/equals.test,
src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/ltltest/randltl.cc, src/ltltest/readltl.cc,
src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc,
src/ltltest/syntimpl.test, src/ltltest/tostring.cc,
src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/misc/bddalloc.cc,
src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh,
src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh,
src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh,
src/saba/Makefile.am, src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/Makefile.am, src/sabatest/defs.in,
src/sanity/Makefile.am, src/tgba/Makefile.am,
src/tgba/bdddict.cc, src/tgba/bddprint.cc,
src/tgba/formula2bdd.cc, src/tgba/state.hh,
src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc,
src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc,
src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc,
src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am,
src/tgbatest/bddprod.test, src/tgbatest/complementation.cc,
src/tgbatest/complementation.test, src/tgbatest/defs.in,
src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
src/tgbatest/explpro3.test, src/tgbatest/explpro4.test,
src/tgbatest/explprod.cc, src/tgbatest/explprod.test,
src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc,
src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc,
src/tgbatest/mixprod.test, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/readsave.test,
src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py:
Fix copyrights.
2010-01-24 20:51:09 +01:00
Alexandre Duret-Lutz
391372ae2a Turn parse_error_list into an opaque type for Swig. This
kills a memory leak warning from swig/python.

* src/ltlparse/public.hh (parse_error_list): Declare
as an empty struct for Swig.
* wrap/python/tests/ltlparse.py: Fix copyright.
2010-01-22 17:29:12 +01:00
Alexandre Duret-Lutz
49d1abbda7 Remove python bindings for ltl::clone and ltl::destroy.
* wrap/python/spot.i: Do not include clone.hh and destroy.hh.
2009-11-11 11:13:00 +01:00
Alexandre Duret-Lutz
77df39b4dd Deprecate ltl::destroy(f) in favor of f->destroy()
* src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
Transform this static function into a member function.
* src/ltlvisit/destroy.hh (destroy): Document and declare as
deprecated.
* bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
src/ltlast/automatop.cc, src/ltlast/binop.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
src/ltltest/equals.cc, src/ltltest/randltl.cc,
src/ltltest/readltl.cc, src/ltltest/reduc.cc,
src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/bddprint.cc, src/tgba/taa.cc,
src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
the #include "destroy.hh" when appropriate.
2009-11-09 07:13:31 +01:00
Alexandre Duret-Lutz
48fb19ea44 Deprecate ltl::clone(f) in favor of f->clone().
* src/ltlvisit/clone.hh (clone): Document and declare as deprecated.
* src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py:
Adjust clone() usage, and remove the #include "clone.hh" when
appropriate.
2009-11-09 07:13:31 +01:00
Alexandre Duret-Lutz
1f6087953b Also revert b28d7ba804 as it was a follow-up to Damien's work. 2009-03-25 17:26:44 +01:00
Alexandre Duret-Lutz
b28d7ba804 adjust #includes in python/ 2008-06-12 16:56:40 +02:00
Alexandre Duret-Lutz
5ef7084b61 Add .gitignore files 2008-03-14 16:59:32 +01:00
Alexandre Duret-Lutz
ec6bca7992 * wrap/python/cgi/ltl2tgba.in: Adjust to newer versions of swig. 2008-02-25 14:37:54 +01:00
Alexandre Duret-Lutz
3751960ac8 * wrap/python/cgi/ltl2tgba.in: Fix degeneralisation and output of
accepting runs.
2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
851ca0d807 * wrap/python/spot.i: Wrap spot::emptiness_check_instantiator.
* wrap/python/cgi/ltl2tgba.in: Offers all 6 emptiness
check algorithms, and a text box for options.
2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
fed4b6f05c * src/misc/optionmap.hh, src/misc/optionmap.cc
(option_map::parse_options): Rewrite.  Do not modify the input
string, allow !foo as a shorthand for foo=0, and support K and
M suffixes for values.
* src/tgbatest/randtgba.cc (cons_emptiness_check): Simplify.
* wrap/python/spot.i: Process optionmap.hh.
* wrap/python/tests/optionmap.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
2005-02-17 15:01:51 +00:00
Alexandre Duret-Lutz
b0a51a0656 Adjust Swig rules for Swig 1.3.24 (and probably 1.3.23 too).
Compiling the runtime in a separate modules is no longer required,
and actually it does not work anymore...
* wrap/python/swigpy.i: Remove.
* wrap/python/Makefile.am (_swigpy.la): Remove all references.
($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Do not
use -noruntime.
2004-12-15 12:59:46 +00:00
Alexandre Duret-Lutz
541705a36a * src/misc/random.hh (nrand, bmrand, prand): New functions.
(barand): New class.
* src/misc/random.cc (nrand, bmrand, prand): New functions.
* wrap/python/spot.i: Process src/misc/random.hh.
2004-12-07 18:52:10 +00:00
Alexandre Duret-Lutz
fdeea6dbf8 * wrap/python/tests/run.in: Do not override PYTHONPATH, just add
to it.
Report from Akim Demaille.
2004-11-28 17:12:21 +00:00
Alexandre Duret-Lutz
b61fab1eb0 * wrap/python/tests/run.in: Define DYLD_LIBRARY_PATH so that
Darwin finds non-installed libraries.
Report from Akim Demaille.
2004-11-28 13:52:27 +00:00
Alexandre Duret-Lutz
ca6084160e * wrap/python/cgi/ltl2tgba.in: Add options to check the produced
automata for emptiness, using the existing algorithms.
* wrap/python/spot.i: Declare spot::explicit_magic_search,
and spot::explicit_se05_search as allocating their output.
2004-11-14 23:10:56 +00:00
Alexandre Duret-Lutz
1d3100607a * wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh,
tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and
tgbaalgos/rundotdec.hh.
2004-11-04 08:03:59 +00:00
Alexandre Duret-Lutz
91b9682bd8 * wrap/python/Makefile.am (_spot_la_SOURCES): Add spot_wrap.h. 2004-10-21 11:01:27 +00:00
Alexandre Duret-Lutz
094ddca665 * src/misc/modgray.hh, src/misc/modgray.cc: New files.
* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
* wrap/python/spot.i: Activate directors, and interface modgray.hh.
* wrap/python/tests/modgray.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
2004-10-20 15:46:56 +00:00
Alexandre Duret-Lutz
d647e7a0db * wrap/python/tests/run.in: Typo. From Akim Demaille. 2004-10-12 07:41:19 +00:00
Alexandre Duret-Lutz
f0aa58034c Update to SWIG 1.3.22.
* wrap/python/libpy.c: Delete.
* wrap/python/swigpy.i: New file.
* wrap/python/Makefile.am (swigpy_wrap.c): Build this from swigpy.i
and use it instead of libpy.c.
2004-09-20 16:35:46 +00:00
Alexandre Duret-Lutz
7b314789ca * configure.ac: Call AC_PROG_CC and AM_PROG_CC_C_O.
* wrap/python/Makefile.am (_buddy_la_LDFLAGS): Move libspotswigpy.la ...
(_buddy_la_LIBADD): ... here.
2004-08-07 22:11:45 +00:00
Alexandre Duret-Lutz
bd69b16e46 * wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options.
* wrap/python/spot.i: Wrap src/ltlvisite/reduce.hh.
2004-06-23 08:28:50 +00:00
Alexandre Duret-Lutz
c68d182951 * wrap/python/cgi/ltl2tgba.in: Typos. 2004-05-25 09:03:51 +00:00
Alexandre Duret-Lutz
2b1efe172c * wrap/python/cgi/ltl2tgba.in: Typos. 2004-05-25 08:56:16 +00:00
Alexandre Duret-Lutz
41589e2818 * wrap/python/buddy.i: Define typemap for input_buf and use it
for fdd_extdomain.  Define const_int_ptr and use it for fdd_vars.
2004-05-17 13:18:32 +00:00
Alexandre Duret-Lutz
1e2669d640 * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. 2004-05-14 16:11:46 +00:00
Alexandre Duret-Lutz
aa5cef3c83 * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
fair_loop_approx.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the
fair_loop_approx optimization.
(ltl_promise_visitor, ltl_possible_fair_loop_visitor,
possible_fair_loop_checker): New classes.
* src/tgbatest/ltl2tgba.cc: Add the -L option.
* src/tgbatest/spotlbtt.test: Exercise fair_loop_approx.
* wrap/python/cgi/ltl2tgba.in: Make it an option.
2004-05-10 10:41:28 +00:00
Alexandre Duret-Lutz
6b06e28f3d * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
branching_postponement.
* src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
from ltl_to_tgba_fm().
(ltl_to_tgba_fm): Implement the branching_postponement optimization.
* src/tgbatest/ltl2tgba.cc: Add the -p option.
* src/tgbatest/spotlbtt.test: Exercise branching postponement.
* wrap/python/cgi/ltl2tgba.in: Make it an option.
2004-05-07 10:00:34 +00:00
Alexandre Duret-Lutz
b052e92537 * wrap/python/cgi/ltl2tgba.in: Fix output HTML. 2004-05-04 07:33:12 +00:00
Alexandre Duret-Lutz
28288e0478 * wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics
when show_never_claim.  Change the title to LTL-to-TGBA.
2004-04-22 10:13:10 +00:00
Alexandre Duret-Lutz
d07e549832 * wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's
version a separate variable.
2004-04-21 21:03:56 +00:00
Alexandre Duret-Lutz
9a8d554f59 * wrap/python/cgi/ltl2tgba.in: Pass the formula to
never_claim_reachable, and cgi.escape its output.
Lighten the color a bit.
2004-04-21 20:23:57 +00:00
Alexandre Duret-Lutz
231a77a05f * wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
the new variable dot_bgcolor.
2004-04-21 19:52:30 +00:00
Alexandre Duret-Lutz
5904255b14 * wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output
using this new function.
2004-04-21 19:32:37 +00:00
Alexandre Duret-Lutz
0c3d4fef9f * wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.
2004-04-21 19:02:31 +00:00
Alexandre Duret-Lutz
80b7cbcf45 * wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx)
($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c.
2004-04-13 09:38:49 +00:00
Alexandre Duret-Lutz
9e269dadc2 * wrap/python/cgi/ltl2tgba.in: Process ltl2tgba.opt if it exists. 2004-02-20 23:15:04 +00:00
Alexandre Duret-Lutz
ab26065f4c * wrap/python/cgi/ltl2tgba.in: Color translators and their options. 2004-02-20 22:51:13 +00:00
Alexandre Duret-Lutz
153962aa9d * wrap/python/cgi/ltl2tgba.in: Present the options in a table. 2004-02-20 21:51:39 +00:00
Alexandre Duret-Lutz
0a1fc73eed * wrap/python/cgi/ltl2tgba.in: Remove the "print dot" options,
add a "dot source" source behind each picture instead.  Do
not run `dot' on big automata.
2004-02-20 21:00:06 +00:00