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

/***********************************

  Maria Hultstrom

  28-10-1990

  Checks If a specification diverges or is unguarded.


  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:

  (none)

  ************************************/

/* LINTLIBRARY */

#include "listdh.h"
#include "badefca.h"
#include "batables.h"
#include "baattr.h"
#include "lilists.h"
#include "libst.h"
#include "exdiver.h"
#include "licell.h"
#include "limisc.h"
#include "listdout.h"
#include "expre_br.h"
#include "balotosf.h"


static boolean first_time_div,first_time_ung;
static BstTyp  unguardedProcesses = CreateBST();
/* KJT 22/01/23: added "int" type */
static int usedNodes = 0;
static BstTyp  exploredDiverge, exploredSearch;

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

/* Print_msg
 * Prints which process the problem occured in and the path.
 */
static void Print_msg( l, proc )
     ListTyp l;
     DescriptorTyp proc;
{
  printMsgs("        See path: ");
  Print_list( l, GetP_name, printMsgs );
  printMsgs(", ");
  printMsgs(GetP_name(proc));
  printMsgs("\n");
}

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

static boolean Search_proc_aux( b, proc, dp1, dp2, guard )
     BehTyp b;
     DescriptorTyp proc;
     ListTyp dp1, dp2;
     boolean guard;
{
  DescriptorTyp pdef;
  ListTyp       tmp1, tmp2;
  int           argnum, i;
  boolean       found = FALSE;

  if (b)
    switch( LookTypeB(b) )
      {
      case ProcessInstC:
	pdef = LookNameB(b);
	if ( pdef == proc ) {
	  if (guard)
	    Warning("Possible divergent behaviour.");
	  else
	    Warning("Divergent behaviour.");
	  tmp1 = Copy_list( dp1, (DataListTyp (*)())EchoInt );
	  tmp2 = Copy_list( dp2, (DataListTyp (*)())EchoInt );
	  tmp1 = Reverse_list( Join_list(tmp2,tmp1) );
	  Print_msg( tmp1, proc);
	  Disp_list( tmp1 );
	  found = TRUE;
	}
	else {
	  if (!guard) {
	    if (!LookForBST((DataBstTyp)proc,exploredSearch,EchoInt,EqInt))
	      exploredSearch = InsertBST((DataBstTyp)proc,exploredSearch,
					 EchoInt);
	    else
	      found = FALSE;
	  }
	  if ( ! In_list((DataListTyp) pdef, dp2, EqInt) ) {
	    dp2   = Insert_list( (DataListTyp) pdef, dp2);
	    found = Search_proc_aux(GetP_def(pdef), proc,dp1,dp2,guard);
	    dp2   = DeleteNode_list(dp2, dp2);
	  }
	}
	break;

      case GateC:
	if ( LookAInfo(LookA(b,PA))!=NULL )
	  found = Search_proc_aux( LookArgB(b,1), proc, dp1, dp2, TRUE);
	else
	  found = Search_proc_aux( LookArgB(b,1),proc, dp1, dp2, guard);
	break;

      case GuardC:
	found = Search_proc_aux( LookArgB(b,1), proc, dp1, dp2, TRUE);
	break;

      default:
	argnum = NumArgB(b);
	for ( i=1; (i<=argnum) &&
	     ! ( found = Search_proc_aux(LookArgB(b,i),proc,dp1, dp2, guard));
	     ++i )
	  ;
      }
  return (found);
}


/* Search_proc
 * Searchs a possible divergent behaviour for the process instantiation
 * proc. If found it informs the user of which type of divergence occured,
 * i.e. if the process was proceeded by a guard or not. dp1 + dp2 is the path.
 */
static boolean Search_proc( b, proc, dp1, dp2, guard )
     BehTyp b;
     DescriptorTyp proc;
     ListTyp dp1, dp2;
     boolean guard;
{
  boolean res;

  exploredSearch = CreateBST();
  res = Search_proc_aux( b, proc, dp1, dp2, guard );
  FreeBST( exploredSearch , (void(*)())NULL );
  return res;
}

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

static void Diverge( b, proc, dp, guard )
     BehTyp b;
     DescriptorTyp proc;
     ListTyp dp;
     boolean guard;
{
  DescriptorTyp pdef;
  int argnum, i;

  if (b)
    switch( LookTypeB(b) )
      {
      case ProcessInstC:
      case ProcessDefC:
	pdef = LookNameB(b);
	if (!guard) {
	  if (!LookForBST((DataBstTyp)proc,exploredDiverge,EchoInt,EqInt))
	    exploredDiverge = InsertBST((DataBstTyp)proc,exploredDiverge,
					EchoInt);
	  else
	    break;
	}
	if ( ! In_list( (DataListTyp) pdef, dp, EqInt) ) {
	  dp = Insert_list( (DataListTyp) pdef, dp );
	  Diverge( LookArgB(GetP_def(pdef),1), proc, dp, guard );
	  dp = DeleteNode_list( dp, dp );
	}
	break;

      case ParallelC:
	if ( Search_proc( LookArgB(b,1), proc, dp, (ListTyp)NULL, guard ) )
	  ;
	else
	  (void)Search_proc( LookArgB(b,2), proc, dp, (ListTyp)NULL, guard );
	break;

      case EnablingC:
      case DisablingC:
	(void)Search_proc( LookArgB(b,1), proc, dp, (ListTyp)NULL, guard );
	Diverge( LookArgB(b,1), proc, dp, guard );
	break;

      case GateC:
	if ( LookAInfo(LookA(b, PA)) != NULL )
	  Diverge( LookArgB(b,1), proc, dp, TRUE );
	else
	  Diverge( LookArgB(b,1), proc, dp, guard );
	break;

      case GuardC:
	Diverge( LookArgB(b,1), proc, dp, TRUE );
	break;

      default:
	argnum = NumArgB(b);
	for ( i=1; i<=argnum; ++i )
	  Diverge( LookArgB(b,i), proc, dp, guard );
      }
}

/* CheckDiverge
 * Checks a behaviour for divergence. If possible divergence is found calls
 * Search_proc.
 */
static void CheckDiverge( b, proc, dp, guard )
     BehTyp b;
     DescriptorTyp proc;
     ListTyp dp;
     boolean guard;
{
  exploredDiverge = CreateBST();
  Diverge( b, proc, dp, guard );
  FreeBST( exploredDiverge , (void(*)())NULL );
}


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

/* Unguard
 * Checks if a behaviour is unguarded. If it is, it informs the user of which
 * type, i.e. if the process was proceeded by a guard or not. dp is the path.
 */
static void Unguard( b, proc, dp, guard )
     BehTyp b;
     DescriptorTyp proc;
     ListTyp dp;
     boolean guard;
{
  DescriptorTyp pdef;
  int argnum, i;
  ListTyp tmp;

  if (b)
    switch( LookTypeB(b) )
      {
      case ProcessDefC:
	dp = Insert_list( (DataListTyp) LookNameB(b), dp );
	Unguard( LookArgB(b,1), proc, dp, guard );
	dp = DeleteNode_list( dp, dp );
	break;

      case ProcessInstC:
	pdef = LookNameB(b);
	if ( pdef == proc ) {
	  unguardedProcesses = InsertBST( (DataBstTyp)proc,
					 unguardedProcesses,
					 EchoInt
					 );
	  usedNodes++;
	  if (guard)
	    Warning("Possible unguarded behaviour. ");
	  else
	    Warning("Unguarded behaviour. ");
	  tmp = Copy_list( dp, (DataListTyp (*) ())EchoInt );
	  tmp = Reverse_list(tmp);
	  Print_msg( tmp, proc );
	  Disp_list(tmp);
	}
	else
	  if (! In_list( (DataListTyp) pdef, dp, EqInt) ) {
	    dp = Insert_list( (DataListTyp) pdef, dp );
	    Unguard( LookArgB(GetP_def(pdef),1), proc, dp, guard );
	    dp = DeleteNode_list( dp, dp );
	  }
	break;

      case GateC:
      case IC:
	break;
      case EnablingC:
	Unguard( LookArgB(b,1), proc, dp, guard );
	break;

      case GuardC:
	Unguard( LookArgB(b,1), proc, dp, TRUE );
	break;

      default:
	argnum = NumArgB(b);
	for ( i=1; i<=argnum; ++i )
	  Unguard( LookArgB(b,i), proc, dp, guard );
      }
}


/* Expandable
 * Checks if the processes of the specification are possible to expand,
 * i.e. they do not diverge nor are unguarded.
 * If the specification is not expandable then this function will inform
 * the user why not.
 * divergence  : divergence analysis check
 * unguardance : unuarded process detection
 */
void Expandable( divergence, unguardance )
     boolean divergence, unguardance;
{

  DescriptorTyp i;
  BehTyp        b;
  char          buff[1024];


  if ( divergence && first_time_div) {
    printMsgs(" Analysing divergence conditions.\n");
    for ( i=2 ; i<=LastTableP() ; i++ ) {
      b = GetP_def(i);
      if (runtimeConfig==TextMode) {
	(void)sprintf(buff,"\015%5d = %-71s",i,GetP_name(i));
	LASSERT(strlen(buff)<1024);
	printMsgs(buff);
      }
      else {
	(void)sprintf(buff,"%5d = %-71s",i,GetP_name(i));
	LASSERT(strlen(buff)<1024);
	printPos(buff,-2);
	flushTarget();
      }
      CheckDiverge( b, LookNameB(b), Create_list(), FALSE );
    }
    if (runtimeConfig==TextMode) {
      (void)sprintf(buff,"\015 %-78s\n\n","Analysis done.");
      printMsgs(buff);
    }
    else {
      (void)sprintf(buff," %-78s\n\n","Analysis done.");
      printPos(buff,-2);
      flushTarget();
    }
    first_time_div = FALSE;
  }

  if ( unguardance && first_time_ung) {
    printMsgs(" Analysing unguarded conditions.\n");
    for ( i=2 ; i<=LastTableP() ; i++ ) {
      b = GetP_def(i);
      if (runtimeConfig==TextMode) {
	(void)sprintf(buff,"\015%5d = %-71s",i,GetP_name(i));
	LASSERT(strlen(buff)<1024);
	printMsgs(buff);
      }
      else {
	(void)sprintf(buff,"%5d = %-71s",i,GetP_name(i));
	LASSERT(strlen(buff)<1024);
	printPos(buff,-2);
	flushTarget();
      }
      Unguard( b, LookNameB(b), Create_list(), FALSE );
    }
    if (runtimeConfig==TextMode) {
      (void)sprintf(buff,"\015 %-78s\n\n","Analysis done.");
      printMsgs(buff);
    }
    else {
      (void)sprintf(buff," %-78s\n\n","Analysis done.");
      printPos(buff,-2);
      flushTarget();
    }
    first_time_ung = FALSE;
  }

  return;
}


/* InitDiver
 * Initializes this module.
 * This function must be called when a new specification is loaded.
 */
void InitDiver()
{
  first_time_div = first_time_ung = TRUE;
  if ( !IsEmptyBST(unguardedProcesses) )
    FreeBST( unguardedProcesses, (void(*)())EchoInt );
  unguardedProcesses = CreateBST();
  usedNodes = 0;
}

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

/* IsUnguardedProc
 * Says if a process p is unguarded
 */
boolean IsUnguardedProc( p )
     DescriptorTyp p;
{
  return LookForBST( (DataBstTyp)p, unguardedProcesses, EchoInt, EqInt )!=NULL;
}

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

/* StatDiver
 * Statistic on used BST nodes.
 */
int StatDiver()
{
  return usedNodes;
}

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

/* UngProcBAct
 * Auxiliary function for UngProcBefAct
 */
static boolean UngProcBAct( b )
     BehTyp b;
{
  int n;

  if (IsEmptyBST(unguardedProcesses))
    return FALSE;
  while ( b != NULL ) {
    if ( VisitedB(b) )
      return FALSE;
    switch ( LookTypeB(b) )
      {
      case ProcessInstC :
	if (IsUnguardedProc(LookNameB(b)))
	  return TRUE;
	else
	  b = LookArgB(GetP_def(LookNameB(b)),1);
	break;

      case GateC:
      case ExitC:
      case StopC:
      case TerminationC:
	return FALSE;

      case IC:
	if (!IS_WEAK_EQUIV_EXP)
	  return FALSE;
	else
	  b = LookArgB(b,1);
	break;

      case RelabellingC :
      case HidingC :
      case ChoiceC :
      case PletC :
      case LetC :
      case GuardC :
      case GateChoiceC :
      case ParC:
	b = LookArgB(b,1);
	break;

      case InterleavedC:
      case EnablingC:
      case DisablingC:
      case ParallelC:
	if (UngProcBAct( LookArgB(b,1) ))
	  return TRUE;
	else
	  b = LookArgB(b,2);
	break;

      case AlternativeC:
	for ( n=NumArgB(b) ; n>1 ; n-- )
	  if (UngProcBAct( LookArgB(b,n) ))
	    return TRUE;
	b = LookArgB(b,1);
	break;

      default: Error("UngProcBefAct : Unexpected cell.");
      }
  }
  return FALSE; /*lint*/
}


/* UngProcBefAct
 * Returns TRUE if in the behaviour "b" there are any instantiation to
 * an unguarded process.
 * This exploration ends at the actions.
 */
boolean UngProcBefAct( b )
     BehTyp b;
{
  boolean thereIs;

  Begin_VisitB();
  thereIs = UngProcBAct( b );
  End_VisitB();

  return thereIs;
}
