From da391492f3702b163a201ca55454d57389fea7a0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 12 Jan 2016 19:37:18 +0100 Subject: [PATCH] twa: store property bits as trivals * 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. --- NEWS | 9 +++ doc/org/hoa.org | 38 +++++----- doc/org/tut21.org | 71 ++++++++----------- spot/parseaut/parseaut.yy | 46 ++++++++----- spot/twa/twa.hh | 118 ++++++++++++++------------------ spot/twaalgos/are_isomorphic.cc | 17 +++-- spot/twaalgos/complete.cc | 4 +- spot/twaalgos/dot.cc | 7 +- spot/twaalgos/hoa.cc | 13 ++-- spot/twaalgos/isdet.cc | 9 +-- spot/twaalgos/isunamb.cc | 17 +++-- spot/twaalgos/lbtt.cc | 6 +- spot/twaalgos/ltl2tgba_fm.cc | 12 ++-- spot/twaalgos/postproc.cc | 11 +-- spot/twaalgos/remfin.cc | 10 +-- spot/twaalgos/strength.cc | 37 ++++++---- spot/twaalgos/stutter.cc | 31 ++++----- spot/twaalgos/stutter.hh | 7 +- spot/twaalgos/totgba.cc | 4 +- tests/core/ikwiad.cc | 14 ++-- tests/python/product.ipynb | 110 +++++++++++++++++++++++------ tests/python/remfin.py | 4 +- 22 files changed, 337 insertions(+), 258 deletions(-) diff --git a/NEWS b/NEWS index bb33b9dc5..a080fe084 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/doc/org/hoa.org b/doc/org/hoa.org index aa441c730..31c589ab5 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -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= | diff --git a/doc/org/tut21.org b/doc/org/tut21.org index a35fd155b..2140063d1 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -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("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 diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index f462e1b3b..899d073f4 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -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(); 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 { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 9d1e58b5c..1605d76c6 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -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 #include #include +#include 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; - } + // deterministic implies unambiguous + 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()); - } + prop_stutter_invariant(other->prop_stutter_invariant()); } 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()); } }; diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc index 751f804a3..774014d5b 100644 --- a/spot/twaalgos/are_isomorphic.cc +++ b/spot/twaalgos/are_isomorphic.cc @@ -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 diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 796273e9e..1c6bfd9b2 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -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); } diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 8eda7698d..1265cc579 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -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("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) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index aee404ea6..b2e7e7c77 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -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; diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 79bb27410..010672900 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -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(aut); } diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 800a42ee1..5e6b59924 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -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; } } diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc index c006210c9..5d368cabe 100644 --- a/spot/twaalgos/lbtt.cc +++ b/spot/twaalgos/lbtt.cc @@ -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++) { diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 0bd5d9ee9..e4fd6014a 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -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); diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index c5246195d..aead169be 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -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_) { diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index a9d5ac824..4b9b44cd3 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -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 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(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 state_map(nst); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 3e29a2fbe..1d9083ac7 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -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(std::const_pointer_cast(aut), - si)); + trival v = aut->prop_terminal(); + if (v.is_known()) + return v.is_true(); + return is_type_automaton(std::const_pointer_cast(aut), si); } bool is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) { - return (aut->prop_weak() || - is_type_automaton(std::const_pointer_cast(aut), - si)); + trival v = aut->prop_weak(); + if (v.is_known()) + return v.is_true(); + return is_type_automaton(std::const_pointer_cast(aut), + si); } bool is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) { - return (aut->prop_inherently_weak() || - is_type_automaton - (std::const_pointer_cast(aut), si)); + trival v = aut->prop_inherently_weak(); + if (v.is_known()) + return v.is_true(); + return is_type_automaton + (std::const_pointer_cast(aut), si); } void check_strength(const twa_graph_ptr& aut, scc_info* si) diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 91bcc3261..fb77b4a45 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -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. // @@ -410,10 +410,10 @@ namespace spot } if (num_states != a->num_states()) a->prop_keep({true, // state_based - false, // inherently_weak - false, // deterministic - false, // stutter inv. - }); + false, // inherently_weak + false, // deterministic + false, // stutter inv. + }); a->merge_edges(); return a; } @@ -430,10 +430,10 @@ namespace spot closure(twa_graph_ptr&& a) { a->prop_keep({false, // state_based - false, // inherently_weak - false, // deterministic - false, // stutter inv. - }); + false, // inherently_weak + false, // deterministic + false, // stutter inv. + }); unsigned n = a->num_states(); std::vector todo; @@ -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; } } diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index cd189ee50..1c4d3d832 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -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); } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 91e45a01a..63cc473f9 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -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); diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index 866957614..dfb6f5de9 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -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); diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index 31cdb4550..320e9d543 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -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": [ - "" + "" ] } ], @@ -711,7 +711,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] } ], @@ -1066,7 +1066,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] } ], @@ -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": [ - "" + "" ] }, { @@ -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": [ - "" + "" ] }, { "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", diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 880d6588b..a87187e45 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -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)