Commit 1513a9d9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Merge branch 'master' into next

parents 918548a0 cf1550c3
Pipeline #20441 passed with stages
in 259 minutes and 52 seconds
New in spot 2.9.0.dev (not yet released)
Command-line tools:
- 'ltl2tgba -G -D' is now better at handling formulas that use
'<->' and 'xor' operators at the top level. For instance
ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
now produces a 16-state automaton (instead of 31 in Spot 2.9).
- Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
It can now take three values:
0: never attempt this optimization,
1: always try to determinize and minimize automata as WDBA,
and check (if needed) that the result is correct,
2: determinize and minimize automata as WDBA only if it is known
beforehand (by cheap syntactic means) that the result will be
correct (e.g., the input formula is a syntactic obligation).
The default is 1 in "--high" mode, 2 in "--medium" mode or in
"--deterministic --low" mode, and 0 in other "--low" modes.
- ltlsynt learned --algo=ps to use the default conversion to
deterministic parity automata (the same as ltl2tgba -DP'max odd').
- ltlsynt now has a -x option to fine-tune the translation. See the
spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
New in spot 2.9.1.dev (not yet released)
Library:
......@@ -62,8 +37,37 @@ New in spot 2.9.0.dev (not yet released)
file. With this refactoring, we can retrieve both a kripke or a
kripkecube from a PINS file.
New in spot 2.9.1 (2020-07-15)
Command-line tools:
- 'ltl2tgba -G -D' is now better at handling formulas that use
'<->' and 'xor' operators at the top level. For instance
ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
now produces a 16-state automaton (instead of 31 in Spot 2.9).
- Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
It can now take three values:
0: never attempt this optimization,
1: always try to determinize and minimize automata as WDBA,
and check (if needed) that the result is correct,
2: determinize and minimize automata as WDBA only if it is known
beforehand (by cheap syntactic means) that the result will be
correct (e.g., the input formula is a syntactic obligation).
The default is 1 in "--high" mode, 2 in "--medium" mode or in
"--deterministic --low" mode, and 0 in other "--low" modes.
- ltlsynt learned --algo=ps to use the default conversion to
deterministic parity automata (the same as ltl2tgba -DP'max odd').
- ltlsynt now has a -x option to fine-tune the translation. See the
spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
Library:
- product_xor() and product_xnor() are two new versions of the
synchronized product. The only work with operands that are
synchronized product. They only work with operands that are
deterministic automata, and build automata whose language are
respectively the symmetric difference of the operands, and the
complement of that.
......@@ -101,6 +105,14 @@ New in spot 2.9.0.dev (not yet released)
issues in intersecting_run(), exclusive_run(),
intersecting_word(), exclusive_word(), which all call reduce().
- ltlcross used to crash with "Too many acceptance sets used. The
limit is 32." when complementing an automaton would require more
acceptance sets than supported by Spot. This is now diagnosed
with --verbose, but does not prevent ltlcross from continuing.
- scc_info::edges_of() and scc_info::inner_edges_of() now correctly
honor any filter passed to scc_info.
New in spot 2.9 (2020-04-30)
Command-line tools:
......
......@@ -1336,25 +1336,37 @@ namespace
&& !spot::is_universal(from[i]))
missing_complement = true;
else
to[i] = spot::complement(from[i], aborter);
if (verbose)
{
if (to[i])
{
std::cerr << "\t(";
printsize(from[i]);
std::cerr << ") -> (";
printsize(to[i]);
std::cerr << ")\tComp(" << prefix << i << ")\n";
}
else
{
std::cerr << "\tnot complemented";
if (aborter)
aborter->print_reason(std::cerr << " (") << ')';
std::cerr << '\n';
}
}
try
{
to[i] = spot::complement(from[i], aborter);
if (verbose)
{
if (to[i])
{
std::cerr << "\t(";
printsize(from[i]);
std::cerr << ") -> (";
printsize(to[i]);
std::cerr << ")\tComp(" << prefix
<< i << ")\n";
}
else
{
std::cerr << "\tnot complemented";
if (aborter)
aborter->print_reason(std::cerr
<< " (") << ')';
std::cerr << '\n';
}
}
}
catch (const std::runtime_error& re)
{
missing_complement = true;
if (verbose)
std::cerr << "\tnot complemented ("
<< re.what() << ")\n";
}
}
};
missing_complement = false;
......
......@@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.63])
AC_INIT([spot], [2.9.0.dev], [spot@lrde.epita.fr])
AC_INIT([spot], [2.9.1.dev], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
......
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
#+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html
#+MACRO: SPOTVERSION 2.9
#+MACRO: LASTRELEASE 2.9
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz][=spot-2.9.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9/NEWS][summary of the changes]]
#+MACRO: SPOTVERSION 2.9.1
#+MACRO: LASTRELEASE 2.9.1
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz][=spot-2.9.1.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-1/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2020-04-30
#+ATTR_HTML: :id spotlogo
......
......@@ -38,22 +38,6 @@ namespace spot
{
namespace
{
using EdgeMask = std::vector<bool>;
template< typename Edges, typename Apply >
void for_each_edge(const const_twa_graph_ptr& aut,
const Edges& edges,
const EdgeMask& mask,
Apply apply)
{
for (const auto& e: edges)
{
unsigned edge_id = aut->edge_number(e);
if (mask[edge_id])
apply(edge_id);
}
}
// Transforms automaton from transition based acceptance to state based
// acceptance.
void make_state_acc(twa_graph_ptr & aut)
......@@ -87,7 +71,6 @@ namespace spot
bool is_scc_tba_type(const_twa_graph_ptr aut,
const scc_info& si,
const unsigned scc,
const std::vector<bool>& keep,
const rs_pairs_view& aut_pairs,
std::vector<bool>& final)
{
......@@ -101,10 +84,8 @@ namespace spot
auto aut_fin_alone = aut_pairs.fins_alone();
if ((scc_acc & aut_fin_alone) != aut_fin_alone)
{
for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e)
{
final[e] = true;
});
for (auto& e: si.edges_of(scc))
final[aut->edge_number(e)] = true;
return true;
}
......@@ -126,14 +107,14 @@ namespace spot
// final. Otherwise we do not know: it is possible that there is
// a non-accepting cycle in the SCC that does not visit Fᵢ.
std::set<unsigned> unknown;
for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e)
for (auto& ed: si.inner_edges_of(scc))
{
const auto& ed = aut->edge_data(e);
unsigned e = aut->edge_number(ed);
if (ed.acc & scc_infs_alone)
final[e] = true;
final[e] = true;
else
unknown.insert(e);
});
unknown.insert(e);
}
// Erase edges that cannot belong to a cycle, i.e., the edges
// whose 'dst' is not 'src' of any unknown edges.
......@@ -182,13 +163,11 @@ namespace spot
for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc)
{
for_each_edge(aut, si.edges_of(uscc), keep, [&](unsigned e)
{
unknown.erase(e);
});
for (auto& e: si.edges_of(uscc))
unknown.erase(aut->edge_number(e));
if (si.is_rejecting_scc(uscc))
continue;
if (!is_scc_tba_type(aut, si, uscc, keep, aut_pairs, final))
if (!is_scc_tba_type(aut, si, uscc, aut_pairs, final))
return false;
}
}
......@@ -229,10 +208,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> scc_is_tba_type(si.scc_count(), false);
std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep,
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc,
aut_pairs, final);
auto res = make_twa_graph(aut->get_dict());
......@@ -804,10 +782,9 @@ namespace spot
// if is TBA type
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return false;
return true;
......@@ -827,10 +804,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return nullptr;
auto res = make_twa_graph(aut, twa::prop_set::all());
......
......@@ -27,6 +27,38 @@ namespace spot
{
class scc_info;
/// @{
/// \ingroup twa_misc
/// \brief An edge_filter may be called on each edge to decide what
/// to do with it.
///
/// The edge filter is called with an edge and a destination. (In
/// existential automata the destination is already given by the
/// edge, but in alternating automata, one edge may have several
/// destinations, and in this case the filter will be called for
/// each destination.) The filter should return a value from
/// edge_filter_choice.
///
/// \c keep means to use the edge normally, as if no filter had
/// been given. \c ignore means to pretend the edge does not
/// exist (if the destination is only reachable through this edge,
/// it will not be visited). \c cut also ignores the edge, but
/// it remembers to visit the destination state (as if it were an
/// initial state) in case it is not reachable otherwise.
///
/// Note that successors between SCCs can only be maintained for
/// edges that are kept. If some edges are ignored or cut, the
/// SCC graph that you can explore with scc_info::initial() and
/// scc_info::succ() will be restricted to the portion reachable
/// with "keep" edges. Additionally SCCs might be created when
/// edges are cut, but those will not be reachable from
/// scc_info::initial()..
enum class edge_filter_choice { keep, ignore, cut };
typedef edge_filter_choice
(*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
void* filter_data);
/// @}
namespace internal
{
struct keep_all
......@@ -100,6 +132,9 @@ namespace spot
dv_t* dv_;
Filter filt_;
edge_filter efilter_;
void* efilter_data_;
void inc_state_maybe_()
{
......@@ -113,21 +148,49 @@ namespace spot
inc_state_maybe_();
}
// Do we ignore the current transition?
bool ignore_current()
{
unsigned dst = (*this)->dst;
if ((int)dst >= 0)
// Non-universal branching => a single destination.
return !filt_(&(*this)->dst, 1 + &(*this)->dst);
// Universal branching => multiple destinations.
const unsigned* d = dv_->data() + ~dst;
return !filt_(d + 1, d + *d + 1);
{
// Non-universal branching => a single destination.
if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
return true;
if (efilter_)
return efilter_((*tv_)[t_], dst, efilter_data_)
!= edge_filter_choice::keep;
return false;
}
else
{
// Universal branching => multiple destinations.
const unsigned* d = dv_->data() + ~dst;
if (!filt_(d + 1, d + *d + 1))
return true;
if (efilter_)
{
// Keep the transition if at least one destination
// is not filtered.
const unsigned* end = d + *d + 1;
for (const unsigned* i = d + 1; i != end; ++i)
{
if (efilter_((*tv_)[t_], *i, efilter_data_)
== edge_filter_choice::keep)
return false;
return true;
}
}
return false;
}
}
public:
scc_edge_iterator(state_iterator begin, state_iterator end,
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
: pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
edge_filter efilter, void* efilter_data) noexcept
: pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
efilter_(efilter), efilter_data_(efilter_data)
{
if (pos_ == end_)
return;
......@@ -191,22 +254,26 @@ namespace spot
sv_t* sv_;
dv_t* dv_;
Filter filt_;
edge_filter efilter_;
void* efilter_data_;
public:
scc_edges(state_iterator begin, state_iterator end,
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
: begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
edge_filter efilter, void* efilter_data) noexcept
: begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
efilter_(efilter), efilter_data_(efilter_data)
{
}
iter_t begin() const
{
return {begin_, end_, tv_, sv_, dv_, filt_};
return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
}
iter_t end() const
{
return {end_, end_, nullptr, nullptr, nullptr, filt_};
return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr};
}
};
}
......@@ -378,36 +445,10 @@ namespace spot
// support that yet.
typedef scc_info_node scc_node;
typedef scc_info_node::scc_succs scc_succs;
/// @{
/// \brief An edge_filter may be called on each edge to decide what
/// to do with it.
///
/// The edge filter is called with an edge and a destination. (In
/// existential automata the destination is already given by the
/// edge, but in alternating automata, one edge may have several
/// destinations, and in this case the filter will be called for
/// each destination.) The filter should return a value from
/// edge_filter_choice.
///
/// \c keep means to use the edge normally, as if no filter had
/// been given. \c ignore means to pretend the edge does not
/// exist (if the destination is only reachable through this edge,
/// it will not be visited). \c cut also ignores the edge, but
/// it remembers to visit the destination state (as if it were an
/// initial state) in case it is not reachable otherwise.
///
/// Note that successors between SCCs can only be maintained for
/// edges that are kept. If some edges are ignored or cut, the
/// SCC graph that you can explore with scc_info::initial() and
/// scc_info::succ() will be restricted to the portion reachable
/// with "keep" edges. Additionally SCCs might be created when
/// edges are cut, but those will not be reachable from
/// scc_info::initial()..
enum class edge_filter_choice { keep, ignore, cut };
typedef edge_filter_choice
(*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
void* filter_data);
/// @}
// These types used to be defined here in Spot up to 2.9.
typedef spot::edge_filter_choice edge_filter_choice;
typedef spot::edge_filter edge_filter;
protected:
......@@ -559,7 +600,7 @@ namespace spot
return {states.begin(), states.end(),
&aut_->edge_vector(), &aut_->states(),
&aut_->get_graph().dests_vector(),
internal::keep_all()};
internal::keep_all(), filter_, const_cast<void*>(filter_data_)};
}
/// \brief A fake container to iterate over all edges between
......@@ -576,7 +617,8 @@ namespace spot
return {states.begin(), states.end(),
&aut_->edge_vector(), &aut_->states(),
&aut_->get_graph().dests_vector(),
internal::keep_inner_scc(sccof_, scc)};
internal::keep_inner_scc(sccof_, scc), filter_,
const_cast<void*>(filter_data_)};
}
unsigned one_state_of(unsigned scc) const
......
......@@ -320,6 +320,7 @@ TESTS_twa = \
core/ltlcross.test \
core/spotlbtt2.test \
core/ltlcross2.test \
core/ltlcross6.test \
core/autcross.test \
core/autcross2.test \
core/autcross3.test \
......
This diff is collapsed.
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement
# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -79,7 +79,7 @@ SCC#1
succs: 0
SCC#2
states: 2
edges: 2->2
edges:
succs: 0 1
EOF
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment