983964d037
Reported by Samuel Judson. * spot/twaalgos/strength.cc (is_safety_automaton): Reimplement it. * spot/twaalgos/strength.hh (is_safety_automaton): Update documentation. * tests/python/safety.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention this change. * THANKS: Add Samuel.
446 lines
13 KiB
C++
446 lines
13 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
|
|
//
|
|
// 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 <spot/twaalgos/strength.hh>
|
|
#include <spot/twaalgos/isweakscc.hh>
|
|
#include <spot/twaalgos/mask.hh>
|
|
#include <spot/twaalgos/minimize.hh>
|
|
#include <spot/twaalgos/isdet.hh>
|
|
#include <spot/twaalgos/sccfilter.hh>
|
|
#include <spot/twaalgos/contains.hh>
|
|
#include <spot/twaalgos/stripacc.hh>
|
|
|
|
using namespace std::string_literals;
|
|
|
|
namespace spot
|
|
{
|
|
namespace
|
|
{
|
|
template <bool terminal, bool inweak = false, bool set = false>
|
|
bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
// Create an scc_info if the user did not give one to us.
|
|
bool need_si = !si;
|
|
if (need_si)
|
|
si = new scc_info(aut);
|
|
if (inweak)
|
|
si->determine_unknown_acceptance();
|
|
|
|
acc_cond::mark_t mask = aut->get_acceptance().used_sets();
|
|
|
|
bool is_inweak = true;
|
|
bool is_weak = true;
|
|
bool is_single_state_scc = true;
|
|
bool is_term = true;
|
|
unsigned n = si->scc_count();
|
|
for (unsigned i = 0; i < n; ++i)
|
|
{
|
|
if (si->is_trivial(i))
|
|
continue;
|
|
if (si->states_of(i).size() > 1)
|
|
is_single_state_scc = false;
|
|
bool first = true;
|
|
acc_cond::mark_t m = {};
|
|
if (is_weak)
|
|
for (auto& t: si->edges_of(i))
|
|
// In case of a universal edge we only need to check if
|
|
// the first destination of an edge is inside the SCC,
|
|
// because the others have the same t.acc.
|
|
if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i)
|
|
{
|
|
if (first)
|
|
{
|
|
first = false;
|
|
m = t.acc & mask;
|
|
}
|
|
else if (m != (t.acc & mask))
|
|
{
|
|
is_weak = false;
|
|
if (!inweak)
|
|
goto exit;
|
|
}
|
|
}
|
|
if (!is_weak && si->is_accepting_scc(i))
|
|
{
|
|
assert(inweak);
|
|
if (scc_has_rejecting_cycle(*si, i))
|
|
{
|
|
is_inweak = false;
|
|
break;
|
|
}
|
|
}
|
|
if (terminal && is_term && si->is_accepting_scc(i))
|
|
{
|
|
is_term = is_complete_scc(*si, i);
|
|
if (is_term)
|
|
{
|
|
for (unsigned j: si->succ(i))
|
|
if (si->is_rejecting_scc(j))
|
|
{
|
|
is_term = false;
|
|
break;
|
|
}
|
|
}
|
|
if (!is_term && !set)
|
|
break;
|
|
}
|
|
}
|
|
exit:
|
|
if (need_si)
|
|
delete si;
|
|
if (set)
|
|
{
|
|
if (terminal)
|
|
aut->prop_terminal(is_term && is_weak);
|
|
aut->prop_weak(is_weak);
|
|
aut->prop_very_weak(is_single_state_scc && is_weak);
|
|
if (inweak)
|
|
aut->prop_inherently_weak(is_inweak);
|
|
}
|
|
if (inweak)
|
|
return is_inweak;
|
|
return is_weak && is_term;
|
|
}
|
|
}
|
|
|
|
bool
|
|
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
trival v = aut->prop_terminal();
|
|
if (v.is_known())
|
|
return v.is_true();
|
|
bool res =
|
|
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si);
|
|
std::const_pointer_cast<twa_graph>(aut)->prop_terminal(res);
|
|
return res;
|
|
}
|
|
|
|
bool
|
|
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si, bool)
|
|
{
|
|
return is_terminal_automaton(aut, si);
|
|
}
|
|
|
|
bool
|
|
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
trival v = aut->prop_weak();
|
|
if (v.is_known())
|
|
return v.is_true();
|
|
bool res =
|
|
is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut), si);
|
|
std::const_pointer_cast<twa_graph>(aut)->prop_weak(res);
|
|
return res;
|
|
}
|
|
|
|
bool
|
|
is_very_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
trival v = aut->prop_very_weak();
|
|
if (v.is_known())
|
|
return v.is_true();
|
|
is_type_automaton<false, false, true>
|
|
(std::const_pointer_cast<twa_graph>(aut), si);
|
|
return aut->prop_very_weak().is_true();
|
|
}
|
|
|
|
bool
|
|
is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
trival v = aut->prop_inherently_weak();
|
|
if (v.is_known())
|
|
return v.is_true();
|
|
bool res = is_type_automaton<false, true>
|
|
(std::const_pointer_cast<twa_graph>(aut), si);
|
|
std::const_pointer_cast<twa_graph>(aut)->prop_inherently_weak(res);
|
|
return res;
|
|
}
|
|
|
|
void check_strength(const twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
if (!aut->is_existential())
|
|
is_type_automaton<false, false, true>(aut, si);
|
|
else
|
|
is_type_automaton<true, true, true>(aut, si);
|
|
}
|
|
|
|
bool is_safety_automaton(const const_twa_graph_ptr& aut, scc_info* si)
|
|
{
|
|
if (aut->acc().is_t())
|
|
return true;
|
|
if (!aut->is_existential())
|
|
throw std::runtime_error
|
|
("is_safety_automaton() does not support alternation");
|
|
|
|
std::unique_ptr<scc_info> localsi;
|
|
if (!si)
|
|
{
|
|
localsi = std::make_unique<scc_info>(aut);
|
|
si = localsi.get();
|
|
}
|
|
si->determine_unknown_acceptance();
|
|
|
|
// a trim automaton without rejecting cycle is a safety automaton
|
|
bool has_rejecting_cycle = false;
|
|
|
|
// first, look for rejecting SCCs.
|
|
unsigned scccount = si->scc_count();
|
|
for (unsigned scc = 0; scc < scccount; ++scc)
|
|
if (si->is_useful_scc(scc)
|
|
&& !si->is_trivial(scc)
|
|
&& si->is_rejecting_scc(scc))
|
|
{
|
|
has_rejecting_cycle = true;
|
|
break;
|
|
}
|
|
if (!has_rejecting_cycle && !aut->prop_inherently_weak().is_true())
|
|
{
|
|
// maybe we have rejecting cycles inside accepting SCCs?
|
|
for (unsigned scc = 0; scc < scccount; ++scc)
|
|
if (si->is_useful_scc(scc)
|
|
&& !si->is_trivial(scc)
|
|
&& si->is_accepting_scc(scc)
|
|
&& scc_has_rejecting_cycle(*si, scc))
|
|
{
|
|
has_rejecting_cycle = true;
|
|
break;
|
|
}
|
|
}
|
|
if (!has_rejecting_cycle)
|
|
return true;
|
|
|
|
// If the automaton has a rejecting loop and is deterministic, it
|
|
// cannot be a safety automaton.
|
|
if (is_universal(aut))
|
|
return false;
|
|
|
|
twa_graph_ptr b = make_twa_graph(aut, twa::prop_set::all());
|
|
strip_acceptance_here(b);
|
|
return spot::contains(aut, b);
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
decompose_scc(scc_info& si, const char* keep_opt)
|
|
{
|
|
if (keep_opt == nullptr || *keep_opt == 0)
|
|
throw std::runtime_error
|
|
("option for decompose_scc() should not be empty");
|
|
|
|
enum strength {
|
|
Ignore = 0,
|
|
Terminal = 1,
|
|
WeakStrict = 2,
|
|
Weak = Terminal | WeakStrict,
|
|
Strong = 4,
|
|
Needed = 8, // Needed SCCs are those that lead to the SCCs we
|
|
// want to keep, and also unaccepting SCC we were
|
|
// asked to keep.
|
|
};
|
|
|
|
auto aut = si.get_aut();
|
|
si.determine_unknown_acceptance();
|
|
unsigned n = si.scc_count();
|
|
std::vector<unsigned char> want(n, Ignore);
|
|
|
|
unsigned char keep = Ignore;
|
|
while (auto c = *keep_opt++)
|
|
switch (c)
|
|
{
|
|
case ',':
|
|
case ' ':
|
|
break;
|
|
case '0': // SCC number N.
|
|
case '1':
|
|
case '2':
|
|
case '3':
|
|
case '4':
|
|
case '5':
|
|
case '6':
|
|
case '7':
|
|
case '8':
|
|
case '9':
|
|
{
|
|
char* endptr;
|
|
long int scc = strtol(keep_opt - 1, &endptr, 10);
|
|
if ((long unsigned) scc >= n)
|
|
{
|
|
throw std::runtime_error
|
|
("decompose_scc(): there is no SCC "s
|
|
+ std::to_string(scc) + " in this automaton");
|
|
}
|
|
keep_opt = endptr;
|
|
want[scc] = Needed;
|
|
break;
|
|
}
|
|
case 'a': // Accepting SCC number N.
|
|
{
|
|
char* endptr;
|
|
long int scc = strtol(keep_opt, &endptr, 10);
|
|
if (endptr == keep_opt)
|
|
throw std::runtime_error
|
|
("decompose_scc(): 'a' should be followed by an SCC number");
|
|
int j = 0;
|
|
for (unsigned s = 0; s < n; ++s)
|
|
if (si.is_accepting_scc(s))
|
|
if (j++ == scc)
|
|
{
|
|
want[s] = Needed;
|
|
break;
|
|
}
|
|
if (j != scc + 1)
|
|
{
|
|
throw std::runtime_error
|
|
("decompose_scc(): there is no SCC 'a"s
|
|
+ std::to_string(scc) + "' in this automaton");
|
|
}
|
|
keep_opt = endptr;
|
|
break;
|
|
}
|
|
case 's':
|
|
keep |= Strong;
|
|
break;
|
|
case 't':
|
|
keep |= Terminal;
|
|
break;
|
|
case 'w':
|
|
keep |= WeakStrict;
|
|
break;
|
|
default:
|
|
throw std::runtime_error
|
|
("unknown option for decompose_scc(): "s + c);
|
|
}
|
|
|
|
auto p = aut->acc().unsat_mark();
|
|
bool all_accepting = !p.first;
|
|
acc_cond::mark_t wacc = {}; // acceptance for weak SCCs
|
|
acc_cond::mark_t uacc = p.second; // Acceptance for "needed" SCCs, that
|
|
// we only want to traverse.
|
|
|
|
// If the acceptance condition is always satisfiable, we will
|
|
// consider the automaton as weak (even if that is not the
|
|
// case syntactically) and not output any strong part.
|
|
if (all_accepting)
|
|
keep &= ~Strong;
|
|
|
|
bool nonempty = false;
|
|
bool kept_scc_are_weak = true;
|
|
bool kept_scc_are_terminal = true;
|
|
|
|
for (unsigned i = 0; i < n; ++i) // SCC are topologically ordered
|
|
{
|
|
if (si.is_accepting_scc(i))
|
|
{
|
|
strength scc_strength = Ignore;
|
|
if (all_accepting | is_inherently_weak_scc(si, i))
|
|
scc_strength = is_complete_scc(si, i) ? Terminal : WeakStrict;
|
|
else
|
|
scc_strength = Strong;
|
|
|
|
if (want[i] == Needed)
|
|
want[i] = scc_strength;
|
|
else
|
|
want[i] = scc_strength & keep;
|
|
|
|
if (want[i])
|
|
{
|
|
if (!(scc_strength & Weak))
|
|
kept_scc_are_weak = false;
|
|
if (!(scc_strength & Terminal))
|
|
kept_scc_are_terminal = false;
|
|
}
|
|
}
|
|
|
|
nonempty |= want[i]; // also works "Needed" rejecting SCCs
|
|
|
|
// An SCC is needed if one of its successor is.
|
|
for (unsigned j: si.succ(i))
|
|
if (want[j])
|
|
{
|
|
want[i] |= Needed;
|
|
break;
|
|
}
|
|
}
|
|
|
|
if (!nonempty)
|
|
return nullptr;
|
|
|
|
twa_graph_ptr res = make_twa_graph(aut->get_dict());
|
|
res->copy_ap_of(aut);
|
|
res->prop_copy(aut, { true, false, false, true, false, false });
|
|
|
|
if (kept_scc_are_weak)
|
|
wacc = res->set_buchi();
|
|
else
|
|
res->copy_acceptance_of(aut);
|
|
|
|
auto fun = [&si, &want, uacc, wacc, kept_scc_are_weak]
|
|
(unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)
|
|
{
|
|
if (want[si.scc_of(dst)] == Ignore)
|
|
{
|
|
cond = bddfalse;
|
|
return;
|
|
}
|
|
if (want[si.scc_of(src)] == Needed)
|
|
{
|
|
acc = uacc;
|
|
return;
|
|
}
|
|
if (kept_scc_are_weak)
|
|
acc = wacc;
|
|
};
|
|
|
|
transform_accessible(aut, res, fun);
|
|
|
|
res->prop_weak(kept_scc_are_weak);
|
|
res->prop_terminal(kept_scc_are_terminal);
|
|
return res;
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
decompose_scc(const const_twa_graph_ptr& aut, const char* keep_opt)
|
|
{
|
|
scc_info si(aut);
|
|
return decompose_scc(si, keep_opt);
|
|
}
|
|
|
|
twa_graph_ptr
|
|
decompose_strength(const const_twa_graph_ptr& aut, const char* keep_opt)
|
|
{
|
|
return decompose_scc(aut, keep_opt);
|
|
}
|
|
|
|
twa_graph_ptr
|
|
decompose_scc(scc_info& sm, unsigned scc_num, bool accepting)
|
|
{
|
|
std::string num = std::to_string(scc_num);
|
|
return decompose_scc(sm, (accepting ? ('a' + num) : num).c_str());
|
|
}
|
|
|
|
bool
|
|
is_liveness_automaton(const const_twa_graph_ptr& aut)
|
|
{
|
|
auto mon = minimize_monitor(scc_filter_states(aut));
|
|
return mon->num_states() == 1 && is_complete(mon);
|
|
}
|
|
|
|
|
|
}
|