partial_degeneralize: a support for disjunction of Fin
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh: Implement this. Also throw a runtime error in case were todegen does not match any subformula. * tests/python/pdegen.py: Add tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
f1008c156b
commit
f9e75de647
4 changed files with 120 additions and 26 deletions
3
NEWS
3
NEWS
|
|
@ -59,7 +59,8 @@ New in spot 2.8.5.dev (not yet released)
|
|||
|
||||
- partial_degeneralize() is a new function performing partial
|
||||
degeneralization to get rid of conjunctions of Inf terms in
|
||||
acceptance conditions.
|
||||
acceptance conditions. This also works with disjunctions of
|
||||
Fin terms in deterministic automata.
|
||||
|
||||
- simplify_acceptance_here() and simplify_acceptance() learned to
|
||||
simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@
|
|||
#include <memory>
|
||||
#include <spot/twaalgos/sccinfo.hh>
|
||||
#include <spot/twa/bddprint.hh>
|
||||
#include <spot/twaalgos/isdet.hh>
|
||||
|
||||
//#define DEGEN_DEBUG
|
||||
|
||||
|
|
@ -738,7 +739,8 @@ namespace spot
|
|||
namespace
|
||||
{
|
||||
static acc_cond::mark_t
|
||||
to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen)
|
||||
to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen,
|
||||
bool also_fin)
|
||||
{
|
||||
if (code.empty())
|
||||
return todegen;
|
||||
|
|
@ -753,38 +755,42 @@ namespace spot
|
|||
case acc_cond::acc_op::Or:
|
||||
--pos;
|
||||
break;
|
||||
case acc_cond::acc_op::Fin:
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
if (!also_fin)
|
||||
{
|
||||
pos -= 2;
|
||||
tostrip -= code[pos].mark;
|
||||
break;
|
||||
}
|
||||
// Handle Fin and Inf in the same way
|
||||
SPOT_FALLTHROUGH;
|
||||
case acc_cond::acc_op::Inf:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
pos -= 2;
|
||||
if (code[pos].mark != todegen)
|
||||
tostrip -= code[pos].mark;
|
||||
break;
|
||||
case acc_cond::acc_op::Fin:
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
pos -= 2;
|
||||
tostrip -= code[pos].mark;
|
||||
break;
|
||||
}
|
||||
}
|
||||
while (pos > 0);
|
||||
return tostrip;
|
||||
}
|
||||
|
||||
static void
|
||||
static bool
|
||||
update_acc_for_partial_degen(acc_cond::acc_code& code,
|
||||
acc_cond::mark_t todegen,
|
||||
acc_cond::mark_t tostrip,
|
||||
acc_cond::mark_t accmark)
|
||||
acc_cond::mark_t accmark,
|
||||
bool also_fin)
|
||||
{
|
||||
if (!todegen)
|
||||
if (!todegen || code.empty())
|
||||
{
|
||||
code &= acc_cond::acc_code::inf(accmark);
|
||||
return;
|
||||
return true;
|
||||
}
|
||||
|
||||
if (code.empty())
|
||||
return;
|
||||
|
||||
bool updated = false;
|
||||
unsigned pos = code.size();
|
||||
do
|
||||
{
|
||||
|
|
@ -794,26 +800,46 @@ namespace spot
|
|||
case acc_cond::acc_op::Or:
|
||||
--pos;
|
||||
break;
|
||||
case acc_cond::acc_op::Fin:
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
if (!also_fin)
|
||||
{
|
||||
pos -= 2;
|
||||
code[pos].mark = code[pos].mark.strip(tostrip);
|
||||
break;
|
||||
}
|
||||
// Handle Fin and Inf in the same way
|
||||
SPOT_FALLTHROUGH;
|
||||
case acc_cond::acc_op::Inf:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
pos -= 2;
|
||||
if (code[pos].mark == todegen)
|
||||
{
|
||||
code[pos].mark = accmark;
|
||||
updated = true;
|
||||
}
|
||||
else
|
||||
{
|
||||
code[pos].mark = code[pos].mark.strip(tostrip);
|
||||
break;
|
||||
case acc_cond::acc_op::Fin:
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
pos -= 2;
|
||||
code[pos].mark = code[pos].mark.strip(tostrip);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
while (pos > 0);
|
||||
return updated;
|
||||
}
|
||||
|
||||
|
||||
|
||||
[[noreturn]] static void
|
||||
report_invalid_partial_degen_arg(acc_cond::mark_t todegen,
|
||||
acc_cond::acc_code& cond)
|
||||
{
|
||||
std::ostringstream err;
|
||||
err << "partial_degeneralize(): " << todegen
|
||||
<< " does not match any degeneralizable subformula of "
|
||||
<< cond << '.';
|
||||
throw std::runtime_error(err.str());
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -825,11 +851,17 @@ namespace spot
|
|||
res->copy_ap_of(a);
|
||||
acc_cond::acc_code acc = a->get_acceptance();
|
||||
|
||||
acc_cond::mark_t tostrip = to_strip(acc, todegen);
|
||||
// We can also degeneralize disjunctions of Fin if the input is
|
||||
// deterministic.
|
||||
bool also_fin = a->acc().uses_fin_acceptance() && is_deterministic(a);
|
||||
|
||||
acc_cond::mark_t tostrip = to_strip(acc, todegen, also_fin);
|
||||
acc_cond::mark_t keep = a->acc().all_sets() - tostrip;
|
||||
acc_cond::mark_t degenmark = {keep.count()};
|
||||
|
||||
update_acc_for_partial_degen(acc, todegen, tostrip, degenmark);
|
||||
if (!update_acc_for_partial_degen(acc, todegen, tostrip, degenmark,
|
||||
also_fin))
|
||||
report_invalid_partial_degen_arg(todegen, acc);
|
||||
res->set_acceptance(acc);
|
||||
|
||||
// auto* names = new std::vector<std::string>;
|
||||
|
|
|
|||
|
|
@ -99,7 +99,14 @@ namespace spot
|
|||
/// Fin(2).
|
||||
///
|
||||
/// Cases where the sets listed in \a todegen also occur outside
|
||||
/// of the Inf-conjunction are also supported.
|
||||
/// of the Inf-conjunction are also supported. Subformulas that
|
||||
/// are disjunctions of Fin(.) terms (e.g., Fin(1)|Fin(2)) can
|
||||
/// also be degeneralized if the input automaton is deterministic.
|
||||
///
|
||||
/// If this functions is called with a value of \a todegen that does
|
||||
/// not match a (complete) conjunction of Inf(.), or in a
|
||||
/// deterministic automaton a (complete) disjunction of Fin(.), an
|
||||
/// std::runtime_error exception is thrown.
|
||||
SPOT_API twa_graph_ptr
|
||||
partial_degeneralize(const const_twa_graph_ptr& a,
|
||||
acc_cond::mark_t todegen);
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@
|
|||
|
||||
import spot
|
||||
|
||||
a, b, d = spot.automata("""
|
||||
a, b, d, f = spot.automata("""
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
|
|
@ -59,6 +59,18 @@ Acceptance: 1 Fin(0)
|
|||
State: 0
|
||||
[0] 0 {0}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "p0"
|
||||
Acceptance: 2 Fin(0)|Fin(1)
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0 {0}
|
||||
[0] 1 {1}
|
||||
State: 1
|
||||
[!0] 0
|
||||
--END--
|
||||
""")
|
||||
|
||||
da = spot.partial_degeneralize(a, [0, 1])
|
||||
|
|
@ -97,6 +109,42 @@ assert dd.equivalent_to(d)
|
|||
assert dd.num_states() == 1
|
||||
assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'
|
||||
|
||||
e = spot.dualize(b)
|
||||
de = spot.partial_degeneralize(e, [0, 1])
|
||||
assert de.equivalent_to(e)
|
||||
assert de.num_states() == 4
|
||||
|
||||
de.copy_state_names_from(e)
|
||||
dehoa = de.to_str('hoa')
|
||||
assert dehoa == """HOA: v1
|
||||
States: 4
|
||||
Start: 0
|
||||
AP: 1 "p0"
|
||||
acc-name: parity max even 2
|
||||
Acceptance: 2 Fin(1) & Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0 "0#0"
|
||||
[0] 1
|
||||
[!0] 2
|
||||
State: 1 "1#0"
|
||||
[!0] 2
|
||||
[0] 3 {0 1}
|
||||
State: 2 "3#0"
|
||||
[t] 2 {0}
|
||||
State: 3 "2#0"
|
||||
[0] 1 {0 1}
|
||||
[!0] 2
|
||||
--END--"""
|
||||
|
||||
try:
|
||||
df = spot.partial_degeneralize(f, [0, 1])
|
||||
except RuntimeError as e:
|
||||
assert 'partial_degeneralize(): {0,1} does not' in str(e)
|
||||
else:
|
||||
raise RuntimeError("missing exception")
|
||||
|
||||
aut5 = spot.automaton(""" HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
|
||||
acc-name: generalized-Buchi 10 Acceptance: 10
|
||||
Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)&Inf(7)&Inf(8)&Inf(9)
|
||||
|
|
@ -158,3 +206,9 @@ pdaut8 = spot.partial_degeneralize(aut8, sets)
|
|||
assert pdaut8.equivalent_to(aut8)
|
||||
assert daut8.num_states() == 22
|
||||
assert pdaut8.num_states() == 9
|
||||
|
||||
aut9 = spot.dualize(aut8)
|
||||
pdaut9 = spot.partial_degeneralize(aut9, sets)
|
||||
assert pdaut9.equivalent_to(aut9)
|
||||
# one more state than aut9, because dualize completed the automaton.
|
||||
assert pdaut9.num_states() == 10
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue