Commit a738801e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

product: optimize product with weak automata

Fixes #350.

* spot/twaalgos/product.cc: Implement this change.
* NEWS, spot/twaalgos/product.hh: Mention it.
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method.
* tests/python/_product_weak.ipynb: New file.
* tests/Makefile.am: Add it.
* tests/python/automata.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases.
parent b6550388
Pipeline #1848 passed with stages
in 139 minutes and 30 seconds
......@@ -89,6 +89,11 @@ New in spot 2.5.3.dev (not yet released)
They are most welcome in Python, since we used to redefine
them every now and them.
- spot::product() and spot::product_or() learned so 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::parity_product() and spot::parity_product_or() were dropped.
The code was buggy, hard to maintain, and these functions do not
seem to be used.
......
......@@ -1153,12 +1153,22 @@ namespace spot
}
std::pair<bool, acc_cond::mark_t>
acc_cond::unsat_mark() const
acc_cond::sat_unsat_mark(bool sat) const
{
if (is_t())
return {false, mark_t({})};
if (!uses_fin_acceptance())
return {true, mark_t({})};
if (sat)
{
if (is_f())
return {false, mark_t({})};
if (!uses_fin_acceptance())
return {true, all_sets()};
}
else
{
if (is_t())
return {false, mark_t({})};
if (!uses_fin_acceptance())
return {true, mark_t({})};
}
auto used = code_.used_sets();
unsigned c = used.count();
......@@ -1185,11 +1195,11 @@ namespace spot
bdd res = to_bdd_rec(&code_.back(), &r[0]);
if (res == bddtrue)
return {false, mark_t({})};
return {sat, mark_t({})};
if (res == bddfalse)
return {true, mark_t({})};
return {!sat, mark_t({})};
bdd cube = bdd_satone(!res);
bdd cube = bdd_satone(sat ? res : !res);
mark_t i = {};
while (cube != bddtrue)
{
......
......@@ -1165,10 +1165,21 @@ namespace spot
// Return (true, m) if there exist some acceptance mark m that
// does not satisfy the acceptance condition. Return (false, 0U)
// otherwise.
std::pair<bool, acc_cond::mark_t> unsat_mark() const;
std::pair<bool, acc_cond::mark_t> unsat_mark() const
{
return sat_unsat_mark(false);
}
// Return (true, m) if there exist some acceptance mark m that
// does satisfy the acceptance condition. Return (false, 0U)
// otherwise.
std::pair<bool, acc_cond::mark_t> sat_mark() const
{
return sat_unsat_mark(true);
}
protected:
bool check_fin_acceptance() const;
std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
public:
static acc_code inf(mark_t mark)
......
......@@ -40,33 +40,18 @@ namespace spot
}
};
template<typename T>
static
twa_graph_ptr product_aux(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state,
bool and_acc)
void product_main(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state,
twa_graph_ptr res, T merge_acc)
{
if (!(left->is_existential() && right->is_existential()))
throw std::runtime_error
("product() does not support alternating automata");
std::unordered_map<product_state, unsigned, product_state_hash> s2n;
std::deque<std::pair<product_state, unsigned>> todo;
if (left->get_dict() != right->get_dict())
throw std::runtime_error("product: left and right automata should "
"share their bdd_dict");
auto res = make_twa_graph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
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);
auto v = new product_states;
res->set_named_prop("product-states", v);
......@@ -86,10 +71,10 @@ namespace spot
};
res->set_init_state(new_state(left_state, right_state));
if (right_acc.is_f())
if (res->acc().is_f())
// Do not bother doing any work if the resulting acceptance is
// false.
return res;
return;
while (!todo.empty())
{
auto top = todo.front();
......@@ -102,10 +87,192 @@ namespace spot
continue;
auto dst = new_state(l.dst, r.dst);
res->new_edge(top.second, dst, cond,
l.acc | (r.acc << left_num));
merge_acc(l.acc, r.acc));
// If right is deterministic, we can abort immediately!
}
}
}
static
twa_graph_ptr product_aux(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state,
bool and_acc)
{
if (SPOT_UNLIKELY(!(left->is_existential() && right->is_existential())))
throw std::runtime_error
("product() does not support alternating automata");
if (SPOT_UNLIKELY(left->get_dict() != right->get_dict()))
throw std::runtime_error("product: left and right automata should "
"share their bdd_dict");
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();
bool rightweak = right->prop_weak().is_true();
// We have optimization to the standard product in case one
// of the arguments is weak. However these optimizations
// are pointless if the said arguments are "t" or "f".
if ((leftweak || rightweak)
&& (left->num_sets() > 0) && (right->num_sets() > 0))
{
// If both automata are weak, we can restrict the result to
// Büchi or co-Büchi. We will favor Büchi unless the two
// operands are co-Büchi.
if (leftweak && rightweak)
{
weak_weak:
acc_cond::mark_t accmark = {0};
acc_cond::mark_t rejmark = {};
if (left->acc().is_co_buchi() && right->acc().is_co_buchi())
{
res->set_co_buchi();
std::swap(accmark, rejmark);
}
else
{
res->set_buchi();
}
res->prop_weak(true);
auto& lacc = left->acc();
auto& racc = right->acc();
if (and_acc)
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (lacc.accepting(ml) && racc.accepting(mr))
return accmark;
else
return rejmark;
});
else
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (lacc.accepting(ml) || racc.accepting(mr))
return accmark;
else
return rejmark;
});
}
else if (!rightweak)
{
if (and_acc)
{
auto rightunsatmark = right->acc().unsat_mark();
if (!rightunsatmark.first)
{
// Left is weak. Right was not weak, but it is
// always accepting. We can therefore pretend
// that right is weak.
goto weak_weak;
}
res->copy_acceptance_of(right);
acc_cond::mark_t rejmark = rightunsatmark.second;
auto& lacc = left->acc();
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (lacc.accepting(ml))
return mr;
else
return rejmark;
});
}
else
{
auto rightsatmark = right->acc().sat_mark();
if (!rightsatmark.first)
{
// Left is weak. Right was not weak, but it is
// always rejecting. We can therefore pretend
// that right is weak.
goto weak_weak;
}
res->copy_acceptance_of(right);
acc_cond::mark_t accmark = rightsatmark.second;
auto& lacc = left->acc();
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (!lacc.accepting(ml))
return mr;
else
return accmark;
});
}
}
else
{
assert(!leftweak);
if (and_acc)
{
auto leftunsatmark = left->acc().unsat_mark();
if (!leftunsatmark.first)
{
// Right is weak. Left was not weak, but it is
// always accepting. We can therefore pretend
// that left is weak.
goto weak_weak;
}
res->copy_acceptance_of(left);
acc_cond::mark_t rejmark = leftunsatmark.second;
auto& racc = right->acc();
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (racc.accepting(mr))
return ml;
else
return rejmark;
});
}
else
{
auto leftsatmark = left->acc().sat_mark();
if (!leftsatmark.first)
{
// Right is weak. Left was not weak, but it is
// always rejecting. We can therefore pretend
// that left is weak.
goto weak_weak;
}
res->copy_acceptance_of(left);
acc_cond::mark_t accmark = leftsatmark.second;
auto& racc = right->acc();
product_main(left, right, left_state, right_state, res,
[&] (acc_cond::mark_t ml, acc_cond::mark_t mr)
{
if (!racc.accepting(mr))
return ml;
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_main(left, right, left_state, right_state, res,
[&] (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.
......@@ -147,8 +314,7 @@ namespace spot
unsigned left_state,
unsigned right_state)
{
return product_aux(complete(left),
complete(right),
return product_aux(complete(left), complete(right),
left_state, right_state, false);
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2014, 2015, 2018 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -36,7 +36,10 @@ namespace spot
/// The resulting automaton will accept the intersection of both
/// languages and have an acceptance condition that is the
/// conjunction of the acceptance conditions of the two input
/// automata.
/// automata. In case one of the left or right automaton is weak,
/// the acceptance condition of the result is made simpler: it
/// usually is the acceptance condition of the other argument,
/// therefore avoiding the need to introduce new accepting sets.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
......@@ -56,7 +59,10 @@ namespace spot
/// languages recognized by each input automaton (with its initial
/// state changed) and have an acceptance condition that is the
/// conjunction of the acceptance conditions of the two input
/// automata.
/// automata. In case one of the left or right automaton is weak,
/// the acceptance condition of the result is made simpler: it
/// usually is the acceptance condition of the other argument,
/// therefore avoiding the need to introduce new accepting sets.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
......@@ -74,7 +80,10 @@ namespace spot
/// The resulting automaton will accept the union of both
/// languages and have an acceptance condition that is the
/// disjunction of the acceptance conditions of the two input
/// automata.
/// automata. In case one of the left or right automaton is weak,
/// the acceptance condition of the result is made simpler: it
/// usually is the acceptance condition of the other argument,
/// therefore avoiding the need to introduce new accepting sets.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
......@@ -94,7 +103,10 @@ namespace spot
/// recognized by each input automaton (with its initial state
/// changed) and have an acceptance condition that is the
/// disjunction of the acceptance conditions of the two input
/// automata.
/// automata. In case one of the left or right automaton is weak,
/// the acceptance condition of the result is made simpler: it
/// usually is the acceptance condition of the other argument,
/// therefore avoiding the need to introduce new accepting sets.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
......
......@@ -383,6 +383,7 @@ TESTS_python = \
python/parsetgba.py \
python/parity.py \
python/prodexpt.py \
python/_product_weak.ipynb \
python/randgen.py \
python/relabel.py \
python/remfin.py \
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -106,6 +106,7 @@ diff pand.hoa exp
test 2 = `autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa`
# Xb is weak, so the product will still be Büchi
ltl2tgba -BDH 'GFa' > gfa.hoa
ltl2tgba -BDH 'Xb' > xb.hoa
autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
......@@ -116,14 +117,15 @@ HOA: v1
States: 7
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {1}
State: 0 {0}
[0] 1
[!0] 2
State: 1 {1}
State: 1 {0}
[0&1] 3
[!0&1] 4
[0&!1] 5
......@@ -133,13 +135,13 @@ State: 2
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 3 {0 1}
State: 3 {0}
[0] 3
[!0] 4
State: 4 {0}
[0] 3
[!0] 4
State: 5 {1}
State: 5 {0}
[0] 5
[!0] 6
State: 6
......@@ -159,14 +161,15 @@ HOA: v1
States: 7
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0 1}
State: 0 {0}
[0] 1
[!0] 2
State: 1 {0 1}
State: 1 {0}
[0&1] 3
[!0&1] 4
[0&!1] 5
......@@ -176,13 +179,13 @@ State: 2 {0}
[!0&1] 4
[0&!1] 5
[!0&!1] 6
State: 3 {0 1}
State: 3 {0}
[0] 3
[!0] 4
State: 4 {0}
[0] 3
[!0] 4
State: 5 {1}
State: 5 {0}
[0] 5
[!0] 6
State: 6
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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