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

14 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
8e9002947e ltlcheck: do not ignore ^C during sanity checks 
* src/bin/ltlcheck.cc (sig_handler): Exit when receiving the signal.
 2012-10-14 18:27:50 +02:00
Alexandre Duret-Lutz
7b6337f456 ltlcheck: Add a man page. 
* src/bin/man/ltlcheck.x: New file.
* src/bin/man/Makefile.am: Add it.
* src/bin/ltlcheck.cc: Arrange help text.
 2012-10-14 17:42:25 +02:00
Alexandre Duret-Lutz
b2de0136b2 Add a has_lbt_atomic_props() method to LTL formulas. 
* src/ltlast/formula.hh (has_lbt_atomic_props): New method.
* src/ltlast/formula.cc (printprops): Display it.
* src/ltlast/atomic_prop.cc: Update it.
* src/bin/ltlcheck.cc, src/bin/genltl.cc: Use it.
* doc/tl/tl.tex: Menton has_lbt_atomic_props().
 2012-10-14 17:42:25 +02:00
Alexandre Duret-Lutz
f40925f67b ltlcheck: disable timeout handling when kill() or alarm() are missing 
* configure.ac: Check for kill and alarm.
* src/bin/ltlcheck.cc: Disable timeout code when kill or alarm are
missing.  Recognize the --timeout option, but display a warning.
 2012-10-14 17:42:25 +02:00
Alexandre Duret-Lutz
e46ae2799f ltlcheck: use kill instead of killpg 
kill(-x,y) is more portable than killpg(x,y)

* src/bin/ltlcheck.cc: Use kill.
 2012-10-14 09:12:06 +02:00
Alexandre Duret-Lutz
6167526548 * src/bin/ltlcheck.cc: Fix exit status and error reporting. 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
d0a04f9410 ltlcheck: Add a timeout option. 
* src/bin/ltlcheck.cc: Add option -T and machinery for signal handling.
 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
82babb9d38 ltlcheck: Record translation time. 
* lib/gethrxtime.h, lib/xtime.h: Add extern "C".
* src/bin/Makefile.am (ltlcheck_LDADD): Use LIB_GETHRXTIME.
* src/bin/ltlcheck.cc: Use gethrxtime() to record translation time.
 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
d7e8684d38 * src/bin/ltlcheck.cc: Improve example in --help. 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
122d34cce4 * src/bin/ltlcheck.cc: Compute statistics and print them in JSON. 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
e99fdfb650 Pick the most readable format available for displaying formulas. 
* src/bin/ltlcheck.cc (translator_runner::formula): New function.
(processor::process_formula): Use it.
 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
f6dc6412d3 Use the spot::formater class in ltlcheck to format output commands. 
* src/misc/formater.hh (printable_value): Add more accessors.
* src/bin/ltlcheck.cc: Use the formater class to factor the %-expansion
loop, and reuse filenames (such as %F, %S, and %L) between executions
on the same formula.
 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
62af20d39f * src/bin/ltlcheck.cc: Add support for LBTT's output as %T. 2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
df743e5057 Preliminary implementation of an LBTT clone. 
* src/bin/ltlcheck.cc: New file.
* src/bin/Makefile.am: Add it.
 2012-10-13 13:36:39 +02:00