From 9f3a7a49ded72e549ded03831297df30bca33fd7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 7 May 2015 21:10:23 +0200 Subject: [PATCH] Add support for unambiguous automata * src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/ltl2tgba_fm.cc: Implement generation of unambiguous automata. * src/tests/ltl2tgba.cc: Add option -fu to test it. * src/bin/common_post.cc: Adjust the group of options so we can easily add more from ltl2tgba.cc. * src/bin/ltl2tgba.cc: Add support for -U and --unambigous. * src/twaalgos/translate.cc, src/twaalgos/translate.hh: Add support for Unambiguous. * src/tests/ltlcross.test, src/tests/ltlcross2.test: Test both bin/ltl2tgba and tgbatest/ltl2tgba. * NEWS: Mention the change. --- NEWS | 6 ++++ src/bin/common_post.cc | 8 ++--- src/bin/ltl2tgba.cc | 27 +++++++++++++++- src/tests/ltl2tgba.cc | 11 ++++++- src/tests/ltlcross.test | 1 + src/tests/ltlcross2.test | 2 ++ src/twaalgos/ltl2tgba_fm.cc | 64 ++++++++++++++++++++++++++++++------- src/twaalgos/ltl2tgba_fm.hh | 25 +++++++++++++-- src/twaalgos/translate.cc | 24 ++++++++++++-- src/twaalgos/translate.hh | 9 ++++++ 10 files changed, 154 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index 1843b7915..23e73a6d2 100644 --- a/NEWS +++ b/NEWS @@ -221,6 +221,12 @@ New in spot 1.99b (not yet released) new style can be requested from command-line tools using option --spin=6 (or -s6 for short). + - Support for building unambiguous automata. ltl_to_tgba() has a + new options to produce unambiguous TGBA, i.e., TGBAs in which + every word is accepted by at most one path. The ltl2tgba + command line has a new option, --unambigous (or -U) to produce + these automata. + * Noteworthy code changes - Boost is not used anymore. diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 36f88e2c2..737c6d16a 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -37,11 +37,11 @@ static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Translation intent:", 20 }, - { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, - { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, - { "any", 'a', 0, 0, "no preference", 0 }, + { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 20 }, + { "deterministic", 'D', 0, 0, "prefer deterministic automata", 20 }, + { "any", 'a', 0, 0, "no preference", 20 }, { "complete", 'C', 0, 0, "output a complete automaton (combine " - "with other intents)", 0 }, + "with other intents)", 20 }, /**************************************************/ { 0, 0, 0, 0, "Optimization level:", 21 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index b03e87e78..75c47be90 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -63,7 +63,8 @@ static const argp_option options[] = /**************************************************/ { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "the formula, in Spot's syntax", 4 }, - /**************************************************/ + /**************************************************/ + { "unambiguous", 'U', 0, 0, "produce unambiguous automata", 20 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, @@ -81,6 +82,7 @@ const struct argp_child children[] = }; static spot::option_map extra_options; +bool unambiguous = false; static int parse_opt(int key, char* arg, struct argp_state*) @@ -94,6 +96,9 @@ parse_opt(int key, char* arg, struct argp_state*) case 'M': type = spot::postprocessor::Monitor; break; + case 'U': + unambiguous = true; + break; case 'x': { const char* opt = extra_options.parse_options(arg); @@ -175,6 +180,24 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) exit(err); + // Using both --unambiguous --deterministic do not really make + // sense. + if (unambiguous) + { + if (type == spot::postprocessor::Monitor) + { + // We do not now how to make unambiguous monitors, other + // than deterministic monitors. + unambiguous = false; + pref = spot::postprocessor::Deterministic; + } + else if (pref == spot::postprocessor::Deterministic) + { + error(2, 0, + "--unambiguous and --deterministic are incompatible options"); + } + } + if (jobs.empty()) error(2, 0, "No formula to translate? Run '%s --help' for usage.", program_name); @@ -183,6 +206,8 @@ main(int argc, char** argv) trans.set_pref(pref | comp); trans.set_type(type); trans.set_level(level); + if (unambiguous) + trans.set_pref(spot::translator::Unambiguous); try { diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc index 7f5b2fdaa..d2e164b76 100644 --- a/src/tests/ltl2tgba.cc +++ b/src/tests/ltl2tgba.cc @@ -146,6 +146,7 @@ syntax(char* prog) << "Options for Couvreur's FM algorithm (-f):" << std::endl << " -fr reduce formula at each step of FM" << std::endl << " as specified with the -r{1..7} options" << std::endl + << " -fu build unambiguous automata" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -p branching postponement (implies -f)" << std::endl << " -U[PROPS] consider atomic properties of the formula as " @@ -330,6 +331,7 @@ checked_main(int argc, char** argv) bool fm_red = false; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; + bool fm_unambiguous = false; bool file_opt = false; bool degen_reset = true; bool degen_order = false; @@ -512,6 +514,12 @@ checked_main(int argc, char** argv) fm_red = true; translation = TransFM; } + else if (!strcmp(argv[formula_index], "-fu")) + { + fm_unambiguous = true; + fm_exprop_opt = true; + translation = TransFM; + } else if (!strcmp(argv[formula_index], "-F")) { file_opt = true; @@ -1060,7 +1068,8 @@ checked_main(int argc, char** argv) post_branching, fair_loop_approx, unobservables, - fm_red ? simp : 0); + fm_red ? simp : 0, + fm_unambiguous); break; case TransCompo: { diff --git a/src/tests/ltlcross.test b/src/tests/ltlcross.test index d5a3845bd..bccf485de 100755 --- a/src/tests/ltlcross.test +++ b/src/tests/ltlcross.test @@ -41,6 +41,7 @@ EOF ../../bin/ltlcross --products=2 \ "$ltl2tgba -t -f %f > %T" \ "$ltl2tgba -t -f -y %f > %T" \ + "$ltl2tgba -t -f -fu %f > %T" \ "$ltl2tgba -t -f -r4 %f > %T" \ "$ltl2tgba -t -f -R3 %f > %T" \ "$ltl2tgba -t -f -R3 -Rm %f > %T" \ diff --git a/src/tests/ltlcross2.test b/src/tests/ltlcross2.test index acc5b3e48..e4d51017b 100755 --- a/src/tests/ltlcross2.test +++ b/src/tests/ltlcross2.test @@ -43,4 +43,6 @@ ltl2tgba=../../bin/ltl2tgba "$ltl2tgba --spin=6 --ba --medium %f > %N" \ "$ltl2tgba --hoa -BDC %f > %H" \ "$ltl2tgba --lbtt -BC %f > %T" \ +"$ltl2tgba --lbtt --unambiguous --low %f > %T" \ +"$ltl2tgba --lbtt --unambiguous --high %f > %T" \ --json=output.json --csv=output.csv diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index dcdcf6097..74bce3595 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -142,7 +142,7 @@ namespace spot translate_dict(const bdd_dict_ptr& dict, acc_cond& acc, ltl_simplifier* ls, bool exprop, - bool single_acc) + bool single_acc, bool unambiguous) : dict(dict), ls(ls), a_set(bddtrue), @@ -151,7 +151,8 @@ namespace spot transdfa(*this), exprop(exprop), single_acc(single_acc), - acc(acc) + acc(acc), + unambiguous(unambiguous) { } @@ -187,6 +188,7 @@ namespace spot acc_cond& acc; // Map BDD variables to acceptance marks. std::map bm; + bool unambiguous; enum translate_flags { @@ -1289,6 +1291,15 @@ namespace spot { } + bdd + neg_of(const formula* node) + { + const formula* n = dict_.ls->negative_normal_form(node, true); + bdd r = recurse(n); + n->destroy(); + return r; + } + void reset(bool mark_all) { @@ -1360,6 +1371,8 @@ namespace spot bdd a = bdd_ithvar(dict_.register_a_variable(child)); if (!recurring_) a &= bdd_ithvar(dict_.register_next_variable(node)); + if (dict_.unambiguous) + a &= neg_of(child); res_ = y | a; break; } @@ -1575,6 +1588,8 @@ namespace spot f1 &= bdd_ithvar(dict_.register_a_variable(node->second())); if (!recurring_) f1 &= bdd_ithvar(dict_.register_next_variable(node)); + if (dict_.unambiguous) + f1 &= neg_of(node->second()); res_ = f2 | f1; break; } @@ -1589,6 +1604,8 @@ namespace spot bdd f2 = recurse(node->second()); if (!recurring_) f1 &= bdd_ithvar(dict_.register_next_variable(node)); + if (dict_.unambiguous) + f1 &= neg_of(node->second()); res_ = f2 | f1; break; } @@ -1601,10 +1618,15 @@ namespace spot || node->first() == constant::false_instance()); // r(f1 R f2) = r(f2)(r(f1) + X(f1 R f2)) if not recurring // r(f1 R f2) = r(f2) if recurring - if (recurring_) + if (recurring_ && !dict_.unambiguous) break; bdd f1 = recurse(node->first()); - res_ &= f1 | bdd_ithvar(dict_.register_next_variable(node)); + bdd f2 = bddtrue; + if (!recurring_) + f2 = bdd_ithvar(dict_.register_next_variable(node)); + if (dict_.unambiguous) + f2 &= neg_of(node->first()); + res_ &= f1 | f2; break; } case binop::M: @@ -1630,6 +1652,8 @@ namespace spot bdd a = bdd_ithvar(dict_.register_a_variable(node)); if (!recurring_) a &= bdd_ithvar(dict_.register_next_variable(node)); + if (dict_.unambiguous) + a &= neg_of(node->first()); res_ &= f1 | a; break; } @@ -1805,11 +1829,28 @@ namespace spot } case multop::Or: { - res_ = bddfalse; - unsigned s = node->size(); - for (unsigned n = 0; n < s; ++n) - res_ |= recurse(node->nth(n)); - break; + if (!dict_.unambiguous) + { + res_ = bddfalse; + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + res_ |= recurse(node->nth(n)); + break; + } + else + { + bdd prev = bddtrue; + res_ = bddfalse; + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + { + const formula* sub = node->nth(n); + res_ |= prev & recurse(sub); + prev &= neg_of(sub); + } + break; + + } } case multop::Concat: case multop::Fusion: @@ -2202,7 +2243,7 @@ namespace spot ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, - ltl_simplifier* simplifier) + ltl_simplifier* simplifier, bool unambiguous) { const formula* f2; ltl_simplifier* s = simplifier; @@ -2232,7 +2273,8 @@ namespace spot twa_graph_ptr a = make_twa_graph(dict); auto namer = a->create_namer(); - translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence()); + translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence(), + unambiguous); // Compute the set of all promises that can possibly occur // inside the formula. diff --git a/src/twaalgos/ltl2tgba_fm.hh b/src/twaalgos/ltl2tgba_fm.hh index c0342838a..576c73633 100644 --- a/src/twaalgos/ltl2tgba_fm.hh +++ b/src/twaalgos/ltl2tgba_fm.hh @@ -1,6 +1,6 @@ // -*- 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, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -120,6 +120,24 @@ namespace spot } \endverbatim */ /// + /// \param unambiguous When true, unambigous TGBA will be produced using + /// the trick described in the following paper. + /** \verbatim + @InProceedings{ benedikt.13.tacas, + author = {Michael Benedikt and Rastislav Lenhardt and James + Worrell}, + title = {{LTL} Model Checking of Interval Markov Chains}, + booktitle = {19th International Conference on Tools and Algorithms for + the Construction and Analysis of Systems (TACAS'13)}, + year = {2013}, + pages = {32--46}, + series = {Lecture Notes in Computer Science}, + volume = {7795}, + editor = {Nir Piterman and Scott A. Smolka}, + publisher = {Springer} + } + \endvarbatim */ + /// /// \return A spot::twa_graph that recognizes the language of \a f. SPOT_API twa_graph_ptr ltl_to_tgba_fm(const ltl::formula* f, const bdd_dict_ptr& dict, @@ -127,5 +145,6 @@ namespace spot bool branching_postponement = false, bool fair_loop_approx = false, const ltl::atomic_prop_set* unobs = 0, - ltl::ltl_simplifier* simplifier = 0); + ltl::ltl_simplifier* simplifier = 0, + bool unambiguous = false); } diff --git a/src/twaalgos/translate.cc b/src/twaalgos/translate.cc index 1388ebdab..d6ff47ae2 100644 --- a/src/twaalgos/translate.cc +++ b/src/twaalgos/translate.cc @@ -28,6 +28,7 @@ namespace spot void translator::setup_opt(const option_map* opt) { comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; + unambiguous_ = false; if (!opt) return; @@ -63,6 +64,21 @@ namespace spot twa_graph_ptr translator::run(const ltl::formula** f) { + if (unambiguous_) + { + if (type_ == postprocessor::Monitor) + { + // Deterministic monitor are unambiguous, so the + // unambiguous option is not really relevant for monitors. + unambiguous_ = false; + set_pref(postprocessor::Deterministic); + } + else if (pref_ == postprocessor::Deterministic) + { + unambiguous_ = false; + } + } + const ltl::formula* r = simpl_->simplify(*f); (*f)->destroy(); *f = r; @@ -74,9 +90,10 @@ namespace spot twa_graph_ptr aut; if (comp_susp_ > 0) { + // FIXME: Handle unambiguous_ automata? int skel_wdba = skel_wdba_; if (skel_wdba < 0) - skel_wdba = (pref_ == spot::postprocessor::Deterministic) ? 1 : 2; + skel_wdba = (pref_ == postprocessor::Deterministic) ? 1 : 2; aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0, skel_simul_ == 0, early_susp_ != 0, @@ -84,8 +101,9 @@ namespace spot } else { - bool exprop = level_ == spot::postprocessor::High; - aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop); + bool exprop = unambiguous_ || level_ == postprocessor::High; + aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop, + true, false, false, 0, 0, unambiguous_); } aut = this->postprocessor::run(aut, r); return aut; diff --git a/src/twaalgos/translate.hh b/src/twaalgos/translate.hh index f23bfa280..25bf04d4f 100644 --- a/src/twaalgos/translate.hh +++ b/src/twaalgos/translate.hh @@ -83,6 +83,7 @@ namespace spot } typedef postprocessor::output_pref output_pref; + enum output_pref_extra { Unambiguous }; void set_pref(output_pref pref) @@ -90,6 +91,13 @@ namespace spot this->postprocessor::set_pref(pref); } + void + set_pref(output_pref_extra) + { + unambiguous_ = true; + } + + typedef postprocessor::optimization_level optimization_level; void @@ -122,6 +130,7 @@ namespace spot int early_susp_; int skel_wdba_; int skel_simul_; + bool unambiguous_; }; /// @} }