randomgraph.hh 4.09 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Mar 31, 2015 2 ``````// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et `````` Alexandre Duret-Lutz committed Aug 13, 2014 3 ``````// Développement de l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Feb 02, 2005 4 ``````// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed Jul 29, 2013 5 ``````// département Systèmes Répartis Coopératifs (SRC), Université Pierre `````` Alexandre Duret-Lutz committed Nov 12, 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 Nov 12, 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 Nov 12, 2004 22 `````` `````` Etienne Renault committed Mar 23, 2015 23 ``````#pragma once `````` Alexandre Duret-Lutz committed Nov 12, 2004 24 25 26 `````` #include "ltlvisit/apcollect.hh" #include "ltlenv/defaultenv.hh" `````` Alexandre Duret-Lutz committed Apr 22, 2015 27 28 ``````#include "twa/bdddict.hh" #include "twa/acc.hh" `````` Alexandre Duret-Lutz committed Nov 12, 2004 29 30 31 `````` namespace spot { `````` Alexandre Duret-Lutz committed Apr 22, 2015 32 `````` /// \ingroup twa_misc `````` Alexandre Duret-Lutz committed Jun 08, 2013 33 `````` /// \brief Construct a tgba randomly. `````` Alexandre Duret-Lutz committed Nov 12, 2004 34 `````` /// `````` Alexandre Duret-Lutz committed Feb 02, 2005 35 `````` /// \param n The number of states wanted in the automata (>0). All states `````` Alexandre Duret-Lutz committed Nov 12, 2004 36 37 38 39 40 41 42 43 `````` /// will be connected, and there will be no dead state. /// \param d The density of the automata. This is the probability /// (between 0.0 and 1.0), to add a transition between two /// states. All states have at least one outgoing transition, /// so \a d is considered only when adding the remaining transition. /// A density of 1 means all states will be connected to each other. /// \param ap The list of atomic property that should label the transition. /// \param dict The bdd_dict to used for this automata. `````` Alexandre Duret-Lutz committed Oct 06, 2014 44 `````` /// \param n_accs The number of acceptance sets to use. `````` Alexandre Duret-Lutz committed Nov 23, 2011 45 46 47 `````` /// If this number is non null, then there is no guarantee /// that the generated graph contains an accepting cycle (raise /// the value of \a a to improve the chances). `````` Alexandre Duret-Lutz committed Nov 12, 2004 48 49 50 51 `````` /// \param a The probability (between 0.0 and 1.0) that a transition belongs /// to an acceptance set. /// \param t The probability (between 0.0 and 1.0) that an atomic proposition /// is true. `````` Alexandre Duret-Lutz committed Nov 29, 2014 52 53 `````` /// \param deterministic build a complete and deterministic automaton /// \param state_acc build an automaton with state-based acceptance `````` Alexandre Duret-Lutz committed Jun 01, 2015 54 55 `````` /// \param colored build an automaton in which each transition (or state) /// belongs to a single acceptance set. `````` Alexandre Duret-Lutz committed Nov 12, 2004 56 57 `````` /// /// This algorithms is adapted from the one in Fig 6.2 page 48 of `````` Alexandre Duret-Lutz committed Jun 09, 2013 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 `````` /** \verbatim @TechReport{ tauriainen.00.a66, author = {Heikki Tauriainen}, title = {Automated Testing of {B\"u}chi Automata Translators for {L}inear {T}emporal {L}ogic}, address = {Espoo, Finland}, institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science}, number = {A66}, year = {2000}, url = {http://citeseer.nj.nec.com/tauriainen00automated.html}, type = {Research Report}, note = {Reprint of Master's thesis} } \endverbatim */ `````` Alexandre Duret-Lutz committed Dec 08, 2004 73 `````` /// `````` Alexandre Duret-Lutz committed Sep 27, 2013 74 75 `````` /// Although the intent is similar, there are some differences /// between the above published algorithm and this implementation. `````` Alexandre Duret-Lutz committed Dec 08, 2004 76 77 78 79 80 81 `````` /// First labels are on transitions, and acceptance conditions are /// generated too. Second, the number of successors of a node is /// chosen in \f\$[1,n]\f\$ following a normal distribution with mean /// \f\$1+(n-1)d\f\$ and variance \f\$(n-1)d(1-d)\f\$. (This is less /// accurate, but faster than considering all possible \a n /// successors one by one.) `````` Alexandre Duret-Lutz committed Apr 22, 2015 82 `````` SPOT_API twa_graph_ptr `````` Alexandre Duret-Lutz committed Nov 12, 2004 83 `````` random_graph(int n, float d, `````` Alexandre Duret-Lutz committed Aug 15, 2014 84 `````` const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, `````` Thibaud Michaud committed Nov 14, 2014 85 `````` unsigned n_accs = 0, float a = 0.1, float t = 0.5, `````` Alexandre Duret-Lutz committed Jun 01, 2015 86 87 `````` bool deterministic = false, bool state_acc = false, bool colored = false); `````` Alexandre Duret-Lutz committed Mar 31, 2015 88 89 90 `````` /// Build a random acceptance where each acceptance sets is used once. SPOT_API acc_cond::acc_code random_acceptance(unsigned n_accs); `````` Alexandre Duret-Lutz committed Nov 12, 2004 91 ``}``