From 074678416ff6cc9529888d952e9bd92cf65c57ba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Oct 2021 17:46:21 +0200 Subject: [PATCH] ltlsynt: improve error message in case of missing --ins and --outs * bin/ltlsynt.cc: Here. * tests/core/ltlsynt.test: Test the error. --- bin/ltlsynt.cc | 8 ++++++++ tests/core/ltlsynt.test | 5 ++++- 2 files changed, 12 insertions(+), 1 deletion(-) 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