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

Add a parser for automata in LBTT's format.

Browse source 
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/lbtt.cc (lbtt_parse):
New function.
* src/tgba/tgbaexplicit.hh (get_acceptance_condition): Make it public.
* src/tgbatest/ltl2tgba.cc: Add a -XL option to read LBTT file.
* src/tgbatest/lbttparse.test: New file.
* src/tgbatest/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-02 18:01:35 +02:00
parent df743e5057
commit c55bd831a8
6 changed files with 214 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgba/tgbaexplicit.hh
View file

@ -597,8 +597,6 @@ namespace spot
all_acceptance_conditions_computed_ = false;
}
protected:
bdd get_acceptance_condition(const ltl::formula* f)
{
bdd_dict::fv_map::iterator i = this->dict_->acc_map.find(f);
@ -609,6 +607,8 @@ namespace spot
return v;
}
protected:
virtual bdd compute_support_conditions(const spot::state* in) const
{
const State* s = down_cast<const State*>(in);

114
src/tgbaalgos/lbtt.cc
View file

@ -1,7 +1,8 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 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
// 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,8 +26,10 @@
#include <ostream>
#include <sstream>
#include "tgba/bddprint.hh"
#include "tgba/tgbaexplicit.hh"
#include "reachiter.hh"
#include "misc/bddlt.hh"
#include "ltlparse/public.hh"
namespace spot
{
@ -150,4 +153,111 @@ namespace spot
b.run();
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::vector<bdd> acc_b(num_acc);
for (unsigned n = 0; n < num_acc; ++n)
acc_b[n] = aut->get_acceptance_condition(acc_f[n]);
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;
if (acc_n < 0 || (unsigned)acc_n >= num_acc)
{
error += "invalid acceptance set";
goto fail;
}
acc |= acc_b[acc_n];
}
std::string guard;
std::getline(is, guard);
ltl::parse_error_list pel;
const ltl::formula* f = parse_lbt(guard, pel, env);
if (!f || pel.size() > 0)
{
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_parse(std::istream& is, std::string& error, bdd_dict* dict,
ltl::environment& env, ltl::environment& envacc)
{
is >> std::skipws;
unsigned num_states = 0;
is >> num_states;
if (!is)
{
error += "failed to read the number of states";
return 0;
}
// No states? Read the rest of the line and return an empty automaton.
if (num_states == 0)
{
std::string header;
std::getline(is, header);
return new sba_explicit_number(dict);
}
unsigned num_acc = 0;
is >> num_acc;
std::string rest;
std::getline(is, rest);
if (rest[0] == 't' || rest[0] == 'T')
return lbtt_read_tgba(num_states, num_acc, is, error, dict,
env, envacc);
else
assert(!"unsupported format");
return 0;
}
}

24
src/tgbaalgos/lbtt.hh
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 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.
@ -22,6 +25,7 @@
#include "tgba/tgba.hh"
#include <iosfwd>
#include "ltlenv/defaultenv.hh"
namespace spot
{
@ -31,6 +35,24 @@ namespace spot
/// \param g The automata to print.
/// \param os Where to print.
std::ostream& lbtt_reachable(std::ostream& os, const tgba* g);
/// \brief Read an automaton in LBTT's format
/// \ingroup tgba_io
///
/// \param is The stream on which the automaton should be input.
/// \param error A string in which to write any error message.
/// \param env The environment of atomic proposition into which parsing
/// should take place.
/// \param envacc The environment of acceptance conditions into which parsing
/// should take place.
/// \return the read tgba or 0 on error.
const tgba* lbtt_parse(std::istream& is, std::string& error,
bdd_dict* dict,
ltl::environment& env
= ltl::default_environment::instance(),
ltl::environment& envacc
= ltl::default_environment::instance());
}
#endif // SPOT_TGBAALGOS_LBTT_HH

1
src/tgbatest/Makefile.am
View file

@ -93,6 +93,7 @@ TESTS = \
degendet.test \
degenid.test \
kv.test \
lbttparse.test \
scc.test \
sccsimpl.test \
obligation.test \

41
src/tgbatest/lbttparse.test Executable file
View file

@ -0,0 +1,41 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012 Laboratoire de Recherche et Développement
# 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/>.
. ./defs
set -e
for f in 'p0 U p1 U p2' 'Gp00 | Gp13 | Gp42' '{(1;1)*}[]->p1'
do
# Make sure Spot can read the LBTT it produces
run 0 ../ltl2tgba -t "$f" > out
s=`wc -l < out`
run 0 ../ltl2tgba -t -XL out > out2
s2=`wc -l < out2`
test "$s" -eq "$s2"
# The LBTT output use 2 lines par state, one line per transition,
# and one extra line for header.
run 0 ../ltl2tgba -ks "$f" > size
st=`cat size | sed -n 's/states: //p'`
tr=`cat size | sed -n 's/transitions: //p'`
l=`expr $st \* 2 + $tr + 1`
test "$s" -eq "$l"
done

39
src/tgbatest/ltl2tgba.cc
View file

@ -118,6 +118,8 @@ syntax(char* prog)
<< std::endl
<< " -X do not compute an automaton, read it from a file"
<< std::endl
<< " -XL do not compute an automaton, read it from an"
<< " LBTT file" << std::endl
<< " -XN do not compute an automaton, read it from a"
<< " neverclaim file" << std::endl
<< " -Pfile multiply the formula automaton with the TGBA read"
@ -334,6 +336,7 @@ main(int argc, char** argv)
bool accepting_run_replay = false;
bool from_file = false;
bool read_neverclaim = false;
bool read_lbtt = false;
bool scc_filter = false;
bool simpltl = false;
spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
@ -782,6 +785,11 @@ main(int argc, char** argv)
from_file = true;
read_neverclaim = true;
}
else if (!strcmp(argv[formula_index], "-XL"))
{
from_file = true;
read_lbtt = true;
}
else if (!strcmp(argv[formula_index], "-y"))
{
translation = TransFM;
@ -887,8 +895,8 @@ main(int argc, char** argv)
if (from_file)
{
spot::tgba_explicit_string* e;
if (!read_neverclaim)
spot::tgba_explicit_string* e = 0;
if (!read_neverclaim && !read_lbtt)
{
spot::tgba_parse_error_list pel;
tm.start("parsing automaton");
@ -902,7 +910,7 @@ main(int argc, char** argv)
return 2;
}
}
else
else if (read_neverclaim)
{
spot::neverclaim_parse_error_list pel;
tm.start("parsing neverclaim");
@ -917,7 +925,30 @@ main(int argc, char** argv)
}
assume_sba = true;
}
e->merge_transitions();
else
{
std::string error;
std::fstream f(input.c_str());
if (!f)
{
std::cerr << "cannot open " << input << std::endl;
delete dict;
return 2;
}
tm.start("parsing lbtt");
to_free = a =
const_cast<spot::tgba*>(spot::lbtt_parse(f, error, dict,
env, env));
tm.stop("parsing lbtt");
if (!to_free)
{
std::cerr << error << std::endl;
delete dict;
return 2;
}
}
if (e)
e->merge_transitions();
}
else
{