Commit 782ba001 authored by Ala-Eddine Ben-Salem's avatar Ala-Eddine Ben-Salem Committed by Alexandre Duret-Lutz
Browse files

Add a new form of TA with a Single-pass emptiness check (STA)

* src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/taproduct.cc,src/ta/taproduct.hh,
src/taalgos/dotty.cc, src/taalgos/emptinessta.cc,
src/taalgos/emptinessta.hh, src/taalgos/minimize.cc,
src/taalgos/reachiter.cc, src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Impacts of the
implementation of a new variant of TA, called STA, which involve a
Single-pass emptiness check. The new options (-in and -lv) added to
build the new variants of TA allow to add two artificial states:
1- an initial artificial state to have an unique initial state (-in)
2- a livelock artificial state which has no successors in order to
obtain the new form of TA which requires only a Single-pass emptiness-
check: STA (-lv).
parent 310973f8
......@@ -19,13 +19,16 @@
// 02111-1307, USA.
#include "ta.hh"
namespace spot
{
spot::state*
ta::get_artificial_initial_state() const
{
return 0;
}
scc_stack_ta::connected_component::connected_component(int i)
{
......@@ -76,5 +79,4 @@ namespace spot
return s.empty();
}
}
......@@ -49,6 +49,9 @@ namespace spot
virtual const states_set_t
get_initial_states_set() const = 0;
virtual spot::state*
get_artificial_initial_state() const = 0;
virtual ta_succ_iterator*
succ_iter(const spot::state* s) const = 0;
......@@ -67,6 +70,7 @@ namespace spot
virtual bool
is_livelock_accepting_state(const spot::state* s) const = 0;
virtual bool
is_initial_state(const spot::state* s) const = 0;
......
......@@ -64,7 +64,8 @@ namespace spot
bool
ta_explicit_succ_iterator::done() const
{
return transitions_ == 0 || i_ == transitions_->end();
return transitions_ == 0 || transitions_->empty() || i_
== transitions_->end();
}
state*
......@@ -122,8 +123,6 @@ namespace spot
if (transitions_ == 0)
transitions_ = new transitions;
transitions_->push_back(t);
transitions* transitions_condition = get_transitions(t->condition);
if (transitions_condition == 0)
......@@ -132,7 +131,24 @@ namespace spot
transitions_by_condition[(t->condition).id()] = transitions_condition;
}
state_ta_explicit::transitions::iterator it_trans;
bool transition_found = false;
for (it_trans = transitions_condition->begin(); (it_trans
!= transitions_condition->end() && !transition_found); it_trans++)
{
transition_found = ((*it_trans)->dest == t->dest);
}
if (!transition_found)
{
transitions_condition->push_back(t);
transitions_->push_back(t);
}
else
{
delete t;
}
}
......@@ -185,6 +201,13 @@ namespace spot
is_initial_state_ = is_initial_state;
}
bool
state_ta_explicit::is_hole_state() const
{
state_ta_explicit::transitions* trans = get_transitions();
return trans == 0 || trans->empty();
}
int
state_ta_explicit::compare(const spot::state* other) const
{
......@@ -196,7 +219,16 @@ namespace spot
if (compare_value != 0)
return compare_value;
return tgba_condition_.id() - o->tgba_condition_.id();
compare_value = tgba_condition_.id() - o->tgba_condition_.id();
// if (compare_value != 0)
// return compare_value;
//
// //unique artificial_livelock_accepting_state
// if (o->is_the_artificial_livelock_accepting_state())
// return is_the_artificial_livelock_accepting_state();
return compare_value;
}
size_t
......@@ -266,7 +298,6 @@ namespace spot
delete *it_trans;
}
delete trans;
get_tgba_state()->destroy();
Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i =
transitions_by_condition.begin();
......@@ -282,10 +313,17 @@ namespace spot
// ta_explicit
ta_explicit::ta_explicit(const tgba* tgba_) :
tgba_(tgba_)
ta_explicit::ta_explicit(const tgba* tgba_,
state_ta_explicit* artificial_initial_state) :
tgba_(tgba_), artificial_initial_state_(artificial_initial_state)
{
get_dict()->register_all_variables_of(&tgba_, this);
if (artificial_initial_state != 0)
{
state_ta_explicit* is = add_state(artificial_initial_state);
assert(is == artificial_initial_state);
}
}
ta_explicit::~ta_explicit()
......@@ -296,6 +334,7 @@ namespace spot
state_ta_explicit* s = down_cast<state_ta_explicit*> (*it);
s->free_transitions();
s->get_tgba_state()->destroy();
delete s;
}
get_dict()->unregister_all_my_variables(this);
......@@ -313,13 +352,19 @@ namespace spot
}
void
ta_explicit::add_to_initial_states_set(state* state)
ta_explicit::add_to_initial_states_set(state* state, bdd condition)
{
state_ta_explicit * s = down_cast<state_ta_explicit*> (state);
assert(s);
s->set_initial_state(true);
if (condition == bddfalse)
condition = get_state_condition(s);
std::pair<ta::states_set_t::iterator, bool> add_state =
initial_states_set_.insert(s);
if (get_artificial_initial_state() != 0)
if (add_state.second)
create_transition((state_ta_explicit*) get_artificial_initial_state(),
condition, s);
}
......@@ -329,7 +374,8 @@ namespace spot
state_ta_explicit * state = down_cast<state_ta_explicit*> (s);
assert(state);
state->delete_stuttering_and_hole_successors();
if (state->is_initial_state()) add_to_initial_states_set(state);
if (state->is_initial_state())
add_to_initial_states_set(state);
}
......
......@@ -41,7 +41,8 @@ namespace spot
class ta_explicit : public ta
{
public:
ta_explicit(const tgba* tgba_);
ta_explicit(const tgba* tgba_, state_ta_explicit* artificial_initial_state =
0);
const tgba*
get_tgba() const;
......@@ -50,7 +51,7 @@ namespace spot
add_state(state_ta_explicit* s);
void
add_to_initial_states_set(state* s);
add_to_initial_states_set(state* s, bdd condition = bddfalse);
void
create_transition(state_ta_explicit* source, bdd condition,
......@@ -91,9 +92,28 @@ namespace spot
virtual void
free_state(const spot::state* s) const;
spot::state*
get_artificial_initial_state() const
{
return (spot::state*) artificial_initial_state_;
}
void
set_artificial_initial_state(state_ta_explicit* s)
{
artificial_initial_state_ = s;
}
virtual void
delete_stuttering_and_hole_successors(spot::state* s);
ta::states_set_t
get_states_set()
{
return states_set_;
}
private:
// Disallow copy.
ta_explicit(const ta_explicit& other);
......@@ -103,6 +123,7 @@ namespace spot
ta::states_set_t states_set_;
ta::states_set_t initial_states_set_;
const tgba* tgba_;
state_ta_explicit* artificial_initial_state_;
};
......@@ -122,7 +143,8 @@ namespace spot
state_ta_explicit(const state* tgba_state, const bdd tgba_condition,
bool is_initial_state = false, bool is_accepting_state = false,
bool is_livelock_accepting_state = false, transitions* trans = 0) :
bool is_livelock_accepting_state = false, transitions* trans = 0,
bool is_the_artificial_livelock_accepting_state = false) :
tgba_state_(tgba_state), tgba_condition_(tgba_condition),
is_initial_state_(is_initial_state), is_accepting_state_(
is_accepting_state), is_livelock_accepting_state_(
......@@ -164,10 +186,15 @@ namespace spot
is_livelock_accepting_state() const;
void
set_livelock_accepting_state(bool is_livelock_accepting_state);
bool
is_initial_state() const;
void
set_initial_state(bool is_initial_state);
bool
is_hole_state() const;
void
delete_stuttering_and_hole_successors();
......
// Copykripke_structure (C) 2010 Laboratoire de Recherche et Developpement
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
// de l Epita (LRDE).
//
//
......@@ -138,7 +138,7 @@ namespace spot
== kripke_current_dest_condition);
if (is_stuttering_transition_)
{
current_condition_ = bddtrue;
current_condition_ = bddfalse;
}
else
{
......@@ -274,7 +274,7 @@ namespace spot
{
//build initial states set
const ta::states_set_t ta_init_states_set = ta_->get_initial_states_set();
ta::states_set_t ta_init_states_set;
ta::states_set_t::const_iterator it;
ta::states_set_t initial_states_set;
......@@ -282,10 +282,29 @@ namespace spot
bdd kripke_init_state_condition = kripke_->state_condition(
kripke_init_state);
spot::state* artificial_initial_state = ta_->get_artificial_initial_state();
if (artificial_initial_state != 0)
{
ta_succ_iterator* ta_init_it_ = ta_->succ_iter(
artificial_initial_state, kripke_init_state_condition);
for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next())
{
ta_init_states_set.insert(ta_init_it_->current_state());
}
delete ta_init_it_;
}
else
{
ta_init_states_set = ta_->get_initial_states_set();
}
for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++)
{
if (kripke_init_state_condition == (ta_->get_state_condition(*it)))
if ((artificial_initial_state != 0) || (kripke_init_state_condition
== ta_->get_state_condition(*it)))
{
state_ta_product* stp = new state_ta_product((*it),
kripke_init_state->clone());
......@@ -341,6 +360,13 @@ namespace spot
return ta_->is_livelock_accepting_state(stp->get_ta_state());
}
spot::state*
ta_product::get_artificial_initial_state() const
{
return 0;
}
//TODO BUG FIX
bool
ta_product::is_initial_state(const spot::state* s) const
{
......@@ -356,6 +382,16 @@ namespace spot
== (ta_->get_state_condition(ta_s)));
}
bool
ta_product::is_hole_state_in_ta_component(const spot::state* s) const
{
const state_ta_product* stp = down_cast<const state_ta_product*> (s);
ta_succ_iterator* ta_succ_iter = get_ta()->succ_iter(stp->get_ta_state());
bool is_hole_state = ta_succ_iter->done();
delete ta_succ_iter;
return is_hole_state;
}
bdd
ta_product::get_state_condition(const spot::state* s) const
{
......
......@@ -164,15 +164,34 @@ namespace spot
virtual bool
is_livelock_accepting_state(const spot::state* s) const;
virtual spot::state*
get_artificial_initial_state() const;
virtual bool
is_initial_state(const spot::state* s) const;
virtual bool
is_hole_state_in_ta_component(const spot::state* s) const;
virtual bdd
get_state_condition(const spot::state* s) const;
virtual void
free_state(const spot::state* s) const;
const ta*
get_ta() const
{
return ta_;
}
const kripke*
get_kripke() const
{
return kripke_;
}
private:
bdd_dict* dict_;
const ta* ta_;
......
......@@ -43,10 +43,24 @@ namespace spot
os_ << "digraph G {" << std::endl;
int n = 0;
const ta::states_set_t init_states_set =
t_automata_->get_initial_states_set();
spot::state* artificial_initial_state =
t_automata_->get_artificial_initial_state();
ta::states_set_t init_states_set;
ta::states_set_t::const_iterator it;
if (artificial_initial_state != 0)
{
init_states_set.insert(artificial_initial_state);
}
else
{
init_states_set = t_automata_->get_initial_states_set();
}
for (it = (init_states_set.begin()); it != init_states_set.end(); it++)
{
// cout << (*it).first << " => " << (*it).second << endl;
......@@ -60,6 +74,7 @@ namespace spot
+ "\"]" << std::endl;
}
}
void
......
......@@ -18,7 +18,7 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
// #define TRACE
//#define TRACE
#include <iostream>
#ifdef TRACE
......@@ -34,7 +34,7 @@
namespace spot
{
ta_check::ta_check(const ta* a, option_map o) :
ta_check::ta_check(const ta_product* a, option_map o) :
a_(a), o_(o)
{
is_full_2_pass_ = o.get("is_full_2_pass", 0);
......@@ -46,7 +46,7 @@ namespace spot
}
bool
ta_check::check()
ta_check::check(bool disable_second_pass)
{
// We use five main data in this algorithm:
......@@ -75,23 +75,21 @@ namespace spot
trace
<< "PASS 1" << std::endl;
//const std::string WHITE = "W";
//const std::string GREY = "G";
//const std::string BLUE = "B";
//const std::string BLACK = "BK";
Sgi::hash_map<const state*, std::set<const state*, state_ptr_less_than>,
state_ptr_hash, state_ptr_equal> liveset;
std::stack<spot::state*> livelock_roots;
bool livelock_acceptance_states_not_found = true;
const ta::states_set_t init_states_set = a_->get_initial_states_set();
ta::states_set_t::const_iterator it;
for (it = init_states_set.begin(); it != init_states_set.end(); it++)
{
state* init_state = (*it);
init_set.push(init_state);
//colour[init_state] = WHITE;
}
......@@ -114,7 +112,7 @@ namespace spot
ta_succ_iterator* iter = a_->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
//colour[init] = GREY;
inc_depth();
//push potential root of live-lock accepting cycle
......@@ -143,6 +141,14 @@ namespace spot
trace
<< "PASS 1 : backtrack" << std::endl;
if (a_->is_livelock_accepting_state(curr))
{
livelock_acceptance_states_not_found = false;
trace
<< "PASS 1 : livelock accepting state found" << std::endl;
}
// fill rem with any component removed,
numbered_state_heap::state_index_p spi =
h->index(curr->clone());
......@@ -195,9 +201,14 @@ namespace spot
// Fetch the values destination state we are interested in...
state* dest = succ->current_state();
//may be Buchi accepting scc
scc.top().is_accepting = a_->is_accepting_state(curr)
&& !succ->is_stuttering_transition();
bool curr_is_livelock_hole_state_in_ta_component =
(a_->is_hole_state_in_ta_component(curr))
&& a_->is_livelock_accepting_state(curr);
//may be Buchi accepting scc or livelock accepting state (contains a TA hole and livelock accepting state)
scc.top().is_accepting = (a_->is_accepting_state(curr)
&& !succ->is_stuttering_transition())
|| curr_is_livelock_hole_state_in_ta_component;
bool is_stuttering_transition = succ->is_stuttering_transition();
......@@ -320,6 +331,10 @@ namespace spot
}
clear(h, todo, init_set);
if (disable_second_pass || livelock_acceptance_states_not_found)
return false;
return livelock_detection(a_);
}
......@@ -378,8 +393,6 @@ namespace spot
// * init: the set of the depth-first search initial states
std::stack<spot::state*> init_set;
const ta::states_set_t init_states_set = a_->get_initial_states_set();
ta::states_set_t::const_iterator it;
for (it = init_states_set.begin(); it != init_states_set.end(); it++)
......@@ -387,10 +400,8 @@ namespace spot
state* init_state = (*it);
init_set.push(init_state);
}
while (!init_set.empty())
{
// Setup depth-first search from initial states.
......
......@@ -24,7 +24,7 @@
#ifndef SPOT_TAALGOS_EMPTINESS_HH
# define SPOT_TAALGOS_EMPTINESS_HH
#include "ta/ta.hh"
#include "ta/taproduct.hh"
#include "misc/optionmap.hh"
#include "tgbaalgos/gtec/nsheap.hh"
#include "tgbaalgos/emptiness_stats.hh"
......@@ -43,13 +43,13 @@ namespace spot
class ta_check : public ec_statistics
{
public:
ta_check(const ta* a, option_map o = option_map());
ta_check(const ta_product* a, option_map o = option_map());
virtual
~ta_check();
/// Check whether the automaton's language is empty.
virtual bool
check();
check(bool disable_second_pass = false);
virtual bool
livelock_detection(const ta* t);
......@@ -75,7 +75,7 @@ namespace spot
heuristic_livelock_detection(const state * stuttering_succ,
numbered_state_heap* h, int h_livelock_root, std::set<const state*,
state_ptr_less_than> liveset_curr);
const ta* a_; ///< The automaton.
const ta_product* a_; ///< The automaton.
option_map o_; ///< The options
bool is_full_2_pass_;
......
......@@ -106,7 +106,7 @@ namespace spot
state* tgba_state = tgba->add_state(src_num);
bdd tgba_condition = bddtrue;
bool is_initial_state = a->is_initial_state(src);
if (is_initial_state)
if ((a->get_artificial_initial_state() == 0) && is_initial_state)
tgba_condition = a->get_state_condition(src);
bool is_accepting_state = a->is_accepting_state(src);
bool is_livelock_accepting_state = a->is_livelock_accepting_state(src);
......@@ -120,10 +120,16 @@ namespace spot
if (ta_src != new_src)
{
new_src->destroy();
tgba_state->destroy();
}
else if (a->get_artificial_initial_state() != 0)
{
if (a->get_artificial_initial_state() == src)
ta->set_artificial_initial_state(new_src);
}
else if (is_initial_state)
{
ta->add_to_initial_states_set(new_src);
}
ta_succ_iterator* succit = a->succ_iter(src);
......@@ -138,7 +144,7 @@ namespace spot
state* tgba_state = tgba->add_state(i->second);
bdd tgba_condition = bddtrue;
is_initial_state = a->is_initial_state(dst);
if (is_initial_state)
if ((a->get_artificial_initial_state() == 0) && is_initial_state)
tgba_condition = a->get_state_condition(dst);
bool is_accepting_state = a->is_accepting_state(dst);
bool is_livelock_accepting_state = a->is_livelock_accepting_state(
......@@ -153,8 +159,13 @@ namespace spot
if (ta_dst != new_dst)
{
new_dst->destroy();
tgba_state->destroy();
}
else if (a->get_artificial_initial_state() != 0)
{
if (a->get_artificial_initial_state() == dst)
ta->set_artificial_initial_state(new_dst);
}
else if (is_initial_state)
ta->add_to_initial_states_set(new_dst);
......@@ -196,11 +207,17 @@ namespace spot
std::set<const state*>::iterator it;
spot::state* artificial_initial_state = ta_->get_artificial_initial_state();
for (it = states_set.begin(); it != states_set.end(); it++)
{
const state* s = (*it);
if (ta_->is_initial_state(s))
if (s == artificial_initial_state)
{