Skip to content

GitLab

Spot
Spot
Commit 3ab2dd17 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files
Options

product: add product_xor() and product_xnor() 

* spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
functions.
* tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
* NEWS: Mention them.
parent a78137f9
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 8962 additions and 187 deletions
NEWS
View file @ 3ab2dd17
New in spot 2.9.0.dev (not yet released)
Nothing yet.
Library:
- product_xor() and product_xnor() are two new versions of the
synchronized product. The only work with operands that are
deterministic automata, and build automata whose language are
respectively the symmetric difference of the operands, and the
complement of that.
New in spot 2.9 (2020-04-30)
......@@ -19,7 +26,7 @@ New in spot 2.9 (2020-04-30)
spot-rejected-word: "!a; !a; cycle{a}"
- autfilt learned the --partial-degeneralize option, to remove
conjunctions of Inf, or disjunction of Fin that appears in
conjunctions of Inf, or disjunctions of Fin that appears in
arbitrary conditions.
- ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to
......
spot/twaalgos/product.cc
View file @ 3ab2dd17
......@@ -22,6 +22,7 @@
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isdet.hh>
#include <deque>
#include <unordered_map>
#include <spot/misc/hash.hh>
......@@ -41,7 +42,6 @@ namespace spot
}
};
template<typename T>
static
void product_main(const const_twa_graph_ptr& left,
......@@ -100,12 +100,15 @@ namespace spot
}
}
enum acc_op { and_acc, or_acc, xor_acc, xnor_acc };
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,
acc_op aop,
const output_aborter* aborter)
{
if (SPOT_UNLIKELY(!(left->is_existential() && right->is_existential())))
......@@ -122,164 +125,271 @@ namespace spot
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))
// of the arguments is weak.
if (leftweak || rightweak)
{
// 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.
// t, f, Büchi or co-Büchi. We use co-Büchi only when
// t and f cannot be used, and both acceptance conditions
// are in {t,f,co-Büchi}.
if (leftweak && rightweak)
{
weak_weak:
res->prop_weak(true);
acc_cond::mark_t accmark = {0};
acc_cond::mark_t rejmark = {};
if (left->acc().is_co_buchi() && right->acc().is_co_buchi())
auto& lacc = left->acc();
auto& racc = right->acc();
if ((lacc.is_co_buchi() && (racc.is_co_buchi()
|| racc.num_sets() == 0))
|| (lacc.num_sets() == 0 && racc.is_co_buchi()))
{
res->set_co_buchi();
std::swap(accmark, rejmark);
}
else if ((aop == and_acc && lacc.is_t() && racc.is_t())
|| (aop == or_acc && (lacc.is_t() || racc.is_t()))
|| (aop == xnor_acc && ((lacc.is_t() && racc.is_t()) ||
(lacc.is_f() && racc.is_f())))
|| (aop == xor_acc && ((lacc.is_t() && racc.is_f()) ||
(lacc.is_f() && racc.is_t()))))
{
res->set_acceptance(0, acc_cond::acc_code::t());
accmark = {};
}
else if ((aop == and_acc && (lacc.is_f() || racc.is_f()))
|| (aop == or_acc && lacc.is_f() && racc.is_f())
|| (aop == xor_acc && ((lacc.is_t() && racc.is_t()) ||
(lacc.is_f() && racc.is_f())))
|| (aop == xnor_acc && ((lacc.is_t() && racc.is_f()) ||
(lacc.is_f() && racc.is_t()))))
{
res->set_acceptance(0, acc_cond::acc_code::f());
accmark = {};
}
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;
}, aborter);
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;
}, aborter);
}
else if (!rightweak)
{
if (and_acc)
switch (aop)
{
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();
case 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))
return mr;
if (lacc.accepting(ml) && racc.accepting(mr))
return accmark;
else
return rejmark;
}, aborter);
}
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();
break;
case or_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
if (lacc.accepting(ml) || racc.accepting(mr))
return accmark;
else
return rejmark;
}, aborter);
}
}
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();
break;
case xor_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;
if (lacc.accepting(ml) ^ racc.accepting(mr))
return accmark;
else
return rejmark;
}, aborter);
}
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();
break;
case xnor_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
if (lacc.accepting(ml) == racc.accepting(mr))
return accmark;
else
return rejmark;
}, aborter);
break;
}
}
else if (!rightweak)
{
switch (aop)
{
case 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;
}, aborter);
break;
}
case or_acc:
{
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;
}, aborter);
break;
}
case xor_acc:
case xnor_acc:
{
auto rightsatmark = right->acc().sat_mark();
auto rightunsatmark = right->acc().unsat_mark();
if (!rightunsatmark.first || !rightsatmark.first)
{
// Left is weak. Right was not weak, but it
// is either always rejecting or always
// accepting. We can therefore pretend that
// right is weak.
goto weak_weak;
}
goto generalcase;
break;
}
}
}
else // right weak
{
assert(!leftweak);
switch (aop)
{
case 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;
}, aborter);
break;
}
case or_acc:
{
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;
}, aborter);
break;
}
case xor_acc:
case xnor_acc:
{
auto leftsatmark = left->acc().sat_mark();
auto leftunsatmark = left->acc().unsat_mark();
if (!leftunsatmark.first || !leftsatmark.first)
{
// Right is weak. Left was not weak, but it
// is either always rejecting or always
// accepting. We can therefore pretend that
// left is weak.
goto weak_weak;
}
goto generalcase;
break;
}
}
}
}
else // general case
{
generalcase:
auto left_num = left->num_sets();
auto& left_acc = left->get_acceptance();
auto right_acc = right->get_acceptance() << left_num;
if (and_acc)
right_acc &= left->get_acceptance();
else
right_acc |= left->get_acceptance();
switch (aop)
{
case and_acc:
right_acc &= left_acc;
break;
case or_acc:
right_acc |= left_acc;
break;
case xor_acc:
{
auto tmp = right_acc.complement() & left_acc;
right_acc &= left_acc.complement();
right_acc |= tmp;
break;
}
case xnor_acc:
{
auto tmp = right_acc.complement() & left_acc.complement();
right_acc &= left_acc;
tmp |= right_acc;
std::swap(tmp, right_acc);
break;
}
}
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);
}, aborter);
}
if (!res) // aborted
......@@ -323,7 +433,7 @@ namespace spot
unsigned right_state,
const output_aborter* aborter)
{
return product_aux(left, right, left_state, right_state, true, aborter);
return product_aux(left, right, left_state, right_state, and_acc, aborter);
}
twa_graph_ptr product(const const_twa_graph_ptr& left,
......@@ -341,7 +451,7 @@ namespace spot
unsigned right_state)
{
return product_aux(complete(left), complete(right),
left_state, right_state, false, nullptr);
left_state, right_state, or_acc, nullptr);
}
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
......@@ -352,6 +462,32 @@ namespace spot
right->get_init_state_number());
}
twa_graph_ptr product_xor(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
if (SPOT_UNLIKELY(!is_deterministic(left) || !is_deterministic(right)))
throw std::runtime_error
("product_xor() only works with deterministic automata");
return product_aux(complete(left), complete(right),
left->get_init_state_number(),
right->get_init_state_number(),
xor_acc, nullptr);
}
twa_graph_ptr product_xnor(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right)
{
if (SPOT_UNLIKELY(!is_deterministic(left) || !is_deterministic(right)))
throw std::runtime_error
("product_xnor() only works with deterministic automata");
return product_aux(complete(left), complete(right),
left->get_init_state_number(),
right->get_init_state_number(),
xnor_acc, nullptr);
}
namespace
{
......
spot/twaalgos/product.hh
View file @ 3ab2dd17
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2018, 2019 Laboratoire de Recherche et
// Copyright (C) 2014-2015, 2018-2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -127,6 +127,45 @@ namespace spot
unsigned left_state,
unsigned right_state);
/// \ingroup twa_algorithms
/// \brief XOR two deterministic automata using a synchronous product
///
/// The two operands must be deterministic.
///
/// The resulting automaton will accept the symmetric difference of
/// both languages and have an acceptance condition that is the xor
/// of the acceptance conditions of the two input automata. In case
/// both operands are weak, the acceptance condition of the result
/// is made simpler.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product_xor(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief XNOR two automata using a synchronous product
///
/// The two operands must be deterministic.
///
/// The resulting automaton will accept words that are either in
/// both input languages, or not in both languages. (The XNOR gate
/// it the logical complement of XOR. XNOR is also known as logical
/// equivalence.) The output will have an acceptance condition that
/// is the XNOR of the acceptance conditions of the two input
/// automata. In case both the operands are weak, the acceptance
/// condition of the result is made simpler.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product_xnor(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief Build the product of an automaton with a suspendable
......@@ -136,7 +175,7 @@ namespace spot
/// 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.
/// automaton, i.e., its language L satisfies L = Σ*.L.
/// Therefore the product between the two automata need only be done
/// with the accepting SCCs of left.
///
......@@ -155,7 +194,7 @@ namespace spot
/// both input automata.
///
/// This function *assumes* that \a right_susp is a suspendable
/// automaton, i.e., it its language L satisfies L = Σ*.L.
/// automaton, i.e., 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.
......
tests/python/_product_weak.ipynb
View file @ 3ab2dd17
This diff is collapsed.
tests/python/except.py
View file @ 3ab2dd17
......@@ -188,3 +188,32 @@ except ValueError as e:
assert 'any' in s
else:
report_missing_exception()
a1 = spot.translate('FGa')
a2 = spot.translate('Gb')
assert not spot.is_deterministic(a1)
assert spot.is_deterministic(a2)
try:
spot.product_xor(a1, a2)
except RuntimeError as e:
assert "product_xor() only works with deterministic automata"
else:
report_missing_exception()
try:
spot.product_xor(a2, a1)
except RuntimeError as e:
assert "product_xor() only works with deterministic automata"
else:
report_missing_exception()
try:
spot.product_xnor(a1, a2)
except RuntimeError as e:
assert "product_xnor() only works with deterministic automata"
else:
report_missing_exception()
try:
spot.product_xnor(a2, a1)
except RuntimeError as e:
assert "product_xnor() only works with deterministic automata"
else:
report_missing_exception()
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