ltlsynt: fix the case where AP removal is disabled and decomp fails
* bin/ltlsynt.cc: Correctly update the output variables in the case decomposition failed and AP removal is disabled. * tests/core/ltlsynt.test: Add a test case.
This commit is contained in:
parent
15b876d368
commit
82311c3e3b
2 changed files with 10 additions and 0 deletions
|
|
@ -467,6 +467,12 @@ namespace
|
||||||
sub_outs[0].insert(ap);
|
sub_outs[0].insert(ap);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
for (const std::string& apstr: output_aps)
|
||||||
|
sub_outs[0].insert(spot::formula::ap(apstr));
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
std::vector<std::vector<std::string>> sub_outs_str;
|
std::vector<std::vector<std::string>> sub_outs_str;
|
||||||
std::transform(sub_outs.begin(), sub_outs.end(),
|
std::transform(sub_outs.begin(), sub_outs.end(),
|
||||||
|
|
|
||||||
|
|
@ -1143,3 +1143,7 @@ ltlsynt --ins='/^in/,/env/' --outs='/^out/,/control/' \
|
||||||
-f 'G(controlenv <-> input)' 2>err && :
|
-f 'G(controlenv <-> input)' 2>err && :
|
||||||
test $? -eq 2
|
test $? -eq 2
|
||||||
grep 'controlenv.*matches both' err
|
grep 'controlenv.*matches both' err
|
||||||
|
|
||||||
|
|
||||||
|
ltlsynt --polarity=1 --global-e=1 -f 'G(i -> Xo) & G(!i -> F!o)' --real
|
||||||
|
ltlsynt --polarity=0 --global-e=0 -f 'G(i -> Xo) & G(!i -> F!o)' --real
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue