/*
 * This file is part of the program ltl2dstar (http://www.ltl2dstar.de/).
 * Copyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License version 2 as 
 *  published by the Free Software Foundation.
 *
 * This program 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, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */


#define LTL2DSTAR_VERSION "0.5.1"

/** @file
 * Provides main() and command line parsing for ltl2dstar.
 */

#include "LTL2DRA.hpp"
#include "LTL2DSTAR_Scheduler.hpp"
#include "LTL2NBA.hpp"

#include "Configuration.hpp"

#include "LTLFormula.hpp"
#include "LTLPrefixParser.hpp"

#include "DRA2NBA.hpp"

#include "plugins/PluginManager.hpp"

#include <iostream>
#include <fstream>
#include <sstream>
#include <vector>
#include <cstring>
#include <cassert>

#include "common/Exceptions.hpp"

#include <boost/lexical_cast.hpp>
#include <boost/tokenizer.hpp>


/**
 * The main class.
 */
class LTL2DSTAR_Main {
public:
  /** Flag: Convert LTL->DRA->NBA? */
  bool flag_dra2nba;

  /** Flag: Print the NBA afert LTL->NBA? */
  bool flag_print_ltl_nba;

  /** Flag: Use limiting with scheduler? */
  bool flag_sched_limits;
  
  /** The limiting factor for the scheduler (alpha) */
  double alpha;
  
  /** Flag: Print statistics for NBA? */
  bool flag_stat_nba;

  /** The output format */
  enum {OUT_v2, OUT_NBA, OUT_DOT, OUT_PLUGIN} flag_output;
  
  /** The options for Safra's algorithm */
  Options_Safra opt_safra;
  
  /** The options for LTL2DSTAR */
  LTL2DSTAR_Options opt_ltl2dstar;

  /** Timekeeping: StutterCheck */
  bool stuttercheck_timekeep;
  /** Verbosity: StutterCheck */
  bool stuttercheck_print;

  /** Print usage information or errormessage */
  int usage(const char *programname, const std::string& errormsg="") {
      std::cerr << 
	"ltl2dstar v." << LTL2DSTAR_VERSION << "  Copyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>\n\n";

    if (errormsg=="") {
      std::cerr << 
	"Usage:" << std::endl <<
	"ltl2dstar [parameters] infile outfile\n" <<
	"\ninfile contains a single line LTL formula in prefix format\n" <<
	"infile/outfile can be '-', meaning stdin/stdout\n\n" <<
	"Parameters:\n"<<
	"===========\n\n" <<

	"External LTL-to-Buechi translator:\n" <<
	"  --ltl2nba=interface:path\n" << 
	"  --ltl2nba=interface:path@parameters\n\n" <<
	
	"Type of generated automata:\n" << 
	"  --automata=rabin,streett\n" <<
	"  --automata=rabin\n" <<
	"  --automata=streett\n" <<
	"  --automata=original-nba\n\n" <<

	"Output format:\n" <<
	"  --output=automaton\n" <<
	"  --output=dot\n" <<
	"  --output=nba\n" <<
	"  --output=plugin:NAME\n\n" <<

	"Detailed description of states:\n" <<
	"  --detailed-states=yes/no\n\n" <<

	"Enable/disable \"on-the-fly\" optimizations of Safra's algorithm:\n" <<
	"  --safra=options\n" << 
	"     where options is a comma-seperated list of \n" << 
	"     {all, none, accloop, accsucc, rename, reorder},\n" << 
	"     (a minus '-' in front of an option disables it)\n\n" <<

	"Use bisimulation optimization:\n" <<
	"  --bisimulation=yes/no\n\n" <<
	
	"Optimize acceptance conditions:\n" <<
	"  --opt-acceptance=yes/no\n\n" <<
	
	"Build union automaton for disjunction if beneficial:\n" <<
	"  --union=yes/no\n\n" <<

	"Stuttering:\n" << 
	"  --stutter=yes/no\n" << 
	"  --partial-stutter=yes/no\n\n" << 
	
	"Use scheck for (co-)safe LTL formulas:\n" <<
	"  --scheck=path\n\n" <<

	"Activate Plugins:\n" << 
	"  --plugin=name:\n" <<
	"  --plugin=name:parameter\n\n" << 

	"Print version and quit:\n" <<
	"  --version\n";
      
      std::cerr << std::endl; // flush
    } else {
      std::cerr << errormsg << "\n\n" <<
	"Usage:" << std::endl <<
	programname << " [parameters] infile outfile\n" <<
	"\nFor details on the parameters, use\n  " <<
	programname << " --help" << std::endl << std::endl;
    }

    return 1;
  }
  
  /** Get a full line from input stream */
  std::string getLine(std::istream& in) {
    std::stringstream ss;
    in.get(*ss.rdbuf());
    return ss.str();
  }

  /** A data structure for storing the path and the arguments for an external tool */
  typedef std::pair< std::string, std::vector<std::string> > path_argument_pair;
  
  /**
   * Parse the path and store in path_argument_pair.
   * Path has the form 'path' or 'path\@arguments'
   * @param arg_name the name of the argument (for error message)
   * @param path the path argument
   */
  path_argument_pair parse_path(const std::string& arg_name,
				const std::string& path) {
    size_t pos=path.find('@');
    if (pos!=std::string::npos) {
      if (pos==0) {
	throw CmdLineException("Empty path for parameter '"+arg_name+"'");
      }
      std::string path_=path.substr(0, pos);

      if (pos+1==path.length()) {
	// empty argument part
	return path_argument_pair(path_, 
				  std::vector<std::string>());
      }
      std::string args_=path.substr(pos+1);

      typedef boost::tokenizer<boost::char_separator<char> > tokenizer;

      boost::char_separator<char> sep(" ");
      tokenizer tokens(args_, sep);

      std::vector<std::string> arg;

      for (tokenizer::iterator it=tokens.begin();
	   it!=tokens.end();
	   ++it) {
	arg.push_back(*it);
	// std::cerr<< "[" << *it << "]" << std::endl;
      }

      return path_argument_pair(path_,
				arg);
    } else {
      return path_argument_pair(path, std::vector<std::string>());
    }
  }


  /** 
   * Parse a yes/no value
   * @param arg_name the name of the argument (for error message)
   * @param value the argument value
   * @return true if value=="yes", fals if value=="no"
   */  
  bool parse_yes_no(const std::string& arg_name,
		    const std::string& value) {
    if (value=="yes") {
      return true;
    } else if (value=="no") {
      return false;
    } else {
      throw CmdLineException(std::string("Only yes/no allowed as values for ")+arg_name);
    }
  }

  typedef std::pair<std::string, std::string> string_pair;
  

  /**
   * Split a string at the first occurrence of the character ':'
   */
  string_pair split_at_colon(const std::string& s) {
    size_t pos=s.find(':',0);

    std::string first;
    std::string second;

    if (pos!=std::string::npos) {
      first=s.substr(0, pos);

      if (pos+1!=s.length()) {
	// second not empty
	second=s.substr(pos+1);
      }
    } else {
      first=s;
    }
    
    return string_pair(first, second);
  }


  /** 
   * A value (with optional minus) in a list.
   */
  class ListValue {
  public:
    bool minus;
    std::string value;
  };
  
  /** The type of a vector of ListValue */
  typedef std::vector<ListValue> ListValueVector;

  /**
   * Parse a list of comma-seperated values (optional - in front of values).
   */
  ListValueVector parse_list(const std::string& arg_name,
			     const std::string& value) {
    typedef boost::tokenizer<boost::char_separator<char> > tokenizer;

    boost::char_separator<char> sep(",");
    tokenizer tokens(value, sep);

    std::vector<ListValue> list;

    for (tokenizer::iterator it=tokens.begin();
	 it!=tokens.end();
	 ++it) {

      ListValue lv;
      lv.value=*it;

      if (lv.value.length()==0) {
	throw CmdLineException("Syntax error in "+arg_name);
      }
      
      if (lv.value[0]=='-') {
	lv.minus=true;
	lv.value=lv.value.substr(1);
      } else {
	lv.minus=false;
      }
      list.push_back(lv);
    }

    return list;
  }

  /** 
   * Main function. Parse command line and perform actions.
   */
  int main(int argc, const char *argv[], std::istream& in, std::ostream& out) { 
    try {
      std::map<std::string, std::string> defaults;
      defaults["--ltl2nba"]="--ltl2nba=spin:ltl2ba";
      defaults["--automata"]="--automata=rabin";
      defaults["--output"]="--output=automaton";
      defaults["--detailed-states"]="--detailed-states=no";
      defaults["--safra"]="--safra=all";
      defaults["--bisimulation"]="--bisimulation=yes";
      defaults["--opt-acceptance"]="--opt-acceptance=yes";
      defaults["--union"]="--union=yes";
      defaults["--alpha"]="--alpha=10.0";
      defaults["--stutter"]="--stutter=yes";
      defaults["--partial-stutter"]="--partial-stutter=no";
      //      defaults["--scheck"]=""; // scheck disabled

      // default values...
      flag_dra2nba=false;
      flag_sched_limits=false;

      flag_output=OUT_v2;
      alpha=1.0;

      stuttercheck_timekeep=false;
      stuttercheck_print=false;

      // options not yet covered
      flag_print_ltl_nba=false;
      flag_stat_nba=false;


      const std::string arg_error("Command line error:\n");

      if (argc>1) {
	if (argv[1]==std::string("--help") ||
	    argv[1]==std::string("-h")) {
	  return usage(argv[0]);
	}
	if (argv[1]==std::string("--version")) {
	  std::cout << "ltl2dstar v." << LTL2DSTAR_VERSION << "\nCopyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>\n\n";
	  return 0;
	}
      }

      if (argc<=2) {
	usage(argv[0], "No input/output files specified!");
	return 1;
      }


      std::auto_ptr<LTL2NBA<NBA_t> > ltl2nba;

      std::vector<std::string> arguments;
      int argi;
      for (argi=1;argi<argc;argi++) {
	if (strncmp(argv[argi], "--", 2)==0) {
	  arguments.push_back(argv[argi]);
	} else {
	  break;
	}
      }
      
      if (argc - argi > 2) {
	throw CmdLineException("Too many file arguments!");
      }

      if (argc - argi < 2) {
	throw CmdLineException("Too few file arguments!");
      }


      bool default_phase=false;
      std::vector<std::string>::iterator arg_it;
      std::map<std::string, std::string>::iterator default_it
	=defaults.end(); // precaution

      arg_it=arguments.begin();
      while (true) {
	std::string cur_arg;

	// check for end of actual arguments, go to default arguments
	if (!default_phase && arg_it==arguments.end()) {
	  default_phase=true;
	  default_it=defaults.begin();
	}

	if (arg_it!=arguments.end()) {
	  cur_arg=*arg_it;
	  ++arg_it;
	} else if (default_phase && 
		   default_it!=defaults.end()) {
	  cur_arg=(*default_it).second;
	  ++default_it;
	} else {
	  // processing finished 
	  break;
	}

	// cur_arg is current argument
	std::string::size_type pos;
	pos=cur_arg.find('=', 0); // find =

	if (pos==std::string::npos) {
	  throw CmdLineException("No value given for parameter '"+cur_arg+"'");
	}

	std::string arg_name=cur_arg.substr(0, pos);
	std::string arg_value;
	if (cur_arg.length()==pos+1) {
	  arg_value="";
	} else {
	  arg_value=cur_arg.substr(pos+1);
	}

	// std::cerr << arg_name << " = " << arg_value << std::endl;

	if (!default_phase) {
	  // remove default option with same name
	  std::map<std::string, std::string>::iterator it;
	  it=defaults.find(arg_name);
	  if (it!=defaults.end()) {
	    defaults.erase(it);
	  }
	}


	// parse argument


	if (arg_name=="--ltl2nba") {
	  // ---
	  // The external LTL-to-Buechi translator
	  // ---
		if (arg_value.compare(0, 8, "spinint:")==0 &&
		     arg_value.length()>=9) {
	    path_argument_pair pa=parse_path(arg_name, arg_value.substr(8));
	    //      std::cerr << pa.first << std::endl;
	    ltl2nba.reset(new LTL2NBA_SPINint<NBA_t>(pa.first, pa.second));
	  } else {
		  
	    throw CmdLineException("Illegal argument for '"+arg_name+"'");
	  }


	} else if (arg_name=="--automata") {
	  if (arg_value=="rabin") {
	    opt_ltl2dstar.automata=LTL2DSTAR_Options::RABIN;
	  } else if (arg_value=="streett") {
	    opt_ltl2dstar.automata=LTL2DSTAR_Options::STREETT;
	  } else if (arg_value=="rabin,streett" ||
		     arg_value=="streett,rabin") {
	    opt_ltl2dstar.automata=LTL2DSTAR_Options::RABIN_AND_STREETT;
	  } else if (arg_value=="original-nba") {
	    opt_ltl2dstar.automata=LTL2DSTAR_Options::ORIGINAL_NBA;
	  } else {
	    throw CmdLineException("Illegal value for "+arg_name);
	  }


	} else if (arg_name=="--output") {
	  if (arg_value=="automaton") {
	    flag_output=OUT_v2;
	  } else if (arg_value=="dot") {
	    flag_output=OUT_DOT;
	  } else if (arg_value=="nba") {
	    flag_output=OUT_NBA;
	  } else if (arg_value.compare(0,7,"plugin:") == 0) {
	    flag_output=OUT_PLUGIN;
	    string_pair sp=split_at_colon(arg_value);
	    PluginManager::getManager().setOutputPlugin(sp.second);

	  } else {
	    throw CmdLineException("'"+arg_value+"' is not a valid option for "+arg_name);
	  }

	} else if (arg_name=="--verbose") {
	  opt_ltl2dstar.verbose_scheduler=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--detailed-states") {
	  opt_ltl2dstar.detailed_states=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--time-stuttercheck") {
	  stuttercheck_timekeep=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--print-stuttercheck") {
	  stuttercheck_print=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--safra") {
	  ListValueVector lvv=parse_list(arg_name, arg_value);
	  for (ListValueVector::iterator it=lvv.begin();
	       it!=lvv.end();
	       ++it) {
	    ListValue& lv=*it;

	    if (lv.value=="all") {
	      if (lv.minus) {
		throw CmdLineException("'-all' is illegal for "+arg_name);
	      }
	      opt_safra.opt_all();
	    } else if (lv.value=="none") {
	      if (lv.minus) {
		throw CmdLineException("'-none' is illegal for "+arg_name);
	      }
	      opt_safra.opt_none();
	    } else if (lv.value=="accloop") {
	      opt_safra.opt_accloop=!lv.minus;
	    } else if (lv.value=="accsucc") {
	      opt_safra.opt_accsucc=!lv.minus;
	    } else if (lv.value=="rename") {
	      opt_safra.opt_rename=!lv.minus;
	    } else if (lv.value=="reorder") {
	      opt_safra.opt_reorder=!lv.minus;
	    } else {
	      throw CmdLineException("'"+lv.value+"' is no valid option for "+arg_name);
	    }
	  }

	} else if (arg_name=="--stutter") {
	  opt_safra.stutter=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--partial-stutter") {
	  opt_safra.partial_stutter_check=parse_yes_no(arg_name, arg_value);
	} else if (arg_name=="--stutter-closure") {
	  opt_safra.stutter_closure=parse_yes_no(arg_name, arg_value);
	  
	} else if (arg_name=="--bisimulation") {
	  opt_ltl2dstar.bisim=parse_yes_no(arg_name, arg_value);

	} else if (arg_name=="--opt-acceptance") {
	  opt_ltl2dstar.optimizeAcceptance=parse_yes_no(arg_name, arg_value);

	} else if (arg_name=="--union") {
	    opt_ltl2dstar.allow_union=parse_yes_no(arg_name, arg_value);

	} else if (arg_name=="--scheck") {
	    path_argument_pair pa=parse_path(arg_name, arg_value);
	    
	    if (pa.second.size()!=0) {
	      std::cerr << "Warning: Parameters given the scheck tool are currently ignored" << std::endl;
	    }
	    
	    opt_ltl2dstar.scheck_path=pa.first;


	} else if (arg_name=="--plugin") {
	  string_pair sp=split_at_colon(arg_value);
	  PluginManager::getManager().activatePlugin(sp.first, sp.second);
	} else if (arg_name=="--alpha") {
	  if (arg_value=="unlimited") {
	    flag_sched_limits=false;
	  } else {
	    try {
	      alpha=boost::lexical_cast<double>(arg_value);
	      flag_sched_limits=true;
	    } catch (boost::bad_lexical_cast) {
	      throw CmdLineException ("Argument to '"+arg_name+"' is not a valid (floating-point) number or 'unlimited'");
	    }
	  }
	  
	} else {
	  throw CmdLineException("Unrecognized parameter '"+arg_name+"'");
	}
      }
    
      std::string ltl_string=getLine(in);
      LTLFormula_ptr ltl=LTLPrefixParser::parse(ltl_string);
      APSet_cp ap_set=ltl->getAPSet();

      if (stuttercheck_timekeep) {
	StutterSensitivenessInformation::enableTimekeeping();
      }
      if (stuttercheck_print) {
	StutterSensitivenessInformation::enablePrintInfo();
      }


      assert(ltl2nba.get()!=0);
      LTL2DRA ltl2dra(opt_safra, ltl2nba.get());


      if (opt_ltl2dstar.automata==LTL2DSTAR_Options::ORIGINAL_NBA) {
	// We just generate the NBA for the LTL formula
	// and print it
	
	NBA_ptr nba=ltl2dra.ltl2nba(*ltl);
	if (nba.get()==0) {
	  THROW_EXCEPTION(Exception, "Can't generate NBA for LTL formula");
	}

	if (flag_output==OUT_DOT) {
	  nba->print_dot(out);
	} else {
	  nba->print_lbtt(out);
	}
	return 0;
      }

      DRA_ptr dra;
      
      LTL2DSTAR_Scheduler ltl2dstar_sched(ltl2dra, 
					  flag_sched_limits,
					  alpha);
      
      ltl2dstar_sched.flagStatNBA(flag_stat_nba);
      
      opt_ltl2dstar.opt_safra=opt_safra;
      dra=ltl2dstar_sched.calculate(*ltl, opt_ltl2dstar);
      
      if (!dra->isCompact()) {
	dra->makeCompact();
      }
      if (dra.get()==0) {
	THROW_EXCEPTION(Exception, "Couldn't generate DRA!");
      }
      
      if (!dra->isCompact()) {
	dra->makeCompact();
      }

      PluginManager::getManager().afterDRAGeneration(*dra);

      switch (flag_output) {
      case OUT_v2:
	// standard format
	out << *dra;
	break;
      case OUT_NBA: {
	NBA_t::shared_ptr nba2=DRA2NBA::dra2nba<DRA_t, NBA_t>(*dra);
	nba2->print_lbtt(out);
	break;
      }
      case OUT_PLUGIN:
	PluginManager::getManager().outputDRA(*dra, out);
	break;
      case OUT_DOT:
	dra->print_dot(out);
	break;
      default:
	THROW_EXCEPTION(Exception, "Implementation error");
      }
    } catch (CmdLineException& e) {
      return usage(argv[0], 
		   std::string("===================\nCommand line error:\n ")
		   +e.what()+"\n===================\n");
    } catch (Exception& e) {
      e.print(std::cerr);
      return 1;
    } catch (...) {
      std::cerr << "Unknown fatal error..." << std::cerr;
      return 1;
    }
    return 0;
  }

};

// We need to have it included
#include "plugins/DVE_Process.hpp"

/**
 * Main function, generate LTL2DSTAR_Main and call main() for that.
 */
int main_ltl2dstar(int argc, const char **argv, std::istream& in, std::ostream& out) {
  LTL2DSTAR_Main ltl2dstar_main;
  DVEProcessPlugin dve_process_plugin;
  return ltl2dstar_main.main(argc, argv, in, out);
}