1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de 3 // Recherche et Développement de l'Epita (LRDE). 4 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de 5 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), 6 // Université Pierre et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 #pragma once 24 25 #include <spot/tl/formula.hh> 26 #include <spot/twa/twagraph.hh> 27 #include <spot/tl/apcollect.hh> 28 #include <spot/tl/simplify.hh> 29 #include <spot/twaalgos/powerset.hh> 30 31 namespace spot 32 { 33 /// \ingroup twa_ltl 34 /// \brief Build a spot::twa_graph_ptr from an LTL or PSL formula. 35 /// 36 /// This originally derived from an algorithm by Couvreur 37 /// \cite couvreur.99.fm , but it has been improved in many 38 /// ways \cite duret.14.ijccbs . 39 /// 40 /// \param f The formula to translate into an automaton. 41 /// 42 /// \param dict The spot::bdd_dict the constructed automata should use. 43 /// 44 /// \param exprop When set, the algorithm will consider all properties 45 /// combinations possible on each state, in an attempt to reduce 46 /// the non-determinism. The automaton will have the same size as 47 /// without this option, but because the transitions will be more 48 /// deterministic, the product automaton will be smaller (or, at worse, 49 /// equal). 50 /// 51 /// \param symb_merge When false, states with the same symbolic 52 /// representation (these are equivalent formulae) will not be 53 /// merged. 54 /// 55 /// \param branching_postponement When set, several transitions leaving 56 /// from the same state with the same label (i.e., condition + acceptance 57 /// conditions) will be merged. \cite sebastiani.03.charme 58 /// 59 /// \param fair_loop_approx When set, a really simple characterization of 60 /// unstable state is used to suppress all acceptance conditions from 61 /// incoming transitions. 62 /// 63 /// \param unobs When non-zero, the atomic propositions in the LTL formula 64 /// are interpreted as events that exclude each other. The events in the 65 /// formula are observable events, and \c unobs can be filled with 66 /// additional unobservable events. 67 /// 68 /// \param simplifier If this parameter is set, the LTL formulae 69 /// representing each state of the automaton will be simplified 70 /// before computing the successor. \a simpl should be configured 71 /// for the type of reduction you want, see spot::tl_simplifier. 72 /// This idea is taken from \cite thirioux.02.fmics . 73 /// 74 /// \param unambiguous When true, unambigous TGBA will be produced 75 /// using the trick described in \cite benedikt.13.tacas . 76 /// 77 /// \param aborter When given, aborts the construction whenever the 78 /// constructed automaton would become larger than specified by the 79 /// output_aborter. 80 /// 81 /// \return A spot::twa_graph that recognizes the language of \a f. 82 SPOT_API twa_graph_ptr 83 ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict, 84 bool exprop = false, bool symb_merge = true, 85 bool branching_postponement = false, 86 bool fair_loop_approx = false, 87 const atomic_prop_set* unobs = nullptr, 88 tl_simplifier* simplifier = nullptr, 89 bool unambiguous = false, 90 const output_aborter* aborter = nullptr); 91 } 92