/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 ******************************************************************
 *  $Log$
 ******************************************************************/

#ifndef lint
static char rcsid[]= "$Id$";
#endif

/******************************************************************
 *
 *  Santiago Pavon Gomez
 *  Francisco Monfort Martin
 *
 *  Management of LOLA internal cursor.
 *  This cursor is controlled by the user and always points to a
 *  sub-behaviour of the specification.
 *  Most LOLA commands will be applied to this sub-behaviour.
 *
 *  26 Nov 1990
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : activate debugging checks
 *
 *  LOG:
 *
 ******************************************************************/

/* LINTLIBRARY */

#include "lilists.h"
#include "limisc.h"
#include "batables.h"
#include "baprint.h"
#include "bamove.h"
#include "baexpr.h"
#include "badefca.h"
#include "basust_v.h"


/******************************************************************
 *                                                                *
 *  Data structures to maintain the path to the internal cursor.  *
 *                                                                *
 ******************************************************************/


/*
 * Stack to control the moves of the tree.
 */
static StackTyp move_stack = NULL;


/*
 * cursor to move in a tree.
 */
static BehTyp cursor  = NULL;


/*
 * cursor to the first position of a tree.
 */
static BehTyp mvroot = NULL;


static StackTyp auxStack;
static DescriptorTyp current_process;


/*----------------------------------------------------------------*/

/* StatMove
 * Return the number of node lists used to keep the cursor position.
 */
int StatMove()
{
  return Count_Stack(move_stack);
}

/*----------------------------------------------------------------*/

/* GetCursor
 * Return the position of the "cursor".
 */
BehTyp GetCursor()
{
  return(cursor);
}

/*----------------------------------------------------------------*/

/* GetRoot
 * Return a pointer to the specification or process where the
 * internal cursor is.
 */
BehTyp GetRoot()
{
  return(mvroot);
}

/*----------------------------------------------------------------*/

/* KillMoveStack
 * Kills the stack "move_stack" and assign this one to stack "stack".
 */
static void KillMoveStack(stack)
     StackTyp stack;
{
  if (move_stack != NULL)
    Free_Stack (move_stack,(void(*)())NULL);
  move_stack = stack;
}

/*----------------------------------------------------------------*/

/* InitMove
 * Initialization of this module. This function must be called
 * after a new specification has been loaded.
 * Sets the cursor to the specification or process specified with d.
 */
void InitMove( d )
     DescriptorTyp d;
{
  current_process = d;
  cursor = GetP_def(d);
  mvroot = cursor;
  if (move_stack != NULL) {
    Free_Stack(move_stack,(void(*)())NULL);
    move_stack = Create_Stack();
  }
  move_stack = Save_Stack((DataStackTyp)cursor,move_stack);
}

/*----------------------------------------------------------------*/

/* FreeMove
 * Cleans the internal datas of the module.
 * It must be used when the current specification is deleted.
 */
void FreeMove()
{
  cursor = NULL;
  mvroot = NULL;
  if (move_stack != NULL) {
    Free_Stack(move_stack,(void(*)())NULL);
    move_stack = Create_Stack();
  }
}

/*----------------------------------------------------------------*/

/* MvCursorBeh
 * Move the cursor to the first behaviour operator, i.e. jumps the
 * ProcessDef and Specification operators.
 * Return the new cursor.
 */
BehTyp MvCursorBeh()
{
  BehTyp c;

  c = GetCursor();
  if (c!=NULL) {
    if ( (LookTypeB(c)==SpecificationC) || (LookTypeB(c)==ProcessDefC) ) {
      (void)Move(1,'d');
    }
    return GetCursor();
  }
  else {
    Warning("A specification must be loaded first.\n");
    return NULL;
  }
}

/*----------------------------------------------------------------*/

/* MoveB
 * Move the cursor to the "offset" argument of the current operation.
 */
static BehTyp MoveB(offset)
     int offset;
{
  BehTyp        auxcur;
  ITContListTyp itcl;
  PITContTyp    itc;

  LASSERT(offset > 0);
  if (NumArgB(cursor)>=offset) {
    auxcur = LookArgB(cursor,offset);
    if (OwnersB(auxcur)>1) {
      auxcur = GetArgB(cursor,offset);
      auxcur = CopyOperB(auxcur);
      PutArgB(cursor,auxcur,offset);
    }
    auxStack = Save_Stack((DataStackTyp)auxcur,auxStack);
    cursor = auxcur;
  }
  else if (LookTypeB(cursor)==InterleavedC) {
    itcl = (ITContListTyp)LookAInfo(LookA(LookArgB(cursor,2),ITCLA));
    offset -= 2;
    if (Length_list(itcl)>=offset) {
      while (offset-- > 1)
	itcl = Next_list(itcl);
      itc = (PITContTyp)LookInfo_list(itcl);
      if (OwnersB(itc->b)>1) {
	itc->b = UnshareB(itc->b);
	itc->b = ShareB(GetOperB(itc->b));
      }
      auxStack = Save_Stack((DataStackTyp)itc->b,auxStack);
      cursor = itc->b;
    }
    else
      auxcur = NULL;
  }
  else
    auxcur = NULL;

  return auxcur;
}

/*----------------------------------------------------------------*/

/* MoveD
 * Try to move "offset" positions down in the tree.
 */
static BehTyp MoveD(offset)
     int offset;
{
  int cont;
  BehTyp auxcur;

  LASSERT(offset > 0);
  cont = 0;
  for (auxcur = cursor;(auxcur!=NULL) && (cont!=offset); cont++) {
    if (NumArgB(auxcur)>0) {
      auxcur = MoveB(1);
    }
    else
      auxcur = NULL;
  }
  return auxcur;
}

/*----------------------------------------------------------------*/

/* MoveU
 * Try to move "offset" positions up the tree.
 */
static BehTyp MoveU(offset)
     int offset;
{
  int cont;
  BehTyp auxcur;

  LASSERT(offset > 0);
  cont = 0;
  for (auxcur = cursor;(cont!=offset) && (auxcur!=NULL);cont++) {
    auxStack = Remove_Stack(&auxStack,(void(*)())NULL);
    auxcur = (BehTyp) Look_Stack(auxStack);
  }
  cursor = (BehTyp) Look_Stack(auxStack);
  return auxcur;
}

/*----------------------------------------------------------------*/

/* MoveRoot
 * Move the root and the cursor to the specification level, i.e. to the
 * first position of the process table.
 */
BehTyp MoveRoot()
{
  InitMove(1);
  return cursor;
}

/*----------------------------------------------------------------*/

/* MoveDProc
 * Move the cursor to the definition of the process "d".
 */
BehTyp MoveDProc( d )
     DescriptorTyp  d;
{
  LASSERT(d<=LastTableP());
  InitMove(d);
  return cursor;
}

/*----------------------------------------------------------------*/

/* MoveProc
 * Move the cursor to the definition of the process called "name".
 */
BehTyp MoveProc(name)
     char *name;
{
  int aux;

  aux = FindP(name);
  if (aux != 0) {
    InitMove(aux);
    return cursor;
  }
  else {
    (void)printf("\nProcess %s doesn't exist.\n",name);
    return NULL;
  }
}

/*----------------------------------------------------------------*/

static void MovePrintLine(l)
     ListTyp l;
{
  int i;

  if (l!=NULL) {
    i = (int) LookInfo_list(l);
    if (Next_list(l)==NULL) {
      if (i<0)
	(void)MoveDProc(-i);
      else
	(void)Move(i,'u');
    }
    else {
      MovePrintLine(Next_list(l));
      if (i>0)
	(void)Move(i,'d');
      else
	(void)Move(-i,'b');
    }
  }
}

/*----------------------------------------------------------------*/

/* Move
 * Move the cursor to the specified place.
 */
BehTyp Move(offset,direction)
     int  offset;
     char direction;
{
  BehTyp c;

  if (offset==0)
    return NULL;
  if (direction=='l') {
    MovePrintLine(GetMove(offset));
    return NULL;
  }
  auxStack = Copy_Stack(move_stack,EchoInt);
  switch (direction)
    { case 'd':
      case 'D':
	if (offset < 0)
	  c = MoveU(-offset);
	else
	  c = MoveD(offset);
	break;
      case 'b':
      case 'B':
	if (offset < 0)
	  { if ((c=MoveU(1))!=NULL)
	      c = MoveB(-offset);
	  }
	else
	  c = MoveB(offset);
	break;
      case 'u':
      case 'U':
	if (offset < 0) {
	  c = MoveD(-offset);
	}
	else
	  c = MoveU(offset);
	break;
      default:
	c = NULL;
	break;
      }
  if (c == NULL)
    { Free_Stack(auxStack,(void(*)())NULL);
      (void)printf("\nI can't do the specified movement.\n");
      cursor = (BehTyp) Look_Stack(move_stack);
      return NULL;
    }
  KillMoveStack(auxStack);
  cursor = (BehTyp) Look_Stack(move_stack);
  return cursor;
}

/*----------------------------------------------------------------*/

/* Current_Process
 * Return the descriptor of the process whose behaviour the cursor is
 * pointing to.
 */
DescriptorTyp Current_Process()
{
  return current_process;
}


/******************************************************************
 *                                                                *
 * Copy the path root-cursor and share the cells not in the path. *
 *                                                                *
 ******************************************************************/

/* CopyMovePath
 * return a copy of the path root-cursor.
 */
BehTyp CopyMovePath()
{
  BehTyp   prev,origprev,copy,res;
  StackTyp mstk;
  int      n;

  mstk     = Copy_Stack(move_stack,EchoInt);
  origprev = NULL;
  while ( mstk!=NULL ) {
    prev = (BehTyp)Get_Stack(&mstk);
    copy = CopyOperB(prev);
    if ( origprev ==NULL )
      res = copy;
    else
      for ( n=NumArgB(copy); n>0 ; n-- )
	if ( LookArgB(copy,n)==origprev ) {
	  (void)GetArgB(copy,n);
	  PutArgB( copy, res, n );
	  res = copy;
	  break;
	}
    origprev = prev;
  }
  return res;
}

/*----------------------------------------------------------------*/

/* IsCursorAt_WBE_Context
 * Says if the cursor is at a context where an i removal i;B ~ B
 * would leave it Weak Bisimulation Congruent.
 */
boolean IsCursorAt_WBE_Context()
{
  StackTyp mstk;
  BehTyp   down, up;

  mstk = Copy_Stack(move_stack,EchoInt);
  down = (BehTyp) Get_Stack(&mstk);
  up   = (BehTyp) Get_Stack(&mstk);
  while ( up!=NULL ) {
    switch ( LookTypeB(up) )
      {
      case GateC:
      case IC:
	Free_Stack( mstk, (void(*)())NULL );
	return TRUE;

      case AlternativeC:
      case GateChoiceC:
      case ChoiceC:
	Free_Stack( mstk, (void(*)())NULL );
	return FALSE;

      case DisablingC:
	if ( LookArgB(up,2)==down ) {
	  Free_Stack( mstk, (void(*)())NULL );
	  return FALSE;
	}
      default:
	break;
      }
    down = up;
    up   = (BehTyp)Get_Stack(&mstk);
  }
  return TRUE;
}

/*----------------------------------------------------------------*/
