diff --git a/bin/Makefile.am b/bin/Makefile.am
index b665d859c..c92cdf6f6 100644
--- a/bin/Makefile.am
+++ b/bin/Makefile.am
@@ -43,6 +43,8 @@ libcommon_a_SOURCES = \
common_finput.hh \
common_hoaread.cc \
common_hoaread.hh \
+ common_ioap.cc \
+ common_ioap.hh \
common_output.cc \
common_output.hh \
common_post.cc \
diff --git a/bin/common_ioap.cc b/bin/common_ioap.cc
new file mode 100644
index 000000000..d38a190aa
--- /dev/null
+++ b/bin/common_ioap.cc
@@ -0,0 +1,166 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// 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 .
+
+#include "common_ioap.hh"
+#include "error.h"
+#include
+
+// --ins and --outs, as supplied on the command-line
+std::optional> all_output_aps;
+std::optional> all_input_aps;
+
+// Store refirst, separate the filters that are regular expressions from
+// the others. Compile the regular expressions while we are at it.
+std::vector regex_in;
+std::vector regex_out;
+// map identifier to input/output (false=input, true=output)
+std::unordered_map identifier_map;
+
+static std::string
+str_tolower(std::string s)
+{
+ std::transform(s.begin(), s.end(), s.begin(),
+ [](unsigned char c){ return std::tolower(c); });
+ return s;
+}
+
+void
+split_aps(const 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));
+ }
+}
+
+void process_io_options()
+{
+ // Filter identifiers from regexes.
+ if (all_input_aps.has_value())
+ for (const std::string& f: *all_input_aps)
+ {
+ unsigned sz = f.size();
+ if (f[0] == '/' && f[sz - 1] == '/')
+ regex_in.push_back(std::regex(f.substr(1, sz - 2)));
+ else
+ identifier_map.emplace(f, false);
+ }
+ if (all_output_aps.has_value())
+ for (const std::string& f: *all_output_aps)
+ {
+ unsigned sz = f.size();
+ if (f[0] == '/' && f[sz - 1] == '/')
+ regex_out.push_back(std::regex(f.substr(1, sz - 2)));
+ else if (auto [it, is_new] = identifier_map.try_emplace(f, true);
+ !is_new && !it->second)
+ error(2, 0, "'%s' appears in both --ins and --outs",
+ f.c_str());
+ }
+}
+
+static std::unordered_set
+list_aps_in_formula(spot::formula f)
+{
+ std::unordered_set aps;
+ f.traverse([&aps](spot::formula s) {
+ if (s.is(spot::op::ap))
+ aps.emplace(s.ap_name());
+ return false;
+ });
+ return aps;
+}
+
+// Takes a set of the atomic propositions appearing in the formula,
+// and separate them into two vectors: input APs and output APs.
+std::pair, std::vector>
+filter_list_of_aps(spot::formula f, const char* filename, int linenum)
+{
+ std::unordered_set aps = list_aps_in_formula(f);
+ // now iterate over the list of atomic propositions to filter them
+ std::vector matched[2]; // 0 = input, 1 = output
+ for (const std::string& a: aps)
+ {
+ if (auto it = identifier_map.find(a); it != identifier_map.end())
+ {
+ matched[it->second].push_back(a);
+ continue;
+ }
+
+ bool found_in = false;
+ for (const std::regex& r: regex_in)
+ if (std::regex_search(a, r))
+ {
+ found_in = true;
+ break;
+ }
+ bool found_out = false;
+ for (const std::regex& r: regex_out)
+ if (std::regex_search(a, r))
+ {
+ found_out = true;
+ break;
+ }
+ if (all_input_aps.has_value() == all_output_aps.has_value())
+ {
+ if (!all_input_aps.has_value())
+ {
+ // If the atomic proposition hasn't been classified
+ // because neither --ins nor --out were specified,
+ // attempt to classify automatically using the first
+ // letter.
+ int fl = a[0];
+ if (fl == 'i' || fl == 'I')
+ found_in = true;
+ else if (fl == 'o' || fl == 'O')
+ found_out = true;
+ }
+ if (found_in && found_out)
+ error_at_line(2, 0, filename, linenum,
+ "'%s' matches both --ins and --outs",
+ a.c_str());
+ if (!found_in && !found_out)
+ {
+ if (all_input_aps.has_value() || all_output_aps.has_value())
+ error_at_line(2, 0, filename, linenum,
+ "one of --ins or --outs should match '%s'",
+ a.c_str());
+ else
+ error_at_line(2, 0, filename, linenum,
+ "since '%s' does not start with 'i' or 'o', "
+ "it is unclear if it is an input or "
+ "an output;\n use --ins or --outs",
+ a.c_str());
+ }
+ }
+ else
+ {
+ // if we had only --ins or only --outs, anything not
+ // matching that was given is assumed to belong to the
+ // other one.
+ if (!all_input_aps.has_value() && !found_out)
+ found_in = true;
+ else if (!all_output_aps.has_value() && !found_in)
+ found_out = true;
+ }
+ matched[found_out].push_back(a);
+ }
+ return {matched[0], matched[1]};
+}
diff --git a/bin/common_ioap.hh b/bin/common_ioap.hh
new file mode 100644
index 000000000..960b26a8a
--- /dev/null
+++ b/bin/common_ioap.hh
@@ -0,0 +1,51 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// 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 .
+
+#pragma once
+
+#include "common_sys.hh"
+#include
+#include
+#include
+#include
+#include
+#include
+
+// --ins and --outs, as supplied on the command-line
+extern std::optional> all_output_aps;
+extern std::optional> all_input_aps;
+
+// Comma-separated list of strings, such as those passed to --ins/--outs
+void split_aps(const std::string& arg, std::vector& where);
+
+// process the all_output_aps and all_input_aps above to
+// fill regex_in, regex_out, and identifier_map.
+void process_io_options();
+
+// Store refirst, separate the filters that are regular expressions from
+// the others. Compile the regular expressions while we are at it.
+extern std::vector regex_in;
+extern std::vector regex_out;
+// map identifier to input/output (false=input, true=output)
+extern std::unordered_map identifier_map;
+
+// Separate the set of the atomic propositions appearing in f, into
+// two vectors: input APs and output APs, becased on regex_in,
+// regex_out, and identifier_map.
+std::pair, std::vector>
+filter_list_of_aps(spot::formula f, const char* filename, int linenum);
diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 456d2cb41..9e7aee595 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -26,6 +26,7 @@
#include "common_setup.hh"
#include "common_sys.hh"
#include "common_trans.hh"
+#include "common_ioap.hh"
#include
#include
@@ -43,7 +44,6 @@
#include
#include
#include
-#include
enum
{
@@ -178,17 +178,6 @@ Exit status:\n\
1 if at least one input problem was not realizable\n\
2 if any error has been reported";
-// --ins and --outs, as supplied on the command-line
-static std::optional> all_output_aps;
-static std::optional> all_input_aps;
-
-// first, separate the filters that are regular expressions from
-// the others. Compile the regular expressions while we are at it.
-static std::vector regex_in;
-static std::vector regex_out;
-// map identifier to input/output (false=input, true=output)
-static std::unordered_map identifier_map;
-
static const char* opt_csv = nullptr;
static bool opt_print_pg = false;
static bool opt_print_hoa = false;
@@ -323,14 +312,6 @@ namespace
return opt_print_pg || opt_print_hoa;
}
- auto str_tolower = [] (std::string s)
- {
- std::transform(s.begin(), s.end(), s.begin(),
- [](unsigned char c){ return std::tolower(c); });
- return s;
- };
-
-
static void
dispatch_print_hoa(spot::twa_graph_ptr& game,
const spot::realizability_simplifier* rs = nullptr)
@@ -753,108 +734,6 @@ namespace
return 0;
}
- static void
- split_aps(const 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 std::unordered_set
- list_aps_in_formula(spot::formula f)
- {
- std::unordered_set aps;
- f.traverse([&aps](spot::formula s) {
- if (s.is(spot::op::ap))
- aps.emplace(s.ap_name());
- return false;
- });
- return aps;
- }
-
- // Takes a set of the atomic propositions appearing in the formula,
- // and separate them into two vectors: input APs and output APs.
- static std::pair, std::vector>
- filter_list_of_aps(const std::unordered_set& aps,
- const char* filename, int linenum)
- {
- // now iterate over the list of atomic propositions to filter them
- std::vector matched[2]; // 0 = input, 1 = output
- for (const std::string& a: aps)
- {
- if (auto it = identifier_map.find(a); it != identifier_map.end())
- {
- matched[it->second].push_back(a);
- continue;
- }
-
- bool found_in = false;
- for (const std::regex& r: regex_in)
- if (std::regex_search(a, r))
- {
- found_in = true;
- break;
- }
- bool found_out = false;
- for (const std::regex& r: regex_out)
- if (std::regex_search(a, r))
- {
- found_out = true;
- break;
- }
- if (all_input_aps.has_value() == all_output_aps.has_value())
- {
- if (!all_input_aps.has_value())
- {
- // If the atomic proposition hasn't been classified
- // because neither --ins nor --out were specified,
- // attempt to classify automatically using the first
- // letter.
- int fl = a[0];
- if (fl == 'i' || fl == 'I')
- found_in = true;
- else if (fl == 'o' || fl == 'O')
- found_out = true;
- }
- if (found_in && found_out)
- error_at_line(2, 0, filename, linenum,
- "'%s' matches both --ins and --outs",
- a.c_str());
- if (!found_in && !found_out)
- {
- if (all_input_aps.has_value() || all_output_aps.has_value())
- error_at_line(2, 0, filename, linenum,
- "one of --ins or --outs should match '%s'",
- a.c_str());
- else
- error_at_line(2, 0, filename, linenum,
- "since '%s' does not start with 'i' or 'o', "
- "it is unclear if it is an input or "
- "an output;\n use --ins or --outs",
- a.c_str());
- }
- }
- else
- {
- // if we had only --ins or only --outs, anything not
- // matching was was given is assumed to belong to the
- // other one.
- if (!all_input_aps.has_value() && !found_out)
- found_in = true;
- else if (!all_output_aps.has_value() && !found_in)
- found_out = true;
- }
- matched[found_out].push_back(a);
- }
- return {matched[0], matched[1]};
- }
-
-
class ltl_processor final : public job_processor
{
@@ -866,9 +745,8 @@ namespace
int process_formula(spot::formula f,
const char* filename, int linenum) override
{
- std::unordered_set aps = list_aps_in_formula(f);
auto [input_aps, output_aps] =
- filter_list_of_aps(aps, filename, linenum);
+ filter_list_of_aps(f, filename, linenum);
int res = solve_formula(f, input_aps, output_aps);
if (opt_csv)
print_csv(f);
@@ -1193,28 +1071,7 @@ main(int argc, char **argv)
exit(err);
check_no_formula();
-
- // Filter identifiers from regexes.
- if (all_input_aps.has_value())
- for (const std::string& f: *all_input_aps)
- {
- unsigned sz = f.size();
- if (f[0] == '/' && f[sz - 1] == '/')
- regex_in.push_back(std::regex(f.substr(1, sz - 2)));
- else
- identifier_map.emplace(f, false);
- }
- if (all_output_aps.has_value())
- for (const std::string& f: *all_output_aps)
- {
- unsigned sz = f.size();
- if (f[0] == '/' && f[sz - 1] == '/')
- regex_out.push_back(std::regex(f.substr(1, sz - 2)));
- else if (auto [it, is_new] = identifier_map.try_emplace(f, true);
- !is_new && !it->second)
- error(2, 0, "'%s' appears in both --ins and --outs",
- f.c_str());
- }
+ process_io_options();
ltl_processor processor;
if (int res = processor.run(); res == 0 || res == 1)