852abc770f
Reported by Reuben Rowe. * spot/twaalgos/complement.cc (complement): Remove the hard-coded simul=0 option on automata with >32 states. In 2.10 simul=0 now implies det-simul=0, causing the regression, and most importantly it is not needed anymore, because we have other threashold like simul-max and simul-trans-pruning in place. * tests/core/complement.test: Add Reuben's automaton as test case. * NEWS: Mention the fix.
538 lines
16 KiB
C++
538 lines
16 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2013-2015, 2017-2021 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/>.
|
|
|
|
#include "config.h"
|
|
#include <deque>
|
|
#include <map>
|
|
#include <spot/twaalgos/complement.hh>
|
|
#include <spot/twaalgos/dualize.hh>
|
|
#include <spot/twaalgos/isdet.hh>
|
|
#include <spot/twaalgos/alternation.hh>
|
|
#include <spot/twaalgos/postproc.hh>
|
|
#include <spot/twaalgos/strength.hh>
|
|
#include <spot/twaalgos/sccinfo.hh>
|
|
|
|
namespace spot
|
|
{
|
|
twa_graph_ptr
|
|
dtwa_complement(const const_twa_graph_ptr& aut)
|
|
{
|
|
if (!is_deterministic(aut))
|
|
throw
|
|
std::runtime_error("dtwa_complement() requires a deterministic input");
|
|
|
|
return dualize(aut);
|
|
}
|
|
|
|
namespace
|
|
{
|
|
enum ncsb
|
|
{
|
|
ncsb_n = 0, // non deterministic
|
|
ncsb_c = 2, // needs check
|
|
ncsb_cb = 3, // needs check AND in breakpoint
|
|
ncsb_s = 4, // safe
|
|
ncsb_m = 1, // missing
|
|
};
|
|
|
|
typedef std::vector<ncsb> mstate;
|
|
typedef std::vector<std::pair<unsigned, ncsb>> small_mstate;
|
|
|
|
struct small_mstate_hash
|
|
{
|
|
size_t
|
|
operator()(small_mstate s) const noexcept
|
|
{
|
|
size_t hash = 0;
|
|
for (const auto& p: s)
|
|
{
|
|
hash = wang32_hash(hash ^ ((p.first<<2) | p.second));
|
|
}
|
|
return hash;
|
|
}
|
|
};
|
|
|
|
class ncsb_complementation
|
|
{
|
|
private:
|
|
// The source automaton.
|
|
const const_twa_graph_ptr aut_;
|
|
|
|
// SCCs information of the source automaton.
|
|
scc_info si_;
|
|
|
|
// Number of states in the input automaton.
|
|
unsigned nb_states_;
|
|
|
|
// The complement being built.
|
|
twa_graph_ptr res_;
|
|
|
|
// Association between NCSB states and state numbers of the
|
|
// complement.
|
|
std::unordered_map<small_mstate, unsigned, small_mstate_hash> ncsb2n_;
|
|
|
|
// States to process.
|
|
std::deque<std::pair<mstate, unsigned>> todo_;
|
|
|
|
// Support for each state of the source automaton.
|
|
std::vector<bdd> support_;
|
|
|
|
// Propositions compatible with all transitions of a state.
|
|
std::vector<bdd> compat_;
|
|
|
|
// Whether a SCC is deterministic or not
|
|
std::vector<bool> is_deter_;
|
|
|
|
// Whether a state only has accepting transitions
|
|
std::vector<bool> is_accepting_;
|
|
|
|
// State names for graphviz display
|
|
std::vector<std::string>* names_;
|
|
|
|
// Show NCSB states in state name to help debug
|
|
bool show_names_;
|
|
|
|
std::string
|
|
get_name(const small_mstate& ms)
|
|
{
|
|
std::string res = "{";
|
|
|
|
bool first_state = true;
|
|
for (const auto& p: ms)
|
|
if (p.second == ncsb_n)
|
|
{
|
|
if (!first_state)
|
|
res += ",";
|
|
first_state = false;
|
|
res += std::to_string(p.first);
|
|
}
|
|
|
|
res += "},{";
|
|
|
|
first_state = true;
|
|
for (const auto& p: ms)
|
|
if (p.second & ncsb_c)
|
|
{
|
|
if (!first_state)
|
|
res += ",";
|
|
first_state = false;
|
|
res += std::to_string(p.first);
|
|
}
|
|
|
|
res += "},{";
|
|
|
|
first_state = true;
|
|
for (const auto& p: ms)
|
|
if (p.second == ncsb_s)
|
|
{
|
|
if (!first_state)
|
|
res += ",";
|
|
first_state = false;
|
|
res += std::to_string(p.first);
|
|
}
|
|
|
|
res += "},{";
|
|
|
|
first_state = true;
|
|
for (const auto& p: ms)
|
|
if (p.second == ncsb_cb)
|
|
{
|
|
if (!first_state)
|
|
res += ",";
|
|
first_state = false;
|
|
res += std::to_string(p.first);
|
|
}
|
|
|
|
return res + "}";
|
|
}
|
|
|
|
small_mstate
|
|
to_small_mstate(const mstate& ms)
|
|
{
|
|
unsigned count = 0;
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
count+= (ms[i] != ncsb_m);
|
|
small_mstate small;
|
|
small.reserve(count);
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
if (ms[i] != ncsb_m)
|
|
small.emplace_back(i, ms[i]);
|
|
return small;
|
|
}
|
|
|
|
// From a NCSB state, looks for a duplicate in the map before
|
|
// creating a new state if needed.
|
|
unsigned
|
|
new_state(mstate&& s)
|
|
{
|
|
auto p = ncsb2n_.emplace(to_small_mstate(s), 0);
|
|
if (p.second) // This is a new state
|
|
{
|
|
p.first->second = res_->new_state();
|
|
if (show_names_)
|
|
names_->push_back(get_name(p.first->first));
|
|
todo_.emplace_back(std::move(s), p.first->second);
|
|
}
|
|
return p.first->second;
|
|
}
|
|
|
|
void
|
|
ncsb_successors(mstate&& ms, unsigned origin, bdd letter)
|
|
{
|
|
std::vector<mstate> succs;
|
|
succs.emplace_back(nb_states_, ncsb_m);
|
|
|
|
// Handle S states.
|
|
//
|
|
// Treated first because we can escape early if the letter
|
|
// leads to an accepting transition for a Safe state.
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
{
|
|
if (ms[i] != ncsb_s)
|
|
continue;
|
|
|
|
for (const auto& t: aut_->out(i))
|
|
{
|
|
if (!bdd_implies(letter, t.cond))
|
|
continue;
|
|
if (t.acc || is_accepting_[t.dst])
|
|
// Exit early; transition is forbidden for safe
|
|
// state.
|
|
return;
|
|
|
|
succs[0][t.dst] = ncsb_s;
|
|
|
|
// No need to look for other compatible transitions
|
|
// for this state; it's in the deterministic part of
|
|
// the automaton
|
|
break;
|
|
}
|
|
}
|
|
|
|
// Handle C states.
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
{
|
|
if (!(ms[i] & ncsb_c))
|
|
continue;
|
|
|
|
bool has_succ = false;
|
|
for (const auto& t: aut_->out(i))
|
|
{
|
|
if (!bdd_implies(letter, t.cond))
|
|
continue;
|
|
|
|
has_succ = true;
|
|
|
|
// state can become safe, if transition is accepting
|
|
// and destination isn't an accepting state
|
|
if (t.acc)
|
|
{
|
|
// double all the current possible states
|
|
unsigned length = succs.size();
|
|
for (unsigned j = 0; j < length; ++j)
|
|
{
|
|
if (succs[j][t.dst] == ncsb_m)
|
|
{
|
|
if (!is_accepting_[t.dst])
|
|
{
|
|
succs.push_back(succs[j]);
|
|
succs.back()[t.dst] = ncsb_s;
|
|
}
|
|
succs[j][t.dst] = ncsb_c;
|
|
}
|
|
}
|
|
}
|
|
else // state stays in check
|
|
{
|
|
// remove states that should stay in s (ncsb_s),
|
|
// and mark the other as ncsb_c.
|
|
// The first two loops form a kind of remove_if()
|
|
// that set the non-removed states to ncsb_c.
|
|
auto it = succs.begin();
|
|
auto end = succs.end();
|
|
for (; it != end; ++it)
|
|
if ((*it)[t.dst] != ncsb_s)
|
|
(*it)[t.dst] = ncsb_c;
|
|
else
|
|
break;
|
|
if (it != end)
|
|
for (auto it2 = it; ++it2 != end;)
|
|
if ((*it2)[t.dst] != ncsb_s)
|
|
*it++ = std::move(*it2);
|
|
succs.erase(it, end);
|
|
}
|
|
// No need to look for other compatible transitions
|
|
// for this state; it's in the deterministic part of
|
|
// the automaton
|
|
break;
|
|
}
|
|
if (!has_succ && !is_accepting_[i])
|
|
return;
|
|
}
|
|
|
|
// Handle N states.
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
{
|
|
if (ms[i] != ncsb_n)
|
|
continue;
|
|
for (const auto& t: aut_->out(i))
|
|
{
|
|
if (!bdd_implies(letter, t.cond))
|
|
continue;
|
|
|
|
if (is_deter_[si_.scc_of(t.dst)])
|
|
{
|
|
// double all the current possible states
|
|
unsigned length = succs.size();
|
|
for (unsigned j = 0; j < length; ++j)
|
|
{
|
|
if (succs[j][t.dst] == ncsb_m)
|
|
{
|
|
// Can become safe if the destination is
|
|
// not an accepting state.
|
|
if (!is_accepting_[t.dst])
|
|
{
|
|
succs.push_back(succs[j]);
|
|
succs.back()[t.dst] = ncsb_s;
|
|
}
|
|
succs[j][t.dst] = ncsb_c;
|
|
}
|
|
}
|
|
}
|
|
else
|
|
for (auto& succ: succs)
|
|
succ[t.dst] = ncsb_n;
|
|
}
|
|
}
|
|
|
|
// Revisit B states to see if they still exist in successors.
|
|
// This is done at the end because we need to know all of the
|
|
// states present in C before this stage
|
|
bool b_empty = true;
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
{
|
|
if (ms[i] != ncsb_cb)
|
|
continue;
|
|
|
|
// The original B set wasn't empty
|
|
b_empty = false;
|
|
|
|
for (const auto& t: aut_->out(i))
|
|
{
|
|
if (!bdd_implies(letter, t.cond))
|
|
continue;
|
|
|
|
for (auto& succ: succs)
|
|
{
|
|
if (succ[t.dst] == ncsb_c)
|
|
succ[t.dst] = ncsb_cb;
|
|
}
|
|
|
|
// No need to look for other compatible transitions
|
|
// for this state; it's in the deterministic part of
|
|
// the automaton
|
|
break;
|
|
}
|
|
}
|
|
|
|
// If B was empty, then set every c_not_b to cb in successors
|
|
if (b_empty)
|
|
for (auto& succ: succs)
|
|
for (unsigned i = 0; i < succ.size(); ++i)
|
|
if (succ[i] == ncsb_c)
|
|
succ[i] = ncsb_cb;
|
|
|
|
// create the automaton states
|
|
for (auto& succ: succs)
|
|
{
|
|
bool b_empty = true;
|
|
for (const auto& state: succ)
|
|
if (state == ncsb_cb)
|
|
{
|
|
b_empty = false;
|
|
break;
|
|
}
|
|
if (b_empty) // becomes accepting
|
|
{
|
|
for (unsigned i = 0; i < succ.size(); ++i)
|
|
if (succ[i] == ncsb_c)
|
|
succ[i] = ncsb_cb;
|
|
unsigned dst = new_state(std::move(succ));
|
|
res_->new_edge(origin, dst, letter, {0});
|
|
}
|
|
else
|
|
{
|
|
unsigned dst = new_state(std::move(succ));
|
|
res_->new_edge(origin, dst, letter);
|
|
}
|
|
}
|
|
}
|
|
|
|
public:
|
|
ncsb_complementation(const const_twa_graph_ptr& aut, bool show_names)
|
|
: aut_(aut),
|
|
si_(aut),
|
|
nb_states_(aut->num_states()),
|
|
support_(nb_states_),
|
|
compat_(nb_states_),
|
|
is_accepting_(nb_states_),
|
|
show_names_(show_names)
|
|
{
|
|
res_ = make_twa_graph(aut->get_dict());
|
|
res_->copy_ap_of(aut);
|
|
res_->set_buchi();
|
|
|
|
// Generate bdd supports and compatible options for each state.
|
|
// Also check if all its transitions are accepting.
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
{
|
|
bdd res_support = bddtrue;
|
|
bdd res_compat = bddfalse;
|
|
bool accepting = true;
|
|
bool has_transitions = false;
|
|
for (const auto& out: aut->out(i))
|
|
{
|
|
has_transitions = true;
|
|
res_support &= bdd_support(out.cond);
|
|
res_compat |= out.cond;
|
|
if (!out.acc)
|
|
accepting = false;
|
|
}
|
|
support_[i] = res_support;
|
|
compat_[i] = res_compat;
|
|
is_accepting_[i] = accepting && has_transitions;
|
|
}
|
|
|
|
|
|
|
|
// Compute which SCCs are part of the deterministic set.
|
|
is_deter_ = semidet_sccs(si_);
|
|
|
|
if (show_names_)
|
|
{
|
|
names_ = new std::vector<std::string>();
|
|
res_->set_named_prop("state-names", names_);
|
|
}
|
|
|
|
// Because we only handle one initial state, we assume it
|
|
// belongs to the N set. (otherwise the automaton would be
|
|
// deterministic)
|
|
unsigned init_state = aut->get_init_state_number();
|
|
mstate new_init_state(nb_states_, ncsb_m);
|
|
new_init_state[init_state] = ncsb_n;
|
|
res_->set_init_state(new_state(std::move(new_init_state)));
|
|
}
|
|
|
|
twa_graph_ptr
|
|
run()
|
|
{
|
|
// Main stuff happens here
|
|
|
|
while (!todo_.empty())
|
|
{
|
|
auto top = todo_.front();
|
|
todo_.pop_front();
|
|
|
|
mstate ms = top.first;
|
|
|
|
// Compute support of all available states.
|
|
bdd msupport = bddtrue;
|
|
bdd n_s_compat = bddfalse;
|
|
bdd c_compat = bddtrue;
|
|
bool c_empty = true;
|
|
for (unsigned i = 0; i < nb_states_; ++i)
|
|
if (ms[i] != ncsb_m)
|
|
{
|
|
msupport &= support_[i];
|
|
if (ms[i] == ncsb_n || ms[i] == ncsb_s || is_accepting_[i])
|
|
n_s_compat |= compat_[i];
|
|
else
|
|
{
|
|
c_empty = false;
|
|
c_compat &= compat_[i];
|
|
}
|
|
}
|
|
|
|
bdd all;
|
|
if (!c_empty)
|
|
all = c_compat;
|
|
else
|
|
{
|
|
all = n_s_compat;
|
|
if (all != bddtrue)
|
|
{
|
|
mstate empty_state(nb_states_, ncsb_m);
|
|
res_->new_edge(top.second,
|
|
new_state(std::move(empty_state)),
|
|
!all,
|
|
{0});
|
|
}
|
|
}
|
|
for (bdd one: minterms_of(all, msupport))
|
|
// Compute all new states available from the generated
|
|
// letter.
|
|
ncsb_successors(std::move(ms), top.second, one);
|
|
}
|
|
|
|
res_->merge_edges();
|
|
return res_;
|
|
}
|
|
};
|
|
|
|
}
|
|
|
|
twa_graph_ptr
|
|
complement_semidet(const const_twa_graph_ptr& aut, bool show_names)
|
|
{
|
|
if (!is_semi_deterministic(aut))
|
|
throw std::runtime_error
|
|
("complement_semidet() requires a semi-deterministic input");
|
|
|
|
auto ncsb = ncsb_complementation(aut, show_names);
|
|
return ncsb.run();
|
|
}
|
|
|
|
twa_graph_ptr
|
|
complement(const const_twa_graph_ptr& aut, const output_aborter* aborter)
|
|
{
|
|
if (!aut->is_existential() || is_universal(aut))
|
|
return dualize(aut);
|
|
if (is_very_weak_automaton(aut))
|
|
return remove_alternation(dualize(aut), aborter);
|
|
// Determinize
|
|
spot::option_map m;
|
|
if (aborter)
|
|
{
|
|
m.set("det-max-states", aborter->max_states());
|
|
m.set("det-max-edges", aborter->max_edges());
|
|
}
|
|
// In addition to the above options, the simulation-based
|
|
// optimization of the determinization is already restricted by
|
|
// the default values of simul-max and simul-trans-pruning.
|
|
// (See spot-x(7) for details.)
|
|
spot::postprocessor p(&m);
|
|
p.set_type(spot::postprocessor::Generic);
|
|
p.set_pref(spot::postprocessor::Deterministic);
|
|
p.set_level(spot::postprocessor::Low);
|
|
auto det = p.run(std::const_pointer_cast<twa_graph>(aut));
|
|
if (!det || !is_universal(det))
|
|
return nullptr;
|
|
return dualize(det);
|
|
}
|
|
}
|