diff --git a/src/priv/Makefile.am b/src/priv/Makefile.am
index 0fd46aefc0886361539dfbee18268d4408874bf9..6cec370d0e8f96e4221d64114b5e0bee4a15512a 100644
--- a/src/priv/Makefile.am
+++ b/src/priv/Makefile.am
@@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2013 Laboratoire de Recherche et
+## Copyright (C) 2013, 2014 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
@@ -23,6 +23,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
noinst_HEADERS = \
acccompl.hh \
accconv.hh \
+ accmap.hh \
bddalloc.hh \
countstates.hh \
freelist.hh
diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh
new file mode 100644
index 0000000000000000000000000000000000000000..9791642ff58c9f5b4ec333b1b30bf4bd8ba45eed
--- /dev/null
+++ b/src/priv/accmap.hh
@@ -0,0 +1,87 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+
+#ifndef SPOT_PRIV_ACCMAP_HH
+# define SPOT_PRIV_ACCMAP_HH
+
+#include
+#include "misc/hash.hh"
+#include "ltlast/formula.hh"
+#include "ltlenv/defaultenv.hh"
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+ class acc_mapper
+ {
+ bdd_dict* dict_;
+ tgba_digraph* aut_;
+ ltl::environment& env_;
+ std::unordered_map map_;
+ bdd neg_;
+
+ public:
+ acc_mapper(tgba_digraph *aut,
+ ltl::environment& env = ltl::default_environment::instance())
+ : dict_(aut->get_dict()), aut_(aut), env_(env), neg_(bddtrue)
+ {
+ }
+
+ const ltl::environment& get_env() const
+ {
+ return env_;
+ }
+
+ // Declare an acceptance name.
+ bool declare(const std::string& name)
+ {
+ auto i = map_.find(name);
+ if (i != map_.end())
+ return true;
+ const ltl::formula* f = env_.require(name);
+ if (!f)
+ return false;
+ int v = dict_->register_acceptance_variable(f, aut_);
+ f->destroy();
+ map_[name] = v;
+ neg_ &= bdd_nithvar(v);
+ return true;
+ }
+
+ // Commit all acceptance set to the automaton.
+ void commit()
+ {
+ aut_->set_acceptance_conditions(neg_);
+ }
+
+ std::pair lookup(std::string name) const
+ {
+ auto p = map_.find(name);
+ if (p == map_.end())
+ return std::make_pair(false, bddfalse);
+ return std::make_pair(true, bdd_compose(neg_,
+ bdd_nithvar(p->second),
+ p->second));
+ }
+
+ };
+
+}
+
+#endif // SPOT_PRIV_ACCCONV_HH
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index 4b8f96fdf0be64e7be4190a839970f3679bc79d2..222a10707a5cee89278fb9de47c4553f0e257734 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -174,10 +174,20 @@ namespace spot
last_support_conditions_input_ = 0;
}
+ // FIXME: Once we ditch GCC 4.6, we can using a template aliases
+ // (supported from GCC 4.7 onward) instead of this.
template ,
typename Name_Equal = std::equal_to>
- named_graph*
+ struct namer
+ {
+ typedef named_graph type;
+ };
+
+ template ,
+ typename Name_Equal = std::equal_to>
+ typename namer::type*
create_namer()
{
return new named_graph(g_);
diff --git a/src/tgbaparse/parsedecl.hh b/src/tgbaparse/parsedecl.hh
index 727f542c60aab1955802529dde13f61f78c6853c..52c7b4357509c2faff8949b4f5eb455835246b97 100644
--- a/src/tgbaparse/parsedecl.hh
+++ b/src/tgbaparse/parsedecl.hh
@@ -1,5 +1,7 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2003, 2005, 2013 Laboratoire d'Informatique de Paris
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita.
+// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
@@ -37,17 +39,4 @@ namespace spot
}
-// Gross kludge to compile yy::Parser in another namespace (tgbayy::)
-// but still use yy::Location. The reason is that Bison's C++
-// skeleton does not support anything close to %name-prefix at the
-// moment. All parser are named yy::Parser which makes it somewhat
-// difficult to define multiple parsers.
-// namespace tgbayy
-// {
-// using namespace yy;
-// }
-// #define yy tgbayy
-
-
-
#endif // SPOT_TGBAPARSE_PARSEDECL_HH
diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh
index a62ed25e8c73224c639ff2c8afb9c7b8f0455719..b8953f8d72006f80a165cde44df9b439db137d71 100644
--- a/src/tgbaparse/public.hh
+++ b/src/tgbaparse/public.hh
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita.
+// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita.
// 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.
@@ -23,7 +23,7 @@
#ifndef SPOT_TGBAPARSE_PUBLIC_HH
# define SPOT_TGBAPARSE_PUBLIC_HH
-# include "tgba/tgbaexplicit.hh"
+# include "tgba/tgbagraph.hh"
# include "misc/location.hh"
# include "ltlenv/defaultenv.hh"
# include
@@ -46,7 +46,7 @@ namespace spot
struct tgba_parse_error_list {};
#endif
- /// \brief Build a spot::tgba_explicit from a text file.
+ /// \brief Build a spot::tgba_digraph from a text file.
/// \param filename The name of the file to parse.
/// \param error_list A list that will be filled with
/// parse errors that occured during parsing.
@@ -66,14 +66,14 @@ namespace spot
///
/// \warning This function is not reentrant.
SPOT_API
- tgba_explicit_string* tgba_parse(const std::string& filename,
- tgba_parse_error_list& error_list,
- bdd_dict* dict,
- ltl::environment& env
- = ltl::default_environment::instance(),
- ltl::environment& envacc
- = ltl::default_environment::instance(),
- bool debug = false);
+ tgba_digraph* tgba_parse(const std::string& filename,
+ tgba_parse_error_list& error_list,
+ bdd_dict* dict,
+ ltl::environment& env
+ = ltl::default_environment::instance(),
+ ltl::environment& envacc
+ = ltl::default_environment::instance(),
+ bool debug = false);
/// \brief Format diagnostics produced by spot::tgba_parse.
/// \param os Where diagnostics should be output.
diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy
index 31a4b2a6245237d3f9696412cd69afaf514e59d3..64201c1ea235c78cf5d2afa7154a0def09d6b544 100644
--- a/src/tgbaparse/tgbaparse.yy
+++ b/src/tgbaparse/tgbaparse.yy
@@ -32,25 +32,29 @@
{
#include
#include "public.hh"
+#include "priv/accmap.hh"
+#include "tgba/formula2bdd.hh"
/* Cache parsed formulae. Labels on arcs are frequently identical and
it would be a waste of time to parse them to formula* over and
over, and to register all their atomic_propositions in the
bdd_dict. Keep the bdd result around so we can reuse it. */
-typedef std::map formula_cache;
+ typedef std::map formula_cache;
+ typedef typename spot::tgba_digraph::namer::type named_tgba_t;
}
%parse-param {spot::tgba_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
-%parse-param {spot::ltl::environment& parse_envacc}
-%parse-param {spot::tgba_explicit_string*& result}
+%parse-param {spot::acc_mapper& acc_map}
+%parse-param {spot::tgba_digraph*& result}
+%parse-param {named_tgba_t*& namer}
%parse-param {formula_cache& fcache}
%union
{
int token;
std::string* str;
const spot::ltl::formula* f;
- std::list* list;
+ bdd* acc;
}
%code
@@ -72,28 +76,25 @@ typedef std::pair pair;
%token IDENT
%type strident string
%type condition
-%type acc_list
+%type acc_list
%token ACC_DEF
%destructor { delete $$; }
-%destructor {
- for (std::list::iterator i = $$->begin();
- i != $$->end(); ++i)
- (*i)->destroy();
- delete $$;
- }
+%destructor { delete $$; }
%printer { debug_stream() << *$$; }
+%printer { debug_stream() << *$$; }
%%
tgba: acceptance_decl lines
| acceptance_decl
- { result->add_state("0"); }
+ { namer->new_state("0"); }
| lines
|
- { result->add_state("0"); };
+ { namer->new_state("0"); };
acceptance_decl: ACC_DEF acc_decl ';'
+ { acc_map.commit(); }
/* At least one line. */
lines: line
@@ -102,8 +103,7 @@ lines: line
line: strident ',' strident ',' condition ',' acc_list ';'
{
- spot::state_explicit_string::transition* t
- = result->create_transition(*$1, *$3);
+ bdd cond = bddtrue;
if ($5)
{
formula_cache::const_iterator i = fcache.find(*$5);
@@ -113,35 +113,34 @@ line: strident ',' strident ',' condition ',' acc_list ';'
const formula* f =
spot::ltl::parse_boolean(*$5, pel, parse_environment,
debug_level());
- for (parse_error_list::iterator i = pel.begin();
- i != pel.end(); ++i)
+ for (auto& j: pel)
{
// Adjust the diagnostic to the current position.
spot::location here = @5;
- here.end.line = here.begin.line + i->first.end.line - 1;
- here.end.column =
- here.begin.column + i->first.end.column;
- here.begin.line += i->first.begin.line - 1;
- here.begin.column += i->first.begin.column;
- error_list.emplace_back(here, i->second);
+ here.end.line = here.begin.line + j.first.end.line - 1;
+ here.end.column = here.begin.column + j.first.end.column;
+ here.begin.line += j.first.begin.line - 1;
+ here.begin.column += j.first.begin.column;
+ error_list.emplace_back(here, j.second);
}
if (f)
- result->add_condition(t, f);
- else
- result->add_conditions(t, bddfalse);
- fcache[*$5] = t->condition;
+ {
+ cond = formula_to_bdd(f, result->get_dict(), result);
+ f->destroy();
+ }
+ fcache[*$5] = cond;
}
else
{
- t->condition = i->second;
+ cond = i->second;
}
- delete $5;
}
- std::list::iterator i;
- for (i = $7->begin(); i != $7->end(); ++i)
- result->add_acceptance_condition(t, *i);
+ unsigned s = namer->new_state(*$1);
+ unsigned d = namer->new_state(*$3);
+ namer->graph().new_transition(s, d, cond, *$7);
delete $1;
delete $3;
+ delete $5;
delete $7;
}
;
@@ -167,26 +166,21 @@ condition:
acc_list:
{
- $$ = new std::list;
+ $$ = new bdd(bddfalse);
}
| acc_list strident
{
- if (*$2 == "true")
+ if (*$2 != "" && *$2 != "false")
{
- $1->push_back(constant::true_instance());
- }
- else if (*$2 != "" && *$2 != "false")
- {
- const formula* f = parse_envacc.require(*$2);
- if (! result->has_acceptance_condition(f))
+ auto p = acc_map.lookup(*$2);
+ if (! p.first)
{
error_list.emplace_back(@2,
"undeclared acceptance condition `" + *$2 + "'");
- f->destroy();
// $2 will be destroyed on error recovery.
YYERROR;
}
- $1->push_back(f);
+ *$1 |= p.second;
}
delete $2;
$$ = $1;
@@ -197,18 +191,16 @@ acc_list:
acc_decl:
| acc_decl strident
{
- const formula* f = parse_envacc.require(*$2);
- if (! f)
+ if (! acc_map.declare(*$2))
{
std::string s = "acceptance condition `";
s += *$2;
s += "' unknown in environment `";
- s += parse_envacc.name();
+ s += acc_map.get_env().name();
s += "'";
error_list.emplace_back(@2, s);
YYERROR;
}
- result->declare_acceptance_condition(f);
delete $2;
}
;
@@ -224,7 +216,7 @@ tgbayy::parser::error(const location_type& location,
namespace spot
{
- tgba_explicit_string*
+ tgba_digraph*
tgba_parse(const std::string& name,
tgba_parse_error_list& error_list,
bdd_dict* dict,
@@ -239,12 +231,24 @@ namespace spot
return 0;
}
formula_cache fcache;
- tgba_explicit_string* result = new tgba_explicit_string(dict);
- tgbayy::parser parser(error_list, env, envacc, result, fcache);
+ tgba_digraph* result = new tgba_digraph(dict);
+ auto* namer = result->create_namer();
+ spot::acc_mapper acc_map(result, envacc);
+ tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
parser.set_debug_level(debug);
parser.parse();
tgbayyclose();
- return result;
+
+ if (namer) // No fatal error
+ {
+ delete namer;
+ return result;
+ }
+ else // Fatal error
+ {
+ delete result;
+ return nullptr;
+ }
}
}
diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc
index d82bd869543394434e382009e7e7ef7775225b58..2a6a1648d6e863dc429151a427017a427313312d 100644
--- a/src/tgbatest/complementation.cc
+++ b/src/tgbatest/complementation.cc
@@ -130,7 +130,7 @@ int main(int argc, char* argv[])
{
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
- spot::tgba_explicit_string* a = spot::tgba_parse(file, pel, dict, env);
+ spot::tgba* a = spot::tgba_parse(file, pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, file, pel))
return 2;
diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test
index cdbce90e7725fd5952619c9939c48b8fd6a10e0d..03236df80c5dd987718b7b38576fa051dc609738 100755
--- a/src/tgbatest/explpro2.test
+++ b/src/tgbatest/explpro2.test
@@ -1,9 +1,10 @@
#!/bin/sh
-# Copyright (C) 2013 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 Laboratoire
-# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
-# Coopératifs (SRC), Université Pierre et Marie Curie.
+# 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.
#
@@ -39,8 +40,8 @@ EOF
cat >expected <<'EOF'
acc = "p2$1" "p3" "p2" "p1";
-"s1 * s1", "s2 * s2", "!a & b", "p2$1" "p1";
-"s1 * s1", "s3 * s3", "a & !b", "p3" "p2";
+"0 * 0", "1 * 1", "!a & b", "p2$1" "p1";
+"0 * 0", "2 * 2", "a & !b", "p3" "p2";
EOF
run 0 ../explprod input1 input2 | tee stdout
diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test
index 79b0d689b9fce2949783bb4adb5e1d3256639b0a..6fd503eb8e0a7e35bf46d6da7baa67113faa93ec 100755
--- a/src/tgbatest/explpro3.test
+++ b/src/tgbatest/explpro3.test
@@ -1,8 +1,9 @@
#!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2014 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
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
@@ -39,8 +40,8 @@ EOF
cat >expected <expected <<'EOF'
acc = "p1$1" "p1";
-"s1 * s1", "s1 * s1", "a", "p1";
-"s1 * s1", "s1 * s1", "!a", "p1$1";
+"0 * 0", "0 * 0", "a", "p1";
+"0 * 0", "0 * 0", "!a", "p1$1";
EOF
run 0 ../explprod input1 input2 > stdout
diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc
index 8637ce66c622111785469db1b8bd10258c3ebe7f..560a69bbc284edd8e2c730d203f53cdf249b80dd 100644
--- a/src/tgbatest/explprod.cc
+++ b/src/tgbatest/explprod.cc
@@ -1,7 +1,8 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2008, 2014 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
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
@@ -47,11 +48,11 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1;
- spot::tgba_explicit_string* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
+ spot::tgba* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
return 2;
spot::tgba_parse_error_list pel2;
- spot::tgba_explicit_string* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
+ spot::tgba* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
return 2;
diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test
index c28a62b4f5d046ee2b560f71dc2997e9d5468236..75b396320a7add9a4696b0e0d0e5679ab195c976 100755
--- a/src/tgbatest/explprod.test
+++ b/src/tgbatest/explprod.test
@@ -1,9 +1,10 @@
#!/bin/sh
-# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2008, 2009, 2013, 2014 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
# 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.
+# 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.
#
@@ -41,9 +42,9 @@ EOF
cat >expected <merge_transitions();
}
break;
case ReadNeverclaim:
diff --git a/src/tgbatest/maskacc.cc b/src/tgbatest/maskacc.cc
index 992a5cfb68541caf803cd8e0df696acf17f0002d..9f9f9258158e353cbd1f317d72721b96d4b516df 100755
--- a/src/tgbatest/maskacc.cc
+++ b/src/tgbatest/maskacc.cc
@@ -1,3 +1,4 @@
+// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
@@ -43,7 +44,7 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
- spot::tgba_explicit_string* aut = spot::tgba_parse(argv[1], pel, dict, env);
+ spot::tgba* aut = spot::tgba_parse(argv[1], pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel))
return 2;
diff --git a/src/tgbatest/maskacc.test b/src/tgbatest/maskacc.test
index e1082be88b9673b12c3b091b6228b6153dc47082..0734028eeb7ede5ff970d1ff3bb60578882cdadc 100755
--- a/src/tgbatest/maskacc.test
+++ b/src/tgbatest/maskacc.test
@@ -35,15 +35,15 @@ EOF
cat >expect1 <expected <<\EOF
acc = "c" "d";
-"s1", "s2", "a & !b", "c" "d";
-"s2", "state 3", "\"F\\G\"", "c";
-"state 3", "s1", "1",;
+"0", "1", "a & !b", "c" "d";
+"1", "2", "\"F\\G\"", "c";
+"2", "0", "1",;
EOF
# Sort out some possible inversions in the output.
@@ -71,10 +72,10 @@ EOF
cat >expected <<\EOF
acc = "c";
-"s1", "s2", "a", "c";
-"s1", "s2", "!b",;
-"s2", "s1", "!b",;
-"s2", "s1", "a", "c";
+"0", "1", "a", "c";
+"0", "1", "!b",;
+"1", "0", "!b",;
+"1", "0", "a", "c";
EOF
run 0 ../ltl2tgba -b -X input > stdout
@@ -85,13 +86,18 @@ run 0 ../randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ &&
mv tmp_ input
cat input
+# the first read-write can renumber the states
run 0 ../ltl2tgba -b -X input > stdout
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ &&
- mv tmp_ stdout
-
-diff input stdout
-
-rm -f input stdout
+mv tmp_ stdout
+test `wc -l < input` = `wc -l < stdout`
+# But this second shout output the same as the first
+run 0 ../ltl2tgba -b -X input > stdout2
+sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout2 > tmp_ &&
+mv tmp_ stdout2
+diff stdout stdout2
+
+rm -f input stdout stdout2
# Check the position of syntax errors in the diagnostics:
diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc
index c088f538225671ac98372eb5a16da5d01dd94735..ab9194c719f594082b7b507f5dfbd44a7d6929bb 100644
--- a/src/tgbatest/tgbaread.cc
+++ b/src/tgbatest/tgbaread.cc
@@ -1,8 +1,9 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2008, 2014 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.
+// 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.
//
@@ -56,8 +57,8 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
- spot::tgba_explicit_string* a = spot::tgba_parse(argv[filename_index],
- pel, dict, env, env, debug);
+ spot::tgba* a = spot::tgba_parse(argv[filename_index],
+ pel, dict, env, env, debug);
if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel))
return 2;
diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test
index fd6749d12e996f1902cbad5859cacc46f93eddb7..186ffee7d040d80b6d90abbc4f2f0b5252bc8a42 100755
--- a/src/tgbatest/tgbaread.test
+++ b/src/tgbatest/tgbaread.test
@@ -1,5 +1,5 @@
#!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2014 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
@@ -38,11 +38,11 @@ cat >expected < 1
- 1 [label="s1"]
+ 1 [label="0"]
1 -> 2 [label="a & !b\n{Acc[d], Acc[c]}"]
- 2 [label="s2"]
+ 2 [label="1"]
2 -> 3 [label="a\n{Acc[c]}"]
- 3 [label="state 3"]
+ 3 [label="2"]
3 -> 1 [label="1\n"]
}
EOF
diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc
index dfd65ebbc5cf02b2a4af9db8e6bf0ed4c0064638..ca419997d976c5735d7f3d759274d2c73c5c6872 100644
--- a/src/tgbatest/tripprod.cc
+++ b/src/tgbatest/tripprod.cc
@@ -1,8 +1,9 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2008, 2014 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.
+// 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.
//
@@ -47,15 +48,15 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1;
- spot::tgba_explicit_string* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
+ spot::tgba* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
return 2;
spot::tgba_parse_error_list pel2;
- spot::tgba_explicit_string* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
+ spot::tgba* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
return 2;
spot::tgba_parse_error_list pel3;
- spot::tgba_explicit_string* a3 = spot::tgba_parse(argv[3], pel3, dict, env);
+ spot::tgba* a3 = spot::tgba_parse(argv[3], pel3, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[3], pel3))
return 2;
diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test
index 9b7d6d52ae27650a68d36064fe2ea9ddeb0a35b8..3c06c9d54df47b56c9fe45214fbb638e4a3e150b 100755
--- a/src/tgbatest/tripprod.test
+++ b/src/tgbatest/tripprod.test
@@ -1,6 +1,6 @@
#!/bin/sh
-# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2008, 2009, 2013, 2014 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
# 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.
@@ -49,12 +49,12 @@ EOF
cat >expected <;
%template(explicit_graph__number_tgba)