kripke.hh 3 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Feb 15, 2016 2 3 ``````// Copyright (C) 2009, 2010, 2013, 2014, 2016 Laboratoire de Recherche // et 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 `````` `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Alexandre Duret-Lutz committed Jun 02, 2009 21 `````` `````` Alexandre Duret-Lutz committed Dec 04, 2015 22 ``````#include `````` Alexandre Duret-Lutz committed Jun 02, 2009 23 24 25 26 `````` namespace spot { `````` Alexandre Duret-Lutz committed Nov 26, 2010 27 `````` /// \ingroup kripke `````` Alexandre Duret-Lutz committed Jun 08, 2013 28 `````` /// \brief Iterator code for Kripke structure `````` Alexandre Duret-Lutz committed Nov 26, 2010 29 30 31 32 33 34 35 36 37 38 `````` /// /// 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() `````` Alexandre Duret-Lutz committed Oct 28, 2015 39 `````` /// - kripke_succ_iterator::dst() `````` Alexandre Duret-Lutz committed Nov 26, 2010 40 `````` /// `````` Alexandre Duret-Lutz committed Oct 28, 2015 41 42 `````` /// This class implements kripke_succ_iterator::cond(), /// and kripke_succ_iterator::acc(). `````` Alexandre Duret-Lutz committed Apr 22, 2015 43 `````` class SPOT_API kripke_succ_iterator : public twa_succ_iterator `````` Alexandre Duret-Lutz committed Nov 26, 2010 44 45 46 47 48 `````` { public: /// \brief Constructor /// /// The \a cond argument will be the one returned `````` Alexandre Duret-Lutz committed Oct 28, 2015 49 `````` /// by kripke_succ_iterator::cond(). `````` Alexandre Duret-Lutz committed Feb 12, 2014 50 51 52 53 54 55 56 57 58 59 `````` kripke_succ_iterator(const bdd& cond) : cond_(cond) { } void recycle(const bdd& cond) { cond_ = cond; } `````` Alexandre Duret-Lutz committed Nov 26, 2010 60 61 `````` virtual ~kripke_succ_iterator(); `````` Alexandre Duret-Lutz committed Feb 16, 2016 62 63 `````` virtual bdd cond() const override; virtual acc_cond::mark_t acc() const override; `````` Alexandre Duret-Lutz committed Nov 26, 2010 64 65 66 `````` protected: bdd cond_; }; `````` Alexandre Duret-Lutz committed Jun 02, 2009 67 `````` `````` Alexandre Duret-Lutz committed Nov 26, 2010 68 `````` /// \ingroup kripke `````` Alexandre Duret-Lutz committed Jun 08, 2013 69 `````` /// \brief Interface for a Kripke structure `````` Alexandre Duret-Lutz committed Nov 26, 2010 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 `````` /// /// 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() /// /// 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. `````` Alexandre Duret-Lutz committed Jul 29, 2013 90 `````` class SPOT_API kripke: public fair_kripke `````` Alexandre Duret-Lutz committed Jun 02, 2009 91 92 `````` { public: `````` Alexandre Duret-Lutz committed Oct 06, 2014 93 94 95 96 97 `````` kripke(const bdd_dict_ptr& d) : fair_kripke(d) { } `````` Alexandre Duret-Lutz committed Jun 02, 2009 98 99 `````` virtual ~kripke(); `````` Alexandre Duret-Lutz committed Oct 06, 2014 100 `````` virtual acc_cond::mark_t state_acceptance_conditions(const state*) const; `````` Alexandre Duret-Lutz committed Jun 02, 2009 101 `````` }; `````` Alexandre Duret-Lutz committed Aug 15, 2014 102 103 104 `````` typedef std::shared_ptr kripke_ptr; typedef std::shared_ptr const_kripke_ptr; `````` Alexandre Duret-Lutz committed Jun 02, 2009 105 ``}``