public.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// 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/>.
 
#pragma once
 
#include <spot/twa/twagraph.hh>
#include <spot/kripke/kripkegraph.hh>
#include <spot/misc/location.hh>
#include <spot/tl/defaultenv.hh>
#include <string>
#include <list>
#include <utility>
#include <iosfwd>
#include <spot/misc/bitvect.hh>
 
namespace spot
{
 
#ifndef SWIG
  typedef std::pair<spot::location, std::string> parse_aut_error;
  typedef std::list<parse_aut_error> parse_aut_error_list;
#else
    // Turn parse_aut_error_list into an opaque type for Swig.
  struct parse_aut_error_list {};
#endif
 
  enum class parsed_aut_type {
    HOA,
    NeverClaim,
    LBTT,
    DRA, /* DSTAR format for Rabin */
    DSA, /* DSTAR format for Streett */
    PGAME, /* PG Solver Game */
    Unknown };
 
  struct SPOT_API parsed_aut final
  {
    twa_graph_ptr aut;
    kripke_graph_ptr ks;
 
    bool aborted = false;
    spot::location loc;
    parsed_aut_type type = parsed_aut_type::Unknown;
    std::string filename;
    parse_aut_error_list errors;
 
    parsed_aut(const std::string& str)
      : filename(str)
    {
    }
    bool format_errors(std::ostream& os);
  };
 
  typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
  typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
 
  struct automaton_parser_options final
  {
    bool ignore_abort = false;  
    bool debug = false;         
    bool trust_hoa = true;      
    bool raise_errors = false;  
    bool want_kripke = false;   
  };
 
  class SPOT_API automaton_stream_parser final
  {
    spot::location last_loc;
    std::string filename_;
    automaton_parser_options opts_;
    void* scanner_;
  public:
    automaton_stream_parser(const std::string& filename,
                            automaton_parser_options opts = {});
 
    automaton_stream_parser(int fd, const std::string& filename,
                            automaton_parser_options opts = {});
 
    automaton_stream_parser(const char* data,
                            const std::string& filename,
                            automaton_parser_options opts = {});
 
    ~automaton_stream_parser();
 
    parsed_aut_ptr parse(const bdd_dict_ptr& dict,
                         environment& env =
                         default_environment::instance());
  };
 
  SPOT_API parsed_aut_ptr
  parse_aut(const std::string& filename,
            const bdd_dict_ptr& dict,
            environment& env = default_environment::instance(),
            automaton_parser_options opts = {});
}