diff --git a/ChangeLog b/ChangeLog index a0a1bf8d3..72f7980ac 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,30 @@ +2008-03-14 Alexandre Duret-Lutz + + Make sure Spot compiles with g++-4.3. + + * src/ltlast/formula.hh (hash): Remove const from return type. + This kills a g++-4.3 warning. + * src/misc/hash.hh: Adjust to use unordered_set and unordered_map + from TR1 when g++-4.3 is used. + * src/evtgba/product.cc, src/ltltest/randltl.cc, + src/ltlvisit/randomltl.cc, src/ltlvisit/tostring.cc, + src/misc/freelist.hh, src/misc/optionmap.cc, + src/tgba/tgbareduc.hh, src/tgbaalgos/gv04.cc, + src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/randomgraph.cc, + src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc, + src/ltltest/equals.cc, src/ltltest/readltl.cc, + src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, + src/ltltest/tostring.cc, src/tgbatest/ltlprod.cc, + src/tgbatest/powerset.cc, src/tgbatest/explprod.cc, + src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, + src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc, + src/tgbatest/tripprod.cc, src/evtgbatest/product.cc, + src/evtgbatest/readsave.cc, src/evtgbatest/ltl2evtgba.cc, + src/evtgbatest/readsave.cc: Add missing includes. + * src/tgbatest/explicit.test, src/tgbatest/explprod.test, + src/tgbatest/explpro2.test, src/tgbatest/troprod.test, + src/tgbatest/emptchk.test: Cope with different outputs. + 2008-03-11 Alexandre Duret-Lutz * doc/Doxyfile.in (LATEX_HIDE_INDICES): Do not generate indices diff --git a/src/evtgba/product.cc b/src/evtgba/product.cc index 139d090bd..6152c09d7 100644 --- a/src/evtgba/product.cc +++ b/src/evtgba/product.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,6 +24,7 @@ #include "misc/modgray.hh" #include #include +#include namespace spot { diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc index 4510c88c1..2777caf74 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" diff --git a/src/evtgbatest/product.cc b/src/evtgbatest/product.cc index 49250bde5..822d3fced 100644 --- a/src/evtgbatest/product.cc +++ b/src/evtgbatest/product.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "evtgbaparse/public.hh" #include "evtgbaalgos/save.hh" #include "evtgbaalgos/dotty.hh" diff --git a/src/evtgbatest/readsave.cc b/src/evtgbatest/readsave.cc index 755677270..a5971c9b6 100644 --- a/src/evtgbatest/readsave.cc +++ b/src/evtgbatest/readsave.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "evtgbaparse/public.hh" #include "evtgbaalgos/save.hh" diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 439f767b8..749db27bc 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005, 2008 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. // @@ -95,7 +95,7 @@ namespace spot const std::string& dump() const; /// Return a hash_key for the formula. - const size_t + size_t hash() const { return hash_key_; diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 287c5b0cb..32cb4d5fd 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2006, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "ltlparse/public.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 4c0f40620..c0f6109da 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,6 +23,8 @@ #include #include #include +#include +#include #include "ltlast/atomic_prop.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index ae20c7695..b32e6b1d6 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "ltlparse/public.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/dotty.hh" diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index a6388f3f7..75ee28ab8 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris +// Copyright (C) 2004, 2006, 2007, 2008 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -21,6 +21,7 @@ #include #include +#include #include "ltlparse/public.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index 73f0f2f54..4e0dcf474 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2008 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. // @@ -21,6 +21,7 @@ #include #include +#include #include "ltlparse/public.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index cd7d4f67b..43cf021d7 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,6 +21,7 @@ #include #include +#include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/destroy.hh" diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index c3a3f9ae5..73cf99493 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2005, 2008 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. // @@ -25,6 +25,7 @@ #include "ltlast/allnodes.hh" #include "misc/random.hh" #include +#include namespace spot { diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index a4c5e5378..05b0a3827 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,6 +23,7 @@ #include #include #include +#include #include "tostring.hh" #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" diff --git a/src/misc/freelist.hh b/src/misc/freelist.hh index 6368d9dd8..4dd9cc744 100644 --- a/src/misc/freelist.hh +++ b/src/misc/freelist.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -25,6 +25,7 @@ #include #include +#include namespace spot { diff --git a/src/misc/hash.hh b/src/misc/hash.hh index b47cab6ae..4cc1ad376 100644 --- a/src/misc/hash.hh +++ b/src/misc/hash.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -34,16 +34,26 @@ namespace Sgi { // inherit globals using ::hash_map; + using ::hash_multimap; using ::hash_set; using ::hash; - }; + } # else -# include -# include -# if __GNUC__ == 3 && __GNUC_MINOR__ == 0 - namespace Sgi = std; // GCC 3.0 +# if (__GNUC__ == 4 && __GNUC_MINOR__ > 3) || __GNUC__ >= 4 +# include // GCC 4.3 +# include + namespace Sgi = std::tr1; +# define hash_map unordered_map +# define hash_multimap unordered_multimap +# define hash_set unordered_set # else - namespace Sgi = ::__gnu_cxx; // GCC 3.1 and later +# include +# include +# if __GNUC__ == 3 && __GNUC_MINOR__ == 0 + namespace Sgi = std; // GCC 3.0 +# else + namespace Sgi = ::__gnu_cxx; // GCC 3.1 to 4.2 +# endif # endif # endif # else // ... there are other compilers, right? @@ -70,6 +80,10 @@ namespace spot /// \brief A hash function for strings. /// \ingroup hash_funcs + /// @{ +# if (__GNUC__ == 4 && __GNUC_MINOR__ > 3) || __GNUC__ >= 4 + typedef std::tr1::hash string_hash; +# else // GCC < 4.3 struct string_hash : public Sgi::hash, public std::unary_function @@ -81,6 +95,8 @@ namespace spot return Sgi::hash::operator()(s.c_str()); } }; + /// @} +# endif } #endif // SPOT_MISC_HASH_HH diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc index ac44bb382..c267579fa 100644 --- a/src/misc/optionmap.cc +++ b/src/misc/optionmap.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,6 +21,7 @@ #include #include +#include #include "optionmap.hh" namespace spot diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index 47d7c8231..0ab5cd218 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2006, 2008 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. // @@ -28,6 +28,7 @@ #include "tgbaalgos/gtec/nsheap.hh" #include +#include namespace spot { diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 5dc5468eb..f0c66f48b 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2008 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. // @@ -30,6 +30,7 @@ #include #include +#include #include "tgba/tgba.hh" #include "misc/hash.hh" #include "emptiness.hh" diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 01fd317d4..cc6e3ab3d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2005, 2006, 2008 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. // @@ -830,8 +830,9 @@ namespace spot bdd all_props = bdd_existcomp(res, d.var_set); while (all_props != bddfalse) { - bdd one_prop_set = - exprop ? bdd_satoneset(all_props, var_set, bddtrue) : bddtrue; + bdd one_prop_set = bddtrue; + if (exprop) + one_prop_set = bdd_satoneset(all_props, var_set, bddtrue); all_props -= one_prop_set; typedef std::map succ_map; diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 901751242..f85e5e5b8 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Copyright (C) 2004, 2005, 2007, 2008 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. @@ -28,6 +28,7 @@ #include #include #include +#include namespace spot { diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 0666bd274..993905c3d 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -1,7 +1,7 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2003, 2004, 2005, 2008 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. # @@ -93,5 +93,5 @@ expect_ce 'Fa & Xa & GFc & Gc' 2 expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1 expect_ce '!((FF a) <=> (F x))' 3 expect_no '!((FF a) <=> (F a))' 4 -expect_no 'Xa && (!a U b) && !b && X!b' 5 +expect_no 'Xa && (!a U b) && !b && X!b' 4 expect_no '(a U !b) && Gb' 3 diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test index bab2cbb88..6510e43cd 100755 --- a/src/tgbatest/explicit.test +++ b/src/tgbatest/explicit.test @@ -1,7 +1,7 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2003, 2004, 2005, 2008 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. # @@ -25,7 +25,7 @@ set -e -run 0 ./explicit > stdout +run 0 ./explicit | sed 's/c & b/b \& c/' > stdout cat >expected < stdout +run 0 ./explprod input1 input2 | + sed 's/!a & b/b \& !a/;s/!b & a/a \& !b/'> stdout cat stdout diff stdout expected diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index f4b39e385..94648919a 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,6 +21,7 @@ #include #include +#include #include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 85643af2f..062ede06b 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -1,7 +1,7 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2003, 2004, 2005, 2008 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. # @@ -46,7 +46,8 @@ acc = "p3" "p2" "p1"; "s2 * s2", "s3 * s1", "a & c", "p3" "p1"; EOF -run 0 ./explprod input1 input2 > stdout +run 0 ./explprod input1 input2 | + sed 's/b & a/a \& b/;s/c & a/a \& c/' > stdout cat stdout diff stdout expected diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index ed41e3c9d..2c823d019 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -24,6 +24,7 @@ #include #include #include +#include #include "ltlvisit/destroy.hh" #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 82d67f6f4..2bc0e4a49 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,6 +21,7 @@ #include #include +#include #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index e70870e60..dc246c2e2 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2008 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. // @@ -21,6 +21,7 @@ #include #include +#include #include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index a49e7ba13..6bfebd85e 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2008 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. // @@ -21,6 +21,7 @@ #include #include +#include #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/powerset.hh" #include "tgbaparse/public.hh" diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 66e579a0b..5204484af 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2005, 2008 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. // @@ -29,6 +29,7 @@ #include #include #include +#include #include "ltlparse/public.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/destroy.hh" diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index 0e3056acd..6783ed265 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Copyright (C) 2003, 2004, 2006, 2008 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. @@ -21,6 +21,8 @@ #include #include +#include +#include #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/save.hh" diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 5ae491e1f..26e92266f 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Copyright (C) 2003, 2004, 2006, 2008 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. @@ -19,6 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include + #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/reductgba_sim.hh" #include "tgba/tgbareduc.hh" diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index b3baec66c..d05e6cf78 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2006, 2008 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. // @@ -21,6 +21,8 @@ #include #include +#include +#include #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index 3911da452..0a33f2e6b 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2008 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. // @@ -21,6 +21,7 @@ #include #include +#include #include "tgba/tgbaexplicit.hh" #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index 0f33831ff..d297567e8 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -1,7 +1,7 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2003, 2004, 2005, 2008 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. # @@ -57,7 +57,8 @@ acc = "p4" "p3" "p2" "p1"; "s2 * s2 * s3", "s3 * s1 * s2", "a & c", "p4" "p3"; EOF -run 0 ./tripprod input1 input2 input3 > stdout +run 0 ./tripprod input1 input2 input3 | + sed 's/b & a/a \& b/;s/c & a/a \& c/'> stdout cat stdout diff stdout expected