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

simplify: rewrite GF(a & Fb) as G(Fa & Fb)

Browse source 
This addresses part of #35, and is just a generalization of the rules
from 646c5170 for #263 (hence, no new documentation).

* spot/tl/simplify.cc: Implement this.
* tests/core/reduccmp.test: Add test cases.
* tests/core/stutter-tgba.test: Adjust to expect smaller automata.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-02 19:54:07 +02:00
parent e8527d5ae9
commit 6cd6802ace
3 changed files with 64 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

84
spot/tl/simplify.cc
View file

@ -910,6 +910,23 @@ namespace spot
if (opt_.event_univ && c.is_eventual())
return c;
auto g_in_f = [this](formula g, std::vector<formula>* to)
{
if (g[0].is(op::Or))
{
mospliter s2(mospliter::Split_Univ, g[0], c_);
for (formula e: *s2.res_Univ)
to->push_back(e.is(op::X) ? e[0] : e);
to->push_back
(unop_multop(op::G, op::Or,
std::move(*s2.res_other)));
}
else
{
to->push_back(g);
}
};
if (opt_.reduce_basics)
{
// F(a U b) = F(b)
@ -927,6 +944,17 @@ namespace spot
if (c.is(op::X))
return recurse(unop_unop(op::X, op::F, c[0]));
// G(F(a & Fb)) = G(Fa & Fb)
if (c.is({op::G, op::Or}))
{
std::vector<formula> toadd;
g_in_f(c, &toadd);
formula res = unop_multop(op::F, op::Or,
std::move(toadd));
if (res != f)
return recurse(res);
}
// FG(a & Xb) = FG(a & b)
// FG(a & Gb) = FG(a & b)
if (c.is({op::G, op::And}))
@ -1018,18 +1046,7 @@ namespace spot
std::vector<formula>* to = opt_.favor_event_univ ?
s.res_Univ.get() : s.res_other.get();
for (formula g: *s.res_G)
if (g[0].is(op::Or))
{
mospliter s2(mospliter::Split_Univ, g[0], c_);
for (formula u: *s2.res_Univ)
to->push_back(u.is(op::X) ? u[0] : u);
to->push_back(unop_multop(op::G, op::Or,
std::move(*s2.res_other)));
}
else
{
to->push_back(g);
}
g_in_f(g, to);
formula res = unop_multop(op::F, op::Or,
std::move(*s.res_other));
if (s.res_Univ)
@ -1057,6 +1074,23 @@ namespace spot
if (opt_.event_univ && c.is_universal())
return c;
auto f_in_g = [this](formula f, std::vector<formula>* to)
{
if (f[0].is(op::And))
{
mospliter s2(mospliter::Split_Event, f[0], c_);
for (formula e: *s2.res_Event)
to->push_back(e.is(op::X) ? e[0] : e);
to->push_back
(unop_multop(op::F, op::And,
std::move(*s2.res_other)));
}
else
{
to->push_back(f);
}
};
if (opt_.reduce_basics)
{
// G(a R b) = G(b)
@ -1074,6 +1108,17 @@ namespace spot
if (c.is(op::X))
return recurse(unop_unop(op::X, op::G, c[0]));
// G(F(a & Fb)) = G(Fa & Fb)
if (c.is({op::F, op::And}))
{
std::vector<formula> toadd;
f_in_g(c, &toadd);
formula res = unop_multop(op::G, op::And,
std::move(toadd));
if (res != f)
return recurse(res);
}
// G(f1|f2|GF(f3)|GF(f4)|f5|f6) =
// G(f1|f2) | GF(f3|f4) | f5 | f6
// if f5 and f6 are both eventual and universal.
@ -1118,19 +1163,8 @@ namespace spot
std::vector<formula>* to = opt_.favor_event_univ ?
s.res_Event.get() : s.res_other.get();
for (formula f: *s.res_F)
if (f[0].is(op::And))
{
mospliter s2(mospliter::Split_Event, f[0], c_);
for (formula e: *s2.res_Event)
to->push_back(e.is(op::X) ? e[0] : e);
to->push_back
(unop_multop(op::F, op::And,
std::move(*s2.res_other)));
}
else
{
to->push_back(f);
}
f_in_g(f, to);
formula res = unop_multop(op::G, op::And,
std::move(*s.res_other));
if (s.res_Event)

2
tests/core/reduccmp.test
View file

@ -302,8 +302,10 @@ GFa M b, GFa & b
G(a & XFb), G(a & Fb)
G(a & XF(b & XFc & Fd)), G(a & Fb & Fc & Fd)
GF(a & XF(b & Fc)), G(Fa & Fb & Fc)
F(a | XGb), F(a | Gb)
F(a | XG(b | XGc | Gd)), F(a | Gb | Gc | Gd)
FG(a | XG(b | Gc)), F(Ga | Gb | Gc)
Fa|Xb|GFc, Fa | X(b|GFc)
Fa|GFc, F(a|GFc)

6
tests/core/stutter-tgba.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
# Copyright (C) 2014-2017 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -29,13 +29,13 @@ $ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa
$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa
$autfilt pos.hoa --product neg.hoa -H > prod.hoa
$autfilt --is-empty prod.hoa -q && exit 1
$autfilt --states=10 prod.hoa -q
$autfilt --states=7 prod.hoa -q
$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa
$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa
$autfilt pos.hoa --product neg.hoa -H > prod.hoa
$autfilt --is-empty prod.hoa -q && exit 1
$autfilt --states=12 prod.hoa -q
$autfilt --states=9 prod.hoa -q
# Check for issue #7.