spot 2.10.6.dev
public.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2022 Laboratoire de Recherche et
3// Développement de l'Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <spot/twa/twagraph.hh>
23#include <spot/kripke/kripkegraph.hh>
24#include <spot/misc/location.hh>
25#include <spot/tl/defaultenv.hh>
26#include <string>
27#include <list>
28#include <utility>
29#include <iosfwd>
30#include <spot/misc/bitvect.hh>
31
32namespace spot
33{
36
37#ifndef SWIG
39 typedef std::pair<spot::location, std::string> parse_aut_error;
41 typedef std::list<parse_aut_error> parse_aut_error_list;
42#else
43 // Turn parse_aut_error_list into an opaque type for Swig.
44 struct parse_aut_error_list {};
45#endif
46
47 enum class parsed_aut_type {
48 HOA,
49 NeverClaim,
50 LBTT,
51 DRA, /* DSTAR format for Rabin */
52 DSA, /* DSTAR format for Streett */
53 PGAME, /* PG Solver Game */
54 Unknown };
55
57 struct SPOT_API parsed_aut final
58 {
65 twa_graph_ptr aut;
70 kripke_graph_ptr ks;
71
73 bool aborted = false;
75 spot::location loc;
77 parsed_aut_type type = parsed_aut_type::Unknown;
79 std::string filename;
85
86 parsed_aut(const std::string& str)
87 : filename(str)
88 {
89 }
93 bool format_errors(std::ostream& os);
94 };
95
96 typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
97 typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
98
100 {
101 bool ignore_abort = false;
102 bool debug = false;
103 bool trust_hoa = true;
104 bool raise_errors = false;
105 bool want_kripke = false;
106 };
107
133 class SPOT_API automaton_stream_parser final
134 {
135 spot::location last_loc;
136 std::string filename_;
138 void* scanner_;
139 public:
144 automaton_stream_parser(const std::string& filename,
145 automaton_parser_options opts = {});
146
154 automaton_stream_parser(int fd, const std::string& filename,
155 automaton_parser_options opts = {});
156
162 automaton_stream_parser(const char* data,
163 const std::string& filename,
164 automaton_parser_options opts = {});
165
167
183 parsed_aut_ptr parse(const bdd_dict_ptr& dict,
184 environment& env =
186 };
187
204 SPOT_API parsed_aut_ptr
205 parse_aut(const std::string& filename,
206 const bdd_dict_ptr& dict,
208 automaton_parser_options opts = {});
210}
Parse a stream of automata.
Definition: public.hh:134
automaton_stream_parser(int fd, const std::string &filename, automaton_parser_options opts={})
Parse from an already opened file descriptor.
automaton_stream_parser(const std::string &filename, automaton_parser_options opts={})
Parse from a file.
parsed_aut_ptr parse(const bdd_dict_ptr &dict, environment &env=default_environment::instance())
Parse the next automaton in the stream.
automaton_stream_parser(const char *data, const std::string &filename, automaton_parser_options opts={})
Parse from a buffer.
static default_environment & instance()
Get the sole instance of spot::default_environment.
An environment that describes atomic propositions.
Definition: environment.hh:33
std::list< parse_aut_error > parse_aut_error_list
A list of parser diagnostics, as filled by parse.
Definition: public.hh:41
parsed_aut_ptr parse_aut(const std::string &filename, const bdd_dict_ptr &dict, environment &env=default_environment::instance(), automaton_parser_options opts={})
Read the first spot::twa_graph from a file.
std::pair< spot::location, std::string > parse_aut_error
A parse diagnostic with its location.
Definition: public.hh:39
Definition: automata.hh:27
Definition: public.hh:100
bool trust_hoa
Trust properties in HOA files.
Definition: public.hh:103
bool debug
Run the parser in debug mode?
Definition: public.hh:102
bool want_kripke
Parse as a Kripke structure.
Definition: public.hh:105
bool ignore_abort
Skip aborted automata.
Definition: public.hh:101
bool raise_errors
Raise errors as exceptions.
Definition: public.hh:104
Result of the automaton parser.
Definition: public.hh:58
spot::location loc
Location of the automaton in the stream.
Definition: public.hh:75
kripke_graph_ptr ks
The parsed kripke structure.
Definition: public.hh:70
bool format_errors(std::ostream &os)
Format diagnostics produced by spot::parse_aut.
parse_aut_error_list errors
Syntax errors that occurred during parsing.
Definition: public.hh:84
std::string filename
Name of the stream (used for displaying syntax errors)
Definition: public.hh:79
twa_graph_ptr aut
The parsed automaton.
Definition: public.hh:65

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4