diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index a131ca872..e397c76ad 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // // This file is part of Spot, a model checking library. @@ -68,8 +69,9 @@ namespace spot //////////////////////////////////////////////////////////// // ta_succ_iterator_product ta_succ_iterator_product::ta_succ_iterator_product(const state_ta_product* s, - const ta* t, const kripke* k) : - source_(s), ta_(t), kripke_(k) + const ta* t, + const kripke* k) + : source_(s), ta_(t), kripke_(k) { kripke_source_condition = kripke_->state_condition(s->get_kripke_state()); @@ -269,7 +271,8 @@ namespace spot bdd kripke_init_state_condition = kripke_->state_condition( kripke_init_state); - spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + spot::state* artificial_initial_state = + ta_->get_artificial_initial_state(); if (artificial_initial_state != 0) { @@ -358,8 +361,6 @@ namespace spot return ta_->is_livelock_accepting_state(stp->get_ta_state()); } - - bool ta_product::is_initial_state(const spot::state* s) const { @@ -411,17 +412,14 @@ namespace spot } - - ta_succ_iterator_product_by_changeset::ta_succ_iterator_product_by_changeset( - const state_ta_product* s, const ta* t, const kripke* k, bdd changeset) : - ta_succ_iterator_product(s, t, k) + ta_succ_iterator_product_by_changeset:: + ta_succ_iterator_product_by_changeset(const state_ta_product* s, const ta* t, + const kripke* k, bdd changeset) + : ta_succ_iterator_product(s, t, k) { current_condition_ = changeset; } - - - void ta_succ_iterator_product_by_changeset::next_kripke_dest() { @@ -465,8 +463,5 @@ namespace spot current_condition_); ta_succ_it_->first(); } - } - - } diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh index e54a726d2..3bda29dcd 100644 --- a/src/ta/tgta.hh +++ b/src/ta/tgta.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita_explicit (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -18,8 +18,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TA_TGBTA_HH -# define SPOT_TA_TGBTA_HH +#ifndef SPOT_TA_TGTA_HH +# define SPOT_TA_TGTA_HH #include "tgba/tgba.hh" @@ -82,4 +82,4 @@ namespace spot } -#endif // SPOT_TA_TGBTA_HH +#endif // SPOT_TA_TGTA_HH diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index bdbec7325..dfe0fd059 100644 --- a/src/ta/tgtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -74,8 +74,8 @@ namespace spot // tgbtgta_succ_iterator_product tgta_succ_iterator_product::tgta_succ_iterator_product( const state_product* s, const kripke* k, const tgta* t, - fixed_size_pool* pool) : - source_(s), tgta_(t), kripke_(k), pool_(pool) + fixed_size_pool* pool) + : source_(s), tgta_(t), kripke_(k), pool_(pool) { state * tgta_init_state = tgta_->get_init_state(); @@ -151,9 +151,9 @@ namespace spot } // If one of the two successor sets is empty initially, we reset - // kripke_succ_it_, so that done() can detect this situation easily. (We - // choose to reset kripke_succ_it_ because this variable is already used by - // done().) + // kripke_succ_it_, so that done() can detect this situation + // easily. (We choose to reset kripke_succ_it_ because this + // variable is already used by done().) if (kripke_succ_it_->done()) { delete kripke_succ_it_; diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 8d77592c7..da99c198b 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 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), -// Université Pierre et Marie Curie. +// 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. // @@ -21,8 +22,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_tgta_TGBAPRODUCT_HH -# define SPOT_tgta_TGBAPRODUCT_HH +#ifndef SPOT_TA_TGTAPRODUCT_HH +# define SPOT_TA_TGTAPRODUCT_HH #include "tgba/tgba.hh" #include "tgba/tgbaproduct.hh" @@ -54,7 +55,8 @@ namespace spot class tgta_succ_iterator_product : public tgba_succ_iterator { public: - tgta_succ_iterator_product(const state_product* s, const kripke* k, const tgta* tgta, fixed_size_pool* pool); + tgta_succ_iterator_product(const state_product* s, const kripke* k, + const tgta* tgta, fixed_size_pool* pool); virtual ~tgta_succ_iterator_product(); @@ -107,4 +109,4 @@ namespace spot } -#endif // SPOT_tgta_TGBAPRODUCT_HH +#endif // SPOT_TA_TGTAPRODUCT_HH diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 2b5099489..157cc2f7c 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -60,7 +60,7 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. + numbered_state_heap_hash_map_factory::instance()->build(); // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -216,7 +216,9 @@ namespace spot (a_->is_hole_state_in_ta_component(curr)) && a_->is_livelock_accepting_state(curr); - //may be Buchi accepting scc or livelock accepting scc (contains a livelock accepting state that have no successors in TA) + // May be Buchi accepting scc or livelock accepting scc + // (contains a livelock accepting state that have no + // successors in TA). scc.top().is_accepting = (a_->is_accepting_state(curr) && (!succ->is_stuttering_transition() || a_->is_livelock_accepting_state(curr))) @@ -308,26 +310,28 @@ namespace spot if (is_accepting_sscc) { trace - << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " - << a_->is_livelock_accepting_state(curr) << std::endl; + << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " + << a_->is_livelock_accepting_state(curr) << std::endl; trace - << "PASS 1: scc.top().condition : " << bdd_format_accset( - a_->get_dict(), scc.top().condition) << std::endl; + << "PASS 1: scc.top().condition : " + << bdd_format_accset(a_->get_dict(), scc.top().condition) + << std::endl; trace << "PASS 1: a_->all_acceptance_conditions() : " - << (a_->all_acceptance_conditions()) << std::endl; + << (a_->all_acceptance_conditions()) << std::endl; trace - << "PASS 1 CYCLE and (scc.top().condition == a_->all_acceptance_conditions()) : " - << (scc.top().condition - == a_->all_acceptance_conditions()) << std::endl; + << ("PASS 1 CYCLE and (scc.top().condition == " + "a_->all_acceptance_conditions()) : ") + << (scc.top().condition + == a_->all_acceptance_conditions()) << std::endl; trace << "PASS 1: bddtrue : " << (a_->all_acceptance_conditions() - == bddtrue) << std::endl; + == bddtrue) << std::endl; trace << "PASS 1: bddfalse : " << (a_->all_acceptance_conditions() - == bddfalse) << std::endl; + == bddfalse) << std::endl; clear(h, todo, ta_init_it_); return true; @@ -418,7 +422,7 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. + numbered_state_heap_hash_map_factory::instance()->build(); // * num: the number of visited nodes. Used to set the order of each // visited node, diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh index 68b21281a..873c33a11 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Development de +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2012 Laboratoire de Recherche et Dévelopment 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. +// 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. // @@ -21,8 +22,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TAALGOS_EMPTINESS_HH -# define SPOT_TAALGOS_EMPTINESS_HH +#ifndef SPOT_TAALGOS_EMPTINESSTA_HH +# define SPOT_TAALGOS_EMPTINESSTA_HH #include "ta/taproduct.hh" #include "misc/optionmap.hh" @@ -161,4 +162,4 @@ namespace spot /// \ingroup ta_emptiness_check } -#endif // SPOT_TAALGOS_EMPTINESS_HH +#endif // SPOT_TAALGOS_EMPTINESSTA_HH diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 18959ff2e..8da2984d9 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -30,6 +31,7 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgba/formula2bdd.hh" +#include "tgba/tgbatba.hh" #include "misc/bddop.hh" #include #include "ltlvisit/tostring.hh" diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index bad425c15..1286333ce 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -18,17 +19,10 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBAALGOS_SBA2TA_HH -# define SPOT_TGBAALGOS_SBA2TA_HH +#ifndef SPOT_TAALGOS_TGBA2TA_HH +# define SPOT_TAALGOS_TGBA2TA_HH -#include "misc/hash.hh" -#include -#include -#include -#include "tgba/tgbatba.hh" -#include "ltlast/formula.hh" -#include -#include "misc/bddlt.hh" +#include "tgba/tgba.hh" #include "ta/taexplicit.hh" #include "ta/tgtaexplicit.hh" @@ -59,7 +53,7 @@ namespace spot /// /// \param degeneralized When false, the returned automaton is a generalized /// form of TA, called GTA (Generalized Testing Automaton). - /// Like TGBA, GTA use Generalized Büchi acceptance + /// Like TGBA, GTA use Generalized Büchi acceptance /// conditions intead of Buchi-accepting states: there are several acceptance /// sets (of transitions), and a path is accepted if it traverses /// at least one transition of each set infinitely often or if it contains a @@ -100,11 +94,11 @@ namespace spot /// \param atomic_propositions_set The set of atomic propositions used in the /// input TGBA \a tgba_to_convert /// - /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same + /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same /// language as the TGBA \a tgba_to_convert. tgta_explicit* tgba_to_tgta(const tgba* tgba_to_convert, bdd atomic_propositions_set); } -#endif // SPOT_TGBAALGOS_SBA2TA_HH +#endif // SPOT_TAALGOS_TGBA2TA_HH diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index f84b7d938..469abda22 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -1,6 +1,6 @@ #!/bin/sh -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -132,63 +132,61 @@ run 0 ../ltl2tgba -TGTA -Rm -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout grep 'transitions: 294$' stdout grep 'states: 21$' stdout +f="FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" -run 0 ../ltl2tgba -TA -Rm -ks -in -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -in -R3f -x -DS "$f" >stdout grep 'transitions: 521$' stdout grep 'states: 43$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -lv -R3f -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -lv -R3f -x -DS "$f" >stdout grep 'transitions: 636$' stdout grep 'states: 45$' stdout -run 0 ../ltl2tgba -TA -Rm -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks "$f" >stdout grep 'transitions: 498$' stdout grep 'states: 34$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -in "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -in "$f" >stdout grep 'transitions: 566$' stdout grep 'states: 35$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -in -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -in -R3 -x -DS "$f" >stdout grep 'transitions: 464$' stdout grep 'states: 36$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -R3 -x -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -R3 -x -DS "$f" >stdout grep 'transitions: 565$' stdout grep 'states: 38$' stdout -run 0 ../ltl2tgba -TA -ks -sp -lv -DS "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -ks -sp -lv -DS "$f" >stdout grep 'transitions: 831$' stdout grep 'states: 56$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -sp -lv "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp -lv "$f" >stdout grep 'transitions: 585$' stdout grep 'states: 36$' stdout -run 0 ../ltl2tgba -TGTA -Rm -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +run 0 ../ltl2tgba -TGTA -Rm -ks "$f" >stdout grep 'transitions: 598$' stdout grep 'states: 35$' stdout +g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" -run 0 ../ltl2tgba -TA -Rm -ks -DS "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -DS "$g" >stdout grep 'transitions: 2779$' stdout grep 'states: 127$' stdout -run 0 ../ltl2tgba -TA -Rm -ks -sp "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +run 0 ../ltl2tgba -TA -Rm -ks -sp "$g" >stdout grep 'transitions: 1219$' stdout grep 'states: 65$' stdout -run 0 ../ltl2tgba -TGTA -Rm -ks "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +run 0 ../ltl2tgba -TGTA -Rm -ks "$g" >stdout grep 'transitions: 1283$' stdout grep 'states: 65$' stdout - - - -echo '.................. TESTs: OK' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c6dcf26af..401ad6f1d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1103,7 +1103,7 @@ main(int argc, char** argv) { spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0); - bdd atomic_props_set_bdd = bdd_true(); + bdd atomic_props_set_bdd = bddtrue; for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i != aps->end(); ++i) {