Logo Search packages:      
Sourcecode: maria version File versions

LSTS.C

Go to the documentation of this file.
// 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 Mäkelä (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) */
00041 static const char transitionSuffix[] = "-trans";
/** Suffix for the action file */
00043 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
00050 escapeString (const char* name,
            FILE* file)
{
  while (*name) {
    register const char c = *name++;
    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);
  }
}

00063 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);
}

00075 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
00129 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 */
00168 struct propcontext {
00169   card_t state;         ///< the state number
00170   FILE** props;         ///< array of property files
};

/** Report a state property that holds
 * @param prop    number of the property
 * @param data    the context
 */
static bool
00178 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
00186 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
00214 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
00272 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);
}

Generated by  Doxygen 1.6.0   Back to index