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

* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check2):

Browse source 
New function, variant of emptiness_check::check().
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2):
Likewise.
* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Exercize -e2.
* src/tgbatest/ltl2tgba.cc: Support -e2, for emptiness_check::check2().
* iface/gspn/Makefile.am [WITH_GSPN_EESRG] (check_PROGRAMS):
Compile ltlgspn-eesrg instead of ltleesrg.
(ltleesrg_SOURCES, ltleesrg_LDADD): Replace by...
(ltlgspn_eesrg_SOURCES, ltlgspn_eesrg_LDADD, LIBGSPNESRG_LDFLAGS):
... these.
* iface/gspn/ltleesrg.cc: Delete.
* iface/gspn/ltlgspn.cc [EESRG]: Support EESRG conditionally.
Support -e2.
This commit is contained in:
Alexandre Duret-Lutz 2004-01-09 17:22:09 +00:00
parent a1f990b125
commit 93f1cc0d47
9 changed files with 271 additions and 109 deletions
Download patch file Download diff file Expand all files Collapse all files

15
ChangeLog
View file

@ -1,5 +1,20 @@
2004-01-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check2):
New function, variant of emptiness_check::check().
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2):
Likewise.
* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Exercize -e2.
* src/tgbatest/ltl2tgba.cc: Support -e2, for emptiness_check::check2().
* iface/gspn/Makefile.am [WITH_GSPN_EESRG] (check_PROGRAMS):
Compile ltlgspn-eesrg instead of ltleesrg.
(ltleesrg_SOURCES, ltleesrg_LDADD): Replace by...
(ltlgspn_eesrg_SOURCES, ltlgspn_eesrg_LDADD, LIBGSPNESRG_LDFLAGS):
... these.
* iface/gspn/ltleesrg.cc: Delete.
* iface/gspn/ltlgspn.cc [EESRG]: Support EESRG conditionally.
Support -e2.
* src/tgbaalgos/ltl2tgba_lacim.cc: Typo in comment.
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Typos

7
iface/gspn/Makefile.am
View file

@ -44,7 +44,7 @@ if WITH_GSPN_EESRG
gspn_HEADERS += eesrg.hh
check_PROGRAMS += \
dottygspn-eesrg \
ltleesrg
ltlgspn-eesrg
libspotgspneesrg_la_LIBADD = $(top_builddir)/src/libspot.la
libspotgspneesrg_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS)
@ -69,8 +69,9 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
ltlgspn_srg_SOURCES = ltlgspn.cc
ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
ltleesrg_SOURCES = ltleesrg.cc
ltleesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS)
ltlgspn_eesrg_SOURCES = ltlgspn.cc
ltlgspn_eesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS)
ltlgspn_eesrg_CPPFLAGS = -DEESRG=1 $(AM_CPPFLAGS)
EXTRA_DIST = \
examples/DCSwave/DCSWave.def \

98
iface/gspn/ltleesrg.cc
View file

@ -1,98 +0,0 @@
// 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.
//
// 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 "eesrg.hh"
#include "tgbaalgos/dotty.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/emptinesscheck.hh"
#include "ltlparse/public.hh"
#include "ltlvisit/destroy.hh"
#include "tgba/tgbaproduct.hh"
int
main(int argc, char **argv)
try
{
spot::gspn_environment env;
if (argc <= 4)
{
std::cerr << "usage: " << argv[0]
<< " model ltlformula automata props..."
<< std::endl;
exit(1);
}
while (argc > 4)
env.declare(argv[--argc]);
spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(argv[2], pel, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel))
exit(2);
spot::gspn_eesrg_interface gspn(2, argv);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[3], pel1,
dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
spot::tgba* a_f = spot::ltl_to_tgba_fm(f, dict);
spot::ltl::destroy(f);
spot::tgba_product* prod = new spot::tgba_product(control, a_f);
{
spot::tgba_gspn_eesrg a(dict, env, prod);
spot::emptiness_check ec(&a);
bool res = ec.check();
if (!res)
{
ec.counter_example();
ec.print_result(std::cout, &a);
}
else
{
std::cout << "empty" << std::endl;
}
std::cout << std::endl;
ec.print_stats(std::cout);
if (!res)
exit(1);
}
delete prod;
delete a_f;
delete control;
delete dict;
}
catch (spot::gspn_exeption e)
{
std::cerr << e << std::endl;
throw;
}

55
iface/gspn/ltlgspn.cc
View file

@ -19,7 +19,15 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef EESRG
#include "gspn.hh"
#define MIN_ARG 3
#else
#include "eesrg.hh"
#define MIN_ARG 4
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
#endif
#include "ltlparse/public.hh"
#include "ltlvisit/destroy.hh"
#include "tgba/tgbatba.hh"
@ -29,16 +37,22 @@
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/emptinesscheck.hh"
void
syntax(char* prog)
{
std::cerr << "Usage: "<< prog
#ifndef EESRG
<< " [OPTIONS...] model formula props..." << std::endl
#else
<< " [OPTIONS...] model formula automata props..." << std::endl
#endif
<< std::endl
<< " -c compute an example" << std::endl
<< " (instead of just checking for emptiness)" << std::endl
<< std::endl
<< " -e use Couvreur's emptiness-check (default)" << std::endl
<< " -e2 use Couvreur's emptiness-check variant" << std::endl
<< " -m degeneralize and perform a magic-search" << std::endl
<< std::endl
<< " -l use Couvreur's LaCIM algorithm for translation (default)"
@ -53,7 +67,7 @@ main(int argc, char **argv)
try
{
int formula_index = 1;
enum { Couvreur, Magic } check = Couvreur;
enum { Couvreur, Couvreur2, Magic } check = Couvreur;
enum { Lacim, Fm } trans = Lacim;
bool compute_counter_example = false;
bool proj = true;
@ -70,6 +84,10 @@ main(int argc, char **argv)
{
check = Couvreur;
}
else if (!strcmp(argv[formula_index], "-e2"))
{
check = Couvreur2;
}
else if (!strcmp(argv[formula_index], "-m"))
{
check = Magic;
@ -92,11 +110,11 @@ main(int argc, char **argv)
}
++formula_index;
}
if (argc < formula_index + 3)
if (argc < formula_index + MIN_ARG)
syntax(argv[0]);
while (argc > formula_index + 2)
while (argc >= formula_index + 3)
{
env.declare(argv[argc - 1]);
--argc;
@ -111,9 +129,20 @@ main(int argc, char **argv)
exit(2);
argv[1] = argv[formula_index];
spot::gspn_interface gspn(2, argv);
spot::bdd_dict* dict = new spot::bdd_dict();
#if EESRG
spot::gspn_eesrg_interface gspn(2, argv);
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
#else
spot::gspn_interface gspn(2, argv);
#endif
spot::tgba* a_f = 0;
switch (trans)
{
@ -126,15 +155,26 @@ main(int argc, char **argv)
}
spot::ltl::destroy(f);
#ifndef EESRG
spot::tgba* model = new spot::tgba_gspn(dict, env);
spot::tgba_product* prod = new spot::tgba_product(model, a_f);
#else
spot::tgba_product* ca = new spot::tgba_product(control, a_f);
spot::tgba* model = new spot::tgba_gspn_eesrg(dict, env, ca);
spot::tgba* prod = model;
#endif
switch (check)
{
case Couvreur:
case Couvreur2:
{
spot::emptiness_check ec(prod);
bool res = ec.check();
bool res;
if (check == Couvreur)
res = ec.check();
else
res = ec.check2();
if (!res)
{
if (compute_counter_example)
@ -177,8 +217,13 @@ main(int argc, char **argv)
delete d;
}
}
#ifndef EESRG
delete prod;
delete model;
#else
delete model;
delete control;
#endif
delete a_f;
delete dict;
}

168
src/tgbaalgos/emptinesscheck.cc
View file

@ -25,6 +25,7 @@
#include <stdio.h>
#include <vector>
#include <map>
#include <list>
namespace spot
{
@ -208,7 +209,7 @@ namespace spot
if (dest != i->first)
delete dest;
// If we have reached a dead component. Ignore it.
// If we have reached a dead component, ignore it.
if (i->second == -1)
continue;
@ -257,6 +258,171 @@ namespace spot
return true;
}
struct successor {
bdd acc;
const spot::state* s;
successor(bdd acc, const spot::state* s): acc(acc), s(s) {}
};
bool
emptiness_check::check2()
{
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
// * emptiness_check::h, a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * num, the number of visited nodes. Used to set the order of each
// visited node,
int num = 1;
// * todo, the depth-first search stack. This holds pairs of the
// form (STATE, SUCCESSORS) where SUCCESSORS is a list of
// (ACCEPTANCE_CONDITIONS, STATE) pairs.
typedef std::list<successor> succ_queue;
typedef std::pair<const state*, succ_queue> pair_state_successors;
std::stack<pair_state_successors> todo;
// Setup depth-first search from the initial state.
todo.push(pair_state_successors(0, succ_queue()));
todo.top().second.push_front(successor(bddtrue, aut_->get_init_state()));
for (;;)
{
assert(root.size() == arc.size());
// Get the successors of the current state.
succ_queue& queue = todo.top().second;
// First, we process all successors that we have already seen.
// This is an idea from Soheib Baarir. It helps to merge SCCs
// and get shorter traces faster.
succ_queue::iterator q = queue.begin();
while (q != queue.end())
{
hash_type::iterator i = h.find(q->s);
if (i == h.end())
{
// Skip unknown states.
++q;
continue;
}
// Skip states from dead SCCs.
if (i->second != -1)
{
// Now this is the most interesting case. We have
// reached a state S1 which is already part of a
// non-dead SCC. Any such non-dead SCC has
// necessarily been crossed by our path to this
// state: there is a state S2 in our path which
// belongs to this SCC too. We are going to merge
// all states between this S1 and S2 into this
// SCC.
//
// This merge is easy to do because the order of
// the SCC in ROOT is ascending: we just have to
// merge all SCCs from the top of ROOT that have
// an index greater to the one of the SCC of S2
// (called the "threshold").
int threshold = i->second;
bdd acc = q->acc;
while (threshold < root.top().index)
{
assert(!root.empty());
assert(!arc.empty());
acc |= root.top().condition;
acc |= arc.top();
root.pop();
arc.pop();
}
// Note that we do not always have
// threshold == root.top().index
// after this loop, the SCC whose index is threshold
// might have been merged with a lower SCC.
// Accumulate all acceptance conditions into the
// merged SCC.
root.top().condition |= acc;
if (root.top().condition == aut_->all_acceptance_conditions())
{
// We have found an accepting SCC. Clean up TODO.
// We must delete all states of apparing in TODO
// unless they are used as keys in H.
while (!todo.empty())
{
succ_queue& queue = todo.top().second;
for (succ_queue::iterator q = queue.begin();
q != queue.end(); ++q)
{
hash_type::iterator i = h.find(q->s);
if (i == h.end() || i->first != q->s)
delete q->s;
}
todo.pop();
}
return false;
}
}
// We know the state exists. Since a state can have several
// representations (i.e., objects), make sure we delete
// anything but the first one seen (the one used as key in H).
if (q->s != i->first)
delete q->s;
// Remove that state from the queue, so we do not
// recurse into it.
succ_queue::iterator old = q++;
queue.erase(old);
}
// If there is no more successor, backtrack.
if (queue.empty())
{
// We have explored all successors of state CURR.
const state* curr = todo.top().first;
// Backtrack TODO.
todo.pop();
if (todo.empty())
// This automaton recognizes no word.
return true;
// When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC.
hash_type::iterator i = h.find(curr);
assert(i != h.end());
assert(!root.empty());
if (root.top().index == i->second)
{
assert(!arc.empty());
arc.pop();
root.pop();
remove_component(curr);
}
continue;
}
// Recurse. (Finally!)
// Pick one successor off the list, and schedule its
// successors first on TODO. Update the various hashes and
// stacks.
successor succ = queue.front();
queue.pop_front();
h[succ.s] = ++num;
root.push(connected_component(num));
arc.push(succ.acc);
todo.push(pair_state_successors(succ.s, succ_queue()));
succ_queue& new_queue = todo.top().second;
tgba_succ_iterator* iter = aut_->succ_iter(succ.s);
for (iter->first(); ! iter->done(); iter->next())
new_queue.push_back(successor(iter->current_acceptance_conditions(),
iter->current_state()));
delete iter;
}
}
std::ostream&
emptiness_check::print_result(std::ostream& os, const tgba* restrict) const

1
src/tgbaalgos/emptinesscheck.hh
View file

@ -64,6 +64,7 @@ namespace spot
/// This function returns true if the automata's language is empty,
/// and builds a stack of SCC.
bool check();
bool check2();
/// Compute a counter example if tgba_emptiness_check() returned false.
void counter_example();

8
src/tgbatest/emptchk.test
View file

@ -31,6 +31,10 @@ expect_ce()
run 0 ./ltl2tgba -e -D "$1"
run 0 ./ltl2tgba -e -f "$1"
run 0 ./ltl2tgba -e -f -D "$1"
run 0 ./ltl2tgba -e2 "$1"
run 0 ./ltl2tgba -e2 -D "$1"
run 0 ./ltl2tgba -e2 -f "$1"
run 0 ./ltl2tgba -e2 -f -D "$1"
run 0 ./ltl2tgba -m "$1"
run 0 ./ltl2tgba -m -f "$1"
}
@ -41,6 +45,10 @@ expect_no()
run 0 ./ltl2tgba -E -D "$1"
run 0 ./ltl2tgba -E -f "$1"
run 0 ./ltl2tgba -E -f -D "$1"
run 0 ./ltl2tgba -E2 "$1"
run 0 ./ltl2tgba -E2 -D "$1"
run 0 ./ltl2tgba -E2 -f "$1"
run 0 ./ltl2tgba -E2 -f -D "$1"
run 0 ./ltl2tgba -M "$1"
run 0 ./ltl2tgba -M -f "$1"
}

1
src/tgbatest/emptchke.test
View file

@ -33,4 +33,5 @@ s1, "s2", "a & !b", c d;
EOF
run 0 ./ltl2tgba -e -X input
run 0 ./ltl2tgba -e2 -X input
run 0 ./ltl2tgba -m -X input

27
src/tgbatest/ltl2tgba.cc
View file

@ -32,8 +32,12 @@ syntax(char* prog)
<< " -D degeneralize the automaton" << std::endl
<< " -e emptiness-check (Couvreur), expect and compute "
<< "a counter-example" << std::endl
<< " -e2 emptiness-check (Couvreur variant), expect and compute "
<< "a counter-example" << std::endl
<< " -E emptiness-check (Couvreur), expect no counter-example "
<< std::endl
<< " -E2 emptiness-check (Couvreur variant), expect no "
<< "counter-example " << std::endl
<< " -f use Couvreur's FM algorithm for translation"
<< std::endl
<< " -F read the formula from the file" << std::endl
@ -69,7 +73,7 @@ main(int argc, char** argv)
bool file_opt = false;
int output = 0;
int formula_index = 0;
enum { None, Couvreur, MagicSearch } echeck = None;
enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
bool magic_many = false;
bool expect_counter_example = false;
@ -104,12 +108,24 @@ main(int argc, char** argv)
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-e2"))
{
echeck = Couvreur2;
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-E"))
{
echeck = Couvreur;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-E2"))
{
echeck = Couvreur2;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-f"))
{
fm_opt = true;
@ -290,9 +306,16 @@ main(int argc, char** argv)
case None:
break;
case Couvreur:
case Couvreur2:
{
spot::emptiness_check ec = spot::emptiness_check(a);
bool res = ec.check();
bool res;
if (echeck == Couvreur)
res = ec.check();
else
res = ec.check2();
if (expect_counter_example)
{
if (res)