/**
 * @file lsts2dot.C
 * TVT LSTS to GraphViz dot (graph description language) translator
 */

/*
 * Copyright © 2001,2002 Marko Mäkelä <msmakela@tcs.hut.fi>
 *
 *  This program 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 2
 *  of the License, or (at your option) any later version.
 *
 *  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.
 */

#include "InOutStream.hh"
#include "Header.hh"
#include "ActionNamesAP.hh"
#include "TransitionsAP.hh"
#include "DivBitsAP.hh"
#include "StatePropsAP.hh"
#include "StateNamesAP.hh"
#if TVT_VERSION >= 2002000L
# include "iLSTS_File.hh"
# define LSTS_File iLSTS_File
# define ActionNamesAP iActionNamesAP
# define StatePropsAP iStatePropsAP
# define TransitionsAP iTransitionsAP
#else
# include "LSTS_File.hh"
#endif
#include <multimap.h>

using std::string;
using std::ostream;
using std::cout;

/** Encapsulate the special characters in a character string
 * @param escaped	target string for the encapsulated copy
 * @param source	source string to be encapsulated and copied
 */
static void
escape (string& escaped,
	const string& source)
{
  /** original and escaped length, and an index */
  string::size_type len = source.length (), elen, i;
  for (i = len, elen = 0; i--; elen++) {
    register const char c = source[i];
    if ((c >= 0 && c < 040) || (c >= char (0200) && c < char (0240)) ||
	c == 0177 || c == '^' || c == '\\' || c == '"')
      elen++;
  }
  escaped.assign (elen, 0);
  for (i = elen = 0; i < len; i++, elen++) {
    register const char c = source[i];
    if ((c >= 0 && c < 040) || (c >= char (0200) && c < char (0240)) ||
	c == 0177 || c == '^') {
      escaped.replace (elen++, 1, 1, '^');
      if (c == '^')
	escaped.replace (elen, 1, 1, '!');
      else if (c >= 0 && c < 040)
	escaped.replace (elen, 1, 1, c | '@');
      else if (c == 0177)
	escaped.replace (elen, 1, 1, '?');
      else if (c == char (0237))
	escaped.replace (elen, 1, 1, '#');
      else
	escaped.replace (elen, 1, 1, (c & ~0200) | '`');
      continue;
    }
    else if (c == '\\' || c == '"')
      escaped.replace (elen++, 1, 1, '\\');
    escaped.replace (elen, 1, 1, c);
  }
}

/** Action name reader */
class ActionNamesReader : public ActionNamesAP
{
public:
  /** Default constructor */
  ActionNamesReader () : myNumActions (0), myActions (0) {}
private:
  /** Copy constructor */
  ActionNamesReader (const class ActionNamesReader&);
  /** Assignment operator */
  class ActionNamesReader& operator= (const class ActionNamesReader&);
public:
  /** Destructor */
  ~ActionNamesReader () { delete[] myActions; }
  /** Callback for starting the action names section
   * @param header	the LSTS file header
   */
  void lsts_StartActionNames (class Header& header) {
    myNumActions = header.GiveActionCnt ();
    delete[] myActions;
    myActions = new string[myNumActions];
  }
  /** Callback for mapping action numbers to names
   * @param number	the action number (1..myNumActions)
   * @param name	the action name
   */
  void lsts_ActionName (lsts_index_t number,
			const string& name) {
    assert (number >= 1 && number <= myNumActions);
    escape (myActions[number - 1], name);
  }
  /** Callback for ending the action names section */
  void lsts_EndActionNames () {}

  /** Get an action name by number
   * @param number	the action number (1..myNumActions)
   * @return		the corresponding action name
   */
  const string& operator[] (lsts_index_t number) const {
    assert (number >= 1 && number <= myNumActions);
    return myActions[number - 1];
  }

private:
  /** Number of the actions */
  lsts_index_t myNumActions;
  /** Action names indexed by number */
  string* myActions;
};

/** State proposition reader */
class StatePropsReader : public StatePropsAP
{
public:
  /** Multi-map from state numbers to names of propositions that hold */
  typedef multimap<lsts_index_t,const string*> Map;
  
  /** Constructor
   * @param out		the output stream
   */
  StatePropsReader (ostream& out) :
    myNumProps (0), myInitial (0), myProps (0), myStates (), myOutput (out) {}
private:
  /** Copy constructor */
  StatePropsReader (const class StatePropsReader&);
  /** Assignment operator */
  class StatePropsReader& operator= (const class StatePropsReader&);
public:
  /** Destructor */
  ~StatePropsReader () {
    while (myNumProps--)
      delete myProps[myNumProps];
    delete[] myProps;
  }

  /** Callback for starting the state proposition section
   * @param header	the LSTS file header
   */
  void lsts_StartStateProps (class Header& header) {
    myNumProps = 0;
    myInitial = header.GiveInitialState ();
  }

  /** Callback for starting the state numbers in which a proposition holds
   * @param prop	name of the state proposition
   */
  void lsts_StartPropStates (const string& prop) {
    if (!(myNumProps & (myNumProps + 1))) {
      string** props = new string*[(myNumProps + 1) << 1];
      memcpy (props, myProps, myNumProps * sizeof *myProps);
      delete[] myProps;
      myProps = props;
    }
    escape (*(myProps[myNumProps++] = new string), prop);
  }
  /** Callback for reporting a state where the last proposition
   * reported with lsts_StartPropStates holds
   * @param state	the state number
   */
  void lsts_PropState (lsts_index_t state) {
    assert (myNumProps > 0);
    myStates.insert (Map::value_type (state, myProps[myNumProps - 1]));
  }
  /** Callback for ending the state numbers in which a proposition holds */
  void lsts_EndPropStates (const string&) {}
  /** Callback for ending the state proposition section */
  void lsts_EndStateProps () {
    /** Number of the current state */
    lsts_index_t state = 0;

    if (myInitial)
      myOutput << myInitial << "[style=bold];\n";

    for (Map::iterator i = myStates.begin (); i != myStates.end (); i++) {
      if (i->first != state) {
	if (state)
	  endLabel (myOutput);
	beginLabel (myOutput, state = i->first);
      }
      myOutput << "\\n" << *(i->second);
    }

    if (state)
      endLabel (myOutput);
  }

private:
  /** Print the label prefix for a state proposition list
   * @param out		the output stream
   * @param state	the state number
   */
  static void beginLabel (ostream& out, lsts_index_t state) {
    out << state << "[label=\"" << state;
  }
  /** Print the label suffix for a state proposition list
   * @param out		the output stream
   */
  static void endLabel (ostream& out) {
    out << "\"];\n";
  }

private:
  /** Number of encountered propositions */
  lsts_index_t myNumProps;
  /** Number of the initial state (0=unknown) */
  lsts_index_t myInitial;
  /** Proposition names */
  string** myProps;
  /** Mapping from state numbers to propositions that hold in the states */
  Map myStates;
  /** The output stream */
  ostream& myOutput;
};

/** Transition reader */
class TransitionsReader : public TransitionsAP
{
public:
  /** Constructor
   * @param out		the output stream
   * @param actions	the action names
   */
  TransitionsReader (ostream& out,
		     const class ActionNamesReader& actions) :
    myOutput (out), myActions (actions), myDest (0) {}
private:
  /** Copy constructor */
  TransitionsReader (const class TransitionsReader&);
  /** Assignment operator */
  class TransitionsReader& operator= (const class TransitionsReader&);
public:
  /** Destructor */
  ~TransitionsReader () {}
  /** Callback for starting the transition section */
  void lsts_StartTransitions (class Header&) {}
  /** Callback for starting the transitions from a state */
  void lsts_StartTransitionsFromState (lsts_index_t) { myDest = 0; }
  /** Callback for reading a transition
   * @param source	the source state
   * @param dest	the destination state
   * @param action	the action number
   */
  void lsts_Transition (lsts_index_t source,
			lsts_index_t dest,
			lsts_index_t action) {
    if (dest == myDest)
      myOutput << ",\\n";
    else {
      if (myDest)
	endLabel (myOutput);
      myDest = dest;
      myOutput << source << "->" << dest;
      beginLabel (myOutput);
    }

    if (action)
      myOutput << myActions[action];
  }
  /** Callback for ending the transitions from a state */
  void lsts_EndTransitionsFromState (lsts_index_t) {
    if (myDest) endLabel (myOutput); myDest = 0;
  }
  /** Callback for ending the transition section */
  void lsts_EndTransitions () {}

private:
  /** Print the label prefix for an action list
   * @param out		the output stream
   */
  static void beginLabel (ostream& out) {
    out << "[label=\"";
  }
  /** Print the label suffix for a state proposition list
   * @param out		the output stream
   */
  static void endLabel (ostream& out) {
    out << "\"];\n";
  }

private:
  /** The output stream */
  ostream& myOutput;
  /** The action names */
  const class ActionNamesReader& myActions;
  /** Destination state for the last processed transition (0=none) */
  lsts_index_t myDest;
};

/** The main program
 * @param argc		number of command-line arguments
 * @param argv		the command-line arguments
 */
int
main (int argc, char** argv)
{
  /** The input stream maintainer library */
  class InStream inp;
  /** The action name reader */
  class ActionNamesReader actions;
  /** The transition name reader */
  class TransitionsReader transitions (cout, actions);
  /** The state property reader */
  class StatePropsReader properties (cout);
  /** A string for holding the escaped name of the LSTS being processed */
  string esc;

  // Interpret all command-line arguments as names of LSTS to be converted
  for (int k = 1; k < argc; k++) {
    class InStream& is = inp.OpenInputFile (argv[k]);
    class LSTS_File lsts (is, true);
#if TVT_VERSION >= 2002000L
    lsts.SkipUnwantedSections (false);
#else
    lsts.SkipDivBits ();
    lsts.SkipAccSets ();
    lsts.SkipStateNames ();
#endif
    lsts.AddActionNamesReader (actions);
    lsts.AddTransitionsReader (transitions);
    lsts.AddStatePropsReader (properties);
    escape (esc, argv[k]);
    cout << "digraph \"" << esc << "\"\n{\n";
    lsts.ReadFile ();
    is.CloseFile ();
    cout << "}\n";
  }

  return 0;
}