alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: store property bits as trivals

Browse source 
* spot/twa/twa.hh: Store property bits as trivals.
* NEWS: Mention the change.
* spot/parseaut/parseaut.yy, spot/twaalgos/are_isomorphic.cc,
spot/twaalgos/complete.cc, spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh,
spot/twaalgos/totgba.cc, tests/core/ikwiad.cc,
tests/python/product.ipynb, tests/python/remfin.py: Adjust.
* doc/org/hoa.org, doc/org/tut21.org: Update documentation.
This commit is contained in:
Alexandre Duret-Lutz 2016-01-12 19:37:18 +01:00
parent 1aeb260adf
commit da391492f3
22 changed files with 337 additions and 258 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -74,6 +74,15 @@ New in spot 1.99.6a (not yet released)
acc_cond::is_ff() -> acc_cond::is_f()
parse_acc_code() -> acc_cond::acc_code(...)
* Automata property bits (those that tell whether the automaton is
deterministic, weak, stutter-invariant, etc.) are now stored using
three-valued logic: in addition to "maybe"/"yes" they can now also
represent "no". This is some preparation for the upcomming
support of the HOA v1.1 format, but it also saves some time in
some algorithms (e.g, is_deterministic() can now return
immediately on automata marked as not deterministic).
Python:
* Iterating over the transitions leaving a state (the

38
doc/org/hoa.org
View file

@ -186,15 +186,15 @@ rm -f stvstracc.hoa
Even if an input HOA file uses only state-based acceptance, Spot
internally stores it using transition-based acceptance. However in
that case the TωA will have a property bit indicating that it actually
that case the TωA will have a property flag indicating that it actually
represents an automaton with the "state-based acceptance" property:
this implies that transitions leaving one state all belong to the same
acceptance sets. A couple of algorithms in Spot checks for this
property, and enable specialized treatments of state-based automata.
Furthermore, even if an automaton does not have the "state-based
acceptance" property bit set, the HOA output routine may detect that
the automaton satisfies this property. In that case, it output the
acceptance" property flag set, the HOA output routine may detect that
the automaton satisfies this property. In that case, it outputs the
automaton with state-based acceptance.
For instance in the following automaton, the outgoing transitions of
@ -583,7 +583,7 @@ labels whenever that is possible. The option is named =k= (i.e., use
=-Hk= with command-line tools) because it is useful when the HOA file
is used to describe a Kripke structure.
** Property bits
** Property flags
:PROPERTIES:
:CUSTOM_ID: property-bits
:END:
@ -593,7 +593,7 @@ These properties can be useful to speedup certain algorithms: for
instance it is easier to complement a deterministic automaton that is
known to be inherently weak.
Spot stores this properties that matters to its algorithms as
Spot stores the properties that matters to its algorithms as
additional bits attached to each automaton. Currently the HOA parser
ignores all the properties that are unused by Spot.
@ -603,22 +603,22 @@ is parsed; this is for instance the case of =deterministic=,
body of the file, and then return and error if what has been declared
does not correspond to the reality.
Some supported properties (like =weak=, =unambiguous=, or
=stutter-invariant=) are not double-checked, because that would
require too much additional operations. Command-line tools that read
HOA files all take a =--trust-hoa=no= option to ignore properties that
are not double-checked by the parser.
Some supported properties (like =weak=, =inherently-weak=,
=unambiguous=, or =stutter-invariant=) are not double-checked, because
that would require more operations. Command-line tools that
read HOA files all take a =--trust-hoa=no= option to ignore properties
that are not double-checked by the parser.
It should be noted that these bits are only implications. When such a
bit is false, it only means that it is unknown whether the property is
true. For instance if in some algorithm you want to know whether an
automaton is deterministic (the equivalent of calling =autfilt -q
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
the property bit, and it might be false even if the =aut= is
the property bits, and it might return =maybe= even if =aut= is
deterministic. Instead, call the function =is_deterministic(aut)=.
This function will first test the property bit, and do the actual
check if it has to.
This function will first test the property bits, and do the actual
check in case it is unknown.
Algorithms that update a TωA should call the method =prop_keep()= and
use the argument to specify which of the properties they preserve.
@ -632,7 +632,7 @@ take a new argument).
The =HOA= printer also tries to not bloat the output with many
redundant and useless properties. For instance =deterministic=
automata are necessarily =unambiguous=, and people interested in
unambiguous automata know that, so Spot only output the =unambiguous=
unambiguous automata know that, so Spot only outputs the =unambiguous=
property if an unambiguous automaton is non-deterministic. Similarly,
while Spot only outputs non-alternating automata, it does not output
the =no-univ-branch= property because we cannot think of a situation
@ -666,7 +666,7 @@ particular:
| =complete= | checked | no | checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored | can be checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored (opposite of =stutter-invariant=) | can be checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= |

71
doc/org/tut21.org
View file

@ -37,8 +37,7 @@ Start: 0
AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc unambiguous
properties: stutter-invariant
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[0] 1
@ -121,29 +120,22 @@ corresponding BDD variable number, and then use for instance
if (auto name = aut->get_named_prop<std::string>("automaton-name"))
out << "Name: " << *name << '\n';
// For the following prop_*() methods, true means "it's sure", false
// means "I don't know". These properties correspond to bits stored
// in the automaton, so they can be queried in constant time. They
// are only set whenever they can be determined at a cheap cost: for
// instance any algorithm that always produce deterministic automata
// would set the deterministic bit on its output. In this example,
// the properties that are set come from the "properties:" line of
// the input file.
out << "Deterministic: "
<< (aut->prop_deterministic() ? "yes\n" : "maybe\n");
out << "Unambiguous: "
<< (aut->prop_unambiguous() ? "yes\n" : "maybe\n");
out << "State-Based Acc: "
<< (aut->prop_state_acc() ? "yes\n" : "maybe\n");
out << "Terminal: "
<< (aut->prop_terminal() ? "yes\n" : "maybe\n");
out << "Weak: "
<< (aut->prop_weak() ? "yes\n" : "maybe\n");
out << "Inherently Weak: "
<< (aut->prop_inherently_weak() ? "yes\n" : "maybe\n");
out << "Stutter Invariant: "
<< (aut->prop_stutter_invariant() ? "yes\n" :
aut->prop_stutter_sensitive() ? "no\n" : "maybe\n");
// For the following prop_*() methods, the return value is an
// instance of the spot::trival class that can represent
// yes/maybe/no. These properties correspond to bits stored in the
// automaton, so they can be queried in constant time. They are
// only set whenever they can be determined at a cheap cost: for
// instance an algorithm that always produces deterministic automata
// 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 << "Deterministic: " << aut->prop_deterministic() << '\n';
out << "Unambiguous: " << aut->prop_unambiguous() << '\n';
out << "State-Based Acc: " << aut->prop_state_acc() << '\n';
out << "Terminal: " << aut->prop_terminal() << '\n';
out << "Weak: " << aut->prop_weak() << '\n';
out << "Inherently Weak: " << aut->prop_inherently_weak() << '\n';
out << "Stutter Invariant: " << aut->prop_stutter_invariant() << '\n';
// States are numbered from 0 to n-1
unsigned n = aut->num_states();
@ -175,8 +167,8 @@ Number of edges: 10
Initial state: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: Fa | G(Fb & Fc)
Deterministic: maybe
Unambiguous: yes
Deterministic: no
Unambiguous: maybe
State-Based Acc: maybe
Terminal: maybe
Weak: maybe
@ -226,12 +218,6 @@ Here is the very same example, but written in Python:
import spot
def maybe_yes(pos, neg=False):
if neg:
return "no"
return "yes" if pos else "maybe"
def custom_print(aut):
bdict = aut.get_dict()
print("Acceptance:", aut.get_acceptance())
@ -249,14 +235,13 @@ Here is the very same example, but written in Python:
name = aut.get_name()
if name:
print("Name: ", name)
print("Deterministic:", maybe_yes(aut.prop_deterministic()))
print("Unambiguous:", maybe_yes(aut.prop_unambiguous()))
print("State-Based Acc:", maybe_yes(aut.prop_state_acc()))
print("Terminal:", maybe_yes(aut.prop_terminal()))
print("Weak:", maybe_yes(aut.prop_weak()))
print("Inherently Weak:", maybe_yes(aut.prop_inherently_weak()))
print("Stutter Invariant:", maybe_yes(aut.prop_stutter_invariant(),
aut.prop_stutter_sensitive()))
print("Deterministic:", aut.prop_deterministic())
print("Unambiguous:", aut.prop_unambiguous())
print("State-Based Acc:", aut.prop_state_acc())
print("Terminal:", aut.prop_terminal())
print("Weak:", aut.prop_weak())
print("Inherently Weak:", aut.prop_inherently_weak())
print("Stutter Invariant:", aut.prop_stutter_invariant())
for s in range(0, aut.num_states()):
print("State {}:".format(s))
@ -280,8 +265,8 @@ Number of states: 4
Initial states: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: Fa | G(Fb & Fc)
Deterministic: maybe
Unambiguous: yes
Deterministic: no
Unambiguous: maybe
State-Based Acc: maybe
Terminal: maybe
Weak: maybe

46
spot/parseaut/parseaut.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
** Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
**
@ -132,7 +132,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
bool accept_all_seen = false;
bool aliased_states = false;
bool deterministic = false;
spot::trival deterministic = spot::trival::maybe();
bool complete = false;
bool trans_acc_seen = false;
@ -457,12 +457,25 @@ header: format-version header-items
auto& a = res.aut_or_ks;
auto& p = res.props;
auto e = p.end();
a->prop_stutter_invariant(p.find("stutter-invariant") != e);
a->prop_stutter_sensitive(p.find("stutter-sensitive") != e);
a->prop_inherently_weak(p.find("inherently-weak") != e);
a->prop_weak(p.find("weak") != e);
a->prop_terminal(p.find("terminal") != e);
a->prop_unambiguous(p.find("unambiguous") != e);
if (p.find("stutter-invariant") != e)
{
a->prop_stutter_invariant(true);
auto i = p.find("stutter-sensitive");
if (i != e)
error(i->second,
"automaton cannot be both stutter-invariant"
"and stutter-sensitive");
}
if (p.find("stutter-sensitive") != e)
a->prop_stutter_invariant(false);
if (p.find("inherently-weak") != e)
a->prop_inherently_weak(true);
if (p.find("weak") != e)
a->prop_weak(true);
if (p.find("terminal") != e)
a->prop_terminal(true);
if (p.find("unambiguous") != e)
a->prop_unambiguous(true);
}
}
@ -952,8 +965,9 @@ state: state-name labeled-edges
}
| error
{
// Assume the worse.
res.deterministic = false;
// Assume the worse. This skips the tests about determinism
// we might perform on the state.
res.deterministic = spot::trival::maybe();
res.complete = false;
}
@ -1242,8 +1256,8 @@ dstar_header: dstar_sizes
res.h->aut->new_states(res.states);;
res.info_states.resize(res.states);
}
res.h->aut->prop_state_acc(true);
res.h->aut->prop_deterministic(true);
res.acc_style = State_Acc;
res.deterministic = true;
// res.h->aut->prop_complete();
fill_guards(res);
res.cur_guard = res.guards.end();
@ -1394,8 +1408,7 @@ never: "never"
}
res.namer = res.h->aut->create_namer<std::string>();
res.h->aut->set_buchi();
res.h->aut->prop_state_acc(true);
res.acc_state = State_Acc;
res.acc_style = State_Acc;
res.pos_acc_sets = res.h->aut->acc().all_sets();
}
'{' nc-states '}'
@ -1658,8 +1671,7 @@ lbtt-header-states: LBTT
lbtt-header: lbtt-header-states INT_S
{
res.acc_mapper = new spot::acc_mapper_int(res.h->aut, $2);
res.h->aut->prop_state_acc(true);
res.acc_state = State_Acc;
res.acc_style = State_Acc;
}
| lbtt-header-states INT
{

114
spot/twa/twa.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// 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.
@ -34,6 +34,7 @@
#include <spot/misc/casts.hh>
#include <spot/misc/hash.hh>
#include <spot/tl/formula.hh>
#include <spot/misc/trival.hh>
namespace spot
{
@ -757,14 +758,13 @@ namespace spot
// holds, but false means the property is unknown.
struct bprop
{
bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Inherently Weak automaton.
bool weak:1; // Weak automaton.
bool terminal:1; // Terminal automaton.
bool deterministic:1; // Deterministic automaton.
bool unambiguous:1; // Unambiguous automaton.
bool stutter_invariant:1; // Stutter invariant language.
bool stutter_sensitive:1; // Stutter sensitive language.
trival::repr_t state_based_acc:2; // State-based acceptance.
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 unambiguous:2; // Unambiguous automaton.
trival::repr_t stutter_invariant:2; // Stutter invariant language.
};
union
{
@ -810,104 +810,92 @@ namespace spot
named_prop_.clear();
}
bool prop_state_acc() const
trival prop_state_acc() const
{
return is.state_based_acc;
}
void prop_state_acc(bool val)
void prop_state_acc(trival val)
{
is.state_based_acc = val;
is.state_based_acc = val.val();
}
bool is_sba() const
trival is_sba() const
{
return prop_state_acc() && acc().is_buchi();
}
bool prop_inherently_weak() const
trival prop_inherently_weak() const
{
return is.inherently_weak;
}
void prop_inherently_weak(bool val)
void prop_inherently_weak(trival val)
{
is.inherently_weak = val;
is.inherently_weak = val.val();
if (!val)
is.terminal = is.weak = val.val();
}
bool prop_terminal() const
trival prop_terminal() const
{
return is.terminal;
}
void prop_terminal(bool val)
void prop_terminal(trival val)
{
is.terminal = val.val();
if (val)
is.inherently_weak = is.weak = is.terminal = true;
else
is.terminal = false;
is.inherently_weak = is.weak = val.val();
}
bool prop_weak() const
trival prop_weak() const
{
return is.weak;
}
void prop_weak(bool val)
void prop_weak(trival val)
{
is.weak = val.val();
if (val)
is.inherently_weak = is.weak = true;
else
is.weak = false;
is.inherently_weak = val.val();
if (!val)
is.terminal = val.val();
}
bool prop_deterministic() const
trival prop_deterministic() const
{
return is.deterministic;
}
void prop_deterministic(bool val)
void prop_deterministic(trival val)
{
is.deterministic = val.val();
if (val)
{
// deterministic implies unambiguous
is.deterministic = true;
is.unambiguous = true;
}
else
{
is.deterministic = false;
}
is.unambiguous = val.val();
}
bool prop_unambiguous() const
trival prop_unambiguous() const
{
return is.unambiguous;
}
void prop_unambiguous(bool val)
void prop_unambiguous(trival val)
{
is.unambiguous = val;
is.unambiguous = val.val();
if (!val)
is.deterministic = val.val();
}
bool prop_stutter_invariant() const
trival prop_stutter_invariant() const
{
return is.stutter_invariant;
}
bool prop_stutter_sensitive() const
void prop_stutter_invariant(trival val)
{
return is.stutter_sensitive;
}
void prop_stutter_invariant(bool val)
{
is.stutter_invariant = val;
}
void prop_stutter_sensitive(bool val)
{
is.stutter_sensitive = val;
is.stutter_invariant = val.val();
}
struct prop_set
@ -941,32 +929,26 @@ namespace spot
prop_unambiguous(other->prop_unambiguous());
}
if (p.stutter_inv)
{
prop_stutter_invariant(other->prop_stutter_invariant());
prop_stutter_sensitive(other->prop_stutter_sensitive());
}
}
void prop_keep(prop_set p)
{
if (!p.state_based)
prop_state_acc(false);
prop_state_acc(trival::maybe());
if (!p.inherently_weak)
{
prop_terminal(false);
prop_weak(false);
prop_inherently_weak(false);
prop_terminal(trival::maybe());
prop_weak(trival::maybe());
prop_inherently_weak(trival::maybe());
}
if (!p.deterministic)
{
prop_deterministic(false);
prop_unambiguous(false);
prop_deterministic(trival::maybe());
prop_unambiguous(trival::maybe());
}
if (!p.stutter_inv)
{
prop_stutter_invariant(false);
prop_stutter_sensitive(false);
}
prop_stutter_invariant(trival::maybe());
}
};

17
spot/twaalgos/are_isomorphic.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -113,9 +113,16 @@ namespace spot
isomorphism_checker::isomorphism_checker(const const_twa_graph_ptr ref)
{
ref_ = make_twa_graph(ref, twa::prop_set::all());
ref_deterministic_ = ref_->prop_deterministic();
if (!ref_deterministic_)
trival prop_det = ref_->prop_deterministic();
if (prop_det)
{
ref_deterministic_ = true;
}
else
{
// Count the number of state even if we know that the
// automaton is non-deterministic, as this can be used to
// decide if two automata are non-isomorphic.
nondet_states_ = spot::count_nondet_states(ref_);
ref_deterministic_ = (nondet_states_ == 0);
}
@ -125,10 +132,10 @@ namespace spot
bool
isomorphism_checker::is_isomorphic_(const const_twa_graph_ptr aut)
{
bool autdet = aut->prop_deterministic();
trival autdet = aut->prop_deterministic();
if (ref_deterministic_)
{
if (autdet || spot::is_deterministic(aut))
if (autdet || (!autdet && spot::is_deterministic(aut)))
return are_isomorphic_det(ref_, aut);
}
else

4
spot/twaalgos/complete.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -114,7 +114,7 @@ namespace spot
}
// In case the automaton use state-based acceptance, propagate
// the acceptance of the first edge to the one we add.
if (!aut->prop_state_acc())
if (aut->prop_state_acc() != true)
acc = 0U;
aut->new_edge(i, sink, missingcond, acc);
}

7
spot/twaalgos/dot.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
// et Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -499,7 +499,8 @@ namespace spot
}
if (opt_name_)
name_ = aut_->get_named_prop<std::string>("automaton-name");
mark_states_ = !opt_force_acc_trans_ && aut_->prop_state_acc();
mark_states_ = (!opt_force_acc_trans_
&& aut_->prop_state_acc().is_true());
if (opt_shape_ == ShapeAuto)
{
if (sn_ || sprod_ || aut->num_states() > 100)

13
spot/twaalgos/hoa.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -159,8 +159,8 @@ 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(!aut->prop_deterministic() || deterministic);
assert(!aut->prop_state_acc() || state_acc);
assert(deterministic || aut->prop_deterministic() != true);
assert(state_acc || aut->prop_state_acc() != true);
}
void number_all_ap()
@ -433,16 +433,15 @@ namespace spot
// in the case of deterministic automata.
if (aut->prop_unambiguous() && (verbose || !md.is_deterministic))
prop(" unambiguous");
assert(!(aut->prop_stutter_invariant() && aut->prop_stutter_sensitive()));
if (aut->prop_stutter_invariant())
prop(" stutter-invariant");
if (aut->prop_stutter_sensitive())
if (!aut->prop_stutter_invariant())
prop(" stutter-sensitive");
if (aut->prop_terminal())
prop(" terminal");
if (aut->prop_weak() && (verbose || !aut->prop_terminal()))
if (aut->prop_weak() && (verbose || aut->prop_terminal() != true))
prop(" weak");
if (aut->prop_inherently_weak() && (verbose || !aut->prop_weak()))
if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
prop(" inherently-weak");
os << nl;

9
spot/twaalgos/isdet.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -63,8 +63,9 @@ namespace spot
bool
is_deterministic(const const_twa_graph_ptr& aut)
{
if (aut->prop_deterministic())
return true;
trival d = aut->prop_deterministic();
if (d.is_known())
return d.is_true();
return !count_nondet_states_aux<false>(aut);
}

17
spot/twaalgos/isunamb.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
// Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -27,20 +27,23 @@ namespace spot
{
bool is_unambiguous(const const_twa_graph_ptr& aut)
{
if (aut->prop_unambiguous())
return true;
trival u = aut->prop_unambiguous();
if (u.is_known())
return u.is_true();
auto clean_a = scc_filter_states(aut);
if (clean_a->num_edges() == 0)
return true;
auto prod = product(clean_a, clean_a);
auto clean_p = scc_filter_states(prod);
return clean_a->num_states() == clean_p->num_states()
&& clean_a->num_edges() == clean_p->num_edges();
return (clean_a->num_states() == clean_p->num_states()
&& clean_a->num_edges() == clean_p->num_edges());
}
bool check_unambiguous(const twa_graph_ptr& aut)
{
aut->prop_unambiguous(is_unambiguous(aut));
return aut->prop_unambiguous();
bool u = is_unambiguous(aut);
aut->prop_unambiguous(u);
return u;
}
}

6
spot/twaalgos/lbtt.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2011, 2012, 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.
@ -133,7 +133,7 @@ namespace spot
throw std::runtime_error
("LBTT only supports generalized Büchi acceptance");
bool sba = g->prop_state_acc();
bool sba = g->prop_state_acc().is_true();
if (opt)
switch (char c = *opt++)
{

12
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
@ -2182,16 +2182,18 @@ namespace spot
acc.set_generalized_buchi();
a->prop_inherently_weak(f2.is_syntactic_persistence());
a->prop_stutter_invariant(f2.is_syntactic_stutter_invariant());
if (f2.is_syntactic_persistence())
a->prop_inherently_weak(true);
if (f2.is_syntactic_stutter_invariant())
a->prop_stutter_invariant(true);
if (orig_f.is_syntactic_guarantee())
{
a->prop_terminal(true);
assert(a->num_sets() <= 1);
}
// Currently the unambiguous option work only with LTL.
a->prop_unambiguous(f2.is_ltl_formula() && unambiguous);
if (unambiguous)
a->prop_unambiguous();
// Set the following to true to preserve state names.
a->release_formula_namer(namer, false);

11
spot/twaalgos/postproc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -146,7 +146,8 @@ namespace spot
return a;
// If the automaton is weak, using transition-based acceptance
// won't help, so let's preserve it.
if ((state_based_ || a->prop_inherently_weak()) && a->prop_state_acc())
if ((state_based_ || a->prop_inherently_weak().is_true())
&& a->prop_state_acc().is_true())
return scc_filter_states(a, arg);
else
return scc_filter(a, arg);
@ -253,7 +254,9 @@ namespace spot
{
bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, nullptr, reject_bigger);
if (dba && dba->prop_inherently_weak() && dba->prop_deterministic())
if (dba
&& dba->prop_inherently_weak().is_true()
&& dba->prop_deterministic().is_true())
{
// The WDBA is a BA, so no degeneralization is required.
// We just need to add an acceptance set if there is none.
@ -272,7 +275,7 @@ namespace spot
// at hard levels if we want a small output.
if (!dba || (level_ == High && PREF_ == Small))
{
if (((SBACC_ && a->prop_state_acc())
if (((SBACC_ && a->prop_state_acc().is_true())
|| (type_ == BA && a->is_sba()))
&& !tba_determinisation_)
{

10
spot/twaalgos/remfin.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -227,7 +227,7 @@ namespace spot
res->new_states(nst);
res->set_buchi();
res->set_init_state(aut->get_init_state_number());
bool deterministic = aut->prop_deterministic();
trival deterministic = aut->prop_deterministic();
std::vector<unsigned> state_map(aut->num_states());
for (unsigned n = 0; n < scc_max; ++n)
@ -307,7 +307,7 @@ namespace spot
static twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
{
if (!aut->prop_state_acc())
if (!aut->prop_state_acc().is_true())
return nullptr;
auto code = aut->get_acceptance();
@ -508,7 +508,7 @@ namespace spot
return std::const_pointer_cast<twa_graph>(aut);
// FIXME: we should check whether the automaton is weak.
if (aut->prop_inherently_weak() && is_deterministic(aut))
if (aut->prop_inherently_weak().is_true() && is_deterministic(aut))
return remove_fin_det_weak(aut);
if (auto maybe = streett_to_generalized_buchi_maybe(aut))
@ -668,7 +668,7 @@ namespace spot
res->set_acceptance(aut->num_sets() + extra_sets, new_code);
res->set_init_state(aut->get_init_state_number());
bool sbacc = aut->prop_state_acc();
bool sbacc = aut->prop_state_acc().is_true();
scc_info si(aut);
unsigned nscc = si.scc_count();
std::vector<unsigned> state_map(nst);

37
spot/twaalgos/strength.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@ -84,10 +84,12 @@ namespace spot
delete si;
if (set)
{
if (terminal)
aut->prop_terminal(is_term && is_weak);
aut->prop_weak(is_weak);
aut->prop_inherently_weak(is_inweak);
if (terminal && is_term && is_weak)
aut->prop_terminal(true);
if (is_weak)
aut->prop_weak(true);
if (is_inweak)
aut->prop_inherently_weak(true);
}
if (inweak)
return is_inweak;
@ -98,25 +100,30 @@ namespace spot
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return (aut->prop_terminal() ||
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut),
si));
trival v = aut->prop_terminal();
if (v.is_known())
return v.is_true();
return is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si);
}
bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return (aut->prop_weak() ||
is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut),
si));
trival v = aut->prop_weak();
if (v.is_known())
return v.is_true();
return is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut),
si);
}
bool
is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return (aut->prop_inherently_weak() ||
is_type_automaton<false, true>
(std::const_pointer_cast<twa_graph>(aut), si));
trival v = aut->prop_inherently_weak();
if (v.is_known())
return v.is_true();
return is_type_automaton<false, true>
(std::const_pointer_cast<twa_graph>(aut), si);
}
void check_strength(const twa_graph_ptr& aut, scc_info* si)

15
spot/twaalgos/stutter.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -612,12 +612,12 @@ namespace spot
}
}
bool
trival
check_stutter_invariance(const twa_graph_ptr& aut, formula f)
{
bool is_stut = aut->prop_stutter_invariant();
if (is_stut)
return is_stut;
trival is_stut = aut->prop_stutter_invariant();
if (is_stut.is_known())
return is_stut.is_true();
twa_graph_ptr neg = nullptr;
if (f)
@ -630,14 +630,13 @@ namespace spot
// know how to complement it.
aut->prop_deterministic(is_deterministic(aut));
if (!aut->prop_deterministic())
return false;
return trival::maybe();
neg = remove_fin(dtwa_complement(aut));
}
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
std::move(neg), aut->ap_var());
aut->prop_stutter_invariant(is_stut);
aut->prop_stutter_sensitive(!is_stut);
return is_stut;
}
}

7
spot/twaalgos/stutter.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -63,7 +63,10 @@ namespace spot
/// This procedure only works if \a aut is deterministic, or if the
/// equivalent formula \a f is given. The stutter-invariant property
/// of the automaton is updated and also returned.
SPOT_API bool
///
/// If no formula is given and the automaton is not deterministic,
/// the result will be returned as trival::maybe().
SPOT_API trival
check_stutter_invariance(const twa_graph_ptr& aut,
formula f = nullptr);
}

4
spot/twaalgos/totgba.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -164,7 +164,7 @@ namespace spot
bs2num[s] = out->new_state();
todo.push_back(s);
bool sbacc = in->prop_state_acc();
bool sbacc = in->prop_state_acc().is_true();
// States of the original automaton are marked with s.pend == -1U.
const acc_cond::mark_t orig_copy(-1U);

14
tests/core/ikwiad.cc
View file

@ -1,9 +1,9 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
// Copyright (C) 2007-2016 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003-2007 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.
//
@ -937,7 +937,7 @@ checked_main(int argc, char** argv)
if (nra2nba)
a = spot::to_generalized_buchi(daut->aut);
assume_sba = a->is_sba();
assume_sba = a->is_sba().is_true();
}
else
{
@ -1025,7 +1025,7 @@ checked_main(int argc, char** argv)
if (scc_filter)
{
tm.start("SCC-filter");
if (a->prop_state_acc() & !scc_filter_all)
if (a->prop_state_acc().is_true() & !scc_filter_all)
a = spot::scc_filter_states(ensure_digraph(a));
else
a = spot::scc_filter(ensure_digraph(a), scc_filter_all);

110
tests/python/product.ipynb
View file

@ -1,7 +1,7 @@
{
"metadata": {
"name": "",
"signature": "sha256:50d5adbd44f5981c700cec9133b926c8edb75b3ff80a4cf28e7c26cf918fe04a"
"signature": "sha256:08e64ee189c19ed7e56e5f1c841f51faac25e0bd5e4a6b838856ba8b6f2b5344"
},
"nbformat": 3,
"nbformat_minor": 0,
@ -367,7 +367,7 @@
"output_type": "pyout",
"prompt_number": 2,
"text": [
"<IPython.core.display.HTML at 0x7fc8fd6de160>"
"<IPython.core.display.HTML at 0x7ff45181d390>"
]
}
],
@ -711,7 +711,7 @@
"metadata": {},
"output_type": "display_data",
"text": [
"<IPython.core.display.HTML at 0x7fc8df0b6630>"
"<IPython.core.display.HTML at 0x7ff444140860>"
]
}
],
@ -1066,7 +1066,7 @@
"metadata": {},
"output_type": "display_data",
"text": [
"<IPython.core.display.HTML at 0x7fc8df07bf28>"
"<IPython.core.display.HTML at 0x7ff451801208>"
]
}
],
@ -1076,7 +1076,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"Besides the obvious lack of acceptance condition (which defaults to `t`) and acceptance sets, there is a less obvious problem: we never declared the set of atomic proposition used by the result automaton. This as two consequences:\n",
"Besides the obvious lack of acceptance condition (which defaults to `t`) and acceptance sets, there is a less obvious problem: we never declared the set of atomic propositions used by the result automaton. This as two consequences:\n",
"- calling `p1.ap()` will return an empty set of atomic propositions"
]
},
@ -1487,7 +1487,7 @@
"metadata": {},
"output_type": "display_data",
"text": [
"<IPython.core.display.HTML at 0x7fc8df015d68>"
"<IPython.core.display.HTML at 0x7ff44409ef98>"
]
},
{
@ -1533,10 +1533,10 @@
"output_type": "stream",
"stream": "stdout",
"text": [
"True\n",
"True\n",
"True\n",
"False\n"
"yes\n",
"yes\n",
"yes\n",
"maybe\n"
]
}
],
@ -1546,11 +1546,76 @@
"cell_type": "markdown",
"metadata": {},
"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",
"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",
" \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",
" \n",
"at the end of our function. However the question is in fact more general than just determinism: the product of two weak automata is weak, the product of two stutter-invariant automata is stutter-invariant, etc. So when writing an algorithm one should consider which of the [property bits](https://spot.lrde.epita.fr/hoa.html#property-bits) are naturally preserved by the algorithm, and set the relevant bits: this can save time later if the resulting automaton is used as input for another algorithm."
"\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",
"\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: "
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"yes = spot.trival(True)\n",
"no = spot.trival(False)\n",
"maybe = spot.trival_maybe()\n",
"for u in (no, maybe, yes):\n",
" for v in (no, maybe, yes):\n",
" print(\"{u!s:>5} & {v!s:<5} = {r1!s:<5} {u!s:>5} and {v!s:<5} = {r2!s:<5}\"\n",
" .format(u=u, v=v, r1=(u&v), r2=(u and v)))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
" no & no = no no and no = no \n",
" no & maybe = no no and maybe = no \n",
" no & yes = no no and yes = no \n",
"maybe & no = no maybe and no = maybe\n",
"maybe & maybe = maybe maybe and maybe = maybe\n",
"maybe & yes = maybe maybe and yes = maybe\n",
" yes & no = no yes and no = no \n",
" yes & maybe = maybe yes and maybe = maybe\n",
" yes & yes = yes yes and yes = yes \n"
]
}
],
"prompt_number": 8
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The reason `maybe and no` is equal to `maybe` is that Python evaluate it like `no if maybe else maybe`, but when a trival is evaluated in a Boolean context (as in `if maybe`) the result is True only if the trival is equal to yes.\n",
"\n",
"So our\n",
"\n",
" if left.prop_deterministic() and right.prop_deterministic():\n",
" result.prop_deterministic(True)\n",
"\n",
"is OK because the `if` body will only be entered of both input automata are known to be deterministic."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"However the question is in fact more general than just determinism: the product of two weak automata is weak, the product of two stutter-invariant automata is stutter-invariant, etc. So when writing an algorithm one should consider which of the [property bits](https://spot.lrde.epita.fr/hoa.html#property-bits) are naturally preserved by the algorithm, and set the relevant bits: this can save time later if the resulting automaton is used as input for another algorithm."
]
},
{
@ -1598,10 +1663,11 @@
" # Remember the names of our states\n",
" result.set_state_names(names)\n",
" \n",
" # Loop over all the properties we want to preserve if they are in both automata\n",
" # Loop over all the properties we want to preserve if they hold in both automata\n",
" for p in ('prop_deterministic', 'prop_weak', 'prop_inherently_weak', \n",
" 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n",
" getattr(result, p)(getattr(left, p)() and getattr(right, p)())\n",
" if getattr(left, p)() and getattr(right, p)():\n",
" getattr(result, p)(True)\n",
" return result\n",
"\n",
"p3 = product3(a1, a2)\n",
@ -1925,18 +1991,18 @@
"metadata": {},
"output_type": "display_data",
"text": [
"<IPython.core.display.HTML at 0x7fc8df001240>"
"<IPython.core.display.HTML at 0x7ff44408aa58>"
]
},
{
"output_type": "stream",
"stream": "stdout",
"text": [
"True\n"
"yes\n"
]
}
],
"prompt_number": 8
"prompt_number": 9
},
{
"cell_type": "markdown",
@ -1960,11 +2026,11 @@
"output_type": "stream",
"stream": "stdout",
"text": [
"1000 loops, best of 3: 353 \u00b5s per loop\n"
"1000 loops, best of 3: 342 \u00b5s per loop\n"
]
}
],
"prompt_number": 9
"prompt_number": 10
},
{
"cell_type": "code",
@ -1979,11 +2045,11 @@
"output_type": "stream",
"stream": "stdout",
"text": [
"100000 loops, best of 3: 6.39 \u00b5s per loop\n"
"100000 loops, best of 3: 6.44 \u00b5s per loop\n"
]
}
],
"prompt_number": 10
"prompt_number": 11
},
{
"cell_type": "markdown",

4
tests/python/remfin.py
View file

@ -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() == False)
assert(a.prop_unambiguous() == False)
assert(a.prop_deterministic().is_maybe())
assert(a.prop_unambiguous().is_maybe())
assert(a.is_deterministic() == True)
assert(a.is_unambiguous() == True)