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

Stable version of TGTA approach implementation (automaton + product)

Browse source 
* src/ta/tgta.hh, src/ta/tgta.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/ta/tgtaproduct.cc,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/emptinessta.hh, src/taalgos/emptinessta.hh,
src/taalgos/emptinessta.cc, src/taalgos/tgba2ta.hh,
src/taalgos/tgba2ta.cc: rename tgbta to tgta
in this source files.
* src/ta/tgbtaexplicit.hh, src/ta/tgbtaproduct.hh,  src/ta/tgbta.cc,
src/ta/tgbtaproduct.cc, src/ta/tgbta.hh, src/ta/tgbtaexplicit.cc:
Rename as...
* src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
src/ta/taproduct.hh, src/ta/tgtaexplicit.cc: ... these.
* src/taalgos/sba2ta.hh, src/taalgos/sba2ta.cc: deleted because
the implementation of all the transformations beteween TGBA and
the different forms of TA are new implemented in src/taalgos/tgba2ta.hh
 and src/taalgos/tgba2ta.cc.
* src/tgbatest/ltl2tgba.cc: rename the options of commands that build
the different forms of TA.
* src/ta/ta.hh: BUG Fix
* src/ta/Makefile.am, src/tgbatest/ltl2ta.test: impacts of this renaming
This commit is contained in:
Ala-Eddine Ben-Salem 2012-04-10 23:30:03 +02:00 • committed by Alexandre Duret-Lutz
parent c76e651bad
commit 5a706300b0
24 changed files with 1308 additions and 1580 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/taalgos/emptinessta.cc
View file

@ -47,7 +47,7 @@ namespace spot
bool
ta_check::check(bool disable_second_pass,
disable_heuristic_for_livelock_detection)
bool disable_heuristic_for_livelock_detection)
{
// We use five main data in this algorithm:

31
src/taalgos/emptinessta.hh
View file

@ -39,14 +39,15 @@ namespace spot
typedef std::pair<spot::state*, ta_succ_iterator_product*> pair_state_iter;
}
/// \addtogroup emptiness_check Emptiness-checks
/// \addtogroup ta_emptiness_check Emptiness-checks
/// \ingroup ta_algorithms
///
/// \brief Check whether the language of a product between a Kripke structure
/// and a TA is empty. It works for both standard and generalized form of TA.
/// \brief Check whether the language of a product (spot::ta_product) between
/// a Kripke structure and a TA is empty. It works also for the product
/// using Generalized TA (GTA and SGTA).
///
/// you should call \c check to check the product automaton.
/// If \c check() returns false, then the product automaton
/// you should call spot::ta_check::check() to check the product automaton.
/// If spot::ta_check::check() returns false, then the product automaton
/// was found empty. Otherwise the automaton accepts some run.
///
/// This is based on the following paper.
@ -64,21 +65,22 @@ namespace spot
/// }
/// \endverbatim
///
/// the implementation of \c check is inspired from the two-pass algorithm
/// of the paper above:
/// the implementation of spot::ta_check::check() is inspired from the
/// two-pass algorithm of the paper above:
/// - the fist-pass detect all Buchi-accepting cycles and includes
// the heuristic proposed in the paper to detect some
/// the heuristic proposed in the paper to detect some
/// livelock-accepting cycles.
/// - the second-pass detect all livelock-accepting cycles.
/// In addition, we add some optimizations to the fist pass:
/// 1- Detection of all (livelock-accepting) cycles containing a least
/// one state that is both livelock and accepting states
/// 1- Detection of all cycles containing a least
/// one state that is both livelock and Buchi accepting states
/// 2- Detection of all livelock-accepting cycles containing a least
/// one state (k,t) such as its "TA component" t is a livelock-accepting
/// state that has no successors in the TA automaton.
///
/// The implementation of each pass is a SCC-based algorithm inspired
/// from spot::gtec.hh.
/// The implementation of the algorithm of each pass is a SCC-based algorithm
/// inspired from spot::gtec.hh.
/// @{
/// \brief An implementation of the emptiness-check algorithm for a product
/// between a TA and a Kripke structure
@ -153,7 +155,10 @@ namespace spot
};
/// @}
/// @}
/// \addtogroup ta_emptiness_check_algorithms Emptiness-check algorithms
/// \ingroup ta_emptiness_check
}
#endif // SPOT_TAALGOS_EMPTINESS_HH

573
src/taalgos/minimize.cc
View file

@ -34,7 +34,7 @@
#include "ltlast/allnodes.hh"
#include "misc/hash.hh"
#include "misc/bddlt.hh"
#include "ta/tgbtaexplicit.hh"
#include "ta/tgtaexplicit.hh"
#include "taalgos/statessetbuilder.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/bddprint.hh"
@ -73,7 +73,8 @@ namespace spot
// From the base automaton and the list of sets, build the minimal automaton
void
build_result(const ta* a, std::list<hash_set*>& sets, tgba_explicit_number* result_tgba, ta_explicit* result)
build_result(const ta* a, std::list<hash_set*>& sets,
tgba_explicit_number* result_tgba, ta_explicit* result)
{
// For each set, create a state in the tgbaulting automaton.
@ -168,314 +169,331 @@ namespace spot
else if (is_initial_state)
result->add_to_initial_states_set(new_dst);
result->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst);
result->create_transition(ta_src, succit->current_condition(),
succit->current_acceptance_conditions(), ta_dst);
}
delete succit;
}
}
partition_t build_partition(const ta* ta_){
partition_t
build_partition(const ta* ta_)
{
partition_t cur_run;
partition_t next_run;
partition_t next_run;
// The list of equivalent states.
partition_t done;
// The list of equivalent states.
partition_t done;
std::set<const state*> states_set = get_states_set(ta_);
std::set<const state*> states_set = get_states_set(ta_);
hash_set* I = new hash_set;
hash_set* I = new hash_set;
// livelock acceptance states
hash_set* G = new hash_set;
// livelock acceptance states
hash_set* G = new hash_set;
// Buchi acceptance states
hash_set* F = new hash_set;
// Buchi acceptance states
hash_set* F = new hash_set;
// Buchi and livelock acceptance states
hash_set* G_F = new hash_set;
// Buchi and livelock acceptance states
hash_set* G_F = new hash_set;
// the other states (non initial and not in G, F and G_F)
hash_set* S = new hash_set;
// the other states (non initial and not in G, F and G_F)
hash_set* S = new hash_set;
std::set<const state*>::iterator it;
std::set<const state*>::iterator it;
spot::state* artificial_initial_state = ta_->get_artificial_initial_state();
spot::state* artificial_initial_state = ta_->get_artificial_initial_state();
for (it = states_set.begin(); it != states_set.end(); it++)
for (it = states_set.begin(); it != states_set.end(); it++)
{
const state* s = (*it);
if (s == artificial_initial_state)
{
const state* s = (*it);
if (s == artificial_initial_state)
{
I->insert(s);
}
else if (artificial_initial_state == 0 && ta_->is_initial_state(s))
{
I->insert(s);
}
else if (ta_->is_livelock_accepting_state(s)
&& ta_->is_accepting_state(s))
{
G_F->insert(s);
}
else if (ta_->is_accepting_state(s))
{
F->insert(s);
}
else if (ta_->is_livelock_accepting_state(s))
{
G->insert(s);
}
else
{
S->insert(s);
}
I->insert(s);
}
else if (artificial_initial_state == 0 && ta_->is_initial_state(s))
{
I->insert(s);
}
else if (ta_->is_livelock_accepting_state(s)
&& ta_->is_accepting_state(s))
{
G_F->insert(s);
}
else if (ta_->is_accepting_state(s))
{
F->insert(s);
}
hash_map state_set_map;
// Size of ta_
unsigned size = states_set.size() + 6;
// Use bdd variables to number sets. set_num is the first variable
// available.
unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_);
std::set<int> free_var;
for (unsigned i = set_num; i < set_num + size; ++i)
free_var.insert(i);
std::map<int, int> used_var;
else if (ta_->is_livelock_accepting_state(s))
{
for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i)
{
hash_set* cI = new hash_set;
cI->insert(*i);
done.push_back(cI);
used_var[set_num] = 1;
free_var.erase(set_num);
state_set_map[*i] = set_num;
set_num++;
}
}
delete I;
if (!G->empty())
{
unsigned s = G->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(G);
else
done.push_back(G);
for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i)
state_set_map[*i] = num;
G->insert(s);
}
else
delete G;
if (!F->empty())
{
unsigned s = F->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(F);
else
done.push_back(F);
for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i)
state_set_map[*i] = num;
S->insert(s);
}
else
delete F;
if (!G_F->empty())
}
hash_map state_set_map;
// Size of ta_
unsigned size = states_set.size() + 6;
// Use bdd variables to number sets. set_num is the first variable
// available.
unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_);
std::set<int> free_var;
for (unsigned i = set_num; i < set_num + size; ++i)
free_var.insert(i);
std::map<int, int> used_var;
{
for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i)
{
unsigned s = G_F->size();
unsigned num = set_num;
hash_set* cI = new hash_set;
cI->insert(*i);
done.push_back(cI);
used_var[set_num] = 1;
free_var.erase(set_num);
state_set_map[*i] = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(G_F);
else
done.push_back(G_F);
for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i)
state_set_map[*i] = num;
}
else
delete G_F;
if (!S->empty())
{
unsigned s = S->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(S);
else
done.push_back(S);
for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i)
state_set_map[*i] = num;
}
else
delete S;
}
delete I;
// A bdd_states_map is a list of formulae (in a BDD form) associated with a
// destination set of states.
typedef std::map<bdd, hash_set*, bdd_less_than> bdd_states_map;
bool did_split = true;
if (!G->empty())
{
unsigned s = G->size();
unsigned num = set_num;
set_num++;
used_var[num] = 1;
used_var[num] = s;
free_var.erase(num);
bdd bdd_false_acceptance_condition = bdd_ithvar(num);
if (s > 1)
cur_run.push_back(G);
else
done.push_back(G);
for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i)
state_set_map[*i] = num;
while (did_split)
}
else
delete G;
if (!F->empty())
{
unsigned s = F->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(F);
else
done.push_back(F);
for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i)
state_set_map[*i] = num;
}
else
delete F;
if (!G_F->empty())
{
unsigned s = G_F->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(G_F);
else
done.push_back(G_F);
for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i)
state_set_map[*i] = num;
}
else
delete G_F;
if (!S->empty())
{
unsigned s = S->size();
unsigned num = set_num;
set_num++;
used_var[num] = s;
free_var.erase(num);
if (s > 1)
cur_run.push_back(S);
else
done.push_back(S);
for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i)
state_set_map[*i] = num;
}
else
delete S;
// A bdd_states_map is a list of formulae (in a BDD form) associated with a
// destination set of states.
typedef std::map<bdd, hash_set*, bdd_less_than> bdd_states_map;
bool did_split = true;
unsigned num = set_num;
set_num++;
used_var[num] = 1;
free_var.erase(num);
bdd bdd_false_acceptance_condition = bdd_ithvar(num);
while (did_split)
{
did_split = false;
while (!cur_run.empty())
{
did_split = false;
while (!cur_run.empty())
// Get a set to process.
hash_set* cur = cur_run.front();
cur_run.pop_front();
trace
<< "processing " << format_hash_set(cur, ta_) << std::endl;
hash_set::iterator hi;
bdd_states_map bdd_map;
for (hi = cur->begin(); hi != cur->end(); ++hi)
{
// Get a set to process.
hash_set* cur = cur_run.front();
cur_run.pop_front();
const state* src = *hi;
bdd f = bddfalse;
ta_succ_iterator* si = ta_->succ_iter(src);
trace
<< "processing " << format_hash_set(cur, ta_) << std::endl;
hash_set::iterator hi;
bdd_states_map bdd_map;
for (hi = cur->begin(); hi != cur->end(); ++hi)
<< "+src: " << src << std::endl;
for (si->first(); !si->done(); si->next())
{
const state* src = *hi;
bdd f = bddfalse;
ta_succ_iterator* si = ta_->succ_iter(src);
trace << "+src: " << src << std::endl;
for (si->first(); !si->done(); si->next())
{
const state* dst = si->current_state();
hash_map::const_iterator i = state_set_map.find(dst);
const state* dst = si->current_state();
hash_map::const_iterator i = state_set_map.find(dst);
assert(i != state_set_map.end());
bdd current_acceptance_conditions =
si->current_acceptance_conditions();
if (current_acceptance_conditions == bddfalse)
current_acceptance_conditions
= bdd_false_acceptance_condition;
f |= (bdd_ithvar(i->second) & si->current_condition()
& current_acceptance_conditions);
trace << "+f: " << bdd_format_accset(ta_->get_dict(),f) << std::endl;;
trace << " -bdd_ithvar(i->second): " << bdd_format_accset(ta_->get_dict(),bdd_ithvar(i->second)) << std::endl;;
trace << " -si->current_condition(): " << bdd_format_accset(ta_->get_dict(),si->current_condition()) << std::endl;;
trace << " -current_acceptance_conditions: " << bdd_format_accset(ta_->get_dict(),current_acceptance_conditions) << std::endl;;
}
delete si;
// Have we already seen this formula ?
bdd_states_map::iterator bsi = bdd_map.find(f);
if (bsi == bdd_map.end())
{
// No, create a new set.
hash_set* new_set = new hash_set;
new_set->insert(src);
bdd_map[f] = new_set;
}
else
{
// Yes, add the current state to the set.
bsi->second->insert(src);
}
}
bdd_states_map::iterator bsi = bdd_map.begin();
if (bdd_map.size() == 1)
{
// The set was not split.
assert(i != state_set_map.end());
bdd current_acceptance_conditions =
si->current_acceptance_conditions();
if (current_acceptance_conditions == bddfalse)
current_acceptance_conditions
= bdd_false_acceptance_condition;
f |= (bdd_ithvar(i->second) & si->current_condition()
& current_acceptance_conditions);
trace
<< "set " << format_hash_set(bsi->second, ta_)
<< " was not split" << std::endl;
next_run.push_back(bsi->second);
<< "+f: " << bdd_format_accset(ta_->get_dict(), f)
<< std::endl;
;
trace
<< " -bdd_ithvar(i->second): " << bdd_format_accset(
ta_->get_dict(), bdd_ithvar(i->second)) << std::endl;
;
trace
<< " -si->current_condition(): "
<< bdd_format_accset(ta_->get_dict(),
si->current_condition()) << std::endl;
;
trace
<< " -current_acceptance_conditions: "
<< bdd_format_accset(ta_->get_dict(),
current_acceptance_conditions) << std::endl;
;
}
delete si;
// Have we already seen this formula ?
bdd_states_map::iterator bsi = bdd_map.find(f);
if (bsi == bdd_map.end())
{
// No, create a new set.
hash_set* new_set = new hash_set;
new_set->insert(src);
bdd_map[f] = new_set;
}
else
{
did_split = true;
for (; bsi != bdd_map.end(); ++bsi)
// Yes, add the current state to the set.
bsi->second->insert(src);
}
}
bdd_states_map::iterator bsi = bdd_map.begin();
if (bdd_map.size() == 1)
{
// The set was not split.
trace
<< "set " << format_hash_set(bsi->second, ta_)
<< " was not split" << std::endl;
next_run.push_back(bsi->second);
}
else
{
did_split = true;
for (; bsi != bdd_map.end(); ++bsi)
{
hash_set* set = bsi->second;
// Free the number associated to these states.
unsigned num = state_set_map[*set->begin()];
assert(used_var.find(num) != used_var.end());
unsigned left = (used_var[num] -= set->size());
// Make sure LEFT does not become negative (hence bigger
// than SIZE when read as unsigned)
assert(left < size);
if (left == 0)
{
hash_set* set = bsi->second;
// Free the number associated to these states.
unsigned num = state_set_map[*set->begin()];
assert(used_var.find(num) != used_var.end());
unsigned left = (used_var[num] -= set->size());
// Make sure LEFT does not become negative (hence bigger
// than SIZE when read as unsigned)
assert(left < size);
if (left == 0)
{
used_var.erase(num);
free_var.insert(num);
}
// Pick a free number
assert(!free_var.empty());
num = *free_var.begin();
free_var.erase(free_var.begin());
used_var[num] = set->size();
for (hash_set::iterator hit = set->begin(); hit
!= set->end(); ++hit)
state_set_map[*hit] = num;
// Trivial sets can't be splitted any further.
if (set->size() == 1)
{
trace
<< "set " << format_hash_set(set, ta_)
<< " is minimal" << std::endl;
done.push_back(set);
}
else
{
trace
<< "set " << format_hash_set(set, ta_)
<< " should be processed further" << std::endl;
next_run.push_back(set);
}
used_var.erase(num);
free_var.insert(num);
}
// Pick a free number
assert(!free_var.empty());
num = *free_var.begin();
free_var.erase(free_var.begin());
used_var[num] = set->size();
for (hash_set::iterator hit = set->begin(); hit
!= set->end(); ++hit)
state_set_map[*hit] = num;
// Trivial sets can't be splitted any further.
if (set->size() == 1)
{
trace
<< "set " << format_hash_set(set, ta_)
<< " is minimal" << std::endl;
done.push_back(set);
}
else
{
trace
<< "set " << format_hash_set(set, ta_)
<< " should be processed further" << std::endl;
next_run.push_back(set);
}
}
delete cur;
}
if (did_split)
trace
<< "splitting did occur during this pass." << std::endl;
//elsetrace << "splitting did not occur during this pass." << std::endl;
std::swap(cur_run, next_run);
delete cur;
}
if (did_split)
trace
<< "splitting did occur during this pass." << std::endl;
//elsetrace << "splitting did not occur during this pass." << std::endl;
std::swap(cur_run, next_run);
}
done.splice(done.end(), cur_run);
done.splice(done.end(), cur_run);
#ifdef TRACE
trace << "Final partition: ";
for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
trace << format_hash_set(*i, ta_) << " ";
trace << std::endl;
#endif
#ifdef TRACE
trace << "Final partition: ";
for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
trace << format_hash_set(*i, ta_) << " ";
trace << std::endl;
#endif
return done;
return done;
}
ta*
@ -486,11 +504,8 @@ namespace spot
ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions());
partition_t partition = build_partition(ta_);
// Build the ta automata result.
build_result(ta_, partition, tgba, res);
@ -503,32 +518,30 @@ namespace spot
return res;
}
tgbta*
minimize_tgbta(const tgbta* tgbta_)
{
tgta*
minimize_tgta(const tgta* tgta_)
{
tgba_explicit_number* tgba = new tgba_explicit_number(tgbta_->get_dict());
tgba_explicit_number* tgba = new tgba_explicit_number(tgta_->get_dict());
tgbta_explicit* res = new tgbta_explicit(tgba, tgbta_->all_acceptance_conditions(),0);
tgta_explicit* res = new tgta_explicit(tgba,
tgta_->all_acceptance_conditions(), 0);
const ta_explicit* tgbta = dynamic_cast <const tgbta_explicit*> (tgbta_);
//TODO copier le tgta_ dans un tgta_explicit au lieu de faire un cast...
const ta_explicit* tgta = dynamic_cast<const tgta_explicit*> (tgta_);
partition_t partition = build_partition(tgbta);
partition_t partition = build_partition(tgta);
// Build the minimal tgta automaton.
build_result(tgta, partition, tgba, res);
// Free all the allocated memory.
std::list<hash_set*>::iterator itdone;
for (itdone = partition.begin(); itdone != partition.end(); ++itdone)
delete *itdone;
//delete ta_;
// Build the tgbault.
build_result(tgbta, partition,tgba, res);
// Free all the allocated memory.
std::list<hash_set*>::iterator itdone;
for (itdone = partition.begin(); itdone != partition.end(); ++itdone)
delete *itdone;
//delete ta_;
return res;
}
return res;
}
}

45
src/taalgos/minimize.hh
View file

@ -22,19 +22,58 @@
# define SPOT_TAALGOS_MINIMIZE_HH
# include "ta/ta.hh"
# include "ta/tgbta.hh"
# include "ta/tgta.hh"
# include "ta/taexplicit.hh"
namespace spot
{
/// \addtogroup ta_reduction
/// @{
/// \brief Construct a simplified TA by merging bisimilar states.
///
/// A TA automaton can be simplified by merging bisimilar states:
/// Two states are bisimilar if the automaton can accept the
/// same executions starting for either of these states. This can be
/// achieved using any algorithm based on partition refinement
///
/// For more detail about this type of algorithm, see the following paper:
/// \verbatim
/// @InProceedings{valmari.09.icatpn,
/// author = {Antti Valmari},
/// title = {Bisimilarity Minimization in in O(m logn) Time},
/// booktitle = {Proceedings of the 30th International Conference on
/// the Applications and Theory of Petri Nets
/// (ICATPN'09)},
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer},
/// isbn = {978-3-642-02423-8},
/// pages = {123--142},
/// volume = 5606,
/// url = {http://dx.doi.org/10.1007/978-3-642-02424-5_9},
/// year = {2009}
/// }
/// \endverbatim
///
/// \param ta_ the TA automaton to convert into a simplified TA
ta*
minimize_ta(const ta* ta_);
tgbta*
minimize_tgbta(const tgbta* tgbta_);
/// \brief Construct a simplified TGTA by merging bisimilar states.
///
/// A TGTA automaton can be simplified by merging bisimilar states:
/// Two states are bisimilar if the automaton can accept the
/// same executions starting for either of these states. This can be
/// achieved using same algorithm used to simplify a TA taking into account
/// the acceptance conditions of the outgoing transitions.
///
/// \param tgta_ the TGTA automaton to convert into a simplified TGTA
tgta*
minimize_tgta(const tgta* tgta_);
/// @}
}

454
src/taalgos/sba2ta.cc
View file

@ -1,454 +0,0 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement
// de l Epita (LRDE).
//
// 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 "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include <cassert>
#include "ltlvisit/tostring.hh"
#include <iostream>
#include "tgba/bddprint.hh"
#include "tgbaalgos/gtec/nsheap.hh"
#include <stack>
#include "sba2ta.hh"
#include "taalgos/statessetbuilder.hh"
using namespace std;
namespace spot
{
ta*
sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_,
bool artificial_initial_state_mode,
bool artificial_livelock_accepting_state_mode)
{
ta_explicit* ta;
std::stack<state_ta_explicit*> todo;
// 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_, ta_init_state);
}
else
{
ta = new spot::ta_explicit(tgba_);
}
bdd tgba_condition = tgba_->support_conditions(tgba_init_state);
bdd satone_tgba_condition;
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
atomic_propositions_set_, bddtrue)) != bddfalse)
{
tgba_condition -= satone_tgba_condition;
state_ta_explicit* init_state = new state_ta_explicit(
tgba_init_state->clone(), satone_tgba_condition, true,
tgba_->state_is_accepting(tgba_init_state));
state_ta_explicit* s = ta->add_state(init_state);
assert(s == init_state);
ta->add_to_initial_states_set(s);
todo.push(init_state);
}
tgba_init_state->destroy();
while (!todo.empty())
{
state_ta_explicit* source = todo.top();
todo.pop();
tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter(
source->get_tgba_state());
for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next())
{
const state* tgba_state = tgba_succ_it->current_state();
bdd tgba_condition = tgba_succ_it->current_condition();
bdd satone_tgba_condition;
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
atomic_propositions_set_, bddtrue)) != bddfalse)
{
tgba_condition -= satone_tgba_condition;
bdd all_props = bddtrue;
bdd dest_condition;
if (satone_tgba_condition == source->get_tgba_condition())
while ((dest_condition = bdd_satoneset(all_props,
atomic_propositions_set_, bddtrue)) != bddfalse)
{
all_props -= dest_condition;
state_ta_explicit* new_dest = new state_ta_explicit(
tgba_state->clone(), dest_condition, false,
tgba_->state_is_accepting(tgba_state));
state_ta_explicit* dest = ta->add_state(new_dest);
if (dest != new_dest)
{
// the state dest already exists in the testing automata
new_dest->get_tgba_state()->destroy();
delete new_dest;
}
else
{
todo.push(dest);
}
ta->create_transition(source, bdd_setxor(
source->get_tgba_condition(),
dest->get_tgba_condition()), bddfalse, dest);
}
}
tgba_state->destroy();
}
delete tgba_succ_it;
}
compute_livelock_acceptance_states(ta);
if (artificial_livelock_accepting_state_mode)
{
state_ta_explicit* artificial_livelock_accepting_state =
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse,
false, false, true, 0, true);
add_artificial_livelock_accepting_state(ta,
artificial_livelock_accepting_state);
}
return ta;
}
void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
state_ta_explicit* 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;
std::set<bdd, bdd_less_than>* conditions_to_livelock_accepting_states =
new std::set<bdd, bdd_less_than>;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* source = static_cast<state_ta_explicit*> (*it);
conditions_to_livelock_accepting_states->clear();
state_ta_explicit::transitions* trans = source->get_transitions();
state_ta_explicit::transitions::iterator it_trans;
if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end();)
{
state_ta_explicit* dest = (*it_trans)->dest;
if (dest->is_livelock_accepting_state())
{
conditions_to_livelock_accepting_states->insert(
(*it_trans)->condition);
}
//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(
*it_trans);
delete (*it_trans);
it_trans = trans->erase(it_trans);
}
else
{
it_trans++;
}
}
if (conditions_to_livelock_accepting_states != 0)
{
std::set<bdd, bdd_less_than>::iterator it_conditions;
for (it_conditions
= conditions_to_livelock_accepting_states->begin(); it_conditions
!= conditions_to_livelock_accepting_states->end(); it_conditions++)
{
testing_automata->create_transition(source, (*it_conditions),bddfalse,
artificial_livelock_accepting_state);
}
}
}
delete conditions_to_livelock_accepting_states;
}
namespace
{
typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
}
void
compute_livelock_acceptance_states(ta_explicit* testing_automata)
{
// We use five main data in this algorithm:
// * sscc: a stack of strongly stuttering-connected components (SSCC)
scc_stack_ta sscc;
// * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states.
// * num: the number of visited nodes. Used to set the order of each
// visited node,
int num = 0;
// * todo: the depth-first search stack. This holds pairs of the
// form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
// over the successors of STATE. In our use, ITERATOR should
// always be freed when TODO is popped, but STATE should not because
// 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<state*> init_set;
ta::states_set_t::const_iterator it;
ta::states_set_t init_states = testing_automata->get_initial_states_set();
for (it = init_states.begin(); it != init_states.end(); it++)
{
state* init_state = (*it);
init_set.push(init_state);
}
while (!init_set.empty())
{
// Setup depth-first search from initial states.
{
state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top());
init_set.pop();
state_ta_explicit* init_clone = init->clone();
numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first)
continue;
h->insert(init_clone, ++num);
sscc.push(num);
sscc.top().is_accepting
= testing_automata->is_accepting_state(init);
tgba_succ_iterator* iter = testing_automata->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
}
while (!todo.empty())
{
state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr->clone());
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
{
todo.pop();
continue;
}
// We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack.
if (succ->done())
{
// We have explored all successors of state CURR.
// Backtrack TODO.
todo.pop();
// fill rem with any component removed,
numbered_state_heap::state_index_p spi =
h->index(curr->clone());
assert(spi.first);
sscc.rem().push_front(curr);
// When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC.
assert(!sscc.empty());
if (sscc.top().index == *spi.second)
{
// removing states
std::list<state*>::iterator i;
bool is_livelock_accepting_sscc = (sscc.top().is_accepting
&& (sscc.rem().size() > 1));
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{
numbered_state_heap::state_index_p spi = h->index(
(*i)->clone());
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
if (is_livelock_accepting_sscc)
{//if it is an accepting sscc
//add the state to G (=the livelock-accepting states set)
state_ta_explicit * livelock_accepting_state =
down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state(
true);
}
}
sscc.pop();
}
// automata reduction
testing_automata->delete_stuttering_and_hole_successors(curr);
delete succ;
// Do not delete CURR: it is a key in H.
continue;
}
// Fetch the values destination state we are interested in...
state* dest = succ->current_state();
// ... and point the iterator to the next successor, for
// the next iteration.
succ->next();
// We do not need SUCC from now on.
// Are we going to a new state through a stuttering transition?
bool is_stuttering_transition =
testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest);
state* dest_clone = dest->clone();
spi = h->find(dest_clone);
// Is this a new state?
if (!spi.first)
{
if (!is_stuttering_transition)
{
init_set.push(dest);
dest_clone->destroy();
continue;
}
// Number it, stack it, and register its successors
// for later processing.
h->insert(dest_clone, ++num);
sscc.push(num);
sscc.top().is_accepting = testing_automata->is_accepting_state(
dest);
tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
iter->first();
todo.push(pair_state_iter(dest, iter));
continue;
}
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
continue;
if (!curr->compare(dest))
{
state_ta_explicit * self_loop_state =
down_cast<state_ta_explicit*> (curr);
assert(self_loop_state);
if (testing_automata->is_accepting_state(self_loop_state))
self_loop_state->set_livelock_accepting_state(true);
}
// Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC.
//
// This merge is easy to do because the order of the SSCC in
// ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold").
int threshold = *spi.second;
std::list<state*> rem;
bool acc = false;
while (threshold < sscc.top().index)
{
assert(!sscc.empty());
acc |= sscc.top().is_accepting;
rem.splice(rem.end(), sscc.rem());
sscc.pop();
}
// Note that we do not always have
// threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC.
sscc.top().is_accepting |= acc;
sscc.rem().splice(sscc.rem().end(), rem);
}
}
delete h;
}
}

49
src/taalgos/sba2ta.hh
View file

@ -1,49 +0,0 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
// de l Epita (LRDE).
//
// 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_TGBAALGOS_SBA2TA_HH
# define SPOT_TGBAALGOS_SBA2TA_HH
#include "misc/hash.hh"
#include <list>
#include <map>
#include <set>
#include "tgba/tgbatba.hh"
#include "ltlast/formula.hh"
#include <cassert>
#include "misc/bddlt.hh"
#include "ta/taexplicit.hh"
namespace spot
{
ta*
sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set, bool artificial_initial_state_mode = true,
bool artificial_livelock_accepting_state_mode = false);
void
compute_livelock_acceptance_states(ta_explicit* testing_automata);
void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state);
}
#endif // SPOT_TGBAALGOS_SBA2TA_HH

859
src/taalgos/tgba2ta.cc
View file

@ -39,16 +39,412 @@
#include <stack>
#include "tgba2ta.hh"
#include "taalgos/statessetbuilder.hh"
#include "ta/tgbtaexplicit.hh"
#include "ta/tgtaexplicit.hh"
using namespace std;
namespace spot
{
namespace
{
typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
}
void
transform_to_single_pass_automaton(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state = 0)
{
if (artificial_livelock_accepting_state != 0)
{
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);
artificial_livelock_accepting_state->set_livelock_accepting_state(true);
artificial_livelock_accepting_state->free_transitions();
}
ta::states_set_t states_set = testing_automata->get_states_set();
ta::states_set_t::iterator it;
state_ta_explicit::transitions* transitions_to_livelock_states =
new state_ta_explicit::transitions;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* source = static_cast<state_ta_explicit*> (*it);
transitions_to_livelock_states->clear();
state_ta_explicit::transitions* trans = source->get_transitions();
state_ta_explicit::transitions::iterator it_trans;
if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end();)
{
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();
//select transitions where a destination is a livelock state
// which isn't a Buchi accepting state and has successors
if (dest->is_livelock_accepting_state()
&& (!dest->is_accepting_state()) && (!dest_trans_empty))
{
transitions_to_livelock_states->push_front(*it_trans);
}
//optimization to have, after
// minimization, an unique livelock state which has no successors
if (dest->is_livelock_accepting_state() && (dest_trans_empty))
{
dest->set_accepting_state(false);
}
it_trans++;
}
if (transitions_to_livelock_states != 0)
{
state_ta_explicit::transitions::iterator it_trans;
for (it_trans = transitions_to_livelock_states->begin(); it_trans
!= transitions_to_livelock_states->end(); it_trans++)
{
if (artificial_livelock_accepting_state != 0)
{
testing_automata->create_transition(source,
(*it_trans)->condition,
(*it_trans)->acceptance_conditions,
artificial_livelock_accepting_state, true);
}
else
{
testing_automata->create_transition(source,
(*it_trans)->condition,
(*it_trans)->acceptance_conditions,
((*it_trans)->dest)->stuttering_reachable_livelock,
true);
}
}
}
}
delete transitions_to_livelock_states;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
state_ta_explicit::transitions* state_trans =
(state)->get_transitions();
bool state_trans_empty = state_trans == 0 || state_trans->empty();
if (state->is_livelock_accepting_state()
&& (!state->is_accepting_state()) && (!state_trans_empty))
state->set_livelock_accepting_state(false);
}
}
void
compute_livelock_acceptance_states(ta_explicit* testing_automata,
bool single_pass_emptiness_check,
state_ta_explicit* artificial_livelock_accepting_state)
{
// We use five main data in this algorithm:
// * sscc: a stack of strongly stuttering-connected components (SSCC)
scc_stack_ta sscc;
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build();
///< Heap of visited states.
// * num: the number of visited nodes. Used to set the order of each
// visited node,
int num = 0;
// * todo: the depth-first search stack. This holds pairs of the
// form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
// over the successors of STATE. In our use, ITERATOR should
// always be freed when TODO is popped, but STATE should not because
// 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<state*> init_set;
ta::states_set_t::const_iterator it;
ta::states_set_t init_states = testing_automata->get_initial_states_set();
for (it = init_states.begin(); it != init_states.end(); it++)
{
state* init_state = (*it);
init_set.push(init_state);
}
while (!init_set.empty())
{
// Setup depth-first search from initial states.
{
state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top());
init_set.pop();
state_ta_explicit* init_clone = init;
numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first)
continue;
h->insert(init_clone, ++num);
sscc.push(num);
arc.push(bddfalse);
sscc.top().is_accepting
= testing_automata->is_accepting_state(init);
tgba_succ_iterator* iter = testing_automata->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
}
while (!todo.empty())
{
state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr);
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
{
todo.pop();
continue;
}
// We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack.
if (succ->done())
{
// We have explored all successors of state CURR.
// Backtrack TODO.
todo.pop();
// fill rem with any component removed,
numbered_state_heap::state_index_p spi = h->index(curr);
assert(spi.first);
sscc.rem().push_front(curr);
// When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC.
assert(!sscc.empty());
if (sscc.top().index == *spi.second)
{
// removing states
std::list<state*>::iterator i;
bool is_livelock_accepting_sscc = (sscc.rem().size() > 1)
&& ((sscc.top().is_accepting) || (sscc.top().condition
== testing_automata->all_acceptance_conditions()));
trace
<< "*** sscc.size() = ***"
<< sscc.size() << std::endl;
for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
{
numbered_state_heap::state_index_p spi = h->index((*i));
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
if (is_livelock_accepting_sscc)
{//if it is an accepting sscc add the state to
//G (=the livelock-accepting states set)
trace << "*** sscc.size() > 1: states: ***"
<< testing_automata->format_state(*i)
<< std::endl;
state_ta_explicit * livelock_accepting_state =
down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state(
true);
if (single_pass_emptiness_check)
{
livelock_accepting_state->set_accepting_state(
true);
livelock_accepting_state->stuttering_reachable_livelock
= livelock_accepting_state;
}
}
}
assert(!arc.empty());
sscc.pop();
arc.pop();
}
// automata reduction
testing_automata->delete_stuttering_and_hole_successors(curr);
delete succ;
// Do not delete CURR: it is a key in H.
continue;
}
// Fetch the values destination state we are interested in...
state* dest = succ->current_state();
bdd acc_cond = succ->current_acceptance_conditions();
// ... and point the iterator to the next successor, for
// the next iteration.
succ->next();
// We do not need SUCC from now on.
// Are we going to a new state through a stuttering transition?
bool is_stuttering_transition =
testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest);
state* dest_clone = dest;
spi = h->find(dest_clone);
// Is this a new state?
if (!spi.first)
{
if (!is_stuttering_transition)
{
init_set.push(dest);
dest_clone->destroy();
continue;
}
// Number it, stack it, and register its successors
// for later processing.
h->insert(dest_clone, ++num);
sscc.push(num);
arc.push(acc_cond);
sscc.top().is_accepting = testing_automata->is_accepting_state(
dest);
tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
iter->first();
todo.push(pair_state_iter(dest, iter));
continue;
}
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
continue;
trace
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
if (!curr->compare(dest))
{
state_ta_explicit * self_loop_state =
down_cast<state_ta_explicit*> (curr);
assert(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);
if (single_pass_emptiness_check)
{
self_loop_state->set_accepting_state(true);
self_loop_state->stuttering_reachable_livelock
= self_loop_state;
}
}
trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
<< std::endl;
}
// Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC.
//
// This merge is easy to do because the order of the SSCC in
// ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold").
int threshold = *spi.second;
std::list<state*> rem;
bool acc = false;
while (threshold < sscc.top().index)
{
assert(!sscc.empty());
assert(!arc.empty());
acc |= sscc.top().is_accepting;
acc_cond |= sscc.top().condition;
acc_cond |= arc.top();
rem.splice(rem.end(), sscc.rem());
sscc.pop();
arc.pop();
}
// Note that we do not always have
// threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC.
sscc.top().is_accepting |= acc;
sscc.top().condition |= acc_cond;
sscc.rem().splice(sscc.rem().end(), rem);
}
}
delete h;
if ((artificial_livelock_accepting_state != 0)
|| single_pass_emptiness_check)
transform_to_single_pass_automaton(testing_automata,
artificial_livelock_accepting_state);
}
ta_explicit*
build_ta(ta_explicit* ta, bdd atomic_propositions_set_,
bool artificial_livelock_accepting_state_mode, bool degeneralized)
build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool degeneralized,
bool single_pass_emptiness_check, bool artificial_livelock_state_mode)
{
std::stack<state_ta_explicit*> todo;
@ -115,17 +511,17 @@ namespace spot
all_props -= dest_condition;
state_ta_explicit* new_dest;
if (degeneralized)
{
{
new_dest
= new state_ta_explicit(
tgba_state->clone(),
dest_condition,
false,
new_dest
= new state_ta_explicit(
tgba_state->clone(),
dest_condition,
false,
((const tgba_sba_proxy*) tgba_)->state_is_accepting(
tgba_state));
tgba_state));
}
}
else
{
new_dest = new state_ta_explicit(tgba_state->clone(),
@ -136,7 +532,7 @@ namespace spot
if (dest != new_dest)
{
// the state dest already exists in the testing automata
// the state dest already exists in the automaton
new_dest->get_tgba_state()->destroy();
delete new_dest;
}
@ -163,11 +559,11 @@ namespace spot
trace
<< "*** build_ta: artificial_livelock_accepting_state_mode = ***"
<< artificial_livelock_accepting_state_mode << std::endl;
<< artificial_livelock_state_mode << std::endl;
if (artificial_livelock_accepting_state_mode)
if (artificial_livelock_state_mode)
{
single_pass_emptiness_check = true;
artificial_livelock_accepting_state = new state_ta_explicit(
ta->get_tgba()->get_init_state(), bddtrue, false, false, true, 0);
trace
@ -176,7 +572,8 @@ namespace spot
}
compute_livelock_acceptance_states(ta, artificial_livelock_accepting_state);
compute_livelock_acceptance_states(ta, single_pass_emptiness_check,
artificial_livelock_accepting_state);
return ta;
@ -184,19 +581,19 @@ 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)
bool degeneralized, bool artificial_initial_state_mode,
bool single_pass_emptiness_check, bool artificial_livelock_state_mode)
{
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(
state_ta_explicit* artificial_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);
artificial_init_state);
}
else
{
@ -205,413 +602,38 @@ namespace spot
tgba_init_state->destroy();
// build ta automata:
build_ta(ta, atomic_propositions_set_,
artificial_livelock_accepting_state_mode, degeneralized);
build_ta(ta, atomic_propositions_set_, degeneralized,
single_pass_emptiness_check, artificial_livelock_state_mode);
return ta;
}
void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
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);
trace
<< "*** add_artificial_livelock_accepting_state: "
<< "assert(artificial_livelock_accepting_state_added == "
<< "artificial_livelock_accepting_state) = ***"
<< (artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state) << std::endl;
ta::states_set_t states_set = testing_automata->get_states_set();
ta::states_set_t::iterator it;
std::set<bdd, bdd_less_than>* conditions_to_livelock_accepting_states =
new std::set<bdd, bdd_less_than>;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* source = static_cast<state_ta_explicit*> (*it);
conditions_to_livelock_accepting_states->clear();
state_ta_explicit::transitions* trans = source->get_transitions();
state_ta_explicit::transitions::iterator it_trans;
if (trans != 0)
for (it_trans = trans->begin(); it_trans != trans->end();)
{
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();
//TA++
if (dest->is_livelock_accepting_state()
&& (!dest->is_accepting_state() || dest_trans_empty))
{
conditions_to_livelock_accepting_states->insert(
(*it_trans)->condition);
}
//remove hole successors states
if (dest_trans_empty)
{
source->get_transitions((*it_trans)->condition)->remove(
*it_trans);
delete (*it_trans);
it_trans = trans->erase(it_trans);
}
else
{
it_trans++;
}
}
if (conditions_to_livelock_accepting_states != 0)
{
std::set<bdd, bdd_less_than>::iterator it_conditions;
for (it_conditions
= conditions_to_livelock_accepting_states->begin(); it_conditions
!= conditions_to_livelock_accepting_states->end(); it_conditions++)
{
testing_automata->create_transition(source, (*it_conditions),
bddfalse, artificial_livelock_accepting_state, true);
}
}
}
delete conditions_to_livelock_accepting_states;
for (it = states_set.begin(); it != states_set.end(); it++)
{
state_ta_explicit* state = static_cast<state_ta_explicit*> (*it);
state_ta_explicit::transitions* state_trans =
(state)->get_transitions();
bool state_trans_empty = state_trans == 0 || state_trans->empty();
if (state->is_livelock_accepting_state()
&& (!state->is_accepting_state()) && (!state_trans_empty))
state->set_livelock_accepting_state(false);
}
}
namespace
{
typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
}
void
compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state)
{
// We use five main data in this algorithm:
// * sscc: a stack of strongly stuttering-connected components (SSCC)
scc_stack_ta sscc;
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * h: a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
numbered_state_heap* h =
numbered_state_heap_hash_map_factory::instance()->build();
///< Heap of visited states.
// * num: the number of visited nodes. Used to set the order of each
// visited node,
int num = 0;
// * todo: the depth-first search stack. This holds pairs of the
// form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
// over the successors of STATE. In our use, ITERATOR should
// always be freed when TODO is popped, but STATE should not because
// 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<state*> init_set;
ta::states_set_t::const_iterator it;
ta::states_set_t init_states = testing_automata->get_initial_states_set();
for (it = init_states.begin(); it != init_states.end(); it++)
{
state* init_state = (*it);
init_set.push(init_state);
}
while (!init_set.empty())
{
// Setup depth-first search from initial states.
{
state_ta_explicit* init =
down_cast<state_ta_explicit*> (init_set.top());
init_set.pop();
state_ta_explicit* init_clone = init;
numbered_state_heap::state_index_p h_init = h->find(init_clone);
if (h_init.first)
continue;
h->insert(init_clone, ++num);
sscc.push(num);
arc.push(bddfalse);
sscc.top().is_accepting
= testing_automata->is_accepting_state(init);
tgba_succ_iterator* iter = testing_automata->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
}
while (!todo.empty())
{
state* curr = todo.top().first;
numbered_state_heap::state_index_p spi = h->find(curr);
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
{
todo.pop();
continue;
}
// We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack.
if (succ->done())
{
// We have explored all successors of state CURR.
// Backtrack TODO.
todo.pop();
// fill rem with any component removed,
numbered_state_heap::state_index_p spi = h->index(curr);
assert(spi.first);
sscc.rem().push_front(curr);
// When backtracking the root of an SSCC, we must also
// remove that SSCC from the ROOT stacks. We must
// discard from H all reachable states from this SSCC.
assert(!sscc.empty());
if (sscc.top().index == *spi.second)
{
// removing states
std::list<state*>::iterator i;
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));
assert(spi.first->compare(*i) == 0);
assert(*spi.second != -1);
*spi.second = -1;
if (is_livelock_accepting_sscc)
{//if it is an accepting sscc add the state to
//G (=the livelock-accepting states set)
state_ta_explicit * livelock_accepting_state =
down_cast<state_ta_explicit*> (*i);
livelock_accepting_state->set_livelock_accepting_state(
true);
//case STA (Single-pass Testing Automata) or case
//STGTA (Single-pass Transition-based Generalised Testing Automata)
if (artificial_livelock_accepting_state != 0)
livelock_accepting_state->set_accepting_state(
true);
}
}
assert(!arc.empty());
sscc.pop();
arc.pop();
}
// automata reduction
testing_automata->delete_stuttering_and_hole_successors(curr);
delete succ;
// Do not delete CURR: it is a key in H.
continue;
}
// Fetch the values destination state we are interested in...
state* dest = succ->current_state();
bdd acc_cond = succ->current_acceptance_conditions();
// ... and point the iterator to the next successor, for
// the next iteration.
succ->next();
// We do not need SUCC from now on.
// Are we going to a new state through a stuttering transition?
bool is_stuttering_transition =
testing_automata->get_state_condition(curr)
== testing_automata->get_state_condition(dest);
state* dest_clone = dest;
spi = h->find(dest_clone);
// Is this a new state?
if (!spi.first)
{
if (!is_stuttering_transition)
{
init_set.push(dest);
dest_clone->destroy();
continue;
}
// Number it, stack it, and register its successors
// for later processing.
h->insert(dest_clone, ++num);
sscc.push(num);
arc.push(acc_cond);
sscc.top().is_accepting = testing_automata->is_accepting_state(
dest);
tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
iter->first();
todo.push(pair_state_iter(dest, iter));
continue;
}
// If we have reached a dead component, ignore it.
if (*spi.second == -1)
continue;
trace
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
if (!curr->compare(dest))
{
state_ta_explicit * self_loop_state =
down_cast<state_ta_explicit*> (curr);
assert(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);
if (artificial_livelock_accepting_state != 0)
self_loop_state->set_accepting_state(true);
}
trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***"
<< std::endl;
}
// Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SSCC. Any such
// non-dead SSCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs
// to this SSCC too. We are going to merge all states between
// this S1 and S2 into this SSCC.
//
// This merge is easy to do because the order of the SSCC in
// ROOT is ascending: we just have to merge all SSCCs from the
// top of ROOT that have an index greater to the one of
// the SSCC of S2 (called the "threshold").
int threshold = *spi.second;
std::list<state*> rem;
bool acc = false;
while (threshold < sscc.top().index)
{
assert(!sscc.empty());
assert(!arc.empty());
acc |= sscc.top().is_accepting;
acc_cond |= sscc.top().condition;
acc_cond |= arc.top();
rem.splice(rem.end(), sscc.rem());
sscc.pop();
arc.pop();
}
// Note that we do not always have
// threshold == sscc.top().index
// after this loop, the SSCC whose index is threshold might have
// been merged with a lower SSCC.
// Accumulate all acceptance conditions into the merged SSCC.
sscc.top().is_accepting |= acc;
sscc.top().condition |= acc_cond;
sscc.rem().splice(sscc.rem().end(), rem);
}
}
delete h;
trace
<< "*** compute_livelock_acceptance_states: PRE call add_artificial_livelock_accepting_state() method ... (artificial_livelock_accepting_state != 0) :***"
<< (artificial_livelock_accepting_state != 0) << std::endl;
if (artificial_livelock_accepting_state != 0)
add_artificial_livelock_accepting_state(testing_automata,
artificial_livelock_accepting_state);
trace
<< "*** compute_livelock_acceptance_states: POST call add_artificial_livelock_accepting_state() method ***"
<< std::endl;
}
tgbta_explicit*
tgba_to_tgbta(const tgba* tgba_, bdd atomic_propositions_set_)
tgta_explicit*
tgba_to_tgta(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(
state_ta_explicit* artificial_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);
tgta_explicit* tgta = new spot::tgta_explicit(tgba_,
tgba_->all_acceptance_conditions(), artificial_init_state);
// build ta automata:
build_ta(tgbta, atomic_propositions_set_, true, false);
// build a Generalized TA automaton involving a single_pass_emptiness_check
// (without an artificial livelock state):
build_ta(tgta, atomic_propositions_set_, false, 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();
// adapt a ta automata to build tgta automata :
ta::states_set_t states_set = tgta->get_states_set();
ta::states_set_t::iterator it;
tgba_succ_iterator* initial_states_iter = tgbta->succ_iter(
tgbta->get_artificial_initial_state());
tgba_succ_iterator* initial_states_iter = tgta->succ_iter(
tgta->get_artificial_initial_state());
initial_states_iter->first();
if (initial_states_iter->done())
return tgbta;
return tgta;
bdd first_state_condition = (initial_states_iter)->current_condition();
delete initial_states_iter;
@ -630,21 +652,14 @@ namespace spot
bool trans_empty = (trans == 0 || trans->empty());
if (trans_empty || state->is_accepting_state())
{
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;
tgta->create_transition(state, bdd_stutering_transition,
tgta->all_acceptance_conditions(), state);
}
}
if (state->compare(tgbta->get_artificial_initial_state()))
tgbta->create_transition(state, bdd_stutering_transition, bddfalse,
if (state->compare(tgta->get_artificial_initial_state()))
tgta->create_transition(state, bdd_stutering_transition, bddfalse,
state);
state->set_livelock_accepting_state(false);
@ -654,7 +669,7 @@ namespace spot
}
return tgbta;
return tgta;
}

63
src/taalgos/tgba2ta.hh
View file

@ -30,11 +30,11 @@
#include <cassert>
#include "misc/bddlt.hh"
#include "ta/taexplicit.hh"
#include "ta/tgbtaexplicit.hh"
#include "ta/tgtaexplicit.hh"
namespace spot
{
/// \brief Build a spot::tgba_explicit* from an LTL formula.
/// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
/// \ingroup tgba_ta
///
/// This is based on the following paper.
@ -57,50 +57,53 @@ namespace spot
/// \param atomic_propositions_set The set of atomic propositions used in the
/// input TGBA \a tgba_to_convert
///
/// \param degeneralized When false, the returned automaton is a generalized
/// form of TA, called GTA (Generalized Testing Automaton).
/// Like TGBA, GTA use Generalized Büchi acceptance
/// conditions intead of Buchi-accepting states: there are several acceptance
/// sets (of transitions), and a path is accepted if it traverses
/// at least one transition of each set infinitely often or if it contains a
/// livelock-accepting cycle (like a TA). The spot emptiness check algorithm
/// for TA (spot::ta_check::check) can also be used to check GTA.
///
/// \param artificial_initial_state_mode When set, the algorithm will build
/// a TA automaton with an unique initial state. This
/// artificial initial state have one transition to each real initial state,
/// and this transition is labeled by the corresponding initial condition.
/// (see spot::ta::get_artificial_initial_state())
///
/// \param STA_mode When set, the returned TA
/// automaton is a STA (Single-pass Testing Automata): a STA automaton is a TA
/// \param single_pass_emptiness_check When set, the product between the
/// returned automaton and a kripke structure requires only the fist pass of
/// the emptiness check algorithm (see the parameter \c disable_second_pass
/// of the method spot::ta_check::check)
///
///
/// \param artificial_livelock_state_mode When set, the returned TA automaton
/// is a STA (Single-pass Testing Automata): a STA automaton is a TA
/// where: for every livelock-accepting state s, if s is not also a
/// Buchi-accepting state, then s has no successors. A STA product requires
/// only one-pass emptiness check algorithm (see spot::ta_check::check)
///
/// \param degeneralized When false, the returned automaton is a generalized
/// form of TA, called TGTA (Transition-based Generalized Testing Automaton).
/// Like TGBA, TGTA use Generalized Büchi acceptance
/// conditions intead of Büchi-accepting states: there are several acceptance
/// sets (of transitions), and a path is accepted if it traverses
/// at least one transition of each set infinitely often or if it contains a
/// livelock-accepting cycle.
///
/// \return A spot::ta_explicit that recognizes the same language as the
/// TGBA \a tgba_to_convert.
ta_explicit*
tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set,
bool artificial_initial_state_mode = true, bool STA_mode = false,
bool degeneralized = true);
bool degeneralized = true, bool artificial_initial_state_mode = true,
bool single_pass_emptiness_check = false,
bool artificial_livelock_state_mode = false);
stgta_explicit*
tgba_to_stgta(const tgba* tgba_to_convert, bdd atomic_propositions_set);
//artificial_livelock_accepting_state is used in the case of
//STA (Single-pass Testing Automata) or in the case
//STGTA (Single-pass Transition-based Generalised Testing Automata)
void
compute_livelock_acceptance_states(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state = 0);
//artificial_livelock_accepting_state is added to transform TA into
//STA (Single-pass Testing Automata) or to transform TGTA into
//STGTA (Single-pass Transition-based Generalised Testing Automata)
void
add_artificial_livelock_accepting_state(ta_explicit* testing_automata,
state_ta_explicit* artificial_livelock_accepting_state);
/// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
/// \ingroup tgba_ta
/// \param tgba_to_convert The TGBA automaton to convert into a TGTA automaton
///
/// \param atomic_propositions_set The set of atomic propositions used in the
/// input TGBA \a tgba_to_convert
///
/// \return A spot::tgta_explicit (spot::tgta) that recognizes the same
/// language as the TGBA \a tgba_to_convert.
tgta_explicit*
tgba_to_tgta(const tgba* tgba_to_convert, bdd atomic_propositions_set);
}