transform: copy and accessible versions
* src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh: Rename transform_mask to accessible_mask. Add Copy version and use it in mask_keep_states(). * src/tgbatest/maskkeep.test: Update.
This commit is contained in:
parent
223d41d26b
commit
c61f053e2d
3 changed files with 101 additions and 31 deletions
|
|
@ -32,15 +32,16 @@ namespace spot
|
||||||
unsigned tr = to_remove.count();
|
unsigned tr = to_remove.count();
|
||||||
assert(tr <= na);
|
assert(tr <= na);
|
||||||
res->set_acceptance_conditions(na - tr);
|
res->set_acceptance_conditions(na - tr);
|
||||||
transform_mask(in, res, [&](bdd& cond,
|
transform_accessible(in, res, [&](unsigned,
|
||||||
acc_cond::mark_t& acc,
|
bdd& cond,
|
||||||
unsigned)
|
acc_cond::mark_t& acc,
|
||||||
{
|
unsigned)
|
||||||
if (acc & to_remove)
|
{
|
||||||
cond = bddfalse;
|
if (acc & to_remove)
|
||||||
else
|
cond = bddfalse;
|
||||||
acc = inacc.strip(acc, to_remove);
|
else
|
||||||
});
|
acc = inacc.strip(acc, to_remove);
|
||||||
|
});
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -55,11 +56,12 @@ namespace spot
|
||||||
res->copy_ap_of(in);
|
res->copy_ap_of(in);
|
||||||
res->prop_copy(in, { true, true, true, true });
|
res->prop_copy(in, { true, true, true, true });
|
||||||
res->copy_acceptance_conditions_of(in);
|
res->copy_acceptance_conditions_of(in);
|
||||||
transform_mask(in, res, [&](bdd& cond,
|
transform_copy(in, res, [&](unsigned src,
|
||||||
acc_cond::mark_t&,
|
bdd& cond,
|
||||||
unsigned dst)
|
acc_cond::mark_t&,
|
||||||
|
unsigned dst)
|
||||||
{
|
{
|
||||||
if (!to_keep[dst])
|
if (!to_keep[src] || !to_keep[dst])
|
||||||
cond = bddfalse;
|
cond = bddfalse;
|
||||||
}, init);
|
}, init);
|
||||||
return res;
|
return res;
|
||||||
|
|
|
||||||
|
|
@ -28,9 +28,10 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// Copy the transition of the automaton \a old, into the automaton
|
/// Copy the transition of the automaton \a old, into the automaton
|
||||||
/// \a cpy, creating new states at the same time. The argument \a
|
/// \a cpy, creating new states at the same time. The argument \a
|
||||||
/// trans should behave as a fonction with the following prototype:
|
/// trans should behave as a function with the following prototype:
|
||||||
/// <code>
|
/// <code>
|
||||||
/// void (*trans) (bdd& cond, acc_cond::mark_t& acc, unsigned dst)
|
/// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc,
|
||||||
|
/// unsigned dst)
|
||||||
/// </code>
|
/// </code>
|
||||||
/// It can modify either the condition or the acceptance sets of
|
/// It can modify either the condition or the acceptance sets of
|
||||||
/// the transitions. Set the condition to bddfalse to remove it
|
/// the transitions. Set the condition to bddfalse to remove it
|
||||||
|
|
@ -39,9 +40,9 @@ namespace spot
|
||||||
/// \param init The optional new initial state.
|
/// \param init The optional new initial state.
|
||||||
|
|
||||||
template<typename Trans>
|
template<typename Trans>
|
||||||
void transform_mask(const const_tgba_digraph_ptr& old,
|
void transform_accessible(const const_tgba_digraph_ptr& old,
|
||||||
tgba_digraph_ptr& cpy,
|
tgba_digraph_ptr& cpy,
|
||||||
Trans trans, unsigned int init)
|
Trans trans, unsigned int init)
|
||||||
{
|
{
|
||||||
std::vector<unsigned> todo;
|
std::vector<unsigned> todo;
|
||||||
std::vector<unsigned> seen(old->num_states(), -1U);
|
std::vector<unsigned> seen(old->num_states(), -1U);
|
||||||
|
|
@ -72,7 +73,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
bdd cond = t.cond;
|
bdd cond = t.cond;
|
||||||
acc_cond::mark_t acc = t.acc;
|
acc_cond::mark_t acc = t.acc;
|
||||||
trans(cond, acc, t.dst);
|
trans(t.src, cond, acc, t.dst);
|
||||||
|
|
||||||
if (cond != bddfalse)
|
if (cond != bddfalse)
|
||||||
cpy->new_transition(new_src,
|
cpy->new_transition(new_src,
|
||||||
|
|
@ -82,12 +83,55 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// \brief Copy an automaton and update each transitions.
|
||||||
|
///
|
||||||
|
/// Copy the states of the automaton \a old, into the automaton
|
||||||
|
/// \a cpy. Each state in \a cpy will have the same id as the ones in \a old.
|
||||||
|
/// The argument \a trans
|
||||||
|
/// should behave as a function with the following prototype:
|
||||||
|
/// <code>
|
||||||
|
/// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc,
|
||||||
|
/// unsigned dst)
|
||||||
|
/// </code>
|
||||||
|
/// It can modify either the condition or the acceptance sets of
|
||||||
|
/// the transitions. Set the condition to bddfalse to remove it. Note that
|
||||||
|
/// all transtions will be processed.
|
||||||
|
/// \param init The optional new initial state.
|
||||||
template<typename Trans>
|
template<typename Trans>
|
||||||
void transform_mask(const const_tgba_digraph_ptr& old,
|
void transform_copy(const const_tgba_digraph_ptr& old,
|
||||||
tgba_digraph_ptr& cpy,
|
tgba_digraph_ptr& cpy,
|
||||||
Trans trans)
|
Trans trans, unsigned int init)
|
||||||
{
|
{
|
||||||
transform_mask(old, cpy, trans, old->get_init_state_number());
|
// Each state in cpy corresponds to a unique state in old.
|
||||||
|
cpy->new_states(old->num_states());
|
||||||
|
cpy->set_init_state(init);
|
||||||
|
|
||||||
|
for (auto& t: old->transitions())
|
||||||
|
{
|
||||||
|
bdd cond = t.cond;
|
||||||
|
acc_cond::mark_t acc = t.acc;
|
||||||
|
trans(t.src, cond, acc, t.dst);
|
||||||
|
// Having the same number of states should assure that state ids are
|
||||||
|
// equivilent in old and cpy.
|
||||||
|
assert(t.src < cpy->num_states() && t.dst < cpy->num_states());
|
||||||
|
if (cond != bddfalse)
|
||||||
|
cpy->new_transition(t.src, t.dst, cond, acc);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
template<typename Trans>
|
||||||
|
void transform_accessible(const const_tgba_digraph_ptr& old,
|
||||||
|
tgba_digraph_ptr& cpy,
|
||||||
|
Trans trans)
|
||||||
|
{
|
||||||
|
transform_accessible(old, cpy, trans, old->get_init_state_number());
|
||||||
|
}
|
||||||
|
template<typename Trans>
|
||||||
|
void transform_copy(const const_tgba_digraph_ptr& old,
|
||||||
|
tgba_digraph_ptr& cpy,
|
||||||
|
Trans trans)
|
||||||
|
{
|
||||||
|
transform_copy(old, cpy, trans, old->get_init_state_number());
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Remove all transitions that are in some given acceptance sets.
|
/// \brief Remove all transitions that are in some given acceptance sets.
|
||||||
|
|
|
||||||
|
|
@ -48,7 +48,7 @@ EOF
|
||||||
|
|
||||||
cat >expect1 <<EOF
|
cat >expect1 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 1
|
States: 4
|
||||||
Start: 0
|
Start: 0
|
||||||
AP: 0
|
AP: 0
|
||||||
acc-name: generalized-Buchi 2
|
acc-name: generalized-Buchi 2
|
||||||
|
|
@ -56,6 +56,25 @@ Acceptance: 2 Inf(0)&Inf(1)
|
||||||
properties: trans-labels explicit-labels state-acc deterministic
|
properties: trans-labels explicit-labels state-acc deterministic
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
|
State: 1
|
||||||
|
State: 2
|
||||||
|
State: 3
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
|
||||||
|
cat >expect2 <<EOF
|
||||||
|
HOA: v1
|
||||||
|
States: 4
|
||||||
|
Start: 1
|
||||||
|
AP: 0
|
||||||
|
acc-name: generalized-Buchi 2
|
||||||
|
Acceptance: 2 Inf(0)&Inf(1)
|
||||||
|
properties: trans-labels explicit-labels state-acc deterministic
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
State: 1
|
||||||
|
State: 2
|
||||||
|
State: 3
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
|
@ -63,11 +82,11 @@ run 0 ../../bin/autfilt --keep-states=0 input1 -H >output
|
||||||
diff output expect1
|
diff output expect1
|
||||||
|
|
||||||
run 0 ../../bin/autfilt --keep-states=1 input1 -H >output
|
run 0 ../../bin/autfilt --keep-states=1 input1 -H >output
|
||||||
diff output expect1
|
diff output expect2
|
||||||
|
|
||||||
cat >expect3 <<EOF
|
cat >expect3 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 3
|
States: 4
|
||||||
Start: 0
|
Start: 0
|
||||||
AP: 2 "a" "b"
|
AP: 2 "a" "b"
|
||||||
acc-name: generalized-Buchi 2
|
acc-name: generalized-Buchi 2
|
||||||
|
|
@ -81,22 +100,27 @@ State: 1
|
||||||
[0] 2
|
[0] 2
|
||||||
State: 2
|
State: 2
|
||||||
[1] 1
|
[1] 1
|
||||||
|
State: 3
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
cat >expect4 <<EOF
|
cat >expect4 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 2
|
States: 4
|
||||||
Start: 0
|
Start: 1
|
||||||
AP: 2 "a" "b"
|
AP: 2 "a" "b"
|
||||||
acc-name: generalized-Buchi 2
|
acc-name: generalized-Buchi 2
|
||||||
Acceptance: 2 Inf(0)&Inf(1)
|
Acceptance: 2 Inf(0)&Inf(1)
|
||||||
properties: trans-labels explicit-labels state-acc deterministic
|
properties: trans-labels explicit-labels trans-acc
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
[0] 1
|
[0] 1 {0}
|
||||||
|
[1] 2 {1}
|
||||||
State: 1
|
State: 1
|
||||||
[1] 0
|
[0] 2
|
||||||
|
State: 2
|
||||||
|
[1] 1
|
||||||
|
State: 3
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue