diff --git a/ChangeLog b/ChangeLog index da9a9cac6..0ead8e6e8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-11-26 Alexandre Duret-Lutz + + Finalize Kripke interface. + + * src/kripke/fairkripke.hh, src/kripke/fairkripke.cc, + * src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and + document the Kripke interface. I have tested it by updating + checkpn to use it. + 2010-11-25 Alexandre Duret-Lutz Never claim output used to print the degeneralized automaton diff --git a/src/kripke/fairkripke.cc b/src/kripke/fairkripke.cc index 9b28daff5..fd5c7fadd 100644 --- a/src/kripke/fairkripke.cc +++ b/src/kripke/fairkripke.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement +// de l'Epita // // This file is part of Spot, a model checking library. // @@ -22,10 +23,9 @@ namespace spot { - fair_kripke_succ_iterator::fair_kripke_succ_iterator(const fair_kripke* aut, - const state* st) - : cond(aut->conditions_of_state(st)), - acc_cond(aut->acceptance_conditions_of_state(st)) + fair_kripke_succ_iterator::fair_kripke_succ_iterator(const bdd& cond, + const bdd& acc_cond) + : cond_(cond), acc_cond_(acc_cond) { } @@ -34,26 +34,31 @@ namespace spot } bdd - fair_kripke_succ_iterator::current_conditions() const + fair_kripke_succ_iterator::current_condition() const { - return cond; + // Do not assert(!done()) here. It is OK to call + // this function on a state without successor. + return cond_; } bdd fair_kripke_succ_iterator::current_acceptance_conditions() const { - return acc_cond; + // Do not assert(!done()) here. It is OK to call + // this function on a state without successor. + return acc_cond_; } bdd fair_kripke::compute_support_conditions(const state* s) const { - return conditions_of_state(s); + return state_condition(s); } bdd fair_kripke::compute_support_variables(const state* s) const { - return bdd_support(conditions_of_state(s)); + return bdd_support(state_condition(s)); } + } diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 9ac67903d..36ae31a3f 100644 --- a/src/kripke/fairkripke.hh +++ b/src/kripke/fairkripke.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -23,34 +23,82 @@ #include "tgba/tgba.hh" #include "tgba/succiter.hh" +/// \addtogroup kripke Kripke Structures +/// \ingroup tgba + namespace spot { class fair_kripke; + /// \brief Iterator code for a Fair Kripke structure. + /// \ingroup kripke + /// + /// This iterator can be used to simplify the writing + /// of an iterator on a Fair Kripke structure (or lookalike). + /// + /// If you inherit from this iterator, you should only + /// redefine + /// + /// - fair_kripke_succ_iterator::first() + /// - fair_kripke_succ_iterator::next() + /// - fair_kripke_succ_iterator::done() + /// - fair_kripke_succ_iterator::current_state() + /// + /// This class implements fair_kripke_succ_iterator::current_condition(), + /// and fair_kripke_succ_iterator::current_acceptance_conditions(). class fair_kripke_succ_iterator : public tgba_succ_iterator { public: - fair_kripke_succ_iterator(const fair_kripke* aut, const state* st); + /// \brief Constructor + /// + /// The \a cond and \a acc_cond arguments will be those returned + /// by fair_kripke_succ_iterator::current_condition(), + /// and fair_kripke_succ_iterator::current_acceptance_conditions(). + fair_kripke_succ_iterator(const bdd& cond, const bdd& acc_cond); virtual ~fair_kripke_succ_iterator(); - virtual bdd current_conditions() const; + virtual bdd current_condition() const; virtual bdd current_acceptance_conditions() const; protected: - bdd cond; - bdd acc_cond; + bdd cond_; + bdd acc_cond_; }; + /// \brief Interface for a Fair Kripke structure. + /// \ingroup kripke + /// + /// A Kripke structure is a graph in which each node (=state) is + /// labeled by a conjunction of atomic proposition, and a set of + /// acceptance conditions. + /// + /// Such a structure can be seen as spot::tgba by pushing all labels + /// to the outgoing transitions. + /// + /// A programmer that develops an instance of Fair Kripke structure + /// needs just provide an implementation for the following methods: + /// + /// - kripke::get_init_state() + /// - kripke::succ_iter() + /// - kripke::state_condition() + /// - kripke::state_acceptance_conditions() + /// - kripke::format_state() + /// - and optionally kripke::transition_annotation() + /// + /// The other methods of the tgba interface are supplied by this + /// class and need not be defined. + /// + /// See also spot::fair_kripke_succ_iterator. class fair_kripke : public tgba { public: - virtual bdd conditions_of_state(const state* s) const = 0; - virtual bdd acceptance_conditions_of_state(const state* s) const = 0; - virtual fair_kripke_succ_iterator* kripke_succ_iter(const state* s) = 0; + /// \brief The condition that label the state \a s. + /// + /// This should be a conjunction of atomic propositions. + virtual bdd state_condition(const state* s) const = 0; + + /// \brief The set of acceptance conditions that label the state \a s. + virtual bdd state_acceptance_conditions(const state* s) const = 0; - virtual fair_kripke_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0); protected: virtual bdd compute_support_conditions(const state* s) const; virtual bdd compute_support_variables(const state* s) const; diff --git a/src/kripke/kripke.cc b/src/kripke/kripke.cc index bdb4f0eaf..58854f222 100644 --- a/src/kripke/kripke.cc +++ b/src/kripke/kripke.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -22,12 +22,41 @@ namespace spot { - bdd kripke::acceptance_conditions_of_state(const state*) const + kripke_succ_iterator::kripke_succ_iterator(const bdd& cond) + : cond_(cond) { - // There is no acceptance conditions. + } + + kripke_succ_iterator::~kripke_succ_iterator() + { + } + + bdd + kripke_succ_iterator::current_condition() const + { + // Do not assert(!done()) here. It is OK to call + // this function on a state without successor. + return cond_; + } + + bdd + kripke_succ_iterator::current_acceptance_conditions() const + { + // Do not assert(!done()) here. It is OK to call + // this function on a state without successor. return bddfalse; } + kripke::~kripke() + { + } + + bdd + kripke::state_acceptance_conditions(const state*) const + { + return bddtrue; + } + bdd kripke::all_acceptance_conditions() const { // There is no acceptance conditions. diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh index e74df560e..49c3ee605 100644 --- a/src/kripke/kripke.hh +++ b/src/kripke/kripke.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -25,14 +25,67 @@ namespace spot { - typedef fair_kripke_succ_iterator kripke_succ_iterator; + /// \brief Iterator code for Kripke structure + /// \ingroup kripke + /// + /// This iterator can be used to simplify the writing + /// of an iterator on a Kripke structure (or lookalike). + /// + /// If you inherit from this iterator, you should only + /// redefine + /// + /// - kripke_succ_iterator::first() + /// - kripke_succ_iterator::next() + /// - kripke_succ_iterator::done() + /// - kripke_succ_iterator::current_state() + /// + /// This class implements kripke_succ_iterator::current_condition(), + /// and kripke_succ_iterator::current_acceptance_conditions(). + class kripke_succ_iterator : public tgba_succ_iterator + { + public: + /// \brief Constructor + /// + /// The \a cond argument will be the one returned + /// by kripke_succ_iterator::current_condition(). + kripke_succ_iterator(const bdd& cond); + virtual ~kripke_succ_iterator(); + virtual bdd current_condition() const; + virtual bdd current_acceptance_conditions() const; + protected: + bdd cond_; + }; + + /// \brief Interface for a Kripke structure + /// \ingroup kripke + /// + /// A Kripke structure is a graph in which each node (=state) is + /// labeled by a conjunction of atomic proposition. + /// + /// Such a structure can be seen as spot::tgba without + /// any acceptance condition. + /// + /// A programmer that develops an instance of Kripke structure needs + /// just provide an implementation for the following methods: + /// + /// - kripke::get_init_state() + /// - kripke::succ_iter() + /// - kripke::state_condition() + /// - kripke::format_state() + /// - and optionally kripke::transition_annotation() + /// + /// The other methods of the tgba interface (like those dealing with + /// acceptance conditions) are supplied by this kripke class and + /// need not be defined. + /// + /// See also spot::kripke_succ_iterator. class kripke: public fair_kripke { public: virtual ~kripke(); - virtual bdd acceptance_conditions_of_state(const state* s) const; + virtual bdd state_acceptance_conditions(const state*) const; virtual bdd neg_acceptance_conditions() const; virtual bdd all_acceptance_conditions() const; };