From 04d718ab9cd8efc8c6b7953468a9eef2ec58bd2e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jun 2022 15:20:54 +0200 Subject: [PATCH] ltlsynt: support multiple --tlsf options * bin/common_finput.cc, bin/common_finput.hh: Add support for process_tlsf_file. * bin/ltlsynt.cc: Implement it. * tests/core/syfco.test: Adjust test case. --- bin/common_finput.cc | 9 +++++ bin/common_finput.hh | 6 +++- bin/ltlsynt.cc | 81 +++++++++++++++++++++++-------------------- tests/core/syfco.test | 7 ++-- 4 files changed, 63 insertions(+), 40 deletions(-) diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 8e78b5599..80aca5df7 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -308,6 +308,12 @@ job_processor::process_aut_file(const char*) throw std::runtime_error("process_aut_file not defined for this tool"); } +int +job_processor::process_tlsf_file(const char*) +{ + throw std::runtime_error("process_tlsf_file not defined for this tool"); +} + int job_processor::process_ltl_file(const char* filename) { @@ -377,6 +383,9 @@ job_processor::run() case job_type::AUT_FILENAME: error |= process_aut_file(j.str); break; + case job_type::TLSF_FILENAME: + error |= process_tlsf_file(j.str); + break; default: throw std::runtime_error("unexpected job type"); } diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 44a78bada..2a5815fc3 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -27,7 +27,8 @@ enum class job_type : char { LTL_STRING, LTL_FILENAME, - AUT_FILENAME }; + AUT_FILENAME, + TLSF_FILENAME }; struct job { @@ -77,6 +78,9 @@ public: virtual int process_aut_file(const char* filename); + virtual int + process_tlsf_file(const char* filename); + virtual int run(); diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 0d89c2fc5..b5d4289f5 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -157,8 +157,6 @@ 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; @@ -582,6 +580,18 @@ namespace return 0; } + 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)); + } + } + class ltl_processor final : public job_processor { private: @@ -658,19 +668,40 @@ namespace print_csv(f); return res; } - }; -} -static void -split_aps(std::string arg, std::vector& where) -{ - std::istringstream aps(arg); - std::string ap; - while (std::getline(aps, ap, ',')) + int + process_tlsf_file(const char* filename) override { - ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); - where.push_back(str_tolower(ap)); + 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, + const_cast(filename), nullptr }; + std::string tlsf_string = read_stdout_of_command(command); + + // The set of atomic proposition will be temporary set to those + // given by syfco, unless they were forced from the command-line. + bool reset_aps = false; + if (!input_aps_.has_value() && !output_aps_.has_value()) + { + reset_aps = true; + static char arg5[] = "--print-output-signals"; + char* command[] = { arg0, arg5, + const_cast(filename), nullptr }; + std::string res = read_stdout_of_command(command); + + output_aps_.emplace(std::vector{}); + split_aps(res, *output_aps_); + } + int res = process_string(tlsf_string, filename); + if (reset_aps) + output_aps_.reset(); + return res; } + + }; } static int @@ -726,9 +757,7 @@ parse_opt(int key, char *arg, struct argp_state *) simplify_args, simplify_values); break; case OPT_TLSF: - if (opt_tlsf) - error(2, 0, "option --tlsf may only be used once"); - opt_tlsf = arg; + jobs.emplace_back(arg, job_type::TLSF_FILENAME); break; case OPT_VERBOSE: gi->verbose_stream = &std::cerr; @@ -767,28 +796,6 @@ main(int argc, char **argv) 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(), job_type::LTL_STRING); - - 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/tests/core/syfco.test b/tests/core/syfco.test index b63f729a8..7141f0b4c 100755 --- a/tests/core/syfco.test +++ b/tests/core/syfco.test @@ -44,5 +44,8 @@ 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 +# --tlsf can be used several time +ltlsynt --tlsf test.tlsf > out1 +ltlsynt --tlsf test.tlsf --tlsf test.tlsf > out2 +cat out1 out1 > out11 +diff out11 out2