diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 87805801b..64cbde3fd 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -592,6 +592,14 @@ namespace { res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_)); } + else if (output_aps_.empty() && input_aps_.empty()) + { + for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_)) + error_at_line(2, 0, filename, linenum, + "one of --ins or --outs should list '%s'", + ap.c_str()); + res = solve_formula(f, input_aps_, output_aps_); + } else { for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_)) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index f1f0a458b..d2427ea1a 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -541,4 +541,7 @@ grep "'a' appears both" stderr ltlsynt --ins=a --outs=c -f 'GFa | FGb | GFc' 2>stderr && : test $? -eq 2 -grep "but 'b' is unlisted" stderr +grep "both.*but 'b' is unlisted" stderr +ltlsynt -f 'GFa | FGb | GFc' 2>stderr && : +test $? -eq 2 +grep "one of --ins or --outs" stderr