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

ltlsynt: improve error message in case of missing --ins and --outs

Browse source 
* bin/ltlsynt.cc: Here.
* tests/core/ltlsynt.test: Test the error.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-22 17:46:21 +02:00
parent c43712682f
commit 074678416f
2 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
bin/ltlsynt.cc
View file

@ -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_))

5
tests/core/ltlsynt.test
View file

@ -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