diff --git a/NEWS b/NEWS index 78a14561b..0d165bd95 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,10 @@ New in spot 2.10.4.dev (net yet released) - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). + - ltlsynt as a new option --tlsf that takes the filename of a TLSF + specification and calls syfco (which must be installed) to convert + it into an LTL formula. + Library: - The new function suffix_operator_normal_form() implements diff --git a/bin/common_trans.cc b/bin/common_trans.cc index a9b823ff4..9ab719a5b 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -27,6 +27,7 @@ #include #include #include +#include #if __has_include() #define HAVE_SPAWN_H 1 #include @@ -461,6 +462,93 @@ autproc_runner::round_automaton(spot::const_twa_graph_ptr aut, unsigned serial) filename_automaton.new_round(aut, serial); } + +std::string +read_stdout_of_command(char* const* args) +{ +#if HAVE_SPAWN_H + int cout_pipe[2]; + if (int err = pipe(cout_pipe)) + error(2, err, "pipe() failed"); + + posix_spawn_file_actions_t actions; + if (int err = posix_spawn_file_actions_init(&actions)) + error(2, err, "posix_spawn_file_actions_init() failed"); + + posix_spawn_file_actions_addclose(&actions, STDIN_FILENO); + posix_spawn_file_actions_addclose(&actions, cout_pipe[0]); + posix_spawn_file_actions_adddup2(&actions, cout_pipe[1], STDOUT_FILENO); + posix_spawn_file_actions_addclose(&actions, cout_pipe[1]); + + pid_t pid; + if (int err = posix_spawnp(&pid, args[0], &actions, nullptr, args, environ)) + error(2, err, "failed to run '%s'", args[0]); + + if (int err = posix_spawn_file_actions_destroy(&actions)) + error(2, err, "posix_spawn_file_actions_destroy() failed"); + + if (close(cout_pipe[1]) < 0) + error(2, errno, "closing write-side of pipe failed"); + + std::string buffer(32, 0); + std::string results; + int bytes_read; + for (;;) + { + static char buffer[512]; + bytes_read = read(cout_pipe[0], buffer, sizeof(buffer)); + if (bytes_read > 0) + results.insert(results.end(), buffer, buffer + bytes_read); + else + break; + } + if (bytes_read < 0) + error(2, bytes_read, "failed to read from pipe"); + + if (cout_pipe[0] < 0) + error(2, errno, "closing read-side of pipe failed"); + + int exit_code = 0; + if (waitpid(pid, &exit_code, 0) == -1) + error(2, errno, "waitpid() failed"); + + if (exit_code) + error(2, 0, "'%s' exited with status %d", args[0], exit_code); + + return results; +#else + // We could provide a pipe+fork+exec alternative implementation, but + // systems without posix_spawn() might also not have fork and exec. + // For instance MinGW does not. So let's fallback to system+tmpfile + // instead for maximum portability. + char prefix[30]; + snprintf(prefix, sizeof prefix, "spot-tmp"); + spot::temporary_file* tmpfile = spot::create_tmpfile(prefix); + std::string tmpname = tmpfile->name(); + std::ostringstream cmd; + for (auto t = args; *t != nullptr; ++t) + spot::quote_shell_string(cmd, *t) << ' '; + cmd << '>'; + spot::quote_shell_string(cmd, tmpfile->name()); + std::string cmdstr = cmd.str(); + int exit_code = system(cmdstr.c_str()); + if (exit_code < 0) + error(2, errno, "failed to execute %s", cmdstr.c_str()); + if (exit_code > 0) + error(2, 0, "'%s' exited with status %d", args[0], exit_code); + + std::ifstream ifs(tmpname, std::ifstream::in); + if (!ifs) + error(2, 0, "failed to open %s (output of %s)", tmpname.c_str(), args[0]); + ifs.exceptions(std::ifstream::failbit | std::ifstream::badbit); + std::stringstream buffer; + buffer << ifs.rdbuf(); + delete tmpfile; + return buffer.str(); +#endif +} + + std::atomic timed_out{false}; unsigned timeout_count = 0; @@ -706,6 +794,7 @@ parse_simple_command(const char* cmd) return res; } + #ifndef HAVE_SPAWN_H static void exec_command(const char* cmd) diff --git a/bin/common_trans.hh b/bin/common_trans.hh index e01131350..31c88c80c 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et +// Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -175,3 +175,9 @@ int exec_with_timeout(const char* cmd); #define exec_with_timeout(cmd) system(cmd) #define setup_sig_handler() while (0); #endif // !ENABLE_TIMEOUT + +// Run a command (whose args[0], args[1], etc. are given by args), and +// return its captured stdout. Stderr is not captured. Will abort +// with an error message if the command is not found, or if it exit +// with a non-zero status code. +std::string read_stdout_of_command(char* const* args); diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 0e5d765a1..a6abb7c81 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,6 +25,7 @@ #include "common_finput.hh" #include "common_setup.hh" #include "common_sys.hh" +#include "common_trans.hh" #include #include @@ -54,6 +55,7 @@ enum OPT_PRINT_HOA, OPT_REAL, OPT_SIMPLIFY, + OPT_TLSF, OPT_VERBOSE, OPT_VERIFY }; @@ -64,10 +66,13 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, "Input options:", 1 }, { "outs", OPT_OUTPUT, "PROPS", 0, "comma-separated list of controllable (a.k.a. output) atomic" - " propositions", 0}, + " propositions", 0 }, { "ins", OPT_INPUT, "PROPS", 0, "comma-separated list of uncontrollable (a.k.a. input) atomic" - " propositions", 0}, + " propositions", 0 }, + { "tlsf", OPT_TLSF, "FILENAME", 0, + "Read a TLSF specification from FILENAME, and call syfco to " + "convert it into LTL", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0, @@ -152,6 +157,8 @@ static const char* opt_print_hoa_args = nullptr; static bool opt_real = false; static bool opt_do_verify = false; static const char* opt_print_aiger = nullptr; +static char* opt_tlsf = nullptr; +static std::string opt_tlsf_string; static spot::synthesis_info* gi; @@ -486,8 +493,8 @@ namespace // If we reach this line // a strategy was found for each subformula assert(mealy_machines.size() == sub_form.size() - && "There are subformula for which no mealy like object" - "has been created."); + && ("There are subformula for which no mealy like object" + " has been created.")); spot::aig_ptr saig = nullptr; spot::twa_graph_ptr tot_strat = nullptr; @@ -646,6 +653,18 @@ namespace }; } +static void +split_aps(std::string arg, std::vector& where) +{ + std::istringstream aps(arg); + std::string ap; + while (std::getline(aps, ap, ',')) + { + ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); + where.push_back(str_tolower(ap)); + } +} + static int parse_opt(int key, char *arg, struct argp_state *) { @@ -671,25 +690,13 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_INPUT: { all_input_aps.emplace(std::vector{}); - std::istringstream aps(arg); - std::string ap; - while (std::getline(aps, ap, ',')) - { - ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); - all_input_aps->push_back(str_tolower(ap)); - } + split_aps(arg, *all_input_aps); break; } case OPT_OUTPUT: { all_output_aps.emplace(std::vector{}); - std::istringstream aps(arg); - std::string ap; - while (std::getline(aps, ap, ',')) - { - ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); - all_output_aps->push_back(str_tolower(ap)); - } + split_aps(arg, *all_output_aps); break; } case OPT_PRINT: @@ -710,6 +717,11 @@ parse_opt(int key, char *arg, struct argp_state *) gi->minimize_lvl = XARGMATCH("--simplify", arg, simplify_args, simplify_values); break; + case OPT_TLSF: + if (opt_tlsf) + error(2, 0, "option --tlsf may only be used once"); + opt_tlsf = arg; + break; case OPT_VERBOSE: gi->verbose_stream = &std::cerr; if (not gi->bv) @@ -746,6 +758,29 @@ main(int argc, char **argv) argp_program_doc, children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); + + if (opt_tlsf) + { + static char arg0[] = "syfco"; + static char arg1[] = "-f"; + static char arg2[] = "ltlxba"; + static char arg3[] = "-m"; + static char arg4[] = "fully"; + char* command[] = { arg0, arg1, arg2, arg3, arg4, opt_tlsf, nullptr }; + opt_tlsf_string = read_stdout_of_command(command); + jobs.emplace_back(opt_tlsf_string.c_str(), false); + + if (!all_input_aps.has_value() && !all_output_aps.has_value()) + { + static char arg5[] = "--print-output-signals"; + char* command[] = { arg0, arg5, opt_tlsf, nullptr }; + std::string res = read_stdout_of_command(command); + + all_output_aps.emplace(std::vector{}); + split_aps(res, *all_output_aps); + } + } + check_no_formula(); // Check if inputs and outputs are distinct diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 45b4b2b1c..f05d58309 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -104,14 +104,20 @@ specification language created for the purpose of this competition. Fortunately, the SYNTCOMP organizers also provide a tool called [[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula. -The following four steps show you how a TLSF specification called =FILE= can +The following line shows how a TLSF specification called =FILE= can be synthesized using =syfco= and =ltlsynt=: #+BEGIN_SRC sh :export code -LTL=$(syfco FILE -f ltlxba -m fully) -IN=$(syfco FILE --print-input-signals) -OUT=$(syfco FILE --print-output-signals) -ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT" +ltlsynt --tlsf FILE +#+END_SRC + +The above =--tlsf= option will call =syfco= to perform the conversion +and extract output signals, as if you had used: + +#+BEGIN_SRC sh :export code +LTL=$(syfco -f ltlxba -m fully FILE) +OUT=$(syfco --print-output-signals FILE) +ltlsynt --formula="$LTL" --outs="$OUT" #+END_SRC * Internal details diff --git a/tests/Makefile.am b/tests/Makefile.am index c8a722f5c..3582a8493 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -342,6 +342,7 @@ TESTS_twa = \ core/parity.test \ core/parity2.test \ core/ltlsynt.test \ + core/syfco.test \ core/rabin2parity.test \ core/twacube.test diff --git a/tests/core/syfco.test b/tests/core/syfco.test new file mode 100755 index 000000000..b63f729a8 --- /dev/null +++ b/tests/core/syfco.test @@ -0,0 +1,48 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2022 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 . + +. ./defs || exit 1 +set -e + +# Test that we can pass a tlsf specification to ltlsynt. This +# only work if syfco is installed. + +(syfco --version) || exit 77 + +cat >test.tlsf < X(out)); } +} +EOF + +test REALIZABLE = `ltlsynt --tlsf test.tlsf --realizability` +test UNREALIZABLE = `ltlsynt --tlsf test.tlsf --outs=foo --realizability` +test UNREALIZABLE = `ltlsynt --outs=foo --tlsf test.tlsf --realizability` + +ltlsynt --tlsf test.tlsf --tlsf test.tlsf 2>stderr && exit 0 +grep 'option --tlsf may only be used once' stderr