remove algorithms that where only used by dstar's dra2ba conversion
Since we just removed that conversion, those can go as well. Yay! * src/tests/kv.test, src/twa/twamask.cc, src/twa/twamask.hh, src/twa/twaproxy.cc, src/twa/twaproxy.hh, src/twaalgos/scc.cc, src/twaalgos/scc.hh: Delete. * src/twaalgos/Makefile.am, src/twa/Makefile.am, src/tests/Makefile.am, src/tests/ikwiad.cc: adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
9b5340b90a
commit
62f5b9769b
11 changed files with 1 additions and 1181 deletions
|
|
@ -199,7 +199,6 @@ TESTS_twa = \
|
||||||
degendet.test \
|
degendet.test \
|
||||||
degenid.test \
|
degenid.test \
|
||||||
degenlskip.test \
|
degenlskip.test \
|
||||||
kv.test \
|
|
||||||
randomize.test \
|
randomize.test \
|
||||||
lbttparse.test \
|
lbttparse.test \
|
||||||
scc.test \
|
scc.test \
|
||||||
|
|
|
||||||
|
|
@ -53,7 +53,6 @@
|
||||||
#include "twaalgos/stats.hh"
|
#include "twaalgos/stats.hh"
|
||||||
#include "twaalgos/sccinfo.hh"
|
#include "twaalgos/sccinfo.hh"
|
||||||
#include "twaalgos/emptiness_stats.hh"
|
#include "twaalgos/emptiness_stats.hh"
|
||||||
#include "twaalgos/scc.hh"
|
|
||||||
#include "twaalgos/sccinfo.hh"
|
#include "twaalgos/sccinfo.hh"
|
||||||
#include "twaalgos/isdet.hh"
|
#include "twaalgos/isdet.hh"
|
||||||
#include "twaalgos/cycles.hh"
|
#include "twaalgos/cycles.hh"
|
||||||
|
|
@ -268,8 +267,6 @@ syntax(char* prog)
|
||||||
<< "subtransitions)"
|
<< "subtransitions)"
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< " -K dump the graph of SCCs in dot format" << std::endl
|
<< " -K dump the graph of SCCs in dot format" << std::endl
|
||||||
<< " -KV verbosely dump the graph of SCCs in dot format"
|
|
||||||
<< std::endl
|
|
||||||
<< " -KC list cycles in automaton" << std::endl
|
<< " -KC list cycles in automaton" << std::endl
|
||||||
<< " -KW list weak SCCs" << std::endl
|
<< " -KW list weak SCCs" << std::endl
|
||||||
<< " -N output the never clain for Spin (implies -DS)"
|
<< " -N output the never clain for Spin (implies -DS)"
|
||||||
|
|
@ -556,10 +553,6 @@ checked_main(int argc, char** argv)
|
||||||
return 2;
|
return 2;
|
||||||
tm.stop("reading -KP's argument");
|
tm.stop("reading -KP's argument");
|
||||||
}
|
}
|
||||||
else if (!strcmp(argv[formula_index], "-KV"))
|
|
||||||
{
|
|
||||||
output = 11;
|
|
||||||
}
|
|
||||||
else if (!strcmp(argv[formula_index], "-KC"))
|
else if (!strcmp(argv[formula_index], "-KC"))
|
||||||
{
|
{
|
||||||
output = 15;
|
output = 15;
|
||||||
|
|
@ -1485,24 +1478,7 @@ checked_main(int argc, char** argv)
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
case 10:
|
case 10:
|
||||||
{
|
dump_scc_info_dot(std::cout, ensure_digraph(a));
|
||||||
auto aa =
|
|
||||||
std::dynamic_pointer_cast<const spot::twa_graph>(a);
|
|
||||||
if (!aa)
|
|
||||||
dump_scc_dot(a, std::cout, false);
|
|
||||||
else
|
|
||||||
dump_scc_info_dot(std::cout, aa);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
case 11:
|
|
||||||
{
|
|
||||||
//const spot::twa_graph_ptr g =
|
|
||||||
// dynamic_cast<const spot::twa_graph_ptr>(a);
|
|
||||||
//if (!g)
|
|
||||||
dump_scc_dot(a, std::cout, true);
|
|
||||||
//else
|
|
||||||
// dump_scc_info_dot(std::cout, g);
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
case 12:
|
case 12:
|
||||||
stats_reachable(a).dump(std::cout);
|
stats_reachable(a).dump(std::cout);
|
||||||
|
|
|
||||||
|
|
@ -1,55 +0,0 @@
|
||||||
#!/bin/sh
|
|
||||||
# -*- coding: utf-8 -*-
|
|
||||||
# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
|
|
||||||
# Développement de l'EPITA.
|
|
||||||
#
|
|
||||||
# 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/>.
|
|
||||||
|
|
||||||
|
|
||||||
. ./defs
|
|
||||||
|
|
||||||
set -e
|
|
||||||
|
|
||||||
check ()
|
|
||||||
{
|
|
||||||
run 0 ../ikwiad -f -KV "$1" > out.dot
|
|
||||||
test -z "$DOT" || "$DOT" out.dot > /dev/null
|
|
||||||
rm -f out.dot
|
|
||||||
}
|
|
||||||
|
|
||||||
# We don't check the output, but running these might be
|
|
||||||
# enough to trigger assertions in the code, or raise valgrind concerns.
|
|
||||||
|
|
||||||
check 'a R (b R c)'
|
|
||||||
check '(a U b) U (c U d)'
|
|
||||||
check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
|
|
||||||
|
|
||||||
# Make sure escaped variables print OK.
|
|
||||||
check '"G1"U"GG" && "FF"'
|
|
||||||
|
|
||||||
|
|
||||||
# Make sure we count 4 atomic propositions in
|
|
||||||
# G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"
|
|
||||||
# even after iterated simulation
|
|
||||||
# Report from Etienne Renault.
|
|
||||||
|
|
||||||
../ikwiad -KV -R3 -RIS >out \
|
|
||||||
'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'
|
|
||||||
x=`sed -n '/APrec/{
|
|
||||||
s/.*APrec=\[\([^]]*\)\].*/\1/p
|
|
||||||
q
|
|
||||||
}' out | tr ' ' '\n' | wc -l`
|
|
||||||
test "$x" -eq 4
|
|
||||||
|
|
@ -34,8 +34,6 @@ twa_HEADERS = \
|
||||||
taatgba.hh \
|
taatgba.hh \
|
||||||
twa.hh \
|
twa.hh \
|
||||||
twagraph.hh \
|
twagraph.hh \
|
||||||
twamask.hh \
|
|
||||||
twaproxy.hh \
|
|
||||||
twaproduct.hh \
|
twaproduct.hh \
|
||||||
twasafracomplement.hh
|
twasafracomplement.hh
|
||||||
|
|
||||||
|
|
@ -49,6 +47,4 @@ libtwa_la_SOURCES = \
|
||||||
twa.cc \
|
twa.cc \
|
||||||
twagraph.cc \
|
twagraph.cc \
|
||||||
twaproduct.cc \
|
twaproduct.cc \
|
||||||
twamask.cc \
|
|
||||||
twaproxy.cc \
|
|
||||||
twasafracomplement.cc
|
twasafracomplement.cc
|
||||||
|
|
|
||||||
|
|
@ -1,231 +0,0 @@
|
||||||
// -*- 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 "twamask.hh"
|
|
||||||
#include <vector>
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
namespace
|
|
||||||
{
|
|
||||||
struct transition
|
|
||||||
{
|
|
||||||
const state* dest;
|
|
||||||
bdd cond;
|
|
||||||
acc_cond::mark_t acc;
|
|
||||||
};
|
|
||||||
typedef std::vector<transition> transitions;
|
|
||||||
|
|
||||||
struct succ_iter_filtered: public twa_succ_iterator
|
|
||||||
{
|
|
||||||
~succ_iter_filtered()
|
|
||||||
{
|
|
||||||
for (auto& t: trans_)
|
|
||||||
t.dest->destroy();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool first()
|
|
||||||
{
|
|
||||||
it_ = trans_.begin();
|
|
||||||
return it_ != trans_.end();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool next()
|
|
||||||
{
|
|
||||||
++it_;
|
|
||||||
return it_ != trans_.end();
|
|
||||||
}
|
|
||||||
|
|
||||||
bool done() const
|
|
||||||
{
|
|
||||||
return it_ == trans_.end();
|
|
||||||
}
|
|
||||||
|
|
||||||
state* current_state() const
|
|
||||||
{
|
|
||||||
return it_->dest->clone();
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd current_condition() const
|
|
||||||
{
|
|
||||||
return it_->cond;
|
|
||||||
}
|
|
||||||
|
|
||||||
acc_cond::mark_t current_acceptance_conditions() const
|
|
||||||
{
|
|
||||||
return it_->acc;
|
|
||||||
}
|
|
||||||
|
|
||||||
transitions trans_;
|
|
||||||
transitions::const_iterator it_;
|
|
||||||
};
|
|
||||||
|
|
||||||
/// \ingroup twa_on_the_fly_algorithms
|
|
||||||
/// \brief A masked TGBA (abstract).
|
|
||||||
///
|
|
||||||
/// Ignores some states from a TGBA. What state are preserved or
|
|
||||||
/// ignored is controlled by the wanted() method.
|
|
||||||
///
|
|
||||||
/// This is an abstract class. You should inherit from it and
|
|
||||||
/// supply a wanted() method to specify which states to keep.
|
|
||||||
class twa_mask: public twa_proxy
|
|
||||||
{
|
|
||||||
protected:
|
|
||||||
/// \brief Constructor.
|
|
||||||
/// \param masked The automaton to mask
|
|
||||||
/// \param init Any state to use as initial state. This state will be
|
|
||||||
/// destroyed by the destructor.
|
|
||||||
twa_mask(const const_twa_ptr& masked, const state* init = 0):
|
|
||||||
twa_proxy(masked),
|
|
||||||
init_(init)
|
|
||||||
{
|
|
||||||
if (!init)
|
|
||||||
init_ = masked->get_init_state();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
public:
|
|
||||||
virtual ~twa_mask()
|
|
||||||
{
|
|
||||||
init_->destroy();
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual state* get_init_state() const
|
|
||||||
{
|
|
||||||
return init_->clone();
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual twa_succ_iterator*
|
|
||||||
succ_iter(const state* local_state) const
|
|
||||||
{
|
|
||||||
succ_iter_filtered* res;
|
|
||||||
if (iter_cache_)
|
|
||||||
{
|
|
||||||
res = down_cast<succ_iter_filtered*>(iter_cache_);
|
|
||||||
res->trans_.clear();
|
|
||||||
iter_cache_ = nullptr;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
res = new succ_iter_filtered;
|
|
||||||
}
|
|
||||||
for (auto it: original_->succ(local_state))
|
|
||||||
{
|
|
||||||
const spot::state* s = it->current_state();
|
|
||||||
auto acc = it->current_acceptance_conditions();
|
|
||||||
if (!wanted(s, acc))
|
|
||||||
{
|
|
||||||
s->destroy();
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
res->trans_.emplace_back
|
|
||||||
(transition {s, it->current_condition(), acc});
|
|
||||||
}
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual bool wanted(const state* s, acc_cond::mark_t acc) const = 0;
|
|
||||||
|
|
||||||
protected:
|
|
||||||
const state* init_;
|
|
||||||
};
|
|
||||||
|
|
||||||
class twa_mask_keep: public twa_mask
|
|
||||||
{
|
|
||||||
const state_set& mask_;
|
|
||||||
public:
|
|
||||||
twa_mask_keep(const const_twa_ptr& masked,
|
|
||||||
const state_set& mask,
|
|
||||||
const state* init)
|
|
||||||
: twa_mask(masked, init),
|
|
||||||
mask_(mask)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
bool wanted(const state* s, const acc_cond::mark_t) const
|
|
||||||
{
|
|
||||||
state_set::const_iterator i = mask_.find(s);
|
|
||||||
return i != mask_.end();
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
class twa_mask_ignore: public twa_mask
|
|
||||||
{
|
|
||||||
const state_set& mask_;
|
|
||||||
public:
|
|
||||||
twa_mask_ignore(const const_twa_ptr& masked,
|
|
||||||
const state_set& mask,
|
|
||||||
const state* init)
|
|
||||||
: twa_mask(masked, init),
|
|
||||||
mask_(mask)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
bool wanted(const state* s, const acc_cond::mark_t) const
|
|
||||||
{
|
|
||||||
state_set::const_iterator i = mask_.find(s);
|
|
||||||
return i == mask_.end();
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
class twa_mask_acc_ignore: public twa_mask
|
|
||||||
{
|
|
||||||
unsigned mask_;
|
|
||||||
public:
|
|
||||||
twa_mask_acc_ignore(const const_twa_ptr& masked,
|
|
||||||
unsigned mask,
|
|
||||||
const state* init)
|
|
||||||
: twa_mask(masked, init),
|
|
||||||
mask_(mask)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
bool wanted(const state*, const acc_cond::mark_t acc) const
|
|
||||||
{
|
|
||||||
return !acc.has(mask_);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
const_twa_ptr
|
|
||||||
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
|
||||||
const state_set& to_keep,
|
|
||||||
const state* init)
|
|
||||||
{
|
|
||||||
return std::make_shared<twa_mask_keep>(to_mask, to_keep, init);
|
|
||||||
}
|
|
||||||
|
|
||||||
const_twa_ptr
|
|
||||||
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
|
||||||
const state_set& to_ignore,
|
|
||||||
const state* init)
|
|
||||||
{
|
|
||||||
return std::make_shared<twa_mask_ignore>(to_mask, to_ignore, init);
|
|
||||||
}
|
|
||||||
|
|
||||||
const_twa_ptr
|
|
||||||
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
|
||||||
unsigned to_ignore,
|
|
||||||
const state* init)
|
|
||||||
{
|
|
||||||
return std::make_shared<twa_mask_acc_ignore>(to_mask, to_ignore, init);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,66 +0,0 @@
|
||||||
// -*- 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/>.
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
|
|
||||||
#include <bddx.h>
|
|
||||||
#include "twaproxy.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
|
|
||||||
/// \ingroup twa_on_the_fly_algorithms
|
|
||||||
/// \brief Mask a TGBA, keeping a given set of states.
|
|
||||||
///
|
|
||||||
/// Mask the TGBA \a to_mask, keeping only the
|
|
||||||
/// states from \a to_keep. The initial state
|
|
||||||
/// can optionally be reset to \a init.
|
|
||||||
SPOT_API const_twa_ptr
|
|
||||||
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
|
||||||
const state_set& to_keep,
|
|
||||||
const state* init = 0);
|
|
||||||
|
|
||||||
/// \ingroup twa_on_the_fly_algorithms
|
|
||||||
/// \brief Mask a TGBA, rejecting a given set of states.
|
|
||||||
///
|
|
||||||
/// Mask the TGBA \a to_mask, keeping only the states that are not
|
|
||||||
/// in \a to_ignore. The initial state can optionally be reset to
|
|
||||||
/// \a init.
|
|
||||||
SPOT_API const_twa_ptr
|
|
||||||
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
|
||||||
const state_set& to_ignore,
|
|
||||||
const state* init = 0);
|
|
||||||
|
|
||||||
|
|
||||||
/// \ingroup twa_on_the_fly_algorithms
|
|
||||||
/// \brief Mask a TGBA, rejecting some acceptance set of transitions.
|
|
||||||
///
|
|
||||||
/// This will ignore all transitions that have the TO_IGNORE
|
|
||||||
/// acceptance mark. The initial state can optionally be reset to
|
|
||||||
/// \a init.
|
|
||||||
///
|
|
||||||
/// Note that the acceptance condition of the automaton (i.e. the
|
|
||||||
/// set of all acceptance set) is not changed, because so far this
|
|
||||||
/// function is only needed in graph algorithms that do not call
|
|
||||||
/// all_acceptance_conditions().
|
|
||||||
SPOT_API const_twa_ptr
|
|
||||||
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
|
||||||
unsigned to_ignore,
|
|
||||||
const state* init = 0);
|
|
||||||
}
|
|
||||||
|
|
@ -1,75 +0,0 @@
|
||||||
// -*- 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 "twaproxy.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
twa_proxy::twa_proxy(const const_twa_ptr& original)
|
|
||||||
: twa(original->get_dict()), original_(original)
|
|
||||||
{
|
|
||||||
get_dict()->register_all_variables_of(original, this);
|
|
||||||
acc_.add_sets(original->num_sets());
|
|
||||||
}
|
|
||||||
|
|
||||||
twa_proxy::~twa_proxy()
|
|
||||||
{
|
|
||||||
get_dict()->unregister_all_my_variables(this);
|
|
||||||
}
|
|
||||||
|
|
||||||
state* twa_proxy::get_init_state() const
|
|
||||||
{
|
|
||||||
return original_->get_init_state();
|
|
||||||
}
|
|
||||||
|
|
||||||
twa_succ_iterator*
|
|
||||||
twa_proxy::succ_iter(const state* state) const
|
|
||||||
{
|
|
||||||
if (iter_cache_)
|
|
||||||
{
|
|
||||||
original_->release_iter(iter_cache_);
|
|
||||||
iter_cache_ = nullptr;
|
|
||||||
}
|
|
||||||
return original_->succ_iter(state);
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string
|
|
||||||
twa_proxy::format_state(const state* state) const
|
|
||||||
{
|
|
||||||
return original_->format_state(state);
|
|
||||||
}
|
|
||||||
|
|
||||||
std::string
|
|
||||||
twa_proxy::transition_annotation(const twa_succ_iterator* t) const
|
|
||||||
{
|
|
||||||
return original_->transition_annotation(t);
|
|
||||||
}
|
|
||||||
|
|
||||||
state*
|
|
||||||
twa_proxy::project_state(const state* s, const const_twa_ptr& t) const
|
|
||||||
{
|
|
||||||
return original_->project_state(s, t);
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd
|
|
||||||
twa_proxy::compute_support_conditions(const state* state) const
|
|
||||||
{
|
|
||||||
return original_->support_conditions(state);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,59 +0,0 @@
|
||||||
// -*- 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/>.
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
|
|
||||||
#include "twa.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
/// \ingroup twa_on_the_fly_algorithms
|
|
||||||
/// \brief A TGBA proxy.
|
|
||||||
///
|
|
||||||
/// This implements a simple proxy to an existing
|
|
||||||
/// TGBA, forwarding all methods to the original.
|
|
||||||
/// By itself this class is pointless: better use the
|
|
||||||
/// original automaton right away. However it is useful
|
|
||||||
/// to inherit from this class and override some of its
|
|
||||||
/// methods to implement some on-the-fly algorithm.
|
|
||||||
class SPOT_API twa_proxy: public twa
|
|
||||||
{
|
|
||||||
protected:
|
|
||||||
twa_proxy(const const_twa_ptr& original);
|
|
||||||
|
|
||||||
public:
|
|
||||||
virtual ~twa_proxy();
|
|
||||||
|
|
||||||
virtual state* get_init_state() const;
|
|
||||||
|
|
||||||
virtual twa_succ_iterator*
|
|
||||||
succ_iter(const state* state) const;
|
|
||||||
|
|
||||||
virtual std::string format_state(const state* state) const;
|
|
||||||
|
|
||||||
virtual std::string
|
|
||||||
transition_annotation(const twa_succ_iterator* t) const;
|
|
||||||
|
|
||||||
virtual state* project_state(const state* s, const const_twa_ptr& t) const;
|
|
||||||
|
|
||||||
protected:
|
|
||||||
virtual bdd compute_support_conditions(const state* state) const;
|
|
||||||
const_twa_ptr original_;
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -70,7 +70,6 @@ twaalgos_HEADERS = \
|
||||||
safety.hh \
|
safety.hh \
|
||||||
sbacc.hh \
|
sbacc.hh \
|
||||||
sccfilter.hh \
|
sccfilter.hh \
|
||||||
scc.hh \
|
|
||||||
sccinfo.hh \
|
sccinfo.hh \
|
||||||
se05.hh \
|
se05.hh \
|
||||||
sepsets.hh \
|
sepsets.hh \
|
||||||
|
|
@ -127,7 +126,6 @@ libtwaalgos_la_SOURCES = \
|
||||||
relabel.cc \
|
relabel.cc \
|
||||||
safety.cc \
|
safety.cc \
|
||||||
sbacc.cc \
|
sbacc.cc \
|
||||||
scc.cc \
|
|
||||||
sccinfo.cc \
|
sccinfo.cc \
|
||||||
sccfilter.cc \
|
sccfilter.cc \
|
||||||
se05.cc \
|
se05.cc \
|
||||||
|
|
|
||||||
|
|
@ -1,453 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2008, 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire
|
|
||||||
// de Recherche et Développement de l'Epita.
|
|
||||||
//
|
|
||||||
// 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 <queue>
|
|
||||||
#include <set>
|
|
||||||
#include <iostream>
|
|
||||||
#include <sstream>
|
|
||||||
#include "scc.hh"
|
|
||||||
#include "twa/bddprint.hh"
|
|
||||||
#include "misc/escape.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
scc_map::scc_map(const const_twa_ptr& aut)
|
|
||||||
: aut_(aut)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
scc_map::~scc_map()
|
|
||||||
{
|
|
||||||
hash_type::iterator i = h_.begin();
|
|
||||||
|
|
||||||
while (i != h_.end())
|
|
||||||
{
|
|
||||||
// Advance the iterator before deleting the key.
|
|
||||||
const state* s = i->first;
|
|
||||||
++i;
|
|
||||||
s->destroy();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned
|
|
||||||
scc_map::initial() const
|
|
||||||
{
|
|
||||||
state* in = aut_->get_init_state();
|
|
||||||
int val = scc_of_state(in);
|
|
||||||
in->destroy();
|
|
||||||
return val;
|
|
||||||
}
|
|
||||||
|
|
||||||
const scc_map::succ_type&
|
|
||||||
scc_map::succ(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].succ;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool
|
|
||||||
scc_map::trivial(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].trivial;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool
|
|
||||||
scc_map::accepting(unsigned n) const
|
|
||||||
{
|
|
||||||
if (scc_map_[n].trivial)
|
|
||||||
return false;
|
|
||||||
return aut_->acc().accepting(acc_set_of(n));
|
|
||||||
}
|
|
||||||
|
|
||||||
const_twa_ptr
|
|
||||||
scc_map::get_aut() const
|
|
||||||
{
|
|
||||||
return aut_;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
int
|
|
||||||
scc_map::relabel_component()
|
|
||||||
{
|
|
||||||
assert(!root_.front().states.empty());
|
|
||||||
std::list<const state*>::iterator i;
|
|
||||||
int n = scc_map_.size();
|
|
||||||
for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i)
|
|
||||||
{
|
|
||||||
hash_type::iterator spi = h_.find(*i);
|
|
||||||
assert(spi != h_.end());
|
|
||||||
assert(spi->first == *i);
|
|
||||||
assert(spi->second < 0);
|
|
||||||
spi->second = n;
|
|
||||||
}
|
|
||||||
scc_map_.push_back(root_.front());
|
|
||||||
return n;
|
|
||||||
}
|
|
||||||
|
|
||||||
// recursively update supp rec
|
|
||||||
bdd
|
|
||||||
scc_map::update_supp_rec(unsigned state)
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > state);
|
|
||||||
|
|
||||||
bdd& res = scc_map_[state].supp_rec;
|
|
||||||
|
|
||||||
if (res == bddfalse)
|
|
||||||
{
|
|
||||||
const succ_type& s = succ(state);
|
|
||||||
succ_type::const_iterator it;
|
|
||||||
|
|
||||||
res = scc_map_[state].supp;
|
|
||||||
|
|
||||||
for (it = s.begin(); it != s.end(); ++it)
|
|
||||||
res &= update_supp_rec(it->first) & bdd_support(it->second);
|
|
||||||
}
|
|
||||||
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
scc_map::build_map()
|
|
||||||
{
|
|
||||||
// Setup depth-first search from the initial state.
|
|
||||||
{
|
|
||||||
self_loops_ = 0;
|
|
||||||
state* init = aut_->get_init_state();
|
|
||||||
num_ = -1;
|
|
||||||
h_.emplace(init, num_);
|
|
||||||
root_.emplace_front(num_);
|
|
||||||
arc_acc_.push(0U);
|
|
||||||
arc_cond_.push(bddfalse);
|
|
||||||
twa_succ_iterator* iter = aut_->succ_iter(init);
|
|
||||||
iter->first();
|
|
||||||
todo_.emplace(init, iter);
|
|
||||||
}
|
|
||||||
|
|
||||||
while (!todo_.empty())
|
|
||||||
{
|
|
||||||
assert(root_.size() == arc_acc_.size());
|
|
||||||
assert(root_.size() == arc_cond_.size());
|
|
||||||
|
|
||||||
// We are looking at the next successor in SUCC.
|
|
||||||
twa_succ_iterator* succ = todo_.top().second;
|
|
||||||
|
|
||||||
// If there is no more successor, backtrack.
|
|
||||||
if (succ->done())
|
|
||||||
{
|
|
||||||
// We have explored all successors of state CURR.
|
|
||||||
const state* curr = todo_.top().first;
|
|
||||||
|
|
||||||
// Backtrack TODO_.
|
|
||||||
todo_.pop();
|
|
||||||
|
|
||||||
// Fill rem with any component removed, so that
|
|
||||||
// remove_component() does not have to traverse the SCC
|
|
||||||
// again.
|
|
||||||
hash_type::const_iterator spi = h_.find(curr);
|
|
||||||
assert(spi != h_.end());
|
|
||||||
root_.front().states.push_front(spi->first);
|
|
||||||
|
|
||||||
// When backtracking the root of an SCC, we must also
|
|
||||||
// remove that SCC from the ARC/ROOT stacks. We must
|
|
||||||
// discard from H all reachable states from this SCC.
|
|
||||||
assert(!root_.empty());
|
|
||||||
if (root_.front().index == spi->second)
|
|
||||||
{
|
|
||||||
assert(!arc_acc_.empty());
|
|
||||||
assert(arc_cond_.size() == arc_acc_.size());
|
|
||||||
bdd cond = arc_cond_.top();
|
|
||||||
arc_cond_.pop();
|
|
||||||
arc_acc_.pop();
|
|
||||||
int num = relabel_component();
|
|
||||||
root_.pop_front();
|
|
||||||
|
|
||||||
// Record the transition between the SCC being popped
|
|
||||||
// and the previous SCC.
|
|
||||||
if (!root_.empty())
|
|
||||||
root_.front().succ.emplace(num, cond);
|
|
||||||
}
|
|
||||||
|
|
||||||
aut_->release_iter(succ);
|
|
||||||
// Do not destroy CURR: it is a key in H.
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
// We have a successor to look at.
|
|
||||||
// Fetch the values we are interested in...
|
|
||||||
const state* dest = succ->current_state();
|
|
||||||
if (!dest->compare(todo_.top().first))
|
|
||||||
++self_loops_;
|
|
||||||
auto acc = succ->current_acceptance_conditions();
|
|
||||||
bdd cond = succ->current_condition();
|
|
||||||
root_.front().supp &= bdd_support(cond);
|
|
||||||
// ... 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?
|
|
||||||
hash_type::const_iterator spi = h_.find(dest);
|
|
||||||
if (spi == h_.end())
|
|
||||||
{
|
|
||||||
// Yes. Number it, stack it, and register its successors
|
|
||||||
// for later processing.
|
|
||||||
h_.emplace(dest, --num_);
|
|
||||||
root_.emplace_front(num_);
|
|
||||||
arc_acc_.push(acc);
|
|
||||||
arc_cond_.push(cond);
|
|
||||||
twa_succ_iterator* iter = aut_->succ_iter(dest);
|
|
||||||
iter->first();
|
|
||||||
todo_.emplace(dest, iter);
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
// We already know the state.
|
|
||||||
dest->destroy();
|
|
||||||
|
|
||||||
// Have we reached a maximal SCC?
|
|
||||||
if (spi->second >= 0)
|
|
||||||
{
|
|
||||||
int dest = spi->second;
|
|
||||||
// Record that there is a transition from this SCC to the
|
|
||||||
// dest SCC labelled with cond.
|
|
||||||
succ_type::iterator i = root_.front().succ.find(dest);
|
|
||||||
if (i == root_.front().succ.end())
|
|
||||||
root_.front().succ.emplace(dest, cond);
|
|
||||||
else
|
|
||||||
i->second |= cond;
|
|
||||||
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
// Now this is the most interesting case. We have reached a
|
|
||||||
// state S1 which is already part of a non-dead SCC. Any such
|
|
||||||
// non-dead SCC has necessarily been crossed by our path to
|
|
||||||
// this state: there is a state S2 in our path which belongs
|
|
||||||
// to this SCC too. We are going to merge all states between
|
|
||||||
// this S1 and S2 into this SCC.
|
|
||||||
//
|
|
||||||
// This merge is easy to do because the order of the SCC in
|
|
||||||
// ROOT is descending: we just have to merge all SCCs from the
|
|
||||||
// top of ROOT that have an index lesser than the one of
|
|
||||||
// the SCC of S2 (called the "threshold").
|
|
||||||
int threshold = spi->second;
|
|
||||||
std::list<const state*> states;
|
|
||||||
succ_type succs;
|
|
||||||
cond_set conds;
|
|
||||||
conds.insert(cond);
|
|
||||||
bdd supp = bddtrue;
|
|
||||||
std::set<acc_cond::mark_t> used_acc = { acc };
|
|
||||||
while (threshold > root_.front().index)
|
|
||||||
{
|
|
||||||
assert(!root_.empty());
|
|
||||||
assert(!arc_acc_.empty());
|
|
||||||
assert(arc_acc_.size() == arc_cond_.size());
|
|
||||||
acc |= root_.front().acc;
|
|
||||||
auto lacc = arc_acc_.top();
|
|
||||||
acc |= lacc;
|
|
||||||
used_acc.insert(lacc);
|
|
||||||
used_acc.insert(root_.front().useful_acc.begin(),
|
|
||||||
root_.front().useful_acc.end());
|
|
||||||
states.splice(states.end(), root_.front().states);
|
|
||||||
succs.insert(root_.front().succ.begin(),
|
|
||||||
root_.front().succ.end());
|
|
||||||
conds.insert(arc_cond_.top());
|
|
||||||
conds.insert(root_.front().conds.begin(),
|
|
||||||
root_.front().conds.end());
|
|
||||||
supp &= root_.front().supp;
|
|
||||||
root_.pop_front();
|
|
||||||
arc_acc_.pop();
|
|
||||||
arc_cond_.pop();
|
|
||||||
}
|
|
||||||
|
|
||||||
// Note that we do not always have
|
|
||||||
// threshold == root_.front().index
|
|
||||||
// after this loop, the SCC whose index is threshold might have
|
|
||||||
// been merged with a higher SCC.
|
|
||||||
|
|
||||||
// Accumulate all acceptance conditions, states, SCC
|
|
||||||
// successors, and conditions into the merged SCC.
|
|
||||||
root_.front().acc |= acc;
|
|
||||||
root_.front().states.splice(root_.front().states.end(), states);
|
|
||||||
root_.front().succ.insert(succs.begin(), succs.end());
|
|
||||||
root_.front().conds.insert(conds.begin(), conds.end());
|
|
||||||
root_.front().supp &= supp;
|
|
||||||
// This SCC is no longer trivial.
|
|
||||||
root_.front().trivial = false;
|
|
||||||
assert(!used_acc.empty());
|
|
||||||
root_.front().useful_acc.insert(used_acc.begin(), used_acc.end());
|
|
||||||
}
|
|
||||||
|
|
||||||
// recursively update supp_rec
|
|
||||||
(void) update_supp_rec(initial());
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned scc_map::scc_of_state(const state* s) const
|
|
||||||
{
|
|
||||||
hash_type::const_iterator i = h_.find(s);
|
|
||||||
assert(i != h_.end());
|
|
||||||
return i->second;
|
|
||||||
}
|
|
||||||
|
|
||||||
const scc_map::cond_set& scc_map::cond_set_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].conds;
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd scc_map::ap_set_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].supp;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
bdd scc_map::aprec_set_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].supp_rec;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
acc_cond::mark_t scc_map::acc_set_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].acc;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned scc_map::self_loops() const
|
|
||||||
{
|
|
||||||
return self_loops_;
|
|
||||||
}
|
|
||||||
|
|
||||||
const std::list<const state*>& scc_map::states_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].states;
|
|
||||||
}
|
|
||||||
|
|
||||||
const state* scc_map::one_state_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].states.front();
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned scc_map::scc_count() const
|
|
||||||
{
|
|
||||||
return scc_map_.size();
|
|
||||||
}
|
|
||||||
|
|
||||||
const std::set<acc_cond::mark_t>&
|
|
||||||
scc_map::useful_acc_of(unsigned n) const
|
|
||||||
{
|
|
||||||
assert(scc_map_.size() > n);
|
|
||||||
return scc_map_[n].useful_acc;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::ostream&
|
|
||||||
dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose)
|
|
||||||
{
|
|
||||||
out << "digraph G {\n i [label=\"\", style=invis, height=0]" << std::endl;
|
|
||||||
int start = m.initial();
|
|
||||||
out << " i -> " << start << std::endl;
|
|
||||||
|
|
||||||
std::vector<bool> seen(m.scc_count());
|
|
||||||
seen[start] = true;
|
|
||||||
|
|
||||||
std::queue<int> q;
|
|
||||||
q.push(start);
|
|
||||||
while (!q.empty())
|
|
||||||
{
|
|
||||||
int state = q.front();
|
|
||||||
q.pop();
|
|
||||||
|
|
||||||
const scc_map::cond_set& cs = m.cond_set_of(state);
|
|
||||||
|
|
||||||
std::ostringstream ostr;
|
|
||||||
ostr << state;
|
|
||||||
if (verbose)
|
|
||||||
{
|
|
||||||
size_t n = m.states_of(state).size();
|
|
||||||
ostr << " (" << n << " state";
|
|
||||||
if (n > 1)
|
|
||||||
ostr << 's';
|
|
||||||
ostr << ")\\naccs=";
|
|
||||||
escape_str(ostr, m.get_aut()->acc().format(m.acc_set_of(state)));
|
|
||||||
ostr << "\\nconds=[";
|
|
||||||
for (scc_map::cond_set::const_iterator i = cs.begin();
|
|
||||||
i != cs.end(); ++i)
|
|
||||||
{
|
|
||||||
if (i != cs.begin())
|
|
||||||
ostr << ", ";
|
|
||||||
escape_str(ostr,
|
|
||||||
bdd_format_formula(m.get_aut()->get_dict(), *i));
|
|
||||||
}
|
|
||||||
ostr << "]\\n AP=[";
|
|
||||||
escape_str(ostr,
|
|
||||||
bdd_format_sat(m.get_aut()->get_dict(),
|
|
||||||
m.ap_set_of(state)));
|
|
||||||
ostr << "]\\n APrec=[";
|
|
||||||
escape_str(ostr, bdd_format_sat(m.get_aut()->get_dict(),
|
|
||||||
m.aprec_set_of(state)));
|
|
||||||
ostr << "]\\n useful=[";
|
|
||||||
for (auto a: m.useful_acc_of(state))
|
|
||||||
m.get_aut()->acc().format(a);
|
|
||||||
ostr << ']';
|
|
||||||
}
|
|
||||||
|
|
||||||
out << " " << state << " [shape=box,"
|
|
||||||
<< (m.accepting(state) ? "style=bold," : "")
|
|
||||||
<< "label=\"" << ostr.str() << "\"]" << std::endl;
|
|
||||||
|
|
||||||
const scc_map::succ_type& succ = m.succ(state);
|
|
||||||
|
|
||||||
scc_map::succ_type::const_iterator it;
|
|
||||||
for (it = succ.begin(); it != succ.end(); ++it)
|
|
||||||
{
|
|
||||||
int dest = it->first;
|
|
||||||
bdd label = it->second;
|
|
||||||
|
|
||||||
out << " " << state << " -> " << dest
|
|
||||||
<< " [label=\"";
|
|
||||||
escape_str(out, bdd_format_formula(m.get_aut()->get_dict(), label));
|
|
||||||
out << "\"]" << std::endl;
|
|
||||||
|
|
||||||
if (seen[dest])
|
|
||||||
continue;
|
|
||||||
|
|
||||||
seen[dest] = true;
|
|
||||||
q.push(dest);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
out << '}' << std::endl;
|
|
||||||
|
|
||||||
return out;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::ostream&
|
|
||||||
dump_scc_dot(const const_twa_ptr& a, std::ostream& out, bool verbose)
|
|
||||||
{
|
|
||||||
scc_map m(a);
|
|
||||||
m.build_map();
|
|
||||||
return dump_scc_dot(m, out, verbose);
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,210 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
|
|
||||||
// Laboratoire de Recherche et Développement de l'Epita.
|
|
||||||
//
|
|
||||||
// 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/>.
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
|
|
||||||
#include <map>
|
|
||||||
#include <stack>
|
|
||||||
#include <vector>
|
|
||||||
#include "twa/twa.hh"
|
|
||||||
#include <iosfwd>
|
|
||||||
#include "misc/hash.hh"
|
|
||||||
#include "misc/bddlt.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
|
|
||||||
/// Build a map of Strongly Connected components in in a TGBA.
|
|
||||||
class SPOT_API scc_map
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
typedef std::map<unsigned, bdd> succ_type;
|
|
||||||
typedef std::set<bdd, bdd_less_than> cond_set;
|
|
||||||
|
|
||||||
/// \brief Constructor.
|
|
||||||
///
|
|
||||||
/// This will note compute the map initially. You should call
|
|
||||||
/// build_map() to do so.
|
|
||||||
scc_map(const const_twa_ptr& aut);
|
|
||||||
|
|
||||||
~scc_map();
|
|
||||||
|
|
||||||
/// Actually compute the graph of strongly connected components.
|
|
||||||
void build_map();
|
|
||||||
|
|
||||||
/// Get the automaton for which the map has been constructed.
|
|
||||||
const_twa_ptr get_aut() const;
|
|
||||||
|
|
||||||
/// \brief Get the number of SCC in the automaton.
|
|
||||||
///
|
|
||||||
/// SCCs are labelled from 0 to scc_count()-1.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
unsigned scc_count() const;
|
|
||||||
|
|
||||||
/// \brief Get number of the SCC containing the initial state.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
unsigned initial() const;
|
|
||||||
|
|
||||||
/// \brief Successor SCCs of a SCC.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
const succ_type& succ(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return whether an SCC is trivial.
|
|
||||||
///
|
|
||||||
/// Trivial SCCs have one state and no self-loop.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
bool trivial(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return whether an SCC is accepting.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
bool accepting(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of conditions occurring in an SCC.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
const cond_set& cond_set_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of atomic properties occurring on the
|
|
||||||
/// transitions leaving states from SCC \a n.
|
|
||||||
///
|
|
||||||
/// The transitions considered are all transitions inside SCC
|
|
||||||
/// \a n, as well as the transitions leaving SCC \a n.
|
|
||||||
///
|
|
||||||
/// \return a BDD that is a conjuction of all atomic properties
|
|
||||||
/// occurring on the transitions leaving the states of SCC \a n.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
bdd ap_set_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of atomic properties reachable from this SCC.
|
|
||||||
///
|
|
||||||
/// \return a BDD that is a conjuction of all atomic properties
|
|
||||||
/// occurring on the transitions reachable from this SCC n.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
bdd aprec_set_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of acceptance conditions occurring in an SCC.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
acc_cond::mark_t acc_set_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of useful acceptance conditions of SCC \a n.
|
|
||||||
///
|
|
||||||
/// Useless acceptances conditions are always implied by other acceptances
|
|
||||||
/// conditions. This returns all the other acceptance conditions.
|
|
||||||
const std::set<acc_cond::mark_t>& useful_acc_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the set of states of an SCC.
|
|
||||||
///
|
|
||||||
/// The states in the returned list are still owned by the scc_map
|
|
||||||
/// instance. They should NOT be destroyed by the client code.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
const std::list<const state*>& states_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return one state of an SCC.
|
|
||||||
///
|
|
||||||
/// The state in the returned list is still owned by the scc_map
|
|
||||||
/// instance. It should NOT be destroyed by the client code.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
const state* one_state_of(unsigned n) const;
|
|
||||||
|
|
||||||
/// \brief Return the number of the SCC a state belongs too.
|
|
||||||
///
|
|
||||||
/// \pre This should only be called once build_map() has run.
|
|
||||||
unsigned scc_of_state(const state* s) const;
|
|
||||||
|
|
||||||
/// \brief Return the number of self loops in the automaton.
|
|
||||||
unsigned self_loops() const;
|
|
||||||
|
|
||||||
protected:
|
|
||||||
bdd update_supp_rec(unsigned state);
|
|
||||||
int relabel_component();
|
|
||||||
|
|
||||||
struct scc
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
scc(int index) : index(index), acc(0U),
|
|
||||||
supp(bddtrue), supp_rec(bddfalse),
|
|
||||||
trivial(true) {};
|
|
||||||
/// Index of the SCC.
|
|
||||||
int index;
|
|
||||||
/// The union of all acceptance conditions of transitions which
|
|
||||||
/// connect the states of the connected component.
|
|
||||||
acc_cond::mark_t acc;
|
|
||||||
/// States of the component.
|
|
||||||
std::list<const state*> states;
|
|
||||||
/// Set of conditions used in the SCC.
|
|
||||||
cond_set conds;
|
|
||||||
/// Conjunction of atomic propositions used in the SCC.
|
|
||||||
bdd supp;
|
|
||||||
/// Conjunction of atomic propositions used in the SCC.
|
|
||||||
bdd supp_rec;
|
|
||||||
/// Successor SCC.
|
|
||||||
succ_type succ;
|
|
||||||
/// Trivial SCC have one state and no self-loops.
|
|
||||||
bool trivial;
|
|
||||||
/// \brief Set of acceptance combinations used in the SCC.
|
|
||||||
std::set<acc_cond::mark_t> useful_acc;
|
|
||||||
};
|
|
||||||
|
|
||||||
const_twa_ptr aut_; // Automata to decompose.
|
|
||||||
typedef std::list<scc> stack_type;
|
|
||||||
stack_type root_; // Stack of SCC roots.
|
|
||||||
std::stack<acc_cond::mark_t> arc_acc_; // A stack of acceptance conditions
|
|
||||||
// between each of these SCC.
|
|
||||||
std::stack<bdd> arc_cond_; // A stack of conditions
|
|
||||||
// between each of these SCC.
|
|
||||||
typedef std::unordered_map<const state*, int,
|
|
||||||
state_ptr_hash, state_ptr_equal> hash_type;
|
|
||||||
hash_type h_; // Map of visited states. Values >= 0
|
|
||||||
// designate maximal SCC. Values < 0
|
|
||||||
// number states that are part of
|
|
||||||
// incomplete SCCs being completed.
|
|
||||||
int num_; // Number of visited nodes, negated.
|
|
||||||
typedef std::pair<const spot::state*, twa_succ_iterator*> pair_state_iter;
|
|
||||||
std::stack<pair_state_iter> todo_; // DFS stack. Holds (STATE,
|
|
||||||
// ITERATOR) pairs where
|
|
||||||
// ITERATOR is an iterator over
|
|
||||||
// the successors of STATE.
|
|
||||||
// ITERATOR should always be
|
|
||||||
// freed when TODO is popped,
|
|
||||||
// but STATE should not because
|
|
||||||
// it is used as a key in H.
|
|
||||||
|
|
||||||
typedef std::vector<scc> scc_map_type;
|
|
||||||
scc_map_type scc_map_; // Map of constructed maximal SCC.
|
|
||||||
// SCC number "n" in H_ corresponds to entry
|
|
||||||
// "n" in SCC_MAP_.
|
|
||||||
unsigned self_loops_; // Self loops count.
|
|
||||||
};
|
|
||||||
|
|
||||||
SPOT_API std::ostream&
|
|
||||||
dump_scc_dot(const const_twa_ptr& a,
|
|
||||||
std::ostream& out, bool verbose = false);
|
|
||||||
SPOT_API std::ostream&
|
|
||||||
dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose = false);
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue