fairkripke.hh 3.55 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Feb 17, 2014 2 ``````// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et `````` Alexandre Duret-Lutz committed Jul 29, 2013 3 ``````// Developpement de l'Epita `````` Alexandre Duret-Lutz committed Jun 02, 2009 4 5 6 7 8 ``````// // This file is part of Spot, a model checking library. // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by `````` Alexandre Duret-Lutz committed Oct 12, 2012 9 ``````// the Free Software Foundation; either version 3 of the License, or `````` Alexandre Duret-Lutz committed Jun 02, 2009 10 11 12 13 14 15 16 17 ``````// (at your option) any later version. // // Spot is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public // License for more details. // // You should have received a copy of the GNU General Public License `````` Alexandre Duret-Lutz committed Oct 12, 2012 18 ``````// along with this program. If not, see . `````` Alexandre Duret-Lutz committed Jun 02, 2009 19 20 21 22 23 `````` #ifndef SPOT_KRIPKE_FAIRKRIPKE_HH # define SPOT_KRIPKE_FAIRKRIPKE_HH #include "tgba/tgba.hh" `````` Alexandre Duret-Lutz committed Aug 15, 2014 24 ``````#include "fwd.hh" `````` Alexandre Duret-Lutz committed Jun 02, 2009 25 `````` `````` Alexandre Duret-Lutz committed Nov 26, 2010 26 27 28 ``````/// \addtogroup kripke Kripke Structures /// \ingroup tgba `````` Alexandre Duret-Lutz committed Jun 02, 2009 29 30 ``````namespace spot { `````` Alexandre Duret-Lutz committed Nov 26, 2010 31 `````` /// \ingroup kripke `````` Alexandre Duret-Lutz committed Jun 08, 2013 32 `````` /// \brief Iterator code for a Fair Kripke structure. `````` Alexandre Duret-Lutz committed Nov 26, 2010 33 34 35 36 37 38 39 40 41 42 43 44 45 46 `````` /// /// 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(). `````` Alexandre Duret-Lutz committed Jul 29, 2013 47 `````` class SPOT_API fair_kripke_succ_iterator : public tgba_succ_iterator `````` Alexandre Duret-Lutz committed Jun 02, 2009 48 49 `````` { public: `````` Alexandre Duret-Lutz committed Nov 26, 2010 50 51 52 53 54 55 `````` /// \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); `````` Alexandre Duret-Lutz committed Jun 02, 2009 56 57 `````` virtual ~fair_kripke_succ_iterator(); `````` Alexandre Duret-Lutz committed Nov 26, 2010 58 `````` virtual bdd current_condition() const; `````` Alexandre Duret-Lutz committed Jun 02, 2009 59 60 `````` virtual bdd current_acceptance_conditions() const; protected: `````` Alexandre Duret-Lutz committed Nov 26, 2010 61 62 `````` bdd cond_; bdd acc_cond_; `````` Alexandre Duret-Lutz committed Jun 02, 2009 63 64 `````` }; `````` Alexandre Duret-Lutz committed Nov 26, 2010 65 `````` /// \ingroup kripke `````` Alexandre Duret-Lutz committed Jun 08, 2013 66 `````` /// \brief Interface for a Fair Kripke structure. `````` Alexandre Duret-Lutz committed Nov 26, 2010 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 `````` /// /// 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. `````` Alexandre Duret-Lutz committed Jul 29, 2013 89 `````` class SPOT_API fair_kripke : public tgba `````` Alexandre Duret-Lutz committed Jun 02, 2009 90 91 `````` { public: `````` Alexandre Duret-Lutz committed Nov 26, 2010 92 93 94 95 96 97 98 99 `````` /// \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; `````` Alexandre Duret-Lutz committed Jun 02, 2009 100 101 102 103 104 105 106 107 `````` protected: virtual bdd compute_support_conditions(const state* s) const; }; } #endif // SPOT_KRIPKE_FAIRKRIPKE_HH``````