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

bin/ltlfilt: Use is_persistence() and is_recurrence()

Browse source 
* bin/ltlfilt.cc: Use them.
This commit is contained in:
Alexandre GBAGUIDI AISSE 2017-07-28 13:49:11 +02:00
parent c827f75c37
commit 96974f7c97
1 changed files with 11 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

42
bin/ltlfilt.cc
View file

@ -46,6 +46,7 @@
#include <spot/tl/exclusive.hh> #include <spot/tl/exclusive.hh>
#include <spot/tl/ltlf.hh> #include <spot/tl/ltlf.hh>
#include <spot/tl/print.hh> #include <spot/tl/print.hh>
#include <spot/tl/hierarchy.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh> #include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/minimize.hh> #include <spot/twaalgos/minimize.hh>
@ -707,6 +708,7 @@ namespace
matched = false; matched = false;
break; break;
} }
} }
// Some combinations of options can be simplified. // Some combinations of options can be simplified.
@ -725,18 +727,15 @@ namespace
&& (!safety || f.is_syntactic_safety()) && (!safety || f.is_syntactic_safety())
&& (!obligation || f.is_syntactic_obligation()))) && (!obligation || f.is_syntactic_obligation())))
{ {
if (persistence)
aut = ltl_to_tgba_fm(spot::formula::Not(f),
simpl.get_dict(), true);
else if (!aut)
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
// Match obligations and subclasses using WDBA minimization. // Match obligations and subclasses using WDBA minimization.
// Because this is costly, we compute it later, so that we don't // Because this is costly, we compute it later, so that we don't
// have to compute it on formulas that have been discarded for // have to compute it on formulas that have been discarded for
// other reasons. // other reasons.
if (obligation) if (obligation)
{ {
if (!aut)
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
auto min = minimize_obligation(aut, f); auto min = minimize_obligation(aut, f);
assert(min); assert(min);
if (aut == min) if (aut == min)
@ -752,31 +751,12 @@ namespace
matched &= !safety || is_safety_automaton(min, &si); matched &= !safety || is_safety_automaton(min, &si);
} }
} }
// Recurrence properties are those that can be translated to
// deterministic BA. Persistence are those whose negation else if (persistence)
// can be represented as DBA. matched &= spot::is_persistence(f);
else if (!is_deterministic(aut))
{ else if (recurrence)
assert(recurrence || persistence); matched &= spot::is_recurrence(f, aut);
// if aut is a non-deterministic TGBA, we do
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
// BA will preserve determinism if possible.
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dra = p.run(aut);
if (dra->acc().is_generalized_buchi())
{
assert(is_deterministic(dra));
}
else
{
auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra));
assert(ba);
matched &= is_deterministic(ba);
}
}
} }
} }