apcollect.hh 2.21 KB
 Alexandre Duret-Lutz committed May 02, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Jan 03, 2015 2 ``````// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et `````` Alexandre Duret-Lutz committed Feb 06, 2014 3 ``````// Développement de l'Epita (LRDE). `````` 4 ``````// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed May 02, 2012 5 ``````// département Systèmes Répartis Coopératifs (SRC), Université Pierre `````` Alexandre Duret-Lutz committed Aug 09, 2004 6 7 8 9 10 11 ``````// et Marie Curie. // // 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 12 ``````// the Free Software Foundation; either version 3 of the License, or `````` Alexandre Duret-Lutz committed Aug 09, 2004 13 14 15 16 17 18 19 20 ``````// (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 21 ``````// along with this program. If not, see . `````` Alexandre Duret-Lutz committed Aug 09, 2004 22 `````` `````` Etienne Renault committed Mar 23, 2015 23 ``````#pragma once `````` Alexandre Duret-Lutz committed Aug 09, 2004 24 `````` `````` Alexandre Duret-Lutz committed Sep 28, 2015 25 ``````#include "formula.hh" `````` Alexandre Duret-Lutz committed Jul 29, 2013 26 ``````#include `````` Alexandre Duret-Lutz committed Oct 30, 2014 27 ``````#include `````` Alexandre Duret-Lutz committed Apr 22, 2015 28 ``````#include "twa/fwd.hh" `````` Alexandre Duret-Lutz committed Aug 09, 2004 29 30 31 `````` namespace spot { `````` Alexandre Duret-Lutz committed Sep 29, 2015 32 `````` /// \addtogroup tl_misc `````` Alexandre Duret-Lutz committed Sep 28, 2015 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 `````` /// @{ /// Set of atomic propositions. typedef std::set atomic_prop_set; /// \brief construct an atomic_prop_set with n propositions SPOT_API atomic_prop_set create_atomic_prop_set(unsigned n); /// \brief Return the set of atomic propositions occurring in a formula. /// /// \param f the formula to inspect /// \param s an existing set to fill with atomic_propositions discovered, /// or 0 if the set should be allocated by the function. /// \return A pointer to the supplied set, \c s, augmented with /// atomic propositions occurring in \c f; or a newly allocated /// set containing all these atomic propositions if \c s is 0. SPOT_API atomic_prop_set* atomic_prop_collect(formula f, atomic_prop_set* s = nullptr); /// \brief Return the set of atomic propositions occurring in a /// formula, as a BDD. /// /// \param f the formula to inspect /// \param a that automaton that should register the BDD variables used. /// \return A conjunction the atomic propositions. SPOT_API bdd atomic_prop_collect_as_bdd(formula f, const twa_ptr& a); /// @} `````` Alexandre Duret-Lutz committed Aug 09, 2004 63 ``}``