alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

product: rename the one-the-fly version as otf_product

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-08 22:48:13 +01:00
parent a9748804e4
commit 94577d6519
10 changed files with 41 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

6
iface/ltsmin/modelcheck.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// Developpement de l'Epita (LRDE) // et Developpement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -252,7 +252,7 @@ checked_main(int argc, char **argv)
goto safe_exit; goto safe_exit;
} }
product = spot::product(model, prop); product = spot::otf_product(model, prop);
if (output == DotProduct) if (output == DotProduct)
{ {

3
src/bin/autfilt.cc
View file

@ -37,8 +37,7 @@
#include "tgbaalgos/product.hh" #include "tgbaalgos/product.hh"
#include "tgbaalgos/isdet.hh" #include "tgbaalgos/isdet.hh"
#include "tgbaalgos/stutterize.hh" #include "tgbaalgos/stutter.hh"
#include "tgbaalgos/closure.hh"
#include "misc/optionmap.hh" #include "misc/optionmap.hh"
#include "misc/timer.hh" #include "misc/timer.hh"
#include "misc/random.hh" #include "misc/random.hh"

4
src/bin/ltlfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -45,7 +45,7 @@
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/minimize.hh" #include "tgbaalgos/minimize.hh"
#include "tgbaalgos/safety.hh" #include "tgbaalgos/safety.hh"
#include "tgbaalgos/stutter_invariance.hh" #include "tgbaalgos/stutter.hh"
const char argp_program_doc[] ="\ const char argp_program_doc[] ="\
Read a list of formulas and output them back after some optional processing.\v\ Read a list of formulas and output them back after some optional processing.\v\

16
src/tgba/tgbaproduct.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -131,16 +131,18 @@ namespace spot
const state* right_init_; const state* right_init_;
}; };
inline tgba_product_ptr product(const const_tgba_ptr& left, /// \brief on-the-fly TGBA product
const const_tgba_ptr& right) inline tgba_product_ptr otf_product(const const_tgba_ptr& left,
const const_tgba_ptr& right)
{ {
return std::make_shared<tgba_product>(left, right); return std::make_shared<tgba_product>(left, right);
} }
inline tgba_product_ptr product_at(const const_tgba_ptr& left, /// \brief on-the-fly TGBA product with forced initial states
const const_tgba_ptr& right, inline tgba_product_ptr otf_product_at(const const_tgba_ptr& left,
const state* left_init, const const_tgba_ptr& right,
const state* right_init) const state* left_init,
const state* right_init)
{ {
return std::make_shared<tgba_product_init>(left, right, return std::make_shared<tgba_product_init>(left, right,
left_init, right_init); left_init, right_init);

18
src/tgbaalgos/minimize.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -36,7 +36,7 @@
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "misc/hash.hh" #include "misc/hash.hh"
#include "misc/bddlt.hh" #include "misc/bddlt.hh"
#include "tgba/tgbaproduct.hh" #include "tgbaalgos/product.hh"
#include "tgbaalgos/powerset.hh" #include "tgbaalgos/powerset.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/safety.hh" #include "tgbaalgos/safety.hh"
@ -216,7 +216,7 @@ namespace spot
bool bool
wdba_scc_is_accepting(const const_tgba_digraph_ptr& det_a, unsigned scc_n, 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) power_map& pm)
{ {
@ -247,7 +247,6 @@ namespace spot
assert(++i == loop.end()); assert(++i == loop.end());
loop_a->set_init_state(0U); 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. // Check if the loop is accepting in the original automaton.
bool accepting = false; bool accepting = false;
@ -257,17 +256,16 @@ namespace spot
pm.states_of(det_a->state_number(start)); pm.states_of(det_a->state_number(start));
for (auto& it: ps) for (auto& it: ps)
{ {
// Contrustruct a product between // Construct a product between LOOP_A and ORIG_A starting in
// LOOP_A, and ORIG_A starting in *IT. // *IT. FIXME: This could be sped up a lot!
// FIXME: This could be sped up a lot! if (!product(loop_a, orig_a, 0U,
if (!product_at(loop_a, orig_a, loop_a_init, it)->is_empty()) orig_a->state_number(it))->is_empty())
{ {
accepting = true; accepting = true;
break; break;
} }
} }
loop_a_init->destroy();
return accepting; return accepting;
} }

15
src/tgbaalgos/powerset.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -30,7 +30,7 @@
#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/cycles.hh" #include "tgbaalgos/cycles.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgba/tgbaproduct.hh" #include "tgbaalgos/product.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gtec/gtec.hh"
@ -190,8 +190,8 @@ namespace spot
} }
assert(i == dfs_.end()); assert(i == dfs_.end());
const state* loop_a_init = loop_a->get_init_state(); unsigned loop_a_init = loop_a->get_init_state_number();
assert(loop_a->state_number(loop_a_init) == 0); assert(loop_a_init == 0);
// Check if the loop is accepting in the original automaton. // Check if the loop is accepting in the original automaton.
bool accepting = false; bool accepting = false;
@ -204,14 +204,13 @@ namespace spot
{ {
// Check the product between LOOP_A, and ORIG_A starting // Check the product between LOOP_A, and ORIG_A starting
// in S. // 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; accepting = true;
break; break;
} }
} }
loop_a_init->destroy();
return accepting; return accepting;
} }

6
src/tgbatest/checkpsl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de // Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -27,7 +27,7 @@
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2taa.hh" #include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgba/tgbaproduct.hh" #include "tgbaalgos/product.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
void void

6
src/tgbatest/complementation.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de // Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
// Recherche et Développement de l'Epita (LRDE). // de Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 Anf = spot::ltl_to_tgba_fm(nf1, dict);
auto nAf = spot::make_safra_complement(Af); auto nAf = spot::make_safra_complement(Af);
auto nAnf = spot::make_safra_complement(Anf); 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(); auto res = ec->check();
spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton());
std::cout << "States: " std::cout << "States: "

5
src/tgbatest/ltl2tgba.cc
View file

@ -69,8 +69,7 @@
#include "tgbaalgos/complete.hh" #include "tgbaalgos/complete.hh"
#include "tgbaalgos/dtbasat.hh" #include "tgbaalgos/dtbasat.hh"
#include "tgbaalgos/dtgbasat.hh" #include "tgbaalgos/dtgbasat.hh"
#include "tgbaalgos/closure.hh" #include "tgbaalgos/stutter.hh"
#include "tgbaalgos/stutterize.hh"
#include "taalgos/tgba2ta.hh" #include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh" #include "taalgos/dotty.hh"
@ -1523,7 +1522,7 @@ checked_main(int argc, char** argv)
if (system_aut) if (system_aut)
{ {
a = spot::product(system_aut, a); a = spot::otf_product(system_aut, a);
assume_sba = false; assume_sba = false;

6
src/tgbatest/ltlprod.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2012, 2014 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2012, 2014, 2015 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de // Copyright (C) 2003, 2004 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -25,7 +25,7 @@
#include <cstdlib> #include <cstdlib>
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlparse/public.hh" #include "ltlparse/public.hh"
#include "tgba/tgbaproduct.hh" #include "tgbaalgos/product.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"