Commit 7010a02c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh:

New files.
* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
libevtgbaalgos_la_SOURCES): Add them.
* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
New files.
* src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
(ltl2evtgba_SOURCES): New variable.
parent b89f1e25
2004-10-27 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh:
New files.
* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
libevtgbaalgos_la_SOURCES): Add them.
* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
New files.
* src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
(ltl2evtgba_SOURCES): New variable.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert
that the true state has only one link when unobs is used.
......
......@@ -27,10 +27,12 @@ evtgbaalgosdir = $(pkgincludedir)/evtgbaalgos
evtgbaalgos_HEADERS = \
dotty.hh \
reachiter.hh \
save.hh
save.hh \
tgba2evtgba.hh
noinst_LTLIBRARIES = libevtgbaalgos.la
libevtgbaalgos_la_SOURCES = \
dotty.cc \
reachiter.cc \
save.cc
save.cc \
tgba2evtgba.cc
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "tgba2evtgba.hh"
#include "tgba/tgba.hh"
#include "evtgba/explicit.hh"
#include "tgbaalgos/reachiter.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace
{
class tgba_to_evtgba_iter:
public tgba_reachable_iterator_depth_first
{
public:
tgba_to_evtgba_iter(const tgba* a)
: tgba_reachable_iterator_depth_first(a)
{
res = new evtgba_explicit;
}
~tgba_to_evtgba_iter()
{
}
virtual void
start()
{
const rsymbol_set ss =
acc_to_symbol_set(automata_->all_acceptance_conditions());
for (rsymbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i)
res->declare_acceptance_condition(*i);
}
virtual void
process_state(const state* s, int n, tgba_succ_iterator*)
{
std::string str = this->automata_->format_state(s);
name_[n] = str;
if (n == 1)
res->set_init_state(str);
}
virtual void
process_link(int in, int out, const tgba_succ_iterator* si)
{
// We might need to format out before process_state is called.
name_map_::const_iterator i = name_.find(out);
if (i == name_.end())
{
const state* s = si->current_state();
process_state(s, out, 0);
delete s;
}
rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions());
bdd all = si->current_condition();
while (all != bddfalse)
{
bdd one = bdd_satone(all);
all -= one;
while (one != bddfalse)
{
bdd low = bdd_low(one);
if (low == bddfalse)
{
const ltl::formula* v =
automata_->get_dict()->var_formula_map[bdd_var(one)];
res->add_transition(name_[in],
to_string(v),
ss,
name_[out]);
break;
}
else
{
one = low;
}
}
assert(one != bddfalse);
}
}
evtgba_explicit* res;
protected:
typedef std::map<int, std::string> name_map_;
name_map_ name_;
rsymbol_set
acc_to_symbol_set(bdd acc) const
{
rsymbol_set ss;
while (acc != bddfalse)
{
bdd one = bdd_satone(acc);
acc -= one;
while (one != bddfalse)
{
bdd low = bdd_low(one);
if (low == bddfalse)
{
const ltl::formula* v =
automata_->get_dict()->acc_formula_map[bdd_var(one)];
ss.insert(rsymbol(to_string(v)));
break;
}
else
{
one = low;
}
}
assert(one != bddfalse);
}
return ss;
}
};
} // anonymous
evtgba_explicit*
tgba_to_evtgba(const tgba* a)
{
tgba_to_evtgba_iter i(a);
i.run();
return i.res;
}
} // spot
// Copyright (C) 2004 Laboratoire 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.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH
# define SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH
namespace spot
{
class tgba;
class evtgba_explicit;
/// \brief Convert a tgba into an evtgba.
///
/// (This cannot be done on-the-fly because the alphabet of a tgba
/// as unknown beforehand.)
evtgba_explicit* tgba_to_evtgba(const tgba* a);
}
#endif // SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH
......@@ -26,11 +26,13 @@ LDADD = ../libspot.la
check_SCRIPTS = defs
# Keep this sorted alphabetically.
check_PROGRAMS = \
ltl2evtgba \
explicit \
product \
readsave
# Keep this sorted alphabetically.
ltl2evtgba_SOURCES = ltl2evtgba.cc
explicit_SOURCES = explicit.cc
product_SOURCES = product.cc
readsave_SOURCES = readsave.cc
......@@ -40,7 +42,8 @@ readsave_SOURCES = readsave.cc
TESTS = \
explicit.test \
readsave.test \
product.test
product.test \
ltl2evtgba.test
EXTRA_DIST = $(TESTS)
CLEANFILES = input1 input2 input3 stdout expected
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <iostream>
#include <cassert>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "evtgbaparse/public.hh"
#include "evtgbaalgos/save.hh"
#include "evtgbaalgos/dotty.hh"
#include "evtgbaalgos/tgba2evtgba.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
void
syntax(char* prog)
{
std::cerr << prog << " [-d] [-D] formula" << std::endl;
exit(2);
}
int
main(int argc, char** argv)
{
int exit_code = 0;
if (argc < 2)
syntax(argv[0]);
bool debug_opt = false;
bool dotty_opt = false;
bool post_branching = false;
bool fair_loop_approx = false;
int formula_index = 1;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* unobservables = new spot::ltl::atomic_prop_set;
while (argv[formula_index][0] == '-' && formula_index < argc)
{
if (!strcmp(argv[formula_index], "-d"))
{
debug_opt = true;
}
else if (!strcmp(argv[formula_index], "-D"))
{
dotty_opt = true;
}
else if (!strcmp(argv[formula_index], "-L"))
{
fair_loop_approx = true;
}
else if (!strcmp(argv[formula_index], "-p"))
{
post_branching = true;
}
else if (!strncmp(argv[formula_index], "-U", 2))
{
// Parse -U's argument.
const char* tok = strtok(argv[formula_index] + 2, ", \t;");
while (tok)
{
unobservables->insert
(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
tok = strtok(0, ", \t;");
}
}
else
{
syntax(argv[0]);
}
++formula_index;
}
if (formula_index == argc)
syntax(argv[0]);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::formula* f = 0;
{
spot::ltl::parse_error_list pel;
f = spot::ltl::parse(argv[formula_index], pel, env, debug_opt);
exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index],
pel);
}
if (f)
{
spot::tgba* a = spot::ltl_to_tgba_fm(f, dict, false, true,
post_branching,
fair_loop_approx, unobservables);
spot::ltl::destroy(f);
spot::evtgba* e = spot::tgba_to_evtgba(a);
if (dotty_opt)
spot::dotty_reachable(std::cout, e);
else
spot::evtgba_save_reachable(std::cout, e);
delete e;
delete a;
}
for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin();
i != unobservables->end(); ++i)
spot::ltl::destroy(*i);
delete unobservables;
delete dict;
return exit_code;
}
#!/bin/sh
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
# et Marie Curie.
#
# 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 2 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 Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
. ./defs
set -e
check ()
{
run 0 ./ltl2evtgba "$1"
run 0 ./ltl2evtgba -Uun1,un2,un3 "$1"
}
# We don't check the output, but just running these might be enough to
# trigger assertions.
check a
check 'a U b'
check 'X a'
check 'a & b & c'
check 'a | b | (c U (d & (g U (h ^ i))))'
check 'Xa & (b U !a) & (b U !a)'
check 'Fa & Xb & GFc & Gd'
check 'Fa & Xa & GFc & Gc'
check 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 'a R (b R c)'
check '(a U b) U (c U d)'
check '((Xp2)U(X(1)))*(p1 R(p2 R p0))'
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