From f3ef9de0be34e1eb1c67e7a7148e6f7ddd140e47 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 21 Oct 2012 13:23:02 +0200 Subject: [PATCH] rename ltlcheck as ltlcross * src/bin/ltlcheck.cc, src/bin/man/ltlcheck.x, src/tgbatest/ltlcheck.test, src/tgbatest/ltlcheck2.test: Rename as ... * src/bin/ltlcross.cc, src/bin/man/ltlcross.x, src/tgbatest/ltlcross.test, src/tgbatest/ltlcross2.test: ... these. * NEWS, src/bin/Makefile.am, src/bin/man/Makefile.am, src/tgbatest/Makefile.am: Adjust. --- NEWS | 2 +- src/bin/Makefile.am | 6 +++--- src/bin/{ltlcheck.cc => ltlcross.cc} | 4 ++-- src/bin/man/Makefile.am | 6 +++--- src/bin/man/{ltlcheck.x => ltlcross.x} | 15 ++++++++------- src/tgbatest/Makefile.am | 4 ++-- src/tgbatest/{ltlcheck.test => ltlcross.test} | 2 +- src/tgbatest/{ltlcheck2.test => ltlcross2.test} | 2 +- 8 files changed, 21 insertions(+), 20 deletions(-) rename src/bin/{ltlcheck.cc => ltlcross.cc} (99%) rename src/bin/man/{ltlcheck.x => ltlcross.x} (79%) rename src/tgbatest/{ltlcheck.test => ltlcross.test} (98%) rename src/tgbatest/{ltlcheck2.test => ltlcross2.test} (98%) diff --git a/NEWS b/NEWS index 8d53f9ce9..d91b6925c 100644 --- a/NEWS +++ b/NEWS @@ -33,7 +33,7 @@ New in spot 0.9.2a: - ltl2tgta: Translate LTL/PSL formulas into Testing Automata. - - ltlcheck: Compare the output of translators from LTL/PSL to + - ltlcross: Compare the output of translators from LTL/PSL to Büchi automata, to find bug or for benchmarking. This is essentially a Spot-based reimplementation of LBTT that supports PSL in addition to LTL, and that can diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 9b48207a6..fdb1a5027 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -42,11 +42,11 @@ libcommon_a_SOURCES = \ common_setup.hh \ common_sys.hh -bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcheck +bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross ltlfilt_SOURCES = ltlfilt.cc genltl_SOURCES = genltl.cc randltl_SOURCES = randltl.cc ltl2tgba_SOURCES = ltl2tgba.cc ltl2tgta_SOURCES = ltl2tgta.cc -ltlcheck_SOURCES = ltlcheck.cc -ltlcheck_LDADD = $(LDADD) $(LIB_GETHRXTIME) +ltlcross_SOURCES = ltlcross.cc +ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcross.cc similarity index 99% rename from src/bin/ltlcheck.cc rename to src/bin/ltlcross.cc index 3376bf304..08c7f9855 100644 --- a/src/bin/ltlcheck.cc +++ b/src/bin/ltlcross.cc @@ -70,7 +70,7 @@ Exit status:\n\ 0 everything went fine (timeouts are OK too)\n\ 1 some translator failed to output something we understand, or failed\n\ sanity checks (statistics were output nonetheless)\n\ - 2 ltlcheck aborted on error\n\ + 2 ltlcross aborted on error\n\ "; @@ -104,7 +104,7 @@ static const argp_option options[] = "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " "relabeled automatically.", 0 }, /**************************************************/ - { 0, 0, 0, 0, "ltlcheck behavior:", 4 }, + { 0, 0, 0, 0, "ltlcross behavior:", 4 }, { "allow-dups", OPT_DUPS, 0, 0, "translate duplicate formulas in input", 0 }, { "no-checks", OPT_NOCHECKS, 0, 0, diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index 9fa95657c..300ea97f3 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -26,7 +26,7 @@ dist_man1_MANS = \ genltl.1 \ ltl2tgba.1 \ ltl2tgta.1 \ - ltlcheck.1 \ + ltlcross.1 \ ltlfilt.1 \ randltl.1 @@ -39,8 +39,8 @@ ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc ltl2tgta.1: $(common_dep) $(srcdir)/ltl2tgta.x $(srcdir)/../ltl2tgta.cc $(convman) ../ltl2tgta$(EXEEXT) $(srcdir)/ltl2tgta.x $@ -ltlcheck.1: $(common_dep) $(srcdir)/ltlcheck.x $(srcdir)/../ltlcheck.cc - $(convman) ../ltlcheck$(EXEEXT) $(srcdir)/ltlcheck.x $@ +ltlcross.1: $(common_dep) $(srcdir)/ltlcross.x $(srcdir)/../ltlcross.cc + $(convman) ../ltlcross$(EXEEXT) $(srcdir)/ltlcross.x $@ ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ diff --git a/src/bin/man/ltlcheck.x b/src/bin/man/ltlcross.x similarity index 79% rename from src/bin/man/ltlcheck.x rename to src/bin/man/ltlcross.x index e4e5fba9d..4e56c9541 100644 --- a/src/bin/man/ltlcheck.x +++ b/src/bin/man/ltlcross.x @@ -1,4 +1,5 @@ -[NAME] ltlcheck \- translate LTL/PSL formulas into Büchi automata +[NAME] +ltlcross \- cross-compare LTL/PSL translators to Büchi automata [DESCRIPTION] .\" Add any additional description here [EXAMPLES] @@ -10,7 +11,7 @@ written to \f(CWresults.json\fR. .nf % randltl \-n100 \-\-tree\-size=20..30 a b c | \e -ltlcheck \-T120 'ltl2tgba \-s %f >%N' 'spin \-f %s >%N' \-\-json=results.json +ltlcross \-T120 'ltl2tgba \-s %f >%N' 'spin \-f %s >%N' \-\-json=results.json .fi .LP @@ -22,16 +23,16 @@ in LBT's format, and \f(CW%T\fR to read the output in LBTT's format (which is a superset of the format output by LBT). .nf -% ltlcheck \-F input.ltl \-\-csv=results.csv \e +% ltlcross \-F input.ltl \-\-csv=results.csv \e 'lbt <%L >%T' \e 'ltl3ba \-f %s >%N' \e 'ltl2tgba \-\-lbtt %f >%T' .fi .LP -If you use ltlcheck in an automated testsuite just to check for +If you use ltlcross in an automated testsuite just to check for potential problems, avoid the \fB\-\-csv\fR and \fB\-\-json\fR -options: ltlcheck is faster when it does not have to compute these +options: ltlcross is faster when it does not have to compute these statistics. [SEE ALSO] @@ -41,13 +42,13 @@ statistics. .BR ltl2tgba (1) [BIBLIOGRAPHY] -ltlcheck is a Spot-based reimplementation of a tool called LBTT. LBTT +ltlcross is a Spot-based reimplementation of a tool called LBTT. LBTT was developped by Heikki Tauriainen at the Helsinki University of Technology. The main motivation for the reimplementation was to support PSL, and output more statistics about the translations. The sanity checks performed on the result of each translator (by -either LBTT or ltlcheck) are described in the following paper. Our +either LBTT or ltlcross) are described in the following paper. Our implementation will detect and reports problems (like inconsistencies between two translations) but unlike LBTT it does not offer an interactive mode to investigate such problems. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index c2a926e3e..2b122e3a3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -107,9 +107,9 @@ TESTS = \ emptchkr.test \ ltlcounter.test \ spotlbtt.test \ - ltlcheck.test \ + ltlcross.test \ spotlbtt2.test \ - ltlcheck2.test \ + ltlcross2.test \ complementation.test \ randpsl.test \ cycles.test diff --git a/src/tgbatest/ltlcheck.test b/src/tgbatest/ltlcross.test similarity index 98% rename from src/tgbatest/ltlcheck.test rename to src/tgbatest/ltlcross.test index 9debe2f8f..223686d64 100755 --- a/src/tgbatest/ltlcheck.test +++ b/src/tgbatest/ltlcross.test @@ -23,7 +23,7 @@ ltl2tgba=../ltl2tgba ../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | -../../bin/ltlcheck \ +../../bin/ltlcross \ "$ltl2tgba -t -l %f > %T" \ "$ltl2tgba -t -l -R3b -r4 %f > %T" \ "$ltl2tgba -t -f %f > %T" \ diff --git a/src/tgbatest/ltlcheck2.test b/src/tgbatest/ltlcross2.test similarity index 98% rename from src/tgbatest/ltlcheck2.test rename to src/tgbatest/ltlcross2.test index 263d813e2..a9c8ab109 100755 --- a/src/tgbatest/ltlcheck2.test +++ b/src/tgbatest/ltlcross2.test @@ -23,7 +23,7 @@ ltl2tgba=../../bin/ltl2tgba ../../bin/randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | -../../bin/ltlcheck \ +../../bin/ltlcross \ "$ltl2tgba --lbtt --any --small %f > %T" \ "$ltl2tgba --lbtt --any --medium %f > %T" \ "$ltl2tgba --lbtt --any --high %f > %T" \