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

derive: extract AndNLM rewriting

Browse source
This commit is contained in:
Antoine Martin 2022-03-18 19:27:19 +01:00
parent cc32f35f45
commit 4ab97a6841
3 changed files with 60 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

55
spot/tl/derive.cc
View file

@ -48,6 +48,61 @@ namespace spot
}
}
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(formula f, bool deterministic)
{

3
spot/tl/derive.hh
View file

@ -40,4 +40,7 @@ namespace spot
SPOT_API twa_graph_ptr
derive_finite_automaton(formula f, bool deterministic = true);
SPOT_API formula
rewrite_and_nlm(formula f);
}

51
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -19,6 +19,7 @@
#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>
@ -748,55 +749,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:
{