diff --git a/NEWS b/NEWS index 5ba383540..6c2724751 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 1.2.4a (not yet released) +New in spot 1.2.5a (not yet released) * Major changes (including backward incompatible changes): @@ -87,6 +87,56 @@ New in spot 1.2.4a (not yet released) automata (when viewed explictely), using the above and non longuer supported tgba_bdd_concrete class. +New in spot 1.2.5 (2014-08-21) + + * 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. 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 + current draft is at http://adl.github.io/hoaf/ + The corresponding C++ function is spot::hoaf_reachable() in + tgbaalgos/hoaf.hh. + + - '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 + about TGBA and about monitors. + + * 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 incorrect translation of PSL formulas of the form !{f} where + f is unsatisifable. A similar bug was fixed for {f} in Spot + 1.1.4, but for some reason it was not fixed for !{f}. + - 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. + - 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. + - '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) * New features: 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/configure.ac b/configure.ac index 5973f62e8..66ae8a1e2 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.4a], [spot@lrde.epita.fr]) +AC_INIT([spot], [1.2.5a], [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/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/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/doc/org/satmin.org b/doc/org/satmin.org index f2f8c394c..a6e8819d7 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -418,17 +418,14 @@ export SPOT_SATLOG=stats.csv ltlfilt -f "Ga R (F!b & (c U b))" -l | ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' -echo cat stats.csv #+END_SRC - #+RESULTS: : input(states=11) output(states=5, acc-sets=2, det=1) -: -: 9,8,35,64,44064,9043076,930,22,290,21 -: 7,7,33,56,14504,2191905,224,4,106,4 -: 6,6,28,48,10512,1358243,137,0,44,1 -: 5,,,,7200,782342,78,1,26,2 +: 9,8,35,64,44064,9043076,978,26,277,21 +: 7,7,33,56,14504,2191905,237,7,113,4 +: 6,6,28,48,10512,1358243,145,4,45,2 +: 5,,,,7200,782342,82,3,31,2 The generated CSV file use the following columns: - the n passed to the SAT-based minimization algorithm diff --git a/doc/org/tools.org b/doc/org/tools.org index 24c937364..26dd29f2b 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,4 +1,4 @@ -#+TITLE: Command-line tools installed by Spot 1.2.4 +#+TITLE: Command-line tools installed by Spot 1.2.5 #+EMAIL spot@lrde.epita.fr #+OPTIONS: H:2 num:nil toc:t diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 5ae92bb79..88b61075a 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 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. // @@ -34,6 +34,7 @@ #include "ltlast/formula.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" @@ -71,6 +72,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 }, @@ -121,9 +126,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 @@ -141,6 +147,10 @@ parse_opt(int key, char* arg, struct argp_state*) case 'F': jobs.emplace_back(arg, true); break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; case 'M': type = spot::postprocessor::Monitor; break; @@ -317,6 +327,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 dedbf650b..c44989b68 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -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; @@ -244,6 +254,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/bin/ltlcross.cc b/src/bin/ltlcross.cc index 0e187faed..383f57e40 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -95,6 +95,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[] = { @@ -160,6 +161,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 } }; @@ -188,7 +191,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"; @@ -207,6 +210,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 { @@ -510,6 +515,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) @@ -850,7 +863,8 @@ namespace } spot::const_tgba_ptr - 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); @@ -875,11 +889,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"; @@ -889,6 +905,7 @@ namespace { es = WEXITSTATUS(es); status_str = "exit code"; + problem = true; global_error() << "error: execution returned exit code " << es << ".\n"; end_error(); @@ -896,6 +913,7 @@ namespace else { status_str = "ok"; + problem = false; es = 0; switch (output.format) { @@ -907,6 +925,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: ") @@ -951,6 +972,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" @@ -1043,7 +1065,7 @@ namespace } }; - static void + static bool check_empty_prod(const spot::const_tgba_ptr& aut_i, const spot::const_tgba_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) @@ -1086,9 +1108,10 @@ namespace } delete res; delete ec; + return res; } - static void + static bool cross_check(const std::vector& maps, char l, unsigned p) { size_t m = maps.size(); @@ -1141,7 +1164,9 @@ namespace else err << "the state-space\n"; end_error(); + return true; } + return false; } typedef std::set state_set; @@ -1204,12 +1229,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 @@ -1236,7 +1284,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; @@ -1260,6 +1308,9 @@ namespace } } + + int problems = 0; + // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); @@ -1280,7 +1331,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() @@ -1318,7 +1372,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 @@ -1345,7 +1402,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. @@ -1363,13 +1421,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 @@ -1448,14 +1511,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; @@ -1481,7 +1546,7 @@ namespace // Shall we stop processing formulas now? abort_run = global_error_flag && stop_on_error; - return 0; + return problems; } }; } @@ -1499,7 +1564,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); } @@ -1537,7 +1602,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); } @@ -1616,10 +1681,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) @@ -1636,6 +1707,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/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: diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 346b8419f..98b1f098a 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) @@ -184,7 +191,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) @@ -235,6 +242,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; @@ -249,7 +282,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)) @@ -339,14 +372,17 @@ 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); + spot::srand(opt_seed); + typedef std::unordered_set> fset_t; - fset_t unique_set; spot::ltl::ltl_simplifier simpl(simplifier_options()); @@ -357,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; 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 diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 40caef278..2cffa71b5 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -85,7 +85,7 @@ static bool accept_all_seen = false; %token FORMULA "boolean formula" %token IDENT "identifier" %type formula -%type opt_dest +%type opt_dest formula_or_ident %type

transition src_dest %type transitions transition_block %type ident_list @@ -193,7 +193,9 @@ transitions: } -formula: FORMULA +formula_or_ident: FORMULA | IDENT + +formula: formula_or_ident { formula_cache::const_iterator i = fcache.find(*$1); if (i == fcache.end()) diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index b482660f2..e31120b86 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -42,6 +42,7 @@ tgbaalgos_HEADERS = \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ + hoaf.hh \ isdet.hh \ isweakscc.hh \ lbtt.hh \ @@ -87,6 +88,7 @@ libtgbaalgos_la_SOURCES = \ dupexp.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..9417bbc83 --- /dev/null +++ b/src/tgbaalgos/hoaf.cc @@ -0,0 +1,364 @@ +// -*- 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 "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 std::unordered_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 const_tgba_ptr& 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 const_tgba_ptr& 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 const_tgba_ptr& 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()) + { + auto src = todo.front(); + todo.pop_front(); + bdd prev = bddtrue; + bool st_acc = true; + bdd sum = bddfalse; + bdd available = bddtrue; + for (auto i: aut->succ(src)) + { + 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; + } + } + + 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 const_tgba_ptr& 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(); + auto 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(); + } + aut->release_iter(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 const_tgba_ptr& 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..ca9a0c705 --- /dev/null +++ b/src/tgbaalgos/hoaf.hh @@ -0,0 +1,67 @@ +// -*- 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" +#include "tgba/fwd.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 const_tgba_ptr& 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 const_tgba_ptr& g, + const char* opt, + const ltl::formula* f = 0); +} + +#endif // SPOT_TGBAALGOS_HOAF_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 7e59ef84d..40821f222 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -260,24 +260,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); @@ -1346,8 +1381,7 @@ namespace spot } else { - dest->clone(); - const formula* dest2 = unop::instance(op, dest); + const formula* dest2 = unop::instance(op, dest->clone()); if (dest2 == constant::false_instance()) continue; int x = dict_.register_next_variable(dest2); @@ -1363,48 +1397,48 @@ namespace spot case unop::NegClosure: rat_seen_ = true; { - const formula* c = node->child(); if (mark_all_) { op = unop::NegClosureMarked; has_marked_ = true; } - bdd f1 = translate_ratexp(c, dict_); - // trace_ltl_bdd(dict_, f1); + const formula* f = node->child(); + auto p = dict_.transdfa.succ(f); + res_ = bddtrue; + auto aut = std::get<0>(p); + auto namer = std::get<1>(p); + auto st = std::get<2>(p); - bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set); - bdd all_props = bdd_existcomp(f1, dict_.var_set); + if (!aut) + break; - res_ = !all_props & + res_ = bddfalse; + bdd missing = bddtrue; + for (auto i: aut->succ(st)) + { + bdd label = i->current_condition(); + state* s = i->current_state(); + const formula* dest = namer->get_name(aut->state_number(s)); + + missing -= label; + + if (!dest->accepts_eword()) + { + const formula* dest2 = unop::instance(op, dest->clone()); + if (dest2 == constant::false_instance()) + continue; + int x = dict_.register_next_variable(dest2); + dest2->destroy(); + res_ |= label & bdd_ithvar(x); + } + } + + res_ |= missing & // stick X(1) to preserve determinism. bdd_ithvar(dict_.register_next_variable (constant::true_instance())); - - while (all_props != bddfalse) - { - bdd label = bdd_satoneset(all_props, var_set, bddtrue); - all_props -= label; - - const formula* dest = - dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); - - // !{ Exp } is false if Exp accepts the empty word. - if (dest->accepts_eword()) - { - dest->destroy(); - continue; - } - - const formula* dest2 = unop::instance(op, dest); - - if (dest2 == constant::false_instance()) - continue; - - int x = dict_.register_next_variable(dest2); - dest2->destroy(); - res_ |= label & bdd_ithvar(x); - } + //trace_ltl_bdd(dict_, res_); } break; @@ -1479,9 +1513,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 36d53805c..03a78f4ea 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -389,26 +389,26 @@ in: Gq|Gr|(G(q|FGp)&G(r|FG!p)) -x -TA -DS -in | 33 | 152 | 25 -x -TA -DS -in -RT | 21 | 112 | 17 in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) --TGTA | 35 | 543 | XXX --TGTA -RT | 32 | 527 | XXX --TA | 34 | 428 | 11 --TA -RT | 30 | 408 | 9 --TA -lv | 35 | 498 | 5 --TA -lv -RT | 32 | 485 | 4 --TA -sp | 34 | 490 | 4 --TA -sp -RT | 31 | 477 | 3 --TA -lv -sp | 35 | 498 | 5 --TA -lv -sp -RT | 32 | 485 | 4 --TA -DS | 44 | 504 | 21 --TA -DS -RT | 40 | 486 | 18 --TA -DS -lv | 45 | 578 | 15 --TA -DS -lv -RT | 41 | 560 | 12 --TA -DS -sp | 44 | 568 | 14 --TA -DS -sp -RT | 40 | 550 | 11 --TA -DS -lv -sp | 45 | 578 | 15 --TA -DS -lv -sp -RT | 41 | 560 | 12 --x -TA -DS -in | 45 | 558 | 11 --x -TA -DS -in -RT | 39 | 532 | 8 +-TGTA | 45 | 717 | XXX +-TGTA -RT | 35 | 598 | XXX +-TA | 44 | 602 | 16 +-TA -RT | 33 | 482 | 9 +-TA -lv | 45 | 676 | 9 +-TA -lv -RT | 35 | 566 | 4 +-TA -sp | 44 | 654 | 8 +-TA -sp -RT | 34 | 545 | 3 +-TA -lv -sp | 45 | 676 | 9 +-TA -lv -sp -RT | 35 | 566 | 4 +-TA -DS | 54 | 722 | 26 +-TA -DS -RT | 42 | 608 | 18 +-TA -DS -lv | 55 | 800 | 19 +-TA -DS -lv -RT | 44 | 702 | 13 +-TA -DS -sp | 54 | 776 | 18 +-TA -DS -sp -RT | 43 | 678 | 12 +-TA -DS -lv -sp | 55 | 800 | 19 +-TA -DS -lv -sp -RT | 44 | 702 | 13 +-x -TA -DS -in | 55 | 694 | 11 +-x -TA -DS -in -RT | 41 | 597 | 8 in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TGTA | 69 | 1539 | XXX -TGTA -RT | 49 | 935 | XXX diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index fc2981ef3..46ca0c17c 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -36,6 +36,7 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" #include "tgba/tgbasgba.hh" #include "tgbaalgos/degen.hh" #include "tgba/tgbaproduct.hh" @@ -385,6 +386,7 @@ checked_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_ptr system_aut = 0; @@ -553,6 +555,11 @@ checked_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; @@ -1693,7 +1700,11 @@ checked_main(int argc, char** argv) } break; } - + case 17: + { + hoaf_reachable(std::cout, a, hoaf_opt, f) << '\n'; + break; + } default: SPOT_UNREACHABLE(); } diff --git a/src/tgbatest/ltlcross.test b/src/tgbatest/ltlcross.test index ce801ac5a..d5a3845bd 100755 --- a/src/tgbatest/ltlcross.test +++ b/src/tgbatest/ltlcross.test @@ -23,7 +23,21 @@ set -e ltl2tgba=../ltl2tgba -../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | + +( +# Some formulas supplied by Joachim Klein. The first two were +# incorrectly translated by ltl_to_tgba_fm(), while the other have +# shown some bugs in other translators. +cat <p0) +p0 xor (p0 W X!p0) +p0 & (!p0 W Xp0) +EOF +# Random formulas +../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 +) | ../../bin/ltlcross --products=2 \ "$ltl2tgba -t -f %f > %T" \ "$ltl2tgba -t -f -y %f > %T" \ @@ -44,4 +58,3 @@ ltl2tgba=../ltl2tgba "$ltl2tgba -t -taa -r4 %f > %T" \ "$ltl2tgba -t -taa -r4 -c %f > %T" \ "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T" - diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test index 6150ac722..43427c495 100755 --- a/src/tgbatest/ltlcross2.test +++ b/src/tgbatest/ltlcross2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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 (LRDE). # # This file is part of Spot, a model checking library. @@ -23,8 +23,8 @@ set -e ltl2tgba=../../bin/ltl2tgba -../../bin/randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | -../../bin/ltlcross --products=3 \ +../../bin/randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 | +../../bin/ltlcross --products=3 --timeout=60 \ "$ltl2tgba --lbtt --any --low %f > %T" \ "$ltl2tgba --lbtt --any --medium %f > %T" \ "$ltl2tgba --lbtt --any --high %f > %T" \ 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` diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index fc6cb3f67..22e8565b4 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, 2014 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< out.tgba - ../ltl2tgba -f -R3 -Pout.tgba -E "!($1)" - # Also try with -x turned on. - ../ltl2tgba -f -x -R3 -b "$1" > out.tgba - ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)" -} - # Generate 50 random unique PSL formula that do not simplify to LTL # formulae, and that have a size of at lease 12. ../../bin/randltl -n -1 --tree-size 30 --seed 0 --psl a b c | ../../bin/ltlfilt -r --size-min 12 --unique | ../../bin/ltlfilt -v --ltl | head -n 50 | -while read formula; do - check_psl "$formula" -done +../../bin/ltlcross '../ltl2tgba -R3 -t %f >%T' '../ltl2tgba -x -R3 -t %f >%T' \ + -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}' diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css index 28b3038b2..ad6842488 100644 --- a/wrap/python/ajax/css/ltl2tgba.css +++ b/wrap/python/ajax/css/ltl2tgba.css @@ -130,3 +130,7 @@ table.ltltable white-space: pre; font-size: 1.1em; } + +#ltl3ba-tab { + margin-left: 1em; +} diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 0ba0f5a62..8042709ed 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
+

diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt index 374ffb283..bb1588711 100644 --- a/wrap/python/ajax/protocol.txt +++ b/wrap/python/ajax/protocol.txt @@ -27,6 +27,7 @@ Type of formula output if o=f (pick one) ff=o Spot syntax ff=i Spin syntax + ff=l LBT syntax ff=g graphviz output of the AST ff=p property dump diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 4f2418d2f..6d77fa918 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -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: @@ -441,7 +447,7 @@ if dored: # Formula manipulation only. if output_type == 'f': formula_format = form.getfirst('ff', 'o') - # o = Spot, i = Spin, g = GraphViz, p = properties + # o = Spot, i = Spin, l = LBT, g = GraphViz, p = properties if formula_format == 'o': unbufprint(format_formula(f)) elif formula_format == 'i': @@ -452,6 +458,11 @@ if output_type == 'f': if simpopt.reduce_size_strictly: s = '
Try enabling larger formula rewritings.' unbufprint('
The above formula contains PSL operators that Spin will not understand.%s
' % s) + elif formula_format == 'l': + if not f.is_ltl_formula(): + unbufprint('
PSL formulas cannot be expressed in this format.
') + else: + unbufprint('
' + spot.to_lbt_string(f) + '
') elif formula_format == 'g': render_formula(f) elif formula_format == 'p': diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 45ec9ea7b..a4483cb52 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -98,6 +98,7 @@ namespace std { #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/apcollect.hh" +#include "ltlvisit/lbt.hh" #include "tgba/bddprint.hh" #include "tgba/fwd.hh" @@ -203,6 +204,7 @@ using namespace spot; %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" %include "ltlvisit/apcollect.hh" +%include "ltlvisit/lbt.hh" %feature("new") spot::emptiness_check::check; %feature("new") spot::emptiness_check_instantiator::construct;