From df685433f473b2830cf5aae93581489b0964ad0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jun 2022 14:33:16 +0200 Subject: [PATCH] bin: separate process_file() for aut and ltl * bin/common_finput.cc, bin/common_finput.hh, bin/common_hoaread.hh (process_file): Split into... (process_ltl_file, process_aut_filt): ... these, as we will need both in ltlsynt. --- bin/common_finput.cc | 12 ++++++++++-- bin/common_finput.hh | 5 ++++- bin/common_hoaread.hh | 8 +++++--- 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 6f09601e0..8e78b5599 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -303,7 +303,13 @@ job_processor::process_stream(std::istream& is, } int -job_processor::process_file(const char* filename) +job_processor::process_aut_file(const char*) +{ + throw std::runtime_error("process_aut_file not defined for this tool"); +} + +int +job_processor::process_ltl_file(const char* filename) { col_to_read = 0; @@ -366,8 +372,10 @@ job_processor::run() error |= process_string(j.str); break; case job_type::LTL_FILENAME: + error |= process_ltl_file(j.str); + break; case job_type::AUT_FILENAME: - error |= process_file(j.str); + error |= process_aut_file(j.str); break; default: throw std::runtime_error("unexpected job type"); diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 54ced7f7b..44a78bada 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -72,7 +72,10 @@ public: process_stream(std::istream& is, const char* filename); virtual int - process_file(const char* filename); + process_ltl_file(const char* filename); + + virtual int + process_aut_file(const char* filename); virtual int run(); diff --git a/bin/common_hoaread.hh b/bin/common_hoaread.hh index b3cc912a5..e66967393 100644 --- a/bin/common_hoaread.hh +++ b/bin/common_hoaread.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2017, 2018, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -80,8 +80,10 @@ public: } int - process_file(const char* filename) override + process_aut_file(const char* filename) override { + col_to_read = 0; + // If we have a filename like "foo/NN" such // that: // ① foo/NN is not a file,