From 4170080c357110f50cc9f760da23aee34ab68883 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Jun 2014 23:07:33 +0200 Subject: [PATCH] tgbaparse: Return a tgba_digraph. * src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Adjust to return a tgba_digraph. * src/priv/accmap.hh: New file to help creating acceptance conditions from strings. * src/priv/Makefile.am: Add accmap.hh * src/tgba/tgbagraph.hh (tgba_digraph::named_t): New typedef. * wrap/python/spot.i: Declare that tgba_digraph inherits from tgba. * src/tgbatest/complementation.cc, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explpro4.test, src/tgbatest/explprod.cc, src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test, src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc, src/tgbatest/randtgba.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test: Adjust to the change. --- src/priv/Makefile.am | 3 +- src/priv/accmap.hh | 87 ++++++++++++++++++++++++++ src/tgba/tgbagraph.hh | 12 +++- src/tgbaparse/parsedecl.hh | 17 +----- src/tgbaparse/public.hh | 24 ++++---- src/tgbaparse/tgbaparse.yy | 104 +++++++++++++++++--------------- src/tgbatest/complementation.cc | 2 +- src/tgbatest/explpro2.test | 13 ++-- src/tgbatest/explpro3.test | 9 +-- src/tgbatest/explpro4.test | 9 +-- src/tgbatest/explprod.cc | 9 +-- src/tgbatest/explprod.test | 15 ++--- src/tgbatest/ltl2tgba.cc | 4 +- src/tgbatest/maskacc.cc | 3 +- src/tgbatest/maskacc.test | 16 ++--- src/tgbatest/mixprod.cc | 4 +- src/tgbatest/powerset.cc | 9 +-- src/tgbatest/randtgba.test | 6 +- src/tgbatest/readsave.test | 36 ++++++----- src/tgbatest/tgbaread.cc | 11 ++-- src/tgbatest/tgbaread.test | 8 +-- src/tgbatest/tripprod.cc | 13 ++-- src/tgbatest/tripprod.test | 16 ++--- wrap/python/spot.i | 8 +++ 24 files changed, 278 insertions(+), 160 deletions(-) create mode 100644 src/priv/accmap.hh diff --git a/src/priv/Makefile.am b/src/priv/Makefile.am index 0fd46aefc..6cec370d0 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 000000000..9791642ff --- /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 4b8f96fdf..222a10707 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 727f542c6..52c7b4357 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 a62ed25e8..b8953f8d7 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 31a4b2a62..64201c1ea 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 d82bd8695..2a6a1648d 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 cdbce90e7..03236df80 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 79b0d689b..6fd503eb8 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 8637ce66c..560a69bbc 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 c28a62b4f..75b396320 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 992a5cfb6..9f9f92581 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 e1082be88..0734028ee 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 c088f5382..ab9194c71 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 fd6749d12..186ffee7d 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 dfd65ebbc..ca419997d 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 9b7d6d52a..3c06c9d54 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) -- GitLab