diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 3b6c59392..cdacb485b 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -180,6 +180,12 @@ the following words, then the string on the right is appended. ltl3dra -f %f>%O modella %L %O spin -f %s>%O + +Any {name} and directory component is skipped for the purpose of +matching those prefixes. So for instance + '{DRA} ~/mytools/ltl2dstar-0.5.2' +will changed into + '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O' #+end_example What this implies is that running =ltlcross ltl2ba ltl3ba ...= is diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 6ce8a924d..281c3c5b9 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -58,6 +58,12 @@ void show_shorthands() std::cout << " " << std::left << std::setw(12) << s.prefix << s.suffix << '\n'; + std::cout + << ("\nAny {name} and directory component is skipped for the purpose of\n" + "matching those prefixes. So for instance\n" + " '{DRA} ~/mytools/ltl2dstar-0.5.2'\n" + "will changed into\n" + " '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O'\n"); } @@ -84,15 +90,28 @@ translator_spec::translator_spec(const char* spec) } } } - // If we recognize a shorthand, add the suffixes. + // If there is no % in the string, look for a known + // command from our shorthand list. If we find it, + // add the suffix. bool allocated = false; if (!strchr(cmd, '%')) { + // Skip any leading directory name. + auto basename = cmd; + auto pos = cmd; + while (*pos) + { + if (*pos == '/') + basename = pos + 1; + else if (*pos == ' ') + break; + ++pos; + } + // Match a shorthand. for (auto& p: shorthands) { int n = strlen(p.prefix); - if (strncmp(cmd, p.prefix, n) == 0 && - (cmd[n] == 0 || cmd[n] == ' ')) + if (strncmp(basename, p.prefix, n) == 0) { int m = strlen(p.suffix); int q = strlen(cmd); diff --git a/src/tests/ltldo.test b/src/tests/ltldo.test index b8fadba2d..fb050c08a 100755 --- a/src/tests/ltldo.test +++ b/src/tests/ltldo.test @@ -110,3 +110,6 @@ $ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1 test $? = 2 grep 'error: command ".*" produced an empty output.' stderr grep 'ltldo: aborting' stderr + +$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1 +grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr