diff --git a/Makefile.am b/Makefile.am index ff39947bb..0d40a33aa 100644 --- a/Makefile.am +++ b/Makefile.am @@ -58,8 +58,9 @@ debian/changelog: configure.ac ACLOCAL_AMFLAGS = -I m4 EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog \ - tools/help2man tools/test-driver-teamcity $(UTF8) \ - $(DEBIAN) m4/gnulib-cache.m4 .dir-locals.el + tools/help2man tools/man2html.pl \ + tools/test-driver-teamcity $(UTF8) $(DEBIAN) \ + m4/gnulib-cache.m4 .dir-locals.el dist-hook: gen-ChangeLog diff --git a/NEWS b/NEWS index a1e490d56..8740c008e 100644 --- a/NEWS +++ b/NEWS @@ -5,11 +5,14 @@ New in spot 1.99.2a (not yet released) * Bugs fixed - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) - where not detected as generalized-Rabin. + were not detected as generalized-Rabin. - Unknown arguments for print_hoa() (i.e., option -H in command-line tools) are now diagnosed. - - the CGI script for LTL translation now force transition-based - acceptance on WDBA-minimized automata when TGBA is requested + - The CGI script for LTL translation now force transition-based + acceptance on WDBA-minimized automata when TGBA is requested. + - ltlgrind --help output had some options documented twice, or + in the wrong place. + - The man page for ltlcross had obsolete examples. New in spot 1.99.2 (2015-07-18) diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index cf58a67ba..14c3d66c9 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -114,7 +114,7 @@ static const argp_option options[] = { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL, "relabel Boolean subexpressions, alphabetically unless " \ "specified otherwise", 0 }, - { "define", OPT_DEFINE, "[FILENAME]", OPTION_ARG_OPTIONAL, + { "define", OPT_DEFINE, "FILENAME", OPTION_ARG_OPTIONAL, "when used with --relabel or --relabel-bool, output the relabeling map " "using #define statements", 0 }, { "remove-wm", OPT_REMOVE_WM, 0, 0, diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index ba1153078..231b437db 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -55,9 +55,6 @@ static const char * argp_program_doc = "List formulas that are similar to but simpler than a given formula."; static const argp_option options[] = { - {"mutations", 'm', "NUM", 0, "number of mutations to apply to the " \ - "formulae (default: 1)", -1}, - {"sort", OPT_SORT, 0, 0, "sort the result by formula size", 0}, {0, 0, 0, 0, "Mutation rules (all enabled unless those options are used):", 15}, {"ap-to-const", OPT_AP2CONST, 0, 0, @@ -83,6 +80,9 @@ static const argp_option options[] = { "0 or max to unbounded", 15}, {0, 0, 0, 0, "Output options:", 20}, {"max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20}, + {"mutations", 'm', "NUM", 0, "number of mutations to apply to the " \ + "formulae (default: 1)", 0}, + {"sort", OPT_SORT, 0, 0, "sort the result by formula size", 0}, {0, 0, 0, 0, "Miscellaneous options:", -1}, {0, 0, 0, 0, 0, 0} }; @@ -171,7 +171,7 @@ main(int argc, char* argv[]) const argp ap = { options, parse_opt, 0, argp_program_doc, children, 0, 0 }; - if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) exit(err); mut_opts |= opt_all; diff --git a/src/bin/man/autfilt.x b/src/bin/man/autfilt.x index 159fb5b6e..593dd3878 100644 --- a/src/bin/man/autfilt.x +++ b/src/bin/man/autfilt.x @@ -4,3 +4,4 @@ autfilt \- filter, convert, and transform Büchi automata .\" Add any additional description here [SEE ALSO] .BR spot-x (7) +.BR dstar2tgba (1) diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x index 1198b6e94..e1dbce322 100644 --- a/src/bin/man/dstar2tgba.x +++ b/src/bin/man/dstar2tgba.x @@ -37,6 +37,6 @@ LNCS 8461. Explains the SAT-based minimization techniques that can be used (on request only) by dstar2tgba to minimize deterministic Büchi automata. - [SEE ALSO] -.BR spot-x (7) +.BR spot-x (7), +.BR autfilt (1) diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index a26430c7d..f8fab80e4 100644 --- a/src/bin/man/ltl2tgba.x +++ b/src/bin/man/ltl2tgba.x @@ -1,13 +1,13 @@ +.\" -*- coding: utf-8 -*- [NAME] ltl2tgba \- translate LTL/PSL formulas into Büchi automata [NOTE ON TGBA] - TGBA stands for Transition-based Generalized Büchi Automaton. The name was coined by Dimitra Giannakopoulou and Flavio Lerda in their FORTE'02 paper (From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata), although similar automata have been used under different names long before that. - +.PP As its name implies a TGBA uses a generalized Büchi acceptance condition, meanings that a run of the automaton is accepted iff it visits ininitely often multiple acceptance sets, and it also uses @@ -16,20 +16,28 @@ transitions. TGBA are often more consise than traditional Büchi automata. For instance the LTL formula \f(CWGFa & GFb\fR can be translated into a single-state TGBA while a traditional Büchi automaton would need 3 states. Compare - - % ltl2tgba 'GFa & GFb' - +.PP +.in +4n +.nf +.ft C +% ltl2tgba 'GFa & GFb' +.fi +.PP with - - % ltl2tgba --ba 'GFa & GFb' - +.PP +.in +4n +.ft C +.nf +% ltl2tgba --ba 'GFa & GFb' +.fi +.PP In the dot output produced by the above commands, the membership of the transitions to the various acceptance sets is denoted using names in braces. The actuall names do not really matter as they may be produced by the translation algorithm or altered by any latter postprocessing. - -When the \fB\--ba\fR option is used to request a Büchi automaton, Spot +.PP +When the \fB\-\-ba\fR option is used to request a Büchi automaton, Spot builds a TGBA with a single acceptance set, and in which for any state either all outgoing transitions are accepting (this is equivalent to the state being accepting) or none of them are. Double circles are @@ -38,97 +46,116 @@ denoting the accepting transitions are still shown because the underling structure really is a TGBA. [NOTE ON LBTT'S FORMAT] -The format, described at -http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html, +.UR http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html +LBTT's format +.UE has support for both transition-based and state based generalized acceptance. - +.PP Because Spot uses transition-based generalized Büchi automata internally, it will normally use the transition-based flavor of that format, indicated with a 't' flag after the number of acceptance sets. For instance: - - % ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2' - 2 2t // 2 states, 2 transition-based acceptance sets - 0 1 // state 0: initial - 0 -1 t // trans. to state 0, no acc., label: true - 1 -1 | & p0 p2 & p1 p2 // trans. to state 1, no acc., label: (p0&p2)|(p1&p2) - -1 // end of state 0 - 1 0 // state 1: not initial - 1 0 1 -1 & & p0 p1 p2 // trans. to state 1, acc. 0 and 1, label: p0&p1&p2 - 1 0 -1 & & p1 p2 ! p0 // trans. to state 1, acc. 0, label: !p0&p1&p2 - 1 1 -1 & & p0 p2 ! p1 // trans. to state 1, acc. 1, label: p0&!p1&p2 - 1 -1 & & p2 ! p0 ! p1 // trans. to state 1, no acc., label: !p0&!p1&p2 - -1 // end if state 1 - +.PP +.in +4n +.ft C +.nf +% ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2' +2 2t // 2 states, 2 transition-based acceptance sets +0 1 // state 0: initial +0 -1 t // trans. to state 0, no acc., label: true +1 -1 | & p0 p2 & p1 p2 // trans. to state 1, no acc., label: (p0&p2)|(p1&p2) +-1 // end of state 0 +1 0 // state 1: not initial +1 0 1 -1 & & p0 p1 p2 // trans. to state 1, acc. 0 and 1, label: p0&p1&p2 +1 0 -1 & & p1 p2 ! p0 // trans. to state 1, acc. 0, label: !p0&p1&p2 +1 1 -1 & & p0 p2 ! p1 // trans. to state 1, acc. 1, label: p0&!p1&p2 +1 -1 & & p2 ! p0 ! p1 // trans. to state 1, no acc., label: !p0&!p1&p2 +-1 // end if state 1 +.fi +.PP Here, the two acceptance sets are represented by the numbers 0 and 1, and they each contain two transitions (the first transition of state 1 belongs to both sets). - -When both --ba and --lbtt options are used, the state-based flavor of +.PP +When both \fB\-\-ba\fR and \fB\-\-lbtt\fR options are used, +the state-based flavor of the format is used instead. Note that the LBTT format supports generalized acceptance conditions on states, but Spot only use this format for Büchi automata, where there is always only one acceptance set. Unlike in the LBTT documentation, we do not use the -optional 's' flag to indicate the state-based acceptance, this way our -output is also compatible with that of LBT (see -http://www.tcs.hut.fi/Software/maria/tools/lbt/). - - % ltl2tgba --ba --lbtt FGp0 - 2 1 // 2 states, 1 (state-based) accepance set - 0 1 -1 // state 0: initial, non-accepting - 0 t // trans. to state 0, label: true - 1 p0 // trans. to state 1, label: p0 - -1 // end of state 0 - 1 0 0 -1 // state 1: not initial, in acceptance set 0 - 1 p0 // trans. to state 0, label: p0 - -1 // end if state 1 - +optional '\fBs\fR' flag to indicate the state-based acceptance, this way our +output is also compatible with that of +.UR http://www.tcs.hut.fi/Software/maria/tools/lbt/ +LBT +.UE . +.PP +.in +4n +.ft C +.nf +% ltl2tgba --ba --lbtt FGp0 +2 1 // 2 states, 1 (state-based) accepance set +0 1 -1 // state 0: initial, non-accepting +0 t // trans. to state 0, label: true +1 p0 // trans. to state 1, label: p0 +-1 // end of state 0 +1 0 0 -1 // state 1: not initial, in acceptance set 0 +1 p0 // trans. to state 0, label: p0 +-1 // end if state 1 +.fi +.PP You can force ltl2tgba to use the transition-based flavor of the -format even for Büchi automaton using --lbtt=t. - - % ltl2tgba --ba --lbtt=t FGp0 - 2 1t // 2 states, 1 transition-based accepance set. - 0 1 // state 0: initial - 0 -1 t // trans. to state 0, no acc., label: true - 1 -1 p0 // trans. to state 1, no acc., label: p0 - -1 // end of state 0 - 1 0 // state 1: not initial - 1 0 -1 p0 // trans. to state 1, acc. 0, label: p0 - -1 // end if state 1 - +format even for Büchi automaton using \fB\-\-lbtt=t\fR. +.PP +.in +4n +.ft C +.nf +% ltl2tgba --ba --lbtt=t FGp0 +2 1t // 2 states, 1 transition-based accepance set. +0 1 // state 0: initial +0 -1 t // trans. to state 0, no acc., label: true +1 -1 p0 // trans. to state 1, no acc., label: p0 +-1 // end of state 0 +1 0 // state 1: not initial +1 0 -1 p0 // trans. to state 1, acc. 0, label: p0 +-1 // end if state 1 +.fi +.PP When representing a Büchi automaton using transition-based acceptance, all transitions leaving accepting states are put into the acceptance set. - +.PP A final note concerns the name of the atomic propositions. The original LBTT and LBT formats require these atomic propositions to -have names such as 'p0', 'p32', ... We extend the format to accept +have names such as '\fBp0\fR', '\fBp32\fR', ... We extend the format to accept atomic proposition with arbitrary names that do not conflict with -LBT's operators (e.g. 'i' is the symbol of the implication operator so +LBT's operators (e.g. '\fBi\fR' is the symbol of the implication operator so it may not be used as an atomic proposition), or as double-quoted strings. Spot will always output atomic-proposition that do not match -p[0-9]+ as double-quoted strings. - - % bin/ltl2tgba --lbtt 'GFa & GFb' - 1 2t - 0 1 - 0 0 1 -1 & "a" "b" - 0 0 -1 & "b" ! "a" - 0 1 -1 & "a" ! "b" - 0 -1 & ! "b" ! "a" - -1 +\fBp[0-9]+\fR as double-quoted strings. +.PP +.in +4n +.ft C +.nf +% bin/ltl2tgba --lbtt 'GFa & GFb' +1 2t +0 1 +0 0 1 -1 & "a" "b" +0 0 -1 & "b" ! "a" +0 1 -1 & "a" ! "b" +0 -1 & ! "b" ! "a" +-1 +.fi [NOTE ON GENERATING MONITORS] - The monitors generated with option \fB\-M\fR are finite state automata used to reject finite words that cannot be extended to infinite words compatible with the supplied formula. The idea is that the monitor should progress alongside the system, and can only make decisions based on the finite prefix read so far. - +.PP Monitors can be seen as Büchi automata in which all recognized runs are accepting. As such, the only infinite words they can reject are those are not recognized, i.e., infinite words that start with a bad prefix. - +.PP Because of this limited expressiveness, a monitor for some given LTL or PSL formula may accept a larger language than the one specified by the formula. For instance a monitor for the LTL formula \f(CWa U b\fR @@ -136,7 +163,7 @@ will reject (for instance) any word starting with \f(CW!a&!b\fR as there is no way such a word can validate the formula, but it will not reject a finite prefix repeating only \f(CWa&!b\fR as such a prefix could be extented in a way that is comptible with \f(CWa U b\fR. - +.PP For more information about monitors, we refer the readers to the following two papers (the first paper describes the construction of the second paper in a more concise way): diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 7508d4cd8..0e59de5d9 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -1,58 +1,89 @@ +.\" -*- coding: utf-8 -*- [NAME] ltlcross \- cross-compare LTL/PSL translators to Büchi automata -[DESCRIPTION] -.\" Add any additional description here [EXAMPLES] -The following commands compare never claims produced by ltl2tgba(1) -and spin(1) and 100 random formulas, using a timeout of 2 minutes. A -trace of the execution of the two tools, including any potential issue -detected, is reported on standard error, while statistics are -written to \f(CWresults.json\fR. - +The following commands compare never claims produced by +.BR ltl2tgba (1), +.BR spin (1), +and +.B lbt +for 100 random formulas, using a timeout of 2 minutes. Because +.B ltlcross +knows those tools, there is no need to specify their input and +output. A trace of the execution of the two tools, including any +potential issue detected, is reported on standard error, while +statistics are written to \f(CWresults.json\fR. +.PP +.in +4n .nf +.ft C % randltl \-n100 \-\-tree\-size=20..30 a b c | \e -ltlcross \-T120 'ltl2tgba \-s %f >%N' 'spin \-f %s >%N' \-\-json=results.json +ltlcross \-T120 ltl2tgba spin lbt \-\-json=results.json .fi -.LP - -The next command compares lbt, ltl3ba, and ltl2tgba(1) on a set of -formulas saved in file \f(CWinput.ltl\fR. Statistics are again writen -as CSV into \f(CWresults.csv\fR. Note the use of \f(CW%L\fR to -indicate that the formula passed to lbt should be written into a file -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). - +.PP +The next command compares +.BR lbt , +.BR ltl3ba , +and +.BR ltl2tgba (1) +on a set of formulas saved in file \f(CWinput.ltl\fR. +Statistics are again writen +as CSV into \f(CWresults.csv\fR. This examples specify the +input and output for each tool, to show how this can be done. +Note the use of \f(CW%L\fR to indicate that the formula passed t +for the formula in +.BR spin (1)'s +format, and \f(CW%f\fR for the +formula in Spot's format. Each of these tool produces an +automaton in a different format (respectively, LBTT's format, +Spin's never claims, and HOA format), but Spot's parser can +distinguish and understand these three formats. +.PP +.in +4n .nf +.ft C % ltlcross \-F input.ltl \-\-csv=results.csv \e - 'lbt <%L >%T' \e - 'ltl3ba \-f %s >%N' \e - 'ltl2tgba \-\-lbtt %f >%T' + 'lbt <%L >%O' \e + 'ltl3ba \-f %s >%O' \e + 'ltl2tgba \-H %f >%O' .fi -.LP - -Rabin or Streett automata output by ltl2dstar can be read from a -file specified with \f(CW%D\fR. For instance: - +.PP +Rabin or Streett automata output by +.B ltl2dstar +can be read from a +file specified with \f(CW%D\fR instead of \f(CW%O\fR. For instance: +.PP +.in +4n .nf +.ft C % ltlcross \-F input.ltl \e - 'ltl2dstar \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e - 'ltl2dstar \-\-automata=streett \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e + 'ltl2dstar \-\-ltl2nba=spin:ltl2tgba@\-s %L %D' \e + 'ltl2dstar \-\-automata=streett \-\-ltl2nba=spin:ltl2tgba@\-s %L %D' \e .fi -.LP - -However because Spot only supports Büchi acceptance, these Rabin and +.PP +However, for historical reasons these Rabin and Streett automata are immediately converted to TGBA before further -processing by ltlcross. This is still interesting to search for bugs +processing by +.BR ltlcross . +This is still interesting to search for bugs in translators to Rabin or Streett automata, but the statistics might -not be very relevant. - +not be very relevant. If statistics matters to you and you do not want +this conversion to occur, use the HOA format to interface with ltl2dstar: +.PP +.in +4n +.nf +.ft C +% ltlcross \-F input.ltl \e + 'ltl2dstar \-\-output\-format=hoa \-\-ltl2nba=spin:ltl2tgba@\-s %L %O' \e + 'ltl2dstar \-\-output\-format=hoa \-\-automata=streett \-\-ltl2nba=spin:ltl2tgba@\-s %L %O' \e +.fi +.PP If you use ltlcross in an automated testsuite just to check for potential problems, avoid the \fB\-\-csv\fR and \fB\-\-json\fR options: ltlcross is faster when it does not have to compute these statistics. [ENVIRONMENT VARIABLES] - .TP \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR These variables control in which directory temporary files (e.g., @@ -61,28 +92,22 @@ translators) are created. \fBTMPDIR\fR is only read if \fBSPOT_TMPDIR\fR does not exist. If none of these environment variables exist, or if their value is empty, files are created in the current directory. - .TP \fBSPOT_TMPKEEP\fR When this variable is defined, temporary files are not removed. This is mostly useful for debugging. - [OUTPUT DATA] - The following columns are output in the CSV or JSON files. - -.TP 7 +.TP \fBformula\fR The formula translated. - .TP \fBtool\fR The tool used to translate this formula. This is either the value of the full \fICOMMANDFMT\fR string specified on the command-line, or, -if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\FiCMD\fR, +if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\fICMD\fR, the value of \fISHORTNAME\fR. - .TP \fBexit_status\fR, \fBexit_code\fR Information about how the execution of the translator went. If the @@ -90,60 +115,51 @@ option \fB\-\-omit\-missing\fR is given, these two columns are omitted and only the lines corresponding to successful translation are output. Otherwise, \fBexit_status\fR is a string that can take the following values: - .RS .TP \f(CW"ok"\fR The translator ran succesfully (this does not imply that the produced automaton is correct) and ltlcross could parse the resulting automaton. In this case \fBexit_code\fR is always 0. - .TP \f(CW"timeout"\fR The translator ran for more than the number of seconds specified with the \fB\-\-timeout\fR option. In this case \fBexit_code\fR is always -1. - .TP \f(CW"exit code"\fR The translator terminated with a non-zero exit code. \fBexit_code\fR contains that value. - .TP \f(CW"signal"\fR The translator terminated with a signal. \fBexit_code\fR contains that signal's number. - .TP \f(CW"parse error"\fR The translator terminated normally, but ltlcross could not parse its output. In this case \fBexit_code\fR is always -1. - .TP \f(CW"no output"\fR The translator terminated normally, but without creating the specified output file. In this case \fBexit_code\fR is always -1. .RE - .TP \fBtime\fR A floating point number giving the run time of the translator in seconds. This is reported for all executions, even failling ones. - .PP Unless the \fB\-\-omit\-missing\fR option is used, data for all the following columns might be missing. - .TP -\fBin_type\fR, \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR, \fBin_acc\fR , \fBin_scc\fR -These columns are only output if \f(CW%D\fR appears in any command -specification, i.e., if any of the tools output some Streett or Rabin -automata. In this case \fBin_type\fR contains a string that is either -\f(CWDRA\fR (Deterministic Rabin Automaton) or \f(CWDSA\fR -(Deterministic Streett Automaton). The other columns respectively -give the number of states, edges, transitions, acceptance pairs, and -strongly connected components in that automaton. - +\fBin_type\fR, \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR, +\fBin_acc\fR , \fBin_scc\fR These columns are only output if +\f(CW%D\fR appears in any command specification, i.e., if any of the +tools output some Streett or Rabin automata. In this case +\fBin_type\fR contains a string that is either \f(CWDRA\fR +(Deterministic Rabin Automaton) or \f(CWDSA\fR (Deterministic Streett +Automaton). The other columns respectively give the number of states, +edges, transitions, acceptance pairs, and strongly connected +components in that automaton. .TP \fBstates\fR, \fBedges\fR, \fBtransitions\fR, \fBacc\fR The number of states, edges, transitions, and acceptance sets in the @@ -153,13 +169,12 @@ translated automaton. Column \fBedges\fR counts the number of edges that might have been merged into a formula-labeled edge. For instance an edge labeled by \f(CWtrue\fR will be counted as 2^3=8 transitions if the automaton mention 3 atomic propositions. - +.PP If the translator produced a Streett or Rabin automaton, these columns contains the size of a TGBA (or BA) produced by ltlcross from that Streett or Rabin automaton. Check \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR, and \fBin_acc\fR for statistics about the actual input automaton. - .TP \fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR The number of strongly connected components in the automaton. The @@ -168,18 +183,15 @@ count the SCCs that are non-accepting (a.k.a. transiant), terminal (recognizes and accepts all words), weak (do not recognize all words, but accepts all recognized words), or strong (accept some words, but reject some recognized words). - .TP \fBnondet_states\fR, \fBnondet_aut\fR The number of nondeterministic states, and a Boolean indicating whether the automaton is nondeterministic. - .TP \fBterminal_aut\fR, \fBweak_aut\fR, \fBstrong_aut\fR Three Boolean used to indicate whether the automaton is terminal (no weak nor strong SCCs), weak (some weak SCCs but no strong SCCs), or strong (some strong SCCs). - .TP \fBproduct_states\fR, \fBproduct_transitions\fR, \fBproduct_scc\fR Size of the product between the translated automaton and a randomly @@ -198,18 +210,21 @@ over the \fIN\fR products performed. [BIBLIOGRAPHY] If you would like to give a reference to this tool in an article, we suggest you cite the following paper: +.PP .TP \(bu Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. .PP -ltlcross is a Spot-based reimplementation of a tool called LBTT. LBTT +.B 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. - +.PP The sanity checks performed on the result of each translator (by either LBTT or ltlcross) are described in the following paper: +.PP .TP \(bu H. Tauriainen and K. Heljanko: Testing LTL formula translation into @@ -227,7 +242,12 @@ equivalent to Test 2 of Tauriainen and Heljanko. If only one automaton is deterministic, say P1, it can still be used to check we can be used to check the result of another translators, for instance checking the emptiness of Comp(P1)*P2. - +.PP 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. +.PP +Another major difference with LBTT is that ltlcross is +not restricted to generalized Büchi acceptance. It supports +Rabin and Streett automata via ltl2dstar's format, and automata +with arbitrary acceptance conditions via the HOA format. diff --git a/src/bin/man/ltlgrind.x b/src/bin/man/ltlgrind.x index ef05873b1..6f114534e 100644 --- a/src/bin/man/ltlgrind.x +++ b/src/bin/man/ltlgrind.x @@ -3,4 +3,4 @@ ltlgrind \- list mutations of a formula. [DESCRIPTION] .\" Add any additional description here [SEE ALSO] -.BR ltlcross (1), +.BR ltlcross (1) diff --git a/src/bin/man/randltl.x b/src/bin/man/randltl.x index f5d125720..c3167fecf 100644 --- a/src/bin/man/randltl.x +++ b/src/bin/man/randltl.x @@ -11,4 +11,5 @@ Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. [SEE ALSO] .BR genltl (1), -.BR ltlfilt (1) +.BR ltlfilt (1), +.BR randaut (1) diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index e570d1228..972397e5c 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -120,3 +120,4 @@ paper to deal with TBA or TGBA. .BR ltl2tgba (1) .BR ltl2tgta (1) .BR dstar2tgba (1) +.BR autfilt (1) diff --git a/tools/help2man b/tools/help2man index 95200c1a2..fb7c4da78 100755 --- a/tools/help2man +++ b/tools/help2man @@ -2,7 +2,7 @@ # Generate a short man page from --help and --version output. # Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2009, -# 2010, 2011, 2012 Free Software Foundation, Inc. +# 2010, 2011, 2012, 2015 Free Software Foundation, Inc. # This program is free software; you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by @@ -485,7 +485,14 @@ while (length) my $content = ''; # Option with description. - if (s/^( {1,10}([+-]\S.*?))(?:( +(?!-))|\n( {20,}))(\S.*)\n//) + my $descrpat2 = '(?:( +(?!-))|\n( {20,}))(\S.*)\n'; + my $descrpat1 = '(?:( (?!-))|\n( {20,}))(\S.*)\n'; + if (s/^( {1,10}([+-]\S.*?))$descrpat2//o || + # Cases where "-x, --option" or "--option" is separated from + # "description" by a single space, because "description" then + # starts on column 29. This is output by argp. + s/^( {2}([+-]\S.{24}))$descrpat1//o || + s/^( {6}([+-]\S.{20}))$descrpat1//o) { $matched .= $& if %append; $indent = length ($4 || "$1$3"); @@ -548,7 +555,8 @@ while (length) s/\x84//g; # Convert options. - s/(^| |\()(-[][\w=-]+)/$1 . convert_option $2/mge; + s/(^| )(-[][\w-]+(?:=[][\w=\/|()'"-]*)?)/$1 . convert_option $2/mge; + s/\((-[][\w-]+(?:=[][\w=\/|()'"-]*)?)\)/"(" . convert_option $1 . ")"/mge; # Escape remaining hyphens s/-/\x83/g; @@ -682,10 +690,15 @@ sub convert_option local $_ = '\fB' . shift; s/-/\x83/g; - unless (s/\[=(.*)\]$/\\fR[=\\fI$1\\fR]/) + if (s/\[=(.*)\]$/\\fR[=\\fI$1\\fR]/) + { + s/\|/\\fR|\\fI/g; + } + else { s/=(.)/\\fR=\\fI$1/; s/ (.)/ \\fI$1/; + s/[\[\|\]]/\\fR$&\\fI/g; $_ .= '\fR'; } diff --git a/tools/man2html.pl b/tools/man2html.pl new file mode 100755 index 000000000..ffea7dc5c --- /dev/null +++ b/tools/man2html.pl @@ -0,0 +1,64 @@ +#!/usr/bin/perl +## -*- coding: utf-8 -*- +## Copyright (C) 2015 Laboratoire de Recherche et Développement de +## l'Epita (LRDE). +## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 3 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with this program. If not, see . + +use strict; + +sub error($) +{ + print "$0: ", @_; + exit 1; +} + +error "Specify a directory with man pages\n" if @ARGV != 1; + +my $dir = @ARGV[0]; + +opendir(DIR, $dir) or die $!; +while (my $file = readdir(DIR)) +{ + next unless $file =~ m/\.\d$/; + $file = "$dir/$file"; + print "converting $file to $file.html with groff\n"; + my $html = `(echo '.HEAD ' + echo '.HEAD ' + cat $file) | groff -Kutf8 -mandoc -Thtml - -P -r`; + $html =~ s|GNU GPL version 3 or later.*http://gnu.org/licenses/gpl.html>|GNU GPL version 3 or later|s; + $html =~ s|

.*?

|
$&
|smg; + $html =~ s|(.*?
\n)+|

Table of Contents

    \n$&
|sm; + $html =~ s|(.*?)
|
  • $1
    • |g; + $html =~ s|•

    ..|•

    \n|smg; + $html =~ s|<spot\@lrde.epita.fr>|<spot\@lrde.epita.fr>|; + $html =~ s|<(https?://.*)>|<$1>|; + $html =~ s|

    ([^<>]*?:)\s*
    |

    $1

    |smg; + $html =~ s|

    ([^<>]*?:)\s*\s*
    |

    $1

    |smg; + $html =~ s|

    ([^<>]*?:)\s*

    |

    $1

    |smg; + $html =~ s@@@; + $html =~ s{([\w-]+)\((\d+)\)}{ + (-f "$1.$2") ? "$1($2)" : $&; + }xge; + open(FILE, ">$file.html"); + print FILE $html; + close(FILE); +} +closedir(DIR); +exit 0;