Commit 9b5340b9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

dstarparse: get rid of the deticated data structures and conversions

* src/dstarparse/dstarparse.yy: Use the twa_graph_ptr to store the
acceptance condition.
* src/dstarparse/dra2ba.cc, src/dstarparse/dstar2tgba.cc,
src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc: Delete
all these conversion routines.
* src/dstarparse/public.hh, src/dstarparse/Makefile.am: Adjust.
* src/bin/dstar2tgba.cc: Adjust to call to_generalized_buchi()
instead.
* src/bin/ltlcross.cc: Adjust to call remove_fin() instead.
* src/bin/ltldo.cc: Use the parsed automaton as-is.
* src/tests/degenid.test, src/tests/dstar.test, src/tests/ikwiad.cc:
Adjust test cases.
parent 5f0b6dc3
......@@ -37,6 +37,7 @@
#include "twaalgos/hoa.hh"
#include "twaalgos/neverclaim.hh"
#include "twaalgos/stats.hh"
#include "twaalgos/totgba.hh"
#include "twa/bddprint.hh"
#include "misc/optionmap.hh"
#include "misc/timer.hh"
......@@ -290,7 +291,7 @@ namespace
}
if (has('A'))
daut_acc_ = daut->accpair_count;
daut_acc_ = daut->aut->num_sets() / 2;
if (has('C'))
daut_scc_ = spot::scc_info(daut->aut).scc_count();
......@@ -355,7 +356,7 @@ namespace
spot::stopwatch sw;
sw.start();
auto nba = spot::dstar_to_tgba(daut);
auto nba = spot::to_generalized_buchi(daut->aut);
auto aut = post.run(nba, 0);
const double conversion_time = sw.stop();
......
......@@ -620,14 +620,14 @@ namespace
st->in_states= s.states;
st->in_edges = s.transitions;
st->in_transitions = s.sub_transitions;
st->in_acc = aut->accpair_count;
st->in_acc = aut->aut->num_sets() / 2;
st->in_scc = spot::scc_info(aut->aut).scc_count();
}
// convert it into TGBA for further processing
if (verbose)
std::cerr << "info: converting " << type << " to TGBA\n";
res = dstar_to_tgba(aut);
res = remove_fin(aut->aut);
}
break;
}
......
......@@ -40,6 +40,7 @@
#include "misc/timer.hh"
#include "twaalgos/lbtt.hh"
#include "twaalgos/relabel.hh"
#include "twaalgos/totgba.hh"
#include "parseaut/public.hh"
#include "dstarparse/public.hh"
......@@ -185,7 +186,7 @@ namespace
}
else
{
res = dstar_to_tgba(aut);
res = aut->aut;
}
break;
}
......
## -*- coding: utf-8 -*-
## Copyright (C) 2013 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
## Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
......@@ -52,10 +52,6 @@ EXTRA_DIST = $(DSTARPARSE_YY)
libdstarparse_la_SOURCES = \
fmterror.cc \
dra2ba.cc \
dstar2tgba.cc \
nra2nba.cc \
nsa2tgba.cc \
$(FROM_DSTARPARSE_YY) \
dstarscan.ll \
parsedecl.hh
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "public.hh"
#include "twa/twamask.hh"
#include "twaalgos/scc.hh"
#include "twaalgos/reachiter.hh"
#include "twaalgos/gtec/gtec.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/dot.hh"
namespace spot
{
// IMPORTANT NOTE: If you attempt to follow Krishnan et
// al. (ISAAC'94) paper while reading this code, make sure you
// understand the difference between their Rabin acceptance
// definition and the one we are using.
//
// Here, a cycle is accepting in a Rabin automaton if there exists
// an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ are
// visited while no states from Uᵢ are visited. This is the
// same definition used by ltl2dstar.
//
// In the Krishnan et al. paper, a cycle is accepting in a Rabin
// automaton if there exists an acceptance pair (Lᵢ, Uᵢ) such that
// some states from Lᵢ are visited and all visited states belongs to
// Uᵢ. In other words, you can switch from one definition to
// the other by complementing the Uᵢ set.
//
// This is a source of confusion; you have been warned.
// This function is defined in nra2nba.cc, and used only here.
SPOT_LOCAL
twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra,
const const_twa_ptr& aut);
namespace
{
typedef std::list<const state*> state_list;
// The functions that take aut and dra as first arguments are
// either called on the main automaton, in which case dra->aut ==
// aut, or it is called on a sub-automaton in which case aut is a
// masked version of dra->aut. So we should always explore the
// automaton aut, but because the state of aut are states of
// dra->aut, we can use dra->aut to get labels, and dra->acccs to
// retrive acceptances.
static bool
filter_states(const const_twa_ptr& aut,
const const_dstar_aut_ptr& dra,
const state_list& sl,
state_list& final,
state_list& nonfinal);
static bool
filter_scc(const const_twa_ptr& aut,
const const_dstar_aut_ptr& dra,
state_list& final,
state_list& nonfinal)
{
// Iterate over all non-trivial SCCs.
scc_map sm(aut);
sm.build_map();
for (unsigned scc_max = sm.scc_count(), scc = 0;
scc < scc_max; ++scc)
{
if (sm.trivial(scc))
{
nonfinal.push_back(sm.one_state_of(scc));
continue;
}
// Get the list of states of that SCC
const std::list<const state*>& sl = sm.states_of(scc);
assert(!sl.empty());
if (!filter_states(aut, dra, sl, final, nonfinal))
return false;
}
return true;
}
static bool
filter_states(const const_twa_ptr& aut,
const const_dstar_aut_ptr& dra,
const state_list& sl,
state_list& final,
state_list& nonfinal)
{
// Check whether the SCC composed of all states in sl contains
// non-accepting cycles.
//
// A cycle is accepting (in a Rabin automaton) if there exists
// an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ
// are visited while no states from Uᵢ are visited.
//
// Consequently, a cycle is non-accepting if for all acceptance
// pairs (Lᵢ, Uᵢ), either no states from Lᵢ are visited or some
// states from Uᵢ are visited. (This corresponds to an
// accepting cycle with Streett acceptance.)
//
// Now we consider the SCC as one large cycle and check its
// intersection with all Lᵢs and Uᵢs. Let l=[l₁,l₂,...] and
// u=[u₁,u₂,...] be bitvectors where bit lᵢ (resp. uᵢ)
// indicates that Lᵢ (resp. Uᵢ) has been visited in the SCC.
state_list::const_iterator it = sl.begin();
int num = dra->aut->state_number(*it++);
bitvect* l = dra->accsets->at(num * 2).clone();
bitvect* u = dra->accsets->at(num * 2 + 1).clone();
for (; it != sl.end(); ++it)
{
num = dra->aut->state_number(*it);
*l |= dra->accsets->at(num * 2);
*u |= dra->accsets->at(num * 2 + 1);
}
// If we have l&!u = [0,0,...] that means that the cycle formed
// by the entire SCC is not accepting. However that does not
// necessarily imply that all cycles in the SCC are also
// non-accepting. We may have a smaller cycle that is
// accepting, but which becomes non-accepting when extended with
// more states.
*l -= *u;
delete u;
if (l->is_fully_clear())
{
delete l;
// Check whether the SCC is accepting. We do that by simply
// converting that SCC into a TGBA and running our emptiness
// check. This is not a really smart implementation and
// could be improved.
{
state_set keep(sl.begin(), sl.end());
auto masked = build_twa_mask_keep(dra->aut, keep, sl.front());
if (!nra_to_nba(dra, masked)->is_empty())
// This SCC is not DBA-realizable.
return false;
}
for (state_list::const_iterator i = sl.begin();
i != sl.end(); ++i)
nonfinal.push_back(*i);
return true;
}
// The bits sets in *l corresponds to Lᵢs that have been seen
// without seeing the matching Uᵢ. In this SCC, any state in Lᵢ
// is therefore final. Otherwise we do not know: it is possible
// that there is a non-accepting cycle in the SCC that do not
// visit Lᵢ.
state_set unknown;
for (it = sl.begin(); it != sl.end(); ++it)
{
num = dra->aut->state_number(*it);
bitvect* l2 = dra->accsets->at(num * 2).clone();
*l2 &= *l;
if (!l2->is_fully_clear())
{
final.push_back(*it);
}
else
{
unknown.insert(*it);
}
delete l2;
}
delete l;
// Check whether it is possible to build non-accepting cycles
// using only the "unknown" states.
while (!unknown.empty())
{
//std::cerr << "unknown\n";
// Build a sub-automaton for just the unknown states,
// starting from any state in the SCC.
auto scc_mask = build_twa_mask_keep(aut, unknown, *unknown.begin());
state_list local_final;
state_list local_nonfinal;
bool dbarealizable =
filter_scc(scc_mask, dra, local_final, local_nonfinal);
if (!dbarealizable)
return false;
for (state_list::const_iterator i = local_final.begin();
i != local_final.end(); ++i)
unknown.erase(*i);
final.splice(final.end(), local_final);
for (state_list::const_iterator i = local_nonfinal.begin();
i != local_nonfinal.end(); ++i)
unknown.erase(*i);
nonfinal.splice(nonfinal.end(), local_nonfinal);
}
return true;
}
class dra_to_ba_worker: public tgba_reachable_iterator_depth_first
{
public:
dra_to_ba_worker(const const_dstar_aut_ptr& a,
const state_set& final,
const scc_map& sm,
const std::vector<bool>& realizable):
tgba_reachable_iterator_depth_first(a->aut),
in_(a),
out_(make_twa_graph(a->aut->get_dict())),
final_(final),
num_states_(a->aut->num_states()),
sm_(sm),
realizable_(realizable)
{
out_->copy_ap_of(a->aut);
out_->prop_state_based_acc();
acc_ = out_->set_buchi();
out_->new_states(num_states_ * (a->accpair_count + 1));
out_->set_init_state(a->aut->get_init_state_number());
}
twa_graph_ptr
result()
{
return out_;
}
void
process_link(const state* sin, int,
const state* sout, int,
const twa_succ_iterator* si)
{
int in = in_->aut->state_number(sin);
int out = in_->aut->state_number(sout);
unsigned in_scc = sm_.scc_of_state(sin);
bdd cond = si->current_condition();
unsigned t = out_->new_edge(in, out, cond);
if (realizable_[in_scc])
{
if (final_.find(sin) != final_.end())
out_->edge_data(t).acc = acc_;
}
else if (sm_.scc_of_state(sout) == in_scc)
{
// Create one clone of the SCC per accepting pair,
// removing states from the Ui part of the (Li, Ui) pairs.
// (Or the Ei part of Löding's (Ei, Fi) pairs.)
bitvect& l = in_->accsets->at(2 * in);
bitvect& u = in_->accsets->at(2 * in + 1);
for (size_t i = 0; i < in_->accpair_count; ++i)
{
int shift = num_states_ * (i + 1);
// In the Ui set. (Löding's Ei set.)
if (!u.get(i))
{
// Transition t1 is a non-deterministic jump
// from the original automaton to the i-th clone.
//
// Transition t2 constructs the clone.
//
// Löding creates transition t1 regardless of the
// acceptance set. We restrict it to the non-Li
// states. Both his definition and this
// implementation create more transitions than needed:
// we do not need more than one transition per
// accepting cycle.
out_->new_edge(in, out + shift, cond);
// Acceptance transitions are those in the Li
// set. (Löding's Fi set.)
out_->new_acc_edge(in + shift, out + shift, cond, l.get(i));
}
}
}
}
protected:
const const_dstar_aut_ptr& in_;
twa_graph_ptr out_;
const state_set& final_;
size_t num_states_;
acc_cond::mark_t acc_;
const scc_map& sm_;
const std::vector<bool>& realizable_;
};
}
twa_graph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba)
{
assert(dra->type == Rabin);
state_list final;
state_list nonfinal;
// Iterate over all non-trivial SCCs.
scc_map sm(dra->aut);
sm.build_map();
unsigned scc_max = sm.scc_count();
bool dba_realizable = true;
std::vector<bool> realizable(scc_max);
for (unsigned scc = 0; scc < scc_max; ++scc)
{
if (sm.trivial(scc))
{
realizable[scc] = true;
continue;
}
// Get the list of states of that SCC
const std::list<const state*>& sl = sm.states_of(scc);
assert(!sl.empty());
bool scc_realizable = filter_states(dra->aut, dra, sl, final, nonfinal);
dba_realizable &= scc_realizable;
realizable[scc] = scc_realizable;
//std::cerr << "realizable[" << scc << "] = " << scc_realizable << '\n';
}
if (dba)
*dba = dba_realizable;
// for (state_list::const_iterator i = final.begin();
// i != final.end(); ++i)
// std::cerr << dra->aut->get_label(*i) << " is final\n";
// for (state_list::const_iterator i = nonfinal.begin();
// i != nonfinal.end(); ++i)
// std::cerr << dra->aut->get_label(*i) << " is non-final\n";
state_set fs(final.begin(), final.end());
dra_to_ba_worker w(dra, fs, sm, realizable);
w.run();
return scc_filter_states(w.result());
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "public.hh"
namespace spot
{
twa_graph_ptr
dstar_to_tgba(const const_dstar_aut_ptr& daut)
{
switch (daut->type)
{
case spot::Rabin:
return dra_to_ba(daut);
case spot::Streett:
return nsa_to_tgba(daut);
}
SPOT_UNREACHABLE();
}
}
......@@ -46,9 +46,12 @@
std::vector<bdd>::const_iterator cur_guard;
map_t dest_map;
int cur_state;
int plus;
int minus;
unsigned state_count = 0;
unsigned start_state = 0;
unsigned state_count = 0U;
unsigned start_state = 0U;
unsigned accpair_count = 0U;
std::vector<std::string> aps;
bool state_count_seen:1;
......@@ -73,6 +76,7 @@
{
std::string* str;
unsigned int num;
spot::acc_cond::mark_t acc;
}
%code
......@@ -102,6 +106,7 @@
%token <num> NUMBER "number";
%type <num> sign
%type <acc> accsigs state_accsig
%destructor { delete $$; } <str>
%printer {
......@@ -117,9 +122,18 @@ dstar: header ENDOFHEADER eols states
eols : EOL | eols EOL
opt_eols: | opt_eols EOL
auttype: DRA { result.d->type = spot::Rabin; }
| DSA { result.d->type = spot::Streett; }
auttype: DRA
{
result.d->type = spot::Rabin;
result.plus = 1;
result.minus = 0;
}
| DSA
{
result.d->type = spot::Streett;
result.plus = 0;
result.minus = 1;
}
header: auttype opt_eols V2 opt_eols EXPLICIT opt_eols sizes
{
......@@ -168,8 +182,12 @@ sizes:
}
| sizes ACCPAIRS opt_eols NUMBER opt_eols
{
result.d->accpair_count = $4;
result.accpair_count = $4;
result.accpair_count_seen = true;
result.d->aut->set_acceptance(2 * $4,
result.d->type == spot::Rabin ?
spot::acc_cond::acc_code::rabin($4) :
spot::acc_cond::acc_code::streett($4));
}
| sizes STATES opt_eols NUMBER opt_eols
{
......@@ -228,27 +246,30 @@ state_id: STATE opt_eols NUMBER opt_eols opt_name
result.cur_state = $3;
}
sign: '+' { $$ = 0; }
| '-' { $$ = 1; }
sign: '+' { $$ = result.plus; }
| '-' { $$ = result.minus; }
// Membership to a pair is represented as (+NUM,-NUM)
accsigs: opt_eols
{
$$ = 0U;
}
| accsigs sign NUMBER opt_eols
{
if ((unsigned) result.cur_state >= result.state_count)
break;
assert(result.d->accsets);
if ($3 < result.d->accpair_count)
if ($3 < result.accpair_count)
{
result.d->accsets->at(result.cur_state * 2 + $2).set($3);
$$ = $1;
$$.set($3 * 2 + $2);
}
else
{
std::ostringstream o;
if (result.d->accpair_count > 0)
if (result.accpair_count > 0)
{
o << "acceptance pairs should be in the range [0.."
<< result.d->accpair_count - 1<< "]";
<< result.accpair_count - 1 << "]";
}
else
{
......@@ -258,7 +279,7 @@ accsigs: opt_eols
}
}
state_accsig: ACCSIG accsigs
state_accsig: ACCSIG accsigs { $$ = $2; }
transitions:
| transitions NUMBER opt_eols
......@@ -273,9 +294,8 @@ transitions:
states:
| states state_id state_accsig transitions
{
for (map_t::const_iterator i = result.dest_map.begin();
i != result.dest_map.end(); ++i)
result.d->aut->new_edge(result.cur_state, i->first, i->second);
for (auto i: result.dest_map)
result.d->aut->new_edge(result.cur_state, i.first, i.second, $3);
}
%%
......@@ -301,9 +321,6 @@ static void fill_guards(result_& r)
delete[] vars;
r.cur_guard = r.guards.end();
r.d->accsets = spot::make_bitvect_array(r.d->accpair_count,
2 * r.state_count);
}
void
......@@ -331,14 +348,15 @@ namespace spot
result_ r;
r.d = std::make_shared<spot::dstar_aut>();
r.d->aut = make_twa_graph(dict);
r.d->accsets = 0;
r.d->aut->prop_deterministic(true);
r.d->aut->prop_state_based_acc(true);
r.env = &env;
dstaryy::parser parser(error_list, r);
parser.set_debug_level(debug);
parser.parse();
dstaryyclose();
if (!r.d->aut || !r.d->accsets)
if (!r.d->aut)
return nullptr;
return r.d;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement 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 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT