alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

improve readability of parity(false, true, 5)

Browse source 
* spot/twa/acc.hh: Introduce parity_min_odd(n) and friends.
* spot/twaalgos/determinize.cc, spot/twaalgos/rabin2parity.cc,
spot/twaalgos/toparity.cc: Use them.
* tests/python/parity.py: Call each function exhaustively.
* NEWS: Mention the new functions.
This commit is contained in:
Alexandre Duret-Lutz 2019-10-08 15:18:48 +02:00
parent b2539e8399
commit 566a43dd17
6 changed files with 74 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

10
NEWS
View file

@ -30,6 +30,16 @@ New in spot 2.8.2.dev (not yet released)
variants of F[n:m] and G[n:m], but those four are only implemented
as syntactic sugar.
- acc_cond::acc_code::parity(bool, bool, int) was not very readable,
as it was unclear to the reader what the boolean argument meant.
The following sister functions can now improve readability:
parity_max(is_odd, n) = parity(true, is_odd, n)
parity_max_odd(n) = parity_max(true, n)
parity_max_even(n) = parity_max(false, n)
parity_min(is_odd, n) = parity(false, is_odd, n)
parity_min_odd(n) = parity_min(true, n)
parity_min_even(n) = parity_min(false, n)
Python:
- Doing "import spot.foo" will now load any spot-extra/foo.py on

32
spot/twa/acc.hh
View file

@ -816,11 +816,37 @@ namespace spot
/// \brief Build a parity acceptance condition
///
/// In parity acceptance a word is accepting if the maximum (or
/// In parity acceptance a run is accepting if the maximum (or
/// minimum) set number that is seen infinitely often is odd (or
/// even). This function will build a formula for that, as
/// even). These functions will build a formula for that, as
/// specified in the HOA format.
static acc_code parity(bool max, bool odd, unsigned sets);
/// @{
static acc_code parity(bool is_max, bool is_odd, unsigned sets);
static acc_code parity_max(bool is_odd, unsigned sets)
{
return parity(true, is_odd, sets);
}
static acc_code parity_max_odd(unsigned sets)
{
return parity_max(true, sets);
}
static acc_code parity_max_even(unsigned sets)
{
return parity_max(false, sets);
}
static acc_code parity_min(bool is_odd, unsigned sets)
{
return parity(false, is_odd, sets);
}
static acc_code parity_min_odd(unsigned sets)
{
return parity_min(true, sets);
}
static acc_code parity_min_even(unsigned sets)
{
return parity_min(false, sets);
}
/// @}
/// \brief Build a random acceptance condition
///

2
spot/twaalgos/determinize.cc
View file

@ -965,7 +965,7 @@ namespace spot
if (sets % 2 == 1)
sets += 1;
// Acceptance is now min(odd) since we can emit Red on paths 0 with new opti
res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
res->set_acceptance(sets, acc_cond::acc_code::parity_min_odd(sets));
res->prop_universal(true);
res->prop_state_acc(false);

28
spot/twaalgos/rabin2parity.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -77,19 +77,19 @@ namespace spot
build_iar_scc(scc_.initial());
// resulting automaton has acceptance condition: parity max odd
// with priorities ranging from 0 to 2*(nb pairs)
// /!\ priorities are shifted by -1 compared to the original paper
if (is_rabin)
res_->set_acceptance(2*pairs_.size() + 1,
acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1));
else
res_->set_acceptance(2*pairs_.size() + 1,
acc_cond::acc_code::parity(true, false, 2*pairs_.size() + 1));
// set initial state
res_->set_init_state(
iar2num.at(state2iar.at(aut_->get_init_state_number())));
{
// resulting automaton has acceptance condition: parity max odd
// for Rabin-like input and parity max even for Streett-like input.
// with priorities ranging from 0 to 2*(nb pairs)
// /!\ priorities are shifted by -1 compared to the original paper
unsigned sets = 2 * pairs_.size() + 1;
res_->set_acceptance(sets, acc_cond::acc_code::parity_max(is_rabin,
sets));
}
{
unsigned s = iar2num.at(state2iar.at(aut_->get_init_state_number()));
res_->set_init_state(s);
}
// there could be quite a number of unreachable states, prune them
res_->purge_unreachable_states();

13
spot/twaalgos/toparity.cc
View file

@ -128,18 +128,17 @@ namespace spot
lar_state dst{e.dst, new_perm};
unsigned dst_num = get_state(dst);
// do the h last elements satisfy the acceptance condition?
// Do the h last elements satisfy the acceptance condition?
// If they do, emit 2h, if they don't emit 2h+1.
acc_cond::mark_t m(new_perm.end() - h, new_perm.end());
if (aut_->acc().accepting(m))
res_->new_edge(src_num, dst_num, e.cond, {2*h});
else
res_->new_edge(src_num, dst_num, e.cond, {2*h+1});
bool rej = !aut_->acc().accepting(m);
res_->new_edge(src_num, dst_num, e.cond, {2*h + rej});
}
}
// parity max even
res_->set_acceptance(2*aut_->num_sets() + 2,
acc_cond::acc_code::parity(true, false, 2*aut_->num_sets() + 2));
unsigned sets = 2*aut_->num_sets() + 2;
res_->set_acceptance(sets, acc_cond::acc_code::parity_max_even(sets));
if (pretty_print)
{

14
tests/python/parity.py
View file

@ -20,6 +20,20 @@
import spot
max_even_5 = spot.acc_code.parity(True, False, 5)
assert max_even_5 == spot.acc_code.parity_max_even(5)
assert max_even_5 == spot.acc_code.parity_max(False, 5)
min_even_5 = spot.acc_code.parity(False, False, 5)
assert min_even_5 == spot.acc_code.parity_min_even(5)
assert min_even_5 == spot.acc_code.parity_min(False, 5)
max_odd_5 = spot.acc_code.parity(True, True, 5)
assert max_odd_5 == spot.acc_code.parity_max_odd(5)
assert max_odd_5 == spot.acc_code.parity_max(True, 5)
min_odd_5 = spot.acc_code.parity(False, True, 5)
assert min_odd_5 == spot.acc_code.parity_min_odd(5)
assert min_odd_5 == spot.acc_code.parity_min(True, 5)
for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
a1 = spot.translate(f, 'parity')