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

ltl2tgba_fm: implement a small optimization

Browse source 
Fixes #277.

* spot/twaalgos/ltl2tgba_fm.cc: Improve the translation of f U g
when f is universal.  Suggested by Maximilien Colange.
* tests/core/ltl2tgba.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-02 14:48:52 +02:00
parent 42abcf8559
commit 190d4cfaf1
2 changed files with 18 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -1,9 +1,9 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 // Copyright (C) 2008-2017 Laboratoire de Recherche et Développement
// Laboratoire de Recherche et Développement de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Coopératifs (SRC), Université Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -1326,10 +1326,20 @@ namespace spot
bdd f1 = recurse(node[0]); bdd f1 = recurse(node[0]);
bdd f2 = recurse(node[1]); bdd f2 = recurse(node[1]);
// r(f1 U f2) = r(f2) + a(f2)r(f1)X(f1 U f2) if not recurring // r(f1 U f2) = r(f2) + a(f2)r(f1)X(f1 U f2) if not recurring
// and f1 not universal
// r(f1 U f2) = r(f2) + a(f2)r(f1)X(Ff2) if not recurring
// and f1 universal
// r(f1 U f2) = r(f2) + a(f2)r(f1) if recurring // r(f1 U f2) = r(f2) + a(f2)r(f1) if recurring
f1 &= bdd_ithvar(dict_.register_a_variable(node[1])); f1 &= bdd_ithvar(dict_.register_a_variable(node[1]));
if (!recurring_) if (!recurring_)
f1 &= bdd_ithvar(dict_.register_next_variable(node)); {
formula nxt =
node[0].is_universal() ? formula::F(node[1]) : node;
// rewriting r(f1)X(f1 U f2) as r(f1)X(Ff2) when f1 is
// universal is an optimization that helps with formulas
// such as (G(Fa & Fb)) U a.
f1 &= bdd_ithvar(dict_.register_next_variable(nxt));
}
if (dict_.unambiguous) if (dict_.unambiguous)
f1 &= neg_of(node[1]); f1 &= neg_of(node[1]);
return f2 | f1; return f2 | f1;

2
tests/core/ltl2tgba.test
View file

@ -263,3 +263,5 @@ f2='Gp1 | FGp0'
(ltl2tgba -xsimul=1 --low "$f1"; ltl2tgba -xsimul=1 --low "$f2") > res1 (ltl2tgba -xsimul=1 --low "$f1"; ltl2tgba -xsimul=1 --low "$f2") > res1
ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2 ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2
diff res1 res2 diff res1 res2
test 3 = `ltl2tgba -f 'G(Fa & Fb) U a' --stats=%s`