public.hh 5.34 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#ifndef SPOT_DSTARPARSE_PUBLIC_HH
# define SPOT_DSTARPARSE_PUBLIC_HH

23
# include "tgba/tgbagraph.hh"
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
# include "misc/location.hh"
# include "ltlenv/defaultenv.hh"
# include <string>
# include <list>
# include <utility>
# include <iosfwd>
# include <misc/bitvect.hh>

namespace spot
{
  /// \addtogroup tgba_io
  /// @{

  /// \brief A parse diagnostic with its location.
  typedef std::pair<spot::location, std::string> dstar_parse_error;
  /// \brief A list of parser diagnostics, as filled by parse.
  typedef std::list<dstar_parse_error> dstar_parse_error_list;

  enum dstar_type { Rabin, Streett };

  /// \brief Temporary encoding of an omega automaton produced by
  /// ltl2dstar.
  struct SPOT_API dstar_aut
  {
    // Transition structure of the automaton.
    // This is encoded as a TGBA without acceptance condition.
50
    tgba_digraph* aut;
51
52
53
54
55
56
57
    /// Type of the acceptance.
    dstar_type type;
    /// Number of acceptance pairs.
    size_t accpair_count;
    /// \brief acceptance sets encoded as 2*num_state bit-vectors of
    /// num_pairs bits
    ///
58
59
60
    /// Assuming F={(L₀,U₀),…,(Lᵢ,Uᵢ),…},
    /// s∈Lᵢ iff <code>accsets->at(s * 2).get(i)</code>,
    /// s∈Uᵢ iff <code>accsets->at(s * 2 + 1).get(i)</code>.
61
62
63
64
65
66
67
68
69
70
    bitvect_array* accsets;

    ~dstar_aut()
    {
      delete aut;
      delete accsets;
    }
  };


71
  /// \brief Build a spot::tgba_digraph from ltl2dstar's output.
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
  /// \param filename The name of the file to parse.
  /// \param error_list A list that will be filled with
  ///        parse errors that occured during parsing.
  /// \param dict The BDD dictionary where to use.
  /// \param env The environment of atomic proposition into which parsing
  ///        should take place.
  /// \param debug When true, causes the parser to trace its execution.
  /// \return A pointer to the tgba built from \a filename, or
  ///        0 if the file could not be opened.
  ///
  /// Note that the parser usually tries to recover from errors.  It can
  /// return an non zero value even if it encountered error during the
  /// parsing of \a filename.  If you want to make sure \a filename
  /// was parsed succesfully, check \a error_list for emptiness.
  ///
  /// \warning This function is not reentrant.
  SPOT_API dstar_aut*
  dstar_parse(const std::string& filename,
	      dstar_parse_error_list& error_list,
	      bdd_dict* dict,
	      ltl::environment& env = ltl::default_environment::instance(),
	      bool debug = false);

  /// \brief Format diagnostics produced by spot::dstar_parse.
  /// \param os Where diagnostics should be output.
  /// \param filename The filename that should appear in the diagnostics.
  /// \param error_list The error list filled by spot::ltl::parse while
  ///        parsing \a ltl_string.
  /// \return \c true iff any diagnostic was output.
  SPOT_API bool
  format_dstar_parse_errors(std::ostream& os,
			    const std::string& filename,
			    dstar_parse_error_list& error_list);


  /// \brief Convert a non-deterministic Rabin automaton into a
  /// non-deterministic Büchi automaton.
109
  SPOT_API tgba_digraph*
110
111
112
113
114
115
  nra_to_nba(const dstar_aut* nra);

  /// \brief Convert a non-deterministic Rabin automaton into a
  /// non-deterministic Büchi automaton.
  ///
  /// This version simply ignores all states in \a ignore.
116
  SPOT_API tgba_digraph*
117
118
119
  nra_to_nba(const dstar_aut* nra, const state_set* ignore);

  /// \brief Convert a deterministic Rabin automaton into a
120
  /// Büchi automaton, deterministic when possible.
121
122
123
  ///
  /// See "Deterministic ω-automata vis-a-vis Deterministic Büchi
  /// Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for
124
  /// more details about a DRA->DBA construction.
125
  ///
126
127
128
129
130
131
132
133
134
  /// We essentially apply this method SCC-wise.  If an SCC is
  /// DBA-realizable, we duplicate it in the output, fixing just
  /// the acceptance states.   If an SCC is not DBA-realizable,
  /// then we apply the more usual conversion from Rabin to NBA
  /// for this part.
  ///
  /// If the optional \a dba_output argument is non-null, the
  /// pointed Boolean will be updated to indicate whether the
  /// returned Büchi automaton is deterministic.
135
  SPOT_API tgba_digraph*
136
  dra_to_ba(const dstar_aut* dra, bool* dba_output = 0);
137
138
139

  /// \brief Convert a non-deterministic Streett automaton into a
  /// non-deterministic tgba.
140
  SPOT_API tgba_digraph*
141
142
143
144
  nsa_to_tgba(const dstar_aut* nra);

  /// \brief Convert a Rabin or Streett automaton into a TGBA.
  ///
145
  /// This function calls dra_to_ba() or nsa_to_tgba().
146
  SPOT_API tgba_digraph*
147
148
  dstar_to_tgba(const dstar_aut* dstar);

149
150
151
152
153

  /// @}
}

#endif // SPOT_DSTARPARSE_PUBLIC_HH