From f99ddef787a7768986e0102ff9c69b2cd36e166e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Nov 2021 14:12:32 +0100 Subject: [PATCH] bin: use regexes to detect shorthands, and add support for owl-21.0 Fixes #480. * bin/common_trans.cc (shorthands_ltl, shorthands_autproc): Write those lists using regexes. Add entries for Owl 21.0. (show_shorthands, tool_spec): Adjust to use those regexes. * doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org: Update the list of shorthands. * tests/core/ltldo.test: Add a couple of tests. * NEWS: Mention this new feature. --- NEWS | 6 ++++ bin/common_trans.cc | 69 ++++++++++++++++++++++--------------------- doc/org/autcross.org | 15 +++++----- doc/org/ltlcross.org | 30 ++++++++----------- doc/org/ltldo.org | 37 ++++++++++++----------- tests/core/ltldo.test | 9 +++++- 6 files changed, 90 insertions(+), 76 deletions(-) diff --git a/NEWS b/NEWS index 44b18925d..fead4fa6c 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,12 @@ New in spot 2.9.8.dev (not yet released) - autfilt learned a --kill-states=NUM[,NUM...] option. + - ltlcross, autcross, ltldo have learned shorthands for + the commands of Owl 21.0. For instance running + ltlcross 'owl-21 ltl2nba' ... + is equivalent to running + ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ... + Library: - Spot now provides convenient function to create and solve games. The functions are located in twaalgos/game.hh. Additional diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 9c1f27a15..78cb632ed 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,6 +30,7 @@ #ifdef HAVE_SPAWN_H #include #endif +#include #include "error.h" @@ -45,49 +46,52 @@ struct shorthands_t { const char* prefix; + std::regex rprefix; const char* suffix; }; +#define SHORTHAND(PRE, POST) { PRE, std::regex("^" PRE), POST } + static shorthands_t shorthands_ltl[] = { - { "delag", " %f>%O" }, - { "lbt", " <%L>%O" }, - { "ltl2ba", " -f %s>%O" }, - { "ltl2da", " %f>%O" }, - { "ltl2dgra", " %f>%O" }, - { "ltl2dpa", " %f>%O" }, - { "ltl2dra", " %f>%O" }, - { "ltl2dstar", " --output-format=hoa %[MW]L %O"}, - { "ltl2ldba", " %f>%O" }, - { "ltl2na", " %f>%O" }, - { "ltl2nba", " %f>%O" }, - { "ltl2ngba", " %f>%O" }, - { "ltl2tgba", " -H %f>%O" }, - { "ltl3ba", " -f %s>%O" }, - { "ltl3dra", " -f %s>%O" }, - { "ltl3hoa", " -f %f>%O" }, - { "ltl3tela", " -f %f>%O" }, // ltl3tela is the new name of ltl3hoa - { "modella", " %[MWei^]L %O" }, - { "spin", " -f %s>%O" }, - }; + SHORTHAND("delag", " %f>%O"), + SHORTHAND("lbt", " <%L>%O"), + SHORTHAND("ltl2ba", " -f %s>%O"), + SHORTHAND("ltl2(da|dgra|dpa|dra|ldba|na|nba|ngba)", " %f>%O"), + SHORTHAND("ltl2dstar", " --output-format=hoa %[MW]L %O"), + SHORTHAND("ltl2tgba", " -H %f>%O"), + // ltl3tela is the new name of ltl3hoa + SHORTHAND("ltl3(ba|dra|hoa|tela)", " -f %s>%O"), + SHORTHAND("modella", " %[MWei^]L %O"), + SHORTHAND("spin", " -f %s>%O"), + // Starting from Owl 21.0, Owl's tools have been grouped as + // sub-commands of the Owl binary. We still want to support + // use cases where several version of owl are installed with + // different names. + SHORTHAND("owl.* ltl2[bdeglnpr]+a\\b", " -f %f>%O"), + SHORTHAND("owl.* ltl2delta2\\b", " -f %f"), + SHORTHAND("owl.* ltl-utilities\\b", " -f %f"), +}; static shorthands_t shorthands_autproc[] = { - { "autfilt", " %H>%O" }, - { "dra2dpa", " <%H>%O" }, - { "dstar2tgba", " %H>%O" }, - { "ltl2dstar", " -B %H %O" }, - { "nba2dpa", " <%H>%O" }, - { "nba2ldpa", " <%H>%O" }, - { "seminator", " %H>%O" }, - }; + SHORTHAND("autfilt", " %H>%O"), + SHORTHAND("dra2dpa", " <%H>%O"), + SHORTHAND("dstar2tgba", " %H>%O"), + SHORTHAND("ltl2dstar", " -B %H %O"), + SHORTHAND("nba2l?dpa", " <%H>%O"), + SHORTHAND("seminator", " %H>%O"), + SHORTHAND("owl.* " + "(ngba2ldba|nba(2dpa|2det|sim)|aut2parity|gfg-minimization)\\b", + " <%H>%O"), +}; static void show_shorthands(shorthands_t* begin, shorthands_t* end) { 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"); + "the following regexes, then the string on the right is appended.\n\n"); while (begin != end) { std::cout << " " - << std::left << std::setw(12) << begin->prefix + << std::left << std::setw(40) << begin->prefix << begin->suffix << '\n'; ++begin; } @@ -139,8 +143,7 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, while (begin != end) { auto& p = *begin++; - int n = strlen(p.prefix); - if (strncmp(basename, p.prefix, n) == 0) + if (std::regex_search(basename, p.rprefix)) { int m = strlen(p.suffix); int q = strlen(cmd); diff --git a/doc/org/autcross.org b/doc/org/autcross.org index 058b58619..90a268b44 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -105,14 +105,15 @@ autcross --list-shorthands #+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. +the following regexes, then the string on the right is appended. - autfilt %H>%O - dstar2tgba %H>%O - ltl2dstar -B %H %O - nba2dpa <%H>%O - nba2ldpa <%H>%O - seminator %H>%O + autfilt %H>%O + dra2dpa <%H>%O + dstar2tgba %H>%O + ltl2dstar -B %H %O + nba2l?dpa <%H>%O + seminator %H>%O + owl.* (ngba2ldba|nba(2dpa|2det|sim)|aut2parity|gfg-minimization)\b <%H>%O Any {name} and directory component is skipped for the purpose of matching those prefixes. So for instance diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 07f273902..0fdebae1f 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -185,24 +185,20 @@ ltlcross --list-shorthands #+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. +the following regexes, then the string on the right is appended. - delag %f>%O - lbt <%L>%O - ltl2ba -f %s>%O - ltl2da %f>%O - ltl2dgra %f>%O - ltl2dpa %f>%O - ltl2dra %f>%O - ltl2ldba %f>%O - ltl2dstar --output-format=hoa %[MW]L %O - ltl2tgba -H %f>%O - ltl3ba -f %s>%O - ltl3dra -f %s>%O - ltl3hoa -f %f>%O - ltl3tela -f %f>%O - modella %[MWei^]L %O - spin -f %s>%O + delag %f>%O + lbt <%L>%O + ltl2ba -f %s>%O + ltl2(da|dgra|dpa|dra|ldba|na|nba|ngba) %f>%O + ltl2dstar --output-format=hoa %[MW]L %O + ltl2tgba -H %f>%O + ltl3(ba|dra|hoa|tela) -f %s>%O + modella %[MWei^]L %O + spin -f %s>%O + owl.* ltl2[bdeglnpr]+a\b -f %f>%O + owl.* ltl2delta2\b -f %f + owl.* ltl-utilities\b -f %f Any {name} and directory component is skipped for the purpose of matching those prefixes. So for instance diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 5c3a3aba8..b46932c8b 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -306,26 +306,26 @@ ltldo --list-shorthands #+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. +the following regexes, then the string on the right is appended. - lbt <%L>%O - ltl2ba -f %s>%O - ltl2da %f>%O - ltl2dpa %f>%O - ltl2ldba %f>%O - ltl2dstar --output-format=hoa %[MW]L %O - ltl2tgba -H %f>%O - ltl3ba -f %s>%O - ltl3dra -f %s>%O - ltl3hoa -f %f>%O - modella %[MWei^]L %O - spin -f %s>%O + delag %f>%O + lbt <%L>%O + ltl2ba -f %s>%O + ltl2(da|dgra|dpa|dra|ldba|na|nba|ngba) %f>%O + ltl2dstar --output-format=hoa %[MW]L %O + ltl2tgba -H %f>%O + ltl3(ba|dra|hoa|tela) -f %s>%O + modella %[MWei^]L %O + spin -f %s>%O + owl.* ltl2[bdeglnpr]+a\b -f %f>%O + owl.* ltl2delta2\b -f %f + owl.* ltl-utilities\b -f %f 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 %[MR]L %O' +will be changed into + '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MW]L %O' #+end_example Therefore you can type the following to obtain a Dot output (as @@ -353,9 +353,10 @@ digraph "" { The =ltl2ba= argument passed to =ltldo= was interpreted as if you had typed ={ltl2ba}ltl2ba -f %s>%O=. -The shorthand is only used if it is the first word of a command -string that does not use any =%= character. This makes it possible to -add options: +Those shorthand patterns are only tested if the command string does +not contains any =%= character. They should always patch a prefix of +the command, ignoring any leading directory. This makes it possible +to add options: #+BEGIN_SRC sh ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges' diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index 5027dad0c..1504a24c0 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -157,8 +157,15 @@ grep ':.*empty input' stderr ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1 +grep % stderr && exit 1 grep 'ltldo:.*foo/bar/ltl2baextended' stderr +ltldo '{name} foo/bar/owl-21.00 ltl2nba' -f GFa 2>stderr && exit 1 +grep % stderr && exit 1 +grep 'ltldo:.*foo/bar/owl-21.00' stderr + +ltldo '{name} foo/bar/owl-21.00 non-existant' -f GFa 2>stderr && exit 1 +grep % stderr test 2 = `genltl --and-gf=1..4 | ltldo ltl2tgba -n2 | autfilt -c` test 3 = `genltl --and-gf=1..2 | ltldo ltl2tgba 'ltl2tgba -s' -n3 | autfilt -c`