Commit graph

4097 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
835b5ee1cf improve some conditions, as hinted by PVS-Studio
For #192.

* spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/are_isomorphic.cc,
spot/taalgos/tgba2ta.cc: Here.
2016-10-29 12:37:35 +02:00
Alexandre Duret-Lutz
40b8bab890 remove some dead code discovered while studying PVS-Studio's report
For #192.

* spot/misc/timer.hh, spot/twa/bdddict.cc, spot/twa/bdddict.hh,
spot/twaalgos/sbacc.cc: Here.
2016-10-29 12:37:35 +02:00
Alexandre Duret-Lutz
279bfa00bd fix some implicit promotion from bool, as suggested by PVS-Studio
For #192.

* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
spot/tl/randomltl.cc, spot/twa/acc.cc, spot/twaalgos/postproc.hh: Here.
2016-10-29 12:37:35 +02:00
Alexandre Duret-Lutz
630e90b9cc ltsmin: fix constness of arguments as suggested by PVS-Studio
For #192.

* spot/ltsmin/ltsmin.cc (compile_model): Here.  As remove some unused
variable.
2016-10-29 12:37:35 +02:00
Alexandre Duret-Lutz
26e94b774f taproduct: fix incorrect assert() flagged by PVS-Studio
For #192.

* spot/ta/taproduct.cc: Check the output of down_cast, not its input.
2016-10-29 12:37:35 +02:00
Alexandre Duret-Lutz
d0112a7b8a fix unpaired copy-ctor/op= reported by PVS-Stydio
For #192.

* bin/common_trans.cc, bin/common_trans.hh, spot/twa/acc.hh:
Add an operator= in addition to the copy constructor.
* spot/twaalgos/ltl2tgba_fm.cc: Use the default constructor.
* spot/ta/taproduct.cc, spot/ta/taproduct.hh: Delete an unused copy
constructor.
2016-10-29 12:37:21 +02:00
Alexandre Duret-Lutz
63818a3e69 [buddy] Fix several PVS-Studio warnings
For #192.

* src/bddio.c, src/cppext.cxx, src/kernel.c: Fix printf formats, calls
to new, and simplify one check in bdd_delref_nc().
2016-10-28 17:12:21 +02:00
Alexandre Duret-Lutz
41b47966b0 * README: Update description of Spot and its documentation. 2016-10-25 23:17:51 +02:00
Etienne Renault
f9991288f7 compression: fix bad encoding
Fixes #190.

* NEWS, spot/misc/intvcomp.cc: here.
2016-10-25 14:55:27 +02:00
Alexandre Duret-Lutz
ce63c30c0b translate: reset the LTL simplifier on set_level().
Fix an issue reported by Tomáš Babiak, who noticed that he could not
manage to have ltl2tgba process `genltl --go-theta=N` efficiently for
larger values of N.

* spot/twaalgos/translate.hh (set_level): Reset any owned LTL simplifier
whenever the optimization level is changed.
* NEWS: Mention the bug.
2016-10-25 13:53:28 +02:00
Alexandre Duret-Lutz
4be7065b81 simulation: speedup on deterministic automata
* spot/twaalgos/simulation.cc: Detect deterministic automata, and skip
the partial-order update.
* NEWS: Mention the speedup.
2016-10-23 19:55:48 +02:00
Alexandre Duret-Lutz
6ca555ed89 determinize: improve the storage of implications
* spot/twaalgos/determinize.cc: Store implications
in a vector, not a map.
* spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh: Adjust.
2016-10-21 14:26:49 +02:00
Alexandre Duret-Lutz
7ea9454614 * spot/misc/bitvect.hh (is_subset_of): Fix implementation. 2016-10-20 21:00:27 +02:00
Alexandre Duret-Lutz
a32ccd649d [buddy] slight optimization of bdd_implies
* src/bddop.c: Avoid the first recursion when it is obvious that the
second will fail.
2016-10-20 20:59:28 +02:00
Alexandre Duret-Lutz
41866b370c * spot/twaalgos/simulation.cc: Simplify some part. 2016-10-20 09:37:28 +02:00
Alexandre Duret-Lutz
57a055b656 [buddy] typo in comment
* src/bddop.c (bdd_implies): Fix documentation.
2016-10-20 09:37:24 +02:00
Alexandre Duret-Lutz
56f768f5a6 remove_fin: improve behavior on unclean acceptance
Related to #188.  This is a third fix that independently
makes `'utfilt --is-unambiguous -q smaller.hoa' instantaneous.

* spot/twaalgos/remfin.cc: Clean the received automaton if
necessary.
* bin/autfilt.cc: No need to call cleanup_acceptance_here() before
remove_fin() anymore.
* tests/core/remfin.test: Add an additional test.
* NEWS: Mention the change.
2016-10-19 11:00:15 +02:00
Alexandre Duret-Lutz
3dc084c4f6 use mask_keep_accessible_states
* bin/autfilt.cc, spot/twaalgos/isweakscc.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sccinfo.cc: Use mask_keep_accessible_states instead of
mask_keep_states.
2016-10-19 10:51:38 +02:00
Alexandre Duret-Lutz
4c1147e497 [buddy] speedup bdd_init and bdd_noderesize
* src/kernel.c: The initialization code of the BDD cache was
awfully slow due to multiple references to global variables.
2016-10-19 10:51:38 +02:00
Alexandre Duret-Lutz
ad478bd31a sccinfo: improve detection of rejecting 1-self-loop SCCs
As observed in #188, the smaller.hoa automaton is made only of
1-state/1-self-loop SCCs, for which calling remove_fin is a complete
waste of time.  This patch alone (i.e., without the other changes
suggested by #188) improves the run time of

% autofilt -q --is-unambiguous smaller.hoa

from 38s to 0.05s.

* spot/twaalgos/sccinfo.cc: If a single-state SCC has undeterminate SCC
and only one self-loop, then it is necessarily rejecting.
* NEWS: Mention the change.
2016-10-19 10:51:38 +02:00
Alexandre Duret-Lutz
5384a3b89a is_unambiguous: rewrite more efficiently
Avoid calling scc_info::determine_unknown_acceptance on the product, as
suggested in #188.

* spot/twaalgos/isunamb.cc (is_unambiguous): Rewrite.
* tests/core/unambig.test: Add the automaton from #188.
* NEWS: Mention the improved function.
* spot/twaalgos/mask.cc,
spot/twaalgos/mask.hh (mask_keep_accessible_states): New function.
2016-10-19 10:51:38 +02:00
Alexandre Duret-Lutz
9b3451c52e * NEWS: Typo, reported by Alexandre Gbaguidi Aïsse. 2016-10-17 11:43:19 +02:00
Alexandre Duret-Lutz
de665ce28f * configure.ac, NEWS: Bump version to 2.1.2.dev. 2016-10-14 17:30:07 +02:00
Alexandre Duret-Lutz
b0c60e799a Release Spot 2.1.2
* NEWS, configure.ac, doc/org/setup.org: Bump version.
2016-10-14 17:18:23 +02:00
Alexandre Duret-Lutz
497710ecc2 dtgbasat: rename all.log into all.csv
In order to match the tarballs of the FORTE'14 paper.

* bench/dtgbasat/stats.sh, bench/dtgbasat/README: Here.
2016-10-14 16:05:35 +02:00
Alexandre Duret-Lutz
70fa739fd1 dot: improve option initialization
* spot/twaalgos/dot.cc: Rearrange options to speed up their
initialization and avoid an "uninitialized read" error from valgrind
when compiling with clang-3.9.  The uninitialized read is still a bit
misterious to me; valgrind was complaining about opt_shape_ who is
actually initialized in the code.  However looking into the assembly
code generated revealed that all consecutive 0/false values were
initialized together, so this patch reorganize the options to encourage
that.  Also the palette was copied over for each call to print_dot(), so
this is now declared statically.
2016-10-14 14:05:23 +02:00
Alexandre Duret-Lutz
48655c6875 complete Alexandre's patch
* bench/dtgbasat/formulas: Typo.
* NEWS: Mention the fix.
* AUTHORS: Add Alexandre.
2016-10-13 15:55:25 +02:00
Alexandre GBAGUIDI AISSE
ba4345a42b dtgbasat: Fix dtgbasat bench errors
* bench/dtgbasat/formulas: Fix bin's path.
* bench/dtgbasat/prepare.sh: Fix bin's path & ltl2tgba@-sD option.
* bench/dtgbasat/stats.sh: Fix bin's path.
* bench/dtgbasat/stat.sh: Fix bin's path, ltl2tgba@-sD option
2016-10-13 15:51:21 +02:00
Alexandre Duret-Lutz
3b5fa22a3b ltlcross: add option --strength and --ambiguous
Suggested by František Blahoudek.

* bin/ltlcross.cc: Implement the two options.
* doc/org/ltlcross.org, NEWS: Document them.
* tests/core/complementation.test: Adjust test case.
* tests/core/ltlcross3.test, tests/core/unambig.test: More tests.
2016-10-13 15:41:49 +02:00
Alexandre Duret-Lutz
cc1191cd66 ltlcross: fix --verbose --no-check crash
Report from František Blahoudek.

* bin/ltlcross.cc: Do not display stats for automata
that do not exist.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the fix.
2016-10-13 13:53:42 +02:00
Alexandre Duret-Lutz
ad502eb324 * doc/org/citing.org: Update references. 2016-10-13 12:04:54 +02:00
Alexandre Duret-Lutz
062643cc88 * doc/org/tut51.org: Typos. 2016-10-12 10:53:03 +02:00
Etienne Renault
8a8fcf2ac1 spot.ltsmin: fix errors on Darwin
* NEWS, python/spot/ltsmin.i: here.
2016-10-10 20:11:40 +02:00
Alexandre Duret-Lutz
a2575e0d3e org: really hide the plantuml logo
Fix a5d6aa2.

* doc/org/.dir-locals.el.in, doc/org/init.el.in: Use
-Djava.awt.headless=true, not -Djava.awt.headless.
2016-10-10 15:40:19 +02:00
Alexandre Duret-Lutz
ed45be98ea * spot/misc/common.hh (SPOT_FALLTHROUGH): Work around Clang 3.5. 2016-10-10 14:39:44 +02:00
Alexandre Duret-Lutz
7ff50d8913 configure: enable -Wimplicit-fallthrough
* m4/gccwarn.m4: Here.
2016-10-07 21:29:34 +02:00
Alexandre Duret-Lutz
a5d6aa2533 introduce SPOT_FALLTHROUGH to cope with -Wimplicit-fallthrough
* NEWS: Mention the fix.
* HACKING: Mention the new macro.
* spot/misc/common.hh (SPOT_FALLTHROUGH): Add the macro.
* bin/randltl.cc, spot/misc/escape.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.hh, spot/tl/snf.cc, spot/twa/acc.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/sepsets.cc, spot/twaalgos/translate.cc: Use it.
2016-10-07 21:29:34 +02:00
Alexandre Duret-Lutz
fa80571d44 org: avoid displaying the plantuml log during builds
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Make sure plantuml is
started via "java -Djava.awt.headless".
2016-10-07 15:29:41 +02:00
Alexandre Duret-Lutz
9ccdd8c618 genltl: add some formulas from Tabakov & Vardi (RV'10)
* bin/genltl.cc: Implement the families.
* NEWS, bin/man/genltl.x: Document them.
* tests/core/genltl.test: Add a test.
2016-10-03 17:41:14 +02:00
Alexandre Duret-Lutz
e2b4d38ade more file to ignore
* bin/.gitignore, doc/org/.gitignore: Here.
2016-10-03 16:15:35 +02:00
Alexandre Duret-Lutz
959e757a22 org: cleanup some temporary
* doc/org/concepts.org: Here.
2016-10-03 15:27:09 +02:00
Alexandre Duret-Lutz
0c9c4be4ae bin: workaround flushing issues
* bin/common_cout.cc (check_cout): Force a flush of cout if more than
20ms has elapsed since the last explicit flush.
* bin/common_setup.cc (setup): Untie cin and cout if the input
is not a TTY, so that cout is flush less often.
* NEWS: Mention the change.
2016-10-03 15:27:06 +02:00
Alexandre Duret-Lutz
0678d1a662 change the version from 2.1.1a to 2.1.1.dev for Debian
Fixes #186.

* configure.ac, NEWS: Update version.
2016-09-23 15:04:41 +02:00
Alexandre Duret-Lutz
6528d75339 simplify: rewrite GF(a & GFb) as G(Fa & Fb)
Fixes #185.

* spot/tl/simplify.cc: Implement the new rule.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/reduccmp.test: Test it.
2016-09-22 17:37:55 +02:00
Alexandre Duret-Lutz
01d84c4d52 formula: fix valgrind error in is_Kleene_star() with clang++
* spot/tl/formula.hh, spot/tl/formula.cc: Rework the
initialization of fnode.
* NEWS: Mention the bug.
2016-09-22 17:36:43 +02:00
Alexandre Duret-Lutz
633906e347 * bench/dtgbasat/README: Update references. 2016-09-21 13:56:48 +02:00
Alexandre Duret-Lutz
5558bcf05a * NEWS, configure.ac: bump version number 2016-09-20 11:52:35 +02:00
Alexandre Duret-Lutz
fd6614181b Release Spot 2.1.1
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
2016-09-20 08:54:56 +02:00
Alexandre Duret-Lutz
d618495440 * doc/org/citing.org: Add LNCS number. 2016-09-19 21:50:13 +02:00
Alexandre Duret-Lutz
90214d7c39 genltl: fix typo in --help
Reported by František Blahoudek.

* bin/genltl.cc: Here.
* NEWS: Mention it, and the typos previously fixed in spot-x.7.
2016-09-15 15:36:53 +02:00