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

Make sure Spot compiles with g++-4.3.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2008-03-13 17:42:42 +01:00
parent f217ff374c
commit d3b702a97c
36 changed files with 177 additions and 94 deletions
Download patch file Download diff file Expand all files Collapse all files

27
ChangeLog
View file

@ -1,3 +1,30 @@
2008-03-14 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
* doc/Doxyfile.in (LATEX_HIDE_INDICES): Do not generate indices

3
src/evtgba/product.cc
View file

@ -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 <cstdlib>
#include <set>
#include <cstring>
namespace spot
{

8
src/evtgbatest/ltl2evtgba.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"

8
src/evtgbatest/product.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "evtgbaparse/public.hh"
#include "evtgbaalgos/save.hh"
#include "evtgbaalgos/dotty.hh"

8
src/evtgbatest/readsave.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "evtgbaparse/public.hh"
#include "evtgbaalgos/save.hh"

8
src/ltlast/formula.hh
View file

@ -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_;

8
src/ltltest/equals.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "ltlparse/public.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/tunabbrev.hh"

4
src/ltltest/randltl.cc
View file

@ -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 <iostream>
#include <set>
#include <string>
#include <cstdlib>
#include <cstring>
#include "ltlast/atomic_prop.hh"
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/tostring.hh"

8
src/ltltest/readltl.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "ltlparse/public.hh"
#include "ltlvisit/dump.hh"
#include "ltlvisit/dotty.hh"

3
src/ltltest/reduc.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/tunabbrev.hh"

7
src/ltltest/syntimpl.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/tunabbrev.hh"

3
src/ltltest/tostring.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/destroy.hh"

7
src/ltlvisit/randomltl.cc
View file

@ -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 <iostream>
#include <cstring>
namespace spot
{

3
src/ltlvisit/tostring.cc
View file

@ -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 <sstream>
#include <ctype.h>
#include <ostream>
#include <cstring>
#include "tostring.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"

3
src/misc/freelist.hh
View file

@ -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 <list>
#include <utility>
#include <iostream>
namespace spot
{

30
src/misc/hash.hh
View file

@ -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 <ext/hash_map>
# include <ext/hash_set>
# if __GNUC__ == 3 && __GNUC_MINOR__ == 0
namespace Sgi = std; // GCC 3.0
# if (__GNUC__ == 4 && __GNUC_MINOR__ > 3) || __GNUC__ >= 4
# include <tr1/unordered_set> // GCC 4.3
# include <tr1/unordered_map>
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 <ext/hash_map>
# include <ext/hash_set>
# 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<std::string> string_hash;
# else // GCC < 4.3
struct string_hash :
public Sgi::hash<const char*>,
public std::unary_function<const std::string&, size_t>
@ -81,6 +95,8 @@ namespace spot
return Sgi::hash<const char*>::operator()(s.c_str());
}
};
/// @}
# endif
}
#endif // SPOT_MISC_HASH_HH

3
src/misc/optionmap.cc
View file

@ -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 <cstring>
#include <iostream>
#include <cstdlib>
#include "optionmap.hh"
namespace spot

7
src/tgba/tgbareduc.hh
View file

@ -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 <list>
#include <vector>
namespace spot
{

7
src/tgbaalgos/gv04.cc
View file

@ -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 <cassert>
#include <utility>
#include <vector>
#include "tgba/tgba.hh"
#include "misc/hash.hh"
#include "emptiness.hh"

11
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -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<bdd, const formula*, bdd_less_than> succ_map;

5
src/tgbaalgos/randomgraph.cc
View file

@ -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 <list>
#include <set>
#include <iterator>
#include <vector>
namespace spot
{

8
src/tgbatest/emptchk.test
View file

@ -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

8
src/tgbatest/explicit.test
View file

@ -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 <<EOF
digraph G {

9
src/tgbatest/explpro2.test
View file

@ -1,7 +1,7 @@
#!/bin/sh
# 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.
#
@ -43,7 +43,8 @@ acc = "p2$1" "p3" "p2" "p1";
"s1 * s1", "s3 * s3", "a & !b", "p3" "p2";
EOF
run 0 ./explprod input1 input2 > stdout
run 0 ./explprod input1 input2 |
sed 's/!a & b/b \& !a/;s/!b & a/a \& !b/'> stdout
cat stdout
diff stdout expected

3
src/tgbatest/explprod.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaparse/public.hh"

9
src/tgbatest/explprod.test
View file

@ -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

3
src/tgbatest/ltl2tgba.cc
View file

@ -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 <cassert>
#include <fstream>
#include <string>
#include <cstdlib>
#include "ltlvisit/destroy.hh"
#include "ltlvisit/contain.hh"
#include "ltlvisit/tostring.hh"

3
src/tgbatest/ltlprod.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"

7
src/tgbatest/mixprod.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"

7
src/tgbatest/powerset.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/powerset.hh"
#include "tgbaparse/public.hh"

7
src/tgbatest/randtgba.cc
View file

@ -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 <utility>
#include <set>
#include <string>
#include <vector>
#include "ltlparse/public.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/destroy.hh"

6
src/tgbatest/readsave.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/save.hh"

6
src/tgbatest/reductgba.cc
View file

@ -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 <cstdlib>
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgba/tgbareduc.hh"

8
src/tgbatest/tgbaread.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"

7
src/tgbatest/tripprod.cc
View file

@ -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 <iostream>
#include <cassert>
#include <cstdlib>
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaparse/public.hh"

9
src/tgbatest/tripprod.test
View file

@ -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