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

2138 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
b31ddb787d * src/bin/man/Makefile.am (common_dep): Fix dependency. 2013-01-23 14:59:20 +01:00
Alexandre Duret-Lutz
3f61a34bd1 * src/tgbatest/ltlcross2.test: Fix list of tested configurations. 2013-01-22 11:55:03 +01:00
Alexandre Duret-Lutz
362c396356 * src/tgbaalgos/postproc.cc (count_states): Speed up explicit case. 2013-01-21 19:34:41 +01:00
Alexandre Duret-Lutz
76988369dc * src/tgbaalgos/minimize.hh: Fix documentation. 2013-01-21 16:04:20 +01:00
Alexandre Duret-Lutz
5e10057cfc cycles: fix documentation. 
* src/tgbaalgos/cycles.hh: Fix comments.
 2013-01-21 10:58:01 +01:00
Alexandre Duret-Lutz
6a547371d7 ltlcross: diagnose missing i/o specifications earlier. 
* src/misc/formater.cc, src/misc/formater.hh (scan): New method.
(prime): Use it.
* src/bin/ltlcross.cc (translator_runner::translator_runner): Scan each
specification string, and report those missing an input or output
%-sequence.
* NEWS: Mention it.
 2013-01-21 10:20:25 +01:00
Alexandre Duret-Lutz
edd687a301 ltlparse: Add compatibility with ltl2dsar's input. 
* src/ltlparse/ltlscan.ll: Accept as a proposition any
alphanumeric string that is not an operator.
* NEWS: Mention it.
* src/ltltest/lbt.test: New file.  Also tests previous patch.
* src/ltltest/Makefile.am: Add it.
 2013-01-20 03:01:44 +01:00
Alexandre Duret-Lutz
3a5eec42de lbt: Do not write a trailing space. 
* NEWS: Mention it.
* src/ltlvisit/lbt.cc: Instead of outputting a space after each
node, output one before each node but the first one.
 2013-01-20 03:01:44 +01:00
Alexandre Duret-Lutz
bf3c3aecde tostring: quote U, W, M, R when used as atomic propositions 
* src/ltltest/tostring.test, src/ltltest/parse.test: More tests.
* src/ltlvisit/tostring.cc (is_bare_word): Quote U, W, M, R.
* NEWS: Mention it.
 2013-01-20 03:01:44 +01:00
Alexandre Duret-Lutz
5086e24165 ltlcross: Display the number of timeouts. 
* NEWS: Mention it.
* src/bin/ltlcross.cc: Always display the number of timeout
on normal termination.
 2013-01-20 03:01:44 +01:00
Alexandre Duret-Lutz
c5461335c9 ltl2tgba on-line: display edge and transition count 
* wrap/python/ajax/spot.in: Adjust display.
* NEWS: Mention it.
 2013-01-18 09:20:14 +01:00
Alexandre Duret-Lutz
b99cfa88bb Fix two dead assignments detected by clang's static analyzer. 
* src/tgbaalgos/scc.cc, src/tgbatest/ltl2tgba.cc: Remove assignments to
unread variables.
 2013-01-17 14:06:31 +01:00
Alexandre Duret-Lutz
dcd4644d42 eltl2tgba: slight cleanup of the tests. 
* src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Simplify use of
here documents, and also test for ltl2tgba's -lo option with valgrind.
 2013-01-17 14:06:31 +01:00
Alexandre Duret-Lutz
d580cce685 Fix documentation errors reported by clang++ 3.2. 
* m4/gccwarn.m4: Use -Wdocumentation if supported.
* src/ltlast/binop.hh, src/ltlparse/public.hh, src/ta/taproduct.hh,
src/taalgos/emptinessta.hh, src/taalgos/reachiter.hh,
src/tgba/state.hh, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/ltl2tgba_fm.hh: Fix Doxygen documentations errors signaled
by clang++ 3.2.
 2013-01-17 09:07:13 +01:00
Alexandre Duret-Lutz
aa7b43eadf Fix several warnings reported by clang++ 3.2. 
* src/tgba/tgbakvcomplement.cc
(tgba_kv_complement_succ_iterator::current_state_),
src/ta/taexplicit.hh (state_ta_explicit::source_):
Remove useless private member.
* src/ta/taexplicit.cc: Adjust constructors.
* src/ta/tgta.cc, src/ta/taexplicit.hh: Also fix
copyright banner.
* src/bin/ltlcross.cc (exec_with_timeout): Work
around warning about status not being set in the
error path.
 2013-01-16 08:52:27 +01:00
Alexandre Duret-Lutz
361f594655 Test previous patch. 
* iface/dve2/finite.test: Add test case.
* NEWS: Mention the fix.
 2013-01-14 18:26:04 +01:00
Pierre PARUTTO
67b7b86d52 tgbaproduct: fix segfault 
* src/tgba/tgbaproduct.cc (transition_annotation): Adapt down cast to
new hierarchy.
 2013-01-14 18:24:24 +01:00
Alexandre Duret-Lutz
e4ecc2d465 simplify: add four simplification rules for GF and FG 
GF(a|Xb) = GF(a|b)      GF(a|Fb) = GF(a|b)
FG(a&Xb) = FG(a&b)      FG(a&Gb) = FG(a&b)

* src/ltlvisit/simplify.cc: Implement them.
* NEWS, doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Test then.
 2013-01-11 17:16:17 +01:00
Alexandre Duret-Lutz
2580fc6f91 * src/tgbatest/babiak.test: Rewrite using ltlcross. 2013-01-10 18:42:36 +01:00
Alexandre Duret-Lutz
081aa0d120 tgbatest: Rewrite ltl2neverclaim using ltlcross. 
* src/tgbatest/ltl2neverclaim.test: Rename as...
* src/tgbatest/ltl2neverclaim-lbtt.test: ... this.
* src/tgbatest/ltl2neverclaim.test: New version, using ltlcross.
* src/tgbatest/Makefile.am: Add ltl2neverclaim-lbtt.test.
 2013-01-10 18:22:35 +01:00
Alexandre Duret-Lutz
0e74b76521 Work around Debian's patched libtool. 
* configure.ac: Set link_all_deplibs to yes.
 2013-01-10 16:45:54 +01:00
Alexandre Duret-Lutz
c55f282298 * src/bin/common_setup.cc: Bump copyright year. 2013-01-06 21:44:38 +01:00
Alexandre Duret-Lutz
86558f1a5c Add missing copyright notice. 
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/sum.py: Add copyright
notice.
 2013-01-06 21:44:15 +01:00
Alexandre Duret-Lutz
d02376aaa2 * NEWS: Update with recent changes. 2013-01-06 19:55:10 +01:00
Alexandre Duret-Lutz
254896d5d8 Remove anything related to evtgba. 
* src/evtgba/, src/evtgbaalgos/, src/evtgbaparse/, src/evtgbatest/:
Delete.
* src/Makefile.am (SUBDIRS): Adjust.
* configure.ac, README: Adujst.
 2013-01-06 19:26:32 +01:00
Alexandre Duret-Lutz
16c7bc1975 bench: delete useless defs.in files. 
* bench/wdba/defs.in, bench/ltlclasses/defs.in,
bench/ltlcounter/defs.in: Delete.
* bench/wdba/run, bench/ltlclasses/run, bench/ltlcounter/run: Adjust not
to use them.
* configure.ac: Do not output the associated defs files.
 2013-01-06 19:13:18 +01:00
Alexandre Duret-Lutz
885a535184 Rewrite the ltl2tgba bench using ltlcross 
* bench/ltl2tgba/sum.py: New file.
* bench/ltl2tgba/.gitignore, bench/ltl2tgba/Makefile.am,
bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big,
bench/ltl2tgba/defs.in, bench/ltl2tgba/known, bench/ltl2tgba/small:
Rewrite this benchmark completely.  Also drop support of Wring and
Modella, as we cannot get them to work reliably.
* bench/ltl2tgba/formulae.ltl: Rewrite in Spot's syntax.
* bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
bench/ltl2tgba/parseout.pl: Delete these scripts, no
longer needed.
* configure.ac: Do not output ltl2baw.pl anymore.
 2013-01-06 18:57:50 +01:00
Alexandre Duret-Lutz
e2f17f65b8 Remove LBTT. 
* configure.ac: Detect lbtt using AC_CHECK_PROG.
* m4/lbtt.m4: Delete.
* lbtt/: Remove directory.
* Makefile.am, README: Adjust.
 2012-12-28 10:05:12 +01:00
Alexandre Duret-Lutz
a577850eb3 Address several issues reported by cppcheck all over the place. 
* src/bin/common_finput.cc, src/tgbaalgos/lbtt.cc: Use !empty() instead
of size() > 0.
* src/bin/ltl2tgta.cc, src/kripke/kripkeexplicit.cc,
src/tgbatest/complementation.cc: Avoid useless assignments.
* src/bin/ltlcross.cc: Correct mistaken assignment inside assert().
* src/evtgba/symbol.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh,
src/tgba/tgbasafracomplement.cc (operator=): Do not return a const
reference.
* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/product.cc,
src/evtgbatest/product.cc: Check indices before using them, not after.
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/tgbatest/randtgba.cc: Pass constant strings by reference.
* src/kripke/kripkeprint.cc, src/tgbaalgos/simulation.cc:
Remove a useless operation.
* src/ltlvisit/simplify.cc: Remove a duplicate condition.
* src/misc/formater.hh: Remove unused attribute.
* src/misc/modgray.cc: Initialize done_ in the constructor.
* src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh (operator=): Fix prototype.
* src/saba/sabacomplementtgba.cc: Remove unused default constructor.
* src/ta/taexplicit.cc, src/ta/taproduct.cc, src/ta/tgtaproduct.cc,
src/ta/tgtaproduct.hh, src/taalgos/emptinessta.cc,
src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
src/taalgos/tgba2ta.cc, src/tgbaalgos/cutscc.cc: Use C++ casts, and
++it instead of it++.
* src/taalgos/dotty.cc, src/tgbatest/ltl2tgba.cc: Refine the scope of
variables.
* src/tgba/tgbakvcomplement.hh (bdd_order): Always initialize bdd_.
* src/tgba/tgbasgba.cc, src/tgba/wdbacomp.cc: Use the initialization
line to initialize all members.
 2012-12-24 13:14:33 +01:00
Alexandre Duret-Lutz
a3b49f1108 acccompl: Speed up. 
* src/misc/acccompl.cc: Simplify both directions of the conversion.
* src/misc/acccompl.hh: Pass bdds by reference.
 2012-12-24 13:14:33 +01:00
Alexandre Duret-Lutz
ce21af6323 * .dir-locals.el: Fix whitespace-mode configuration. 2012-12-24 13:14:33 +01:00
Alexandre Duret-Lutz
15c9b72f13 [buddy] 
* src/bdd.h: Make all inplace operators return a reference.
 2012-12-24 13:14:23 +01:00
Alexandre Duret-Lutz
13c41ee773 ltlast: use the return of insert() to avoid a double lookup 
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc: Do not look for a key
and then insert the (key,value) on failure.  Simply insert
(key,0), and replace 0 by value on failure.  This replaces two map
lookups by one.
 2012-12-19 22:30:49 +01:00
Alexandre Duret-Lutz
2776de87da More documentation. 
* README: Introduce Spot, and point to the documentation.
* wrap/python/ajax/README: Mention ltl3ba 1.0.2.
 2012-12-19 15:36:56 +01:00
Alexandre Duret-Lutz
aa2374c5a2 Cosmetics. 
* src/sanity/style.test: Catch extra space around operator declarations.
* src/ltlast/automatop.hh, src/ltlast/multop.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgbaalgos/simulation.cc: Fix them.
 2012-12-19 15:23:29 +01:00
Alexandre Duret-Lutz
cffbb7b498 Remove useless variable. 
* src/tgba/tgbaexplicit.hh (add_state): Remove useless variable.
Reported by Étienne Renault.
 2012-12-14 11:22:18 +01:00
Alexandre Duret-Lutz
b3d8b0198f x-to-1: Honor $PERL 
* tools/x-to-1.in: Run $HELP2MAN via $PERL so that the user gets a
chance to use his preferred version of Perl.  This is typically
required by Darwin users whose default /usr/bin/perl do not have all
the libraries required by help2man, and who need to use their MacPorts
installation of Perl instead.
 2012-12-14 11:22:08 +01:00
Alexandre Duret-Lutz
41265cd94f * NEWS: Document recent bug fixes. 2012-11-28 17:53:43 +01:00
Alexandre Duret-Lutz
64484e7816 Print F"proc.st" as Fproc.st. 
* src/ltlvisit/tostring.cc: Allow '.' in bare words while
printing atomic propositions.
* src/ltltest/bare.test: New file.
* src/ltltest/Makefile.am: Add it.
 2012-11-28 17:34:39 +01:00
Alexandre Duret-Lutz
af639e58c7 more files to ignore 2012-11-28 16:45:04 +01:00
Alexandre Duret-Lutz
5efb66cb25 Add a .dir-locals.el file. 
* .dir-locals.el: New file.
* Makefile.am (EXTRA_DIST): Distribute it.
 2012-11-27 15:19:20 +01:00
Thomas Badie
d10e772d35 Fix non determinism in the simulation. 
* src/tgbaalgos/simulation.cc: Fix non determinism.
* src/tgbatest/simdet.test: Test that the behavior is now correct.
* src/tgbatest/Makefile.am (TESTS): Add the new test to the
test-suite.
 2012-11-14 18:22:11 +01:00
Alexandre Duret-Lutz
49d384b1eb ltlcross: diagnose failure to write into temporary files 
The removes a warning about the return code from write() being
ignored.  Reported by Thomas Badie.

* src/bin/ltlcross.cc (string_to_tmp): Call error() on error.
 2012-11-14 15:12:43 +01:00
Alexandre Duret-Lutz
973c5bc050 * NEWS, configure.ac: Bump version to 1.0a 2012-10-27 12:11:59 +02:00
Alexandre Duret-Lutz
213b67e84b Release Spot 1.0. 
* NEWS, configure.ac: Bump version to 1.0.
 2012-10-27 11:58:55 +02:00
Alexandre Duret-Lutz
f9373e4a9f * m4/ax_prefix_config_h.m4: Update to more recent version. 2012-10-26 09:47:51 +02:00
Alexandre Duret-Lutz
e2ed5f6b98 * NEWS: rephrase some items 2012-10-26 07:56:47 +02:00
Alexandre Duret-Lutz
301ad1ebf0 Speed-up translation of persistence formulas. 
* src/tgbaalgos/ltl2tgba_fm.cc: Use a single acceptance for syntactic
persistence formulas.
 2012-10-26 07:46:04 +02:00
Alexandre Duret-Lutz
7c464246f2 * src/tgbaalgos/ltl2tgba_fm.cc: Typo in comment. 2012-10-24 10:16:19 +02:00
Alexandre Duret-Lutz
d552be308b ltlcross: Add a --stop-on-error option. 
* src/bin/ltlcross.cc: Add the option.
* src/bin/common_finput.hh, src/bin/common_finput.cc: Make it possible
to abort run().
 2012-10-23 23:21:14 +02:00