Commit 0de5f50d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

twa: add support for prop_complete()

* spot/twa/twa.hh: Add support.  Make two constructors for prop_set in
order to diagnose constructions with 5 arguments.
* spot/parseaut/parseaut.yy: Adjust diagnostics for complete and
deterministic.
* spot/tl/exclusive.cc, spot/twa/twagraph.cc,
spot/twaalgos/alternation.cc, spot/twaalgos/complete.cc,
spot/twaalgos/complete.hh, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isdet.cc, spot/twaalgos/mask.cc,
spot/twaalgos/minimize.cc, spot/twaalgos/product.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/remprop.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/totgba.cc,
tests/core/parseaut.test, tests/python/product.ipynb: Adjust.
* NEWS, doc/org/concepts.org, doc/org/hoa.org,
doc/org/tut21.org: Document it.
parent 90a8a912
......@@ -10,6 +10,9 @@ New in spot 2.3.2.dev (not yet released)
- spot::sum() and spot::sum_and() implements the union and the
intersection of two automatons, respectively.
- twa objects have a new property: prop_complete(). This obviously
acts as a cache for the is_complete() function.
Bug fixes:
- In "lenient" mode the parser would fail to recover from
......
......@@ -1056,11 +1056,12 @@ automaton, and that can be queried or set by algorithms:
| flag name | meaning when =true= |
|----------------------+----------------------------------------------------------------------------------------------|
| =state_acc= | automaton should be considered has having state-based acceptance |
| =state_acc= | automaton should be considered as having state-based acceptance |
| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC |
| =weak= | transitions of an SCC all belong to the same acceptance sets |
| =very-weak= | weak automaton where all SCCs have size 1 |
| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs |
| =complete= | it is always possible to move the automaton forward, using any letter |
| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it |
| =semi-deterministic= | any nondeterminism occurs before entering an accepting SCC |
| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) |
......
......@@ -661,7 +661,7 @@ particular:
| =no-univ-branch= | ignored | no | only if =-Hv= | |
| =univ-branch= | checked | no | checked | |
| =deterministic= | checked | yes | checked | |
| =complete= | checked | no | checked | |
| =complete= | checked | yes | checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= |
| =semi-deterministic= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=semi-deterministic= |
| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= |
......
......@@ -131,6 +131,7 @@ corresponding BDD variable number, and then use for instance
// would set the deterministic property on its output. In this
// example, the properties that are set come from the "properties:"
// line of the input file.
out << "Complete: " << aut->prop_complete() << '\n';
out << "Deterministic: " << aut->prop_deterministic() << '\n';
out << "Unambiguous: " << aut->prop_unambiguous() << '\n';
out << "State-Based Acc: " << aut->prop_state_acc() << '\n';
......@@ -169,6 +170,7 @@ Number of edges: 10
Initial state: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: Fa | G(Fb & Fc)
Complete: no
Deterministic: no
Unambiguous: yes
State-Based Acc: maybe
......
......@@ -146,7 +146,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
bool aliased_states = false;
spot::trival deterministic = spot::trival::maybe();
bool complete = false;
spot::trival complete = spot::trival::maybe();
bool trans_acc_seen = false;
std::map<std::string, spot::location> labels;
......@@ -471,14 +471,15 @@ header: format-version header-items
error(det.loc,
"deterministic automata should have at most "
"one initial state");
res.deterministic = spot::trival::maybe();
}
res.deterministic = false;
}
else
{
// Assume the automaton is deterministic until proven
// wrong, or unless we are building a Kripke structure.
res.deterministic = !res.opts.want_kripke;
if (!res.opts.want_kripke)
res.deterministic = true;
}
auto complete = res.prop_is_true("complete");
if (ss < 1)
......@@ -495,7 +496,8 @@ header: format-version header-items
{
// Assume the automaton is complete until proven
// wrong.
res.complete = !res.opts.want_kripke;
if (!res.opts.want_kripke)
res.complete = true;
}
// if ap_count == 0, then a Kripke structure could be
// declared complete, although that probably doesn't
......@@ -1034,6 +1036,7 @@ body: states
// mention it in the next loop.
if (s < res.info_states.size())
res.info_states[s].declared = true;
res.complete = spot::trival::maybe();
}
unsigned n = res.info_states.size();
// States with number above res.states have already caused a
......@@ -1043,10 +1046,34 @@ body: states
for (unsigned i = 0; i < n; ++i)
{
auto& p = res.info_states[i];
if (p.used && !p.declared)
error(p.used_loc,
"state " + std::to_string(i) + " has no definition");
if (!p.declared)
{
if (p.used)
error(p.used_loc,
"state " + std::to_string(i) + " has no definition");
if (!p.used && res.complete)
if (auto p = res.prop_is_true("complete"))
{
error(res.states_loc,
"state " + std::to_string(i) +
" has no definition...");
error(p.loc, "... despite 'properties: complete'");
}
res.complete = false;
}
}
if (res.complete)
if (auto p = res.prop_is_false("complete"))
{
error(@1, "automaton is complete...");
error(p.loc, "... despite 'properties: !complete'");
}
if (res.deterministic)
if (auto p = res.prop_is_false("deterministic"))
{
error(@1, "automaton is deterministic...");
error(p.loc, "... despite 'properties: !deterministic'");
}
}
state-num: INT
......@@ -1104,7 +1131,7 @@ checked-state-num: state-num
states: | states state
{
if ((res.deterministic || res.complete) && !res.opts.want_kripke)
if ((res.deterministic.is_true() || res.complete.is_true()))
{
bdd available = bddtrue;
bool det = true;
......@@ -1114,7 +1141,7 @@ states: | states state
det = false;
available -= t.cond;
}
if (res.deterministic && !det)
if (res.deterministic.is_true() && !det)
{
res.deterministic = false;
if (auto p = res.prop_is_true("deterministic"))
......@@ -1124,7 +1151,7 @@ states: | states state
"... despite 'properties: deterministic'");
}
}
if (res.complete && available != bddfalse)
if (res.complete.is_true() && available != bddfalse)
{
res.complete = false;
if (auto p = res.prop_is_true("complete"))
......@@ -1165,7 +1192,7 @@ state: state-name labeled-edges
// Assume the worse. This skips the tests about determinism
// we might perform on the state.
res.deterministic = spot::trival::maybe();
res.complete = false;
res.complete = spot::trival::maybe();
}
......@@ -1177,6 +1204,11 @@ state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
std::ostringstream o;
o << "redeclaration of state " << $3;
error(@1 + @3, o.str());
// The additional transitions from extra states might
// led us to believe that the automaton is complete
// while it is not if we ignore them.
if (res.complete.is_true())
res.complete = spot::trival::maybe();
}
res.info_states[$3].declared = true;
res.acc_state = $5;
......@@ -1499,7 +1531,7 @@ dstar_header: dstar_sizes
}
res.acc_style = State_Acc;
res.deterministic = true;
// res.h->aut->prop_complete();
res.complete = true;
fill_guards(res);
res.cur_guard = res.guards.end();
}
......@@ -2230,6 +2262,10 @@ static void fix_initial_state(result_& r)
"a single initial state");
return;
}
// Fiddling with initial state may turn an incomplete automaton
// into a complete one.
if (r.complete.is_false())
r.complete = spot::trival::maybe();
// Multiple initial states. We might need to add a fake one,
// unless one of the actual initial state has no incoming edge.
auto& aut = r.h->aut;
......@@ -2299,7 +2335,9 @@ static void fix_initial_state(result_& r)
static void fix_properties(result_& r)
{
r.aut_or_ks->prop_deterministic(r.deterministic);
//r.aut_or_ks->prop_complete(r.complete);
// std::cerr << "fix det: " << r.deterministic << '\n';
// std::cerr << "fix complete: " << r.complete << '\n';
r.aut_or_ks->prop_complete(r.complete);
if (r.acc_style == State_Acc ||
(r.acc_style == Mixed_Acc && !r.trans_acc_seen))
r.aut_or_ks->prop_state_acc(true);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -177,7 +177,7 @@ namespace spot
twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
res->prop_copy(aut, { true, true, false, true, true });
res->prop_copy(aut, { true, true, false, true, false, true });
res->copy_acceptance_of(aut);
if (simplify_guards)
{
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// Copyright (C) 2009, 2011, 2013-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -992,6 +992,7 @@ namespace spot
trival::repr_t stutter_invariant:2; // Stutter invariant language.
trival::repr_t very_weak:2; // very-weak, or 1-weak
trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
trival::repr_t complete:2; // Complete automaton.
};
union
{
......@@ -1267,6 +1268,29 @@ namespace spot
}
/// \brief Whether the automaton is complete..
///
/// An automaton is complete if for each state the union of the
/// labels of its outgoing transitions is always true.
///
/// Note that this method may return trival::maybe() when it is
/// unknown whether the automaton is complete or not. If you
/// need a true/false answer, prefer the is_complete() function.
///
/// \see prop_complete()
/// \see is_complete()
trival prop_complete() const
{
return is.complete;
}
/// \brief Set the complete property.
///
/// \see is_complete()
void prop_complete(trival val)
{
is.complete = val.val();
}
/// \brief Whether the automaton is deterministic.
///
......@@ -1404,7 +1428,7 @@ namespace spot
///
/// This can be used for instance as:
/// \code
/// aut->prop_copy(other_aut, {true, false, false, false, true});
/// aut->prop_copy(other_aut, {true, false, false, false, false, true});
/// \endcode
/// This would copy the "state-based acceptance" and
/// "stutter invariant" properties from \c other_aut to \c code.
......@@ -1428,8 +1452,52 @@ namespace spot
bool inherently_weak; ///< preserve inherently weak, weak, & terminal
bool deterministic; ///< preserve deterministic, semi-det, unambiguous
bool improve_det; ///< improves deterministic, semi-det, unambiguous
bool complete; ///< preserves completeness
bool stutter_inv; ///< preserve stutter invariance
prop_set()
: state_based(false),
inherently_weak(false),
deterministic(false),
improve_det(false),
complete(false),
stutter_inv(false)
{
}
prop_set(bool state_based,
bool inherently_weak,
bool deterministic,
bool improve_det,
bool complete,
bool stutter_inv)
: state_based(state_based),
inherently_weak(inherently_weak),
deterministic(deterministic),
improve_det(improve_det),
complete(complete),
stutter_inv(stutter_inv)
{
}
#ifndef SWIG
// The "complete" argument was added in Spot 2.4
SPOT_DEPRECATED("prop_set() now takes 6 arguments")
prop_set(bool state_based,
bool inherently_weak,
bool deterministic,
bool improve_det,
bool stutter_inv)
: state_based(state_based),
inherently_weak(inherently_weak),
deterministic(deterministic),
improve_det(improve_det),
complete(false),
stutter_inv(stutter_inv)
{
}
#endif
/// \brief An all-true \c prop_set
///
/// Use that only in algorithms that copy an automaton without
......@@ -1439,7 +1507,7 @@ namespace spot
/// properties currently implemented, use an explicit
///
/// \code
/// {true, true, true, true, true}
/// {true, true, true, true, true, true}
/// \endcode
///
/// instead of calling \c all(). This way, the day a new
......@@ -1447,7 +1515,7 @@ namespace spot
/// algorithm X, in case that new property is not preserved.
static prop_set all()
{
return { true, true, true, true, true };
return { true, true, true, true, true, true };
}
};
......@@ -1492,6 +1560,8 @@ namespace spot
prop_unambiguous(true);
}
}
if (p.complete)
prop_complete(other->prop_complete());
if (p.stutter_inv)
prop_stutter_invariant(other->prop_stutter_invariant());
}
......@@ -1521,6 +1591,8 @@ namespace spot
if (!(p.improve_det && prop_unambiguous().is_true()))
prop_unambiguous(trival::maybe());
}
if (!p.complete)
prop_complete(trival::maybe());
if (!p.stutter_inv)
prop_stutter_invariant(trival::maybe());
}
......
......@@ -233,6 +233,14 @@ namespace spot
v = current++;
if (current == todo.size())
return; // No unreachable state.
// Removing some non-deterministic dead state could make the
// automaton deterministic.
if (prop_deterministic().is_false())
prop_deterministic(trival::maybe());
if (prop_complete().is_false())
prop_complete(trival::maybe());
defrag_states(std::move(todo), current);
}
......@@ -393,6 +401,14 @@ namespace spot
useful[s] = -1U;
if (current == num_states)
return; // No useless state.
// Removing some non-deterministic dead state could make the
// automaton deterministic. Likewise for non-complete.
if (prop_deterministic().is_false())
prop_deterministic(trival::maybe());
if (prop_complete().is_false())
prop_complete(trival::maybe());
defrag_states(std::move(useful), current);
}
......
......@@ -362,7 +362,7 @@ namespace spot
res->copy_ap_of(aut_);
// We preserve deterministic-like properties, and
// stutter-invariance.
res->prop_copy(aut_, {false, false, false, true, true});
res->prop_copy(aut_, {false, false, false, true, true, true});
res->set_generalized_buchi(has_reject_more_ + reject_1_count_);
// We for easier computation of outgoing sets, we will
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
......@@ -21,10 +21,12 @@
namespace spot
{
unsigned complete_here(twa_graph_ptr aut)
void complete_here(twa_graph_ptr aut)
{
unsigned n = aut->num_states();
unsigned sink = -1U;
if (aut->prop_complete().is_true())
return;
unsigned n = aut->num_states();
// UM is a pair (bool, mark). If the Boolean is false, the
// acceptance is always satisfiable. Otherwise, MARK is an
......@@ -126,24 +128,17 @@ namespace spot
}
}
aut->prop_complete(true);
// Get rid of any named property if the automaton changed.
if (t < aut->num_edges())
aut->release_named_properties();
else
assert(t == aut->num_edges());
return sink;
}
twa_graph_ptr complete(const const_twa_ptr& aut)
{
auto res = make_twa_graph(aut, {
true, // state based
true, // inherently_weak
true, // deterministic
true, // improve det
true, // stutter inv.
});
auto res = make_twa_graph(aut, twa::prop_set::all());
complete_here(res);
return res;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -25,12 +25,9 @@ namespace spot
{
/// \brief Complete a twa_graph in place.
///
/// If the TωA has no acceptance set, one will be added. The
/// returned value is the number of the sink state (it can be a new
/// state added for completion, or an existing non-accepting state
/// that has been reused as sink state because it had no outgoing
/// transitions apart from self-loops.)
SPOT_API unsigned complete_here(twa_graph_ptr aut);
/// If the TωA has an acceptance condition that is a tautology,
/// it will be changed into a Büchi automaton.
SPOT_API void complete_here(twa_graph_ptr aut);
/// \brief Clone a twa and complete it.
///
......
......@@ -212,7 +212,7 @@ namespace spot
if (want_sba)
res->prop_state_acc(true);
// Preserve determinism, weakness, and stutter-invariance
res->prop_copy(a, { false, true, true, true, true });
res->prop_copy(a, { false, true, true, true, true, true });
// Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can
......
......@@ -641,6 +641,7 @@ namespace spot
{ false, // state based
false, // inherently_weak
false, false, // deterministic
true, // complete
true // stutter inv
});
......
......@@ -160,8 +160,11 @@ namespace spot
is_colored = colored && (!has_state_acc || nodeadend);
// If the automaton declares that it is deterministic or
// state-based, make sure that it really is.
assert(deterministic || aut->prop_deterministic() != true);
assert(state_acc || aut->prop_state_acc() != true);
assert(!aut->prop_deterministic().is_known() ||
deterministic == aut->prop_deterministic().is_true());
assert(!aut->prop_complete().is_known() ||
complete == aut->prop_complete().is_true());
assert(state_acc || !aut->prop_state_acc().is_true());
}
void number_all_ap(const const_twa_graph_ptr& aut)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -134,6 +134,9 @@ namespace spot
bool
is_complete(const const_twa_graph_ptr& aut)
{
trival cp = aut->prop_complete();
if (cp.is_known())
return cp.is_true();
unsigned ns = aut->num_states();
for (unsigned src = 0; src < ns; ++src)
{
......@@ -141,11 +144,16 @@ namespace spot
for (auto& t: aut->out(src))
available -= t.cond;
if (available != bddfalse)
return false;
{
std::const_pointer_cast<twa_graph>(aut)->prop_complete(false);
return false;
}
}
// The empty automaton is not complete since it does not have an
// initial state.
return ns > 0;
bool res = ns > 0;
std::const_pointer_cast<twa_graph>(aut)->prop_complete(res);
return res;
}
bool
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -26,7 +26,7 @@ namespace spot
{
auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in);
res->prop_copy(in, { true, true, true, true, false });
res->prop_copy(in, { true, true, false, true, false, false });
unsigned na = in->num_sets();
unsigned tr = to_remove.count();
assert(tr <= na);
......@@ -54,7 +54,7 @@ namespace spot
auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in);
res->prop_copy(in, { true, true, false, true, false });
res->prop_copy(in, { true, true, false, true, false, false });
res->copy_acceptance_of(in);
transform_copy(in, res, [&](unsigned src,
bdd& cond,
......@@ -76,7 +76,7 @@ namespace spot
auto res = make_twa_graph(in->get_dict());
res->copy_ap_of(in);
res->prop_copy(in, { true, true, false, true, false });
res->prop_copy(in, { true, true, false, true, false, false });
res->copy_acceptance_of(in);
transform_accessible(in, res, [&](unsigned src,
bdd& cond,
......
......@@ -486,7 +486,7 @@ namespace spot
// final is empty: there is no acceptance condition
build_state_set(det_a, non_final);
auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, false, true });
res->prop_copy(a, { false, false, false, false, true, true });
res->prop_deterministic(true);
res->prop_weak(true);
res->prop_state_acc(true);
......@@ -595,7 +595,7 @@ namespace spot
}
auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, false, true });
res->prop_copy(a, { false, false, false, false, false, true });
res->prop_deterministic(true);
res->prop_weak(true);
// If the input was terminal, then the output is also terminal.
......
......@@ -106,22 +106,21 @@ namespace spot
}
}
res->prop_deterministic(left->prop_deterministic()
&& right->prop_deterministic());
res->prop_stutter_invariant(left->prop_stutter_invariant()
&& right->prop_stutter_invariant());
// The product of X!a and Xa, two stutter-sentive formulas,
// is stutter-invariant.
//res->prop_stutter_sensitive(left->prop_stutter_sensitive()
// && right->prop_stutter_sensitive());
res->prop_inherently_weak(left->prop_inherently_weak()
&& right->prop_inherently_weak());
res->prop_weak(left->prop_weak()
&& right->prop_weak());
res->prop_terminal(left->prop_terminal()
&& right->prop_terminal());
res->prop_state_acc(left->prop_state_acc()
&& right->prop_state_acc());
// The product of two non-deterministic automata could be
// deterministic. likewise for non-complete automata.
if (left->prop_deterministic() && right->prop_deterministic())
res->prop_deterministic(true);
if (left->prop_complete() && right->prop_complete())
res->prop_complete(