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

neverclaim: do not pass the formula

Browse source 
* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh: Do not
pass the formula.  Use the automaton name instead.
* src/tgbatest/ltl2tgba.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-04 18:01:24 +01:00
parent 490c97d797
commit 892fb11f04
3 changed files with 13 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbatest/ltl2tgba.cc
View file

@ -1596,7 +1596,7 @@ checked_main(int argc, char** argv)
{
assert(degeneralize_opt == DegenSBA);
if (assume_sba)
spot::never_claim_reachable(std::cout, a, f, spin_comments);
spot::never_claim_reachable(std::cout, a, spin_comments);
else
{
// It is possible that we have applied other
@ -1604,7 +1604,7 @@ checked_main(int argc, char** argv)
// degeneralization. Let's degeneralize again!
auto s = spot::degeneralize(ensure_digraph(a), degen_reset,
degen_order, degen_cache);
spot::never_claim_reachable(std::cout, s, f, spin_comments);
spot::never_claim_reachable(std::cout, s, spin_comments);
}
break;
}