/***********************************
  (C) Copyright 1992-1993; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************/

/***********************************
  
  Santiago Pavon Gomez
  
  13/09/1993
  
  Module to keep track of which is the success event in any point of a
  behaviour.
  
  During the test-expansion process, LOLA applies some rules to remove
  internal action (expansion of the parallel operator) in order to reduce the
  number of state to explore.
  
  For example     i;B1 [] i;B2 |[A]| a;B3  
  is expanded to  i;(B1 |[A]| a;B3) [] i;(B2 |[A]| a;B3) 
  
  The third branch (a;(i;B1 [] i;B2 |[A]| B3)) has been removed because
  the testing equivalence relation is maintained.
  
  The problem is that if "a" is the success event, then we are delaying the
  ocurrence of this event and we will explore more states than necessary.
  
  This module maintains an internal stack with the success event actions in
  order to not apply the optimization rules when the success event is offered.
  Note that the success event is a gate set because different gates can be
  relabelled to the success event.
  
  Then the expansion is modified to apply this rule:
  
  (B1 [] choice x:t [] ok;B) |[A]| B2
  
  is transformed into
  
  choice x:t [] ok;stop
  
  where the choice is optional.
  
  Three functions must be called to update the success event set
  when we find a relabel, a parallel or a hide operator:
  
  - HIDE:     The gates of the success event set belonging to the hide set
              must be not considered below the hide operator.
  - RELABEL:  The gates of the success event set must be relabeled to know
              what is the new success event set below the relab operator.
  - PARALLEL: The synchronization gates are removed from the success
              event set. Perhaps, the parallel operator must do any
              synchronization to be able to produce the success event.
  - GENERALIZED PAR: Don't worry. It is transformed into a normal 
              parallel operator.
  
  ************************************/

/* LINTLIBRARY */

#include "badefca.h"
#include "listack.h"
#include "batables.h"
#include "eximmed.h"

/******************************************************************
 *
 * Stack of Success Events
 *
 * There is an internal stack where the current success event set,
 * during the expansion process of each operator, is stored.
 * Initialy the stack is initialized with the success event specified in
 * the command line.
 * In order to save memory, the empty gate set can be stored as NULL 
 * pointers.
 *
 *******************************************************************/

/* Internal Stack of Success Events.
 */
static StackTyp stackSuccess = NULL;

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

/* InitSuccessStack
 * Init the internal stack with the gate set { g }.
 * If "g" is zero, then it is initialized with NULL.
 */ 
void InitSuccessStack( g )
     DescriptorTyp g;
{
  LASSERT(IsEmpty_Stack(stackSuccess));
  if (g==0)
    stackSuccess = Save_Stack((DataStackTyp)NULL,stackSuccess);
  else
    stackSuccess = Save_Stack((DataStackTyp)CopyGS(GetG_mask(g)),
			      stackSuccess);
}

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

/* PopSuccessStack
 * Pop the last element on the stack
 */
void PopSuccessStack()
{
  GateSetTyp gs;
  
  LASSERT(!IsEmpty_Stack(stackSuccess));
  gs = (GateSetTyp)Get_Stack(&stackSuccess);
  if (gs != NULL)
    FreeGS(gs);
}

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

/* RelabUpdateSuccessStack
 * Calculate what is the new success event set after the relabel function
 * "rfl", and store it in the internal stack.
 */
void RelabUpdateSuccessStack( rfl )
     RelabFuncListTyp rfl; 
{
  GateSetTyp       gs;
  
  LASSERT(!IsEmpty_Stack(stackSuccess));
  gs = (GateSetTyp)Look_Stack(stackSuccess);
  if (gs != NULL) {
    gs = InvApplyRFL( rfl, gs );
    stackSuccess = Save_Stack((DataStackTyp)gs,stackSuccess);
  }
  else
    stackSuccess = Save_Stack((DataStackTyp)NULL,stackSuccess);
}

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

/* HideUpdateSuccessStack
 * Calculate what is the new success event set after the hide operator
 * whose gate set is hgs, and store it in the internal stack.
 */
void HideUpdateSuccessStack( hgs )
     GateSetTyp hgs;
{
  GateSetTyp       gs;
  
  LASSERT(!IsEmpty_Stack(stackSuccess));
  gs = (GateSetTyp)Look_Stack(stackSuccess);
  if (gs != NULL) {
    gs = DiffGS( gs, hgs );
    stackSuccess = Save_Stack((DataStackTyp)gs,stackSuccess);
  }
  else
    stackSuccess = Save_Stack((DataStackTyp)NULL,stackSuccess);
}

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

/* ParUpdateSuccessStack 
 * Calculate what is the new success event set after the parallel operator
 * b, and store it in the internal stack.
 */
void ParUpdateSuccessStack(b)
     BehTyp b;
{
  GateSetTyp       gs,pgs;
  
  LASSERT(!IsEmpty_Stack(stackSuccess));
  LASSERT(LookTypeB(b)==ParallelC);
  gs = (GateSetTyp)Look_Stack(stackSuccess);
  if (gs != NULL) {
    switch ( LookNameB(b) ) 
      { case FULL_SYNC:
	  stackSuccess = Save_Stack((DataStackTyp)NULL,stackSuccess);
	  break;
	case INTER_SYNC:
	  stackSuccess = Save_Stack((DataStackTyp)CopyGS(gs),stackSuccess);
	  break;
	case PART_SYNC:
	  pgs = (GateSetTyp)LookAInfo(LookA(b,GSA));
	  gs = DiffGS( gs, pgs );
	  stackSuccess = Save_Stack((DataStackTyp)gs,stackSuccess);
	  break;
	default:
	  Error("ParUpdateSuccessStack: unexpected synchronization type.");
	}
  }
  else
    stackSuccess = Save_Stack((DataStackTyp)NULL,stackSuccess);
}

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

/* Par_to_Success
 * If the parallel operator b offers the success event, then
 * b is glued by that success event and TRUE is returned.
 */ 
boolean Par_to_Success(b)
     BehTyp b;
{
  int        j,i,n;
  BehTyp     b1,b0;
  GateSetTyp gs,gsi;
  
  LASSERT(!IsEmpty_Stack(stackSuccess));
  gs = (GateSetTyp)Look_Stack(stackSuccess);
  if ((gs!=NULL) && (!IsEmptyGS(gs))){
    if ( LookNameB(b)==FULL_SYNC )
      return FALSE;
    if ( LookNameB(b)==PART_SYNC ){
      gsi = IntersGS(gs,(GateSetTyp)LookAInfo(LookA(b,GSA)));
      if (!IsEmptyGS(gsi)){
	FreeGS(gsi);
	return FALSE;
      }
      FreeGS(gsi);
    }
    for ( j=1; j<=2; j++ ) {
      b1 = LookArgB(b,j);
      n  = NumArgIB(b1);
      for ( i=1; i<=n; i++ ) {
	b0 = LookArgIB(b1,i);
	while (LookTypeB(b0)==ChoiceC) b0 = LookArgB(b0,1); /* skip choices */
	if ((LookTypeB(b0)==GateC) && (GateInGS(LookNameB(b0),gs))) {
	  /* Success */
	  GlueB(b,LookArgIB(b1,i));
	  return TRUE;
	}
      }
    }
  }
  return FALSE;
}

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


