// -*- coding: utf-8 -*-
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE)
//
// 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 .
#include "config.h"
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
using namespace std::string_literals;
namespace spot
{
namespace
{
static bool
cobuchi_realizable(spot::formula f,
const const_twa_graph_ptr& aut)
{
// Find which algorithm must be performed between nsa_to_nca() and
// dnf_to_nca(). Throw an exception if none of them can be performed.
std::vector pairs;
bool street_or_parity = aut->acc().is_streett_like(pairs)
|| aut->acc().is_parity();
if (!street_or_parity && !aut->get_acceptance().is_dnf())
throw std::runtime_error("cobuchi_realizable() only works with "
"Streett-like, Parity or any "
"acceptance condition in DNF");
// If !f is a DBA, it belongs to the recurrence class, which means
// f belongs to the persistence class (is cobuchi_realizable).
twa_graph_ptr not_aut = ltl_to_tgba_fm(formula::Not(f), aut->get_dict());
not_aut = scc_filter(not_aut);
if (is_universal(not_aut))
return true;
// Checks if f is cobuchi_realizable.
twa_graph_ptr cobuchi = street_or_parity ? nsa_to_nca(aut)
: dnf_to_nca(aut);
return !cobuchi->intersects(not_aut);
}
[[noreturn]] static void invalid_spot_pr_check()
{
throw std::runtime_error("invalid value for SPOT_PR_CHECK "
"(should be 1, 2, or 3)");
}
static prcheck
algo_to_perform(bool is_persistence, bool aut_given)
{
static unsigned value = [&]()
{
int val;
try
{
auto s = getenv("SPOT_PR_CHECK");
val = s ? std::stoi(s) : 0;
}
catch (const std::exception& e)
{
invalid_spot_pr_check();
}
if (val < 0 || val > 3)
invalid_spot_pr_check();
return val;
}();
switch (value)
{
case 0:
if (aut_given && !is_persistence)
return prcheck::via_Parity;
else
return prcheck::via_CoBuchi;
case 1:
return prcheck::via_CoBuchi;
case 2:
return prcheck::via_Rabin;
case 3:
return prcheck::via_Parity;
default:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
return prcheck::via_Parity;
}
static bool
detbuchi_realizable(const twa_graph_ptr& aut)
{
if (is_universal(aut))
return true;
bool want_old = algo_to_perform(false, true) == prcheck::via_Rabin;
if (want_old)
{
// if aut is a non-deterministic TGBA, we do
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
// BA will preserve determinism if possible.
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dpa = p.run(aut);
if (dpa->acc().is_generalized_buchi())
{
assert(is_deterministic(dpa));
return true;
}
else
{
auto dra = to_generalized_rabin(dpa);
return rabin_is_buchi_realizable(dra);
}
}
// Converting reduce_parity() will produce a Büchi automaton (or
// an automaton with "t" or "f" acceptance) if the parity
// automaton is DBA-realizable.
spot::postprocessor p;
p.set_type(spot::postprocessor::Parity);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dpa = p.run(aut);
return dpa->acc().is_f() || dpa->acc().is_generalized_buchi();
}
}
bool
is_persistence(formula f, twa_graph_ptr aut, prcheck algo)
{
if (f.is_syntactic_persistence())
return true;
// Perform a quick simplification of the formula taking into account the
// following simplification's parameters: basics, synt_impl, event_univ.
spot::tl_simplifier simpl(spot::tl_simplifier_options(true, true, true));
f = simpl.simplify(f);
if (f.is_syntactic_persistence())
return true;
if (algo == prcheck::Auto)
algo = algo_to_perform(true, aut != nullptr);
switch (algo)
{
case prcheck::via_CoBuchi:
return cobuchi_realizable(f, aut ? aut :
ltl_to_tgba_fm(f, make_bdd_dict(), true));
case prcheck::via_Rabin:
case prcheck::via_Parity:
return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f),
make_bdd_dict(), true));
case prcheck::Auto:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
}
bool
is_recurrence(formula f, twa_graph_ptr aut, prcheck algo)
{
if (f.is_syntactic_recurrence())
return true;
// Perform a quick simplification of the formula taking into account the
// following simplification's parameters: basics, synt_impl, event_univ.
spot::tl_simplifier simpl(spot::tl_simplifier_options(true, true, true));
f = simpl.simplify(f);
if (f.is_syntactic_recurrence())
return true;
if (algo == prcheck::Auto)
algo = algo_to_perform(true, aut != nullptr);
switch (algo)
{
case prcheck::via_CoBuchi:
return cobuchi_realizable(formula::Not(f),
ltl_to_tgba_fm(formula::Not(f),
make_bdd_dict(), true));
case prcheck::via_Rabin:
case prcheck::via_Parity:
return detbuchi_realizable(aut ? aut :
ltl_to_tgba_fm(f, make_bdd_dict(), true));
case prcheck::Auto:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
}
[[noreturn]] static void invalid_spot_o_check()
{
throw std::runtime_error("invalid value for SPOT_O_CHECK "
"(should be 1, 2, or 3)");
}
// This private function is defined in minimize.cc for technical
// reasons.
SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr);
bool
is_obligation(formula f, twa_graph_ptr aut, ocheck algo)
{
if (algo == ocheck::Auto)
{
static ocheck env_algo = []()
{
int val;
try
{
auto s = getenv("SPOT_O_CHECK");
val = s ? std::stoi(s) : 0;
}
catch (const std::exception& e)
{
invalid_spot_o_check();
}
if (val == 0)
return ocheck::via_WDBA;
else if (val == 1)
return ocheck::via_CoBuchi;
else if (val == 2)
return ocheck::via_Rabin;
else if (val == 3)
return ocheck::via_WDBA;
else
invalid_spot_o_check();
}();
algo = env_algo;
}
switch (algo)
{
case ocheck::via_WDBA:
return is_wdba_realizable(f, aut);
case ocheck::via_CoBuchi:
return (is_persistence(f, aut, prcheck::via_CoBuchi)
&& is_recurrence(f, aut, prcheck::via_CoBuchi));
case ocheck::via_Rabin:
return (is_persistence(f, aut, prcheck::via_Rabin)
&& is_recurrence(f, aut, prcheck::via_Rabin));
case ocheck::Auto:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
}
char mp_class(formula f)
{
if (f.is_syntactic_safety() && f.is_syntactic_guarantee())
return 'B';
auto dict = make_bdd_dict();
auto aut = ltl_to_tgba_fm(f, dict, true);
auto min = minimize_obligation(aut, f);
if (aut != min) // An obligation.
{
scc_info si(min);
// The minimba WDBA can have some trivial accepting SCCs
// that we should ignore in is_terminal_automaton().
bool g = is_terminal_automaton(min, &si, true);
bool s = is_safety_automaton(min, &si);
if (g)
return s ? 'B' : 'G';
else
return s ? 'S' : 'O';
}
// Not an obligation. Could by 'P', 'R', or 'T'.
if (is_recurrence(f, aut))
return 'R';
if (is_persistence(f, aut))
return 'P';
return 'T';
}
std::string mp_class(formula f, const char* opt)
{
return mp_class(mp_class(f), opt);
}
std::string mp_class(char mpc, const char* opt)
{
bool verbose = false;
bool wide = false;
if (opt)
for (;;)
switch (int o = *opt++)
{
case 'v':
verbose = true;
break;
case 'w':
wide = true;
break;
case ' ':
case '\t':
case '\n':
case ',':
break;
case '\0':
case ']':
goto break2;
default:
{
std::ostringstream err;
err << "unknown option '" << o << "' for mp_class()";
throw std::runtime_error(err.str());
}
}
break2:
std::string c(1, mpc);
if (wide)
{
switch (mpc)
{
case 'B':
c = "GSOPRT";
break;
case 'G':
c = "GOPRT";
break;
case 'S':
c = "SOPRT";
break;
case 'O':
c = "OPRT";
break;
case 'P':
c = "PT";
break;
case 'R':
c = "RT";
break;
case 'T':
break;
default:
throw std::runtime_error("mp_class() called with unknown class");
}
}
if (!verbose)
return c;
std::ostringstream os;
bool first = true;
for (char ch: c)
{
if (first)
first = false;
else
os << ' ';
switch (ch)
{
case 'B':
os << "guarantee safety";
break;
case 'G':
os << "guarantee";
break;
case 'S':
os << "safety";
break;
case 'O':
os << "obligation";
break;
case 'P':
os << "persistence";
break;
case 'R':
os << "recurrence";
break;
case 'T':
os << "reactivity";
break;
}
}
return os.str();
}
unsigned nesting_depth(formula f, op oper)
{
unsigned max_depth = 0;
for (formula child: f)
max_depth = std::max(max_depth, nesting_depth(child, oper));
return max_depth + f.is(oper);
}
unsigned nesting_depth(formula f, const op* begin, const op* end)
{
unsigned max_depth = 0;
for (formula child: f)
max_depth = std::max(max_depth, nesting_depth(child, begin, end));
bool matched = std::find(begin, end, f.kind()) != end;
return max_depth + matched;
}
unsigned nesting_depth(formula f, const char* opers)
{
bool want_nnf = false;
std::vector v;
for (;;)
switch (char c = *opers++)
{
case '~':
want_nnf = true;
break;
case '!':
v.push_back(op::Not);
break;
case '&':
v.push_back(op::And);
break;
case '|':
v.push_back(op::Or);
break;
case 'e':
v.push_back(op::Equiv);
break;
case 'F':
v.push_back(op::F);
break;
case 'G':
v.push_back(op::G);
break;
case 'i':
v.push_back(op::Implies);
break;
case 'M':
v.push_back(op::M);
break;
case 'R':
v.push_back(op::R);
break;
case 'U':
v.push_back(op::U);
break;
case 'W':
v.push_back(op::W);
break;
case 'X':
v.push_back(op::X);
break;
case '\0':
case ']':
goto break2;
default:
throw std::runtime_error
("nesting_depth(): unknown operator '"s + c + '\'');
}
break2:
if (want_nnf)
f = negative_normal_form(f);
const op* vd = v.data();
return nesting_depth(f, vd, vd + v.size());
}
bool is_liveness(formula f)
{
return is_liveness_automaton(ltl_to_tgba_fm(f, spot::make_bdd_dict()));
}
}