From a24a021964bbeb9f49c2c983acfa451e085828e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 27 Jan 2015 15:06:58 +0100 Subject: [PATCH] bin: add shorthands for ltlcross and ltldo * src/bin/common_trans.cc: Implement shorthands. * doc/org/ltlcross.org, doc/org/ltldo.org: Document them. * src/tgbatest/ltldo2.test: Quick test. * NEWS: Mention it. --- NEWS | 6 +++ doc/org/ltlcross.org | 29 +++++++++++ doc/org/ltldo.org | 106 ++++++++++++++++++++++++++++++++++++--- src/bin/common_trans.cc | 99 +++++++++++++++++++++++++++++------- src/tgbatest/ltldo2.test | 4 +- 5 files changed, 217 insertions(+), 27 deletions(-) diff --git a/NEWS b/NEWS index 3bf0da147..7a3c6b03f 100644 --- a/NEWS +++ b/NEWS @@ -37,6 +37,12 @@ New in spot 1.99a (not yet released) now. The short '-n NUM' option is now the same as the new --max-count=N option, for consistency with other tools. + - ltlcross (and ltldo) have a list of hard-coded shorthands + for some existing tools. So for instance running + 'ltlcross spin ...' is the same as running + 'ltlcross "spin -f %s>%N" ...'. This feature is much + more useful for ltldo. + - There is a parser for the HOA format (http://adl.github.io/hoaf/) available as a spot::hoa_stream_parser object or spot::hoa_parse() function. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 9f5fe901d..ae9aa0d29 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -149,6 +149,35 @@ tools: so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file) - '=ltl3dra -f %s >%D=' +To simplify the use of some of the above tools, a set of predefined +shorthands are available. Those can be listed with the +=--list-shorthands= option. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlcross --list-shorthands +#+END_SRC +#+RESULTS: +#+begin_example +If a COMMANDFMT does not use any %-sequence, and starts with one of +the following words, then the string on the right is appended. + + lbt <%L>%T + ltl2ba -f %s>%N + ltl2dstar %L %D + ltl2tgba -H %f>%H + ltl3ba -f %s>%N + ltl3dra -f %f>%D + modella %L %T + spin -f %s>%N +#+end_example + +What this implies is that running =ltlcross ltl2ba ltl3ba ...= is +the same as running =ltlcross 'ltl2ba -f %s>%N' 'ltl3ba -f %s>%N' ...= + +Because only the prefix of the actual command is checked, you can +still specify some options. For instance =ltlcross 'ltl2tgba -D' ...= +is short for =ltlcross 'ltl2tgba -D -H %F>%H' ...= + * Getting statistics Detailed statistics about the result of each translation, and the diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 2f7360d9b..02fc85d49 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -81,7 +81,7 @@ X[]!<>((a && ![]b) || (!a && []b)),4,10 Using =ltldo= the above command can be reduced to this: #+BEGIN_SRC sh :results verbatim :exports both -ltldo -F sample.ltl 'ltl3ba -f %s>%N' --stats='%f,%s,%t' +ltldo 'ltl3ba -f %s>%N' -F sample.ltl --stats='%f,%s,%t' #+END_SRC #+RESULTS: #+begin_example @@ -101,6 +101,27 @@ Note that the formulas look different in both cases, because in the =while= loop the formula printed has already been processed with =ltlfilt=, while =ltldo= emits the input string untouched. +In fact, as we will discuss below, =ltl3ba= is a tool that =ltldo= +already knows about, so there is a shorter way to run the above +command: + +#+BEGIN_SRC sh :results verbatim :exports code +ltldo ltl3ba -F sample.ltl --stats='%f,%s,%t' +#+END_SRC +#+RESULTS: +#+begin_example +1,1,1 +1 U a,2,4 +!(!((a U Gb) U b) U GFa),2,4 +(b <-> Xc) xor Fb,7,21 +FXb R (a R (1 U b)),6,28 +Ga,1,1 +G(!(c | (a & (a W Gb))) M Xa),1,0 +GF((b R !a) U (Xc M 1)),2,4 +G(Xb | Gc),3,11 +XG!F(a xor Gb),4,10 +#+end_example + * Example: running =spin= and producing HOA Here is another example, where we use Spin to produce two automata in @@ -142,6 +163,13 @@ State: 1 {0} --END-- #+end_example +Again, using the shorthands defined below, the previous command can be +simplified to just this: + +#+BEGIN_SRC sh :results verbatim :exports code +ltldo spin -f a -f GFa -H +#+END_SRC + * Syntax for specifying tools to call The syntax for specifying how a tool should be called is the same as @@ -159,9 +187,10 @@ ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' : %N,%T,%D,%H the automaton is output as a Never claim, or in : LBTT's, in LTL2DSTAR's, or in the HOA format -Contrarily to =ltlcross=, it this not mandatory to specify an output filename -using one of the sequence for that later lines. For instance we could -simply run a formula though =echo= to compare different output syntaxes: +Contrarily to =ltlcross=, it this not mandatory to specify an output +filename using one of the sequence for that last line. For instance +we could simply run a formula though =echo= to compare different +output syntaxes: #+BEGIN_SRC sh :results verbatim :exports both ltldo -f 'p0 U p1' -f 'GFp0' 'echo %f, %s, %l, %w' @@ -257,6 +286,66 @@ ltl3ba,4,7 Much more readable! +* Shorthands for existing tools + +There is a list of existing tools for which =ltldo= (and =ltlcross=) +have built-in specifications. This list can be printed using the +=--list-shorthands= option: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo --list-shorthands +#+END_SRC +#+RESULTS: +#+begin_example +If a COMMANDFMT does not use any %-sequence, and starts with one of +the following words, then the string on the right is appended. + + lbt <%L>%T + ltl2ba -f %s>%N + ltl2dstar %L %D + ltl2tgba -H %f>%H + ltl3ba -f %s>%N + ltl3dra -f %f>%D + modella %L %T + spin -f %s>%N +#+end_example + +So for instance you can type just + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl2ba -f a +#+END_SRC + +to obtain a Dot output (this is the default output format for =ltldo=) +for the neverclaim produced by =ltl2ba -f a=. + +#+RESULTS: +: digraph G { +: rankdir=LR +: I [label="", style=invis, width=0] +: I -> 0 +: 0 [label="0", peripheries=2] +: 0 -> 1 [label="a"] +: 1 [label="1", peripheries=2] +: 1 -> 1 [label="1"] +: } + +The =ltl2ba= argument passed to =ltldo= was interpreted as if you had +typed ={ltl2ba}ltl2ba -f %s>%N=. + +The shorthand is only used if it is the first word of an command +string that does not use any =%= character. This makes it possible to +add options: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges' +#+END_SRC + +#+RESULTS: +: ltl3ba, 2 states, 4 edges +: ltl3ba -H2, 1 states, 2 edges + + * Transparent renaming Have you ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate @@ -281,7 +370,7 @@ only atomic propositions starting with a lowercase letter. Running the same command through =ltldo= will work: #+BEGIN_SRC sh :results verbatim :exports both -ltldo -t 'spin -f %s>%N' -f '[]!Error' -s +ltldo spin -f '[]!Error' -s #+END_SRC #+RESULTS: : never { @@ -291,6 +380,9 @@ ltldo -t 'spin -f %s>%N' -f '[]!Error' -s : fi; : } +(We need the =-s= option to obtain a never claim, instead of the +default GraphViz output.) + What happened is that =ltldo= renamed the atomic propositions in the formula before calling =spin=. So =spin= actually received the formula =[]!p0=, produced a never claim using =p0=, and that never @@ -311,7 +403,7 @@ automaton uses the atomic proposition =Error=, but its name contains a reference to =p0=. #+BEGIN_SRC sh :results verbatim :exports both -ltldo 'ltl3ba -H -f %s>%H' -f '[]!Error' -H +ltldo 'ltl3ba -H' -f '[]!Error' -H #+END_SRC #+RESULTS: #+begin_example @@ -333,7 +425,7 @@ If this is a problem, you can always force a new name with the =--name= option: #+BEGIN_SRC sh :results verbatim :exports both -ltldo 'ltl3ba -H -f %s>%H' -f '[]!Error' -H --name='BA for %f' +ltldo 'ltl3ba -H' -f '[]!Error' -H --name='BA for %f' #+END_SRC #+RESULTS: diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 2f4bba3ac..0bfe4bdca 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -24,6 +24,7 @@ #include #include #include +#include #include "error.h" @@ -31,29 +32,81 @@ #include "ltlvisit/lbt.hh" #include "common_conv.hh" +// A set of tools for which we know the correct output +static struct shorthands_t +{ + const char* prefix; + const char* suffix; +} + shorthands[] = { + { "lbt", " <%L>%T" }, + { "ltl2ba", " -f %s>%N" }, + { "ltl2dstar", " %L %D"}, + { "ltl2tgba", " -H %f>%H" }, + { "ltl3ba", " -f %s>%N" }, + { "ltl3dra", " -f %f>%D" }, + { "modella", " %L %T" }, + { "spin", " -f %s>%N" }, + }; + +void show_shorthands() +{ + std::cout + << ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" + "the following words, then the string on the right is appended.\n\n"); + for (auto& s: shorthands) + std::cout << " " + << std::left << std::setw(12) << s.prefix + << s.suffix << '\n'; +} + + translator_spec::translator_spec(const char* spec) : spec(spec), cmd(spec), name(spec) { - if (*cmd != '{') - return; - - // Match the closing '}' - const char* pos = cmd; - unsigned count = 1; - while (*++pos) + if (*cmd == '{') { - if (*pos == '{') - ++count; - else if (*pos == '}') - if (!--count) - { - name = strndup(cmd + 1, pos - cmd - 1); - cmd = pos + 1; - while (*cmd == ' ' || *cmd == '\t') - ++cmd; - break; - } + // Match the closing '}' + const char* pos = cmd; + unsigned count = 1; + while (*++pos) + { + if (*pos == '{') + ++count; + else if (*pos == '}') + if (!--count) + { + name = strndup(cmd + 1, pos - cmd - 1); + cmd = pos + 1; + while (*cmd == ' ' || *cmd == '\t') + ++cmd; + break; + } + } } + // If we recognize a shorthand, add the suffixes. + bool allocated = false; + if (!strchr(cmd, '%')) + { + for (auto& p: shorthands) + { + int n = strlen(p.prefix); + if (strncmp(cmd, p.prefix, n) == 0 && + (cmd[n] == 0 || cmd[n] == ' ')) + { + int m = strlen(p.suffix); + int q = strlen(cmd); + char* tmp = static_cast(malloc(q + m + 1)); + strcpy(tmp, cmd); + strcpy(tmp + q, p.suffix); + cmd = tmp; + allocated = true; + break; + } + } + } + if (!allocated) + cmd = strdup(cmd); } translator_spec::translator_spec(const translator_spec& other) @@ -61,12 +114,16 @@ translator_spec::translator_spec(const translator_spec& other) { if (name != spec) name = strdup(name); + if (cmd != spec) + cmd = strdup(cmd); } translator_spec::~translator_spec() { if (name != spec) free(const_cast(name)); + if (cmd != spec) + free(const_cast(cmd)); } std::vector translators; @@ -326,6 +383,7 @@ exec_with_timeout(const char* cmd) return status; } +#define OPT_LIST 1 static const argp_option options[] = { /**************************************************/ @@ -333,6 +391,8 @@ static const argp_option options[] = { "translator", 't', "COMMANDFMT", 0, "register one translator to call", 0 }, { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 }, + { "list-shorthands", OPT_LIST, 0 , 0, + "list availabled shorthands to use in COMMANDFMT", 0}, /**************************************************/ { 0, 0, 0, 0, "COMMANDFMT should specify input and output arguments using the " @@ -369,6 +429,9 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) << "on your platform" << std::endl; #endif break; + case OPT_LIST: + show_shorthands(); + exit(0); default: return ARGP_ERR_UNKNOWN; } diff --git a/src/tgbatest/ltldo2.test b/src/tgbatest/ltldo2.test index 0ec447a4c..7b8de7e6b 100755 --- a/src/tgbatest/ltldo2.test +++ b/src/tgbatest/ltldo2.test @@ -27,5 +27,5 @@ genltl=../../bin/genltl test -n "$LTL2BA" || exit 77 $genltl --or-g=1..2 | - run 0 $ltldo '{ltl2ba}ltl2ba -f %s>%H' >output -test 2 = `grep -c digraph output` + run 0 $ltldo 'ltl2ba -f %s>%H' '{foo}ltl2ba' >output +test 4 = `grep -c digraph output`