From 0ec5ebac3fb4a6ec845565f037bf54efe79797b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 19 Mar 2018 15:23:22 +0100 Subject: [PATCH] autcross: support %M in tool specifications Fixes #335. * bin/common_trans.cc: Add support. * tests/core/autcross4.test: New file. * tests/Makefile.am: Add it. * doc/org/autcross.org, NEWS: Document it. --- NEWS | 5 +++ bin/common_trans.cc | 25 ++++++++--- doc/org/autcross.org | 92 ++++++++++++++++++++++++++++++++++++++- tests/Makefile.am | 1 + tests/core/autcross4.test | 53 ++++++++++++++++++++++ 5 files changed, 170 insertions(+), 6 deletions(-) create mode 100644 tests/core/autcross4.test diff --git a/NEWS b/NEWS index 630485e4a..146c46a0c 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.5.1.dev (not yet released) + Command-line tools: + + - autcross' tool specifications now have %M replaced by the name of + the input automaton. + Library: - Option "a" of print_dot(), for printing the acceptance condition, diff --git a/bin/common_trans.cc b/bin/common_trans.cc index d254e2806..f9ce9879a 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -312,6 +312,7 @@ filed_automaton::print(std::ostream& os, const char* pos) const { std::ostringstream ss; char* opt = nullptr; + bool filename = true; if (*pos == '[') { ++pos; @@ -330,10 +331,20 @@ filed_automaton::print(std::ostream& os, const char* pos) const case 'L': spot::print_lbtt(ss, aut_, opt); break; + case 'M': + { + filename = false; + std::string* name = aut_->get_named_prop("automaton-name"); + spot::quote_shell_string(os, + name ? name->c_str() : + opt ? opt : + ""); + } } if (opt) free(opt); - os << '\'' << string_to_tmp(ss.str(), serial_) << '\''; + if (filename) + os << '\'' << string_to_tmp(ss.str(), serial_) << '\''; } translator_runner::translator_runner(spot::bdd_dict_ptr dict, @@ -409,6 +420,7 @@ autproc_runner::autproc_runner(bool no_output_allowed) declare('H', &filename_automaton); declare('S', &filename_automaton); declare('L', &filename_automaton); + declare('M', &filename_automaton); declare('O', &output); size_t s = tools.size(); @@ -420,9 +432,10 @@ autproc_runner::autproc_runner(bool no_output_allowed) std::vector has(256); const tool_spec& t = tools[n]; scan(t.cmd, has); - if (!(has['H'] || has['S'] || has['L'])) + if (!(has['H'] || has['S'] || has['L'] || has['M'])) error(2, 0, "no input %%-sequence in '%s'.\n Use " - "one of %%H,%%S,%%L to indicate the input automaton filename.", + "one of %%H,%%S,%%L to indicate the input automaton filename.\n" + " (Or use %%M if you want to work from its name.)\n", t.spec); if (!no_output_allowed && !has['O']) error(2, 0, "no output %%-sequence in '%s'.\n Use " @@ -831,6 +844,8 @@ static const argp_option options_aut[] = { "%H,%S,%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "filename for the input automaton in (H) HOA, (S) Spin's neverclaim, " "or (L) LBTT's format", 0 }, + { "%M, %[val]M", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the name of the input automaton, with an optional default value", 0 }, { "%O", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "filename for the automaton output in HOA, never claim, LBTT, or " "ltl2dstar's format", 0 }, diff --git a/doc/org/autcross.org b/doc/org/autcross.org index 1b4dc96f7..63142f25d 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -40,6 +40,8 @@ following character sequences: : %% a single % : %H,%S,%L filename for the input automaton in (H) HOA, (S) : Spin's neverclaim, or (L) LBTT's format +: %M, %[val]M the name of the input automaton, with an optional +: default value : %O filename for the automaton output in HOA, never : claim, LBTT, or ltl2dstar's format @@ -123,7 +125,7 @@ will be changed into What this implies is our previous example could be shortened to: -#+BEGIN_SRC sh :results verbatim :exports code +#+BEGIN_SRC sh :results silent :exports code randaut -B -n 3 a b | autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' #+END_SRC @@ -386,3 +388,91 @@ No problem detected. # LocalWords: ok complementation Ai Aj gRqrd ubUpHb JxFi oQGbj SQT # LocalWords: kWt Eo Xsc WXgCB vLwKMQ tI SXF qqlE KXplk ZFTCz PNY # LocalWords: hUAK IjnFhD cWys ZqjdQh +* Use-cases for =%M= + +If the input automata are named, it is possible to use =%M= in some +tool specification to pass this name to the tool. In particular, this +can be used to replace the input automaton by something else. + +For instance if the name of the automaton is an actual LTL formula +(automata produced by [[file:ltl2tgba.org][=ltl2tgba=]] follow this convention), you can +cross-compare some tool that input that formula instead of the +automaton. For instance consider the following command-line, where we +compare the determinization of =autfilt -D= (starting from an +automaton) to the determinization of =ltl2dstar= (starting from the +LTL formula encoded in the name of the automaton). That LTL formula +is not in a syntax supported by =ltl2dstar=, so we call =ltl2dstar= +via [[file:ltldo.org][=ltldo=]] to arrange that. + +#+BEGIN_SRC sh :results silent :export code +genltl --eh-patterns=1..3 | ltl2tgba | + autcross 'autfilt -P -D' 'ltldo ltl2dstar -f %M >%O' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :export results +genltl --eh-patterns=1..3 | ltl2tgba | + autcross 'autfilt -P -D' 'ltldo ltl2dstar -f %M >%O' 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1.1-16.7 p0 U (p1 & Gp2) +Running [A0]: autfilt -P -D 'lcr-i0-rBSCo9'>'lcr-o0-xyRJhy' +Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & Gp2)' >'lcr-o1-9uDUjX' +Performing sanity checks and gathering statistics... + +-:17.1-34.7 p0 U (p1 & X(p2 U p3)) +Running [A0]: autfilt -P -D 'lcr-i1-LFDrvm'>'lcr-o0-6fBZGL' +Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 U p3))' >'lcr-o1-AUXx0a' +Performing sanity checks and gathering statistics... + +-:35.1-64.7 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) +Running [A0]: autfilt -P -D 'lcr-i2-UaZCtA'>'lcr-o0-hhbJWZ' +Running [A1]: ltldo ltl2dstar -f 'p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))' >'lcr-o1-xhS4Ap' +Performing sanity checks and gathering statistics... + +No problem detected. +#+end_example + +This example is a bit contrived, and in this case, an alternative would +be to use [[file:ltlcross.org][=ltlcross=]], as in: + +#+BEGIN_SRC sh :results silent :export code +genltl --eh-patterns=1..3 | + ltlcross 'ltl2tgba %f | autfilt -P -D > %O' 'ltl2dstar' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :export results +genltl --eh-patterns=1..3 | + ltlcross 'ltl2tgba %f | autfilt -P -D > %O' 'ltl2dstar' 2>&1 +#+END_SRC + +#+RESULTS: +#+begin_example +-:1: (p0) U ((p1) & (G(p2))) +Running [P0]: ltl2tgba '(p0) U ((p1) & (G(p2)))' | autfilt -P -D > 'lcr-o0-DnV1rm' +Running [P1]: ltl2dstar --output-format=hoa 'lcr-i0-jBLulv' 'lcr-o1-epwYeE' +Running [N0]: ltl2tgba '!((p0) U ((p1) & (G(p2))))' | autfilt -P -D > 'lcr-o0-8bVQ9M' +Running [N1]: ltl2dstar --output-format=hoa 'lcr-i0-5oAAdW' 'lcr-o1-W7elh5' +Performing sanity checks and gathering statistics... + +-:2: (p0) U ((p1) & (X((p2) U (p3)))) +Running [P0]: ltl2tgba '(p0) U ((p1) & (X((p2) U (p3))))' | autfilt -P -D > 'lcr-o0-xMdCve' +Running [P1]: ltl2dstar --output-format=hoa 'lcr-i1-OJU1Sn' 'lcr-o1-wOCsgx' +Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) U (p3)))))' | autfilt -P -D > 'lcr-o0-SzgmFG' +Running [N1]: ltl2dstar --output-format=hoa 'lcr-i1-8iIddQ' 'lcr-o1-zBV5KZ' +Performing sanity checks and gathering statistics... + +-:3: (p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6)))))))))))))) +Running [P0]: ltl2tgba '(p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6))))))))))))))' | autfilt -P -D > 'lcr-o0-FEA6s9' +Running [P1]: ltl2dstar --output-format=hoa 'lcr-i2-E0Ikpj' 'lcr-o1-ppDzlt' +Running [N0]: ltl2tgba '!((p0) U ((p1) & (X((p2) & (F((p3) & (X(F((p4) & (X(F((p5) & (X(F(p6)))))))))))))))' | autfilt -P -D > 'lcr-o0-jqlelD' +Running [N1]: ltl2dstar --output-format=hoa 'lcr-i2-IwU1uN' 'lcr-o1-6YdQEX' +Performing sanity checks and gathering statistics... + +No problem detected. +#+end_example + +However in practice you could also use the =name:= field of the input +automaton, combined with =%M= in the tool specification, to designate +an alternate filename to load, or some key to look up somewhere. diff --git a/tests/Makefile.am b/tests/Makefile.am index 4e25ec2a1..9cb4ac44b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -305,6 +305,7 @@ TESTS_twa = \ core/autcross.test \ core/autcross2.test \ core/autcross3.test \ + core/autcross4.test \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ diff --git a/tests/core/autcross4.test b/tests/core/autcross4.test new file mode 100644 index 000000000..ce21ab31f --- /dev/null +++ b/tests/core/autcross4.test @@ -0,0 +1,53 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# 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 . + +# Test the timeout handling of autcross. +. ./defs +set -e + +ltl2tgba -f FGa '"a = b"U!c' | + autcross 'autfilt' 'ltl2tgba -B %M >%O' --csv=out.csv +test 2 = `grep -c '"FGa"' out.csv` +test 2 = `grep -c '"""a = b"" U !c"' out.csv` + + +cat >in <%O' 'ltl2tgba %M>%O' --csv=out.csv && exit 1 +test 3 = `grep -c '"ok"' out.csv` +