From 94577d65196fcf4423047cb7f4d3f001fa70f226 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Jan 2015 22:48:13 +0100 Subject: [PATCH] product: rename the one-the-fly version as otf_product This avoid compiler errors about ambiguous calls and make sure we are calling the intended algorithms everywhere (this wasn't the case). * src/tgba/tgbaproduct.hh (product, product_at): Rename as... (otf_product, otf_product_at): ... this. * iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc, src/bin/ltlfilt.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc, src/tgbatest/ltlprod.cc: Adjust callers. --- iface/ltsmin/modelcheck.cc | 6 +++--- src/bin/autfilt.cc | 3 +-- src/bin/ltlfilt.cc | 4 ++-- src/tgba/tgbaproduct.hh | 16 +++++++++------- src/tgbaalgos/minimize.cc | 18 ++++++++---------- src/tgbaalgos/powerset.cc | 15 +++++++-------- src/tgbatest/checkpsl.cc | 6 +++--- src/tgbatest/complementation.cc | 6 +++--- src/tgbatest/ltl2tgba.cc | 5 ++--- src/tgbatest/ltlprod.cc | 6 +++--- 10 files changed, 41 insertions(+), 44 deletions(-) diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 5afd444ba..f6391174d 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) +// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -252,7 +252,7 @@ checked_main(int argc, char **argv) goto safe_exit; } - product = spot::product(model, prop); + product = spot::otf_product(model, prop); if (output == DotProduct) { diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 86a19e9c7..d1943fad7 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -37,8 +37,7 @@ #include "tgbaalgos/product.hh" #include "tgbaalgos/isdet.hh" -#include "tgbaalgos/stutterize.hh" -#include "tgbaalgos/closure.hh" +#include "tgbaalgos/stutter.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" #include "misc/random.hh" diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 54f6bdf47..9a45150ef 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -45,7 +45,7 @@ #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/safety.hh" -#include "tgbaalgos/stutter_invariance.hh" +#include "tgbaalgos/stutter.hh" const char argp_program_doc[] ="\ Read a list of formulas and output them back after some optional processing.\v\ diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 415d23e59..ff3b47030 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -131,16 +131,18 @@ namespace spot const state* right_init_; }; - inline tgba_product_ptr product(const const_tgba_ptr& left, - const const_tgba_ptr& right) + /// \brief on-the-fly TGBA product + inline tgba_product_ptr otf_product(const const_tgba_ptr& left, + const const_tgba_ptr& right) { return std::make_shared(left, right); } - inline tgba_product_ptr product_at(const const_tgba_ptr& left, - const const_tgba_ptr& right, - const state* left_init, - const state* right_init) + /// \brief on-the-fly TGBA product with forced initial states + inline tgba_product_ptr otf_product_at(const const_tgba_ptr& left, + const const_tgba_ptr& right, + const state* left_init, + const state* right_init) { return std::make_shared(left, right, left_init, right_init); diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 6e77ac234..6c6a97bea 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -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). // // This file is part of Spot, a model checking library. // @@ -36,7 +36,7 @@ #include "ltlast/allnodes.hh" #include "misc/hash.hh" #include "misc/bddlt.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/powerset.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/safety.hh" @@ -216,7 +216,7 @@ namespace spot bool wdba_scc_is_accepting(const const_tgba_digraph_ptr& det_a, unsigned scc_n, - const const_tgba_ptr& orig_a, scc_info& sm, + const const_tgba_digraph_ptr& orig_a, scc_info& sm, power_map& pm) { @@ -247,7 +247,6 @@ namespace spot assert(++i == loop.end()); loop_a->set_init_state(0U); - const state* loop_a_init = loop_a->get_init_state(); // Check if the loop is accepting in the original automaton. bool accepting = false; @@ -257,17 +256,16 @@ namespace spot pm.states_of(det_a->state_number(start)); for (auto& it: ps) { - // Contrustruct a product between - // LOOP_A, and ORIG_A starting in *IT. - // FIXME: This could be sped up a lot! - if (!product_at(loop_a, orig_a, loop_a_init, it)->is_empty()) + // Construct a product between LOOP_A and ORIG_A starting in + // *IT. FIXME: This could be sped up a lot! + if (!product(loop_a, orig_a, 0U, + orig_a->state_number(it))->is_empty()) { accepting = true; break; } } - loop_a_init->destroy(); return accepting; } diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 6e478885a..46611f334 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -30,7 +30,7 @@ #include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/cycles.hh" #include "tgbaalgos/gtec/gtec.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -190,8 +190,8 @@ namespace spot } assert(i == dfs_.end()); - const state* loop_a_init = loop_a->get_init_state(); - assert(loop_a->state_number(loop_a_init) == 0); + unsigned loop_a_init = loop_a->get_init_state_number(); + assert(loop_a_init == 0); // Check if the loop is accepting in the original automaton. bool accepting = false; @@ -204,14 +204,13 @@ namespace spot { // Check the product between LOOP_A, and ORIG_A starting // in S. - if (!product_at(loop_a, ref_, loop_a_init, s)->is_empty()) + if (!product(loop_a, ref_, + loop_a_init, ref_->state_number(s))->is_empty()) { accepting = true; break; } } - - loop_a_init->destroy(); return accepting; } diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc index ba021635f..836b256e5 100644 --- a/src/tgbatest/checkpsl.cc +++ b/src/tgbatest/checkpsl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -27,7 +27,7 @@ #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2taa.hh" #include "tgbaalgos/sccfilter.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/dotty.hh" void diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 99325ad95..970d069a7 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -235,7 +235,7 @@ int main(int argc, char* argv[]) auto Anf = spot::ltl_to_tgba_fm(nf1, dict); auto nAf = spot::make_safra_complement(Af); auto nAnf = spot::make_safra_complement(Anf); - auto ec = spot::couvreur99(spot::product(nAf, nAnf)); + auto ec = spot::couvreur99(spot::otf_product(nAf, nAnf)); auto res = ec->check(); spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); std::cout << "States: " diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 72fb4c343..740b95189 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -69,8 +69,7 @@ #include "tgbaalgos/complete.hh" #include "tgbaalgos/dtbasat.hh" #include "tgbaalgos/dtgbasat.hh" -#include "tgbaalgos/closure.hh" -#include "tgbaalgos/stutterize.hh" +#include "tgbaalgos/stutter.hh" #include "taalgos/tgba2ta.hh" #include "taalgos/dotty.hh" @@ -1523,7 +1522,7 @@ checked_main(int argc, char** argv) if (system_aut) { - a = spot::product(system_aut, a); + a = spot::otf_product(system_aut, a); assume_sba = false; diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 11b2ee5d8..08654e633 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2012, 2014, 2015 Laboratoire de Recherche +// et Développement 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. @@ -25,7 +25,7 @@ #include #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/dotty.hh"