diff --git a/AUTHORS b/AUTHORS
index 73d749b2b..6a485edb2 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -12,7 +12,7 @@ Guillaume Sadegh
Heikki Tauriainen
Pierre Parutto
Rachid Rebiha
-Soheib Baarir
+Souheib Baarir
Thomas Badie
Thomas Martinez
Tomáš Babiak
diff --git a/NEWS b/NEWS
index 3060576bc..547f8ddc7 100644
--- a/NEWS
+++ b/NEWS
@@ -1,4 +1,4 @@
-New in spot 1.2.3a (not yet released)
+New in spot 1.2.4a (not yet released)
* Major changes (including backward incompatible changes):
@@ -69,6 +69,30 @@ New in spot 1.2.3a (not yet released)
implementation of Couvreur's FM'99 emptiness check.
+New in spot 1.2.4 (2014-05-15)
+
+ * New features:
+
+ - "-B -x degen-lskip" can be used to disable level-skipping in the
+ degeralization procedure called by ltl2tgba and dstar2tgba.
+ This is mostly meant for running experiments.
+ - "-B -x degen-lcache=N" can be used to experiment with different
+ type of level caching during degeneralization.
+
+ * Bug fixes:
+
+ - Change the Python bindings to make them compatible with Swig 3.0.
+ - "ltl2tgta --ta" could crash in certain conditions due to the
+ introduction of a simulation-based reduction after
+ degeneralization.
+ - Fix four incorrect formula-simplification rules, three were
+ related to the factorization of Boolean subformulas in
+ operands of the non-length-matching "&" SERE operator, and
+ a fourth one could only be enabled by explicitely passing the
+ favor_event_univ option to the simplifier (not the default).
+ - Fix incorrect translation of the fusion operator (":") in SERE
+ such as {xx;1}:yy[*] where the left operand has 1 as tail.
+
New in spot 1.2.3 (2014-02-11)
* New features:
@@ -100,8 +124,8 @@ New in spot 1.2.3 (2014-02-11)
- Fix determinism of the SAT-based minimization encoding.
(It would sometimes produce different equivalent automata,
because of a different encoding order.)
- - A the SAT-based minimization is asked for a 10-state automaton
- and return a 6-state automaton, do not ask for a 9-state
+ - If the SAT-based minimization is asked for a 10-state automaton
+ and returns a 6-state automaton, do not ask for a 9-state
automaton in the next iteration...
- Fix some compilation issue with the version of Apple's Clang
that is installed with MacOS X 10.9.
diff --git a/configure.ac b/configure.ac
index 690129e36..2970c4acc 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
# along with this program. If not, see .
AC_PREREQ([2.61])
-AC_INIT([spot], [1.2.3a], [spot@lrde.epita.fr])
+AC_INIT([spot], [1.2.4a], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index 4fc1244a8..f2f8c394c 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -31,8 +31,10 @@ Let us first state a few facts about this minimization procedure.
automaton: when the number of clauses output by Spot (and to be fed
to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was
killed by a signal.
+6) Details about the SAT encoding used in the two procedures can be
+ found in our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]].
-* How change the SAT solver used
+* How to change the SAT solver used
The environment variable =SPOT_SATSOLVER= can be used to change the
SAT solver used by Spot. The default is "=glucose -verb=0 -model %I
diff --git a/doc/org/tools.org b/doc/org/tools.org
index 0d1cd597d..24c937364 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -1,4 +1,4 @@
-#+TITLE: Command-line tools installed by Spot 1.2.3
+#+TITLE: Command-line tools installed by Spot 1.2.4
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
@@ -60,9 +60,9 @@ the following articles:
This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
-- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/.
- In Proc. of VECoS'11. Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011.
- ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.slides.pdf][slides]])
+- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
+ Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
+ ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])
This describes the translation from LTL to TGBA used by =ltl2tgba=
and =ltl2tgta=.
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 6c1c5d79e..b843ff41e 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1460,13 +1460,11 @@ SERE.
\0 &\text{else}\\
\end{cases}\\
\sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} &
- \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
+ \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} \\
\sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} &
- \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \\
- \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} &
- \sere{r_1\CONCAT b_1}\AND \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND b_2} \\
- \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} &
- \sere{r_1\FUSION b_1}\AND \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND b_2} \\
+ \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\
+ \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
+ \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}\\
\end{align*}
Starred subformul\ae{} are rewritten in Star Normal
@@ -1582,7 +1580,6 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\
& & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\
\G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\
\G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\
- & & (f\OR u) \W g & \equivEU (f \W g)\OR u \\
\X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\
& & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\
\end{align*}
diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x
index ce7cec939..1198b6e94 100644
--- a/src/bin/man/dstar2tgba.x
+++ b/src/bin/man/dstar2tgba.x
@@ -2,7 +2,7 @@
dstar2tgba \- convert Rabin or Streett automata into Büchi automata
[BIBLIOGRAPHY]
.TP
-1.
+1.
Documents the output format of ltl2dstar.
@@ -28,5 +28,15 @@ dstar2tgba implements this for the Rabin case only. In other words,
translating a deterministic Rabin automaton with dstar2tgba will
produce a deterministic TGBA or BA if such a automaton exists.
+.TP
+4.
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata. Proceedings of FORTE'14.
+LNCS 8461.
+
+Explains the SAT-based minimization techniques that can be used (on
+request only) by dstar2tgba to minimize deterministic Büchi automata.
+
+
[SEE ALSO]
.BR spot-x (7)
diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 986e3a63d..3df465814 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -85,11 +85,22 @@ If you would like to give a reference to this tool in an article,
we suggest you cite one of the following papers:
.TP
\(bu
-Alexandre Duret-Lutz: LTL translation improvements in Spot. Proceedings of VECoS'11.
+Alexandre Duret-Lutz: LTL translation improvements in Spot 1.0.
+Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
.TP
\(bu
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
Proceedings of ATVA'13. LNCS 8172.
+.TP
+\(bu
+Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
+and Jan Strejček: Compositional approach to suspension and other
+improvements to LTL translation. Proceedings of SPIN'13. LNCS 7976.
+.TP
+\(bu
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata. Proceedings of FORTE'14.
+LNCS 8461.
[SEE ALSO]
.BR spot-x (7)
diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc
index 3be50e8e6..7a1ab2a2f 100644
--- a/src/bin/spot-x.cc
+++ b/src/bin/spot-x.cc
@@ -1,6 +1,5 @@
-
// -*- coding: utf-8 -*-
-// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -70,10 +69,20 @@ a non-accepting SCC.") },
{ DOC("degen-lcache", "If non-zero (the default), whenever the \
degeneralization algorithm enters an SCC on a state that has already \
been associated to a level elsewhere, it should reuse that level. \
-The \"lcache\" stands for \"level cache\".") },
+Different values can be used to select which level to reuse: 1 always \
+uses the first level seen, 2 uses the minimum level seen so far, and \
+3 uses the maximum level seen so far. The \"lcache\" stands for \
+\"level cache\".") },
{ DOC("degen-order", "If non-zero, the degeneralization algorithm \
will compute one degeneralization order for each SCC it processes. \
This is currently disabled by default.") },
+ { DOC("degen-lskip", "If non-zero (the default), the degeneralization \
+algorithm will skip as much levels as possible for each transition. This \
+is enabled by default as it very often reduce the number of resulting \
+states. A consequence of skipping levels is that the degeneralized \
+automaton tends to have smaller cycles around the accepting states. \
+Disabling skipping will produce automata with large cycles, and often \
+with more states.") },
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
simulation. Set to 3 to iterate both direct and reverse simulations. \
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index ddeefe970..ab2a8d3aa 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -140,7 +140,7 @@ namespace spot
/// \brief construct a formula without the nth child.
///
- /// If the formula \c f is a|b|c|d and d
+ /// If the formula \c f is a|b|c|d and c
/// is child number 2, then calling f->all_but(2) will
/// return a new formula a|b|d.
const formula* all_but(unsigned n) const;
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index a9b5905f9..99ae46cfe 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@@ -68,7 +68,7 @@ main(int argc, char** argv)
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
return 2;
- int exit_code;
+ int exit_code = 0;
{
#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
@@ -112,6 +112,14 @@ main(int argc, char** argv)
const spot::ltl::formula* tmp;
tmp = f1;
f1 = simp.simplify(f1);
+
+ if (!simp.are_equivalent(f1, tmp))
+ {
+ std::cerr << "Source and simplified formulae are not equivalent!\n";
+ std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+ exit_code = 1;
+ }
+
tmp->destroy();
}
spot::ltl::dump(std::cout, f1);
@@ -124,6 +132,14 @@ main(int argc, char** argv)
const spot::ltl::formula* tmp;
tmp = f1;
f1 = simp.simplify(f1);
+
+ if (!simp.are_equivalent(f1, tmp))
+ {
+ std::cerr << "Source and simplified formulae are not equivalent!\n";
+ std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+ exit_code = 1;
+ }
+
tmp->destroy();
}
spot::ltl::dump(std::cout, f1);
@@ -136,13 +152,21 @@ main(int argc, char** argv)
const spot::ltl::formula* tmp;
tmp = f1;
f1 = simp.simplify(f1);
+
+ if (!simp.are_equivalent(f1, tmp))
+ {
+ std::cerr << "Source and simplified formulae are not equivalent!\n";
+ std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+ exit_code = 1;
+ }
+
tmp->destroy();
}
spot::ltl::dump(std::cout, f1);
std::cout << std::endl;
#endif
- exit_code = f1 != f2;
+ exit_code |= f1 != f2;
#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
spot::ltl::ltl_simplifier simp;
@@ -150,8 +174,11 @@ main(int argc, char** argv)
if (!simp.are_equivalent(f1, f2))
{
- std::cerr << "Source and destination formulae are not equivalent!"
- << std::endl;
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
+ std::cerr << "Source and destination formulae are not equivalent!\n";
+#else
+ std::cerr << "Simpl. and destination formulae are not equivalent!\n";
+#endif
exit_code = 1;
}
diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test
index 195322795..304e3c903 100755
--- a/src/ltltest/eventuniv.test
+++ b/src/ltltest/eventuniv.test
@@ -1,7 +1,7 @@
#! /bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+# Developpement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -48,7 +48,7 @@ check 'a U (b | Fc)' '(a U b) | Fc'
check 'a W (b | Fc)' '(a W b) | Fc'
check 'a U (b & GFc)' '(a U b) & GFc'
check 'a W (b & GFc)' 'a W (b & GFc)' # Unchanged
-check '(a | Gc) W g' '(a W g) | Gc'
+check '(a | Gc) W g' '(a | Gc) W g' # Unchanged
check '(a | Gc) U g' '(a | Gc) U g' # Unchanged
check '(a & GFc) M b' '(a M b) & GFc'
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 0068be820..cfa5de45c 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,7 +1,7 @@
#! /bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-# et Developpement de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+# Recherche et Developpement de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
@@ -317,9 +317,10 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
'{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
- run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
- run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
- run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
+ run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
+ run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
+ run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced
+ run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced
run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
'{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
@@ -347,6 +348,8 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x '{s[*]}<>->b' 'b M s'
run 0 $x '{s[+]}<>->b' 'b M s'
run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
+ run 0 $x '{1:a*}!' 'a'
+ run 0 $x '{(1;1):a*}!' 'Xa'
run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 178374b52..e3b6d018d 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2068,7 +2068,6 @@ namespace spot
// (a W (b|e)) = (a W b)|e
// (a U (b&q)) = (a U b)&q
// ((a&q) M b) = (a M b)&q
- // ((a|u) W b) = u|(a W b)
// (a R (b&u)) = (a R b)&u
// (a M (b&u)) = (a M b)&u
if (opt_.favor_event_univ)
@@ -2092,24 +2091,6 @@ namespace spot
b2->destroy();
delete s.res_Event;
}
- if (op == binop::W)
- if (const multop* mo = is_Or(a))
- {
- a->clone();
- mospliter s(mospliter::Split_Univ, mo, c_);
- const formula* a2 =
- multop::instance(multop::Or, s.res_other);
- if (a2 != a)
- {
- a->destroy();
- s.res_Univ->push_back(binop::instance(op, a2, b));
- result_ = recurse_destroy
- (multop::instance(multop::Or, s.res_Univ));
- return;
- }
- a2->destroy();
- delete s.res_Univ;
- }
if (op == binop::U)
if (const multop* mo = is_And(b))
{
@@ -3438,22 +3419,14 @@ namespace spot
if (op == multop::Concat)
{
head1->push_back(h->clone());
- multop::vec* tail = new multop::vec;
- unsigned s = f->size();
- for (unsigned j = 1; j < s; ++j)
- tail->push_back(f->nth(j)->clone());
- tail1->push_back(multop::instance(op, tail));
+ tail1->push_back(f->all_but(0));
i->destroy();
i = 0;
}
else if (op == multop::Fusion)
{
head2->push_back(h->clone());
- multop::vec* tail = new multop::vec;
- unsigned s = f->size();
- for (unsigned j = 1; j < s; ++j)
- tail->push_back(f->nth(j)->clone());
- tail2->push_back(multop::instance(op, tail));
+ tail2->push_back(f->all_but(0));
i->destroy();
i = 0;
}
@@ -3516,20 +3489,14 @@ namespace spot
if (op == multop::Concat)
{
tail3->push_back(t->clone());
- multop::vec* head = new multop::vec;
- for (unsigned j = 0; j < s; ++j)
- head->push_back(f->nth(j)->clone());
- head3->push_back(multop::instance(op, head));
+ head3->push_back(f->all_but(s));
i->destroy();
i = 0;
}
else if (op == multop::Fusion)
{
tail4->push_back(t->clone());
- multop::vec* head = new multop::vec;
- for (unsigned j = 0; j < s; ++j)
- head->push_back(f->nth(j)->clone());
- head4->push_back(multop::instance(op, head));
+ head4->push_back(f->all_but(s));
i->destroy();
i = 0;
}
@@ -4127,6 +4094,8 @@ namespace spot
// head1 tail1
// {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2}
// head2 tail2
+ // BEWARE: The second rule is correct only when
+ // both r1 and r2 do not accept [*0].
multop::vec* head1 = new multop::vec;
multop::vec* tail1 = new multop::vec;
@@ -4146,22 +4115,20 @@ namespace spot
if (op == multop::Concat)
{
head1->push_back(h->clone());
- multop::vec* tail = new multop::vec;
- unsigned s = f->size();
- for (unsigned j = 1; j < s; ++j)
- tail->push_back(f->nth(j)->clone());
- tail1->push_back(multop::instance(op, tail));
+ tail1->push_back(f->all_but(0));
i->destroy();
i = 0;
}
else if (op == multop::Fusion)
{
+ const formula* t = f->all_but(0);
+ if (t->accepts_eword())
+ {
+ t->destroy();
+ continue;
+ }
head2->push_back(h->clone());
- multop::vec* tail = new multop::vec;
- unsigned s = f->size();
- for (unsigned j = 1; j < s; ++j)
- tail->push_back(f->nth(j)->clone());
- tail2->push_back(multop::instance(op, tail));
+ tail2->push_back(t);
i->destroy();
i = 0;
}
@@ -4201,82 +4168,6 @@ namespace spot
delete tail2;
}
- // {r1;b1}&{r2;b2} = {r1&r2};{b1∧b2}
- // head3 tail3
- // {r1:b1}&{r2:b2} = {r1&r2}:{b1∧b2}
- // head4 tail4
- multop::vec* head3 = new multop::vec;
- multop::vec* tail3 = new multop::vec;
- multop::vec* head4 = new multop::vec;
- multop::vec* tail4 = new multop::vec;
- for (auto& i: *s.res_other)
- {
- if (!i)
- continue;
- if (i->kind() != formula::MultOp)
- continue;
- const multop* f = down_cast(i);
- unsigned s = f->size() - 1;
- const formula* t = f->nth(s);
- if (!t->is_boolean())
- continue;
- multop::type op = f->op();
- if (op == multop::Concat)
- {
- tail3->push_back(t->clone());
- multop::vec* head = new multop::vec;
- for (unsigned j = 0; j < s; ++j)
- head->push_back(f->nth(j)->clone());
- head3->push_back(multop::instance(op, head));
- i->destroy();
- i = 0;
- }
- else if (op == multop::Fusion)
- {
- tail4->push_back(t->clone());
- multop::vec* head = new multop::vec;
- for (unsigned j = 0; j < s; ++j)
- head->push_back(f->nth(j)->clone());
- head4->push_back(multop::instance(op, head));
- i->destroy();
- i = 0;
- }
- else
- {
- continue;
- }
- }
- if (!head3->empty())
- {
- const formula* h =
- multop::instance(multop::AndNLM, head3);
- const formula* t =
- multop::instance(multop::And, tail3);
- const formula* f =
- multop::instance(multop::Concat, h, t);
- s.res_other->push_back(f);
- }
- else
- {
- delete head3;
- delete tail3;
- }
- if (!head4->empty())
- {
- const formula* h =
- multop::instance(multop::AndNLM, head4);
- const formula* t =
- multop::instance(multop::And, tail4);
- const formula* f =
- multop::instance(multop::Fusion, h, t);
- s.res_other->push_back(f);
- }
- else
- {
- delete head4;
- delete tail4;
- }
-
result_ = multop::instance(multop::AndNLM, s.res_other);
// If we altered the formula in some way, process
// it another time.
diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc
index 3fc3cd0a1..4f9fe8964 100644
--- a/src/taalgos/tgba2ta.cc
+++ b/src/taalgos/tgba2ta.cc
@@ -417,35 +417,31 @@ namespace spot
std::stack todo;
const tgba* tgba_ = ta->get_tgba();
- const sba* sba_ = down_cast(tgba_);
- assert(!degeneralized || sba_);
// build Initial states set:
state* tgba_init_state = tgba_->get_init_state();
bdd tgba_condition = tgba_->support_conditions(tgba_init_state);
+ bool is_acc = false;
+ if (degeneralized)
+ {
+ tgba_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
+ it->first();
+ if (!it->done())
+ is_acc = it->current_acceptance_conditions() != bddfalse;
+ delete it;
+ }
+
bdd satone_tgba_condition;
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
atomic_propositions_set_,
bddtrue)) != bddfalse)
{
tgba_condition -= satone_tgba_condition;
- state_ta_explicit* init_state;
- if (degeneralized)
- {
- init_state = new
- state_ta_explicit(tgba_init_state->clone(),
- satone_tgba_condition, true,
- sba_->state_is_accepting(tgba_init_state));
- }
- else
- {
- init_state = new
- state_ta_explicit(tgba_init_state->clone(),
- satone_tgba_condition, true, false);
- }
-
+ state_ta_explicit* init_state = new
+ state_ta_explicit(tgba_init_state->clone(),
+ satone_tgba_condition, true, is_acc);
state_ta_explicit* s = ta->add_state(init_state);
assert(s == init_state);
ta->add_to_initial_states_set(s);
@@ -478,6 +474,17 @@ namespace spot
bdd all_props = bddtrue;
bdd dest_condition;
+
+ bool is_acc = false;
+ if (degeneralized)
+ {
+ tgba_succ_iterator* it = tgba_->succ_iter(tgba_state);
+ it->first();
+ if (!it->done())
+ is_acc = it->current_acceptance_conditions() != bddfalse;
+ delete it;
+ }
+
if (satone_tgba_condition == source->get_tgba_condition())
while ((dest_condition =
bdd_satoneset(all_props,
@@ -485,21 +492,9 @@ namespace spot
!= bddfalse)
{
all_props -= dest_condition;
- state_ta_explicit* new_dest;
- if (degeneralized)
- {
- new_dest = new state_ta_explicit
- (tgba_state->clone(),
- dest_condition,
- false,
- sba_->state_is_accepting(tgba_state));
- }
- else
- {
- new_dest = new state_ta_explicit
- (tgba_state->clone(),
- dest_condition, false, false);
- }
+ state_ta_explicit* new_dest =
+ new state_ta_explicit(tgba_state->clone(),
+ dest_condition, false, is_acc);
state_ta_explicit* dest = ta->add_state(new_dest);
if (dest != new_dest)
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index a25d579fe..27ca17c3f 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -25,6 +25,7 @@
#include "ltlast/constant.hh"
#include
#include
+#include
#include "tgbaalgos/scc.hh"
#include "tgba/bddprint.hh"
@@ -174,7 +175,7 @@ namespace spot
public:
unsigned
- next_level(bdd all, int slevel, bdd acc)
+ next_level(bdd all, int slevel, bdd acc, bool skip_levels)
{
bdd temp = acc;
if (all != found_)
@@ -200,7 +201,11 @@ namespace spot
acc = temp;
unsigned next = slevel;
while (next < order_.size() && bdd_implies(order_[next], acc))
- ++next;
+ {
+ ++next;
+ if (!skip_levels)
+ break;
+ }
return next;
}
@@ -223,16 +228,18 @@ namespace spot
{
bdd all_;
std::map orders_;
+ bool skip_levels_;
public:
- scc_orders(bdd all): all_(all)
+ scc_orders(bdd all, bool skip_levels):
+ all_(all), skip_levels_(skip_levels)
{
}
unsigned
next_level(int scc, int slevel, bdd acc)
{
- return orders_[scc].next_level(all_, slevel, acc);
+ return orders_[scc].next_level(all_, slevel, acc, skip_levels_);
}
void
@@ -247,7 +254,7 @@ namespace spot
sba*
degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
- bool use_lvl_cache)
+ int use_lvl_cache, bool skip_levels)
{
bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
@@ -290,7 +297,7 @@ namespace spot
}
// Initialize scc_orders
- scc_orders orders(a->all_acceptance_conditions());
+ scc_orders orders(a->all_acceptance_conditions(), skip_levels);
// Make sure we always use the same pointer for identical states
// from the input automaton.
@@ -312,7 +319,7 @@ namespace spot
tr_cache_t tr_cache;
// State level cache
- typedef std::map lvl_cache_t;
+ typedef std::map lvl_cache_t;
lvl_cache_t lvl_cache;
// Compute SCCs in order to use any optimization.
@@ -342,7 +349,11 @@ namespace spot
s.second = orders.next_level(m.initial(), s.second, acc);
else
while (s.second < order.size() && bdd_implies(order[s.second], acc))
- ++s.second;
+ {
+ ++s.second;
+ if (!skip_levels)
+ break;
+ }
}
#ifdef DEGEN_DEBUG
@@ -479,7 +490,8 @@ namespace spot
// }
if (is_scc_acc)
{
- // If lvl_cache is used and switching SCCs, use level from cache
+ // If lvl_cache is used and switching SCCs, use level
+ // from cache
if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end())
{
@@ -520,10 +532,17 @@ namespace spot
// Consider both the current acceptance
// sets, and the acceptance sets common to
// the outgoing transitions of the
- // destination state.
- while (next < order.size()
- && bdd_implies(order[next], acc))
- ++next;
+ // destination state. But don't do
+ // that if the state is accepting and we
+ // are not skipping levels.
+ if (skip_levels || !is_acc)
+ while (next < order.size()
+ && bdd_implies(order[next], acc))
+ {
+ ++next;
+ if (!skip_levels)
+ break;
+ }
d.second = next;
}
}
@@ -547,8 +566,23 @@ namespace spot
ds2num[d] = dest;
todo.push_back(d);
// Insert new state to cache
- if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end())
- lvl_cache[d.first] = d.second;
+
+ if (use_lvl_cache)
+ {
+ std::pair res =
+ lvl_cache.insert(lvl_cache_t::value_type(d.first,
+ d.second));
+
+ if (!res.second)
+ {
+ if (use_lvl_cache == 3)
+ res.first->second =
+ std::max(res.first->second, d.second);
+ else if (use_lvl_cache == 2)
+ res.first->second =
+ std::min(res.first->second, d.second);
+ }
+ }
}
state_explicit_number::transition*& t =
diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh
index f3354cac2..c67528bed 100644
--- a/src/tgbaalgos/degen.hh
+++ b/src/tgbaalgos/degen.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@@ -44,7 +44,9 @@ namespace spot
/// default because our benchmarks show that it usually does more
/// harm than good). If \a use_lvl_cache is set, everytime an SCC
/// is entered on a state that as already been associated to some
- /// level elsewhere, reuse that level).
+ /// level elsewhere, reuse that level (set it to 2 to keep the
+ /// smallest number, 3 to keep the largest level, and 1 to keep the
+ /// first level found).
///
/// Any of these three options will cause the SCCs of the automaton
/// \a a to be computed prior to its actual degeneralization.
@@ -53,7 +55,8 @@ namespace spot
SPOT_API sba*
degeneralize(const tgba* a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
- bool use_lvl_cache = true);
+ int use_lvl_cache = 1,
+ bool skip_levels = true);
}
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 173436a6e..53d5136b1 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -913,11 +913,12 @@ namespace spot
}
- if (dest->kind() != formula::Constant)
+ // If the destination is not 0 or [*0], it means it
+ // can have successors. Fusion the tail and append
+ // anything to concatenate.
+ if (dest->kind() != formula::Constant
+ || dest == ltl::constant::true_instance())
{
- // If the destination is not a constant, it
- // means it can have successors. Fusion the
- // tail and append anything to concatenate.
const formula* dest2 =
multop::instance(multop::Fusion, dest, tail->clone());
if (to_concat_)
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index 0c2be1410..e7d6e6d3c 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -39,15 +39,16 @@ namespace spot
postprocessor::postprocessor(const option_map* opt)
: type_(TGBA), pref_(Small), level_(High),
degen_reset_(true), degen_order_(false), degen_cache_(true),
- simul_(-1), scc_filter_(-1), ba_simul_(-1), tba_determinisation_(false),
- sat_minimize_(0), sat_acc_(0), sat_states_(0), state_based_(false),
- wdba_minimize_(true)
+ degen_lskip_(true), simul_(-1), scc_filter_(-1), ba_simul_(-1),
+ tba_determinisation_(false), sat_minimize_(0), sat_acc_(0),
+ sat_states_(0), state_based_(false), wdba_minimize_(true)
{
if (opt)
{
degen_order_ = opt->get("degen-order", 0);
degen_reset_ = opt->get("degen-reset", 1);
degen_cache_ = opt->get("degen-lcache", 1);
+ degen_lskip_ = opt->get("degen-lskip", 1);
simul_ = opt->get("simul", -1);
simul_limit_ = opt->get("simul-limit", -1);
scc_filter_ = opt->get("scc-filter", -1);
@@ -116,7 +117,8 @@ namespace spot
const tgba* d = degeneralize(a,
degen_reset_,
degen_order_,
- degen_cache_);
+ degen_cache_,
+ degen_lskip_);
delete a;
if (ba_simul_ <= 0)
return d;
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index 693089b42..52b812ec0 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -110,7 +110,8 @@ namespace spot
// Fine-tuning options fetched from the option_map.
bool degen_reset_;
bool degen_order_;
- bool degen_cache_;
+ int degen_cache_;
+ bool degen_lskip_;
int simul_;
int simul_limit_;
int scc_filter_;
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 025752996..ac2ed5a9b 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -99,6 +99,7 @@ TESTS = \
ltl2neverclaim.test \
ltl2neverclaim-lbtt.test \
ltl2ta.test \
+ ltl2ta2.test \
ltlprod.test \
bddprod.test \
explprod.test \
@@ -110,6 +111,7 @@ TESTS = \
dupexp.test \
degendet.test \
degenid.test \
+ degenlskip.test \
kv.test \
lbttparse.test \
scc.test \
diff --git a/src/tgbatest/degenlskip.test b/src/tgbatest/degenlskip.test
new file mode 100755
index 000000000..3836d2cb5
--- /dev/null
+++ b/src/tgbatest/degenlskip.test
@@ -0,0 +1,70 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013, 2014 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 .
+
+. ./defs
+
+set -e
+
+# Make sure degen-skip=0 and degen-skip=1 produce the expected
+# automata for 'GFa & GFb'
+
+../../bin/ltl2tgba -B 'GFa & GFb' > out1
+../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' > out2
+../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' > out3
+
+diff out1 out2
+cmp out2 out3 && exit 1
+
+cat <expected2
+digraph G {
+ 0 [label="", style=invis, height=0]
+ 0 -> 1
+ 1 [label="0", peripheries=2]
+ 1 -> 1 [label="a & b\n{Acc[1]}"]
+ 1 -> 2 [label="!a & b\n{Acc[1]}"]
+ 1 -> 3 [label="!b\n{Acc[1]}"]
+ 2 [label="1"]
+ 2 -> 1 [label="a\n"]
+ 2 -> 2 [label="!a\n"]
+ 3 [label="2"]
+ 3 -> 1 [label="a & b\n"]
+ 3 -> 2 [label="!a & b\n"]
+ 3 -> 3 [label="!b\n"]
+}
+EOF
+
+
+cat <expected3
+digraph G {
+ 0 [label="", style=invis, height=0]
+ 0 -> 1
+ 1 [label="0", peripheries=2]
+ 1 -> 2 [label="1\n{Acc[1]}"]
+ 2 [label="1"]
+ 2 -> 3 [label="b\n"]
+ 2 -> 2 [label="!b\n"]
+ 3 [label="2"]
+ 3 -> 1 [label="a\n"]
+ 3 -> 3 [label="!a\n"]
+}
+EOF
+
+diff out2 expected2
+diff out3 expected3
diff --git a/src/tgbatest/ltl2ta2.test b/src/tgbatest/ltl2ta2.test
new file mode 100755
index 000000000..eed0c9739
--- /dev/null
+++ b/src/tgbatest/ltl2ta2.test
@@ -0,0 +1,27 @@
+#!/bin/sh
+# Copyright (C) 2014 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 .
+
+
+. ./defs
+
+set -e
+
+# This used to trigger an assert because of BA simulation not
+# returning an instance of spot::sba.
+run 0 ../../bin/ltl2tgta --ta 'G(F(a U b) U (c M d))'
diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test
index b21e589d0..6150ac722 100755
--- a/src/tgbatest/ltlcross2.test
+++ b/src/tgbatest/ltlcross2.test
@@ -38,6 +38,7 @@ ltl2tgba=../../bin/ltl2tgba
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
+"$ltl2tgba --lbtt --ba -x degen-skip=0 --lbtt %f >%T" \
"$ltl2tgba --lbtt --ba --high %f > %T" \
"$ltl2tgba --lbtt -BDC %f > %T" \
"$ltl2tgba --lbtt -BC %f > %T" \