rename is_deterministic to is_universal
For #212. * spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(), and keep the old name as deprecated. * spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename is_deterministic() as is_universal(), and add a new function for is_deterministic(). * doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org, spot/tl/hierarchy.cc, spot/twa/twagraph.cc, spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc, spot/twaalgos/postproc.cc, spot/twaalgos/product.cc, spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc, spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc, spot/twaalgos/word.cc, tests/python/product.ipynb, tests/python/remfin.py: Adjust. * NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz
parent
4518724a5b
commit
4a5d7a3978
24 changed files with 181 additions and 180 deletions
12
NEWS
12
NEWS
|
|
@ -36,6 +36,18 @@ New in spot 2.3.2.dev (not yet released)
|
|||
It was never used. You always want to use
|
||||
spot::twa_graph::set_init_state(unsigned) in practice.
|
||||
|
||||
- The previous implementation of spot::is_deterministic() has been
|
||||
renamed to spot::is_universal(). The new version of
|
||||
spot::is_deterministic() requires the automaton to be both
|
||||
universal and existential. This should not make any difference in
|
||||
existing code unless you work with the recently added support for
|
||||
alternating automata.
|
||||
|
||||
- The spot::twa::prop_deterministic() methods have been renamed to
|
||||
spot::twa::prop_universal() for consistency with the above change.
|
||||
We have kept spot::twa::prop_deterministic() as a deprecated
|
||||
synonym for spot::twa::prop_universal() to help backward
|
||||
compatibility.
|
||||
|
||||
New in spot 2.3.2 (2017-03-15)
|
||||
|
||||
|
|
|
|||
|
|
@ -1055,14 +1055,14 @@ There are actually several property flags that are stored into each
|
|||
automaton, and that can be queried or set by algorithms:
|
||||
|
||||
| flag name | meaning when =true= |
|
||||
|----------------------+----------------------------------------------------------------------------------------------|
|
||||
|----------------------+-------------------------------------------------------------------------------------------------------------------------------------------|
|
||||
| =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 |
|
||||
| =universal= | there is no non-determinism branching in the automaton (hence each word is *recognized* by at most one run, but not necessarily accepted) |
|
||||
| =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) |
|
||||
| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] |
|
||||
|
|
@ -1083,12 +1083,14 @@ operator =X= does not prevent the formula from being
|
|||
stutter-invariant, but it would require additional work to check.
|
||||
|
||||
As another example, if you write an algorithm that must check whether
|
||||
an automaton is deterministic, do not call the
|
||||
=twa::prop_deterministic()= method, because that might return
|
||||
=trival::maybe=. Instead, call =spot::is_deterministic(...)=: that
|
||||
will respond in constant time if the =deterministic= property flag was
|
||||
either =true= or =false=, otherwise it will actually explore the
|
||||
automaton to decide its determinism.
|
||||
an automaton is universal, do not call the =twa::prop_universal()=
|
||||
method, because that might return =trival::maybe=. Instead, call
|
||||
=spot::is_universal(...)=: that will respond in constant time if the
|
||||
=universal= property flag was either =true= or =false=, otherwise it
|
||||
will actually explore the automaton to decide its determinism. Note
|
||||
that there is also a =spot::is_deterministic(...)= function, which is
|
||||
equivalent to testing that the automaton is both universal and
|
||||
existential.
|
||||
|
||||
These automata properties are encoded into the [[file:hoa.org::#property-bits][HOA format]], so they can
|
||||
be preserved when building a processing pipeline using the shell.
|
||||
|
|
|
|||
|
|
@ -609,11 +609,11 @@ double-checked by the parser.
|
|||
It should be noted that each property can take three values: true,
|
||||
false, or maybe. So actually two bits are used per property. For
|
||||
instance if in some algorithm you want to know whether an automaton is
|
||||
deterministic (the equivalent of calling =autfilt -q
|
||||
--is-deterministic aut.hoa= from the command-line), you should not
|
||||
call the method =aut->prop_deterministic()= because that only checks
|
||||
complete (the equivalent of calling =autfilt -q
|
||||
--is-complete aut.hoa= from the command-line), you should not
|
||||
call the method =aut->prop_complete()= because that only checks
|
||||
the property bits, and it might return =maybe= even if =aut= is
|
||||
deterministic. Instead, call the function =is_deterministic(aut)=.
|
||||
deterministic. Instead, call the function =is_complete(aut)=.
|
||||
This function will first test the property bits, and do the actual
|
||||
check in case it is unknown.
|
||||
|
||||
|
|
@ -639,12 +639,12 @@ this requests "verbose" properties.
|
|||
|
||||
The following table summarizes how supported properties are handled. In
|
||||
particular:
|
||||
- for the parser =checked= means that the property is always inferred
|
||||
- For the parser, =checked= means that the property is always inferred
|
||||
and checked against any declaration (if present), =trusted= means
|
||||
that the property will be stored without being checked (unless
|
||||
=--trust-hoa=no= is specified).
|
||||
- Stored properties are those represented as bits in the automaton.
|
||||
- the printer will sometime check some properties when it can do
|
||||
- The printer will sometime check some properties when it can do
|
||||
it as part of its initial "survey scan" of the automaton; in that
|
||||
case the stored property is not used. This makes it possible
|
||||
to detect deterministic automata that have been output by algorithms
|
||||
|
|
|
|||
|
|
@ -132,7 +132,8 @@ corresponding BDD variable number, and then use for instance
|
|||
// 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 << "Deterministic: " << (aut->prop_universal()
|
||||
&& aut->is_existential()) << '\n';
|
||||
out << "Unambiguous: " << aut->prop_unambiguous() << '\n';
|
||||
out << "State-Based Acc: " << aut->prop_state_acc() << '\n';
|
||||
out << "Terminal: " << aut->prop_terminal() << '\n';
|
||||
|
|
@ -162,57 +163,6 @@ corresponding BDD variable number, and then use for instance
|
|||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
Acceptance: Inf(0)&Inf(1)
|
||||
Number of sets: 2
|
||||
Number of states: 4
|
||||
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
|
||||
Terminal: maybe
|
||||
Weak: maybe
|
||||
Inherently Weak: maybe
|
||||
Stutter Invariant: yes
|
||||
State 0:
|
||||
edge(0 -> 1)
|
||||
label = a
|
||||
acc sets = {}
|
||||
edge(0 -> 2)
|
||||
label = !a
|
||||
acc sets = {}
|
||||
edge(0 -> 3)
|
||||
label = !a
|
||||
acc sets = {}
|
||||
State 1:
|
||||
edge(1 -> 1)
|
||||
label = 1
|
||||
acc sets = {0,1}
|
||||
State 2:
|
||||
edge(2 -> 1)
|
||||
label = a
|
||||
acc sets = {}
|
||||
edge(2 -> 2)
|
||||
label = !a
|
||||
acc sets = {}
|
||||
State 3:
|
||||
edge(3 -> 3)
|
||||
label = !a & b & c
|
||||
acc sets = {0,1}
|
||||
edge(3 -> 3)
|
||||
label = !a & !b & c
|
||||
acc sets = {1}
|
||||
edge(3 -> 3)
|
||||
label = !a & b & !c
|
||||
acc sets = {0}
|
||||
edge(3 -> 3)
|
||||
label = !a & !b & !c
|
||||
acc sets = {}
|
||||
#+end_example
|
||||
|
||||
* Python
|
||||
|
||||
|
|
@ -239,7 +189,7 @@ Here is the very same example, but written in Python:
|
|||
name = aut.get_name()
|
||||
if name:
|
||||
print("Name: ", name)
|
||||
print("Deterministic:", aut.prop_deterministic())
|
||||
print("Deterministic:", aut.prop_universal() and aut.is_existential())
|
||||
print("Unambiguous:", aut.prop_unambiguous())
|
||||
print("State-Based Acc:", aut.prop_state_acc())
|
||||
print("Terminal:", aut.prop_terminal())
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ namespace spot
|
|||
{
|
||||
static bool is_recurrence(formula f, const twa_graph_ptr& aut)
|
||||
{
|
||||
if (f.is_syntactic_recurrence() || is_deterministic(aut))
|
||||
if (f.is_syntactic_recurrence() || is_universal(aut))
|
||||
return true;
|
||||
// If aut is a non-deterministic TGBA, we do
|
||||
// TGBA->DPA->DRA->(D?)BA. The conversion from DRA to
|
||||
|
|
|
|||
|
|
@ -987,7 +987,7 @@ namespace spot
|
|||
trival::repr_t inherently_weak:2; // Inherently Weak automaton.
|
||||
trival::repr_t weak:2; // Weak automaton.
|
||||
trival::repr_t terminal:2; // Terminal automaton.
|
||||
trival::repr_t deterministic:2; // Deterministic automaton.
|
||||
trival::repr_t universal:2; // Universal automaton.
|
||||
trival::repr_t unambiguous:2; // Unambiguous automaton.
|
||||
trival::repr_t stutter_invariant:2; // Stutter invariant language.
|
||||
trival::repr_t very_weak:2; // very-weak, or 1-weak
|
||||
|
|
@ -1292,35 +1292,53 @@ namespace spot
|
|||
is.complete = val.val();
|
||||
}
|
||||
|
||||
/// \brief Whether the automaton is deterministic.
|
||||
/// \brief Whether the automaton is universal.
|
||||
///
|
||||
/// An automaton is deterministic if the conjunction between the
|
||||
/// An automaton is universal if the conjunction between the
|
||||
/// labels of two transitions leaving a state is always false.
|
||||
///
|
||||
/// Note that this method may return trival::maybe() when it is
|
||||
/// unknown whether the automaton is deterministic or not. If you
|
||||
/// need a true/false answer, prefer the is_deterministic() function.
|
||||
/// unknown whether the automaton is universal or not. If you
|
||||
/// need a true/false answer, prefer the is_universal() function.
|
||||
///
|
||||
/// \see prop_unambiguous()
|
||||
/// \see is_deterministic()
|
||||
trival prop_deterministic() const
|
||||
/// \see is_universal()
|
||||
trival prop_universal() const
|
||||
{
|
||||
return is.deterministic;
|
||||
return is.universal;
|
||||
}
|
||||
|
||||
/// \brief Set the deterministic property.
|
||||
/// \brief Set the universal property.
|
||||
///
|
||||
/// Setting the "deterministic" property automatically sets the
|
||||
/// Setting the "universal" property automatically sets the
|
||||
/// "unambiguous" and "semi-deterministic" properties.
|
||||
///
|
||||
/// \see prop_unambiguous()
|
||||
/// \see prop_semi_deterministic()
|
||||
void prop_universal(trival val)
|
||||
{
|
||||
is.universal = val.val();
|
||||
if (val)
|
||||
// universal implies unambiguous and semi-deterministic
|
||||
is.unambiguous = is.semi_deterministic = val.val();
|
||||
}
|
||||
|
||||
// Starting with Spot 2.4, and automaton is deterministic if it is
|
||||
// both universal and existential, but as we already have
|
||||
// twa::is_existential(), we only need to additionally record the
|
||||
// universal property. Before that, the deterministic property
|
||||
// was just a synonym for universal, hence we keep the deprecated
|
||||
// function prop_deterministic() with this meaning.
|
||||
SPOT_DEPRECATED("use prop_universal() instead")
|
||||
void prop_deterministic(trival val)
|
||||
{
|
||||
is.deterministic = val.val();
|
||||
if (val)
|
||||
// deterministic implies unambiguous and semi-deterministic
|
||||
is.unambiguous = is.semi_deterministic = val.val();
|
||||
prop_universal(val);
|
||||
}
|
||||
|
||||
SPOT_DEPRECATED("use prop_universal() instead")
|
||||
trival prop_deterministic() const
|
||||
{
|
||||
return prop_universal();
|
||||
}
|
||||
|
||||
/// \brief Whether the automaton is unambiguous
|
||||
|
|
@ -1334,7 +1352,7 @@ namespace spot
|
|||
/// unknown whether the automaton is unambiguous or not. If you
|
||||
/// need a true/false answer, prefer the is_unambiguous() function.
|
||||
///
|
||||
/// \see prop_deterministic()
|
||||
/// \see prop_universal()
|
||||
/// \see is_unambiguous()
|
||||
trival prop_unambiguous() const
|
||||
{
|
||||
|
|
@ -1344,27 +1362,27 @@ namespace spot
|
|||
/// \brief Sets the unambiguous property
|
||||
///
|
||||
/// Marking an automaton as "non unambiguous" automatically
|
||||
/// marks it as "non deterministic".
|
||||
/// marks it as "non universal".
|
||||
///
|
||||
/// \see prop_deterministic()
|
||||
void prop_unambiguous(trival val)
|
||||
{
|
||||
is.unambiguous = val.val();
|
||||
if (!val)
|
||||
is.deterministic = val.val();
|
||||
is.universal = val.val();
|
||||
}
|
||||
|
||||
/// \brief Whether the automaton is semi-deterministic
|
||||
///
|
||||
/// An automaton is semi-deterministic if the sub-automaton
|
||||
/// reachable from any accepting SCC is deterministic.
|
||||
/// reachable from any accepting SCC is universal.
|
||||
///
|
||||
/// Note that this method may return trival::maybe() when it is
|
||||
/// unknown whether the automaton is semi-deterministic or not.
|
||||
/// If you need a true/false answer, prefer the
|
||||
/// is_semi_deterministic() function.
|
||||
///
|
||||
/// \see prop_deterministic()
|
||||
/// \see prop_universal()
|
||||
/// \see is_semi_deterministic()
|
||||
trival prop_semi_deterministic() const
|
||||
{
|
||||
|
|
@ -1374,14 +1392,14 @@ namespace spot
|
|||
/// \brief Sets the semi-deterministic property
|
||||
///
|
||||
/// Marking an automaton as "non semi-deterministic" automatically
|
||||
/// marks it as "non deterministic".
|
||||
/// marks it as "non universal".
|
||||
///
|
||||
/// \see prop_deterministic()
|
||||
/// \see prop_universal()
|
||||
void prop_semi_deterministic(trival val)
|
||||
{
|
||||
is.semi_deterministic = val.val();
|
||||
if (!val)
|
||||
is.deterministic = val.val();
|
||||
is.universal = val.val();
|
||||
}
|
||||
|
||||
/// \brief Whether the automaton is stutter-invariant.
|
||||
|
|
@ -1434,7 +1452,7 @@ namespace spot
|
|||
/// "stutter invariant" properties from \c other_aut to \c code.
|
||||
///
|
||||
/// There are two flags for the determinism. If \code
|
||||
/// deterministic is set, the deterministic, semi-deterministic,
|
||||
/// deterministic is set, the universal, semi-deterministic,
|
||||
/// and unambiguous properties are copied as-is. If deterministic
|
||||
/// is unset but improve_det is set, then those properties are
|
||||
/// only copied if they are positive.
|
||||
|
|
@ -1542,15 +1560,15 @@ namespace spot
|
|||
}
|
||||
if (p.deterministic)
|
||||
{
|
||||
prop_deterministic(other->prop_deterministic());
|
||||
prop_universal(other->prop_universal());
|
||||
prop_semi_deterministic(other->prop_semi_deterministic());
|
||||
prop_unambiguous(other->prop_unambiguous());
|
||||
}
|
||||
else if (p.improve_det)
|
||||
{
|
||||
if (other->prop_deterministic().is_true())
|
||||
if (other->prop_universal().is_true())
|
||||
{
|
||||
prop_deterministic(true);
|
||||
prop_universal(true);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -1584,8 +1602,8 @@ namespace spot
|
|||
}
|
||||
if (!p.deterministic)
|
||||
{
|
||||
if (!(p.improve_det && prop_deterministic().is_true()))
|
||||
prop_deterministic(trival::maybe());
|
||||
if (!(p.improve_det && prop_universal().is_true()))
|
||||
prop_universal(trival::maybe());
|
||||
if (!(p.improve_det && prop_semi_deterministic().is_true()))
|
||||
prop_semi_deterministic(trival::maybe());
|
||||
if (!(p.improve_det && prop_unambiguous().is_true()))
|
||||
|
|
|
|||
|
|
@ -235,9 +235,9 @@ namespace spot
|
|||
return; // No unreachable state.
|
||||
|
||||
// Removing some non-deterministic dead state could make the
|
||||
// automaton deterministic.
|
||||
if (prop_deterministic().is_false())
|
||||
prop_deterministic(trival::maybe());
|
||||
// automaton universal.
|
||||
if (prop_universal().is_false())
|
||||
prop_universal(trival::maybe());
|
||||
if (prop_complete().is_false())
|
||||
prop_complete(trival::maybe());
|
||||
|
||||
|
|
@ -403,9 +403,9 @@ namespace spot
|
|||
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());
|
||||
// automaton universal. Likewise for non-complete.
|
||||
if (prop_universal().is_false())
|
||||
prop_universal(trival::maybe());
|
||||
if (prop_complete().is_false())
|
||||
prop_complete(trival::maybe());
|
||||
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ namespace spot
|
|||
isomorphism_checker::isomorphism_checker(const const_twa_graph_ptr ref)
|
||||
{
|
||||
ref_ = make_twa_graph(ref, twa::prop_set::all());
|
||||
trival prop_det = ref_->prop_deterministic();
|
||||
trival prop_det = ref_->prop_universal();
|
||||
if (prop_det)
|
||||
{
|
||||
ref_deterministic_ = true;
|
||||
|
|
@ -135,10 +135,10 @@ namespace spot
|
|||
if (!aut->is_existential())
|
||||
throw std::runtime_error
|
||||
("isomorphism_checker does not yet support alternation");
|
||||
trival autdet = aut->prop_deterministic();
|
||||
trival autdet = aut->prop_universal();
|
||||
if (ref_deterministic_)
|
||||
{
|
||||
if (!spot::is_deterministic(aut))
|
||||
if (!spot::is_universal(aut))
|
||||
return false;
|
||||
return are_isomorphic_det(ref_, aut);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@
|
|||
#include <spot/twaalgos/degen.hh>
|
||||
#include <spot/twaalgos/sccfilter.hh>
|
||||
#include <spot/twaalgos/simulation.hh>
|
||||
#include <spot/twaalgos/isdet.hh>
|
||||
|
||||
|
||||
namespace spot
|
||||
|
|
@ -582,7 +583,7 @@ namespace spot
|
|||
if (!a->is_existential())
|
||||
throw std::runtime_error
|
||||
("tgba_determinize() does not support alternation");
|
||||
if (a->prop_deterministic())
|
||||
if (is_universal(a))
|
||||
return std::const_pointer_cast<twa_graph>(a);
|
||||
|
||||
// Degeneralize
|
||||
|
|
@ -701,7 +702,7 @@ namespace spot
|
|||
remove_dead_acc(res, sets);
|
||||
// Acceptance is now min(odd) since we con emit Red on paths 0 with new opti
|
||||
res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
|
||||
res->prop_deterministic(true);
|
||||
res->prop_universal(true);
|
||||
res->prop_state_acc(false);
|
||||
|
||||
if (pretty_print)
|
||||
|
|
|
|||
|
|
@ -599,7 +599,7 @@ namespace spot
|
|||
a->set_buchi();
|
||||
if (state_based)
|
||||
a->prop_state_acc(true);
|
||||
a->prop_deterministic(true);
|
||||
a->prop_universal(true);
|
||||
a->new_states(satdict.cand_size);
|
||||
|
||||
#if DEBUG
|
||||
|
|
|
|||
|
|
@ -879,7 +879,7 @@ namespace spot
|
|||
a->copy_ap_of(aut);
|
||||
if (state_based)
|
||||
a->prop_state_acc(true);
|
||||
a->prop_deterministic(true);
|
||||
a->prop_universal(true);
|
||||
a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
|
||||
a->new_states(satdict.cand_size);
|
||||
|
||||
|
|
@ -1474,7 +1474,7 @@ namespace spot
|
|||
// mode. If the desired output is a Büchi automaton, or not
|
||||
// desired acceptance was specified, stop here. There is not
|
||||
// point in minimizing a minimal automaton.
|
||||
if (a->prop_inherently_weak() && a->prop_deterministic()
|
||||
if (a->prop_weak() && a->prop_universal()
|
||||
&& (target_is_buchi || !user_supplied_acc))
|
||||
return a;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -158,10 +158,10 @@ namespace spot
|
|||
// some states without successors do not declare it as
|
||||
// colored.
|
||||
is_colored = colored && (!has_state_acc || nodeadend);
|
||||
// If the automaton declares that it is deterministic or
|
||||
// If the automaton declares that it is universal or
|
||||
// state-based, make sure that it really is.
|
||||
assert(!aut->prop_deterministic().is_known() ||
|
||||
deterministic == aut->prop_deterministic().is_true());
|
||||
assert(!aut->prop_universal().is_known() ||
|
||||
deterministic == aut->prop_universal().is_true());
|
||||
assert(!aut->prop_complete().is_known() ||
|
||||
complete == aut->prop_complete().is_true());
|
||||
assert(state_acc || !aut->prop_state_acc().is_true());
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ namespace spot
|
|||
break;
|
||||
}
|
||||
std::const_pointer_cast<twa_graph>(aut)
|
||||
->prop_deterministic(!nondet_states);
|
||||
->prop_universal(!nondet_states);
|
||||
return nondet_states;
|
||||
}
|
||||
}
|
||||
|
|
@ -58,29 +58,35 @@ namespace spot
|
|||
unsigned
|
||||
count_nondet_states(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
if (aut->prop_deterministic())
|
||||
if (aut->prop_universal())
|
||||
return 0;
|
||||
return count_nondet_states_aux<true>(aut);
|
||||
}
|
||||
|
||||
bool
|
||||
is_deterministic(const const_twa_graph_ptr& aut)
|
||||
is_universal(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
trival d = aut->prop_deterministic();
|
||||
trival d = aut->prop_universal();
|
||||
if (d.is_known())
|
||||
return d.is_true();
|
||||
return !count_nondet_states_aux<false>(aut);
|
||||
}
|
||||
|
||||
bool
|
||||
is_deterministic(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
return aut->is_existential() && is_universal(aut);
|
||||
}
|
||||
|
||||
void
|
||||
highlight_nondet_states(twa_graph_ptr& aut, unsigned color)
|
||||
{
|
||||
if (aut->prop_deterministic())
|
||||
if (aut->prop_universal())
|
||||
return;
|
||||
unsigned ns = aut->num_states();
|
||||
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
|
||||
("highlight-states");
|
||||
bool deterministic = true;
|
||||
bool universal = true;
|
||||
for (unsigned src = 0; src < ns; ++src)
|
||||
{
|
||||
bdd available = bddtrue;
|
||||
|
|
@ -88,25 +94,25 @@ namespace spot
|
|||
if (!bdd_implies(t.cond, available))
|
||||
{
|
||||
(*highlight)[src] = color;
|
||||
deterministic = false;
|
||||
universal = false;
|
||||
}
|
||||
else
|
||||
{
|
||||
available -= t.cond;
|
||||
}
|
||||
}
|
||||
aut->prop_deterministic(deterministic);
|
||||
aut->prop_universal(universal);
|
||||
}
|
||||
|
||||
void
|
||||
highlight_nondet_edges(twa_graph_ptr& aut, unsigned color)
|
||||
{
|
||||
if (aut->prop_deterministic())
|
||||
if (aut->prop_universal())
|
||||
return;
|
||||
unsigned ns = aut->num_states();
|
||||
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
|
||||
("highlight-edges");
|
||||
bool deterministic = true;
|
||||
bool universal = true;
|
||||
for (unsigned src = 0; src < ns; ++src)
|
||||
{
|
||||
// Make a first pass to gather non-deterministic labels
|
||||
|
|
@ -116,19 +122,19 @@ namespace spot
|
|||
if (!bdd_implies(t.cond, available))
|
||||
{
|
||||
extra |= (t.cond - available);
|
||||
deterministic = false;
|
||||
universal = false;
|
||||
}
|
||||
else
|
||||
{
|
||||
available -= t.cond;
|
||||
}
|
||||
// Second pass to gather the relevant edges.
|
||||
if (!deterministic)
|
||||
if (!universal)
|
||||
for (auto& t: aut->out(src))
|
||||
if ((t.cond & extra) != bddfalse)
|
||||
(*highlight)[aut->get_graph().index_of_edge(t)] = color;
|
||||
}
|
||||
aut->prop_deterministic(deterministic);
|
||||
aut->prop_universal(universal);
|
||||
}
|
||||
|
||||
bool
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -26,24 +26,33 @@ namespace spot
|
|||
/// \addtogroup twa_misc
|
||||
/// @{
|
||||
|
||||
/// \brief Count the number of non-deterministic states in \a aut.
|
||||
/// \brief Count the number of states with non-deterministic
|
||||
/// branching in \a aut.
|
||||
///
|
||||
/// The automaton is deterministic if it has 0 nondeterministic states,
|
||||
/// but it is more efficient to call is_deterministic() if you do not
|
||||
/// care about the number of nondeterministic states.
|
||||
/// The automaton is universal if it has 0 states with
|
||||
/// non-deterministic branching but it is more efficient to call
|
||||
/// is_universal() if you do not care about the number of
|
||||
/// non-deterministic states.
|
||||
SPOT_API unsigned
|
||||
count_nondet_states(const const_twa_graph_ptr& aut);
|
||||
|
||||
/// \brief Return true iff \a aut is deterministic.
|
||||
/// \brief Return true iff \a aut is universal.
|
||||
///
|
||||
/// This function is more efficient than count_nondet_states() when
|
||||
/// the automaton is nondeterministic, because it can return before
|
||||
/// the entire automaton has been explored.
|
||||
///
|
||||
/// In addition to returning the result as a Boolean, this will set
|
||||
/// the prop_deterministic() property of the automaton as a
|
||||
/// the prop_universal() property of the automaton as a
|
||||
/// side-effect, so further calls will return in constant-time.
|
||||
SPOT_API bool
|
||||
is_universal(const const_twa_graph_ptr& aut);
|
||||
|
||||
/// \brief Return true iff \a aut is deterministic.
|
||||
///
|
||||
/// An automaton is called deterministic if it is both universal and
|
||||
/// existential.
|
||||
SPOT_API bool
|
||||
is_deterministic(const const_twa_graph_ptr& aut);
|
||||
|
||||
/// \brief Highlight nondeterministic states
|
||||
|
|
|
|||
|
|
@ -487,7 +487,7 @@ namespace spot
|
|||
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, true });
|
||||
res->prop_deterministic(true);
|
||||
res->prop_universal(true);
|
||||
res->prop_weak(true);
|
||||
res->prop_state_acc(true);
|
||||
// Quickly check if this is a terminal automaton
|
||||
|
|
@ -596,7 +596,7 @@ namespace spot
|
|||
|
||||
auto res = minimize_dfa(det_a, final, non_final);
|
||||
res->prop_copy(a, { false, false, false, false, false, true });
|
||||
res->prop_deterministic(true);
|
||||
res->prop_universal(true);
|
||||
res->prop_weak(true);
|
||||
// If the input was terminal, then the output is also terminal.
|
||||
// FIXME:
|
||||
|
|
@ -633,7 +633,7 @@ namespace spot
|
|||
|
||||
// If the input automaton was already weak and deterministic, the
|
||||
// output is necessary correct.
|
||||
if (aut_f->prop_weak() && aut_f->prop_deterministic())
|
||||
if (aut_f->prop_weak() && aut_f->prop_universal())
|
||||
return min_aut_f;
|
||||
|
||||
// if f is a syntactic obligation formula, the WDBA minimization
|
||||
|
|
|
|||
|
|
@ -272,7 +272,7 @@ namespace spot
|
|||
dba = minimize_obligation(a, f, nullptr, reject_bigger);
|
||||
if (dba
|
||||
&& dba->prop_inherently_weak().is_true()
|
||||
&& dba->prop_deterministic().is_true())
|
||||
&& dba->prop_universal().is_true())
|
||||
{
|
||||
// The WDBA is a BA, so no degeneralization is required.
|
||||
// We just need to add an acceptance set if there is none.
|
||||
|
|
|
|||
|
|
@ -107,9 +107,9 @@ namespace spot
|
|||
}
|
||||
|
||||
// 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);
|
||||
// deterministic. Likewise for non-complete automata.
|
||||
if (left->prop_universal() && right->prop_universal())
|
||||
res->prop_universal(true);
|
||||
if (left->prop_complete() && right->prop_complete())
|
||||
res->prop_complete(true);
|
||||
if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2008-2010, 2012-2017 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
|
|
@ -130,7 +130,7 @@ namespace spot
|
|||
throw std::invalid_argument("random_graph() requires n>0 states");
|
||||
auto res = make_twa_graph(dict);
|
||||
if (deterministic)
|
||||
res->prop_deterministic(true);
|
||||
res->prop_universal(true);
|
||||
if (state_acc)
|
||||
res->prop_state_acc(true);
|
||||
|
||||
|
|
|
|||
|
|
@ -228,7 +228,7 @@ namespace spot
|
|||
res->new_states(nst);
|
||||
res->set_buchi();
|
||||
res->set_init_state(aut->get_init_state_number());
|
||||
trival deterministic = aut->prop_deterministic();
|
||||
trival deterministic = aut->prop_universal();
|
||||
trival complete = aut->prop_complete();
|
||||
|
||||
std::vector<unsigned> state_map(aut->num_states());
|
||||
|
|
@ -302,7 +302,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
res->prop_complete(complete);
|
||||
res->prop_deterministic(deterministic);
|
||||
res->prop_universal(deterministic);
|
||||
res->purge_dead_states();
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -600,7 +600,7 @@ namespace spot
|
|||
});
|
||||
// !unambiguous and !semi-deterministic are not preserved
|
||||
if (!Cosimulation)
|
||||
res->prop_deterministic(nb_minato == nb_satoneset);
|
||||
res->prop_universal(nb_minato == nb_satoneset);
|
||||
if (Sba)
|
||||
res->prop_state_acc(true);
|
||||
return res;
|
||||
|
|
@ -736,7 +736,7 @@ namespace spot
|
|||
prev = next;
|
||||
direct_simulation<false, Sba> simul(res ? res : t);
|
||||
res = simul.run();
|
||||
if (res->prop_deterministic())
|
||||
if (res->prop_universal())
|
||||
break;
|
||||
|
||||
direct_simulation<true, Sba> cosimul(res);
|
||||
|
|
|
|||
|
|
@ -336,7 +336,7 @@ namespace spot
|
|||
res->set_init_state(res->new_state());
|
||||
res->prop_state_acc(true);
|
||||
res->prop_weak(true);
|
||||
res->prop_deterministic(true);
|
||||
res->prop_universal(true);
|
||||
res->prop_stutter_invariant(true);
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -226,7 +226,7 @@ namespace spot
|
|||
twa_graph_ptr aut = make_twa_graph(dict_);
|
||||
|
||||
aut->prop_weak(true);
|
||||
aut->prop_deterministic(true);
|
||||
aut->prop_universal(true);
|
||||
|
||||
// Register the atomic propositions used in the word.
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1524,23 +1524,23 @@
|
|||
"\n",
|
||||
"We could stop with the previous function: the result is a correct product from a theoretical point of view. However our function is still inferior to `spot.product()` in a couple of points:\n",
|
||||
"- states are not presented as pairs\n",
|
||||
"- the properties of the resulting automaton are not sets\n",
|
||||
"- the properties of the resulting automaton are not set\n",
|
||||
"\n",
|
||||
"The former point can be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output. \n",
|
||||
"\n",
|
||||
"(Note: the original `spot.product()` is in fact *not* naming states. The `spot.product()` function actually attaches a vector of pairs of integers to the automaton because some algorithms need to project a state of the product onto the original automaton. The `dot` printer knows how to display those pairs for states that are not named. Here we shall name states because (1) that is more flexible, and (2) there is a Python interface for this.)\n",
|
||||
"\n",
|
||||
"Regarding the latter point, consider for instance the deterministic nature of these automata:"
|
||||
"Regarding the latter point, consider for instance the deterministic nature of these automata. In Spot an automaton is deterministic if it is both existential (no universal branching) and universal (no non-deterministic branching). In our case we will restrict the algorithm to existantial input (by asserting `is_existential()` on both operands), so we can consider that the `prop_universal()` property is an indication of determinism:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"print(a1.prop_deterministic())\n",
|
||||
"print(a2.prop_deterministic())\n",
|
||||
"print(prod.prop_deterministic())\n",
|
||||
"print(p1.prop_deterministic())"
|
||||
"print(a1.prop_universal())\n",
|
||||
"print(a2.prop_universal())\n",
|
||||
"print(prod.prop_universal())\n",
|
||||
"print(p1.prop_universal())"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
|
|
@ -1564,18 +1564,18 @@
|
|||
"source": [
|
||||
"Because `a1` and `a2` are deterministic, their product is necessarily deterministic. This is a property that the `spot.product()` algorithm will preserve, but that our version does not *yet* preserve. We can fix that by adding\n",
|
||||
"\n",
|
||||
" if left.prop_deterministic() and right.prop_deterministic():\n",
|
||||
" result.prop_deterministic(True)\n",
|
||||
" if left.prop_universal() and right.prop_universal():\n",
|
||||
" result.prop_universal(True)\n",
|
||||
" \n",
|
||||
"at the end of our function. Note that this is **not** the same as\n",
|
||||
"\n",
|
||||
" result.prop_deterministic(left.prop_deterministic() and right.prop_deterministic())\n",
|
||||
" result.prop_universal(left.prop_universal() and right.prop_universal())\n",
|
||||
"\n",
|
||||
"because the results the `prop_*()` family of functions take and return instances of `spot.trival` values. These `spot.trival`, can, as their name implies, take one amongst three values representing `yes`, `no`, and `maybe`. `yes` and `no` should be used when we actually know that the automaton is deterministic or not (not deterministic meaning that there actually exists some non determinitic state in the automaton), and `maybe` when we do not know. \n",
|
||||
"\n",
|
||||
"The one-liner above is wrong for two reasons:\n",
|
||||
"\n",
|
||||
" - if `left` and `right` are non-deterministic, their product could be deterministic, so calling prop_deterministic(False) would be wrong. \n",
|
||||
" - if `left` and `right` are non-deterministic, their product could be deterministic, so calling prop_universal(False) would be wrong. \n",
|
||||
"\n",
|
||||
" - the use of the `and` operator on `trival` is misleading in non-Boolean context. The `&` operator would be the correct operator to use if you want to work in threed-valued logic. Compare: "
|
||||
]
|
||||
|
|
@ -1621,8 +1621,8 @@
|
|||
"\n",
|
||||
"So our\n",
|
||||
"\n",
|
||||
" if left.prop_deterministic() and right.prop_deterministic():\n",
|
||||
" result.prop_deterministic(True)\n",
|
||||
" if left.prop_universal() and right.prop_universal():\n",
|
||||
" result.prop_universal(True)\n",
|
||||
"\n",
|
||||
"is OK because the `if` body will only be entered of both input automata are known to be deterministic."
|
||||
]
|
||||
|
|
@ -1639,6 +1639,9 @@
|
|||
"collapsed": false,
|
||||
"input": [
|
||||
"def product3(left, right):\n",
|
||||
" # the twa_graph.is_existential() method returns a Boolean, not a spot.trival\n",
|
||||
" if not (left.is_existential() and right.is_existential()):\n",
|
||||
" raise RuntimeError(\"alternating automata are not supported\")\n",
|
||||
" bdict = left.get_dict()\n",
|
||||
" if right.get_dict() != bdict:\n",
|
||||
" raise RuntimeError(\"automata should share their dictionary\")\n",
|
||||
|
|
@ -1680,7 +1683,7 @@
|
|||
" result.set_state_names(names)\n",
|
||||
" \n",
|
||||
" # Loop over all the properties we want to preserve if they hold in both automata\n",
|
||||
" for p in ('prop_deterministic', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n",
|
||||
" for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n",
|
||||
" 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n",
|
||||
" if getattr(left, p)() and getattr(right, p)():\n",
|
||||
" getattr(result, p)(True)\n",
|
||||
|
|
@ -1688,7 +1691,7 @@
|
|||
"\n",
|
||||
"p3 = product3(a1, a2)\n",
|
||||
"show_prod(a1, a2, p3)\n",
|
||||
"print(p3.prop_deterministic())"
|
||||
"print(p3.prop_universal())"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
|
|
@ -2018,7 +2021,7 @@
|
|||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 9
|
||||
"prompt_number": 14
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
|
|
@ -2042,7 +2045,7 @@
|
|||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"1000 loops, best of 3: 206 \u00b5s per loop\n"
|
||||
"1000 loops, best of 3: 202 \u00b5s per loop\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
@ -2061,8 +2064,8 @@
|
|||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"The slowest run took 6.27 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
|
||||
"100000 loops, best of 3: 4.2 \u00b5s per loop\n"
|
||||
"The slowest run took 5.71 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
|
||||
"100000 loops, best of 3: 4.39 \u00b5s per loop\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ assert(aut1.get_name() == "test me")
|
|||
# The method is the same as the function
|
||||
|
||||
a = spot.translate('true', 'low', 'any')
|
||||
assert(a.prop_deterministic().is_maybe())
|
||||
assert(a.prop_universal().is_maybe())
|
||||
assert(a.prop_unambiguous().is_maybe())
|
||||
assert(a.is_deterministic() == True)
|
||||
assert(a.is_unambiguous() == True)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue