GTA (Generalized Testing Automata) implementation
* 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/Makefile.am, src/taalgos/dotty.cc, src/taalgos/emptinessta.cc, src/taalgos/minimize.cc, src/taalgos/minimize.hh, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgbatest/ltl2tgba.cc: changes introduced to add a new form of TA called GTA (Generalized Testing Automata). GTA is a TA with acceptance- conditions added on transitions.
This commit is contained in:
Ala-Eddine Ben-Salem
Alexandre Duret-Lutz
parent
c7f4b8e262
commit
83e7f0fa18
14 changed files with 726 additions and 34 deletions
|
|
@ -34,6 +34,7 @@ namespace spot
|
|||
{
|
||||
index = i;
|
||||
is_accepting = false;
|
||||
condition = bddfalse;
|
||||
}
|
||||
|
||||
scc_stack_ta::connected_component&
|
||||
|
|
|
|||
22
src/ta/ta.hh
22
src/ta/ta.hh
|
|
@ -70,7 +70,6 @@ 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;
|
||||
|
||||
|
|
@ -80,6 +79,16 @@ namespace spot
|
|||
virtual void
|
||||
free_state(const spot::state* s) const = 0;
|
||||
|
||||
/// \brief Return the set of all acceptance conditions used
|
||||
/// by this automaton.
|
||||
///
|
||||
/// The goal of the emptiness check is to ensure that
|
||||
/// a strongly connected component walks through each
|
||||
/// of these acceptiong conditions. I.e., the union
|
||||
/// of the acceptiong conditions of all transition in
|
||||
/// the SCC should be equal to the result of this function.
|
||||
virtual bdd all_acceptance_conditions() const = 0;
|
||||
|
||||
};
|
||||
|
||||
/// Successor iterators used by spot::ta.
|
||||
|
|
@ -107,11 +116,8 @@ namespace spot
|
|||
is_stuttering_transition() const = 0;
|
||||
|
||||
bdd
|
||||
current_acceptance_conditions() const
|
||||
{
|
||||
assert(!done());
|
||||
return bddfalse;
|
||||
}
|
||||
current_acceptance_conditions() const = 0;
|
||||
|
||||
};
|
||||
|
||||
// A stack of Strongly-Connected Components
|
||||
|
|
@ -128,6 +134,10 @@ namespace spot
|
|||
|
||||
bool is_accepting;
|
||||
|
||||
/// The bdd condition is the union of all acceptance conditions of
|
||||
/// transitions which connect the states of the connected component.
|
||||
bdd condition;
|
||||
|
||||
std::list<state*> rem;
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -83,6 +83,13 @@ namespace spot
|
|||
return (*i_)->condition;
|
||||
}
|
||||
|
||||
bdd
|
||||
ta_explicit_succ_iterator::current_acceptance_conditions() const
|
||||
{
|
||||
assert(!done());
|
||||
return (*i_)->acceptance_conditions;
|
||||
}
|
||||
|
||||
bool
|
||||
ta_explicit_succ_iterator::is_stuttering_transition() const
|
||||
{
|
||||
|
|
@ -138,6 +145,10 @@ namespace spot
|
|||
!= transitions_condition->end() && !transition_found); it_trans++)
|
||||
{
|
||||
transition_found = ((*it_trans)->dest == t->dest);
|
||||
if (transition_found)
|
||||
{
|
||||
(*it_trans)->acceptance_conditions |= t->acceptance_conditions;
|
||||
}
|
||||
}
|
||||
|
||||
if (!transition_found)
|
||||
|
|
@ -313,9 +324,10 @@ namespace spot
|
|||
// ta_explicit
|
||||
|
||||
|
||||
ta_explicit::ta_explicit(const tgba* tgba_,
|
||||
ta_explicit::ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
|
||||
state_ta_explicit* artificial_initial_state) :
|
||||
tgba_(tgba_), artificial_initial_state_(artificial_initial_state)
|
||||
tgba_(tgba), all_acceptance_conditions_(all_acceptance_conditions),
|
||||
artificial_initial_state_(artificial_initial_state)
|
||||
{
|
||||
get_dict()->register_all_variables_of(&tgba_, this);
|
||||
if (artificial_initial_state != 0)
|
||||
|
|
@ -341,6 +353,7 @@ namespace spot
|
|||
delete tgba_;
|
||||
}
|
||||
|
||||
|
||||
state_ta_explicit*
|
||||
ta_explicit::add_state(state_ta_explicit* s)
|
||||
{
|
||||
|
|
@ -386,6 +399,19 @@ namespace spot
|
|||
state_ta_explicit::transition* t = new state_ta_explicit::transition;
|
||||
t->dest = dest;
|
||||
t->condition = condition;
|
||||
t->acceptance_conditions = bddfalse;
|
||||
source->add_transition(t);
|
||||
|
||||
}
|
||||
|
||||
void
|
||||
ta_explicit::create_transition(state_ta_explicit* source, bdd condition,
|
||||
bdd acceptance_conditions, state_ta_explicit* dest)
|
||||
{
|
||||
state_ta_explicit::transition* t = new state_ta_explicit::transition;
|
||||
t->dest = dest;
|
||||
t->condition = condition;
|
||||
t->acceptance_conditions = acceptance_conditions;
|
||||
source->add_transition(t);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@ namespace spot
|
|||
class ta_explicit : public ta
|
||||
{
|
||||
public:
|
||||
ta_explicit(const tgba* tgba_, state_ta_explicit* artificial_initial_state =
|
||||
0);
|
||||
ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
|
||||
state_ta_explicit* artificial_initial_state = 0);
|
||||
|
||||
const tgba*
|
||||
get_tgba() const;
|
||||
|
|
@ -57,6 +57,10 @@ namespace spot
|
|||
create_transition(state_ta_explicit* source, bdd condition,
|
||||
state_ta_explicit* dest);
|
||||
|
||||
void
|
||||
create_transition(state_ta_explicit* source, bdd condition,
|
||||
bdd acceptance_conditions, state_ta_explicit* dest);
|
||||
|
||||
void
|
||||
delete_stuttering_transitions();
|
||||
// ta interface
|
||||
|
|
@ -114,16 +118,32 @@ namespace spot
|
|||
return states_set_;
|
||||
}
|
||||
|
||||
/// \brief Return the set of all acceptance conditions used
|
||||
/// by this automaton.
|
||||
///
|
||||
/// The goal of the emptiness check is to ensure that
|
||||
/// a strongly connected component walks through each
|
||||
/// of these acceptiong conditions. I.e., the union
|
||||
/// of the acceptiong conditions of all transition in
|
||||
/// the SCC should be equal to the result of this function.
|
||||
bdd
|
||||
all_acceptance_conditions() const
|
||||
{
|
||||
return all_acceptance_conditions_;;
|
||||
}
|
||||
|
||||
|
||||
private:
|
||||
// Disallow copy.
|
||||
ta_explicit(const ta_explicit& other);
|
||||
ta_explicit&
|
||||
operator=(const ta_explicit& other);
|
||||
|
||||
const tgba* tgba_;
|
||||
bdd all_acceptance_conditions_;
|
||||
state_ta_explicit* artificial_initial_state_;
|
||||
ta::states_set_t states_set_;
|
||||
ta::states_set_t initial_states_set_;
|
||||
const tgba* tgba_;
|
||||
state_ta_explicit* artificial_initial_state_;
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -136,6 +156,7 @@ namespace spot
|
|||
struct transition
|
||||
{
|
||||
bdd condition;
|
||||
bdd acceptance_conditions;
|
||||
state_ta_explicit* dest;
|
||||
};
|
||||
|
||||
|
|
@ -201,6 +222,8 @@ namespace spot
|
|||
void
|
||||
free_transitions();
|
||||
|
||||
|
||||
|
||||
private:
|
||||
const state* tgba_state_;
|
||||
const bdd tgba_condition_;
|
||||
|
|
@ -232,6 +255,9 @@ namespace spot
|
|||
virtual bdd
|
||||
current_condition() const;
|
||||
|
||||
virtual bdd
|
||||
current_acceptance_conditions() const;
|
||||
|
||||
virtual bool
|
||||
is_stuttering_transition() const;
|
||||
|
||||
|
|
|
|||
|
|
@ -190,6 +190,7 @@ namespace spot
|
|||
//if stuttering transition, the TA automata stays in the same state
|
||||
current_state_ = new state_ta_product(source_->get_ta_state(),
|
||||
kripke_current_dest_state->clone());
|
||||
current_acceptance_conditions_ = bddfalse;
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
@ -197,6 +198,8 @@ namespace spot
|
|||
{
|
||||
current_state_ = new state_ta_product(ta_succ_it_->current_state(),
|
||||
kripke_current_dest_state->clone());
|
||||
current_acceptance_conditions_
|
||||
= ta_succ_it_->current_acceptance_conditions();
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
@ -249,6 +252,19 @@ namespace spot
|
|||
return current_condition_;
|
||||
}
|
||||
|
||||
bdd
|
||||
ta_succ_iterator_product::current_acceptance_conditions() const
|
||||
{
|
||||
// assert(!done());
|
||||
// bdd kripke_source_condition = kripke_->state_condition(source_->get_kripke_state());
|
||||
// state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
|
||||
// bdd kripke_current_dest_condition = kripke_->state_condition(kripke_succ_it_current_state);
|
||||
// delete kripke_succ_it_current_state;
|
||||
// return bdd_setxor(kripke_source_condition, kripke_current_dest_condition);
|
||||
|
||||
return current_acceptance_conditions_;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// ta_product
|
||||
|
||||
|
|
@ -392,6 +408,12 @@ namespace spot
|
|||
return is_hole_state;
|
||||
}
|
||||
|
||||
bdd
|
||||
ta_product::all_acceptance_conditions() const
|
||||
{
|
||||
return get_ta()->all_acceptance_conditions();
|
||||
}
|
||||
|
||||
bdd
|
||||
ta_product::get_state_condition(const spot::state* s) const
|
||||
{
|
||||
|
|
|
|||
|
|
@ -97,6 +97,9 @@ namespace spot
|
|||
bdd
|
||||
current_condition() const;
|
||||
|
||||
bdd
|
||||
current_acceptance_conditions() const;
|
||||
|
||||
bool
|
||||
is_stuttering_transition() const;
|
||||
|
||||
|
|
@ -121,6 +124,7 @@ namespace spot
|
|||
tgba_succ_iterator* kripke_succ_it_;
|
||||
state_ta_product* current_state_;
|
||||
bdd current_condition_;
|
||||
bdd current_acceptance_conditions_;
|
||||
bool is_stuttering_transition_;
|
||||
bdd kripke_source_condition;
|
||||
state * kripke_current_dest_state;
|
||||
|
|
@ -173,10 +177,12 @@ namespace spot
|
|||
virtual bool
|
||||
is_hole_state_in_ta_component(const spot::state* s) const;
|
||||
|
||||
|
||||
virtual bdd
|
||||
get_state_condition(const spot::state* s) const;
|
||||
|
||||
virtual bdd
|
||||
all_acceptance_conditions() const;
|
||||
|
||||
virtual void
|
||||
free_state(const spot::state* s) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
|||
taalgosdir = $(pkgincludedir)/taalgos
|
||||
|
||||
taalgos_HEADERS = \
|
||||
sba2ta.hh \
|
||||
tgba2ta.hh \
|
||||
dotty.hh \
|
||||
reachiter.hh \
|
||||
stats.hh \
|
||||
|
|
@ -33,10 +33,9 @@ taalgos_HEADERS = \
|
|||
minimize.hh \
|
||||
emptinessta.hh
|
||||
|
||||
|
||||
noinst_LTLIBRARIES = libtaalgos.la
|
||||
libtaalgos_la_SOURCES = \
|
||||
sba2ta.cc \
|
||||
tgba2ta.cc \
|
||||
dotty.cc \
|
||||
reachiter.cc \
|
||||
stats.cc \
|
||||
|
|
|
|||
|
|
@ -119,7 +119,8 @@ namespace spot
|
|||
|
||||
os_ << " " << in << " -> " << out << " [label=\"";
|
||||
escape_str(os_, bdd_format_accset(t_automata_->get_dict(),
|
||||
si->current_condition()))
|
||||
si->current_condition()) + "\n" + bdd_format_accset(
|
||||
t_automata_->get_dict(), si->current_acceptance_conditions()))
|
||||
|
||||
<< "\"]" << std::endl;
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@
|
|||
#include "emptinessta.hh"
|
||||
#include "misc/memusage.hh"
|
||||
#include <math.h>
|
||||
#include "tgba/bddprint.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -51,6 +52,12 @@ namespace spot
|
|||
|
||||
// We use five main data in this algorithm:
|
||||
|
||||
// * scc: a stack of strongly connected components (SCC)
|
||||
scc;
|
||||
|
||||
// * 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 =
|
||||
|
|
@ -108,6 +115,7 @@ namespace spot
|
|||
|
||||
h->insert(init, ++num);
|
||||
scc.push(num);
|
||||
arc.push(bddfalse);
|
||||
|
||||
ta_succ_iterator* iter = a_->succ_iter(init);
|
||||
iter->first();
|
||||
|
|
@ -187,6 +195,9 @@ namespace spot
|
|||
}
|
||||
dec_depth(scc.rem().size());
|
||||
scc.pop();
|
||||
assert(!arc.empty());
|
||||
arc.pop();
|
||||
|
||||
}
|
||||
|
||||
delete succ;
|
||||
|
|
@ -201,6 +212,8 @@ namespace spot
|
|||
// Fetch the values destination state we are interested in...
|
||||
state* dest = succ->current_state();
|
||||
|
||||
bdd acc_cond = succ->current_acceptance_conditions();
|
||||
|
||||
bool curr_is_livelock_hole_state_in_ta_component =
|
||||
(a_->is_hole_state_in_ta_component(curr))
|
||||
&& a_->is_livelock_accepting_state(curr);
|
||||
|
|
@ -228,6 +241,7 @@ namespace spot
|
|||
// for later processing.
|
||||
h->insert(dest, ++num);
|
||||
scc.push(num);
|
||||
arc.push(acc_cond);
|
||||
|
||||
ta_succ_iterator* iter = a_->succ_iter(dest);
|
||||
iter->first();
|
||||
|
|
@ -265,13 +279,18 @@ namespace spot
|
|||
while (threshold < scc.top().index)
|
||||
{
|
||||
assert(!scc.empty());
|
||||
assert(!arc.empty());
|
||||
|
||||
acc |= scc.top().is_accepting;
|
||||
acc_cond |= scc.top().condition;
|
||||
acc_cond |= arc.top();
|
||||
|
||||
rem.splice(rem.end(), scc.rem());
|
||||
scc.pop();
|
||||
arc.pop();
|
||||
|
||||
}
|
||||
|
||||
// Note that we do not always have
|
||||
// threshold == scc.top().index
|
||||
// after this loop, the SSCC whose index is threshold might have
|
||||
|
|
@ -279,13 +298,23 @@ namespace spot
|
|||
|
||||
// Accumulate all acceptance conditions into the merged SSCC.
|
||||
scc.top().is_accepting |= acc;
|
||||
scc.top().condition |= acc_cond;
|
||||
|
||||
scc.rem().splice(scc.rem().end(), rem);
|
||||
if (scc.top().is_accepting)
|
||||
bool is_accepting_sscc = (scc.top().is_accepting)
|
||||
|| (scc.top().condition == a_->all_acceptance_conditions());
|
||||
|
||||
if (is_accepting_sscc)
|
||||
{
|
||||
clear(h, todo, init_set);
|
||||
trace
|
||||
<< "PASS 1: SUCCESS" << std::endl;
|
||||
trace
|
||||
<< "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(),
|
||||
scc.top().condition) << std::endl;
|
||||
trace
|
||||
<< "PASS 1: a_->all_acceptance_conditions() : " << bdd_format_accset(a_->get_dict(),
|
||||
a_->all_acceptance_conditions()) << std::endl;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@
|
|||
#include "ta/taproduct.hh"
|
||||
#include "taalgos/statessetbuilder.hh"
|
||||
#include "tgba/tgbaexplicit.hh"
|
||||
#include "tgba/bddprint.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -75,7 +76,7 @@ namespace spot
|
|||
build_result(const ta* a, std::list<hash_set*>& sets)
|
||||
{
|
||||
tgba_explicit_number* tgba = new tgba_explicit_number(a->get_dict());
|
||||
ta_explicit* ta = new ta_explicit(tgba);
|
||||
ta_explicit* ta = new ta_explicit(tgba, a->all_acceptance_conditions());
|
||||
|
||||
// For each set, create a state in the tgbaulting automaton.
|
||||
// For a state s, state_num[s] is the number of the state in the minimal
|
||||
|
|
@ -111,7 +112,7 @@ namespace spot
|
|||
bool is_accepting_state = a->is_accepting_state(src);
|
||||
bool is_livelock_accepting_state = a->is_livelock_accepting_state(src);
|
||||
|
||||
state_ta_explicit* new_src = new state_ta_explicit(tgba_state,
|
||||
state_ta_explicit* new_src = new state_ta_explicit(tgba_state->clone(),
|
||||
tgba_condition, is_initial_state, is_accepting_state,
|
||||
is_livelock_accepting_state);
|
||||
|
||||
|
|
@ -150,7 +151,7 @@ namespace spot
|
|||
bool is_livelock_accepting_state = a->is_livelock_accepting_state(
|
||||
dst);
|
||||
|
||||
state_ta_explicit* new_dst = new state_ta_explicit(tgba_state,
|
||||
state_ta_explicit* new_dst = new state_ta_explicit(tgba_state->clone(),
|
||||
tgba_condition, is_initial_state, is_accepting_state,
|
||||
is_livelock_accepting_state);
|
||||
|
||||
|
|
@ -169,7 +170,7 @@ namespace spot
|
|||
else if (is_initial_state)
|
||||
ta->add_to_initial_states_set(new_dst);
|
||||
|
||||
ta->create_transition(ta_src, succit->current_condition(), ta_dst);
|
||||
ta->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst);
|
||||
|
||||
}
|
||||
delete succit;
|
||||
|
|
@ -245,7 +246,7 @@ namespace spot
|
|||
hash_map state_set_map;
|
||||
|
||||
// Size of ta_
|
||||
unsigned size = states_set.size();
|
||||
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_);
|
||||
|
|
@ -347,6 +348,11 @@ namespace spot
|
|||
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)
|
||||
{
|
||||
|
|
@ -373,7 +379,14 @@ namespace spot
|
|||
hash_map::const_iterator i = state_set_map.find(dst);
|
||||
|
||||
assert(i != state_set_map.end());
|
||||
f |= (bdd_ithvar(i->second) & si->current_condition());
|
||||
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;;
|
||||
}
|
||||
delete si;
|
||||
|
||||
|
|
@ -470,7 +483,7 @@ namespace spot
|
|||
std::list<hash_set*>::iterator itdone;
|
||||
for (itdone = done.begin(); itdone != done.end(); ++itdone)
|
||||
delete *itdone;
|
||||
delete ta_;
|
||||
//delete ta_;
|
||||
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ namespace spot
|
|||
ta*
|
||||
minimize_ta(const ta* ta_);
|
||||
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
||||
|
|
|
|||
501
src/taalgos/tgba2ta.cc
Normal file
501
src/taalgos/tgba2ta.cc
Normal file
|
|
@ -0,0 +1,501 @@
|
|||
// 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 "tgba2ta.hh"
|
||||
#include "taalgos/statessetbuilder.hh"
|
||||
|
||||
using namespace std;
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
ta*
|
||||
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;
|
||||
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_, 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;
|
||||
while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
|
||||
atomic_propositions_set_, bddtrue)) != bddfalse)
|
||||
{
|
||||
tgba_condition -= satone_tgba_condition;
|
||||
state_ta_explicit* init_state;
|
||||
if (degeneralized)
|
||||
{
|
||||
init_state = new state_ta_explicit(tgba_init_state->clone(),
|
||||
satone_tgba_condition, true,
|
||||
((tgba_sba_proxy*) tgba_)->state_is_accepting(tgba_init_state));
|
||||
}
|
||||
else
|
||||
{
|
||||
init_state = new state_ta_explicit(tgba_init_state->clone(),
|
||||
satone_tgba_condition, true, false);
|
||||
}
|
||||
|
||||
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 tgba_acceptance_conditions =
|
||||
tgba_succ_it->current_acceptance_conditions();
|
||||
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;
|
||||
if (degeneralized)
|
||||
{
|
||||
|
||||
new_dest = new state_ta_explicit(tgba_state->clone(),
|
||||
dest_condition, false,
|
||||
((tgba_sba_proxy*) tgba_)->state_is_accepting(
|
||||
tgba_state));
|
||||
|
||||
}
|
||||
else
|
||||
{
|
||||
new_dest = new state_ta_explicit(tgba_state->clone(),
|
||||
dest_condition, false, false);
|
||||
|
||||
}
|
||||
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()),
|
||||
tgba_acceptance_conditions, 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)
|
||||
{
|
||||
|
||||
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);
|
||||
|
||||
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()
|
||||
&& !dest->is_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),
|
||||
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;
|
||||
|
||||
// * 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->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);
|
||||
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->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)) || (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());
|
||||
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);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
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->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);
|
||||
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;
|
||||
|
||||
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());
|
||||
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;
|
||||
|
||||
}
|
||||
}
|
||||
51
src/taalgos/tgba2ta.hh
Normal file
51
src/taalgos/tgba2ta.hh
Normal file
|
|
@ -0,0 +1,51 @@
|
|||
// 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*
|
||||
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,
|
||||
bool degeneralized = true);
|
||||
|
||||
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
|
||||
|
|
@ -66,7 +66,7 @@
|
|||
#include "kripkeparse/public.hh"
|
||||
#include "tgbaalgos/simulation.hh"
|
||||
|
||||
#include "taalgos/sba2ta.hh"
|
||||
#include "taalgos/tgba2ta.hh"
|
||||
#include "taalgos/dotty.hh"
|
||||
#include "taalgos/stats.hh"
|
||||
|
||||
|
|
@ -1091,11 +1091,11 @@ main(int argc, char** argv)
|
|||
|
||||
if (ta_opt)
|
||||
{
|
||||
const spot::tgba_sba_proxy* degeneralized_new = 0;
|
||||
const spot::tgba_sba_proxy* degeneralized =
|
||||
dynamic_cast<const spot::tgba_sba_proxy*> (a);
|
||||
if (degeneralized == 0)
|
||||
degeneralized_new = degeneralized = new spot::tgba_sba_proxy(a);
|
||||
// const spot::tgba_sba_proxy* degeneralized_new = 0;
|
||||
// const spot::tgba_sba_proxy* degeneralized =
|
||||
// dynamic_cast<const spot::tgba_sba_proxy*> (a);
|
||||
// if (degeneralized == 0)
|
||||
// degeneralized_new = degeneralized = new spot::tgba_sba_proxy(a);
|
||||
|
||||
spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0);
|
||||
|
||||
|
|
@ -1104,15 +1104,19 @@ main(int argc, char** argv)
|
|||
!= aps->end(); ++i)
|
||||
{
|
||||
bdd atomic_prop = bdd_ithvar(
|
||||
(degeneralized->get_dict())->var_map[*i]);
|
||||
(a->get_dict())->var_map[*i]);
|
||||
|
||||
atomic_props_set_bdd &= atomic_prop;
|
||||
|
||||
}
|
||||
delete aps;
|
||||
|
||||
spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock);
|
||||
if (opt_minimize) testing_automata = minimize_ta(testing_automata);
|
||||
spot::ta* testing_automata = tgba_to_ta(a, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock, degeneralize_opt == DegenSBA);
|
||||
spot::ta* testing_automata_nm = 0;
|
||||
if (opt_minimize) {
|
||||
testing_automata_nm = testing_automata;
|
||||
testing_automata = minimize_ta(testing_automata);
|
||||
}
|
||||
|
||||
if (output != -1)
|
||||
{
|
||||
|
|
@ -1130,6 +1134,8 @@ main(int argc, char** argv)
|
|||
}
|
||||
tm.stop("producing output");
|
||||
}
|
||||
|
||||
delete testing_automata_nm;
|
||||
delete testing_automata;
|
||||
output = -1;
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue