Commit 120ce7d8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

lbtt: build an explicit automaton on input.

* src/priv/accmap.hh (acc_mapper): Rename into...
(acc_mapper_string): ... this, and add
(acc_mapper_int): ... this variant.
* src/tgbaparse/tgbaparse.yy: Adjust to renaming.
* src/tgbaalgos/lbtt.cc: Use acc_mapper_int and build an explicit
automaton.
* src/tgbaalgos/lbtt.hh: Adjust return type.
* src/tgbatest/ltl2tgba.cc: Adjust to new return type.
parent 1d28714c
......@@ -28,33 +28,51 @@
namespace spot
{
class acc_mapper
class acc_mapper_common
{
protected:
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())
acc_mapper_common(tgba_digraph *aut, ltl::environment& env)
: dict_(aut->get_dict()), aut_(aut), env_(env), neg_(bddtrue)
{
}
public:
const ltl::environment& get_env() const
{
return env_;
}
// Commit all acceptance set to the automaton.
void commit()
{
aut_->set_acceptance_conditions(neg_);
}
};
class acc_mapper_string: public acc_mapper_common
{
std::unordered_map<std::string, int> map_;
public:
acc_mapper_string(tgba_digraph *aut,
ltl::environment& env
= ltl::default_environment::instance())
: acc_mapper_common(aut, 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);
auto f = env_.require(name);
if (!f)
return false;
int v = dict_->register_acceptance_variable(f, aut_);
......@@ -64,12 +82,6 @@ namespace spot
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);
......@@ -79,7 +91,54 @@ namespace spot
bdd_nithvar(p->second),
p->second));
}
};
// The acceptance sets are named using count integers, but we do not
// assume the numbers are necessarily consecutive.
class acc_mapper_int: public acc_mapper_common
{
std::vector<bdd> usable_;
unsigned used_;
std::map<int, bdd> map_;
public:
acc_mapper_int(tgba_digraph *aut,
unsigned count,
ltl::environment& env = ltl::default_environment::instance())
: acc_mapper_common(aut, env), usable_(count), used_(0)
{
std::vector<int> vmap(count);
for (unsigned n = 0; n < count; ++n)
{
std::ostringstream s;
s << n;
auto f = env.require(s.str());
int v = dict_->register_acceptance_variable(f, aut_);
f->destroy();
vmap[n] = v;
neg_ &= bdd_nithvar(v);
}
for (unsigned n = 0; n < count; ++n)
{
int v = vmap[n];
usable_[n] = bdd_compose(neg_, bdd_nithvar(v), v);
}
commit();
}
std::pair<bool, bdd> lookup(unsigned n)
{
auto p = map_.find(n);
if (p != map_.end())
return std::make_pair(true, p->second);
if (used_ < usable_.size())
{
bdd res = usable_[used_++];
map_[n] = res;
return std::make_pair(true, res);
}
return std::make_pair(false, bddfalse);
}
};
}
......
......@@ -24,10 +24,12 @@
#include <map>
#include <string>
#include <ostream>
#include <sstream>
#include <memory>
#include "tgba/tgbaexplicit.hh"
#include "tgba/formula2bdd.hh"
#include "reachiter.hh"
#include "misc/bddlt.hh"
#include "priv/accmap.hh"
#include "ltlvisit/lbt.hh"
#include "ltlparse/public.hh"
......@@ -166,8 +168,142 @@ namespace spot
const sba* sba_;
};
static
const tgba_digraph*
lbtt_read_tgba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
acc_mapper_int acc_b(aut.get(), num_acc, envacc);
auto& g = aut->get_graph();
g.new_states(num_states);
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
// Read the acceptance conditions.
bdd acc = bddfalse;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
auto p = acc_b.lookup(acc_n);
if (p.first)
{
acc |= p.second;
}
else
{
error += "more acceptance sets used than declared";
return nullptr;
}
}
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
return nullptr;
}
bdd cond = formula_to_bdd(f, dict, aut.get());
f->destroy();
g.new_transition(src_state, dst_state, cond, acc);
}
}
return aut.release();
}
const tgba_digraph*
lbtt_read_gba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
acc_mapper_int acc_b(aut.get(), num_acc, envacc);
auto& g = aut->get_graph();
g.new_states(num_states);
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the acceptance conditions.
bdd acc = bddfalse;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
auto p = acc_b.lookup(acc_n);
if (p.first)
{
acc |= p.second;
}
else
{
error += "more acceptance sets used than declared";
return nullptr;
}
}
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
return nullptr;
}
bdd cond = formula_to_bdd(f, dict, aut.get());
f->destroy();
g.new_transition(src_state, dst_state, cond, acc);
}
}
return aut.release();
}
} // anonymous
std::ostream&
lbtt_reachable(std::ostream& os, const tgba* g, bool sba)
{
......@@ -176,173 +312,8 @@ namespace spot
return os;
}
const tgba*
lbtt_read_tgba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
tgba_explicit_number* aut = new tgba_explicit_number(dict);
std::vector<const ltl::formula*> acc_f(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
{
std::ostringstream s;
s << n;
const ltl::formula* af = acc_f[n] = envacc.require(s.str());
aut->declare_acceptance_condition(af->clone());
}
std::map<int, bdd> acc_b;
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
// Read the acceptance conditions.
bdd acc = bddfalse;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
std::map<int, bdd>::const_iterator i = acc_b.find(acc_n);
if (i != acc_b.end())
{
acc |= i->second;
}
else
{
size_t s = acc_b.size();
if (s >= num_acc)
{
error += "more acceptance sets used than declared";
goto fail;
}
bdd a = aut->get_acceptance_condition(acc_f[s]);
acc_b[acc_n] = a;
acc |= a;
}
}
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
goto fail;
}
state_explicit_number::transition* t
= aut->create_transition(src_state, dst_state);
aut->add_condition(t, f);
t->acceptance_conditions |= acc;
}
}
return aut;
fail:
delete aut;
return 0;
}
const tgba*
lbtt_read_gba(unsigned num_states, unsigned num_acc,
std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
tgba_explicit_number* aut = new tgba_explicit_number(dict);
std::vector<const ltl::formula*> acc_f(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
{
std::ostringstream s;
s << n;
const ltl::formula* af = acc_f[n] = envacc.require(s.str());
aut->declare_acceptance_condition(af->clone());
}
std::map<int, bdd> acc_b;
for (unsigned n = 0; n < num_states; ++n)
{
int src_state = 0;
int initial = 0;
is >> src_state >> initial;
if (initial)
aut->set_init_state(src_state);
// Read the acceptance conditions.
bdd acc = bddfalse;
for (;;)
{
int acc_n = 0;
is >> acc_n;
if (acc_n == -1)
break;
std::map<int, bdd>::const_iterator i = acc_b.find(acc_n);
if (i != acc_b.end())
{
acc |= i->second;
}
else
{
size_t s = acc_b.size();
if (s >= num_acc)
{
error += "more acceptance sets used than declared";
goto fail;
}
bdd a = aut->get_acceptance_condition(acc_f[s]);
acc_b[acc_n] = a;
acc |= a;
}
}
// Read the transitions.
for (;;)
{
int dst_state = 0;
is >> dst_state;
if (dst_state == -1)
break;
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || !pel.empty())
{
error += "failed to parse guard: " + guard;
if (f)
f->destroy();
goto fail;
}
state_explicit_number::transition* t
= aut->create_transition(src_state, dst_state);
aut->add_condition(t, f);
t->acceptance_conditions |= acc;
}
}
return aut;
fail:
delete aut;
return 0;
}
const tgba*
const tgba_digraph*
lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
......@@ -361,7 +332,7 @@ namespace spot
{
std::string header;
std::getline(is, header);
return new sba_explicit_number(dict);
return new tgba_digraph(dict);
}
unsigned num_acc = 0;
......@@ -378,6 +349,5 @@ namespace spot
else
return lbtt_read_gba(num_states, num_acc, is, error, dict,
env, envacc);
return 0;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// Copyright (C) 2012, 2013, 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
......@@ -23,7 +23,7 @@
#ifndef SPOT_TGBAALGOS_LBTT_HH
# define SPOT_TGBAALGOS_LBTT_HH
#include "tgba/tgba.hh"
#include "tgba/tgbagraph.hh"
#include <iosfwd>
#include "ltlenv/defaultenv.hh"
......@@ -51,7 +51,7 @@ namespace spot
/// \param envacc The environment of acceptance conditions into which parsing
/// should take place.
/// \return the read tgba or 0 on error.
SPOT_API const tgba*
SPOT_API const tgba_digraph*
lbtt_parse(std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env = ltl::default_environment::instance(),
......
......@@ -45,7 +45,7 @@
%parse-param {spot::tgba_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
%parse-param {spot::acc_mapper& acc_map}
%parse-param {spot::acc_mapper_string& acc_map}
%parse-param {spot::tgba_digraph*& result}
%parse-param {named_tgba_t*& namer}
%parse-param {formula_cache& fcache}
......@@ -233,7 +233,7 @@ namespace spot
formula_cache fcache;
tgba_digraph* result = new tgba_digraph(dict);
auto namer = result->create_namer<std::string>();
spot::acc_mapper acc_map(result, envacc);
spot::acc_mapper_string acc_map(result, envacc);
tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
parser.set_debug_level(debug);
parser.parse();
......
......@@ -1144,8 +1144,9 @@ main(int argc, char** argv)
}
tm.start("parsing lbtt");
to_free = a =
const_cast<spot::tgba*>(spot::lbtt_parse(*in, error, dict,
env, env));
const_cast<spot::tgba_digraph*>(spot::lbtt_parse(*in,
error, dict,
env, env));
tm.stop("parsing lbtt");
delete f;
if (!to_free)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment