alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: don't fail if --outs or --ins is set to empty

Browse source 
* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: add tests
This commit is contained in:
Florian Renkin 2022-03-21 10:46:42 +01:00 • committed by Alexandre Duret-Lutz
parent 53118d9314
commit d1f49c721a
2 changed files with 40 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

56
bin/ltlsynt.cc
View file

@ -135,8 +135,8 @@ Exit status:\n\
1 if the input problem is not realizable\n\ 1 if the input problem is not realizable\n\
2 if any error has been reported"; 2 if any error has been reported";
static std::vector<std::string> all_output_aps; static std::optional<std::vector<std::string>> all_output_aps;
static std::vector<std::string> all_input_aps; static std::optional<std::vector<std::string>> all_input_aps;
static const char* opt_csv = nullptr; static const char* opt_csv = nullptr;
static bool opt_print_pg = false; static bool opt_print_pg = false;
@ -577,12 +577,12 @@ namespace
class ltl_processor final : public job_processor class ltl_processor final : public job_processor
{ {
private: private:
std::vector<std::string> input_aps_; std::optional<std::vector<std::string>> input_aps_;
std::vector<std::string> output_aps_; std::optional<std::vector<std::string>> output_aps_;
public: public:
ltl_processor(std::vector<std::string> input_aps_, ltl_processor(std::optional<std::vector<std::string>> input_aps_,
std::vector<std::string> output_aps_) std::optional<std::vector<std::string>> output_aps_)
: input_aps_(std::move(input_aps_)), : input_aps_(std::move(input_aps_)),
output_aps_(std::move(output_aps_)) output_aps_(std::move(output_aps_))
{ {
@ -592,11 +592,13 @@ namespace
const char* filename, int linenum) override const char* filename, int linenum) override
{ {
auto unknown_aps = [](spot::formula f, auto unknown_aps = [](spot::formula f,
const std::vector<std::string>& known, const std::optional<std::vector<std::string>>& known,
const std::vector<std::string>* known2 = nullptr) const std::optional<std::vector<std::string>>& known2 = {})
{ {
std::vector<std::string> unknown; std::vector<std::string> unknown;
std::set<spot::formula> seen; std::set<spot::formula> seen;
// If we don't have --ins and --outs, we must not find an AP.
bool can_have_ap = known.has_value();
f.traverse([&](const spot::formula& s) f.traverse([&](const spot::formula& s)
{ {
if (s.is(spot::op::ap)) if (s.is(spot::op::ap))
@ -604,10 +606,11 @@ namespace
if (!seen.insert(s).second) if (!seen.insert(s).second)
return false; return false;
const std::string& a = s.ap_name(); const std::string& a = s.ap_name();
if (std::find(known.begin(), known.end(), a) == known.end() if (!can_have_ap
&& (!known2 || (std::find(known->begin(), known->end(), a) == known->end()
&& (!known2.has_value()
|| std::find(known2->begin(), || std::find(known2->begin(),
known2->end(), a) == known2->end())) known2->end(), a) == known2->end())))
unknown.push_back(a); unknown.push_back(a);
} }
return false; return false;
@ -617,30 +620,30 @@ namespace
// Decide which atomic propositions are input or output. // Decide which atomic propositions are input or output.
int res; int res;
if (input_aps_.empty() && !output_aps_.empty()) if (!input_aps_.has_value() && output_aps_.has_value())
{ {
res = solve_formula(f, unknown_aps(f, output_aps_), output_aps_); res = solve_formula(f, unknown_aps(f, output_aps_), *output_aps_);
} }
else if (output_aps_.empty() && !input_aps_.empty()) else if (!output_aps_.has_value() && input_aps_.has_value())
{ {
res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_)); res = solve_formula(f, *input_aps_, unknown_aps(f, input_aps_));
} }
else if (output_aps_.empty() && input_aps_.empty()) else if (!output_aps_.has_value() && !input_aps_.has_value())
{ {
for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_)) for (const std::string& ap: unknown_aps(f, input_aps_, output_aps_))
error_at_line(2, 0, filename, linenum, error_at_line(2, 0, filename, linenum,
"one of --ins or --outs should list '%s'", "one of --ins or --outs should list '%s'",
ap.c_str()); ap.c_str());
res = solve_formula(f, input_aps_, output_aps_); res = solve_formula(f, *input_aps_, *output_aps_);
} }
else else
{ {
for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_)) for (const std::string& ap: unknown_aps(f, input_aps_, output_aps_))
error_at_line(2, 0, filename, linenum, error_at_line(2, 0, filename, linenum,
"both --ins and --outs are specified, " "both --ins and --outs are specified, "
"but '%s' is unlisted", "but '%s' is unlisted",
ap.c_str()); ap.c_str());
res = solve_formula(f, input_aps_, output_aps_); res = solve_formula(f, *input_aps_, *output_aps_);
} }
if (opt_csv) if (opt_csv)
@ -671,23 +674,25 @@ parse_opt(int key, char *arg, struct argp_state *)
break; break;
case OPT_INPUT: case OPT_INPUT:
{ {
all_input_aps.emplace(std::vector<std::string>{});
std::istringstream aps(arg); std::istringstream aps(arg);
std::string ap; std::string ap;
while (std::getline(aps, ap, ',')) while (std::getline(aps, ap, ','))
{ {
ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
all_input_aps.push_back(str_tolower(ap)); all_input_aps->push_back(str_tolower(ap));
} }
break; break;
} }
case OPT_OUTPUT: case OPT_OUTPUT:
{ {
all_output_aps.emplace(std::vector<std::string>{});
std::istringstream aps(arg); std::istringstream aps(arg);
std::string ap; std::string ap;
while (std::getline(aps, ap, ',')) while (std::getline(aps, ap, ','))
{ {
ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
all_output_aps.push_back(str_tolower(ap)); all_output_aps->push_back(str_tolower(ap));
} }
break; break;
} }
@ -748,9 +753,10 @@ main(int argc, char **argv)
check_no_formula(); check_no_formula();
// Check if inputs and outputs are distinct // Check if inputs and outputs are distinct
for (const std::string& ai : all_input_aps) if (all_input_aps.has_value() && all_output_aps.has_value())
if (std::find(all_output_aps.begin(), all_output_aps.end(), ai) for (const std::string& ai : *all_input_aps)
!= all_output_aps.end()) if (std::find(all_output_aps->begin(), all_output_aps->end(), ai)
!= all_output_aps->end())
error(2, 0, "'%s' appears both in --ins and --outs", ai.c_str()); error(2, 0, "'%s' appears both in --ins and --outs", ai.c_str());
ltl_processor processor(all_input_aps, all_output_aps); ltl_processor processor(all_input_aps, all_output_aps);

8
tests/core/ltlsynt.test
View file

@ -821,3 +821,11 @@ ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \
--verbose --aiger 2> out || true --verbose --aiger 2> out || true
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp diff outx exp
ltlsynt --ins="" -f "GFa"
ltlsynt --outs="" -f "GFb" | grep "UNREALIZABLE"
ltlsynt --outs="" -f "1"
ltlsynt --outs="" --ins="" -f "GFa" 2>&1 | \
grep "both --ins and --outs are specified"