Commit f52082bc authored by Denis Poitrenaud's avatar Denis Poitrenaud

* src/tgbaalgos/magic.cc: rewrite to externalize the heap and

prepare it to a bit state hashing version.
* src/tgbaalgos/magic.hh: adapt to the new interface of
magic_search and se05_search.
* src/tgbaalgos/se05.cc: new file.
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
* src/tgbatest/emptchk.test: more tests.
* src/tgbatest/dfs.test: new file.
* src/tgbatest/Makefile.am: Add it.
parent 908b6129
2004-11-09 Poitrenaud Denis <denis@src.lip6.fr>
* src/tgbaalgos/magic.cc: rewrite to externalize the heap and
prepare it to a bit state hashing version.
* src/tgbaalgos/magic.hh: adapt to the new interface of
magic_search and se05_search.
* src/tgbaalgos/se05.cc: new file.
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
* src/tgbatest/emptchk.test: more tests.
* src/tgbatest/dfs.test: new file.
* src/tgbatest/Makefile.am: Add it.
2004-11-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness.cc (print_tgba_run): Output the
......
......@@ -62,6 +62,7 @@ libtgbaalgos_la_SOURCES = \
replayrun.cc \
rundotdec.cc \
save.cc \
se05.cc \
stats.cc \
reductgba_sim.cc \
reductgba_sim_del.cc
......
This diff is collapsed.
......@@ -22,107 +22,148 @@
#ifndef SPOT_TGBAALGOS_MAGIC_HH
# define SPOT_TGBAALGOS_MAGIC_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include "tgba/tgbatba.hh"
#include "tgba/tgba.hh"
#include "emptiness.hh"
namespace spot
{
/// \brief Emptiness check on spot::tgba_tba_proxy automata using
/// the Magic Search algorithm.
/// \brief Returns an emptiness check on the spot::tgba automaton \a a.
///
/// \pre The automaton \a a must have at most one accepting condition (i.e.
/// it is a TBA).
///
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The method visits only a finite set of accepting paths.
///
/// The implemented algorithm is the following.
///
/// This algorithm comes from
/// \verbatim
/// @InProceedings{ godefroid.93.pstv,
/// author = {Patrice Godefroid and Gerard .J. Holzmann},
/// title = {On the verification of temporal properties},
/// booktitle = {Proceedings of the 13th IFIP TC6/WG6.1 International
/// Symposium on Protocol Specification, Testing, and
/// Verification (PSTV'93)},
/// month = {May},
/// editor = {Andr{\'e} A. S. Danthine and Guy Leduc
/// and Pierre Wolper},
/// address = {Liege, Belgium},
/// pages = {109--124},
/// publisher = {North-Holland},
/// year = {1993},
/// series = {IFIP Transactions},
/// volume = {C-16},
/// isbn = {0-444-81648-8}
/// }
/// procedure nested_dfs ()
/// begin
/// call dfs_blue(s0);
/// end;
///
/// procedure dfs_blue (s)
/// begin
/// s.color = blue;
/// for all t in post(s) do
/// if t.color == white then
/// call dfs_blue(t);
/// end if;
/// if (the edge (s,t) is accepting) then
/// target = s;
/// call dfs_red(t);
/// end if;
/// end for;
/// end;
///
/// procedure dfs_red(s)
/// begin
/// s.color = red;
/// if s == target then
/// report cycle
/// end if;
/// for all t in post(s) do
/// if t.color != red then
/// call dfs_red(t);
/// end if;
/// end for;
/// end;
/// \endverbatim
struct magic_search : public emptiness_check
{
/// Initialize the Magic Search algorithm on the automaton \a a.
magic_search(const tgba_tba_proxy *a);
virtual ~magic_search();
/// \brief Perform a Magic Search.
///
/// \return true iff the algorithm has found a new accepting
/// path.
///
/// check() can be called several times until it return false,
/// to enumerate all accepting paths.
virtual emptiness_check_result* check();
private:
// The names "stack", "h", and "x", are those used in the paper.
/// \brief Records whether a state has be seen with the magic bit
/// on or off.
struct magic
{
bool seen_without : 1;
bool seen_with : 1;
};
/// \brief A state for the spot::magic_search algorithm.
struct magic_state
{
const state* s;
bool m; ///< The state of the magic demon.
};
typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
typedef std::pair<bdd, bdd> tstack_item;
typedef std::list<tstack_item> tstack_type;
/// \brief Stack of transitions.
///
/// This is an addition to the data from the paper.
tstack_type tstack;
typedef Sgi::hash_map<const state*, magic,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// Append a new state to the current path.
void push(const state* s, bool m);
/// Check whether we already visited \a s with the Magic bit set to \a m.
bool has(const state* s, bool m) const;
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
///
/// It is an adaptation to TBA of the Magic Search algorithm
/// which deals with accepting states and is presented in
///
/// \verbatim
/// Article{ courcoubertis.92.fmsd,
/// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
/// Wolper and Mihalis Yannakakis},
/// title = {Memory-Efficient Algorithm for the Verification of
/// Temporal Properties},
/// journal = {Formal Methods in System Design},
/// pages = {275--288},
/// year = {1992},
/// volume = {1}
/// }
/// \endverbatim
emptiness_check* explicit_magic_search(const tgba *a);
#ifndef SWIG
class result: public emptiness_check_result
{
public:
result(magic_search& ms);
virtual tgba_run* accepting_run();
private:
magic_search& ms_;
};
#endif // SWIG
};
/// \brief Returns an emptiness check on the spot::tgba automaton \a a.
///
/// \pre The automaton \a a must have at most one accepting condition (i.e.
/// it is a TBA).
///
/// The method \a check() of the returned checker can be called several times
/// (until it returns a null pointer) to enumerate all the visited accepting
/// paths. The method visits only a finite set of accepting paths.
///
/// The implemented algorithm is the following:
///
/// procedure nested_dfs ()
/// begin
/// weight = 0;
/// call dfs_blue(s0);
/// end;
///
/// procedure dfs_blue (s)
/// begin
/// s.color = cyan;
/// s.weight = weight;
/// for all t in post(s) do
/// if t.color == white then
/// if the edge (s,t) is accepting then
/// weight = weight + 1;
/// end if;
/// call dfs_blue(t);
/// if the edge (s,t) is accepting then
/// weight = weight - 1;
/// end if;
/// else if t.color == cyan and
/// (the edge (s,t) is accepting or
/// weight > t.weight) then
/// report cycle;
/// end if;
/// if the edge (s,t) is accepting then
/// call dfs_red(t);
/// end if;
/// end for;
/// s.color = blue;
/// end;
///
/// procedure dfs_red(s)
/// begin
/// if s.color == cyan then
/// report cycle;
/// end if;
/// s.color = red;
/// for all t in post(s) do
/// if t.color != red then
/// call dfs_red(t);
/// end if;
/// end for;
/// end;
///
/// It is an adaptation to TBA and an extension of the one
/// presented in
/// \verbatim
/// InProceedings{ schwoon.05.tacas,
/// author = {Stephan Schwoon and Javier Esparza},
/// title = {A Note on On-The-Fly Verification Algorithms},
/// booktitle = {TACAS'05},
/// pages = {},
/// year = {2005},
/// volume = {},
/// series = {LNCS},
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
///
/// the extention consists in the introduction of a weight associated
/// to each state in the blue stack. The weight represents the number of
/// accepting arcs traversed to reach it from the initial state.
///
emptiness_check* explicit_se05_search(const tgba *a);
}
......
This diff is collapsed.
......@@ -80,9 +80,14 @@ TESTS = \
reduccmp.test \
reductgba.test \
emptchk.test \
magic.test \
se05.test \
emptchke.test \
dfs.test \
spotlbtt.test
EXTRA_DIST = $(TESTS) ltl2baw.pl
CLEANFILES = input input1 input2 input3 stdout expected config output1 output2
CLEANFILES = input input1 input2 input3 stdout expected config output1 output2 \
red blue_counter blue_last
#!/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
cat >blue_counter <<'EOF'
acc = a;
s1, s2,, a;
s2, s3,,;
s3, s1,,;
s3, s4,,;
s4, s4,,;
s4, s5,,;
s4, s6,,;
s4, s7,,;
s4, s8,,;
s4, s9,,;
s5, s4,,;
s5, s5,,;
s5, s6,,;
s5, s7,,;
s5, s8,,;
s5, s9,,;
s6, s4,,;
s6, s5,,;
s6, s6,,;
s6, s7,,;
s6, s8,,;
s6, s9,,;
s7, s4,,;
s7, s5,,;
s7, s6,,;
s7, s7,,;
s7, s8,,;
s7, s9,,;
s8, s4,,;
s8, s5,,;
s8, s6,,;
s8, s7,,;
s8, s8,,;
s8, s9,,;
s9, s4,,;
s9, s5,,;
s9, s6,,;
s9, s7,,;
s9, s8,,;
s9, s9,,;
EOF
run 0 ./ltl2tgba -emagic_search -X blue_counter
run 0 ./ltl2tgba -ese05_search -X blue_counter
cat >blue_last <<'EOF'
acc = a;
s1, s2,,;
s2, s3,,;
s3, s1,, a;
s3, s4,,;
s4, s4,,;
s4, s5,,;
s4, s6,,;
s4, s7,,;
s4, s8,,;
s4, s9,,;
s5, s4,,;
s5, s5,,;
s5, s6,,;
s5, s7,,;
s5, s8,,;
s5, s9,,;
s6, s4,,;
s6, s5,,;
s6, s6,,;
s6, s7,,;
s6, s8,,;
s6, s9,,;
s7, s4,,;
s7, s5,,;
s7, s6,,;
s7, s7,,;
s7, s8,,;
s7, s9,,;
s8, s4,,;
s8, s5,,;
s8, s6,,;
s8, s7,,;
s8, s8,,;
s8, s9,,;
s9, s4,,;
s9, s5,,;
s9, s6,,;
s9, s7,,;
s9, s8,,;
s9, s9,,;
EOF
run 0 ./ltl2tgba -emagic_search -X blue_last
run 0 ./ltl2tgba -ese05_search -X blue_last
cat >red <<'EOF'
acc = a;
s1, s2,,;
s1, s3,, a;
s2, s3,,;
s3, s1,,;
s3, s4,,;
s4, s4,,;
s4, s5,,;
s4, s6,,;
s4, s7,,;
s4, s8,,;
s4, s9,,;
s5, s4,,;
s5, s5,,;
s5, s6,,;
s5, s7,,;
s5, s8,,;
s5, s9,,;
s6, s4,,;
s6, s5,,;
s6, s6,,;
s6, s7,,;
s6, s8,,;
s6, s9,,;
s7, s4,,;
s7, s5,,;
s7, s6,,;
s7, s7,,;
s7, s8,,;
s7, s9,,;
s8, s4,,;
s8, s5,,;
s8, s6,,;
s8, s7,,;
s8, s8,,;
s8, s9,,;
s9, s4,,;
s9, s5,,;
s9, s6,,;
s9, s7,,;
s9, s8,,;
s9, s9,,;
EOF
run 0 ./ltl2tgba -emagic_search -X red
run 0 ./ltl2tgba -ese05_search -X red
rm -f red blue_counter blue_last
\ No newline at end of file
......@@ -43,6 +43,11 @@ expect_ce()
expect_ce_do -ecouvreur99_shy -f -D "$1"
expect_ce_do -emagic_search "$1"
expect_ce_do -emagic_search -f "$1"
run 0 ./ltl2tgba -ese05_search "$1"
run 0 ./ltl2tgba -ese05_search -f "$1"
# Expect multiple accepting runs
test `./ltl2tgba -emagic_search_repeated "$1" | grep Prefix: | wc -l` -ge $2
test `./ltl2tgba -ese05_search_repeated "$1" | grep Prefix: | wc -l` -ge $2
}
expect_no()
......@@ -57,22 +62,24 @@ expect_no()
run 0 ./ltl2tgba -Ecouvreur99_shy -f -D "$1"
run 0 ./ltl2tgba -Emagic_search "$1"
run 0 ./ltl2tgba -Emagic_search -f "$1"
run 0 ./ltl2tgba -Ese05_search "$1"
run 0 ./ltl2tgba -Ese05_search -f "$1"
test `./ltl2tgba -emagic_search_repeated "!($1)" |
grep Prefix: | wc -l` -ge $2
test `./ltl2tgba -ese05_search_repeated "!($1)" |
grep Prefix: | wc -l` -ge $2
}
expect_ce 'a'
expect_ce 'a U b'
expect_ce 'X a'
expect_ce 'a & b & c'
expect_ce 'a | b | (c U (d & (g U (h ^ i))))'
expect_ce 'Xa & (b U !a) & (b U !a)'
expect_ce 'Fa & Xb & GFc & Gd'
expect_ce 'Fa & Xa & GFc & Gc'
expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
expect_ce '!((FF a) <=> (F x))'
expect_no '!((FF a) <=> (F a))'
expect_no 'Xa && (!a U b) && !b && X!b'
expect_no '(a U !b) && Gb'
# Expect at least four accepting runs
test `./ltl2tgba -emagic_search_repeated 'FFx <=> Fx' |
grep Prefix: | wc -l` -ge 4
expect_ce 'a' 1
expect_ce 'a U b' 2
expect_ce 'X a' 1
expect_ce 'a & b & c' 1
expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 2
expect_ce 'Xa & (b U !a) & (b U !a)' 1
expect_ce 'Fa & Xb & GFc & Gd' 1
expect_ce 'Fa & Xa & GFc & Gc' 2
expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1
expect_ce '!((FF a) <=> (F x))' 3
expect_no '!((FF a) <=> (F a))' 4
expect_no 'Xa && (!a U b) && !b && X!b' 5
expect_no '(a U !b) && Gb' 4
......@@ -119,7 +119,9 @@ syntax(char* prog)
<< " couvreur99 (the default)" << std::endl
<< " couvreur99_shy" << std::endl
<< " magic_search" << std::endl
<< " magic_search_repeated" << std::endl;
<< " magic_search_repeated" << std::endl
<< " se05_search" << std::endl
<< " se05_search_repeated" << std::endl;
exit(2);
}
......@@ -137,7 +139,7 @@ main(int argc, char** argv)
int output = 0;
int formula_index = 0;
std::string echeck_algo;
enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
enum { None, Couvreur, Couvreur2, MagicSearch, Se04Search } echeck = None;
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
bool magic_many = false;
bool expect_counter_example = false;
......@@ -347,6 +349,17 @@ main(int argc, char** argv)
degeneralize_opt = true;
magic_many = true;
}
else if (echeck_algo == "se05_search")
{
echeck = Se04Search;
degeneralize_opt = true;
}
else if (echeck_algo == "se05_search_repeated")
{
echeck = Se04Search;
degeneralize_opt = true;
magic_many = true;
}
else
{
std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl;
......@@ -569,7 +582,12 @@ main(int argc, char** argv)
case MagicSearch:
ec_a = degeneralized;
ec = new spot::magic_search(degeneralized);
ec = spot::explicit_magic_search(degeneralized);
break;
case Se04Search:
ec_a = degeneralized;
ec = spot::explicit_se05_search(degeneralized);
break;
}
......
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