// Labelled state transition system output interface -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "LSTS.h"
#include "Graph.h"
#include "GlobalMarking.h"
#include "Net.h"
#include "Transition.h"
#include "Valuation.h"
#include "VariableDefinition.h"
#include "Expression.h"
#include "Printer.h"

/** @file LSTS.C
 * Labelled state transition system output interface
 */

/* Copyright  2001-2003 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

/** Suffix for the transition file (the longest suffix) */
static const char transitionSuffix[] = "-trans";
/** Suffix for the action file */
static const char actionSuffix[] = "-act";

/** Print a string in special escaped format
 * @param name	the string to be printed
 * @param file	the output stream
 */
static void
escapeString (const char* name,
	      FILE* file)
{
  while (*name) {
    register const char c = *name++;
    /* We cannot use isprint () here, as some LSTS processing tools
       might expect the ASCII character set. */
    if ((c >= 0 && c < 040) || (c >= char (0200) && c < char (0240)) ||
	(c == '"' || c == '\\' || c == 0177))
      fprintf (file, "\\%02x", static_cast<unsigned char>(c));
    else
      putc (c, file);
  }
}

LSTS::LSTS (const class Net& net,
	    const char* filebase) :
  myNet (net), myFilebase (newString (filebase)),
  myNumProps (net.getNumProps ()),
  myNumStates (0), myNumTransitions (0),
  myActionSet (), myProps (new FILE*[net.getNumProps ()]),
  myTransitions (0), myActions (0), myIndex (0)
{
  assert (!!filebase);
  memset (myProps, 0, myNumProps * sizeof *myProps);
}

LSTS::~LSTS ()
{
  unsigned prop;
  for (Set::iterator i = myActionSet.begin (); i != myActionSet.end (); i++)
    operator delete (*i);
  if (myTransitions) {
    fputs ("End Transitions\n", myTransitions);
    fclose (myTransitions);
  }
  if (myActions) {
    fputs ("End Action_names\n", myActions);
    fclose (myActions);
  }
  if (myIndex) {
    fprintf (myIndex,
	     "LSTS_File\n"
	     "Begin Header\n"
	     "State_cnt=%u\n"
	     "Action_cnt=%u\n"
	     "Transition_cnt=%u\n"
	     "State_prop_cnt=%u\n"
	     "Initial_state=1\n"
	     "End Header\n",
	     myNumStates, unsigned (myActionSet.size ()),
	     myNumTransitions, myNumProps);
    fputs ("Include Action_names From \"", myIndex);
    escapeString (myFilebase, myIndex);
    escapeString (actionSuffix, myIndex);
    fputs ("\"\n"
	   "Begin State_props\n", myIndex);
    for (prop = 0; prop < myNumProps; prop++) {
      FILE* f = myProps[prop];
      static char buf[BUFSIZ];
      rewind (f);
      while (size_t len = fread (buf, 1, sizeof buf, f))
	fwrite (buf, 1, len, myIndex);
      fputs (";\n", myIndex);
    }
    fputs ("End State_props\n"
	   "Include Transitions From \"", myIndex);
    escapeString (myFilebase, myIndex);
    escapeString (transitionSuffix, myIndex);
    fputs ("\"\n"
	   "End_LSTS\n", myIndex);
    fclose (myIndex);
  }
  for (prop = myNumProps; prop--; )
    if (myProps[prop])
      fclose (myProps[prop]);
  delete[] myProps;
  delete[] myFilebase;
}

bool
LSTS::openFiles ()
{
  assert (!myNumStates && !myNumTransitions && myActionSet.empty ());
  assert (!myTransitions && !myActions);

  size_t len = strlen (myFilebase);
  char* filename = new char[len + sizeof transitionSuffix];
  memcpy (filename, myFilebase, len);

  class Printer printer (0, Printer::Decimal);
  for (unsigned prop = myNumProps; prop--; ) {
    if (!(myProps[prop] = tmpfile ()))
      goto fail;
    printer.setOutput (myProps[prop]);
    printer.printQuoted (myNet.getPropName (prop));
    fputc (':', myProps[prop]);
  }

  memcpy (filename + len, transitionSuffix, sizeof transitionSuffix);
  if (!(myTransitions = fopen (filename, "w")))
    goto fail;
  fputs ("Begin Transitions\n", myTransitions);
  memcpy (filename + len, actionSuffix, sizeof actionSuffix);
  if (!(myActions = fopen (filename, "w")))
    goto fail;
  fputs ("Begin Action_names\n", myActions);
  if (!(myIndex = fopen (myFilebase, "w")))
    goto fail;
  delete[] filename;
  return true;
 fail:
  fputs (filename, stderr);
  fputs (": ", stderr);
  perror ("fopen");
  delete[] filename;
  return false;
}

/** Context for reporting properties */
struct propcontext {
  card_t state;		///< the state number
  FILE** props;		///< array of property files
};

/** Report a state property that holds
 * @param prop	number of the property
 * @param data	the context
 */
static bool
outputProp (unsigned prop, const void* data)
{
  const struct propcontext& p = *static_cast<const struct propcontext*>(data);
  fprintf (p.props[prop], " %u", p.state);
  return true;
}

void
LSTS::outputState (const class GlobalMarking& m,
		   card_t state)
{
  assert (&myNet == &m.getNet ());
  const struct propcontext p = { state + 1, myProps };
  if (myNumStates <= state)
    myNumStates = state + 1;
  if (!myNet.checkProps (m, ::outputProp, &p))
    assert (false);
}

#ifdef EXPR_COMPILE
# include "Compilation.h"

void
LSTS::outputState (const class Compilation& compilation,
		   card_t state)
{
  const struct propcontext p = { state + 1, myProps };
  if (myNumStates <= state)
    myNumStates = state + 1;
  if (!compilation.checkProps (::outputProp, &p))
    assert (false);
}

#endif // EXPR_COMPILE

void
LSTS::outputArc (card_t source,
		 card_t target,
		 const class Transition& transition,
		 const class Valuation& valuation)
{
  assert (valuation.isOK ());
  fprintf (myTransitions, "%u", source + 1);
  class BitPacker out;
  class StringBuffer sbuf;
  unsigned action = 0;
  myNumTransitions++;
  if (!transition.isHidden (valuation)) {
    // convert the action to canonic form (no values of hidden variables)
    out.clear ();
    if (myNet.getNumTransitions () > 1)
      out.append (transition.getRootIndex (),
		  log2 (myNet.getNumAllTransitions ()));
    else
      assert (myNet.getNumTransitions () == 1);
    for (Transition::const_iterator i = transition.begin ();
	 i != transition.end (); i++) {
      if (i->second->isHidden ())
	continue;
      const class Value* value = valuation.getValue (*i->second);
      if (i->second->isUndefined ())
	out.append (!value, 1);
      else
	assert (!!value);
      if (value)
	out.append (*value);
    }
    out.deflate ();
    size_t* b = static_cast<size_t*>
      (operator new (out.getNumBytes () + 2 * sizeof *b));
    memcpy (b + 2, out.getBuf (), *b = out.getNumBytes ());

    // determine if this is a new action
    std::pair<Set::iterator,bool> p = myActionSet.insert (b);
    if (p.second) {
      action = b[1] = myActionSet.size ();
      fprintf (myActions, "%u=\"", action);
      sbuf.append (transition.getName ());
      sbuf.escape (0);
      valuation.displayEscaped (sbuf, true);
      fwrite (sbuf.getString (), 1, sbuf.getLength (), myActions);
      sbuf.create (0);
      fputs ("\"\n", myActions);
    }
    else {
      operator delete (b);
      action = (*p.first)[1];
    }
  }
  fprintf (myTransitions, " %u %u", target + 1, action);
  fputs (";\n", myTransitions);
}

void
LSTS::outputArcs (const class Graph& graph,
		  card_t source,
		  const card_t* targets,
		  word_t* buf)
{
  assert (targets && *targets && buf);
  fprintf (myTransitions, "%u", source + 1);
  class BitUnpacker in (buf);
  class BitPacker out;
  class StringBuffer sbuf;
  for (card_t i = 1; i <= *targets; i++) {
    const class Transition* transition;
    class Valuation v;
    unsigned action = 0;
    myNet.decode (in, transition, v, true);
    assert (transition && v.isOK ());
    myNumTransitions++;
    if (!transition->isHidden (v)) {
      // convert the action to canonic form (no values of hidden variables)
      out.clear ();
      if (myNet.getNumTransitions () > 1)
	out.append (transition->getRootIndex (),
		    log2 (myNet.getNumAllTransitions ()));
      else
	assert (myNet.getNumTransitions () == 1);
      for (Transition::const_iterator t = transition->begin ();
	   t != transition->end (); t++) {
	if (t->second->isHidden ())
	  continue;
	const class Value* value = v.getValue (*t->second);
	if (t->second->isUndefined ())
	  out.append (!value, 1);
	else
	  assert (!!value);
	if (value)
	  out.append (*value);
      }
      out.deflate ();
      size_t* b = static_cast<size_t*>
	(operator new (out.getNumBytes () + 2 * sizeof *b));
      memcpy (b + 2, out.getBuf (), *b = out.getNumBytes ());

      // determine if this is a new action
      std::pair<Set::iterator,bool> p = myActionSet.insert (b);
      if (p.second) {
	action = b[1] = myActionSet.size ();
	fprintf (myActions, "%u=\"", action);
	sbuf.append (transition->getName ());
	sbuf.escape (0);
	v.displayEscaped (sbuf, true);
	fwrite (sbuf.getString (), 1, sbuf.getLength (), myActions);
	sbuf.create (0);
	fputs ("\"\n", myActions);
      }
      else {
	operator delete (b);
	action = (*p.first)[1];
      }
    }
    fprintf (myTransitions, " %u %u", targets[i] + 1, action);
  }
  fputs (";\n", myTransitions);
}