Commit b428ed31 authored by Thomas Medioni's avatar Thomas Medioni

Implements is_streett_like() and streett_like_pairs(), is_rabin_like...

Adds the method spot::acc_cond::is_streett_like() that behaves like
spot::acc_cond::is_streett() except that it works on a wider range
of acceptance conditions, called Streett-like. Also adds
spot::acc_cond::streett_like_pairs() that returns a boolean assessing
whether the acceptance condition is Streett-like and also returns all
the Streett_like pairs.
Defines the new struct type spot::acc_cond::rs_pair.
Similarily, Adds the methods spot::acc_cond::is_rabin_like() and
spot::acc_cond::rabin_like_pairs().

* NEWS: Mention this modification
* python/spot/impl.i: Declares the new struct to SWIG, and defines
the streett_like_pairs() vector as an output parameter, which makes
the python code return a tuple (boolean, vector) rather than a
pass-by-reference vector.
* spot/twa/acc.cc, spot/twa/acc.hh: Declares an implements the new
methods and the new nested struct.
* tests/Makefile.am: Add new tests to the suite
* tests/python/rs_like.py: Tests the new methods and
the SWIG bindings.
parent 07c2dd3b
...@@ -37,6 +37,21 @@ New in spot 2.3.3.dev (not yet released) ...@@ -37,6 +37,21 @@ New in spot 2.3.3.dev (not yet released)
the second command outputs an automaton with states that show the second command outputs an automaton with states that show
references to the first one. references to the first one.
- spot::acc_cond::is_streett_like() returns whether an acceptance
condition is Streett-like, meaning it is a conjunction of
disjunctive clauses containing at most one Inf and at most one Fin.
It is more permissive than spot::acc_cond::is_streett(),
as the only requirement is that all the marks are present in the
acceptance condition.
In addition, the spot::acc_cond::streett_like_pairs() returns a
boolean that indicates if the acceptance condition is Streett-like
and takes a vector of the new struct spot::acc_cond::streett_pair,
which has members fin and inf, as an output parameter which
contains after the call to the function all the Streett-like pairs.
Likewise, spot::acc_cond::is_rabin_like() and
spot::acc_cond::rabin_like_pairs() are implemented for Rabin-like
pairs.
Bugs fixed: Bugs fixed:
- the transformation to state-based acceptance (spot::sbacc()) was - the transformation to state-based acceptance (spot::sbacc()) was
......
...@@ -441,7 +441,10 @@ namespace std { ...@@ -441,7 +441,10 @@ namespace std {
%implicitconv spot::acc_cond::acc_code; %implicitconv spot::acc_cond::acc_code;
%feature("flatnested") spot::acc_cond::mark_t; %feature("flatnested") spot::acc_cond::mark_t;
%feature("flatnested") spot::acc_cond::acc_code; %feature("flatnested") spot::acc_cond::acc_code;
%feature("flatnested") spot::acc_cond::rs_pair;
%apply bool* OUTPUT {bool& max, bool& odd}; %apply bool* OUTPUT {bool& max, bool& odd};
%template(vector_rs_pair) std::vector<spot::acc_cond::rs_pair>;
%apply std::vector<spot::acc_cond::rs_pair> &OUTPUT {std::vector<spot::acc_cond::rs_pair>& pairs}
%include <spot/twa/acc.hh> %include <spot/twa/acc.hh>
%template(pair_bool_mark) std::pair<bool, spot::acc_cond::mark_t>; %template(pair_bool_mark) std::pair<bool, spot::acc_cond::mark_t>;
......
...@@ -381,7 +381,7 @@ namespace spot ...@@ -381,7 +381,7 @@ namespace spot
{ {
if (s != 4 || mainop != lowop) if (s != 4 || mainop != lowop)
return false; return false;
// Pretend we where in a unary highop. // Pretend we were in a unary highop.
s = 5; s = 5;
} }
acc_cond::mark_t seen_fin = 0U; acc_cond::mark_t seen_fin = 0U;
...@@ -416,6 +416,96 @@ namespace spot ...@@ -416,6 +416,96 @@ namespace spot
return (!(seen_fin & seen_inf) return (!(seen_fin & seen_inf)
&& (seen_fin | seen_inf) == all_sets); && (seen_fin | seen_inf) == all_sets);
} }
// Is Rabin-like or Streett-like, depending on highop and lowop.
static bool
is_rs_like(const acc_cond::acc_code& code,
acc_cond::acc_op highop,
acc_cond::acc_op lowop,
std::vector<acc_cond::rs_pair>& pairs)
{
assert(pairs.empty());
unsigned s = code.back().sub.size;
auto mainop = code.back().sub.op;
if (mainop == acc_cond::acc_op::Fin || mainop == acc_cond::acc_op::Inf)
{
assert(code.size() != 2);
auto m = code[0].mark;
if (m.count() != 1)
return false;
acc_cond::mark_t fin(0U);
acc_cond::mark_t inf(0U);
if (mainop == acc_cond::acc_op::Fin)
fin = m;
else
inf = m;
pairs.emplace_back(fin, inf);
return true;
}
else if (mainop == lowop) // Single pair?
{
if (s != 4)
return false;
// Pretend we were in a unary highop.
s = 5;
}
else if (mainop != highop)
{
return false;
}
while (s)
{
auto op = code[--s].sub.op;
auto size = code[s].sub.size;
if (op == acc_cond::acc_op::Fin
|| op == acc_cond::acc_op::Inf)
{
auto m = code[--s].mark;
acc_cond::mark_t fin(0U);
acc_cond::mark_t inf(0U);
if (m.count() != 1)
return false;
if (op == acc_cond::acc_op::Fin)
fin = m;
else //fin
inf = m;
pairs.emplace_back(fin, inf);
}
else
{
if (op != lowop || size != 4)
return false;
auto o1 = code[--s].sub.op;
auto m1 = code[--s].mark;
auto o2 = code[--s].sub.op;
auto m2 = code[--s].mark;
// We assume
// Fin(n) lowop Inf(n+1)
// o1 (m1) o2 (m2)
// swap if it is the converse
if (o2 == acc_cond::acc_op::Fin)
{
std::swap(o1, o2);
std::swap(m1, m2);
}
if (o1 != acc_cond::acc_op::Fin
|| o2 != acc_cond::acc_op::Inf
|| m1.count() != 1
|| m2.count() != 1)
return false;
pairs.emplace_back(m1, m2);
}
}
return true;
}
} }
int acc_cond::is_rabin() const int acc_cond::is_rabin() const
...@@ -444,6 +534,32 @@ namespace spot ...@@ -444,6 +534,32 @@ namespace spot
return -1; return -1;
} }
bool acc_cond::is_streett_like(std::vector<rs_pair>& pairs) const
{
pairs.clear();
if (code_.is_t())
return true;
if (code_.is_f())
{
pairs.emplace_back(0U, 0U);
return true;
}
return is_rs_like(code_, acc_op::And, acc_op::Or, pairs);
}
bool acc_cond::is_rabin_like(std::vector<rs_pair>& pairs) const
{
pairs.clear();
if (code_.is_f())
return true;
if (code_.is_t())
{
pairs.emplace_back(0U, 0U);
return true;
}
return is_rs_like(code_, acc_op::Or, acc_op::And, pairs);
}
// PAIRS contains the number of Inf in each pair. // PAIRS contains the number of Inf in each pair.
bool acc_cond::is_generalized_rabin(std::vector<unsigned>& pairs) const bool acc_cond::is_generalized_rabin(std::vector<unsigned>& pairs) const
{ {
......
...@@ -1070,6 +1070,66 @@ namespace spot ...@@ -1070,6 +1070,66 @@ namespace spot
// Returns a number of pairs (>=0) if Streett, or -1 else. // Returns a number of pairs (>=0) if Streett, or -1 else.
int is_streett() const; int is_streett() const;
struct SPOT_API rs_pair
{
rs_pair() = default;
rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf):
fin(fin),
inf(inf)
{}
acc_cond::mark_t fin;
acc_cond::mark_t inf;
bool operator==(rs_pair o) const
{
return fin == o.fin && inf == o.inf;
}
bool operator!=(rs_pair o) const
{
return fin != o.fin || inf != o.inf;
}
bool operator<(rs_pair o) const
{
return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
}
bool operator<=(rs_pair o) const
{
return !(o < *this);
}
bool operator>(rs_pair o) const
{
return o < *this;
}
bool operator>=(rs_pair o) const
{
return !(*this < o);
}
};
/// \brief Test whether an acceptance condition is Streett-like
/// and returns each Streett pair in an std::vector<rs_pair>.
///
/// An acceptance condition is Streett-like if it can be transformed into
/// a Streett acceptance with little modification to its automaton.
/// A Streett-like acceptance condition follow one of those rules:
/// -It is a conjunction of disjunctive clauses containing at most one
/// Inf and at most one Fin.
/// -It is true (with 0 pair)
/// -It is false (1 pair [0U, 0U])
bool is_streett_like(std::vector<rs_pair>& pairs) const;
/// \brief Test whether an acceptance condition is Rabin-like
/// and returns each Rabin pair in an std::vector<rs_pair>.
///
/// An acceptance condition is Rabin-like if it can be transformed into
/// a Rabin acceptance with little modification to its automaton.
/// A Rabin-like acceptance condition follow one of those rules:
/// -It is a disjunction of conjunctive clauses containing at most one
/// Inf and at most one Fin.
/// -It is true (1 pair [0U, 0U])
/// -It is false (0 pairs)
bool is_rabin_like(std::vector<rs_pair>& pairs) const;
// Return the number of Inf in each pair. // Return the number of Inf in each pair.
bool is_generalized_rabin(std::vector<unsigned>& pairs) const; bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
......
...@@ -354,6 +354,7 @@ TESTS_python = \ ...@@ -354,6 +354,7 @@ TESTS_python = \
python/sccinfo.py \ python/sccinfo.py \
python/setacc.py \ python/setacc.py \
python/setxor.py \ python/setxor.py \
python/rs_like.py \
python/sum.py \ python/sum.py \
python/trival.py \ python/trival.py \
python/twagraph.py \ python/twagraph.py \
......
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
import spot
a = spot.vector_rs_pair()
m0 = spot.mark_t([0])
m1 = spot.mark_t([1])
m2 = spot.mark_t([2])
m3 = spot.mark_t([3])
mall = spot.mark_t()
def test_rs(acc, rs, expected_res, expected_pairs):
res, p = getattr(acc, 'is_' + rs + '_like')()
assert res == expected_res
if expected_res:
expected_pairs.sort()
p = sorted(p)
for a,b in zip (p, expected_pairs):
assert a.fin == b.fin and a.inf == b.inf
def switch_pairs(pairs):
if pairs == None:
return None
r = []
for p in pairs:
r.append(spot.rs_pair(p.inf, p.fin))
return r
def test_streett(acc, expected_streett_like, expected_pairs):
test_rs(acc, 'streett', expected_streett_like, expected_pairs)
o_acc = spot.acc_cond(acc.get_acceptance().complement())
test_rs(o_acc, 'rabin', expected_streett_like, switch_pairs(expected_pairs))
def test_rabin(acc, expected_rabin_like, expected_pairs):
test_rs(acc, 'rabin', expected_rabin_like, expected_pairs)
o_acc = spot.acc_cond(acc.get_acceptance().complement())
test_rs(o_acc, 'streett', expected_rabin_like, switch_pairs(expected_pairs))
acc = spot.acc_cond(spot.acc_code('Fin(0)|Inf(1)'))
test_streett(acc, True, [spot.rs_pair(m0, m1)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m2, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Inf(3)|Fin(2))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m2, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(3)|Inf(2))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m3, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(0)|Inf(2))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m0, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))'\
'&(Fin(3)&Inf(3))'))
test_streett(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2),\
spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)|Inf(1))&(Fin(1)|Inf(2))'\
'&(Fin(3)&Inf(3))&(Fin(4)|Inf(5)|Inf(6))'))
test_streett(acc, False, None)
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m2, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Inf(3)&Fin(2))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m2, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(3)&Inf(2))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m3, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(0)&Inf(2))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m0, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))'\
'|(Fin(3)|Inf(3))'))
test_rabin(acc, True, [spot.rs_pair(m0, m1), spot.rs_pair(m1, m2),\
spot.rs_pair(m3, mall), spot.rs_pair(mall, m3)])
acc = spot.acc_cond(spot.acc_code('(Fin(0)&Inf(1))|(Fin(1)&Inf(2))'\
'|(Fin(3)|Inf(3))|(Fin(4)&Inf(5)&Inf(6))'))
test_rabin(acc, False, None)
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