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

scc_has_rejecting_cycle: rewrite without copy

Browse source 
* spot/twaalgos/genem.hh, spot/twaalgos/genem.cc
(generic_emptiness_check_for_scc): Add a version that takes an acc.
* spot/twaalgos/isweakscc.cc (scc_has_rejecting_cycle): Use
generic_emptiness_check_for_scc.
This commit is contained in:
Alexandre Duret-Lutz 2019-06-21 22:36:33 +02:00
parent c830b5db25
commit 030ebed367
3 changed files with 25 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

15
spot/twaalgos/genem.cc
View file

@ -75,6 +75,8 @@ namespace spot
else
{
int fo = acc.fin_one();
if (fo < 0)
std::cerr << autacc << acc << '\n';
assert(fo >= 0);
// Try to accept when Fin(fo) == true
acc_cond::mark_t fo_m = {(unsigned) fo};
@ -160,9 +162,16 @@ namespace spot
bool generic_emptiness_check_for_scc(const scc_info& si,
unsigned scc)
{
if (SPOT_UNLIKELY(!si.get_aut()->is_existential()))
throw std::runtime_error("generic_emptiness_check_for_scc() "
"does not support alternating automata");
return is_scc_empty(si, scc, si.get_aut()->acc(), nullptr);
}
bool
generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
const acc_cond& forced_acc)
{
if (si.is_trivial(scc))
return true;
return scc_split_check(si, scc, forced_acc, nullptr, {});
}
}

9
spot/twaalgos/genem.hh
View file

@ -40,4 +40,13 @@ namespace spot
/// \brief Emptiness check of one SCC, for any acceptance condition.
SPOT_API bool
generic_emptiness_check_for_scc(const scc_info& si, unsigned scc);
/// \ingroup emptiness_check_algorithms
/// \brief Emptiness check of one SCC, for any acceptance condition.
///
/// This version makes it possible to ignore the acceptance
/// condition of the automaton, and use \a forced_acc.
SPOT_API bool
generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
const acc_cond& forced_acc);
}

18
spot/twaalgos/isweakscc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -20,7 +20,7 @@
#include "config.h"
#include <spot/tl/formula.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/genem.hh>
namespace spot
{
@ -38,18 +38,8 @@ namespace spot
{
if (SPOT_UNLIKELY(scc >= map.scc_count()))
invalid_scc_number("scc_has_rejecting_cycle");
auto aut = map.get_aut();
// We check that by cloning the SCC and complementing its
// acceptance condition.
std::vector<bool> keep(aut->num_states(), false);
auto& states = map.states_of(scc);
for (auto s: states)
keep[s] = true;
auto sccaut = mask_keep_accessible_states(aut, keep, states.front(),
/* drop_univ_branch = */ true);
sccaut->set_acceptance(sccaut->acc().num_sets(),
sccaut->get_acceptance().complement());
return !sccaut->is_empty();
acc_cond neg_acc = map.get_aut()->get_acceptance().complement();
return !generic_emptiness_check_for_scc(map, scc, neg_acc);
}
bool