Commit 4f2e9512 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

product_susp: new function

* spot/twaalgos/product.cc, spot/twaalgos/product.hh: Implement it.
* tests/python/_product_susp.ipynb: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
parent a4a8ae9a
......@@ -55,11 +55,6 @@ New in spot 2.5.3.dev (not yet released)
{SERE;1} = {1} if {SERE} accepts [*0]
{SERE;1} = {SERE} if {SERE} does not accept [*0]
- spot::product() and spot::product_or() learned to produce an
automaton with a simpler acceptance condition if one of the
argument is a weak automaton. In this case the resulting
acceptance condition is (usually) that of the other argument.
- gf_guarantee_to_ba() is a specialized construction for translating
formulas of the form GF(guarantee) to BA or DBA, and
fg_safety_to_dca() is a specialized construction for translating
......@@ -82,6 +77,16 @@ New in spot 2.5.3.dev (not yet released)
GF(((a & Xb) | XXc) & Xd) 6 4 16 5
GF((b | Fa) & (b R Xb)) 6 2 3 3
- spot::product() and spot::product_or() learned to produce an
automaton with a simpler acceptance condition if one of the
argument is a weak automaton. In this case the resulting
acceptance condition is (usually) that of the other argument.
- spot::product_susp() and spot::product_or_susp() are new
functions for building products between an automaton A and
a "suspendable" automaton B. They are also optimized for
the case that A is weak.
- print_dot(), used to print automata in GraphViz's format,
underwent several changes:
......
......@@ -21,6 +21,7 @@
#include <spot/twaalgos/product.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <deque>
#include <unordered_map>
#include <spot/misc/hash.hh>
......@@ -326,4 +327,223 @@ namespace spot
right->get_init_state_number());
}
namespace
{
template<typename T>
static void
product_susp_aux(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
twa_graph_ptr res, bool and_acc,
bool sync_all, acc_cond::mark_t rejmark, T merge_acc)
{
std::unordered_map<product_state, unsigned, product_state_hash> s2n;
std::deque<std::pair<product_state, unsigned>> todo;
scc_info si(left,
and_acc ? scc_info_options::TRACK_STATES_IF_FIN_USED
: (scc_info_options::TRACK_STATES_IF_FIN_USED
| scc_info_options::TRACK_SUCCS));
si.determine_unknown_acceptance();
auto new_state =
[&](unsigned left_state, unsigned right_state) -> unsigned
{
product_state x(left_state, right_state);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
p.first->second = res->new_state();
todo.emplace_back(x, p.first->second);
}
return p.first->second;
};
unsigned right_init = right->get_init_state_number();
unsigned left_init = left->get_init_state_number();
unsigned res_init;
auto target_scc = [&](unsigned scc) -> bool
{
return (!si.is_trivial(scc)
&& (sync_all ||si.is_accepting_scc(scc) == and_acc));
};
if (target_scc(si.scc_of(left_init)))
res_init = new_state(left_init, right_init);
else
res_init = new_state(left_init, -1U);
res->set_init_state(res_init);
bool sbacc = res->prop_state_acc().is_true();
while (!todo.empty())
{
auto top = todo.front();
todo.pop_front();
for (auto& l: left->out(top.first.first))
if (!target_scc(si.scc_of(l.dst)))
{
if (!sbacc || top.first.second == -1U)
{
res->new_edge(top.second, new_state(l.dst, -1U), l.cond,
merge_acc(l.acc, rejmark));
}
else
{
// This edge leaves a target SCC, but we build a
// state-based automaton, so make sure we still
// use the same acceptance marks as in the SCC.
auto rm = right->state_acc_sets(top.first.second);
res->new_edge(top.second, new_state(l.dst, -1U), l.cond,
merge_acc(l.acc, rm));
}
}
else
{
unsigned right_state = top.first.second;
if (top.first.second == -1U)
right_state = right_init;
for (auto& r: right->out(right_state))
{
auto cond = l.cond & r.cond;
if (cond == bddfalse)
continue;
auto dst = new_state(l.dst, r.dst);
res->new_edge(top.second, dst, cond,
merge_acc(l.acc, r.acc));
}
}
}
}
static twa_graph_ptr
product_susp_main(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
bool and_acc = true)
{
if (SPOT_UNLIKELY(!(left->is_existential() && right->is_existential())))
throw std::runtime_error
("product_susp() does not support alternating automata");
if (SPOT_UNLIKELY(left->get_dict() != right->get_dict()))
throw std::runtime_error("product_susp(): left and right automata "
"should share their bdd_dict");
auto false_or_left = [&] (bool ff)
{
if (ff)
{
auto res = make_twa_graph(left->get_dict());
res->new_state();
return res;
}
return make_twa_graph(left, twa::prop_set::all());
};
// We assume RIGHT is suspendable, but we want to deal with some
// trivial true/false cases so we can later assume right has
// more than one acceptance set.
// Note: suspendable with "t" acceptance = universal language.
if (SPOT_UNLIKELY(right->num_sets() == 0))
{
if (and_acc)
return false_or_left(right->is_empty());
else if (right->is_empty()) // left OR false = left
return make_twa_graph(left, twa::prop_set::all());
else // left OR true = true
return make_twa_graph(right, twa::prop_set::all());
}
auto res = make_twa_graph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
bool leftweak = left->prop_weak().is_true();
res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
auto rightunsatmark = right->acc().unsat_mark();
if (SPOT_UNLIKELY(!rightunsatmark.first))
return false_or_left(and_acc);
acc_cond::mark_t rejmark = rightunsatmark.second;
if (leftweak)
{
res->copy_acceptance_of(right);
if (and_acc)
{
product_susp_aux(left, right, res, true, false, rejmark,
[&] (acc_cond::mark_t,
acc_cond::mark_t mr)
{
return mr;
});
}
else
{
auto rightsatmark = right->acc().sat_mark();
if (!rightsatmark.first)
// Right is always rejecting, no point in making a product_or
return make_twa_graph(left, twa::prop_set::all());
acc_cond::mark_t accmark = rightsatmark.second;
auto& lacc = left->acc();
product_susp_aux(left, right, res, false, false, rejmark,
[&] (acc_cond::mark_t ml,
acc_cond::mark_t mr)
{
if (!lacc.accepting(ml))
return mr;
else
return accmark;
});
}
}
else // general case
{
auto left_num = left->num_sets();
auto right_acc = right->get_acceptance() << left_num;
if (and_acc)
right_acc &= left->get_acceptance();
else
right_acc |= left->get_acceptance();
res->set_acceptance(left_num + right->num_sets(), right_acc);
product_susp_aux(left, right, res, and_acc, !and_acc, rejmark,
[&] (acc_cond::mark_t ml,
acc_cond::mark_t mr)
{
return ml | (mr << left_num);
});
}
// The product of two non-deterministic automata could be
// deterministic. Likewise for non-complete automata.
if (left->prop_universal() && right->prop_universal())
res->prop_universal(true);
if (left->prop_complete() && right->prop_complete())
res->prop_complete(true);
if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
res->prop_stutter_invariant(true);
if (left->prop_inherently_weak() && right->prop_inherently_weak())
res->prop_inherently_weak(true);
if (left->prop_weak() && right->prop_weak())
res->prop_weak(true);
if (left->prop_terminal() && right->prop_terminal())
res->prop_terminal(true);
return res;
}
}
twa_graph_ptr product_susp(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return product_susp_main(left, right);
}
twa_graph_ptr product_or_susp(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
return product_susp_main(complete(left), right, false);
}
}
......@@ -118,4 +118,44 @@ namespace spot
unsigned left_state,
unsigned right_state);
/// \ingroup twa_algorithms
/// \brief Build the product of an automaton with a suspendable
/// automaton.
///
/// The language of this product is the intersection of the
/// languages of both input automata.
///
/// This function *assumes* that \a right_susp is a suspendable
/// automaton, i.e., it its language L satisfies L = Σ*.L.
/// Therefore the product between the two automata need only be done
/// with the accepting SCCs of left.
///
/// If \a left is a weak automaton, the acceptance condition of the
/// output will be that of \a right_susp. Otherwise the acceptance
/// condition is the conjunction of both acceptances.
SPOT_API
twa_graph_ptr product_susp(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right_susp);
/// \ingroup twa_algorithms
/// \brief Build the "or" product of an automaton with a suspendable
/// automaton.
///
/// The language of this product is the union of the languages of
/// both input automata.
///
/// This function *assumes* that \a right_susp is a suspendable
/// automaton, i.e., it its language L satisfies L = Σ*.L.
/// Therefore, after left has been completed (this will be done by
/// product_or_susp) the product between the two automata need only
/// be done with the SCCs of left that contains some rejecting cycles.
///
/// The current implementation is currently suboptimal as instead of
/// looking for SCC with rejecting cycles, it simply loop for
/// non-trivial SCC, (or in the case of weak automata, with
/// non-trivial and rejecting SCCs).
SPOT_API
twa_graph_ptr product_or_susp(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right_susp);
}
......@@ -385,6 +385,7 @@ TESTS_python = \
python/parity.py \
python/prodexpt.py \
python/_product_weak.ipynb \
python/_product_susp.ipynb \
python/randgen.py \
python/relabel.py \
python/remfin.py \
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment