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

New Automata: TGTA (Transition-based Generalized TA)

Browse source 
* src/ta/Makefile.am, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/tgbta.cc, src/ta/tgbta.hh,
src/ta/tgbtaexplicit.cc, src/ta/tgbtaexplicit.hh,
src/ta/tgbtaproduct.cc, src/ta/tgbtaproduct.hh,
src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/sba2ta.cc, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
src/tgbatest/ltl2tgba.cc: Implementation of TGTA, a new kind of automata
combining ideas from TGBA and TA.
This commit is contained in:
Ala-Eddine Ben-Salem 2011-11-23 12:24:25 +01:00 • committed by Alexandre Duret-Lutz
parent 1f0bf0b1cf
commit c882eadda6
16 changed files with 921 additions and 152 deletions
Download patch file Download diff file Expand all files Collapse all files

143
src/taalgos/emptinessta.cc
View file

@ -73,8 +73,7 @@ namespace spot
// it is also used as a key in H.
std::stack<pair_state_iter> todo;
// * init: the set of the depth-first search initial states
std::stack<spot::state*> init_set;
Sgi::hash_map<const state*, std::string, state_ptr_hash, state_ptr_equal>
colour;
@ -89,44 +88,44 @@ namespace spot
bool livelock_acceptance_states_not_found = true;
const ta::states_set_t init_states_set = a_->get_initial_states_set();
bool activate_heuristic = (is_full_2_pass_ == disable_second_pass);
ta::states_set_t::const_iterator it;
for (it = init_states_set.begin(); it != init_states_set.end(); it++)
// Setup depth-first search from initial states.
const ta* ta_ = a_->get_ta();
const kripke* kripke_ = a_->get_kripke();
state* kripke_init_state = kripke_->get_init_state();
bdd kripke_init_state_condition = kripke_->state_condition(
kripke_init_state);
spot::state* artificial_initial_state = ta_->get_artificial_initial_state();
ta_succ_iterator* ta_init_it_ = ta_->succ_iter(artificial_initial_state,
kripke_init_state_condition);
kripke_init_state->destroy();
for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next())
{
state* init_state = (*it);
init_set.push(init_state);
}
state_ta_product* init = new state_ta_product(
(ta_init_it_->current_state()), kripke_init_state->clone());
while (!init_set.empty())
{
// Setup depth-first search from initial states.
numbered_state_heap::state_index_p h_init = h->find(init);
{
state* init = init_set.top();
init_set.pop();
if (h_init.first)
continue;
numbered_state_heap::state_index_p h_init = h->find(init);
h->insert(init, ++num);
scc.push(num);
arc.push(bddfalse);
if (h_init.first)
continue;
ta_succ_iterator* iter = a_->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
h->insert(init, ++num);
scc.push(num);
arc.push(bddfalse);
inc_depth();
ta_succ_iterator* iter = a_->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
inc_depth();
//push potential root of live-lock accepting cycle
if (a_->is_livelock_accepting_state(init))
livelock_roots.push(init);
}
//push potential root of live-lock accepting cycle
if (activate_heuristic && a_->is_livelock_accepting_state(init))
livelock_roots.push(init);
while (!todo.empty())
{
@ -169,8 +168,8 @@ namespace spot
*spi.second = -std::abs(*spi.second);
// Backtrack livelock_roots.
if (!livelock_roots.empty() && !livelock_roots.top()->compare(
curr))
if (activate_heuristic && !livelock_roots.empty()
&& !livelock_roots.top()->compare(curr))
livelock_roots.pop();
// When backtracking the root of an SSCC, we must also
@ -249,7 +248,7 @@ namespace spot
inc_depth();
//push potential root of live-lock accepting cycle
if (a_->is_livelock_accepting_state(dest)
if (activate_heuristic && a_->is_livelock_accepting_state(dest)
&& !is_stuttering_transition)
livelock_roots.push(dest);
@ -276,7 +275,7 @@ namespace spot
bool acc = false;
trace
<< "***PASS 1: CYCLE***" << std::endl;
<< "***PASS 1: CYCLE***" << std::endl;
while (threshold < scc.top().index)
{
@ -309,27 +308,32 @@ namespace spot
if (is_accepting_sscc)
{
trace
<< "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " << a_->is_livelock_accepting_state(curr) << std::endl;
<< "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): "
<< a_->is_livelock_accepting_state(curr) << std::endl;
trace
<< "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(),
scc.top().condition) << std::endl;
<< "PASS 1: scc.top().condition : " << bdd_format_accset(
a_->get_dict(), scc.top().condition) << std::endl;
trace
<< "PASS 1: a_->all_acceptance_conditions() : " << (scc.top().condition == a_->all_acceptance_conditions()) << std::endl;
<< "PASS 1: a_->all_acceptance_conditions() : "
<< ( a_->all_acceptance_conditions()) << std::endl;
trace
<< "PASS 1 CYCLE and (scc.top().condition == a_->all_acceptance_conditions()) : "
<< (scc.top().condition == a_->all_acceptance_conditions()) << std::endl;
trace
<< "PASS 1: bddtrue : " << (a_->all_acceptance_conditions()==
bddtrue) << std::endl;
<< "PASS 1: bddtrue : " << (a_->all_acceptance_conditions()
== bddtrue) << std::endl;
trace
<< "PASS 1: bddfalse : " << (a_->all_acceptance_conditions()==
bddfalse) << std::endl;
<< "PASS 1: bddfalse : " << (a_->all_acceptance_conditions()
== bddfalse) << std::endl;
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
return true;
}
//ADDLINKS
if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr)
if (activate_heuristic && a_->is_livelock_accepting_state(curr)
&& is_stuttering_transition)
{
trace
@ -348,7 +352,7 @@ namespace spot
if (heuristic_livelock_detection(dest, h, h_livelock_root,
liveset_curr))
{
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
return true;
}
@ -359,7 +363,7 @@ namespace spot
if (heuristic_livelock_detection(succ, h, h_livelock_root,
liveset_curr))
{
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
return true;
}
@ -370,7 +374,7 @@ namespace spot
}
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
if (disable_second_pass || livelock_acceptance_states_not_found)
return false;
@ -431,23 +435,23 @@ namespace spot
std::stack<pair_state_iter> todo;
// * init: the set of the depth-first search initial states
std::stack<spot::state*> init_set;
std::queue<spot::state*> ta_init_it_;
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);
ta_init_it_.push(init_state);
}
while (!init_set.empty())
while (!ta_init_it_.empty())
{
// Setup depth-first search from initial states.
{
state* init = init_set.top();
init_set.pop();
state* init = ta_init_it_.front();
ta_init_it_.pop();
numbered_state_heap::state_index_p h_init = h->find(init);
if (h_init.first)
@ -540,7 +544,7 @@ namespace spot
if (!is_stuttering_transition)
{
init_set.push(dest);
ta_init_it_.push(dest);
continue;
}
@ -568,7 +572,7 @@ namespace spot
if (t->is_livelock_accepting_state(self_loop_state))
{
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
trace
<< "PASS 2: SUCCESS" << std::endl;
return true;
@ -612,7 +616,7 @@ namespace spot
sscc.rem().splice(sscc.rem().end(), rem);
if (sscc.top().is_accepting)
{
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
trace
<< "PASS 2: SUCCESS" << std::endl;
return true;
@ -620,20 +624,20 @@ namespace spot
}
}
clear(h, todo, init_set);
clear(h, todo, ta_init_it_);
return false;
}
void
ta_check::clear(numbered_state_heap* h, std::stack<pair_state_iter> todo,
std::stack<spot::state*> init_states)
std::queue<spot::state*> init_states)
{
set_states(states() + h->size());
while (!init_states.empty())
{
a_->free_state(init_states.top());
a_->free_state(init_states.front());
init_states.pop();
}
@ -647,6 +651,27 @@ namespace spot
delete h;
}
void
ta_check::clear(numbered_state_heap* h, std::stack<pair_state_iter> todo,
spot::ta_succ_iterator* init_states_it)
{
set_states(states() + h->size());
delete init_states_it;
// Release all iterators in TODO.
while (!todo.empty())
{
delete todo.top().second;
todo.pop();
dec_depth();
}
delete h;
}
std::ostream&
ta_check::print_stats(std::ostream& os) const
{

8
src/taalgos/emptinessta.hh
View file

@ -29,6 +29,7 @@
#include "tgbaalgos/gtec/nsheap.hh"
#include "tgbaalgos/emptiness_stats.hh"
#include <stack>
#include <queue>
namespace spot
{
@ -69,8 +70,13 @@ namespace spot
protected:
void
clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, std::stack<
clear(numbered_state_heap* h, std::stack<pair_state_iter> todo, std::queue<
spot::state*> init_set);
void
clear(numbered_state_heap* h, std::stack<pair_state_iter> todo,
spot::ta_succ_iterator* init_states_it);
bool
heuristic_livelock_detection(const state * stuttering_succ,
numbered_state_heap* h, int h_livelock_root, std::set<const state*,

13
src/taalgos/sba2ta.cc
View file

@ -122,7 +122,7 @@ namespace spot
ta->create_transition(source, bdd_setxor(
source->get_tgba_condition(),
dest->get_tgba_condition()), dest);
dest->get_tgba_condition()), bddfalse, dest);
}
}
@ -154,12 +154,7 @@ namespace spot
state_ta_explicit* artificial_livelock_accepting_state)
{
state_ta_explicit* artificial_livelock_accepting_state_added =
testing_automata->add_state(artificial_livelock_accepting_state);
// unique artificial_livelock_accepting_state
assert(artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state);
testing_automata->add_state(artificial_livelock_accepting_state);
ta::states_set_t states_set = testing_automata->get_states_set();
ta::states_set_t::iterator it;
@ -182,7 +177,7 @@ namespace spot
{
state_ta_explicit* dest = (*it_trans)->dest;
if (dest->is_livelock_accepting_state() && !dest->is_accepting_state())
if (dest->is_livelock_accepting_state())
{
conditions_to_livelock_accepting_states->insert(
(*it_trans)->condition);
@ -214,7 +209,7 @@ namespace spot
!= conditions_to_livelock_accepting_states->end(); it_conditions++)
{
testing_automata->create_transition(source, (*it_conditions),
testing_automata->create_transition(source, (*it_conditions),bddfalse,
artificial_livelock_accepting_state);
}

168
src/taalgos/tgba2ta.cc
View file

@ -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
@ -27,8 +27,6 @@
#define trace while (0) std::clog
#endif
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh"
@ -41,36 +39,25 @@
#include <stack>
#include "tgba2ta.hh"
#include "taalgos/statessetbuilder.hh"
#include "ta/tgbtaexplicit.hh"
using namespace std;
namespace spot
{
ta*
tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_,
ta_explicit*
build_ta(ta_explicit* ta, bdd atomic_propositions_set_,
bool artificial_initial_state_mode,
bool artificial_livelock_accepting_state_mode, bool degeneralized)
{
ta_explicit* ta;
std::stack<state_ta_explicit*> todo;
const tgba* tgba_ = ta->get_tgba();
// build Initial states set:
state* tgba_init_state = tgba_->get_init_state();
if (artificial_initial_state_mode)
{
state_ta_explicit* ta_init_state = new state_ta_explicit(
tgba_init_state->clone(), bddtrue, true);
ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(),ta_init_state);
}
else
{
ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions());
}
bdd tgba_condition = tgba_->support_conditions(tgba_init_state);
bdd satone_tgba_condition;
@ -174,8 +161,8 @@ namespace spot
{
state_ta_explicit* artificial_livelock_accepting_state =
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse,
false, false, true, 0);
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue,
false, false, true, 0);
add_artificial_livelock_accepting_state(ta,
artificial_livelock_accepting_state);
@ -186,6 +173,34 @@ namespace spot
}
ta_explicit*
tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_,
bool artificial_initial_state_mode,
bool artificial_livelock_accepting_state_mode, bool degeneralized)
{
ta_explicit* ta;
state* tgba_init_state = tgba_->get_init_state();
if (artificial_initial_state_mode)
{
state_ta_explicit* ta_init_state = new state_ta_explicit(
tgba_init_state->clone(), bddfalse, true);
ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(),
ta_init_state);
}
else
{
ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions());
}
tgba_init_state->destroy();
// build ta automata:
build_ta(ta, atomic_propositions_set_, artificial_initial_state_mode,
artificial_livelock_accepting_state_mode, degeneralized);
return ta;
}
void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state)
@ -219,8 +234,13 @@ namespace spot
{
state_ta_explicit* dest = (*it_trans)->dest;
state_ta_explicit::transitions* dest_trans =
(dest)->get_transitions();
bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();
//TODO TA++
if (dest->is_livelock_accepting_state()
&& !dest->is_accepting_state())
&& (!dest->is_accepting_state() || dest_trans_empty))
{
conditions_to_livelock_accepting_states->insert(
(*it_trans)->condition);
@ -228,9 +248,7 @@ namespace spot
}
//remove hole successors states
state_ta_explicit::transitions* dest_trans =
(dest)->get_transitions();
bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();
if (dest_trans_empty)
{
source->get_transitions((*it_trans)->condition)->remove(
@ -253,7 +271,7 @@ namespace spot
{
testing_automata->create_transition(source, (*it_conditions),
artificial_livelock_accepting_state);
bddfalse, artificial_livelock_accepting_state);
}
}
@ -276,7 +294,7 @@ namespace spot
scc_stack_ta sscc;
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
std::stack<bdd> arc;
// * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
@ -313,7 +331,7 @@ namespace spot
state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top());
init_set.pop();
state_ta_explicit* init_clone = init->clone();
state_ta_explicit* init_clone = init;
numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first)
@ -335,7 +353,7 @@ namespace spot
state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr->clone());
numbered_state_heap::state_index_p spi = h->find(curr);
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
{
@ -356,7 +374,7 @@ namespace spot
// fill rem with any component removed,
numbered_state_heap::state_index_p spi =
h->index(curr->clone());
h->index(curr);
assert(spi.first);
sscc.rem().push_front(curr);
@ -369,14 +387,14 @@ namespace spot
{
// removing states
std::list<state*>::iterator i;
bool is_livelock_accepting_sscc = (sscc.top().is_accepting
&& (sscc.rem().size() > 1)) || (sscc.top().condition
== testing_automata->all_acceptance_conditions());
bool is_livelock_accepting_sscc = (sscc.rem().size() > 1)
&& ((sscc.top().is_accepting) || (sscc.top().condition
== testing_automata->all_acceptance_conditions()));
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{
numbered_state_heap::state_index_p spi = h->index(
(*i)->clone());
(*i));
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
@ -421,7 +439,7 @@ namespace spot
bool is_stuttering_transition =
testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest);
state* dest_clone = dest->clone();
state* dest_clone = dest;
spi = h->find(dest_clone);
// Is this a new state?
@ -452,8 +470,8 @@ namespace spot
if (*spi.second == -1)
continue;
trace
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
trace << "***compute_livelock_acceptance_states: CYCLE***"
<< std::endl;
if (!curr->compare(dest))
{
@ -461,10 +479,13 @@ namespace spot
down_cast<state_ta_explicit*> (curr);
assert(self_loop_state);
if (testing_automata->is_accepting_state(self_loop_state))
if (testing_automata->is_accepting_state(self_loop_state)
|| (acc_cond
== testing_automata->all_acceptance_conditions()))
self_loop_state->set_livelock_accepting_state(true);
trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << std::endl;
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
<< std::endl;
}
@ -483,7 +504,6 @@ namespace spot
std::list<state*> rem;
bool acc = false;
while (threshold < sscc.top().index)
{
assert(!sscc.empty());
@ -496,7 +516,6 @@ namespace spot
arc.pop();
}
// Note that we do not always have
// threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have
@ -514,4 +533,73 @@ namespace spot
delete h;
}
tgbta_explicit*
tgba_to_tgbta(const tgba* tgba_, bdd atomic_propositions_set_)
{
state* tgba_init_state = tgba_->get_init_state();
state_ta_explicit* ta_init_state = new state_ta_explicit(
tgba_init_state->clone(), bddfalse, true);
tgba_init_state->destroy();
tgbta_explicit* tgbta = new spot::tgbta_explicit(tgba_,
tgba_->all_acceptance_conditions(), ta_init_state);
// build ta automata:
build_ta(tgbta, atomic_propositions_set_, true, true, false);
trace << "***tgba_to_tgbta: POST build_ta***" << std::endl;
// adapt a ta automata to build tgbta automata :
ta::states_set_t states_set = tgbta->get_states_set();
ta::states_set_t::iterator it;
tgba_succ_iterator* initial_states_iter = tgbta->succ_iter(
tgbta->get_artificial_initial_state());
initial_states_iter->first();
if (initial_states_iter->done())
return tgbta;
bdd first_state_condition = (initial_states_iter)->current_condition();
delete initial_states_iter;
bdd bdd_stutering_transition = bdd_setxor(first_state_condition,
first_state_condition);
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
state_ta_explicit::transitions* trans = state->get_transitions();
if (state->is_livelock_accepting_state())
{
bool trans_empty = (trans == 0 || trans->empty());
if (trans_empty)
{
trace
<< "***tgba_to_tgbta: PRE if (state->is_livelock_accepting_state()) ... create_transition ***"
<< std::endl;
tgbta->create_transition(state, bdd_stutering_transition,
tgbta->all_acceptance_conditions(), state);
trace
<< "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***"
<< std::endl;
}
//state->set_livelock_accepting_state(false);
}
if (state->compare(tgbta->get_artificial_initial_state()))
tgbta->create_transition(state, bdd_stutering_transition, bddfalse,
state);
trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl;
}
return tgbta;
}
}

6
src/taalgos/tgba2ta.hh
View file

@ -30,10 +30,11 @@
#include <cassert>
#include "misc/bddlt.hh"
#include "ta/taexplicit.hh"
#include "ta/tgbtaexplicit.hh"
namespace spot
{
ta*
ta_explicit*
tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set,
bool artificial_initial_state_mode = true,
bool artificial_livelock_accepting_state_mode = false,
@ -46,6 +47,9 @@ namespace spot
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state);
tgbta_explicit*
tgba_to_tgbta(const tgba* tgba_to_convert, bdd atomic_propositions_set);
}
#endif // SPOT_TGBAALGOS_SBA2TA_HH