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

2995 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
579e8fc0a9 add missing utf-8 header to many source files 
* src/sanity/style.test: Test for the missing header.
* iface/ltsmin/check.test, src/kripketest/kripke.test,
src/kripketest/parse_print_test.cc, src/ltlparse/fmterror.cc,
src/ltltest/consterm.test, src/ltltest/kind.test,
src/ltltest/length.test, src/ltltest/ltlfilt.test,
src/ltltest/reduc.cc, src/ltltest/reduc.test,
src/ltltest/reduc0.test, src/ltltest/reducpsl.test,
src/ltltest/remove_x.test, src/ltltest/unabbrevwm.test,
src/ltltest/utf8.test, src/ltltest/uwrm.test, src/ltlvisit/dump.cc,
src/ltlvisit/remove_x.cc, src/misc/casts.hh, src/misc/fixpool.hh,
src/misc/hashfunc.hh, src/misc/ltstr.hh, src/sanity/readme.test,
src/taalgos/tgba2ta.cc, src/tgbaalgos/bfssteps.cc,
src/tgbaalgos/stats.cc, src/tgbatest/acc.test,
src/tgbatest/bitvect.test, src/tgbatest/complementation.test,
src/tgbatest/cycles.test, src/tgbatest/degendet.test,
src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
src/tgbatest/emptchkr.test, src/tgbatest/intvcomp.test,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2ta2.test,
src/tgbatest/ltlprod.test, src/tgbatest/maskacc.test,
src/tgbatest/obligation.test, src/tgbatest/randpsl.test,
src/tgbatest/readsat.cc, src/tgbatest/readsat.test,
src/tgbatest/scc.test, src/tgbatest/sccsimpl.test,
src/tgbatest/taatgba.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test, src/tgbatest/uniq.test,
src/tgbatest/wdba.test: Add it.
 2015-01-09 08:23:49 +01:00
Alexandre Duret-Lutz
3a70b57067 projrun: modernize 
* src/tgbaalgos/emptiness.hh (step): Add constructors...
* src/tgbaalgos/projrun.cc: ... to simplify this.
 2015-01-09 08:23:49 +01:00
Alexandre Duret-Lutz
94577d6519 product: rename the one-the-fly version as otf_product 
This avoid compiler errors about ambiguous calls and make sure we are
calling the intended algorithms everywhere (this wasn't the case).

* src/tgba/tgbaproduct.hh (product, product_at): Rename as...
(otf_product, otf_product_at): ... this.
* iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc, src/bin/ltlfilt.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/complementation.cc, src/tgbatest/ltlprod.cc: Adjust
callers.
 2015-01-09 08:23:49 +01:00
Alexandre Duret-Lutz
a9748804e4 contain: adjust to use explicit product 
* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh: Here.
 2015-01-08 23:39:53 +01:00
Alexandre Duret-Lutz
bb9b204dee stutter: gather all code in one place 
* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh, src/tgbaalgos/closure.cc,
src/tgbaalgos/closure.hh, src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh, src/tgbaalgos/stutterize.cc,
src/tgbaalgos/stutterize.hh: Delete these files, and merge their
contents into...
* src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh: ... these two.
* src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
* wrap/python/spot.i: Adjust.
 2015-01-08 23:39:45 +01:00
Alexandre Duret-Lutz
ab985afa9e * src/tgbaalgos/weight.hh: Remove useless status. 2015-01-08 21:46:44 +01:00
Alexandre Duret-Lutz
5345cae839 * src/tgbaalgos/emptiness_stats.hh: Modernize. 2015-01-08 21:45:22 +01:00
Alexandre Duret-Lutz
d9d46492cb more files to ignore 2015-01-08 21:04:03 +01:00
Alexandre Duret-Lutz
d3fdf55fa3 fix symbol collision, seen with clang-3.5 
autfilt would segfault after reading any file, because the local result_
structure used in hoaparse has the same name as the local result_
structure used in dstarparse.  For some reason I can only see this
problem using clang-3.5, not with gcc.

* src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Declare both
structures in a different namespace.
 2015-01-08 20:59:57 +01:00
Alexandre Duret-Lutz
ee0c0cd28c * doc/org/tools.org: Adjust colors in text. 2015-01-08 18:33:17 +01:00
Alexandre Duret-Lutz
4673427252 remove obsolete comments 
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/neverclaim.hh: Remove obsolete
comments.  Reported by Claire Parquier.
 2015-01-08 17:01:40 +01:00
Alexandre Duret-Lutz
1492acc585 * src/dstarparse/dstarscan.ll: Fix encoding. 2015-01-08 15:22:40 +01:00
Alexandre Duret-Lutz
56ed13a96d org: factor headers into setup.org 
* doc/org/setup.org: New file.
* doc/Makefile.am: Distribute it.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/ltlgrind.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org: Use
setup.org.
 2015-01-07 19:35:30 +01:00
Alexandre Duret-Lutz
15852b4e93 org: update randltl.org 
* doc/org/randltl.org: The first example used to output '1' as
only random formula.  This is not very sexy.
 2015-01-07 19:35:30 +01:00
Alexandre Duret-Lutz
fbcc9fb81f org: use a white background and ship the CSS 
* doc/org/spot.css: New file.
* doc/Makefile.am: Distribute it.
* doc/org/init.el.in, doc/org/.dir-locals.el: Adjust links.
 2015-01-07 19:35:30 +01:00
Alexandre Duret-Lutz
f9029858c4 org: Update results to new output 
The dotty output changed to be horizontal, and also
the acceptance sets are now numbers.

* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
doc/org/satmin.org: Adjust these four.
 2015-01-06 18:42:49 +01:00
Alexandre Duret-Lutz
f88020035c org: fix EMAIL link 
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/ltlgrind.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org: Here.
 2015-01-06 18:23:58 +01:00
Alexandre Duret-Lutz
a3ce452548 Update HACKING 
* HACKING: Update Swig requirement, as reported by Soheib.
 2015-01-06 16:23:26 +01:00
Alexandre Duret-Lutz
7c34c1ae79 stutterize: fix sl2() to keep the correct properties 
Combined with 87c2b29, this fixes #7.

* src/tgbaalgos/stutterize.cc: Call keep_props().
* src/tgbaalgos/closure.cc: Just specify the encoding.
* src/bin/autfilt.cc: Add a --instut=2 option.
* src/tgbatest/stutter.test: More test.
 2015-01-05 21:52:12 +01:00
Alexandre Duret-Lutz
314993b201 hoa: add two asserts 
* src/tgbaalgos/hoa.cc: Here.
 2015-01-05 21:46:21 +01:00
Alexandre Duret-Lutz
0b8b65f96f hoaparse: validate use of deterministic and complete 
* src/hoaparse/hoaparse.yy: validate deterministic and
complete when parsing HOA.  Also set the deterministic
property on the TGBA.
* src/tgbatest/hoaparse.test: Test errors.
 2015-01-05 21:46:21 +01:00
Alexandre Duret-Lutz
578e390d8d hoaparse: validate use of explicit-labels and implicit-labels 
* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.
 2015-01-05 21:45:55 +01:00
Alexandre Duret-Lutz
34b798e115 hoaparse: validate use of state-labels and trans-labels 
* src/hoaparse/hoaparse.yy: Fix a map with properties, and use it to
report error when state-label or trans-label are misused.
* src/tgbatest/hoaparse.test: Test that.
 2015-01-05 13:33:59 +01:00
Alexandre Duret-Lutz
eff4bdb80f more files to ignore 2015-01-05 11:36:29 +01:00
Alexandre Duret-Lutz
0895f11503 hoa: use the tgba_digraph interface to save automata 
* src/tgbaalgos/hoa.cc: Here.
* src/tgbatest/det.test, src/tgbatest/hoaparse.test,
src/tgbatest/monitor.test, doc/org/oaut.org: Adjust.
 2015-01-04 23:39:47 +01:00
Alexandre Duret-Lutz
892fb11f04 neverclaim: do not pass the formula 
* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh: Do not
pass the formula.  Use the automaton name instead.
* src/tgbatest/ltl2tgba.cc: Adjust.
 2015-01-04 18:01:24 +01:00
Alexandre Duret-Lutz
490c97d797 hoa: simplify the interface of hoa_reachable() 
* src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh: Only
keep one function public, and do not pass the formula.
* src/tgbatest/ltl2tgba.cc: Adjust.
 2015-01-04 18:00:32 +01:00
Alexandre Duret-Lutz
cbf1e15b01 org: document common output options for automata 
* doc/org/oaut.org: New file.
* doc/Makefile.am: Add it.
* doc/org/autfilt.org, doc/org/ltl2tgba.org, doc/org/randaut.org,
doc/org/tools.org: Link to it.
 2015-01-04 17:08:39 +01:00
Alexandre Duret-Lutz
403179087e dotty: fix combination of 's' with 'n' 
* src/tgbaalgos/dotty.cc: Add empty label to each cluster
if both 's' and 'n' are used.
* src/tgbatest/neverclaimread.test: Test it.
 2015-01-04 16:04:07 +01:00
Alexandre Duret-Lutz
a5d52633bd bin: fix help text for --dot 
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Here.
 2015-01-04 15:59:45 +01:00
Alexandre Duret-Lutz
c6a5de3e23 dstar2tgba: add support for --name and --stats=%m 
* src/bin/dstar2tgba.cc: Here.
* src/tgbatest/dstar.test: Test them.
 2015-01-04 12:55:26 +01:00
Alexandre Duret-Lutz
2e356aed1d dotty: fix output of name and detection of state-based acceptance 
* src/tgbaalgos/dotty.cc: Do not output name by default.  Display
accepting states by default no acceptance set are used.
Avoid copying the automaton when possible.
* src/tgbatest/dstar.test: Exercise --dot=t.
 2015-01-04 12:38:07 +01:00
Alexandre Duret-Lutz
4d4c5d807b ltl2tgba, randaut: better error reporting 
* src/bin/ltl2tgba.cc, src/bin/randaut.cc: Catch exceptions
in main loop.
* src/tgbatest/ltl2tgba.test, src/tgbatest/randaut.test: Test
errors with unknown --dot argument.
 2015-01-04 11:24:31 +01:00
Alexandre Duret-Lutz
5497bef3d0 * doc/org/ioltl.org: Typo. 2015-01-03 22:36:06 +01:00
Alexandre Duret-Lutz
3b7b52027c More files to ignore. 2015-01-03 19:01:44 +01:00
Alexandre Duret-Lutz
b048f65dd8 bin: --dot=s display SCCs 
* src/tgbaalgos/dotty.cc: Add option 's' to display SCCs.
* src/bin/dstar2tgba.cc, src/bin/common_aoutput.cc: Document it.
* src/tgbatest/neverclaimread.test: Test it.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
5b723bf8c0 work around a swig issue on Arch Linux 
destroy_atomic_prop_set() takes a parameter named 'as', and aparently
Swig reuses this name as-is, although it is a Python keyword.

* src/ltlvisit/apcollect.hh (destroy_atomic_prop_set): Rename the
parameter to please Swig on Arch Linux.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
c73a4ac916 * src/sanity/style.test: Do not use the deprecated GREP_OPTIONS. 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
40fb80ea2c bin: use common_aoutput in ltl2tgba 
* src/bin/common_aoutput.hh, src/bin/common_aoutput.cc: Adjust to
support three kind of statistics printer, depending on whether the
tool input formulas, automata, or nothing.
* src/bin/randaut.cc, src/bin/autfilt.cc: Adjust.
* src/bin/ltl2tgba.cc: Use the common_aoutput printers.  The
--csv-escape option disappeared along the way, but it was not honored
anyway...
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
72737dfefc bin: factor output options of autfilt and randaut 
* src/bin/autfilt.cc: Move output options handling...
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh:... here.
* src/bin/randaut.cc: Use them.
* src/tgbatest/randaut.test: Test --name and --stats for randaut.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
3f4b19142d * src/bin/common_setup.cc: bump copyright year to 2015. 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
cf65f606b4 ltlgrind: cosmetics 
* src/bin/ltlgrind.cc: Adjust help text to match other tools.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
06b8118dec ltl2tgba: rename --hoa to --hoaf 
for consistency with autfilt, randaut, and dstar2tgba

* src/bin/ltl2tgba.cc: Here.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
a7c1d4c479 autfilt, randaut: rename --uniq to --unique 
for consistency with ltlfilt

* src/bin/autfilt.cc, src/bin/randaut.cc: Here.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
18d8c3efc0 bin: tooling and documentation about option names 
* src/bin/options.py: New file.
* src/bin/Makefile.am: Distribute it.
* src/bin/README: New file.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
21dcc73deb randaut: fix --uniq 
* src/bin/autfilt.cc: Also accept '-u' for '--uniq'.
* src/bin/randaut.cc: Likewise, plus fix the unicity check.
* src/tgbatest/uniq.test: Really test it.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
36f995651e autfilt: move output functions to a separate file 
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: New files...
* src/bin/autfilt.cc: ... extracted from here.
* src/bin/Makefile.am: Add them.
 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
bbf019a450 * iface/ltsmin/Makefile.am: Fix location of -lpthread. 2015-01-03 17:08:14 +01:00
Alexandre Duret-Lutz
87c2b291ed tgba_digraph: force selection of properties kept on copy 
* src/tgba/tgba.hh: Declare a prop_set to specify the types.
* src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
* iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
 2015-01-03 17:08:01 +01:00
Alexandre Duret-Lutz
77cb836e47 dotty: Specialize for tgba_digraph_ptr 
* src/tgbaalgos/dotty.cc: Specialize for tgba_digraph_ptr.
* src/tgba/tgbagraph.hh, src/tgbaalgos/dupexp.cc: Copy properties by
default when cloning an automaton.
* src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/ltl2tgba.test, src/tgbatest/monitor.test,
src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test: Adjust
tests.
 2015-01-03 16:49:14 +01:00