From 139f7b49b48a0896f8105f57ce2d6f71237781c5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 May 2014 20:06:43 +0200 Subject: [PATCH 01/24] snf: Fix the handling of bounded repetition. star_normal_form() used to be called under bounded repetitions like [*0..4], but some of these rewritings are only correct for [*0..]. For instance (a*|1)[*] can be rewritten to 1[*] but (a*|1)[*0..1] cannot be rewritten to 1[*0..1] it would be correct to rewrite the latter as (a[+]|1)[*0..1], canceling the empty word in a*. Also (a*;b*)[*] can be rewritten to (a|b)[*] but (a*;b*)[*0..1] cannot be rewritten to (a|b)[*0..1] and it cannot either be rewritten to (a[+]|b[+])[*0..1]. This patch introduces a new function to implement rewritings under bounded repetition. * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded): New function. * src/ltlvisit/simplify.cc: Use it. * src/ltltest/reduccmp.test: Add tests. * doc/tl/tl.tex: Document the rewritings implemented. --- doc/tl/tl.tex | 44 ++++++++++++++++++++++++------- src/ltltest/reduccmp.test | 3 +++ src/ltlvisit/simplify.cc | 23 +++++++++++++++- src/ltlvisit/snf.cc | 55 ++++++++++++++++++++++++++++++++------- src/ltlvisit/snf.hh | 8 ++++-- 5 files changed, 112 insertions(+), 21 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b843ff41e..784f204b2 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1469,27 +1469,53 @@ SERE. Starred subformul\ae{} are rewritten in Star Normal Form~\cite{bruggeman.96.tcs} with: -\[r\STAR{\mvar{0}..\mvar{j}} \equiv r^\circ\STAR{\mvar{0}..\mvar{j}} \] +\[r\STAR{} \equiv r^\circ\STAR{} \] where $r^\circ$ is recursively defined as follows: \begin{align*} r^\circ &= r\text{~if~} \varepsilon\not\VDash r \\ \eword^\circ &= \0 & (r_1\CONCAT r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\ - r\STAR{\mvar{0}..\mvar{j}}^\circ &= r^\circ & + r\STAR{\mvar{i}..\mvar{j}}^\circ &= r^\circ \text{~if~} i=0 \text{~or~} \varepsilon\VDash r& (r_1\AND r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\ (r_1\OR r_2)^\circ &= r_1^\circ \OR r_2^\circ & (r_1\ANDALT r_2)^\circ &= r_1 \ANDALT r_2 \end{align*} Note: the original SNF definition~\cite{bruggeman.96.tcs} does not -include \samp{$\FUSION$}, \samp{$\AND$}, and \samp{$\ANDALT$} -operators, and it guarantees that $\forall r,\,\varepsilon\not\VDash -r^\circ$ because $r^\circ$ is stripping all the stars and empty words -that occur in $r$. For instance $\sere{a\STAR{}\CONCAT - b\STAR{}\CONCAT\sere{\1\OR c}}^\circ\STAR{} = \sere{a\OR b\OR +include \samp{$\AND$} and \samp{$\ANDALT$} operators, and it +guarantees that $\forall r,\,\varepsilon\not\VDash r^\circ$ because +$r^\circ$ is stripping all the stars and empty words that occur in +$r$. For instance $\sere{a\STAR{}\CONCAT + b\STAR{}\CONCAT\sere{\eword\OR c}}^\circ\STAR{} = \sere{a\OR b\OR c}\STAR{}$. Our extended definition still respects this property in -presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but -unfortunately not when the \samp{$\ANDALT$} operator is used. +presence of \samp{$\AND$} operators, but unfortunately not when the +\samp{$\ANDALT$} operator is used. + +We extend the above definition to bounded repetitions with: +\begin{align*} + r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{\0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}} +\end{align*} +where $r^\square$ is recursively defined as follows: +\begin{align*} + r^\square &= r\text{~if~} \varepsilon\not\VDash r \\ + \eword^\square &= \0 & + (r_1\CONCAT r_2)^\square &= r_1\CONCAT r_2\\ + r\STAR{\mvar{i}..\mvar{j}}^\square &= r^\square\STAR{\mvar{\max(1,i)}..\mvar{j}} \text{~if~} i=0 \text{~or~} \varepsilon\VDash r & + (r_1\AND r_2)^\square &= r_1^\square\OR r_2^\square \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\ + (r_1\OR r_2)^\square &= r_1^\square \OR r_2^\square & + (r_1\ANDALT r_2)^\square &= r_1 \ANDALT r_2 +\end{align*} +The differences between $^\square$ and $^\circ$ are in the handling +of $r\STAR{\mvar{i}..\mvar{j}}$ and in the handling of $r_1\CONCAT r_2$. + +% Indeed $(c\STAR{}\OR\1)\STAR{0..1}$ is not equivalent to +% $(c\STAR{}\OR\1)^\circ\STAR{0..1}\equiv(c\OR\1)\STAR{0..1}\equiv +% 1\STAR{0..1}$ but to +% $(c\STAR{}\OR\1)^\square\STAR{0..1}\equiv(c\PLUS{}\OR\1)\STAR{0..1}$. + +% Similarly $(a\STAR{}\CONCAT b\STAR{})\STAR{0..1})$ is definitely not +% equal to $(a\PLUS{}\OR b\PLUS{})\STAR{0..1}). + \subsubsection{Basic Simplifications SERE-LTL Binding Operators} diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index cfa5de45c..0ff861728 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -364,6 +364,9 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)' run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)' run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc' + run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v' + run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v' + run 0 $x '{{b*&c*}[*3..5]}<>-> v' '{{b[+]|c[+]}[*0..5]} <>-> v' # not reduced run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \ diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 88c93c5be..6625ab8f9 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -106,6 +106,16 @@ namespace spot old->first->destroy(); } } + { + snf_cache::iterator i = snfb_cache_.begin(); + snf_cache::iterator end = snfb_cache_.end(); + while (i != end) + { + snf_cache::iterator old = i++; + old->second->destroy(); + old->first->destroy(); + } + } { f2f_map::iterator i = bool_isop_.begin(); f2f_map::iterator end = bool_isop_.end(); @@ -387,6 +397,13 @@ namespace spot return ltl::star_normal_form(f, &snf_cache_); } + const formula* + star_normal_form_bounded(const formula* f) + { + return ltl::star_normal_form_bounded(f, &snfb_cache_); + } + + const formula* boolean_to_isop(const formula* f) { @@ -406,6 +423,7 @@ namespace spot f2f_map nenoform_; syntimpl_cache_t syntimpl_; snf_cache snf_cache_; + snf_cache snfb_cache_; f2f_map bool_isop_; }; @@ -1081,7 +1099,10 @@ namespace spot min = 0; if (min == 0) { - const formula* s = c_->star_normal_form(h); + const formula* s = + bo->max() == bunop::unbounded ? + c_->star_normal_form(h) : + c_->star_normal_form_bounded(h); h->destroy(); h = s; } diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index 35447316f..ab7619c72 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Developpement +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -31,6 +31,7 @@ namespace spot // E° class snf_visitor: public visitor { + protected: const formula* result_; snf_cache* cache_; public: @@ -144,21 +145,50 @@ namespace spot if (!f->accepts_eword()) return f->clone(); - if (cache_) - { - snf_cache::const_iterator i = cache_->find(f); - if (i != cache_->end()) - return i->second->clone(); - } + snf_cache::const_iterator i = cache_->find(f); + if (i != cache_->end()) + return i->second->clone(); f->accept(*this); - if (cache_) - (*cache_)[f->clone()] = result_->clone(); + (*cache_)[f->clone()] = result_->clone(); return result_; } }; + // E^â–¡ + class snf_visitor_bounded: public snf_visitor + { + public: + snf_visitor_bounded(snf_cache* c): snf_visitor(c) + { + } + + void + visit(const bunop* bo) + { + bunop::type op = bo->op(); + switch (op) + { + case bunop::Star: + assert(bo->accepts_eword()); + result_ = bunop::instance(bunop::Star, + recurse(bo->child()), + std::max(bo->min(), 1U), + bo->max()); + break; + } + } + + void + visit(const multop* mo) + { + if (mo->op() == multop::Concat) + result_ = mo->clone(); + else + this->snf_visitor::visit(mo); + } + }; } @@ -169,5 +199,12 @@ namespace spot return v.recurse(sere); } + const formula* + star_normal_form_bounded(const formula* sere, snf_cache* cache) + { + snf_visitor_bounded v(cache); + return v.recurse(sere); + } + } } diff --git a/src/ltlvisit/snf.hh b/src/ltlvisit/snf.hh index 391f40309..4906f73a6 100644 --- a/src/ltlvisit/snf.hh +++ b/src/ltlvisit/snf.hh @@ -1,6 +1,6 @@ // -*- 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. // @@ -52,6 +52,10 @@ namespace spot /// \param cache an optional cache SPOT_API const formula* star_normal_form(const formula* sere, snf_cache* cache = 0); + + /// A variant of star_normal_form() for r[*0..j] where j < ω. + SPOT_API const formula* + star_normal_form_bounded(const formula* sere, snf_cache* cache = 0); } } From 8315cad6dbbe13f930bb91e7dec7cb3d9269381d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 May 2014 21:24:38 +0200 Subject: [PATCH 02/24] * src/ltltest/equals.cc: Fix style. --- src/ltltest/equals.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 99ae46cfe..f359d2584 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -116,7 +116,7 @@ main(int argc, char** argv) 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"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n'; exit_code = 1; } @@ -136,7 +136,7 @@ main(int argc, char** argv) 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"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n'; exit_code = 1; } @@ -156,7 +156,7 @@ main(int argc, char** argv) 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"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << '\n'; exit_code = 1; } From a4934c4f71c6bff405c274f8aa7e21ba69cd6e3d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 17 May 2014 15:13:35 +0200 Subject: [PATCH 03/24] * NEWS: Mention recent fix. --- NEWS | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index f41560a51..e2f767453 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 1.2.4a (not yet released) - Nothing yet. + * Bug fixes: + + - Fix simplification of bounded repetition in SERE formulas. New in spot 1.2.4 (2014-05-15) From 6c76ba408ec78b01cadde6ae8fcd83b3af29d71f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 29 May 2014 15:48:31 +0200 Subject: [PATCH 04/24] neverparse: Fix parsing of Modella's neverclaims. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by FrantiÅ¡ek Blahoudek. * src/neverparse/neverclaimparse.yy: Fix. * src/tgbatest/neverclaimread.test: Test it. * NEWS: Mention the fix. --- NEWS | 1 + src/neverparse/neverclaimparse.yy | 4 ++-- src/tgbatest/neverclaimread.test | 38 +++++++++++++++++++++++++++++-- 3 files changed, 39 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index e2f767453..289c3ef2f 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,7 @@ New in spot 1.2.4a (not yet released) * Bug fixes: - Fix simplification of bounded repetition in SERE formulas. + - Fix parsing of neverclaims produced by Modella. New in spot 1.2.4 (2014-05-15) diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 8d32440b8..6e915b600 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +** Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et ** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -191,7 +191,7 @@ transitions: } -formula: FORMULA | "false" { $$ = new std::string("0"); } +formula: FORMULA | IDENT | "false" { $$ = new std::string("0"); } opt_dest: /* empty */ diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 3e75a715e..06d0b3c7c 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -172,6 +172,40 @@ EOF grep input: stderr >> stderrfilt diff stderrfilt expected + +# This output from MoDeLLa was not property parsed by Spot because of +# the missing parentheses around p0. Report from FrantiÅ¡ek Blahoudek. +cat >input < goto T1 + :: p0 -> goto T2 + fi; +T1: + if + :: true -> goto T1 + :: p0 -> goto accept_T3 + fi; +T2: + if + :: p0 -> goto accept_T3 + fi; +accept_T3: + if + :: p0 -> goto T2 + fi; +} +EOF +cat >expected< output +diff output expected + + cat >formulae< Date: Mon, 28 Apr 2014 10:59:55 +0200 Subject: [PATCH 05/24] org: Prevent a race on the buildfarm. * doc/org/init.el.in (org-publish-timestamp-directory): Use a build directory, not $HOME. --- doc/org/init.el.in | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 572bd100a..a0bb373e4 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -8,6 +8,9 @@ ; the .org-timestamp directory does not always exist, is not always ; created by org, and that causes issues on our buildfarm. (setq org-publish-use-timestamps-flag nil) +;; The default value of writing to ~/.org-timestamps causes race +;; conditions when doing concurrent builds. +(setq org-publish-timestamp-directory "@abs_top_builddir@/.org-timestamps/") (setq org-babel-python-command "/usr/bin/python3") (org-babel-do-load-languages From c7da4003a7c1a8d9b9d7a863dde52a626483e5bb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Jul 2014 16:22:56 +0200 Subject: [PATCH 06/24] * src/tgba/taatgba.cc: Fix a memory leak. --- src/tgba/taatgba.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 1e60bca84..a80bdbb2d 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -275,6 +275,8 @@ namespace spot && (i == seen_.end() || j == i->second.end())) { seen_[b].push_back(t); + if (i != seen_.end()) + delete b; succ_.push_back(t); } else From d4e3a9521be47963606dc6b6d2e0cc1ba867c3cf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Aug 2014 00:18:54 +0200 Subject: [PATCH 07/24] [buddy] Fix a harmless uninitialized read. This can only cause failure when running under valgrind (i.e., in the test suite), but is not a problem in practice as the test is certain to fail the entry->c check whenever entry->b is uninitialized. * src/bddop.c (bdd_implies): Here. --- buddy/src/bddop.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index bb79c7838..314459da5 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -917,7 +917,8 @@ int bdd_implies(BDD l, BDD r) return 0; entry = BddCache_lookup(&misccache, IMPLIESHASH(l,r)); - if (entry->a == l && entry->b == r && entry->c == CACHEID_IMPLIES) + // Check entry->b last, because not_rec() does not initialize it. + if (entry->a == l && entry->c == CACHEID_IMPLIES && entry->b == r) { #ifdef CACHESTATS bddcachestats.opHit++; @@ -1758,7 +1759,7 @@ static BDD simplify_rec(BDD f, BDD d) entry = BddCache_lookup(&applycache, APPLYHASH(f,d,bddop_simplify)); - // Check entry->c last, because not_rec() does not initialize it. + // Check entry->b last, because not_rec() does not initialize it. if (entry->a == f && entry->c == bddop_simplify && entry->b == d) { #ifdef CACHESTATS From e5124faa13e1856e58bc9038515896d9f8f51b0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Aug 2014 14:52:51 +0200 Subject: [PATCH 08/24] man: more doc about TGBA and monitors This was prompted by an exchange of emails with Caroline Lemieux. * src/bin/man/ltl2tgba.x: Add notes and references. * NEWS, THANKS: Update. --- NEWS | 5 +++ THANKS | 1 + src/bin/man/ltl2tgba.x | 71 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 76 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 289c3ef2f..f8378d199 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 1.2.4a (not yet released) + * Documentation + + - The man page for ltl2tgba has some new notes and references + about TGBA and about monitors. + * Bug fixes: - Fix simplification of bounded repetition in SERE formulas. diff --git a/THANKS b/THANKS index 66d9e0a81..89d52b874 100644 --- a/THANKS +++ b/THANKS @@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or suggestions. Akim Demaille +Caroline Lemieux Christian Dax Ernesto Posse Étienne Renault diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index 3df465814..a26430c7d 100644 --- a/src/bin/man/ltl2tgba.x +++ b/src/bin/man/ltl2tgba.x @@ -1,5 +1,42 @@ [NAME] ltl2tgba \- translate LTL/PSL formulas into Büchi automata +[NOTE ON TGBA] + +TGBA stands for Transition-based Generalized Büchi Automaton. The +name was coined by Dimitra Giannakopoulou and Flavio Lerda in their +FORTE'02 paper (From States to Transitions: Improving Translation of +LTL Formulae to Büchi Automata), although similar automata have been +used under different names long before that. + +As its name implies a TGBA uses a generalized Büchi acceptance +condition, meanings that a run of the automaton is accepted iff it +visits ininitely often multiple acceptance sets, and it also uses +transition-based acceptance, i.e., those acceptance sets are sets of +transitions. TGBA are often more consise than traditional Büchi +automata. For instance the LTL formula \f(CWGFa & GFb\fR can be +translated into a single-state TGBA while a traditional Büchi +automaton would need 3 states. Compare + + % ltl2tgba 'GFa & GFb' + +with + + % ltl2tgba --ba 'GFa & GFb' + +In the dot output produced by the above commands, the membership of +the transitions to the various acceptance sets is denoted using names +in braces. The actuall names do not really matter as they may be +produced by the translation algorithm or altered by any latter +postprocessing. + +When the \fB\--ba\fR option is used to request a Büchi automaton, Spot +builds a TGBA with a single acceptance set, and in which for any state +either all outgoing transitions are accepting (this is equivalent to +the state being accepting) or none of them are. Double circles are +used to highlight accepting states in the output, but the braces +denoting the accepting transitions are still shown because the +underling structure really is a TGBA. + [NOTE ON LBTT'S FORMAT] The format, described at http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html, @@ -10,7 +47,7 @@ internally, it will normally use the transition-based flavor of that format, indicated with a 't' flag after the number of acceptance sets. For instance: - % bin/ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2' + % ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2' 2 2t // 2 states, 2 transition-based acceptance sets 0 1 // state 0: initial 0 -1 t // trans. to state 0, no acc., label: true @@ -80,6 +117,38 @@ p[0-9]+ as double-quoted strings. 0 -1 & ! "b" ! "a" -1 +[NOTE ON GENERATING MONITORS] + +The monitors generated with option \fB\-M\fR are finite state automata +used to reject finite words that cannot be extended to infinite words +compatible with the supplied formula. The idea is that the monitor +should progress alongside the system, and can only make decisions +based on the finite prefix read so far. + +Monitors can be seen as Büchi automata in which all recognized runs are +accepting. As such, the only infinite words they can reject are those +are not recognized, i.e., infinite words that start with a bad prefix. + +Because of this limited expressiveness, a monitor for some given LTL +or PSL formula may accept a larger language than the one specified by +the formula. For instance a monitor for the LTL formula \f(CWa U b\fR +will reject (for instance) any word starting with \f(CW!a&!b\fR as +there is no way such a word can validate the formula, but it will not +reject a finite prefix repeating only \f(CWa&!b\fR as such a prefix +could be extented in a way that is comptible with \f(CWa U b\fR. + +For more information about monitors, we refer the readers to the +following two papers (the first paper describes the construction of +the second paper in a more concise way): +.TP +\(bu +Deian Tabakov and Moshe Y. Vardi: Optimized Temporal Monitors for SystemC. +Proceedings of RV'10. LNCS 6418. +.TP +\(bu +Marcelo d’Amorim and Grigoire RoÅŸu: Efficient monitoring of +ω-languages. Proceedings of CAV'05. LNCS 3576. + [BIBLIOGRAPHY] If you would like to give a reference to this tool in an article, we suggest you cite one of the following papers: From e7dc62e3c8e50a3c8071dc31dd69fb6223de0b08 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 Aug 2014 14:57:35 +0200 Subject: [PATCH 09/24] * NEWS: Add more news. --- NEWS | 3 +++ 1 file changed, 3 insertions(+) diff --git a/NEWS b/NEWS index f8378d199..70ce8d566 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,9 @@ New in spot 1.2.4a (not yet released) - Fix simplification of bounded repetition in SERE formulas. - Fix parsing of neverclaims produced by Modella. + - Fix a memory leak in the little-used conversion from + transition-based alternating automata to tgba. + - Fix a harmless uninitialized read in BuDDy. New in spot 1.2.4 (2014-05-15) From 795c2f17202ce5878bb62279a01ce8d1c22d3292 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Aug 2014 20:52:18 +0200 Subject: [PATCH 10/24] ltl2tgba_fm: Fix incorrect simplification of promises for M The bug was reported by Joachim Klein. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable): Reduce P(a M b) to P(a & b), not to P(a). * src/tgbatest/ltlcross.test: Test Joachim's formula. * src/tgbatest/ltl2ta.test: Adjust some expected values. * NEWS: Mention the bug. --- NEWS | 4 ++ src/tgbaalgos/ltl2tgba_fm.cc | 87 ++++++++++++++++++++++++++++-------- src/tgbatest/ltl2ta.test | 38 ++++++++-------- src/tgbatest/ltlcross.test | 14 +++--- 4 files changed, 99 insertions(+), 44 deletions(-) diff --git a/NEWS b/NEWS index 70ce8d566..8afde42a5 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,10 @@ New in spot 1.2.4a (not yet released) * Bug fixes: + - Fix incorrect simplification of promises in the translation + of the M operator (you may suffer from the bug even if you do + not use this operator as some LTL patterns are automatically + reduced to it). - Fix simplification of bounded repetition in SERE formulas. - Fix parsing of neverclaims produced by Modella. - Fix a memory leak in the little-used conversion from diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index a972cb12c..48c108f8b 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -254,24 +254,59 @@ namespace spot // Similarly // a M b = (a R (b&P(a))) // (a M b) M c = (a R (b & Pa)) R (c & P(a M b)) - // = (a R (b & Pa)) R (c & P(a)) - // The rules also apply to F: - // P(F(a)) = P(a) - again: - while (const binop* b = is_binop(f)) + // = (a R (b & Pa)) R (c & P(a & b)) + // + // The code below therefore implement the following + // rules: + // P(a U b) = P(b) + // P(F(a)) = P(a) + // P(a M b) = P(a & b) + // + // The latter rule INCORRECTLY appears as P(a M b)=P(a) + // in section 3.5 of + // "LTL translation improvements in Spot 1.0", + // A. Duret-Lutz. IJCCBS 5(1/2):31-54, March 2014. + // and was unfortunately implemented this way until Spot + // 1.2.4. A counterexample is given by the formula + // G(Fa & ((a M b) U ((c U !d) M d))) + // that was found by Joachim Klein. Here P((c U !d) M d) + // and P(c U !d) should not both be simplified to P(!d). + for (;;) { - binop::type op = b->op(); - if (op == binop::U) - f = b->second(); - else if (op == binop::M) - f = b->first(); + if (const binop* b = is_binop(f)) + { + binop::type op = b->op(); + if (op == binop::U) + { + // P(a U b) = P(b) + f = b->second(); + } + else if (op == binop::M) + { + // P(a M b) = P(a & b) + const formula* g = + multop::instance(multop::And, + b->first()->clone(), + b->second()->clone()); + int num = dict->register_acceptance_variable(g, this); + a_set &= bdd_ithvar(num); + g->destroy(); + return num; + } + else + { + break; + } + } + else if (const unop* u = is_unop(f, unop::F)) + { + // P(F(a)) = P(a) + f = u->child(); + } else - break; - } - if (const unop* u = is_unop(f, unop::F)) - { - f = u->child(); - goto again; + { + break; + } } int num = dict->register_acceptance_variable(f, this); a_set &= bdd_ithvar(num); @@ -1521,9 +1556,23 @@ namespace spot { res_ = recurse(node->second(), recurring_); bdd f1 = recurse(node->first()); - // r(f1 M f2) = r(f2)(r(f1) + a(f1)X(f1 M f2)) if not recurring - // r(f1 M f2) = r(f2)(r(f1) + a(f1)) if recurring - bdd a = bdd_ithvar(dict_.register_a_variable(node->first())); + // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2)X(f1 M f2)) if not recurring + // r(f1 M f2) = r(f2)(r(f1) + a(f1&f2)) if recurring + // + // Note that the rule above differs from the one given + // in Figure 2 of + // "LTL translation improvements in Spot 1.0", + // A. Duret-Lutz. IJCCBS 5(1/2):31-54, March 2014. + // Both rules should be OK, but this one is a better fit + // to the promises simplifications performed in + // register_a_variable() (see comments in this function). + // We do not want a U (c M d) to generate two different + // promises. Generating c&d also makes the output similar + // to what we would get with the equivalent a U (d U (c & d)). + // + // Here we just appear to emit a(f1 M f2) and the conversion + // to a(f1&f2) is done by register_a_variable(). + bdd a = bdd_ithvar(dict_.register_a_variable(node)); if (!recurring_) a &= bdd_ithvar(dict_.register_next_variable(node)); res_ &= f1 | a; diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 7690aeaba..a2f8030dd 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -133,46 +133,46 @@ grep 'states: 21$' stdout f="FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" run 0 ../ltl2tgba -TA -RT -ks -in -R3f -x -DS "$f" >stdout -grep 'transitions: 450$' stdout -grep 'states: 38$' stdout +grep 'transitions: 505$' stdout +grep 'states: 40$' stdout run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x -DS "$f" >stdout -grep 'transitions: 551$' stdout -grep 'states: 40$' stdout +grep 'transitions: 616$' stdout +grep 'states: 42$' stdout run 0 ../ltl2tgba -TA -RT -ks "$f" >stdout -grep 'transitions: 424$' stdout -grep 'states: 31$' stdout +grep 'transitions: 498$' stdout +grep 'states: 34$' stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv -in "$f" >stdout -grep 'transitions: 485$' stdout -grep 'states: 32$' stdout +grep 'transitions: 566$' stdout +grep 'states: 35$' stdout run 0 ../ltl2tgba -TA -RT -ks -in -R3 -x -DS "$f" >stdout -grep 'transitions: 450$' stdout -grep 'states: 38$' stdout +grep 'transitions: 505$' stdout +grep 'states: 40$' stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv -R3 -x -DS "$f" >stdout -grep 'transitions: 551$' stdout -grep 'states: 40$' stdout +grep 'transitions: 616$' stdout +grep 'states: 42$' stdout run 0 ../ltl2tgba -TA -ks -sp -lv -DS "$f" >stdout -grep 'transitions: 597$' stdout -grep 'states: 46$' stdout +grep 'transitions: 819$' stdout +grep 'states: 56$' stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv "$f" >stdout -grep 'transitions: 504$' stdout -grep 'states: 33$' stdout +grep 'transitions: 585$' stdout +grep 'states: 36$' stdout run 0 ../ltl2tgba -TGTA -RT -ks "$f" >stdout -grep 'transitions: 527$' stdout -grep 'states: 32$' stdout +grep 'transitions: 598$' stdout +grep 'states: 35$' stdout g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" diff --git a/src/tgbatest/ltlcross.test b/src/tgbatest/ltlcross.test index 38bcf0015..b8fb882ba 100755 --- a/src/tgbatest/ltlcross.test +++ b/src/tgbatest/ltlcross.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013 Laboratoire de Recherche et +# 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. @@ -23,7 +23,13 @@ set -e ltl2tgba=../ltl2tgba -../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | + +( +# A bug reported by Joachim Klein +echo 'G(Fa & ((a M b) U ((c U !d) M d)))' +# Random formulas +../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 +) | ../../bin/ltlcross --products=2 \ "$ltl2tgba -t -l %f > %T" \ "$ltl2tgba -t -l -R3b -r4 %f > %T" \ @@ -47,7 +53,3 @@ ltl2tgba=../ltl2tgba "$ltl2tgba -t -taa -r4 %f > %T" \ "$ltl2tgba -t -taa -r4 -c %f > %T" \ "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T" - -# Disabled because too slow, and too big automata produced. -# "$ltl2tgba -t -lo -r4 %f > %T" -# "$ltl2tgba -t -lo -R3b -r4 %f > %T" \ From e78548ebae4ed7ceb8df8cc705496fae6918c0ab Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Aug 2014 21:29:57 +0200 Subject: [PATCH 11/24] ltlcross: display formulas in blue instead of white So that people using white-background terminal can still read them... Reported by Joachim Klein. * src/bin/ltlcross.cc: Adjust. * NEWS: Mention it. --- NEWS | 5 +++++ src/bin/ltlcross.cc | 8 ++++---- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index 8afde42a5..2c6cd84ab 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,11 @@ New in spot 1.2.4a (not yet released) - Fix a memory leak in the little-used conversion from transition-based alternating automata to tgba. - Fix a harmless uninitialized read in BuDDy. + - When writing to the terminal, ltlcross used to display each + formula in bright white, to make them stand out. It turns out + this was actually hiding the formulas for people using a + terminal with white background... This version displays formula + in bright blue instead. New in spot 1.2.4 (2014-05-15) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 137def2ba..b776d02e9 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.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. // @@ -187,7 +187,7 @@ ARGMATCH_VERIFY(color_args, color_types); color_type color_opt = color_if_tty; const char* bright_red = "\033[01;31m"; -const char* bright_white = "\033[01;37m"; +const char* bright_blue = "\033[01;34m"; const char* bright_yellow = "\033[01;33m"; const char* reset_color = "\033[m"; @@ -1244,7 +1244,7 @@ namespace if (filename || linenum) std::cerr << " "; if (color_opt) - std::cerr << bright_white; + std::cerr << bright_blue; std::cerr << fstr << "\n"; if (color_opt) std::cerr << reset_color; From e997676c3e7d03e695025e2d2ad9bc222a1102b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Aug 2014 21:40:51 +0200 Subject: [PATCH 12/24] Support LBT formula in ltl2tgba.html. Suggested by Joachim Klein. * wrap/python/ajax/spot.in: Try parse_lbt() when parse() fails. * NEWS: Mention it. --- NEWS | 8 +++++++- wrap/python/ajax/spot.in | 14 ++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 2c6cd84ab..a6fbca306 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,12 @@ New in spot 1.2.4a (not yet released) - * Documentation + * New feature: + + - The online ltl2tgba translator will automatically attempt to + parse a formula using LBT's syntax if it cannot parse it using + the normal infix syntax. + + * Documentation: - The man page for ltl2tgba has some new notes and references about TGBA and about monitors. diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 2057f9a48..c396baa5a 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -1,6 +1,6 @@ #!@PYTHON@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +# Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -405,9 +405,15 @@ pel = spot.empty_parse_error_list() f = spot.parse(formula, pel, env) if pel: - unbufprint('
') - err = spot.format_parse_errors(spot.get_cout(), formula, pel) - unbufprint('
') + # Try the LBT parser in case someone is throwing LBT formulas at us. + pel2 = spot.empty_parse_error_list() + g = spot.parse_lbt(formula, pel2, env) + if pel2: + unbufprint('
') + err = spot.format_parse_errors(spot.get_cout(), formula, pel) + unbufprint('
') + else: + f = g # Do not continue if we could not parse anything sensible. if not f: From 310a98c15a597e4a99f5d9216bb381e060238fc4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 1 Jun 2014 19:44:43 +0200 Subject: [PATCH 13/24] hoaf: first implementation of the HOA Format output. The specifications are at http://adl.github.io/hoaf/ * src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/tgbatest/ltl2tgba.cc: Add option to output HOA. * NEWS: Mention it. --- NEWS | 8 +- src/bin/dstar2tgba.cc | 19 +- src/bin/ltl2tgba.cc | 19 +- src/tgbaalgos/Makefile.am | 6 +- src/tgbaalgos/hoaf.cc | 366 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/hoaf.hh | 66 +++++++ src/tgbatest/ltl2tgba.cc | 17 +- 7 files changed, 489 insertions(+), 12 deletions(-) create mode 100644 src/tgbaalgos/hoaf.cc create mode 100644 src/tgbaalgos/hoaf.hh diff --git a/NEWS b/NEWS index a6fbca306..5d4844a5e 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,17 @@ New in spot 1.2.4a (not yet released) - * New feature: + * New features: - The online ltl2tgba translator will automatically attempt to parse a formula using LBT's syntax if it cannot parse it using the normal infix syntax. + - ltl2tgba and dstar2tgba have a new experimental option --hoaf to + output automata in the Hanoï Omega Automaton Format whose + current draft is at http://adl.github.io/hoaf/ + The corresponding C++ function is spot::hoaf_reachable() in + tgbaalgos/hoaf.hh. + * Documentation: - The man page for ltl2tgba has some new notes and references diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 1b4b92038..f877423c6 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -35,6 +35,7 @@ #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" @@ -72,6 +73,10 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + "Output the automaton in HOA format. Add letters to select " + "(s) state-based acceptance, (t) transition-based acceptance, " + "(m) mixed acceptance, (l) single-line output", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, @@ -122,9 +127,10 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; bool utf8 = false; const char* stats = ""; +const char* hoaf_opt = 0; spot::option_map extra_options; static int @@ -142,6 +148,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'F': jobs.push_back(job(arg, true)); break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; case 'M': type = spot::postprocessor::Monitor; break; @@ -340,6 +350,9 @@ namespace case Lbtt_t: spot::lbtt_reachable(std::cout, aut, false); break; + case Hoa: + spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n'; + break; case Spot: spot::tgba_save_reachable(std::cout, aut); break; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index c81db4331..7e49cbedc 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.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,6 +39,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/save.hh" +#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/translate.hh" #include "tgba/bddprint.hh" @@ -72,6 +73,10 @@ static const argp_option options[] = { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format " "for use in CSV file", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + "Output the automaton in HOA format. Add letters to select " + "(s) state-based acceptance, (t) transition-based acceptance, " + "(m) mixed acceptance, (l) single-line output", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, @@ -118,9 +123,10 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; bool utf8 = false; const char* stats = ""; +const char* hoaf_opt = 0; spot::option_map extra_options; static int @@ -136,6 +142,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; case 'M': type = spot::postprocessor::Monitor; break; @@ -255,6 +265,9 @@ namespace case Lbtt_t: spot::lbtt_reachable(std::cout, aut, false); break; + case Hoa: + spot::hoaf_reachable(std::cout, aut, hoaf_opt, f) << '\n'; + break; case Spot: spot::tgba_save_reachable(std::cout, aut); break; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index cb710ffc3..811165958 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -## Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +## de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -44,6 +44,7 @@ tgbaalgos_HEADERS = \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ + hoaf.hh \ isdet.hh \ isweakscc.hh \ lbtt.hh \ @@ -92,6 +93,7 @@ libtgbaalgos_la_SOURCES = \ eltl2tgba_lacim.cc \ emptiness.cc \ gv04.cc \ + hoaf.cc \ isdet.cc \ isweakscc.cc \ lbtt.cc \ diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc new file mode 100644 index 000000000..80eb8f3fe --- /dev/null +++ b/src/tgbaalgos/hoaf.cc @@ -0,0 +1,366 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). +// Copyright (C) 2003, 2004 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 . + +#include +#include +#include +#include "tgba/tgba.hh" +#include "tgba/sba.hh" +#include "hoaf.hh" +#include "reachiter.hh" +#include "misc/escape.hh" +#include "misc/bddlt.hh" +#include "misc/minato.hh" +#include "tgba/formula2bdd.hh" +#include "ltlvisit/tostring.hh" + +namespace spot +{ + namespace + { + struct metadata + { + // Assign a number to each atomic proposition. + typedef std::map ap_map; + ap_map ap; + typedef std::vector vap_t; + vap_t vap; + + // Assign a number to each acceptance condition. + typedef std::map acc_map; + acc_map acc; + + // Map each state to a number. + typedef Sgi::hash_map state_map; + state_map sm; + // Map each number to its states. + typedef std::vector number_map; + number_map nm; + + std::vector common_acc; + bool state_acc; + bool is_complete; + bool is_deterministic; + + // Label support: the set of all conditions occurring in the + // automaton. + typedef std::map sup_map; + sup_map sup; + + metadata(const tgba* aut) + : state_acc(true), is_complete(true), is_deterministic(true) + { + number_all_acc(aut); + number_all_states_and_fill_sup(aut); + number_all_ap(); + } + + void number_all_acc(const tgba* aut) + { + bdd all_acc = aut->all_acceptance_conditions(); + unsigned count = 0; + while (all_acc != bddfalse) + { + bdd one = bdd_satone(all_acc); + all_acc -= one; + acc[one] = count++; + } + } + + std::ostream& + emit_acc(std::ostream& os, bdd b) + { + // FIXME: We could use a cache for this. + if (b == bddfalse) + return os; + os << " {"; + bool notfirst = false; + while (b != bddfalse) + { + bdd one = bdd_satone(b); + b -= one; + if (notfirst) + os << ' '; + else + notfirst = true; + os << acc[one]; + } + os << '}'; + return os; + } + + void number_all_states_and_fill_sup(const tgba* aut) + { + std::string empty; + + // Scan the whole automaton to number states. + std::deque todo; + + const state* init = aut->get_init_state(); + sm[init] = 0; + nm.push_back(init); + todo.push_back(init); + + while (!todo.empty()) + { + tgba_succ_iterator* i = aut->succ_iter(todo.front()); + todo.pop_front(); + bdd prev = bddtrue; + bool st_acc = true; + bdd sum = bddfalse; + bdd available = bddtrue; + for (i->first(); !i->done(); i->next()) + { + const state* dst = i->current_state(); + bdd cond = i->current_condition(); + if (is_complete) + sum |= cond; + if (is_deterministic) + { + if (!bdd_implies(cond, available)) + is_deterministic = false; + else + available -= cond; + } + sup.insert(std::make_pair(cond, empty)); + if (sm.insert(std::make_pair(dst, nm.size())).second) + { + nm.push_back(dst); + todo.push_back(dst); + } + else + { + dst->destroy(); + } + if (st_acc) + { + bdd acc = i->current_acceptance_conditions(); + if (prev != bddtrue && prev != acc) + st_acc = false; + else + prev = acc; + } + } + if (is_complete) + is_complete &= sum == bddtrue; + + common_acc.push_back(st_acc); + state_acc &= st_acc; + delete i; + } + } + + void number_all_ap() + { + sup_map::iterator i; + bdd all = bddtrue; + for (i = sup.begin(); i != sup.end(); ++i) + all &= bdd_support(i->first); + + while (all != bddtrue) + { + int v = bdd_var(all); + all = bdd_high(all); + ap.insert(std::make_pair(v, vap.size())); + vap.push_back(v); + } + + for (i = sup.begin(); i != sup.end(); ++i) + { + bdd cond = i->first; + if (cond == bddtrue) + { + i->second = "t"; + continue; + } + if (cond == bddfalse) + { + i->second = "f"; + continue; + } + std::ostringstream s; + bool notfirstor = false; + + minato_isop isop(cond); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + if (notfirstor) + s << " | "; + bool notfirstand = false; + while (cube != bddtrue) + { + if (notfirstand) + s << '&'; + else + notfirstand = true; + bdd h = bdd_high(cube); + if (h == bddfalse) + { + s << '!' << ap[bdd_var(cube)]; + cube = bdd_low(cube); + } + else + { + s << ap[bdd_var(cube)]; + cube = h; + } + } + notfirstor = true; + } + i->second = s.str(); + } + } + + }; + + } + + + std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* aut, + const ltl::formula* f, + hoaf_acceptance acceptance, + hoaf_alias alias, + bool newline) + { + (void) alias; + + metadata md(aut); + + if (acceptance == Hoaf_Acceptance_States + && !md.state_acc) + acceptance = Hoaf_Acceptance_Transitions; + + unsigned num_states = md.nm.size(); + + const char nl = newline ? '\n' : ' '; + os << "HOA: v1" << nl; + if (f) + escape_str(os << "name: \"", to_string(f)) << '"' << nl; + os << "States: " << num_states << nl + << "Start: 0" << nl + << "AP: " << md.vap.size(); + bdd_dict* d = aut->get_dict(); + for (metadata::vap_t::const_iterator i = md.vap.begin(); + i != md.vap.end(); ++i) + escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"'; + os << nl; + unsigned num_acc = md.acc.size(); + if (num_acc == 0) + os << "acc-name: all"; + else if (num_acc == 1) + os << "acc-name: Buchi"; + else + os << "acc-name: generalized-Buchi " << num_acc; + os << nl; + os << "Acceptance: " << num_acc; + if (num_acc > 0) + { + os << " I(0"; + for (unsigned i = 1; i < num_acc; ++i) + os << ")&I(" << i; + os << ')'; + } + else + { + os << " t"; + } + os << nl; + os << "properties: trans-labels explicit-labels"; + if (acceptance == Hoaf_Acceptance_States) + os << " state-acc"; + else if (acceptance == Hoaf_Acceptance_Transitions) + os << " trans-acc"; + if (md.is_complete) + os << " complete"; + if (md.is_deterministic) + os << " deterministic"; + os << nl; + os << "--BODY--" << nl; + for (unsigned i = 0; i < num_states; ++i) + { + hoaf_acceptance this_acc = acceptance; + if (this_acc == Hoaf_Acceptance_Mixed) + this_acc = (md.common_acc[i] ? + Hoaf_Acceptance_States : Hoaf_Acceptance_Transitions); + + tgba_succ_iterator* j = aut->succ_iter(md.nm[i]); + j->first(); + + os << "State: " << i; + if (this_acc == Hoaf_Acceptance_States && !j->done()) + md.emit_acc(os, j->current_acceptance_conditions()); + os << nl; + + for (; !j->done(); j->next()) + { + const state* dst = j->current_state(); + os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst]; + if (this_acc == Hoaf_Acceptance_Transitions) + md.emit_acc(os, j->current_acceptance_conditions()); + os << nl; + dst->destroy(); + } + delete j; + } + os << "--END--"; // No newline. Let the caller decide. + for (unsigned i = 0; i < num_states; ++i) + md.nm[i]->destroy(); + return os; + } + + std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* aut, + const char* opt, + const ltl::formula* f) + { + bool newline = true; + hoaf_acceptance acceptance = Hoaf_Acceptance_States; + hoaf_alias alias = Hoaf_Alias_None; + + if (opt) + while (*opt) + { + switch (*opt++) + { + case 'l': + newline = false; + break; + case 'm': + acceptance = Hoaf_Acceptance_Mixed; + break; + case 's': + acceptance = Hoaf_Acceptance_States; + break; + case 't': + acceptance = Hoaf_Acceptance_Transitions; + break; + } + } + return hoaf_reachable(os, aut, f, acceptance, alias, newline); + } + +} diff --git a/src/tgbaalgos/hoaf.hh b/src/tgbaalgos/hoaf.hh new file mode 100644 index 000000000..4fe83cbc2 --- /dev/null +++ b/src/tgbaalgos/hoaf.hh @@ -0,0 +1,66 @@ +// -*- coding: utf-8 -*- +// 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 . + +#ifndef SPOT_TGBAALGOS_HOAF_HH +# define SPOT_TGBAALGOS_HOAF_HH + +#include +#include "ltlast/formula.hh" + +namespace spot +{ + class tgba; + enum hoaf_alias { Hoaf_Alias_None, Hoaf_Alias_Ap, Hoaf_Alias_Cond }; + enum hoaf_acceptance + { + Hoaf_Acceptance_States, /// state-based acceptance if + /// (globally) possible + /// transition-based acceptance + /// otherwise. + Hoaf_Acceptance_Transitions, /// transition-based acceptance globally + Hoaf_Acceptance_Mixed /// mix state-based and transition-based + }; + + /// \ingroup tgba_io + /// \brief Print reachable states in Hanoi Omega Automata format. + /// + /// \param os The output stream to print on. + /// \param g The automaton to output. + /// \param f The (optional) formula associated to the automaton. If given + /// it will be output as a comment. + /// \parama acceptance Force the type of acceptance mode used + /// in output. + /// \param alias Whether aliases should be used in output. + /// \param newslines Whether to use newlines in output. + SPOT_API std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* g, + const ltl::formula* f = 0, + hoaf_acceptance acceptance = Hoaf_Acceptance_States, + hoaf_alias alias = Hoaf_Alias_None, + bool newlines = true); + + SPOT_API std::ostream& + hoaf_reachable(std::ostream& os, + const tgba* g, + const char* opt, + const ltl::formula* f = 0); +} + +#endif // SPOT_TGBAALGOS_HOAF_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7ab4c93a0..4f6739d70 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. @@ -37,6 +37,7 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasgba.hh" #include "tgbaalgos/degen.hh" @@ -403,6 +404,7 @@ main(int argc, char** argv) bool containment = false; bool show_fc = false; bool spin_comments = false; + const char* hoaf_opt = 0; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba* system_aut = 0; @@ -581,6 +583,11 @@ main(int argc, char** argv) accepting_run = true; graph_run_tgba_opt = true; } + else if (!strncmp(argv[formula_index], "-H", 2)) + { + output = 17; + hoaf_opt = argv[formula_index] + 2; + } else if (!strcmp(argv[formula_index], "-k")) { output = 9; @@ -1883,7 +1890,11 @@ main(int argc, char** argv) } break; } - + case 17: + { + hoaf_reachable(std::cout, a, hoaf_opt, f) << '\n'; + break; + } default: assert(!"unknown output option"); } From 44fc323e7b83e3994e2b8992beb6fb8d251fc57f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 13:17:18 +0200 Subject: [PATCH 14/24] randltl: accept a number of atomic propositions Suggested by Joachim Klein. * src/bin/randltl.cc: Implement it. * src/ltltest/rand.test: Test it. * doc/org/randltl.org, NEWS: Document it. --- NEWS | 2 ++ doc/org/randltl.org | 25 +++++++++++++++++-------- src/bin/randltl.cc | 43 +++++++++++++++++++++++++++++++++++++++---- src/ltltest/rand.test | 26 ++++++++++++++++++++++++++ 4 files changed, 84 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 5d4844a5e..c1956b8fe 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,8 @@ New in spot 1.2.4a (not yet released) The corresponding C++ function is spot::hoaf_reachable() in tgbaalgos/hoaf.hh. + - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'. + * Documentation: - The man page for ltl2tgba has some new notes and references diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 7faa12176..a795331f5 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -19,6 +19,15 @@ randltl a b c Note that the result does not always use all atomic propositions. +If you do not care about how the atomic propositions are named, +you can give a nonnegative number instead: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl 3 +#+END_SRC +#+RESULTS: +: G(Gp1 W (Gp1 M p2)) + The syntax of the formula output can be changed using the [[file:ioltl.org][common output options]]: @@ -40,16 +49,16 @@ like =p0=, =p1=, etc... (Atomic proposition named differently will be output by Spot in double-quotes, but this is not supported by LBT.) #+BEGIN_SRC sh :results verbatim :exports both -randltl -l p1 p2 p3 -randltl -8 p1 p2 p3 -randltl -s p1 p2 p3 -randltl --wring p1 p2 p3 +randltl -l 3 +randltl -8 3 +randltl -s 3 +randltl --wring 3 #+END_SRC #+RESULTS: -: G W G p2 M G p2 p3 -: □(□p2 W (□p2 M p3)) -: []((p3 U (p3 && []p2)) V ([]p2 || (p3 U (p3 && []p2)))) -: (G(((p3=1) U ((p3=1) * (G(p2=1)))) R ((G(p2=1)) + ((p3=1) U ((p3=1) * (G(p2=1))))))) +: G W G p1 M G p1 p2 +: □(□p1 W (□p1 M p2)) +: []((p2 U (p2 && []p1)) V ([]p1 || (p2 U (p2 && []p1)))) +: (G(((p2=1) U ((p2=1) * (G(p1=1)))) R ((G(p1=1)) + ((p2=1) U ((p2=1) * (G(p1=1))))))) As you might guess from the above result, for a given set of atomic propositions (and on the same computer) the generated formula will diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index b3730f31d..d32cd7d19 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -44,13 +44,19 @@ #include "misc/hash.hh" const char argp_program_doc[] ="\ -Generate random temporal logic formulas.\v\ +Generate random temporal logic formulas.\n\n\ +The formulas are built over the atomic propositions named by PROPS...\n\ +or, if N is a nonnegative number, using N arbitrary names.\v\ Examples:\n\ \n\ The following generates 10 random LTL formulas over the propositions a, b,\n\ and c, with the default tree-size, and all available operators.\n\ % randltl -n10 a b c\n\ \n\ +If you do not mind about the name of the atomic propositions, just give\n\ +a number instead:\n\ + % ./randltl -n10 3\n\ +\n\ You can disable or favor certain operators by changing their priority.\n\ The following disables xor, implies, and equiv, and multiply the probability\n\ of X to occur by 10.\n\ @@ -139,6 +145,7 @@ static int opt_seed = 0; static range opt_tree_size = { 15, 15 }; static bool opt_unique = true; static bool opt_wf = false; +static bool ap_count_given = false; void remove_some_props(spot::ltl::atomic_prop_set& s) @@ -185,7 +192,7 @@ to_int(const char* s) } static int -parse_opt(int key, char* arg, struct argp_state*) +parse_opt(int key, char* arg, struct argp_state* as) { // This switch is alphabetically-ordered. switch (key) @@ -236,6 +243,32 @@ parse_opt(int key, char* arg, struct argp_state*) opt_wf = true; break; case ARGP_KEY_ARG: + // If this is the unique non-option argument, it can + // be a number of atomic propositions to build. + // + // argp reorganizes argv[] so that options always come before + // non-options. So if as->argc == as->next we know this is the + // last non-option argument, and if aprops.empty() we know this + // is the also the first one. + if (aprops.empty() && as->argc == as->next) + { + char* endptr; + int res = strtol(arg, &endptr, 10); + if (!*endptr && res >= 0) // arg is a number + { + ap_count_given = true; + spot::ltl::default_environment& e = + spot::ltl::default_environment::instance(); + for (int i = 0; i < res; ++i) + { + std::ostringstream p; + p << 'p' << i; + aprops.insert(static_cast + (e.require(p.str()))); + } + break; + } + } aprops.insert(static_cast (spot::ltl::default_environment::instance().require(arg))); break; @@ -250,7 +283,7 @@ main(int argc, char** argv) { setup(argv); - const argp ap = { options, parse_opt, "PROP...", argp_program_doc, + const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc, children, 0, 0 }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) @@ -340,7 +373,9 @@ main(int argc, char** argv) exit(0); } - if (aprops.empty()) + // running 'randltl 0' is one way to generate formulas using no + // atomic propositions so do not complain in that case. + if (aprops.empty() && !ap_count_given) error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", program_name); diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test index b7750582c..59a0ad660 100755 --- a/src/ltltest/rand.test +++ b/src/ltltest/rand.test @@ -97,3 +97,29 @@ c EOF diff expected out2 + + +# atomic proposition can be implicitly specified using a number +$randltl -n 1000 3 --tree-size=10..20 > out +grep -q p0 out +grep -q p1 out +grep -q p2 out +grep p3 out && exit 1 + + +# We should be able to generate exactly two formulas with 0 atomic +# propositions. +run 0 $randltl -n2 0 | sort > out +cat >expected < out +grep -q '"0"' out +grep -q '"1"' out From 2227ad60cf4335492fdd0584d48de9609c2f5203 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 13:23:36 +0200 Subject: [PATCH 15/24] randltl: do not reset the seed between formulas Reported by Joachim Klein. * src/bin/randltl.cc: Here. * NEWS: Mention the fix. --- NEWS | 4 ++++ src/bin/randltl.cc | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index c1956b8fe..d061cb4e9 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,10 @@ New in spot 1.2.4a (not yet released) this was actually hiding the formulas for people using a terminal with white background... This version displays formula in bright blue instead. + - 'randltl -n -1 --seed 0' and 'randltl -n -1 --seed 1' used to + generate nearly the same list of formulas, shifted by one, + because the PRNG write reset with an incremented seed between + each output formula. The PRNG is now reset only once. New in spot 1.2.4 (2014-05-15) diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index d32cd7d19..676c044e5 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -379,9 +379,10 @@ main(int argc, char** argv) error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", program_name); + spot::srand(opt_seed); + typedef Sgi::hash_set > fset_t; - fset_t unique_set; spot::ltl::ltl_simplifier simpl(simplifier_options()); @@ -392,7 +393,6 @@ main(int argc, char** argv) unsigned trials = MAX_TRIALS; bool ignore; const spot::ltl::formula* f = 0; - spot::srand(opt_seed++); do { ignore = false; From 829012fe43dd4af38b655db4a8b88c14d30fd6a8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 14:54:29 +0200 Subject: [PATCH 16/24] ltlcross: implement a --save-bogus=FILENAME option Suggested by Joachim Klein. * src/bin/ltlcross.cc: Implement it. * src/tgbatest/ltlcross3.test: Test it. * doc/org/ltlcross.org, NEWS: Document it. --- NEWS | 4 ++ doc/org/ltlcross.org | 30 +++++++++- src/bin/ltlcross.cc | 115 +++++++++++++++++++++++++++++------- src/tgbatest/ltlcross3.test | 12 +++- 4 files changed, 134 insertions(+), 27 deletions(-) diff --git a/NEWS b/NEWS index d061cb4e9..e6b10c458 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,10 @@ New in spot 1.2.4a (not yet released) - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'. + - ltlcross has a new option --save-bogus=FILENAME to save any + formula for which a problem (other than timeout) was detected + during translation or using the resulting automatas. + * Documentation: - The man page for ltl2tgba has some new notes and references diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 34762984d..aff718f97 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -610,9 +610,9 @@ automaton as well. ** =--stop-on-error= -The =--stop-on-error= will cause =ltlcross= to abort on the first -detected error. This include failure to start some translator, read -its output, or failure to passe the sanity checks. Timeouts are +The =--stop-on-error= option will cause =ltlcross= to abort on the +first detected error. This include failure to start some translator, +read its output, or failure to passe the sanity checks. Timeouts are allowed. One use for this option is when =ltlcross= is used in combination with @@ -627,6 +627,30 @@ to remove duplicate formulas will keep growing). randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' #+END_SRC +** =--save-bogus=FILENAME= + +The =--save-bogus=FILENAME= will save any formula for which an error +was detected (either some translation failed, or some problem was +detected using the resulting automata) in =FILENAME=. Again, timeouts +are not considered to be errors, and therefore not reported in this +file. + +The main use for this feature is in conjunction with =randltl='s +generation of random formulas. For instance the following command +will run the translators on an infinite number of formulas, saving +any problematic formula in =bugs.ltl=. + +#+BEGIN_SRC sh :export code :eval no +randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' +#+END_SRC + +You can periodically check the contents of =bugs.ltl=, and then run +=ltlcross= only on those formulas to look at the problems: + +#+BEGIN_SRC sh :export code :eval no +ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' +#+END_SRC + ** =--no-check= The =--no-check= option disables all sanity checks, and only use the supplied diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index b776d02e9..be5f577fc 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -94,6 +94,7 @@ Exit status:\n\ #define OPT_COLOR 10 #define OPT_NOCOMP 11 #define OPT_OMIT 12 +#define OPT_BOGUS 13 static const argp_option options[] = { @@ -159,6 +160,8 @@ static const argp_option options[] = "colorize output; WHEN can be 'never', 'always' (the default if " "--color is used without argument), or " "'auto' (the default if --color is not used)", 0 }, + { "save-bogus", OPT_BOGUS, "FILENAME", 0, + "save formulas for which problems were detected in FILENAME", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -206,6 +209,8 @@ unsigned products = 1; bool products_avg = true; bool opt_omit = false; bool has_sr = false; // Has Streett or Rabin automata to process. +const char* bogus_output_filename = 0; +std::ofstream* bogus_output = 0; struct translator_spec { @@ -509,6 +514,14 @@ parse_opt(int key, char* arg, struct argp_state*) << "on your platform" << std::endl; #endif break; + case OPT_BOGUS: + { + bogus_output = new std::ofstream(arg); + if (!*bogus_output) + error(2, errno, "cannot open '%s'", arg); + bogus_output_filename = arg; + break; + } case OPT_COLOR: { if (arg) @@ -849,7 +862,8 @@ namespace } const spot::tgba* - translate(unsigned int translator_num, char l, statistics_formula* fstats) + translate(unsigned int translator_num, char l, statistics_formula* fstats, + bool& problem) { output.reset(translator_num); @@ -874,11 +888,13 @@ namespace std::cerr << "warning: timeout during execution of command\n"; ++timeout_count; status_str = "timeout"; + problem = false; // A timeout is not a sign of a bug es = -1; } else if (WIFSIGNALED(es)) { status_str = "signal"; + problem = true; es = WTERMSIG(es); global_error() << "error: execution terminated by signal " << es << ".\n"; @@ -888,6 +904,7 @@ namespace { es = WEXITSTATUS(es); status_str = "exit code"; + problem = true; global_error() << "error: execution returned exit code " << es << ".\n"; end_error(); @@ -895,6 +912,7 @@ namespace else { status_str = "ok"; + problem = false; es = 0; switch (output.format) { @@ -906,6 +924,7 @@ namespace if (!pel.empty()) { status_str = "parse error"; + problem = true; es = -1; std::ostream& err = global_error(); err << "error: failed to parse the produced neverclaim.\n"; @@ -923,6 +942,7 @@ namespace if (!f) { status_str = "no output"; + problem = true; es = -1; global_error() << "Cannot open " << output.val() << std::endl; @@ -934,6 +954,7 @@ namespace if (!res) { status_str = "parse error"; + problem = true; es = -1; global_error() << ("error: failed to parse output in " "LBTT format: ") @@ -952,6 +973,7 @@ namespace if (!pel.empty()) { status_str = "parse error"; + problem = true; es = -1; std::ostream& err = global_error(); err << "error: failed to parse the produced DSTAR" @@ -1048,7 +1070,7 @@ namespace } }; - static void + static bool check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j, size_t i, size_t j, bool icomp, bool jcomp) { @@ -1091,9 +1113,10 @@ namespace delete res; delete ec; delete prod; + return res; } - static void + static bool cross_check(const std::vector& maps, char l, unsigned p) { size_t m = maps.size(); @@ -1146,7 +1169,9 @@ namespace else err << "the state-space\n"; end_error(); + return true; } + return false; } typedef std::set state_set; @@ -1212,12 +1237,35 @@ namespace (*i++)->destroy(); } + int + process_string(const std::string& input, + const char* filename, + int linenum) + { + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = parse_formula(input, pel); + + if (!f || !pel.empty()) + { + if (filename) + error_at_line(0, 0, filename, linenum, "parse error:"); + spot::ltl::format_parse_errors(std::cerr, input, pel); + if (f) + f->destroy(); + return 1; + } + int res = process_formula(f, filename, linenum); + + if (res && bogus_output) + *bogus_output << input << std::endl; + return 0; + } + + int process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { - (void) filename; - (void) linenum; static unsigned round = 0; // If we need LBT atomic proposition in any of the input or @@ -1268,6 +1316,9 @@ namespace } } + + int problems = 0; + // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); @@ -1288,7 +1339,10 @@ namespace for (size_t n = 0; n < m; ++n) { - pos[n] = runner.translate(n, 'P', pstats); + bool prob; + pos[n] = runner.translate(n, 'P', pstats, prob); + problems += prob; + // If the automaton is deterministic, compute its complement // as well. Note that if we have computed statistics // already, there is no need to call is_deterministic() @@ -1326,7 +1380,10 @@ namespace for (size_t n = 0; n < m; ++n) { - neg[n] = runner.translate(n, 'N', nstats); + bool prob; + neg[n] = runner.translate(n, 'N', nstats, prob); + problems += prob; + // If the automaton is deterministic, compute its // complement as well. Note that if we have computed // statistics already, there is no need to call @@ -1353,7 +1410,8 @@ namespace for (size_t j = 0; j < m; ++j) if (neg[j]) { - check_empty_prod(pos[i], neg[j], i, j, false, false); + problems += + check_empty_prod(pos[i], neg[j], i, j, false, false); // Deal with the extra complemented automata if we // have some. @@ -1371,13 +1429,18 @@ namespace // translation was not deterministic. if (i != j && comp_pos[j] && !comp_neg[j]) - check_empty_prod(pos[i], comp_pos[j], i, j, false, true); + problems += + check_empty_prod(pos[i], comp_pos[j], + i, j, false, true); if (i != j && comp_neg[i] && !comp_neg[i]) - check_empty_prod(comp_neg[i], neg[j], i, j, true, false); + problems += + check_empty_prod(comp_neg[i], neg[j], + i, j, true, false); if (comp_pos[i] && comp_neg[j] && (i == j || (!comp_neg[i] && !comp_pos[j]))) - check_empty_prod(comp_pos[i], comp_neg[j], - i, j, true, true); + problems += + check_empty_prod(comp_pos[i], comp_neg[j], + i, j, true, true); } } else @@ -1457,14 +1520,16 @@ namespace if (!no_checks) { // cross-comparison test - cross_check(pos_map, 'P', p); - cross_check(neg_map, 'N', p); + problems += cross_check(pos_map, 'P', p); + problems += cross_check(neg_map, 'N', p); // consistency check for (size_t i = 0; i < m; ++i) if (pos_map[i] && neg_map[i] && !(consistency_check(pos_map[i], neg_map[i], statespace))) { + ++problems; + std::ostream& err = global_error(); err << "error: inconsistency between P" << i << " and N" << i; @@ -1507,7 +1572,7 @@ namespace // Shall we stop processing formulas now? abort_run = global_error_flag && stop_on_error; - return 0; + return problems; } }; } @@ -1525,7 +1590,7 @@ print_stats_csv(const char* filename) else { out = outfile = new std::ofstream(filename); - if (!outfile) + if (!*outfile) error(2, errno, "cannot open '%s'", filename); } @@ -1563,7 +1628,7 @@ print_stats_json(const char* filename) else { out = outfile = new std::ofstream(filename); - if (!outfile) + if (!*outfile) error(2, errno, "cannot open '%s'", filename); } @@ -1642,10 +1707,16 @@ main(int argc, char** argv) if (global_error_flag) { std::ostream& err = global_error(); - err << ("error: some error was detected during the above runs,\n" - " please search for 'error:' messages in the above " - "trace.") - << std::endl; + if (bogus_output) + err << ("error: some error was detected during the above runs.\n" + " Check file ") + << bogus_output_filename + << " for problematic formulas."; + else + err << ("error: some error was detected during the above runs,\n" + " please search for 'error:' messages in the above" + " trace."); + err << std::endl; if (timeout_count == 1) err << "Additionally, 1 timeout occurred." << std::endl; else if (timeout_count > 1) @@ -1662,6 +1733,8 @@ main(int argc, char** argv) << " timeouts, but no other problem detected." << std::endl; } + delete bogus_output; + if (json_output) print_stats_json(json_output); if (csv_output) diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test index 386afbe25..2ecfe25fb 100755 --- a/src/tgbatest/ltlcross3.test +++ b/src/tgbatest/ltlcross3.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013 Laboratoire de Recherche et +# 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. @@ -55,13 +55,18 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0 check_csv out.csv # Likewise for timeouts +echo foo >bug run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ - --timeout 2 -f a --csv=out.csv 2>stderr + --timeout 2 -f a --csv=out.csv \ + --save-bogus=bug 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 test `grep '"timeout",-1' out.csv | wc -l` -eq 2 check_csv out.csv +# 'bug' should exist but be empty +test -f bug +test -s bug && exit 1 run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ --timeout 2 --omit-missing -f a --csv=out.csv 2>stderr @@ -115,12 +120,13 @@ test $q -eq `expr $p + 12` # Check with Rabin/Streett output run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ - -f a --csv=out.csv 2>stderr + -f 'X a' --csv=out.csv --save-bogus=bug.txt 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2 test `grep '"exit code",1' out.csv | wc -l` -eq 2 check_csv out.csv +grep 'X a' bug.txt test $q -eq `expr $p + 6` From d9d9837e55350cfb9adec59e01caa2cd182091fd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 15:04:12 +0200 Subject: [PATCH 17/24] * wrap/python/ajax/ltl2tgba.html: Update tooltips. --- wrap/python/ajax/ltl2tgba.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 211f768e8..949cfad06 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -564,11 +564,11 @@ an identifier: aUb is an atomic proposition, unlike
From 85beeec2e4348cef6440d0670677c61975c7315c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 15:18:43 +0200 Subject: [PATCH 18/24] ltl2tgba.html: Add option to output LBT format. Suggested by Joachim Klein. * wrap/python/ajax/ltl2tgba.html: New option. * wrap/python/ajax/protocol.txt, NEWS: Document it. * wrap/python/ajax/spot.in: Implement it. * wrap/python/spot.i: Export src/ltlvisit/lbt.hh. --- NEWS | 3 ++- wrap/python/ajax/ltl2tgba.html | 4 ++++ wrap/python/ajax/protocol.txt | 1 + wrap/python/ajax/spot.in | 7 ++++++- wrap/python/spot.i | 2 ++ 5 files changed, 15 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index e6b10c458..66922d6c7 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,8 @@ New in spot 1.2.4a (not yet released) - The online ltl2tgba translator will automatically attempt to parse a formula using LBT's syntax if it cannot parse it using - the normal infix syntax. + the normal infix syntax. It also has an option to display + formulas using LBT's syntax. - ltl2tgba and dstar2tgba have a new experimental option --hoaf to output automata in the Hanoï Omega Automaton Format whose diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 949cfad06..231e612ec 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -489,6 +489,10 @@ an identifier: aUb is an atomic proposition, unlike text in Spin's syntax
+