Commit 4170080c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent c0b28dc9
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2013 Laboratoire de Recherche et ## Copyright (C) 2013, 2014 Laboratoire de Recherche et
## Développement de l'Epita (LRDE). ## Développement de l'Epita (LRDE).
## ##
## This file is part of Spot, a model checking library. ## This file is part of Spot, a model checking library.
...@@ -23,6 +23,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) ...@@ -23,6 +23,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
noinst_HEADERS = \ noinst_HEADERS = \
acccompl.hh \ acccompl.hh \
accconv.hh \ accconv.hh \
accmap.hh \
bddalloc.hh \ bddalloc.hh \
countstates.hh \ countstates.hh \
freelist.hh freelist.hh
......
// -*- 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_PRIV_ACCMAP_HH
# define SPOT_PRIV_ACCMAP_HH
#include <bdd.h>
#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<std::string, int> 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<bool, bdd> 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
...@@ -174,10 +174,20 @@ namespace spot ...@@ -174,10 +174,20 @@ namespace spot
last_support_conditions_input_ = 0; 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 State_Name, template <typename State_Name,
typename Name_Hash = std::hash<State_Name>, typename Name_Hash = std::hash<State_Name>,
typename Name_Equal = std::equal_to<State_Name>> typename Name_Equal = std::equal_to<State_Name>>
named_graph<graph_t, State_Name, Name_Hash, Name_Equal>* struct namer
{
typedef named_graph<graph_t, State_Name, Name_Hash, Name_Equal> type;
};
template <typename State_Name,
typename Name_Hash = std::hash<State_Name>,
typename Name_Equal = std::equal_to<State_Name>>
typename namer<State_Name, Name_Hash, Name_Equal>::type*
create_namer() create_namer()
{ {
return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_); return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_);
......
// -*- coding: utf-8 -*- // -*- 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), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
...@@ -37,17 +39,4 @@ namespace spot ...@@ -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 #endif // SPOT_TGBAPARSE_PARSEDECL_HH
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// de l'Epita. // Développement de l'Epita.
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie. // Coopératifs (SRC), Université Pierre et Marie Curie.
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
#ifndef SPOT_TGBAPARSE_PUBLIC_HH #ifndef SPOT_TGBAPARSE_PUBLIC_HH
# define SPOT_TGBAPARSE_PUBLIC_HH # define SPOT_TGBAPARSE_PUBLIC_HH
# include "tgba/tgbaexplicit.hh" # include "tgba/tgbagraph.hh"
# include "misc/location.hh" # include "misc/location.hh"
# include "ltlenv/defaultenv.hh" # include "ltlenv/defaultenv.hh"
# include <string> # include <string>
...@@ -46,7 +46,7 @@ namespace spot ...@@ -46,7 +46,7 @@ namespace spot
struct tgba_parse_error_list {}; struct tgba_parse_error_list {};
#endif #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 filename The name of the file to parse.
/// \param error_list A list that will be filled with /// \param error_list A list that will be filled with
/// parse errors that occured during parsing. /// parse errors that occured during parsing.
...@@ -66,14 +66,14 @@ namespace spot ...@@ -66,14 +66,14 @@ namespace spot
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
SPOT_API SPOT_API
tgba_explicit_string* tgba_parse(const std::string& filename, tgba_digraph* tgba_parse(const std::string& filename,
tgba_parse_error_list& error_list, tgba_parse_error_list& error_list,
bdd_dict* dict, bdd_dict* dict,
ltl::environment& env ltl::environment& env
= ltl::default_environment::instance(), = ltl::default_environment::instance(),
ltl::environment& envacc ltl::environment& envacc
= ltl::default_environment::instance(), = ltl::default_environment::instance(),
bool debug = false); bool debug = false);
/// \brief Format diagnostics produced by spot::tgba_parse. /// \brief Format diagnostics produced by spot::tgba_parse.
/// \param os Where diagnostics should be output. /// \param os Where diagnostics should be output.
......
...@@ -32,25 +32,29 @@ ...@@ -32,25 +32,29 @@
{ {
#include <string> #include <string>
#include "public.hh" #include "public.hh"
#include "priv/accmap.hh"
#include "tgba/formula2bdd.hh"
/* Cache parsed formulae. Labels on arcs are frequently identical and /* Cache parsed formulae. Labels on arcs are frequently identical and
it would be a waste of time to parse them to formula* over 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 over, and to register all their atomic_propositions in the
bdd_dict. Keep the bdd result around so we can reuse it. */ bdd_dict. Keep the bdd result around so we can reuse it. */
typedef std::map<std::string, bdd> formula_cache; typedef std::map<std::string, bdd> formula_cache;
typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
} }
%parse-param {spot::tgba_parse_error_list& error_list} %parse-param {spot::tgba_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment} %parse-param {spot::ltl::environment& parse_environment}
%parse-param {spot::ltl::environment& parse_envacc} %parse-param {spot::acc_mapper& acc_map}
%parse-param {spot::tgba_explicit_string*& result} %parse-param {spot::tgba_digraph*& result}
%parse-param {named_tgba_t*& namer}
%parse-param {formula_cache& fcache} %parse-param {formula_cache& fcache}
%union %union
{ {
int token; int token;
std::string* str; std::string* str;
const spot::ltl::formula* f; const spot::ltl::formula* f;
std::list<const spot::ltl::formula*>* list; bdd* acc;
} }
%code %code
...@@ -72,28 +76,25 @@ typedef std::pair<bool, spot::ltl::formula*> pair; ...@@ -72,28 +76,25 @@ typedef std::pair<bool, spot::ltl::formula*> pair;
%token <str> IDENT %token <str> IDENT
%type <str> strident string %type <str> strident string
%type <str> condition %type <str> condition
%type <list> acc_list %type <acc> acc_list
%token ACC_DEF %token ACC_DEF
%destructor { delete $$; } <str> %destructor { delete $$; } <str>
%destructor { %destructor { delete $$; } <acc>
for (std::list<const spot::ltl::formula*>::iterator i = $$->begin();
i != $$->end(); ++i)
(*i)->destroy();
delete $$;
} <list>
%printer { debug_stream() << *$$; } <str> %printer { debug_stream() << *$$; } <str>
%printer { debug_stream() << *$$; } <acc>
%% %%
tgba: acceptance_decl lines tgba: acceptance_decl lines
| acceptance_decl | acceptance_decl
{ result->add_state("0"); } { namer->new_state("0"); }
| lines | lines
| |
{ result->add_state("0"); }; { namer->new_state("0"); };
acceptance_decl: ACC_DEF acc_decl ';' acceptance_decl: ACC_DEF acc_decl ';'
{ acc_map.commit(); }
/* At least one line. */ /* At least one line. */
lines: line lines: line
...@@ -102,8 +103,7 @@ lines: line ...@@ -102,8 +103,7 @@ lines: line
line: strident ',' strident ',' condition ',' acc_list ';' line: strident ',' strident ',' condition ',' acc_list ';'
{ {
spot::state_explicit_string::transition* t bdd cond = bddtrue;
= result->create_transition(*$1, *$3);
if ($5) if ($5)
{ {
formula_cache::const_iterator i = fcache.find(*$5); formula_cache::const_iterator i = fcache.find(*$5);
...@@ -113,35 +113,34 @@ line: strident ',' strident ',' condition ',' acc_list ';' ...@@ -113,35 +113,34 @@ line: strident ',' strident ',' condition ',' acc_list ';'
const formula* f = const formula* f =
spot::ltl::parse_boolean(*$5, pel, parse_environment, spot::ltl::parse_boolean(*$5, pel, parse_environment,
debug_level()); debug_level());
for (parse_error_list::iterator i = pel.begin(); for (auto& j: pel)
i != pel.end(); ++i)
{ {
// Adjust the diagnostic to the current position. // Adjust the diagnostic to the current position.
spot::location here = @5; spot::location here = @5;
here.end.line = here.begin.line + i->first.end.line - 1; here.end.line = here.begin.line + j.first.end.line - 1;
here.end.column = here.end.column = here.begin.column + j.first.end.column;
here.begin.column + i->first.end.column; here.begin.line += j.first.begin.line - 1;
here.begin.line += i->first.begin.line - 1; here.begin.column += j.first.begin.column;
here.begin.column += i->first.begin.column; error_list.emplace_back(here, j.second);
error_list.emplace_back(here, i->second);
} }
if (f) if (f)
result->add_condition(t, f); {
else cond = formula_to_bdd(f, result->get_dict(), result);
result->add_conditions(t, bddfalse); f->destroy();
fcache[*$5] = t->condition; }
fcache[*$5] = cond;
} }
else else
{ {
t->condition = i->second; cond = i->second;
} }
delete $5;
} }
std::list<const formula*>::iterator i; unsigned s = namer->new_state(*$1);
for (i = $7->begin(); i != $7->end(); ++i) unsigned d = namer->new_state(*$3);
result->add_acceptance_condition(t, *i); namer->graph().new_transition(s, d, cond, *$7);
delete $1; delete $1;
delete $3; delete $3;
delete $5;
delete $7; delete $7;
} }
; ;
...@@ -167,26 +166,21 @@ condition: ...@@ -167,26 +166,21 @@ condition:
acc_list: acc_list:
{ {
$$ = new std::list<const formula*>; $$ = new bdd(bddfalse);
} }
| acc_list strident | acc_list strident
{ {
if (*$2 == "true") if (*$2 != "" && *$2 != "false")
{ {
$1->push_back(constant::true_instance()); auto p = acc_map.lookup(*$2);
} if (! p.first)
else if (*$2 != "" && *$2 != "false")
{
const formula* f = parse_envacc.require(*$2);
if (! result->has_acceptance_condition(f))
{ {
error_list.emplace_back(@2, error_list.emplace_back(@2,
"undeclared acceptance condition `" + *$2 + "'"); "undeclared acceptance condition `" + *$2 + "'");
f->destroy();
// $2 will be destroyed on error recovery. // $2 will be destroyed on error recovery.
YYERROR; YYERROR;
} }
$1->push_back(f); *$1 |= p.second;
} }
delete $2; delete $2;
$$ = $1; $$ = $1;
...@@ -197,18 +191,16 @@ acc_list: ...@@ -197,18 +191,16 @@ acc_list:
acc_decl: acc_decl:
| acc_decl strident | acc_decl strident
{ {
const formula* f = parse_envacc.require(*$2); if (! acc_map.declare(*$2))
if (! f)
{ {
std::string s = "acceptance condition `"; std::string s = "acceptance condition `";
s += *$2; s += *$2;
s += "' unknown in environment `"; s += "' unknown in environment `";
s += parse_envacc.name(); s += acc_map.get_env().name();
s += "'"; s += "'";
error_list.emplace_back(@2, s); error_list.emplace_back(@2, s);
YYERROR; YYERROR;
} }
result->declare_acceptance_condition(f);
delete $2; delete $2;
} }
; ;
...@@ -224,7 +216,7 @@ tgbayy::parser::error(const location_type& location, ...@@ -224,7 +216,7 @@ tgbayy::parser::error(const location_type& location,
namespace spot namespace spot
{ {
tgba_explicit_string* tgba_digraph*
tgba_parse(const std::string& name, tgba_parse(const std::string& name,
tgba_parse_error_list& error_list, tgba_parse_error_list& error_list,
bdd_dict* dict, bdd_dict* dict,
...@@ -239,12 +231,24 @@ namespace spot ...@@ -239,12 +231,24 @@ namespace spot
return 0; return 0;
} }
formula_cache fcache; formula_cache fcache;
tgba_explicit_string* result = new tgba_explicit_string(dict); tgba_digraph* result = new tgba_digraph(dict);
tgbayy::parser parser(error_list, env, envacc, result, fcache); auto* namer = result->create_namer<std::string>();
spot::acc_mapper acc_map(result, envacc);
tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
parser.set_debug_level(debug); parser.set_debug_level(debug);
parser.parse(); parser.parse();
tgbayyclose(); tgbayyclose();
return result;
if (namer) // No fatal error
{
delete namer;
return result;
}
else // Fatal error
{
delete result;
return nullptr;
}
} }
} }
......
...@@ -130,7 +130,7 @@ int main(int argc, char* argv[]) ...@@ -130,7 +130,7 @@ int main(int argc, char* argv[])
{ {
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel; 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)) if (spot::format_tgba_parse_errors(std::cerr, file, pel))
return 2; return 2;
......
#!/bin/sh #!/bin/sh
# Copyright (C) 2013 Laboratoire de Recherche et Dveloppement de # -*- coding: utf-8 -*-
# l'Epita (LRDE). # Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 Laboratoire # Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 Laboratoire
# d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
# Coopratifs (SRC), Universit Pierre et Marie Curie. # Coopératifs (SRC), Université Pierre et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
...@@ -39,8 +40,8 @@ EOF ...@@ -39,8 +40,8 @@ EOF
cat >expected <<'EOF' cat >expected <<'EOF'
acc = "p2$1" "p3" "p2" "p1"; acc = "p2$1" "p3" "p2" "p1";
"s1 * s1", "s2 * s2", "!a & b", "p2$1" "p1"; "0 * 0", "1 * 1", "!a & b", "p2$1" "p1";
"s1 * s1", "s3 * s3", "a & !b", "p3" "p2"; "0 * 0", "2 * 2", "a & !b", "p3" "p2";
EOF EOF
run 0 ../explprod input1 input2 | tee stdout run 0 ../explprod input1 input2 | tee stdout
......
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Dveloppement # -*- coding: utf-8 -*-
# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -39,8 +40,8 @@ EOF ...@@ -39,8 +40,8 @@ EOF
cat >expected <<EOF cat >expected <<EOF
acc = "p2" "p3"; acc = "p2" "p3";
"s1 * s1", "s2 * s2", "!a & b", "p2"; "0 * 0", "1 * 1", "!a & b", "p2";
"s1 * s1", "s3 * s3", "a & !b", "p3"; "0 * 0", "2 * 2", "a & !b", "p3";
EOF EOF
run 0 ../explprod input1 input2 | run 0 ../explprod input1 input2 |
......
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Dveloppement # -*- coding: utf-8 -*-
# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -39,8 +40,8 @@ EOF ...@@ -39,8 +40,8 @@ EOF
cat >expected <<'EOF' cat >expected <<'EOF'
acc = "p1$1" "p1"; acc = "p1$1" "p1";