// -*- coding: utf-8 -*-
// Copyright (C) 2017 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/>.

#include "common_sys.hh"

#include <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
#include "error.h"
#include <vector>

#include "common_setup.hh"
#include "common_aoutput.hh"
#include "common_range.hh"
#include "common_cout.hh"

#include <cassert>
#include <iostream>
#include <sstream>
#include <set>
#include <string>
#include <cmath>
#include <cstdlib>
#include <cstring>
#include <spot/gen/automata.hh>

using namespace spot;

const char argp_program_doc[] ="\
Generate omega automata from predefined patterns.";

enum {
  FIRST_CLASS = 256,
  OPT_KS_COBUCHI = FIRST_CLASS,
  LAST_CLASS,
};

const char* const class_name[LAST_CLASS - FIRST_CLASS] =
  {
    "ks-cobuchi",
  };

#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }

static const argp_option options[] =
  {
    /**************************************************/
    // Keep this alphabetically sorted (expect for aliases).
    { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
    { "ks-cobuchi", OPT_KS_COBUCHI, "RANGE", 0,
      "A co-Büchi automaton with 2N+1 states for which any equivalent "
      "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
    RANGE_DOC,
  /**************************************************/
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
  };

struct job
{
  int pattern;
  struct range range;
};

typedef std::vector<job> jobs_t;
static jobs_t jobs;

const struct argp_child children[] =
  {
    { &aoutput_argp, 0, nullptr, 3 },
    { &aoutput_o_format_argp, 0, nullptr, 4 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
  };

static void
enqueue_job(int pattern, const char* range_str)
{
  job j;
  j.pattern = pattern;
  j.range = parse_range(range_str);
  jobs.push_back(j);
}

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case OPT_KS_COBUCHI:
      enqueue_job(key, arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

static void
output_pattern(int pattern, int n)
{
  twa_graph_ptr aut = nullptr;
  switch (pattern)
    {
      // Keep this alphabetically-ordered!
    case OPT_KS_COBUCHI:
      aut = spot::gen::ks_cobuchi(n);
      break;
    default:
      error(100, 0, "internal error: pattern not implemented");
    }

  process_timer timer;
  automaton_printer printer;
  printer.print(aut, timer, nullptr, class_name[pattern - FIRST_CLASS], n);
}

static void
run_jobs()
{
  for (auto& j: jobs)
    {
      int inc = (j.range.max < j.range.min) ? -1 : 1;
      int n = j.range.min;
      for (;;)
        {
          output_pattern(j.pattern, n);
          if (n == j.range.max)
            break;
          n += inc;
        }
    }
}


int
main(int argc, char** argv)
{
  strcpy(F_doc, "the name of the pattern");
  strcpy(L_doc, "the argument of the pattern");
  setup(argv);

  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
                    children, nullptr, nullptr };

  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
    exit(err);

  if (jobs.empty())
    error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
          program_name);

  try
    {
      run_jobs();
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }

  flush_cout();
  return 0;
}