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

ltlsynt: report AP missing from --ins and --outs

Browse source 
* bin/ltlsynt.cc (process_formula): Add a check.
* tests/core/ltlsynt.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-09 21:18:21 +02:00
parent 0e5f2d4819
commit 82d4fc8ed9
2 changed files with 34 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

33
bin/ltlsynt.cc
View file

@ -555,10 +555,12 @@ namespace
{ {
} }
int process_formula(spot::formula f, const char*, int) override int process_formula(spot::formula f,
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::vector<std::string>& known,
const std::vector<std::string>* known2 = nullptr)
{ {
std::vector<std::string> unknown; std::vector<std::string> unknown;
std::set<spot::formula> seen; std::set<spot::formula> seen;
@ -569,7 +571,10 @@ 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 (std::find(known.begin(), known.end(), a) == known.end()
&& (!known2
|| std::find(known2->begin(),
known2->end(), a) == known2->end()))
unknown.push_back(a); unknown.push_back(a);
} }
return false; return false;
@ -580,11 +585,22 @@ 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_.empty() && !output_aps_.empty())
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_.empty() && !input_aps_.empty())
res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_)); {
res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_));
}
else else
res = solve_formula(f, input_aps_, output_aps_); {
for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_))
error_at_line(2, 0, filename, linenum,
"both --ins and --outs are specified, "
"but '%s' is unlisted",
ap.c_str());
res = solve_formula(f, input_aps_, output_aps_);
}
if (opt_csv) if (opt_csv)
print_csv(f); print_csv(f);
@ -691,11 +707,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 auto& ai : all_input_aps) for (const std::string& ai : all_input_aps)
if (std::find(all_output_aps.begin(), all_output_aps.end(), ai) if (std::find(all_output_aps.begin(), all_output_aps.end(), ai)
!= all_output_aps.end()) != all_output_aps.end())
throw std::runtime_error("ltlsynt(): " + ai + error(2, 0, "'%s' appears both in --ins and --outs", ai.c_str());
" appears in the input AND output APs.");
ltl_processor processor(all_input_aps, all_output_aps); ltl_processor processor(all_input_aps, all_output_aps);
if (int res = processor.run(); res == 0 || res == 1) if (int res = processor.run(); res == 0 || res == 1)

11
tests/core/ltlsynt.test
View file

@ -243,7 +243,7 @@ diff outx exp
for r in '' '--real'; do for r in '' '--real'; do
opts="$r --ins=a --outs=b -f" opts="$r --ins=a,c --outs=b -f"
ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || : ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
@ -533,3 +533,12 @@ ltlsynt --ins=a,b -f 'G (a & b <=> c)' >stdout
diff stdout expected diff stdout expected
ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout
diff stdout expected diff stdout expected
ltlsynt --ins=a,b --outs=c,a -f 'GFa | FGc | GFb' 2>stderr && :
test $? -eq 2
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