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

merge

Browse source
This commit is contained in:
Antoine Martin 2025-03-07 11:58:47 +01:00
commit 4ee8746b64
24 changed files with 3616 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

10
python/spot/impl.i
View file

@ -86,7 +86,10 @@
#include <spot/tl/apcollect.hh>
#include <spot/tl/contain.hh>
#include <spot/tl/derive.hh>
#include <spot/tl/dot.hh>
#include <spot/tl/expansions.hh>
#include <spot/tl/expansions2.hh>
#include <spot/tl/nenoform.hh>
#include <spot/tl/print.hh>
#include <spot/tl/simplify.hh>
@ -162,6 +165,7 @@
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/translate_aa.hh>
#include <spot/twaalgos/toweak.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/dtwasat.hh>
@ -544,6 +548,8 @@ namespace std {
%template(vectorofvectorofformulas) vector<vector<spot::formula>>;
%template(setunsigned) set<unsigned>;
%template(relabeling_map) map<spot::formula, spot::formula>;
%template(pair_formula) pair<spot::formula, spot::formula>;
%template(vector_pair_formula) vector<pair<spot::formula, spot::formula>>;
}
%include <spot/tl/environment.hh>
@ -631,6 +637,9 @@ namespace std {
%include <spot/tl/apcollect.hh>
%include <spot/tl/contain.hh>
%include <spot/tl/derive.hh>
%include <spot/tl/expansions.hh>
%include <spot/tl/expansions2.hh>
%include <spot/tl/dot.hh>
%include <spot/tl/nenoform.hh>
%include <spot/tl/sonf.hh>
@ -788,6 +797,7 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/stutter.hh>
%include <spot/twaalgos/synthesis.hh>
%include <spot/twaalgos/translate.hh>
%include <spot/twaalgos/translate_aa.hh>
%include <spot/twaalgos/toweak.hh>
%include <spot/twaalgos/hoa.hh>
%include <spot/twaalgos/dtwasat.hh>

8
spot/graph/graph.hh
View file

@ -557,10 +557,11 @@ namespace spot
{
std::map<std::vector<unsigned>, unsigned> uniq_;
G& g_;
unsigned acc_sink_;
public:
univ_dest_mapper(G& graph)
: g_(graph)
univ_dest_mapper(G& graph, unsigned sink = -1u)
: g_(graph), acc_sink_(sink)
{
}
@ -570,6 +571,9 @@ namespace spot
std::vector<unsigned> tmp(begin, end);
std::sort(tmp.begin(), tmp.end());
tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
if (acc_sink_ != -1u && tmp.size() > 1)
tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_),
tmp.end());
auto p = uniq_.emplace(tmp, 0);
if (p.second)
p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());

5
spot/tl/Makefile.am
View file

@ -28,9 +28,11 @@ tl_HEADERS = \
declenv.hh \
defaultenv.hh \
delta2.hh \
derive.hh \
dot.hh \
environment.hh \
exclusive.hh \
expansions2.hh \
formula.hh \
hierarchy.hh \
length.hh \
@ -54,8 +56,11 @@ libtl_la_SOURCES = \
declenv.cc \
defaultenv.cc \
delta2.cc \
derive.cc \
dot.cc \
exclusive.cc \
expansions.cc \
expansions2.cc \
formula.cc \
hierarchy.cc \
length.cc \

589
spot/tl/derive.cc Normal file
View file

@ -0,0 +1,589 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/priv/robin_hood.hh>
#include <spot/tl/derive.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/remprop.hh>
namespace spot
{
namespace
{
static std::pair<bdd, bdd>
first(formula f, const bdd_dict_ptr& d, void* owner)
{
if (f.is_boolean())
{
bdd res = formula_to_bdd(f, d, owner);
return { res, bdd_support(res) };
}
switch (f.kind())
{
// handled by is_boolean above
case op::ff:
case op::tt:
case op::ap:
case op::And:
case op::Or:
SPOT_UNREACHABLE();
case op::eword:
return { bddfalse, bddtrue };
case op::OrRat:
{
bdd res = bddfalse;
bdd support = bddtrue;
for (auto subformula : f)
{
auto [r, sup] = first(subformula, d, owner);
res |= r;
support &= sup;
}
return { res, support };
}
case op::AndRat:
{
bdd res = bddtrue;
bdd support = bddtrue;
for (auto subformula : f)
{
auto [r, sup] = first(subformula, d, owner);
res &= r;
support &= sup;
}
return { res, support };
}
case op::AndNLM:
return first(rewrite_and_nlm(f), d, owner);
case op::Concat:
{
auto [res, support] = first(f[0], d, owner);
if (f[0].accepts_eword())
{
auto [r, sup] = first(f.all_but(0), d, owner);
res |= r;
support &= sup;
}
return { res, support };
}
case op::Fusion:
{
auto [res, support] = first(f[0], d, owner);
// this should be computed only if f[0] recognizes words of size 1
// or accepts eword ?
auto p = first(f.all_but(0), d, owner);
return { res, support & p.second };
}
case op::Star:
case op::first_match:
return first(f[0], d, owner);
case op::FStar:
{
auto [res, support] = first(f[0], d, owner);
if (f.min() == 0)
res = bddtrue;
return { res, support };
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())
<< std::endl;
SPOT_UNIMPLEMENTED();
}
return { bddfalse, bddtrue };
}
static std::vector<std::string>
formula_aps(formula f)
{
auto res = std::unordered_set<std::string>();
f.traverse([&res](formula f)
{
if (f.is(op::ap))
{
res.insert(f.ap_name());
return true;
}
return false;
});
return std::vector(res.begin(), res.end());
}
}
formula
rewrite_and_nlm(formula f)
{
unsigned s = f.size();
std::vector<formula> final;
std::vector<formula> non_final;
for (auto g: f)
if (g.accepts_eword())
final.emplace_back(g);
else
non_final.emplace_back(g);
if (non_final.empty())
// (a* & b*);c = (a*|b*);c
return formula::OrRat(std::move(final));
if (!final.empty())
{
// let F_i be final formulae
// N_i be non final formula
// (F_1 & ... & F_n & N_1 & ... & N_m)
// = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
// | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
formula f = formula::OrRat(std::move(final));
formula n = formula::AndNLM(std::move(non_final));
formula t = formula::one_star();
formula ft = formula::Concat({f, t});
formula nt = formula::Concat({n, t});
formula ftn = formula::AndRat({ft, n});
formula fnt = formula::AndRat({f, nt});
return formula::OrRat({ftn, fnt});
}
// No final formula.
// Translate N_1 & N_2 & ... & N_n into
// N_1 && (N_2;[*]) && ... && (N_n;[*])
// | (N_1;[*]) && N_2 && ... && (N_n;[*])
// | (N_1;[*]) && (N_2;[*]) && ... && N_n
formula star = formula::one_star();
std::vector<formula> disj;
for (unsigned n = 0; n < s; ++n)
{
std::vector<formula> conj;
for (unsigned m = 0; m < s; ++m)
{
formula g = f[m];
if (n != m)
g = formula::Concat({g, star});
conj.emplace_back(g);
}
disj.emplace_back(formula::AndRat(std::move(conj)));
}
return formula::OrRat(std::move(disj));
}
twa_graph_ptr
derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic, derive_opts options)
{
auto aut = make_twa_graph(bdd_dict);
aut->prop_state_acc(true);
const auto acc_mark = aut->set_buchi();
auto formula2state = robin_hood::unordered_map<formula, unsigned>();
unsigned init_state = aut->new_state();
aut->set_init_state(init_state);
formula2state.insert({ f, init_state });
auto f_aps = formula_aps(f);
for (auto& ap : f_aps)
aut->register_ap(ap);
auto todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state});
auto state_names = new std::vector<std::string>();
std::ostringstream ss;
ss << f;
state_names->push_back(ss.str());
auto find_dst = [&](formula derivative) -> unsigned
{
unsigned dst;
auto it = formula2state.find(derivative);
if (it != formula2state.end())
{
dst = it->second;
}
else
{
dst = aut->new_state();
todo.push_back({derivative, dst});
formula2state.insert({derivative, dst});
std::ostringstream ss;
ss << derivative;
state_names->push_back(ss.str());
}
return dst;
};
while (!todo.empty())
{
auto [curr_f, curr_state] = todo[todo.size() - 1];
todo.pop_back();
auto curr_acc_mark = curr_f.accepts_eword()
? acc_mark
: acc_cond::mark_t();
auto [firsts, firsts_support] = first(curr_f, bdd_dict, aut.get());
for (const bdd one : minterms_of(firsts, firsts_support))
{
formula derivative =
partial_derivation(curr_f, one, bdd_dict, aut.get(), options);
// no transition possible from this letter
if (derivative.is(op::ff))
continue;
// either the formula isn't an OrRat, or if it is we consider it as
// as a whole to get a deterministic automaton
if (deterministic || !derivative.is(op::OrRat))
{
auto dst = find_dst(derivative);
aut->new_edge(curr_state, dst, one, curr_acc_mark);
continue;
}
// formula is an OrRat and we want a non deterministic automaton,
// so consider each child as a destination
for (const auto& subformula : derivative)
{
auto dst = find_dst(subformula);
aut->new_edge(curr_state, dst, one, curr_acc_mark);
}
}
// if state has no transitions and should be accepting, create
// artificial transition
if (aut->get_graph().state_storage(curr_state).succ == 0
&& curr_f.accepts_eword())
aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
}
aut->set_named_prop("state-names", state_names);
aut->merge_edges();
return aut;
}
twa_graph_ptr
derive_finite_automaton(formula f, bool deterministic)
{
auto bdd_dict = make_bdd_dict();
auto aut = make_twa_graph(bdd_dict);
aut->prop_state_acc(true);
const auto acc_mark = aut->set_buchi();
auto formula2state = robin_hood::unordered_map<formula, unsigned>();
unsigned init_state = aut->new_state();
aut->set_init_state(init_state);
formula2state.insert({ f, init_state });
auto f_aps = formula_aps(f);
for (auto& ap : f_aps)
aut->register_ap(ap);
bdd all_aps = aut->ap_vars();
auto todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state});
auto state_names = new std::vector<std::string>();
std::ostringstream ss;
ss << f;
state_names->push_back(ss.str());
auto find_dst = [&](formula derivative) -> unsigned
{
unsigned dst;
auto it = formula2state.find(derivative);
if (it != formula2state.end())
{
dst = it->second;
}
else
{
dst = aut->new_state();
todo.push_back({derivative, dst});
formula2state.insert({derivative, dst});
std::ostringstream ss;
ss << derivative;
state_names->push_back(ss.str());
}
return dst;
};
while (!todo.empty())
{
auto [curr_f, curr_state] = todo[todo.size() - 1];
todo.pop_back();
auto curr_acc_mark = curr_f.accepts_eword()
? acc_mark
: acc_cond::mark_t();
for (const bdd one : minterms_of(bddtrue, all_aps))
{
formula derivative =
partial_derivation(curr_f, one, bdd_dict, aut.get());
// no transition possible from this letter
if (derivative.is(op::ff))
continue;
// either the formula isn't an OrRat, or if it is we consider it as
// as a whole to get a deterministic automaton
if (deterministic || !derivative.is(op::OrRat))
{
auto dst = find_dst(derivative);
aut->new_edge(curr_state, dst, one, curr_acc_mark);
continue;
}
// formula is an OrRat and we want a non deterministic automaton,
// so consider each child as a destination
for (const auto& subformula : derivative)
{
auto dst = find_dst(subformula);
aut->new_edge(curr_state, dst, one, curr_acc_mark);
}
}
// if state has no transitions and should be accepting, create
// artificial transition
if (aut->get_graph().state_storage(curr_state).succ == 0
&& curr_f.accepts_eword())
aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
}
aut->set_named_prop("state-names", state_names);
aut->merge_edges();
return aut;
}
twa_graph_ptr
derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic)
{
auto finite = derive_finite_automaton_with_first(f, bdd_dict,
deterministic);
return from_finite(finite);
}
twa_graph_ptr
derive_automaton(formula f, bool deterministic)
{
auto finite = derive_finite_automaton(f, deterministic);
return from_finite(finite);
}
formula
partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
void* owner, derive_opts options)
{
if (f.is_boolean())
{
auto f_bdd = formula_to_bdd(f, d, owner);
if (bdd_implies(var, f_bdd))
return formula::eword();
return formula::ff();
}
switch (f.kind())
{
// handled by is_boolean above
case op::ff:
case op::tt:
case op::ap:
SPOT_UNREACHABLE();
case op::eword:
return formula::ff();
// d(E.F) = { d(E).F } U { c(E).d(F) }
case op::Concat:
{
formula E = f[0];
formula F = f.all_but(0);
formula d_E = partial_derivation(E, var, d, owner, options);
formula res;
if (options.concat_star_distribute && d_E.is(op::OrRat))
{
std::vector<formula> distributed;
for (auto g : d_E)
{
distributed.push_back(formula::Concat({g, F}));
}
res = formula::OrRat(distributed);
}
else
{
res =
formula::Concat({ partial_derivation(E, var, d, owner, options), F });
}
if (E.accepts_eword())
res = formula::OrRat(
{ res, partial_derivation(F, var, d, owner, options) });
return res;
}
// d(E*) = d(E).E*
// d(E[*i..j]) = d(E).E[*(i-1)..(j-1)]
case op::Star:
{
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
formula d_E = partial_derivation(f[0], var, d, owner, options);
if (options.concat_star_distribute && !f[0].is_finite() && d_E.is(op::OrRat))
{
std::vector<formula> distributed;
for (auto g : d_E)
{
distributed.push_back(formula::Concat({g, formula::Star(f[0], min, max)}));
}
return formula::OrRat(distributed);
}
return formula::Concat({ d_E, formula::Star(f[0], min, max) });
}
// d(E[:*i..j]) = E:E[:*(i-1)..(j-1)] + (eword if i == 0 or c(d(E)))
case op::FStar:
{
formula E = f[0];
if (f.min() == 0 && f.max() == 0)
return formula::tt();
auto d_E = partial_derivation(E, var, d, owner, options);
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
auto results = std::vector<formula>();
auto E_i_j_minus = formula::FStar(E, min, max);
results.push_back(formula::Fusion({ d_E, E_i_j_minus }));
if (d_E.accepts_eword())
results.push_back(d_E);
if (f.min() == 0)
results.push_back(formula::eword());
return formula::OrRat(std::move(results));
}
// d(E && F) = d(E) && d(F)
// d(E + F) = {d(E)} U {d(F)}
case op::AndRat:
case op::OrRat:
{
std::vector<formula> subderivations;
for (auto subformula : f)
{
auto subderivation =
partial_derivation(subformula, var, d, owner, options);
subderivations.push_back(subderivation);
}
return formula::multop(f.kind(), std::move(subderivations));
}
case op::AndNLM:
{
formula rewrite = rewrite_and_nlm(f);
return partial_derivation(rewrite, var, d, owner, options);
}
// d(E:F) = {d(E):F} U {c(d(E)).d(F)}
case op::Fusion:
{
formula E = f[0];
formula F = f.all_but(0);
auto d_E = partial_derivation(E, var, d, owner, options);
auto res = formula::Fusion({ d_E, F });
if (d_E.accepts_eword())
res =
formula::OrRat({ res, partial_derivation(F, var, d, owner, options) });
return res;
}
case op::first_match:
{
formula E = f[0];
auto d_E = partial_derivation(E, var, d, owner, options);
// if d_E.accepts_eword(), first_match(d_E) will return eword
return formula::first_match(d_E);
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())
<< std::endl;
SPOT_UNIMPLEMENTED();
}
return formula::ff();
}
}

60
spot/tl/derive.hh Normal file
View file

@ -0,0 +1,60 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <vector>
#include <bddx.h>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/twagraph.hh>
namespace spot
{
struct derive_opts
{
bool concat_star_distribute = true;
};
/// \ingroup tl_misc
/// \brief Produce a SERE formula's partial derivative
SPOT_API formula
partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
void* owner, derive_opts options = {});
SPOT_API twa_graph_ptr
derive_automaton(formula f, bool deterministic = true);
SPOT_API twa_graph_ptr
derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic = true);
SPOT_API twa_graph_ptr
derive_finite_automaton(formula f, bool deterministic = true);
SPOT_API twa_graph_ptr
derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
bool deterministic = true, derive_opts options = {});
SPOT_API formula
rewrite_and_nlm(formula f);
}

966
spot/tl/expansions.cc Normal file
View file

@ -0,0 +1,966 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <algorithm>
#include <spot/misc/minato.hh>
#include <spot/priv/robin_hood.hh>
#include <spot/tl/expansions.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/remprop.hh>
namespace spot
{
namespace
{
// FIXME: could probably just return a map directly
static std::vector<std::string>
formula_aps(formula f)
{
auto res = std::unordered_set<std::string>();
f.traverse([&res](formula f)
{
if (f.is(op::ap))
{
res.insert(f.ap_name());
return true;
}
return false;
});
return std::vector(res.begin(), res.end());
}
formula
rewrite_and_nlm(formula f)
{
unsigned s = f.size();
std::vector<formula> final;
std::vector<formula> non_final;
for (auto g: f)
if (g.accepts_eword())
final.emplace_back(g);
else
non_final.emplace_back(g);
if (non_final.empty())
// (a* & b*);c = (a*|b*);c
return formula::OrRat(std::move(final));
if (!final.empty())
{
// let F_i be final formulae
// N_i be non final formula
// (F_1 & ... & F_n & N_1 & ... & N_m)
// = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
// | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
formula f = formula::OrRat(std::move(final));
formula n = formula::AndNLM(std::move(non_final));
formula t = formula::one_star();
formula ft = formula::Concat({f, t});
formula nt = formula::Concat({n, t});
formula ftn = formula::AndRat({ft, n});
formula fnt = formula::AndRat({f, nt});
return formula::OrRat({ftn, fnt});
}
// No final formula.
// Translate N_1 & N_2 & ... & N_n into
// N_1 && (N_2;[*]) && ... && (N_n;[*])
// | (N_1;[*]) && N_2 && ... && (N_n;[*])
// | (N_1;[*]) && (N_2;[*]) && ... && N_n
formula star = formula::one_star();
std::vector<formula> disj;
for (unsigned n = 0; n < s; ++n)
{
std::vector<formula> conj;
for (unsigned m = 0; m < s; ++m)
{
formula g = f[m];
if (n != m)
g = formula::Concat({g, star});
conj.emplace_back(g);
}
disj.emplace_back(formula::AndRat(std::move(conj)));
}
return formula::OrRat(std::move(disj));
}
class bdd_finalizer
{
public:
int encode(formula f)
{
bool is_anon = false;
int var_num;
auto it = formula2bdd_.find(f);
if (it != formula2bdd_.end())
{
var_num = it->second;
}
else
{
if (opt_sigma_star_ && (f.is(op::Star)
&& f[0].is(op::tt)
&& f.min() == 0
&& f.max() == formula::unbounded()))
{
var_num = bddtrue.id();
}
else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat)))
{
bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse);
for (const auto& sub_f : f)
{
int bddid = encode(sub_f);
bdd subvar = bdd_ithvar(bddid);
var = f.is(op::AndRat) ? var & subvar : var | subvar;
}
var_num = var.id();
}
else
{
var_num = d_->register_anonymous_variables(1, this);
is_anon = true;
}
formula2bdd_.insert({f, var_num});
bdd2formula_.insert({var_num, f});
}
bdd var = bdd_ithvar(var_num);
if (is_anon)
anon_set_ &= var;
return var_num;
}
bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode)
: anon_set_(bddtrue)
, d_(d)
, opt_sigma_star_(opt_sigma_star)
, opt_bdd_encode_(opt_bdd_encode)
{
for (const auto& [prefix, suffix] : exp)
{
int var_num = encode(suffix);
bdd var = bdd_ithvar(var_num);
exp_ |= prefix & var;
}
}
~bdd_finalizer()
{
d_->unregister_all_my_variables(this);
}
expansion_t
simplify(exp_opts::expand_opt opts);
private:
bdd exp_;
bdd anon_set_;
std::map<formula, int> formula2bdd_;
std::map<int, formula> bdd2formula_;
bdd_dict_ptr d_;
bool opt_sigma_star_;
bool opt_bdd_encode_;
formula var_to_formula(int var);
formula conj_bdd_to_sere(bdd b);
formula bdd_to_sere(bdd b);
};
formula
bdd_finalizer::var_to_formula(int var)
{
formula f = bdd2formula_[var];
assert(f);
return f;
}
formula
bdd_finalizer::bdd_to_sere(bdd f)
{
if (f == bddfalse)
return formula::ff();
std::vector<formula> v;
minato_isop isop(f);
bdd cube;
while ((cube = isop.next()) != bddfalse)
v.emplace_back(conj_bdd_to_sere(cube));
return formula::OrRat(std::move(v));
}
formula
bdd_finalizer::conj_bdd_to_sere(bdd b)
{
if (b == bddtrue)
{
if (opt_sigma_star_){
return formula::Star(formula::tt(), 0, formula::unbounded());
} else {
return formula::tt();
}
}
if (b == bddfalse)
return formula::ff();
// Unroll the first loop of the next do/while loop so that we
// do not have to create v when b is not a conjunction.
formula res = var_to_formula(bdd_var(b));
bdd high = bdd_high(b);
if (high == bddfalse)
{
res = formula::Not(res);
b = bdd_low(b);
}
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
if (b == bddtrue)
return res;
std::vector<formula> v{std::move(res)};
do
{
res = var_to_formula(bdd_var(b));
high = bdd_high(b);
if (high == bddfalse)
{
res = formula::Not(res);
b = bdd_low(b);
}
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
assert(b != bddfalse);
v.emplace_back(std::move(res));
}
while (b != bddtrue);
return formula::multop(op::AndRat, std::move(v));
}
expansion_t
bdd_finalizer::simplify(exp_opts::expand_opt opts)
{
expansion_t res;
if (opts & exp_opts::expand_opt::BddMinterm)
{
bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
bdd or_labels = bdd_exist(exp_, anon_set_);
// TODO: check are_equivalent avec or_labels/exp_ en premier argument
for (bdd letter: minterms_of(or_labels, prop_set))
{
bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = bdd_to_sere(dest_bdd);
// #ifndef NDEBUG
// // make sure it didn't exist before
// auto it = std::find(res.begin(), res.end(), {letter, dest});
// SPOT_ASSERT(it == res.end());
// #endif
res.push_back({letter, dest});
}
}
else // BddIsop
{
minato_isop isop(exp_);
bdd cube;
while ((cube = isop.next()) != bddfalse)
{
bdd letter = bdd_exist(cube, anon_set_);
bdd suffix = bdd_existcomp(cube, anon_set_);
formula dest = conj_bdd_to_sere(suffix);
res.push_back({letter, dest});
}
}
return res;
}
expansion_t
unique_prefix(const expansion_t& exp)
{
std::map<bdd, formula, bdd_less_than> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({prefix, suffix});
if (!res.second)
{
auto it = res.first;
it->second = formula::OrRat({it->second, suffix});
}
}
expansion_t res(unique_map.begin(), unique_map.end());
return res;
}
expansion_t
unique_prefix_seen(const expansion_t& exp, std::unordered_set<formula>* seen)
{
std::map<bdd, formula, bdd_less_than> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({prefix, suffix});
if (!res.second)
{
auto it = res.first;
it->second = formula::OrRat({it->second, suffix});
}
}
expansion_t res;
for (const auto& [prefix, suffix] : unique_map)
{
if (!suffix.is(op::OrRat))
{
res.push_back({prefix, suffix});
continue;
}
std::vector<formula> merge;
std::vector<formula> single;
for (const auto& sub_f : suffix)
{
if (seen->find(sub_f) != seen->end())
{
single.push_back(sub_f);
}
else
{
merge.push_back(sub_f);
}
}
for (const auto& sub_f : single)
res.push_back({prefix, sub_f});
if (!merge.empty())
res.push_back({prefix, formula::OrRat(merge)});
}
return res;
}
size_t count_new(const expansion_t& exp, std::unordered_set<formula>* seen)
{
size_t count = 0;
for (const auto& [_, suffix] : exp)
{
if (seen->find(suffix) == seen->end())
count++;
}
return count;
}
const expansion_t&
find_smallest(const expansion_t& left,
const expansion_t& right,
std::unordered_set<formula>* seen)
{
size_t left_new = count_new(left, seen);
size_t right_new = count_new(right, seen);
if (left_new < right_new)
return left;
if (left_new == right_new && left.size() > right.size())
return right;
return right;
}
expansion_t
unique_prefix_count(const expansion_t& exp, std::unordered_set<formula>* seen)
{
expansion_t up = unique_prefix(exp);
expansion_t up_seen = unique_prefix_seen(exp, seen);
const expansion_t& maybe_smallest = find_smallest(exp, up, seen);
const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen);
return smallest;
}
void
finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set<formula>* seen)
{
if (opts & (exp_opts::expand_opt::BddIsop
| exp_opts::expand_opt::BddMinterm))
{
bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode);
exp = bddf.simplify(opts);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPre)
{
std::map<formula, bdd> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({suffix, prefix});
if (!res.second)
{
auto it = res.first;
it->second |= prefix;
}
}
exp.clear();
for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
}
if (opts & exp_opts::expand_opt::UniquePrefix
|| opts & exp_opts::expand_opt::UniquePrefixSeenOpt
|| opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
{
if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
exp = unique_prefix_seen(exp, seen);
else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
exp = unique_prefix_count(exp, seen);
else
exp = unique_prefix(exp);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPost)
{
std::map<formula, bdd> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({suffix, prefix});
if (!res.second)
{
auto it = res.first;
it->second |= prefix;
}
}
exp.clear();
for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
}
if (opts & exp_opts::expand_opt::Determinize)
{
expansion_t exp_new;
bdd props = bddtrue;
for (const auto& [prefix, _] : exp)
props &= bdd_support(prefix);
std::vector<formula> dests;
for (bdd letter : minterms_of(bddtrue, props))
{
for (const auto& [prefix, suffix] : exp)
{
if (bdd_implies(letter, prefix))
dests.push_back(suffix);
}
formula or_dests = formula::OrRat(dests);
exp_new.push_back({letter, or_dests});
dests.clear();
}
exp = exp_new;
}
// sort and remove duplicates from expansion to canonicalize it for
// eventual signature use
if (exp.size() >= 2)
{
std::sort(exp.begin(), exp.end(),
[](const auto& lhs, const auto& rhs) {
return std::make_pair(lhs.first.id(), lhs.second.id())
< std::make_pair(rhs.first.id(), rhs.second.id());
});
exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
}
}
}
formula
expansion_to_formula(expansion_t e, bdd_dict_ptr& d)
{
std::vector<formula> res;
for (const auto& [key, val] : e)
{
formula prefix = bdd_to_formula(key, d);
res.push_back(formula::Concat({prefix, val}));
}
return formula::OrRat(res);
}
void print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict)
{
for (const auto& [prefix, suffix] : exp)
{
std::cout << bdd_to_formula(prefix, dict) << ": " << suffix << std::endl;
}
}
std::vector<std::pair<formula, formula>>
expansion_simple(formula f)
{
int owner = 42;
auto d = make_bdd_dict();
auto exp = expansion(f, d, &owner, exp_opts::None);
std::vector<std::pair<formula, formula>> res;
for (const auto& [bdd, f] : exp)
res.push_back({bdd_to_formula(bdd, d), f});
d->unregister_all_my_variables(&owner);
return res;
}
expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen)
{
using exp_t = expansion_t;
if (f.is_boolean())
{
auto f_bdd = formula_to_bdd(f, d, owner);
if (f_bdd == bddfalse)
return {};
return {{f_bdd, formula::eword()}};
}
auto rec = [&d, owner, seen](formula f){
return expansion(f, d, owner, exp_opts::None, seen);
};
switch (f.kind())
{
case op::ff:
case op::tt:
case op::ap:
SPOT_UNREACHABLE();
case op::eword:
// return {{bddfalse, formula::ff()}};
return {};
case op::Concat:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})});
}
if (f[0].accepts_eword())
{
auto exps_rest = rec(f.all_but(0));
for (const auto& [bdd_l, form] : exps_rest)
{
res.push_back({bdd_l, form});
}
}
finalize(res, opts, d, seen);
return res;
}
case op::FStar:
{
formula E = f[0];
if (f.min() == 0 && f.max() == 0)
return {{bddtrue, formula::eword()}};
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
auto E_i_j_minus = formula::FStar(E, min, max);
auto exp = rec(E);
exp_t res;
for (const auto& [li, ei] : exp)
{
res.push_back({li, formula::Fusion({ei, E_i_j_minus})});
if (ei.accepts_eword() && f.min() != 0)
{
for (const auto& [ki, fi] : rec(E_i_j_minus))
{
// FIXME: build bdd once
if ((li & ki) != bddfalse)
res.push_back({li & ki, fi});
}
}
}
if (f.min() == 0)
res.push_back({bddtrue, formula::eword()});
finalize(res, opts, d, seen);
return res;
}
case op::Star:
{
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
}
finalize(res, opts, d, seen);
return res;
}
case op::AndNLM:
{
formula rewrite = rewrite_and_nlm(f);
auto res = rec(rewrite);
finalize(res, opts, d, seen);
return res;
}
case op::first_match:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, form});
}
// determinize
bdd or_labels = bddfalse;
bdd support = bddtrue;
bool is_det = true;
for (const auto& [l, _] : res)
{
support &= bdd_support(l);
if (is_det)
is_det = !bdd_have_common_assignment(l, or_labels);
or_labels |= l;
}
if (is_det)
{
for (auto& [_, dest] : res)
dest = formula::first_match(dest);
finalize(res, opts, d, seen);
return res;
}
exp_t res_det;
std::vector<formula> dests;
for (bdd l: minterms_of(or_labels, support))
{
for (const auto& [ndet_label, ndet_dest] : res)
{
if (bdd_implies(l, ndet_label))
dests.push_back(ndet_dest);
}
formula or_dests = formula::OrRat(dests);
res_det.push_back({l, or_dests});
dests.clear();
}
for (auto& [_, dest] : res_det)
dest = formula::first_match(dest);
finalize(res_det, opts, d, seen);
return res_det;
}
case op::Fusion:
{
exp_t res;
formula E = f[0];
formula F = f.all_but(0);
exp_t Ei = rec(E);
// TODO: std::option
exp_t Fj = rec(F);
for (const auto& [li, ei] : Ei)
{
if (ei.accepts_eword())
{
for (const auto& [kj, fj] : Fj)
if ((li & kj) != bddfalse)
res.push_back({li & kj, fj});
}
formula ei_fusion_F = formula::Fusion({ei, F});
if (!ei_fusion_F.is(op::ff))
res.push_back({li, ei_fusion_F});
}
finalize(res, opts, d, seen);
return res;
}
case op::AndRat:
{
exp_t res;
for (const auto& sub_f : f)
{
auto exps = rec(sub_f);
if (exps.empty())
{
// op::AndRat: one of the expansions was empty (the only
// edge was `false`), so the AndRat is empty as
// well
res.clear();
break;
}
if (res.empty())
{
res = std::move(exps);
continue;
}
exp_t new_res;
bool inserted = false;
for (const auto& [l_key, l_val] : exps)
{
for (const auto& [r_key, r_val] : res)
{
if ((l_key & r_key) != bddfalse)
{
new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
inserted = true;
}
}
}
if (!inserted)
{
// all prefix conjuctions led to bddfalse, And is empty
res.clear();
break;
}
res = std::move(new_res);
}
finalize(res, opts, d, seen);
return res;
}
case op::OrRat:
{
exp_t res;
for (const auto& sub_f : f)
{
auto exps = rec(sub_f);
if (exps.empty())
continue;
if (res.empty())
{
res = std::move(exps);
continue;
}
for (const auto& [label, dest] : exps)
res.push_back({label, dest});
}
finalize(res, opts, d, seen);
return res;
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())
<< std::endl;
SPOT_UNIMPLEMENTED();
}
return {};
}
twa_graph_ptr
expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
{
auto finite = expand_finite_automaton(f, d, opts);
return from_finite(finite);
}
struct signature_hash
{
std::size_t
operator() (const std::pair<bool, expansion_t>& sig) const noexcept
{
size_t hash = std::hash<bool>()(sig.first);
for (const auto& keyvalue : sig.second)
{
hash ^= (bdd_hash()(keyvalue.first) ^ std::hash<formula>()(keyvalue.second))
+ 0x9e3779b9 + (hash << 6) + (hash >> 2);
}
return hash;
}
};
twa_graph_ptr
expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
{
bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge;
auto aut = make_twa_graph(d);
aut->prop_state_acc(true);
const auto acc_mark = aut->set_buchi();
auto formula2state = robin_hood::unordered_map<formula, unsigned>();
auto signature2state = std::unordered_map<std::pair<bool, expansion_t>, unsigned, signature_hash>();
auto seen = std::unordered_set<formula>();
seen.insert(f);
unsigned init_state = aut->new_state();
aut->set_init_state(init_state);
formula2state.insert({ f, init_state });
auto f_aps = formula_aps(f);
for (auto& ap : f_aps)
aut->register_ap(ap);
if (signature_merge)
signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts, &seen)}, init_state});
auto todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state});
auto state_names = new std::vector<std::string>();
std::ostringstream ss;
ss << f;
state_names->push_back(ss.str());
auto find_dst = [&](formula suffix) -> unsigned
{
unsigned dst;
auto it = formula2state.find(suffix);
if (it != formula2state.end())
{
dst = it->second;
}
else
{
if (signature_merge)
{
auto exp = expansion(suffix, d, aut.get(), opts, &seen);
bool accepting = suffix.accepts_eword();
auto it2 = signature2state.find({accepting, exp});
if (it2 != signature2state.end())
{
formula2state.insert({suffix, it2->second});
return it2->second;
}
}
dst = aut->new_state();
todo.push_back({suffix, dst});
seen.insert(suffix);
formula2state.insert({suffix, dst});
if (signature_merge)
signature2state.insert({{suffix.accepts_eword(), expansion(suffix, d, aut.get(), opts, &seen)}, dst});
std::ostringstream ss;
ss << suffix;
state_names->push_back(ss.str());
}
return dst;
};
while (!todo.empty())
{
auto [curr_f, curr_state] = todo[todo.size() - 1];
todo.pop_back();
auto curr_acc_mark= curr_f.accepts_eword()
? acc_mark
: acc_cond::mark_t();
auto exp = expansion(curr_f, d, aut.get(), opts, &seen);
for (const auto& [letter, suffix] : exp)
{
if (suffix.is(op::ff))
// TODO ASSERT NOT
continue;
auto dst = find_dst(suffix);
aut->new_edge(curr_state, dst, letter, curr_acc_mark);
}
// if state has no transitions and should be accepting, create
// artificial transition
if (aut->get_graph().state_storage(curr_state).succ == 0
&& curr_f.accepts_eword())
aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
}
aut->set_named_prop("state-names", state_names);
if ((opts & exp_opts::MergeEdges)
&& !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost))
aut->merge_edges();
return aut;
}
}

72
spot/tl/expansions.hh Normal file
View file

@ -0,0 +1,72 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <map>
#include <bddx.h>
#include <spot/misc/bddlt.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/twagraph.hh>
namespace spot
{
using expansion_t = std::vector<std::pair<bdd, formula>>;
struct exp_opts
{
enum expand_opt {
None = 0,
UniqueSuffixPre = 1,
UniquePrefix = 2,
BddIsop = 4,
BddMinterm = 8,
BddSigmaStar = 16,
BddEncode = 32,
MergeEdges = 64,
SignatureMerge = 128,
Determinize = 256,
UniquePrefixSeenOpt = 512,
UniqueSuffixPost = 1024,
UniquePrefixSeenCountOpt = 2048,
TransitionBased = 4096,
};
};
SPOT_API std::vector<std::pair<formula, formula>>
expansion_simple(formula f);
SPOT_API expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen = nullptr);
SPOT_API twa_graph_ptr
expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
SPOT_API twa_graph_ptr
expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
SPOT_API formula
expansion_to_formula(expansion_t e, bdd_dict_ptr& d);
SPOT_API void
print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict);
}

946
spot/tl/expansions2.cc Normal file
View file

@ -0,0 +1,946 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <algorithm>
#include <spot/misc/minato.hh>
#include <spot/priv/robin_hood.hh>
#include <spot/tl/expansions2.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/remprop.hh>
namespace spot
{
namespace
{
// FIXME: could probably just return a map directly
static std::vector<std::string>
formula_aps(formula f)
{
auto res = std::unordered_set<std::string>();
f.traverse([&res](formula f)
{
if (f.is(op::ap))
{
res.insert(f.ap_name());
return true;
}
return false;
});
return std::vector(res.begin(), res.end());
}
formula
rewrite_and_nlm(formula f)
{
unsigned s = f.size();
std::vector<formula> final;
std::vector<formula> non_final;
for (auto g: f)
if (g.accepts_eword())
final.emplace_back(g);
else
non_final.emplace_back(g);
if (non_final.empty())
// (a* & b*);c = (a*|b*);c
return formula::OrRat(std::move(final));
if (!final.empty())
{
// let F_i be final formulae
// N_i be non final formula
// (F_1 & ... & F_n & N_1 & ... & N_m)
// = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
// | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
formula f = formula::OrRat(std::move(final));
formula n = formula::AndNLM(std::move(non_final));
formula t = formula::one_star();
formula ft = formula::Concat({f, t});
formula nt = formula::Concat({n, t});
formula ftn = formula::AndRat({ft, n});
formula fnt = formula::AndRat({f, nt});
return formula::OrRat({ftn, fnt});
}
// No final formula.
// Translate N_1 & N_2 & ... & N_n into
// N_1 && (N_2;[*]) && ... && (N_n;[*])
// | (N_1;[*]) && N_2 && ... && (N_n;[*])
// | (N_1;[*]) && (N_2;[*]) && ... && N_n
formula star = formula::one_star();
std::vector<formula> disj;
for (unsigned n = 0; n < s; ++n)
{
std::vector<formula> conj;
for (unsigned m = 0; m < s; ++m)
{
formula g = f[m];
if (n != m)
g = formula::Concat({g, star});
conj.emplace_back(g);
}
disj.emplace_back(formula::AndRat(std::move(conj)));
}
return formula::OrRat(std::move(disj));
}
class bdd_finalizer
{
public:
int encode(formula f)
{
bool is_anon = false;
int var_num;
auto it = formula2bdd_.find(f);
if (it != formula2bdd_.end())
{
var_num = it->second;
}
else
{
if (opt_sigma_star_ && (f.is(op::Star)
&& f[0].is(op::tt)
&& f.min() == 0
&& f.max() == formula::unbounded()))
{
var_num = bddtrue.id();
}
else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat)))
{
bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse);
for (const auto& sub_f : f)
{
int bddid = encode(sub_f);
bdd subvar = bdd_ithvar(bddid);
var = f.is(op::AndRat) ? var & subvar : var | subvar;
}
var_num = var.id();
}
else
{
var_num = d_->register_anonymous_variables(1, this);
is_anon = true;
}
formula2bdd_.insert({f, var_num});
bdd2formula_.insert({var_num, f});
}
bdd var = bdd_ithvar(var_num);
if (is_anon)
anon_set_ &= var;
return var_num;
}
bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode)
: anon_set_(bddtrue)
, d_(d)
, opt_sigma_star_(opt_sigma_star)
, opt_bdd_encode_(opt_bdd_encode)
{
for (const auto& [prefix, suffix] : exp)
{
int var_num = encode(suffix);
bdd var = bdd_ithvar(var_num);
exp_ |= prefix & var;
}
}
~bdd_finalizer()
{
d_->unregister_all_my_variables(this);
}
expansion_t
simplify(exp_opts::expand_opt opts);
private:
bdd exp_;
bdd anon_set_;
std::map<formula, int> formula2bdd_;
std::map<int, formula> bdd2formula_;
bdd_dict_ptr d_;
bool opt_sigma_star_;
bool opt_bdd_encode_;
formula var_to_formula(int var);
formula conj_bdd_to_sere(bdd b);
formula bdd_to_sere(bdd b);
};
formula
bdd_finalizer::var_to_formula(int var)
{
formula f = bdd2formula_[var];
assert(f);
return f;
}
formula
bdd_finalizer::bdd_to_sere(bdd f)
{
if (f == bddfalse)
return formula::ff();
std::vector<formula> v;
minato_isop isop(f);
bdd cube;
while ((cube = isop.next()) != bddfalse)
v.emplace_back(conj_bdd_to_sere(cube));
return formula::OrRat(std::move(v));
}
formula
bdd_finalizer::conj_bdd_to_sere(bdd b)
{
if (b == bddtrue)
{
if (opt_sigma_star_){
return formula::Star(formula::tt(), 0, formula::unbounded());
} else {
return formula::tt();
}
}
if (b == bddfalse)
return formula::ff();
// Unroll the first loop of the next do/while loop so that we
// do not have to create v when b is not a conjunction.
formula res = var_to_formula(bdd_var(b));
bdd high = bdd_high(b);
if (high == bddfalse)
{
res = formula::Not(res);
b = bdd_low(b);
}
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
if (b == bddtrue)
return res;
std::vector<formula> v{std::move(res)};
do
{
res = var_to_formula(bdd_var(b));
high = bdd_high(b);
if (high == bddfalse)
{
res = formula::Not(res);
b = bdd_low(b);
}
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
assert(b != bddfalse);
v.emplace_back(std::move(res));
}
while (b != bddtrue);
return formula::multop(op::AndRat, std::move(v));
}
expansion_t
bdd_finalizer::simplify(exp_opts::expand_opt opts)
{
expansion_t res;
if (opts & exp_opts::expand_opt::BddMinterm)
{
bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
bdd or_labels = bdd_exist(exp_, anon_set_);
// TODO: check are_equivalent avec or_labels/exp_ en premier argument
for (bdd letter: minterms_of(or_labels, prop_set))
{
bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = bdd_to_sere(dest_bdd);
// #ifndef NDEBUG
// // make sure it didn't exist before
// auto it = std::find(res.begin(), res.end(), {letter, dest});
// SPOT_ASSERT(it == res.end());
// #endif
res.push_back({letter, dest});
}
}
else // BddIsop
{
minato_isop isop(exp_);
bdd cube;
while ((cube = isop.next()) != bddfalse)
{
bdd letter = bdd_exist(cube, anon_set_);
bdd suffix = bdd_existcomp(cube, anon_set_);
formula dest = conj_bdd_to_sere(suffix);
res.push_back({letter, dest});
}
}
return res;
}
expansion_t
unique_prefix(const expansion_t& exp)
{
std::map<bdd, formula, bdd_less_than> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({prefix, suffix});
if (!res.second)
{
auto it = res.first;
it->second = formula::OrRat({it->second, suffix});
}
}
expansion_t res(unique_map.begin(), unique_map.end());
return res;
}
expansion_t
unique_prefix_seen(const expansion_t& exp, std::unordered_set<formula>* seen)
{
std::map<bdd, formula, bdd_less_than> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({prefix, suffix});
if (!res.second)
{
auto it = res.first;
it->second = formula::OrRat({it->second, suffix});
}
}
expansion_t res;
for (const auto& [prefix, suffix] : unique_map)
{
if (!suffix.is(op::OrRat))
{
res.push_back({prefix, suffix});
continue;
}
std::vector<formula> merge;
std::vector<formula> single;
for (const auto& sub_f : suffix)
{
if (seen->find(sub_f) != seen->end())
{
single.push_back(sub_f);
}
else
{
merge.push_back(sub_f);
}
}
for (const auto& sub_f : single)
res.push_back({prefix, sub_f});
if (!merge.empty())
res.push_back({prefix, formula::OrRat(merge)});
}
return res;
}
size_t count_new(const expansion_t& exp, std::unordered_set<formula>* seen)
{
size_t count = 0;
for (const auto& [_, suffix] : exp)
{
if (seen->find(suffix) == seen->end())
count++;
}
return count;
}
const expansion_t&
find_smallest(const expansion_t& left,
const expansion_t& right,
std::unordered_set<formula>* seen)
{
size_t left_new = count_new(left, seen);
size_t right_new = count_new(right, seen);
if (left_new < right_new)
return left;
if (left_new == right_new && left.size() > right.size())
return right;
return right;
}
expansion_t
unique_prefix_count(const expansion_t& exp, std::unordered_set<formula>* seen)
{
expansion_t up = unique_prefix(exp);
expansion_t up_seen = unique_prefix_seen(exp, seen);
const expansion_t& maybe_smallest = find_smallest(exp, up, seen);
const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen);
return smallest;
}
void
finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set<formula>* seen)
{
if (opts & (exp_opts::expand_opt::BddIsop
| exp_opts::expand_opt::BddMinterm))
{
bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode);
exp = bddf.simplify(opts);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPre)
{
std::map<formula, bdd> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({suffix, prefix});
if (!res.second)
{
auto it = res.first;
it->second |= prefix;
}
}
exp.clear();
for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
}
if (opts & exp_opts::expand_opt::UniquePrefix
|| opts & exp_opts::expand_opt::UniquePrefixSeenOpt
|| opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
{
if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
exp = unique_prefix_seen(exp, seen);
else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
exp = unique_prefix_count(exp, seen);
else
exp = unique_prefix(exp);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPost)
{
std::map<formula, bdd> unique_map;
for (const auto& [prefix, suffix] : exp)
{
auto res = unique_map.insert({suffix, prefix});
if (!res.second)
{
auto it = res.first;
it->second |= prefix;
}
}
exp.clear();
for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
}
if (opts & exp_opts::expand_opt::Determinize)
{
expansion_t exp_new;
bdd props = bddtrue;
for (const auto& [prefix, _] : exp)
props &= bdd_support(prefix);
std::vector<formula> dests;
for (bdd letter : minterms_of(bddtrue, props))
{
for (const auto& [prefix, suffix] : exp)
{
if (bdd_implies(letter, prefix))
dests.push_back(suffix);
}
formula or_dests = formula::OrRat(dests);
exp_new.push_back({letter, or_dests});
dests.clear();
}
exp = exp_new;
}
// sort expansion to canonicalize it for eventual signature use
if (exp.size() >= 2)
{
std::sort(exp.begin(), exp.end(),
[](const auto& lhs, const auto& rhs) {
return std::make_pair(lhs.first.id(), lhs.second.id())
< std::make_pair(rhs.first.id(), rhs.second.id());
});
exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
}
}
}
formula
expansion_to_formula2(expansion_t e, bdd_dict_ptr& d)
{
std::vector<formula> res;
for (const auto& [key, val] : e)
{
formula prefix = bdd_to_formula(key, d);
res.push_back(formula::Concat({prefix, val}));
}
return formula::OrRat(res);
}
expansion_t
expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen)
{
using exp_t = expansion_t;
if (f.is_boolean())
{
auto f_bdd = formula_to_bdd(f, d, owner);
if (f_bdd == bddfalse)
return {};
return {{f_bdd, formula::eword()}};
}
auto rec = [&d, owner, seen](formula f){
return expansion2(f, d, owner, exp_opts::None, seen);
};
switch (f.kind())
{
case op::ff:
case op::tt:
case op::ap:
SPOT_UNREACHABLE();
case op::eword:
// return {{bddfalse, formula::ff()}};
return {};
case op::Concat:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})});
}
if (f[0].accepts_eword())
{
auto exps_rest = rec(f.all_but(0));
for (const auto& [bdd_l, form] : exps_rest)
{
res.push_back({bdd_l, form});
}
}
finalize(res, opts, d, seen);
return res;
}
case op::FStar:
{
formula E = f[0];
if (f.min() == 0 && f.max() == 0)
return {{bddtrue, formula::eword()}};
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
auto E_i_j_minus = formula::FStar(E, min, max);
auto exp = rec(E);
exp_t res;
for (const auto& [li, ei] : exp)
{
res.push_back({li, formula::Fusion({ei, E_i_j_minus})});
if (ei.accepts_eword() && f.min() != 0)
{
for (const auto& [ki, fi] : rec(E_i_j_minus))
{
// FIXME: build bdd once
if ((li & ki) != bddfalse)
res.push_back({li & ki, fi});
}
}
}
if (f.min() == 0)
res.push_back({bddtrue, formula::eword()});
finalize(res, opts, d, seen);
return res;
}
case op::Star:
{
auto min = f.min() == 0 ? 0 : (f.min() - 1);
auto max = f.max() == formula::unbounded()
? formula::unbounded()
: (f.max() - 1);
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
}
finalize(res, opts, d, seen);
return res;
}
case op::AndNLM:
{
formula rewrite = rewrite_and_nlm(f);
auto res = rec(rewrite);
finalize(res, opts, d, seen);
return res;
}
case op::first_match:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.push_back({bdd_l, form});
}
// determinize
bdd or_labels = bddfalse;
bdd support = bddtrue;
bool is_det = true;
for (const auto& [l, _] : res)
{
support &= bdd_support(l);
if (is_det)
is_det = !bdd_have_common_assignment(l, or_labels);
or_labels |= l;
}
if (is_det)
{
for (auto& [_, dest] : res)
dest = formula::first_match(dest);
finalize(res, opts, d, seen);
return res;
}
exp_t res_det;
std::vector<formula> dests;
for (bdd l: minterms_of(or_labels, support))
{
for (const auto& [ndet_label, ndet_dest] : res)
{
if (bdd_implies(l, ndet_label))
dests.push_back(ndet_dest);
}
formula or_dests = formula::OrRat(dests);
res_det.push_back({l, or_dests});
dests.clear();
}
for (auto& [_, dest] : res_det)
dest = formula::first_match(dest);
finalize(res_det, opts, d, seen);
return res_det;
}
case op::Fusion:
{
exp_t res;
formula E = f[0];
formula F = f.all_but(0);
exp_t Ei = rec(E);
// TODO: std::option
exp_t Fj = rec(F);
for (const auto& [li, ei] : Ei)
{
if (ei.accepts_eword())
{
for (const auto& [kj, fj] : Fj)
if ((li & kj) != bddfalse)
res.push_back({li & kj, fj});
}
formula ei_fusion_F = formula::Fusion({ei, F});
if (!ei_fusion_F.is(op::ff))
res.push_back({li, ei_fusion_F});
}
finalize(res, opts, d, seen);
return res;
}
case op::AndRat:
{
exp_t res;
for (const auto& sub_f : f)
{
auto exps = rec(sub_f);
if (exps.empty())
{
// op::AndRat: one of the expansions was empty (the only
// edge was `false`), so the AndRat is empty as
// well
res.clear();
break;
}
if (res.empty())
{
res = std::move(exps);
continue;
}
exp_t new_res;
bool inserted = false;
for (const auto& [l_key, l_val] : exps)
{
for (const auto& [r_key, r_val] : res)
{
if ((l_key & r_key) != bddfalse)
{
new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
inserted = true;
}
}
}
if (!inserted)
{
// all prefix conjuctions led to bddfalse, And is empty
res.clear();
break;
}
res = std::move(new_res);
}
finalize(res, opts, d, seen);
return res;
}
case op::OrRat:
{
exp_t res;
for (const auto& sub_f : f)
{
auto exps = rec(sub_f);
if (exps.empty())
continue;
if (res.empty())
{
res = std::move(exps);
continue;
}
for (const auto& [label, dest] : exps)
res.push_back({label, dest});
}
finalize(res, opts, d, seen);
return res;
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())
<< std::endl;
SPOT_UNIMPLEMENTED();
}
return {};
}
twa_graph_ptr
expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
{
auto finite = expand_finite_automaton2(f, d, opts);
return from_finite(finite);
}
struct signature_hash
{
std::size_t
operator() (const expansion_t& sig) const noexcept
{
size_t hash = 0;
for (const auto& keyvalue : sig)
{
hash ^= (bdd_hash()(keyvalue.first) ^ std::hash<formula>()(keyvalue.second))
+ 0x9e3779b9 + (hash << 6) + (hash >> 2);
}
return hash;
}
};
twa_graph_ptr
expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
{
bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge;
auto aut = make_twa_graph(d);
aut->prop_state_acc(false);
const auto acc_mark = aut->set_buchi();
auto formula2state = robin_hood::unordered_map<formula, unsigned>();
auto signature2state = std::unordered_map<expansion_t, unsigned, signature_hash>();
auto seen = std::unordered_set<formula>();
seen.insert(f);
unsigned init_state = aut->new_state();
aut->set_init_state(init_state);
formula2state.insert({ f, init_state });
auto f_aps = formula_aps(f);
for (auto& ap : f_aps)
aut->register_ap(ap);
auto formula2signature = robin_hood::unordered_map<formula, expansion_t>();
auto get_signature = [&](const formula& form) -> expansion_t
{
auto it = formula2signature.find(form);
if (it != formula2signature.end())
{
return it->second;
}
auto exp = expansion2(form, d, aut.get(), opts, &seen);
formula2signature.insert({form, exp});
return exp;
};
if (signature_merge)
signature2state.insert({ get_signature(f), init_state});
auto todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state});
auto state_names = new std::vector<std::string>();
std::ostringstream ss;
ss << f;
state_names->push_back(ss.str());
auto find_dst = [&](formula suffix) -> unsigned
{
unsigned dst;
auto it = formula2state.find(suffix);
if (it != formula2state.end())
{
dst = it->second;
}
else
{
if (signature_merge)
{
auto exp = get_signature(suffix);
auto it2 = signature2state.find(exp);
if (it2 != signature2state.end())
{
formula2state.insert({suffix, it2->second});
return it2->second;
}
}
dst = aut->new_state();
todo.push_back({suffix, dst});
seen.insert(suffix);
formula2state.insert({suffix, dst});
if (signature_merge)
signature2state.insert({get_signature(suffix), dst});
std::ostringstream ss;
ss << suffix;
state_names->push_back(ss.str());
}
return dst;
};
while (!todo.empty())
{
auto [curr_f, curr_state] = todo[todo.size() - 1];
todo.pop_back();
auto exp = get_signature(curr_f);
for (const auto& [letter, suffix] : exp)
{
if (suffix.is(op::ff))
// TODO ASSERT NOT
continue;
auto dst = find_dst(suffix);
auto curr_acc_mark = suffix.accepts_eword() ? acc_mark : acc_cond::mark_t();
aut->new_edge(curr_state, dst, letter, curr_acc_mark);
}
}
aut->set_named_prop("state-names", state_names);
if ((opts & exp_opts::MergeEdges)
&& !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost))
aut->merge_edges();
return aut;
}
}

45
spot/tl/expansions2.hh Normal file
View file

@ -0,0 +1,45 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <map>
#include <bddx.h>
#include <spot/misc/bddlt.hh>
#include <spot/tl/expansions.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/twagraph.hh>
namespace spot
{
SPOT_API expansion_t
expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen = nullptr);
SPOT_API twa_graph_ptr
expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
SPOT_API twa_graph_ptr
expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
SPOT_API formula
expansion_to_formula2(expansion_t e, bdd_dict_ptr& d);
}

2
spot/tl/sonf.cc
View file

@ -131,7 +131,7 @@ namespace spot
{
// recurse into rhs first (_ []-> rhs)
formula rhs =
f[1].map(extractor, extracted, extractor, false, false);
extractor(f[1], extracted, extractor, false, false);
f = formula::binop(kind, f[0], rhs);
formula ap = formula::ap(new_ap_name());

10
spot/twa/twagraph.cc
View file

@ -230,11 +230,15 @@ namespace spot
// them.
});
bool is_state_acc = this->prop_state_acc().is_true();
unsigned out = 0;
unsigned in = 1;
// Skip any leading false edge.
while (in < tend && trans[in].cond == bddfalse)
while (in < tend
&& trans[in].cond == bddfalse
&& (!is_state_acc || trans[in].src != trans[in].dst))
++in;
if (in < tend)
{
@ -243,7 +247,9 @@ namespace spot
trans[out] = trans[in];
for (++in; in < tend; ++in)
{
if (trans[in].cond == bddfalse) // Unusable edge
if (trans[in].cond == bddfalse
&& (!is_state_acc
|| trans[in].src != trans[in].dst)) // Unusable edge
continue;
// Merge edges with the same source, destination, and
// colors. (We test the source last, because this is the

2
spot/twaalgos/Makefile.am
View file

@ -99,6 +99,7 @@ twaalgos_HEADERS = \
totgba.hh \
toweak.hh \
translate.hh \
translate_aa.hh \
word.hh \
zlktree.hh
@ -177,6 +178,7 @@ libtwaalgos_la_SOURCES = \
totgba.cc \
toweak.cc \
translate.cc \
translate_aa.cc \
word.cc \
zlktree.cc

60
spot/twaalgos/alternation.cc
View file

@ -28,8 +28,8 @@
namespace spot
{
outedge_combiner::outedge_combiner(const twa_graph_ptr& aut)
: aut_(aut), vars_(bddtrue)
outedge_combiner::outedge_combiner(const twa_graph_ptr& aut, unsigned sink)
: aut_(aut), vars_(bddtrue), acc_sink_(sink)
{
}
@ -38,7 +38,9 @@ namespace spot
aut_->get_dict()->unregister_all_my_variables(this);
}
bdd outedge_combiner::operator()(unsigned st)
bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter,
const std::vector<std::tuple<unsigned, bdd, unsigned>>& edge_filter,
bool remove_original_edges)
{
const auto& dict = aut_->get_dict();
bdd res = bddtrue;
@ -47,9 +49,43 @@ namespace spot
bdd res2 = bddfalse;
for (auto& e: aut_->out(d1))
{
// handle edge filtering
if (!edge_filter.empty())
{
// Trying all univ dests for e, find if there was at least one
// compatible edge that was accepting in the original TFA
auto univ_dests = aut_->univ_dests(e.dst);
if (std::all_of(univ_dests.begin(), univ_dests.end(),
[&](unsigned dst) {
for (const auto& acc_e : edge_filter)
if(std::get<0>(acc_e) == e.src
&& std::get<2>(acc_e) == dst
&& bdd_implies(e.cond, std::get<1>(acc_e)))
return false; // false because we don't want to skip it
return true;
}))
continue;
}
else if (!dst_filter.empty()) // same for state-based acc
{
// if any edge destination is an accepting state in the SERE
// automaton, handle the edge, otherwise skip it
auto univ_dests = aut_->univ_dests(e.dst);
if (std::all_of(univ_dests.begin(), univ_dests.end(),
[&](unsigned dst)
{
return std::find(dst_filter.begin(), dst_filter.end(), dst)
== dst_filter.end();
}))
continue;
}
bdd out = bddtrue;
for (unsigned d: aut_->univ_dests(e.dst))
{
if (d == acc_sink_)
continue;
auto p = state_to_var.emplace(d, 0);
if (p.second)
{
@ -61,7 +97,11 @@ namespace spot
out &= bdd_ithvar(p.first->second);
}
res2 |= e.cond & out;
if (remove_original_edges)
e.cond = bddfalse;
}
res &= res2;
}
return res;
@ -78,7 +118,17 @@ namespace spot
{
bdd cond = bdd_exist(cube, vars_);
bdd dest = bdd_existcomp(cube, vars_);
while (dest != bddtrue)
if (dest == bddtrue)
{
// if dest is bddtrue then the accepting sink is the only
// destination for this edge, in that case don't filter it out
assert(acc_sink_ != -1u);
aut_->new_edge(st, acc_sink_, cond);
continue;
}
do
{
assert(bdd_low(dest) == bddfalse);
auto it = var_to_state.find(bdd_var(dest));
@ -86,6 +136,8 @@ namespace spot
univ_dest.push_back(it->second);
dest = bdd_high(dest);
}
while (dest != bddtrue);
std::sort(univ_dest.begin(), univ_dest.end());
aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond);
univ_dest.clear();

7
spot/twaalgos/alternation.hh
View file

@ -49,10 +49,13 @@ namespace spot
std::map<unsigned, int> state_to_var;
std::map<int, unsigned> var_to_state;
bdd vars_;
unsigned acc_sink_;
public:
outedge_combiner(const twa_graph_ptr& aut);
outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
~outedge_combiner();
bdd operator()(unsigned st);
bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>(),
const std::vector<std::tuple<unsigned, bdd, unsigned>>& edge_filter = std::vector<std::tuple<unsigned, bdd, unsigned>>(),
bool remove_original_edges = false);
void new_dests(unsigned st, bdd out) const;
};

184
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -19,9 +19,12 @@
#include "config.h"
#include <spot/misc/bddlt.hh>
#include <spot/misc/minato.hh>
#include <spot/tl/derive.hh>
#include <spot/tl/print.hh>
#include <spot/tl/apcollect.hh>
#include <spot/tl/mark.hh>
#include <spot/tl/nenoform.hh>
#include <spot/tl/expansions.hh>
#include <cassert>
#include <memory>
#include <utility>
@ -99,15 +102,14 @@ namespace spot
class ratexp_to_dfa final
{
typedef twa_graph::namer<formula> namer;
// Use robin_hood::pair because std::pair is not no-throw constructible
typedef robin_hood::pair<twa_graph_ptr, const namer*> labelled_aut;
public:
ratexp_to_dfa(translate_dict& dict);
ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false);
std::vector<std::pair<bdd, formula>> succ(formula f);
~ratexp_to_dfa();
protected:
// Use robin_hood::pair because std::pair is not no-throw constructible
typedef robin_hood::pair<twa_graph_ptr, const namer*> labelled_aut;
labelled_aut translate(formula f);
private:
@ -115,6 +117,7 @@ namespace spot
typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
std::vector<labelled_aut> automata_;
f2a_t f2a_;
bool disable_scc_trimming_;
};
// Helper dictionary. We represent formulae using BDDs to
@ -221,6 +224,7 @@ namespace spot
int
register_proposition(formula f)
{
// TODO: call this in expansions
int num = dict->register_proposition(f, this);
var_set &= bdd_ithvar(num);
return num;
@ -747,55 +751,7 @@ namespace spot
SPOT_UNREACHABLE();
case op::AndNLM:
{
unsigned s = f.size();
vec final;
vec non_final;
for (auto g: f)
if (g.accepts_eword())
final.emplace_back(g);
else
non_final.emplace_back(g);
if (non_final.empty())
// (a* & b*);c = (a*|b*);c
return recurse_and_concat(formula::OrRat(std::move(final)));
if (!final.empty())
{
// let F_i be final formulae
// N_i be non final formula
// (F_1 & ... & F_n & N_1 & ... & N_m)
// = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
// | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
formula f = formula::OrRat(std::move(final));
formula n = formula::AndNLM(std::move(non_final));
formula t = formula::one_star();
formula ft = formula::Concat({f, t});
formula nt = formula::Concat({n, t});
formula ftn = formula::AndRat({ft, n});
formula fnt = formula::AndRat({f, nt});
return recurse_and_concat(formula::OrRat({ftn, fnt}));
}
// No final formula.
// Translate N_1 & N_2 & ... & N_n into
// N_1 && (N_2;[*]) && ... && (N_n;[*])
// | (N_1;[*]) && N_2 && ... && (N_n;[*])
// | (N_1;[*]) && (N_2;[*]) && ... && N_n
formula star = formula::one_star();
vec disj;
for (unsigned n = 0; n < s; ++n)
{
vec conj;
for (unsigned m = 0; m < s; ++m)
{
formula g = f[m];
if (n != m)
g = formula::Concat({g, star});
conj.emplace_back(g);
}
disj.emplace_back(formula::AndRat(std::move(conj)));
}
return recurse_and_concat(formula::OrRat(std::move(disj)));
return recurse_and_concat(rewrite_and_nlm(f));
}
case op::AndRat:
{
@ -932,8 +888,22 @@ namespace spot
bdd res;
if (!f.is_boolean())
{
ratexp_trad_visitor v(dict, to_concat);
res = v.visit(f);
if (sere_translation_options() == 0)
{
ratexp_trad_visitor v(dict, to_concat);
res = v.visit(f);
}
else // version expansion
{
res = bddfalse;
for (auto [label, succ]: expansion(f, dict.dict, &dict, exp_opts::expand_opt::None, nullptr))
{
if (to_concat)
succ = formula::Concat({succ, to_concat});
int x = dict.register_next_variable(succ);
res |= label & bdd_ithvar(x);
}
}
}
else
{
@ -948,8 +918,9 @@ namespace spot
}
ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict)
ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming)
: dict_(dict)
, disable_scc_trimming_(disable_scc_trimming)
{
}
@ -1002,6 +973,12 @@ namespace spot
}
}
if (disable_scc_trimming_)
{
automata_.emplace_back(a, namer);
return labelled_aut(a, namer);
}
// The following code trims the automaton in a crude way by
// eliminating SCCs that are not coaccessible. It does not
// actually remove the states, it simply marks the corresponding
@ -2226,4 +2203,99 @@ namespace spot
return a;
}
twa_graph_ptr
sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming)
{
// make sure we use bdd translation in this case
auto old_opt = sere_translation_options();
sere_translation_options("bdd");
f = negative_normal_form(f);
tl_simplifier* s = new tl_simplifier(dict);
twa_graph_ptr a = make_twa_graph(dict);
translate_dict d(a, s, false, false, false);
ratexp_to_dfa sere2dfa(d, disable_scc_trimming);
auto [dfa, namer] = sere2dfa.translate(f);
// language was empty, build an automaton with one non accepting state
if (dfa == nullptr)
{
auto res = make_twa_graph(dict);
res->set_init_state(res->new_state());
res->prop_universal(true);
res->prop_complete(false);
res->prop_stutter_invariant(true);
res->prop_terminal(true);
res->prop_state_acc(true);
return res;
}
auto res = make_twa_graph(dfa, {false, false, true, false, false, false});
// HACK: translate_dict registers the atomic propositions in the "final"
// automaton that would be produced by a full translation, not in the
// intermediate automaton we're interested in. We can copy them from the
// resulting automaton.
res->copy_ap_of(a);
res->prop_state_acc(true);
const auto acc_mark = res->set_buchi();
size_t sn = namer->state_to_name.size();
auto names = new std::vector<std::string>(sn);
for (size_t i = 0; i < sn; ++i)
{
formula g = namer->state_to_name[i];
(*names)[i] = str_psl(g);
if (g.accepts_eword())
{
if (res->get_graph().state_storage(i).succ == 0)
res->new_edge(i, i, bddfalse, acc_mark);
else
{
for (auto& e : res->out(i))
e.acc = acc_mark;
}
}
}
res->set_named_prop("state-names", names);
// restore previous option
if (old_opt != 0)
sere_translation_options("expansion");
return res;
}
int sere_translation_options(const char* version)
{
static int pref = -1;
const char *env = nullptr;
if (!version && pref < 0)
version = env = getenv("SPOT_SERE_TRANSLATE_OPT");
if (version)
{
if (!strcasecmp(version, "bdd"))
pref = 0;
else if (!strcasecmp(version, "expansion"))
pref = 1;
else
{
const char* err = ("sere_translation_options(): argument"
" should be one of {bdd,expansion}");
if (env)
err = "SPOT_SERE_TRANSLATE_OPT should be one of {bdd,expansion}";
throw std::runtime_error(err);
}
}
else if (pref < 0)
{
pref = 0;
}
return pref;
}
}

5
spot/twaalgos/ltl2tgba_fm.hh
View file

@ -89,4 +89,9 @@ namespace spot
bool unambiguous = false,
const output_aborter* aborter = nullptr,
bool label_with_ltl = false);
SPOT_API twa_graph_ptr
sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming = false);
SPOT_API int sere_translation_options(const char* version = nullptr);
}

47
spot/twaalgos/remprop.cc
View file

@ -245,4 +245,51 @@ namespace spot
}
twa_graph_ptr from_finite(const_twa_graph_ptr aut, const char* alive)
{
twa_graph_ptr res =
make_twa_graph(aut,
{ true, false, true, false, false, false });
if (aut->get_named_prop<std::vector<std::string>>("state-names"))
res->copy_state_names_from(aut);
auto* names = res->get_named_prop<std::vector<std::string>>("state-names");
unsigned alive_sink = res->new_state();
if (names != nullptr)
names->push_back("sink");
auto acc = res->acc().all_sets();
auto alive_bdd = bdd_ithvar(res->register_ap(alive));
res->new_edge(alive_sink, alive_sink, !alive_bdd, acc);
unsigned ns = res->num_states();
for (unsigned s = 0; s < ns; ++s)
{
if (s == alive_sink)
continue;
bool was_acc = res->state_is_accepting(s);
// erase accepting marks, require alive on non-accepting transition,
// and remove self-loop edges used to mark acceptance
auto i = res->out_iteraser(s);
while (i)
{
if (i->src == i->dst && i->cond == bddfalse)
{
i.erase();
continue;
}
i->cond &= alive_bdd;
i->acc = {};
++i;
}
if (was_acc)
res->new_edge(s, alive_sink, !alive_bdd);
}
return res;
}
}

3
spot/twaalgos/remprop.hh
View file

@ -53,5 +53,8 @@ namespace spot
SPOT_API twa_graph_ptr
to_finite(const_twa_graph_ptr aut, const char* alive = "alive");
/// \brief The opposite of the to_finite operation
SPOT_API twa_graph_ptr
from_finite(const_twa_graph_ptr aut, const char* alive = "alive");
}

578
spot/twaalgos/translate_aa.cc Normal file
View file

@ -0,0 +1,578 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2018, 2020-2021 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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <string.h>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/translate_aa.hh>
#include <spot/tl/derive.hh>
#include <spot/tl/expansions.hh>
#include <spot/tl/expansions2.hh>
#include <spot/tl/nenoform.hh>
#include <iostream>
namespace spot
{
namespace
{
twa_graph_ptr sere_aa_translate(formula f, const bdd_dict_ptr& dict)
{
// old bdd method
if (sere_aa_translation_options() == 0)
return sere_to_tgba(f, dict, true);
// derivation
if (sere_aa_translation_options() == 1)
return derive_finite_automaton_with_first(f, dict);
// linear form
if (sere_aa_translation_options() == 2)
return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
// linear form - trans-based
return expand_finite_automaton2(f, dict, exp_opts::expand_opt::None);
}
struct ltl_to_aa_builder
{
ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink)
: aut_(aut)
, accepting_sink_(accepting_sink)
, uniq_(aut_->get_graph(), accepting_sink)
, oe_(aut_, accepting_sink)
{
}
~ltl_to_aa_builder()
{
aut_->get_dict()->unregister_all_my_variables(this);
}
twa_graph_ptr aut_;
unsigned accepting_sink_;
internal::univ_dest_mapper<twa_graph::graph_t> uniq_;
outedge_combiner oe_;
void add_self_loop(twa_graph::edge_storage_t const& e,
unsigned init_state,
acc_cond::mark_t acc)
{
if (e.dst == accepting_sink_)
{
// avoid creating a univ_dests vector if the only dest is an
// accepting sink, which can be simplified, only keeping the self
// loop
aut_->new_edge(init_state, init_state, e.cond, acc);
return;
}
auto dests = aut_->univ_dests(e);
std::vector<unsigned> new_dests(dests.begin(), dests.end());
new_dests.push_back(init_state);
unsigned dst = uniq_.new_univ_dests(new_dests.begin(),
new_dests.end());
aut_->new_edge(init_state, dst, e.cond, acc);
}
unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut,
std::map<unsigned, unsigned>& old_to_new,
std::vector<unsigned>* acc_edges = nullptr,
bool use_accepting_sink = true)
{
unsigned ns = sere_aut->num_states();
bool trans_based = sere_aut->prop_state_acc().is_false();
// TODO: create all new states at once, keeping an initial offset (the
// number of states already present in aut_)
aut_->copy_ap_of(sere_aut);
auto register_state = [&](unsigned st) -> unsigned {
auto p = old_to_new.emplace(st, 0);
if (p.second)
{
unsigned new_st = aut_->new_state();
p.first->second = new_st;
}
return p.first->second;
};
for (unsigned st = 0; st < ns; ++st)
{
unsigned new_st = register_state(st);
for (const auto& e : sere_aut->out(st))
{
bool edge_is_acc = ((trans_based && e.acc)
|| (!trans_based && sere_aut->state_is_accepting(e.dst)));
if (edge_is_acc)
{
// point to accepting sink instead of original dst if asked
if (use_accepting_sink)
aut_->new_edge(new_st, accepting_sink_, e.cond);
else
{
unsigned new_e = aut_->new_edge(new_st, register_state(e.dst), e.cond);
// remember if old edges were accepting
if (acc_edges != nullptr)
acc_edges->push_back(new_e);
}
}
}
}
auto it = old_to_new.find(sere_aut->get_init_state_number());
assert(it != old_to_new.end());
return it->second;
}
unsigned recurse(formula f)
{
switch (f.kind())
{
case op::ff:
return aut_->new_state();
case op::tt:
{
unsigned init_state = aut_->new_state();
aut_->new_edge(init_state, accepting_sink_, bddtrue, {});
return init_state;
}
case op::ap:
case op::Not:
{
unsigned init_state = aut_->new_state();
bdd ap;
if (f.kind() == op::ap)
ap = bdd_ithvar(aut_->register_ap(f.ap_name()));
else
ap = bdd_nithvar(aut_->register_ap(f[0].ap_name()));
aut_->new_edge(init_state, accepting_sink_, ap, {});
return init_state;
}
// FIXME: is this right for LTLf?
case op::strong_X:
case op::X:
{
unsigned sub_init_state = recurse(f[0]);
unsigned new_init_state = aut_->new_state();
aut_->new_edge(new_init_state, sub_init_state, bddtrue, {});
return new_init_state;
}
case op::Or:
{
unsigned init_state = aut_->new_state();
for (const auto& sub_formula : f)
{
unsigned sub_init = recurse(sub_formula);
for (auto& e : aut_->out(sub_init))
{
unsigned dst = e.dst;
if (aut_->is_univ_dest(e.dst))
{
auto dests = aut_->univ_dests(e);
dst = uniq_.new_univ_dests(dests.begin(), dests.end());
}
aut_->new_edge(init_state, dst, e.cond, {});
}
}
return init_state;
}
case op::And:
{
unsigned init_state = aut_->new_state();
bdd comb = bddtrue;
for (const auto& sub_formula : f)
{
unsigned sub_init = recurse(sub_formula);
comb &= oe_(sub_init);
}
oe_.new_dests(init_state, comb);
return init_state;
}
case op::U:
case op::W:
{
auto acc = f.kind() == op::U
? acc_cond::mark_t{0}
: acc_cond::mark_t{};
unsigned init_state = aut_->new_state();
unsigned lhs_init = recurse(f[0]);
unsigned rhs_init = recurse(f[1]);
std::vector<unsigned> new_dests;
for (auto& e : aut_->out(lhs_init))
add_self_loop(e, init_state, acc);
for (auto& e : aut_->out(rhs_init))
{
unsigned dst = e.dst;
if (aut_->is_univ_dest(e.dst))
{
auto dests = aut_->univ_dests(e);
dst = uniq_.new_univ_dests(dests.begin(), dests.end());
}
aut_->new_edge(init_state, dst, e.cond, {});
}
return init_state;
}
case op::R:
case op::M:
{
auto acc = f.kind() == op::M
? acc_cond::mark_t{0}
: acc_cond::mark_t{};
unsigned init_state = aut_->new_state();
unsigned lhs_init = recurse(f[0]);
unsigned rhs_init = recurse(f[1]);
for (auto& e : aut_->out(rhs_init))
add_self_loop(e, init_state, acc);
bdd comb = oe_(lhs_init);
comb &= oe_(rhs_init);
oe_.new_dests(init_state, comb);
return init_state;
}
// F(phi) = tt U phi
case op::F:
{
auto acc = acc_cond::mark_t{0};
// if phi is boolean then we can reuse its initial state (otherwise
// we can't because of potential self loops)
if (f[0].is_boolean())
{
unsigned init_state = recurse(f[0]);
aut_->new_edge(init_state, init_state, bddtrue, acc);
return init_state;
}
unsigned init_state = aut_->new_state();
unsigned sub_init = recurse(f[0]);
aut_->new_edge(init_state, init_state, bddtrue, acc);
for (auto& e : aut_->out(sub_init))
aut_->new_edge(init_state, e.dst, e.cond, {});
return init_state;
}
// G phi = ff R phi
case op::G:
{
unsigned init_state = aut_->new_state();
unsigned sub_init = recurse(f[0]);
// translate like R, but only the self loop part; `ff` cancels out
// the product of edges
std::vector<unsigned> new_dests;
for (auto& e : aut_->out(sub_init))
add_self_loop(e, init_state, {});
return init_state;
}
case op::EConcat:
{
unsigned rhs_init = recurse(f[1]);
const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
// TODO: this should be a std::vector<bool> !
std::vector<unsigned> acc_edges;
std::map<unsigned, unsigned> old_to_new;
copy_sere_aut_to_res(sere_aut, old_to_new, &acc_edges, false);
// mark all edges from NFA in new automaton
unsigned ns = sere_aut->num_states();
for (unsigned st = 0; st < ns; ++st)
{
auto it = old_to_new.find(st);
assert(it != old_to_new.end());
unsigned new_st = it->second;
for (auto& e : aut_->out(new_st))
e.acc = acc_cond::mark_t{0};
}
for (unsigned i : acc_edges)
{
auto& e1 = aut_->edge_storage(i);
for (const auto& e2 : aut_->out(rhs_init))
aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond);
}
auto it = old_to_new.find(sere_aut->get_init_state_number());
assert(it != old_to_new.end());
return it->second;
}
case op::UConcat:
{
unsigned rhs_init = recurse(f[1]);
const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
bool trans_based = sere_aut->prop_state_acc().is_false();
// DFA recognizes the empty language, so {0} []-> rhs is always true
unsigned ns = sere_aut->num_states();
bool accepts = false;
for (unsigned st = 0; st < ns && !accepts; ++st)
{
if (trans_based)
{
for (const auto& e : sere_aut->out(st))
if (e.acc)
{
accepts = true;
break;
}
}
else
accepts = sere_aut->state_is_accepting(st);
}
if (!accepts)
return accepting_sink_;
std::map<unsigned, unsigned> old_to_new;
std::map<unsigned, int> state_to_var;
std::map<int, unsigned> var_to_state;
bdd vars = bddtrue;
bdd aps = sere_aut->ap_vars();
std::vector<unsigned> univ_dest;
// TODO: this should be a std::vector<bool> !
std::vector<unsigned> acc_states;
// any edge compatible with that should be considered accepting
std::vector<std::tuple<unsigned, bdd, unsigned>> acc_edges;
// registers a state in various maps and returns the index of the
// anonymous bdd var representing that state
auto register_state = [&](unsigned st) -> int {
auto p = state_to_var.emplace(st, 0);
if (p.second)
{
int v = dict->register_anonymous_variables(1, this);
p.first->second = v;
unsigned new_st = aut_->new_state();
old_to_new.emplace(st, new_st);
var_to_state.emplace(v, new_st);
if (!trans_based && sere_aut->state_is_accepting(st))
acc_states.push_back(new_st);
vars &= bdd_ithvar(v);
}
return p.first->second;
};
// FIXME: this code handles dualization, but we cannot dualize if
// this situation arises:
//
// State: 0
// [a] 1
// [a] 2 {0}
//
// The quick fix is to simply determinize the NFA before dualizing,
// which removes any existentialism.
aut_->copy_ap_of(sere_aut);
for (unsigned st = 0; st < ns; ++st)
{
register_state(st);
bdd sig = bddfalse;
for (const auto& e : sere_aut->out(st))
{
int st_bddi = register_state(e.dst);
sig |= e.cond & bdd_ithvar(st_bddi);
// register edge that was accepting in TFA
if (trans_based && e.acc)
{
unsigned new_src = old_to_new[e.src];
unsigned new_dst = old_to_new[e.dst];
acc_edges.push_back({new_src, e.cond, new_dst});
}
}
for (bdd cond : minterms_of(bddtrue, aps))
{
bdd dest = bdd_appex(sig, cond, bddop_and, aps);
while (dest != bddfalse)
{
assert(bdd_high(dest) == bddtrue);
auto it = var_to_state.find(bdd_var(dest));
assert(it != var_to_state.end());
univ_dest.push_back(it->second);
dest = bdd_low(dest);
}
auto it = old_to_new.find(st);
assert(it != old_to_new.end());
unsigned src = it->second;
unsigned dst = univ_dest.empty()
? accepting_sink_
: (uniq_.new_univ_dests(univ_dest.begin(),
univ_dest.end()));
aut_->new_edge(src, dst, cond, {});
univ_dest.clear();
}
}
for (unsigned st = 0; st < ns; ++st)
{
auto it = old_to_new.find(st);
assert(it != old_to_new.end());
unsigned new_st = it->second;
bdd comb = bddtrue;
comb &= oe_(new_st, acc_states, acc_edges, true);
if (comb != bddtrue)
{
comb &= oe_(rhs_init);
oe_.new_dests(new_st, comb);
}
}
auto it = old_to_new.find(sere_aut->get_init_state_number());
assert(it != old_to_new.end());
aut_->merge_edges();
return it->second;
}
case op::Closure:
{
twa_graph_ptr sere_aut =
derive_finite_automaton_with_first(f[0], aut_->get_dict());
std::map<unsigned, unsigned> old_to_new;
return copy_sere_aut_to_res(sere_aut, old_to_new);
}
case op::NegClosure:
case op::NegClosureMarked:
case op::eword:
case op::Xor:
case op::Implies:
case op::Equiv:
case op::EConcatMarked:
case op::OrRat:
case op::AndRat:
case op::AndNLM:
case op::Concat:
case op::Fusion:
case op::Star:
case op::FStar:
case op::first_match:
SPOT_UNREACHABLE();
return -1;
}
SPOT_UNREACHABLE();
}
};
}
twa_graph_ptr
ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states)
{
f = negative_normal_form(f);
auto aut = make_twa_graph(dict);
aut->set_co_buchi();
unsigned accepting_sink = aut->new_state();
aut->new_edge(accepting_sink, accepting_sink, bddtrue, {});
auto builder = ltl_to_aa_builder(aut, accepting_sink);
unsigned init_state = builder.recurse(f);
aut->set_init_state(init_state);
if (purge_dead_states)
{
aut->purge_dead_states();
aut->merge_edges();
}
return aut;
}
int sere_aa_translation_options(const char* version)
{
static int pref = -1;
const char *env = nullptr;
if (!version && pref < 0)
version = env = getenv("SPOT_SERE_AA_TRANSLATE_OPT");
if (version)
{
if (!strcasecmp(version, "bdd"))
pref = 0;
else if (!strcasecmp(version, "derive"))
pref = 1;
else if (!strcasecmp(version, "lf"))
pref = 2;
else if (!strcasecmp(version, "lft"))
pref = 3;
else
{
const char* err = ("sere_aa_translation_options(): argument"
" should be one of {bdd,derive,lf,lft}");
if (env)
err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,lf,lft}";
throw std::runtime_error(err);
}
}
else if (pref < 0)
{
pref = 0;
}
return pref;
}
}

34
spot/twaalgos/translate_aa.hh Normal file
View file

@ -0,0 +1,34 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// 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/>.
#pragma once
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
namespace spot
{
SPOT_API twa_graph_ptr
ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states = false);
SPOT_API int sere_aa_translation_options(const char* version = nullptr);
}

2
tests/Makefile.am
View file

@ -76,6 +76,7 @@ check_PROGRAMS = \
core/intvcomp \
core/intvcmp2 \
core/kripkecat \
core/ltl2aa \
core/ltl2dot \
core/ltl2text \
core/ltlrel \
@ -125,6 +126,7 @@ core_cube_SOURCES = core/cube.cc
core_equals_SOURCES = core/equalsf.cc
core_kind_SOURCES = core/kind.cc
core_length_SOURCES = core/length.cc
core_ltl2aa_SOURCES = core/ltl2aa.cc
core_ltl2dot_SOURCES = core/readltl.cc
core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
core_ltl2text_SOURCES = core/readltl.cc

1
tests/core/.gitignore vendored
View file

@ -33,6 +33,7 @@ kripkecat
length
.libs
ikwiad
ltl2aa
ltl2dot
ltl2text
ltlmagic

25
tests/core/expand.cc Normal file
View file

@ -0,0 +1,25 @@
#include "config.h"
#include <spot/tl/expansions.hh>
#include <spot/tl/parse.hh>
#include <spot/twa/formula2bdd.hh>
#include <iostream>
int main(int argc, char** argv)
{
if (argc != 2)
return 1;
spot::formula f = spot::parse_infix_sere(argv[1]).f;
auto d = spot::make_bdd_dict();
auto m = spot::expansion(f, d, nullptr);
for (const auto& [bdd_l, form] : m)
std::cout << '[' << bdd_to_formula(bdd_l, d) << ']' << ": " << form << std::endl;
std::cout << "formula: " << expansion_to_formula(m, d) << std::endl;
d->unregister_all_my_variables(nullptr);
return 0;
}

22
tests/core/ltl2aa.cc Normal file
View file

@ -0,0 +1,22 @@
#include "config.h"
#include <fstream>
#include <spot/tl/formula.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/translate_aa.hh>
int main(int argc, char * argv[])
{
if (argc < 3)
return 1;
spot::formula f = spot::parse_formula(argv[1]);
spot::bdd_dict_ptr d = spot::make_bdd_dict();
auto aut = ltl_to_aa(f, d, true);
std::ofstream out(argv[2]);
spot::print_hoa(out, aut);
return 0;
}