Skip to content
Snippets Groups Projects
Select Git revision
  • Lip6-2025
  • avatarSysML_Graphics
  • avatarSysML_04_2024
  • master default protected
  • alan_attack_tree_gen
  • tags
  • separate_simulator
  • tests_explo
  • debug_simulator_07_2024
  • auto-security-diplodocus
  • correction_timeline_display
  • fix-tml2Avatar-translator
  • WSec2
  • WSec
  • tml2AvatarTranslation
  • parser_06_2023
  • auto-sec-diplodocus
  • JURASSIC
  • avatar_security_tests
  • revert-d2eab2e7
20 results
Blame Permalink
spec_5.h 18.00 KiB 
/*** generated by caesar.adt 5.2 with options -cc "" ***/

#define CAESAR_ADT 5.2

#include <stdio.h>
#include <signal.h>
#include <string.h>
#include <stdlib.h>

#ifndef CAESAR_ADT_ALLOC

#ifndef CAESAR_ADT_GARBAGE_COLLECTION
#define GC_malloc(CAESAR_ADT_0) malloc(CAESAR_ADT_0)
#else
extern char *GC_malloc ();
#endif

#define CAESAR_ADT_ALLOC(CAESAR_ADT_0,CAESAR_ADT_BODY,CAESAR_ADT_TYPE,CAESAR_ADT_LOTOS_OPERATION,CAESAR_ADT_C_FUNCTION) if (((CAESAR_ADT_0) = (CAESAR_ADT_TYPE) GC_malloc (sizeof (CAESAR_ADT_BODY))) == NULL) {printf ("#249 erreur dans le fichier ``.h'' :\n     penurie de memoire pour les types abstraits\n     dans l'operation %s\n     implementee par la fonction %s [%s:%d]\n", CAESAR_ADT_LOTOS_OPERATION, CAESAR_ADT_C_FUNCTION, __FILE__, __LINE__); raise (15); }

#endif

#ifndef CAESAR_ADT_ERROR
#define CAESAR_ADT_ERROR(CAESAR_ADT_LOTOS_OPERATION,CAESAR_ADT_C_FUNCTION) if (1) {printf ("#250 erreur dans le fichier ``.h'' :\n     cas imprevu (non defini par les equations)\n     dans l'operation %s\n     implementee par la fonction %s [%s:%d]\n", CAESAR_ADT_LOTOS_OPERATION, CAESAR_ADT_C_FUNCTION, __FILE__, __LINE__); raise (15); } else
#endif

/* LINTLIBRARY */

/* ========================================================================= */

#define CAESAR_ADT_UNCANONICAL_CAESAR_ADT_TYPE_QUEUE_NAT

#define CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT(CAESAR_ADT_0) (*(CAESAR_ADT_0))

#define CAESAR_ADT_SCALAR_CAESAR_ADT_TYPE_QUEUE_NAT

 /* forward */ typedef struct CAESAR_ADT_STRUCT_CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_TYPE_QUEUE_NAT);
 /* forward */ int CAESAR_ADT_CMP_QUEUE_NAT ();
 /* forward */ void CAESAR_ADT_PRT_QUEUE_NAT ();

/* ========================================================================= */

typedef unsigned char ADT_BOOL;

#define CAESAR_ADT_SCALAR_ADT_BOOL

#define CAESAR_ADT_BITS_ADT_BOOL : 1

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

#define ADT_FALSE() ((ADT_BOOL) 0)
#define ADT_TRUE() ((ADT_BOOL) 1)

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

#define ADT_CMP_BOOL(CAESAR_ADT_1,CAESAR_ADT_2) ((CAESAR_ADT_1) == (CAESAR_ADT_2))

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

#ifdef CAESAR_ADT_INTERFACE

extern char *CAESAR_ADT_ASCII_ADT_BOOL[];

#else

char *CAESAR_ADT_ASCII_ADT_BOOL[] = {
     "FALSE",
     "TRUE"
};

#endif				/* CAESAR_ADT_INTERFACE */

#define ADT_PRINT_BOOL(CAESAR_ADT_FILE,CAESAR_ADT_0) fprintf (CAESAR_ADT_FILE, CAESAR_ADT_ASCII_ADT_BOOL [CAESAR_ADT_0])

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

#define CAESAR_ADT_is_ADT_FALSE(CAESAR_ADT_0) ((CAESAR_ADT_0) == ADT_FALSE())
#define CAESAR_ADT_is_ADT_TRUE(CAESAR_ADT_0) ((CAESAR_ADT_0) == ADT_TRUE())

/* ========================================================================= */

#include "spec_1.t"

#define CAESAR_ADT_INCLUDE_T

/* CAUTION: there exists C types, comparison functions, enumeration functions and printing macros that can not be generated automatically by CAESAR.ADT, since the corresponding LOTOS sorts have no constructors. These C objects will be considered as extern and it is assumed that their definition is contained in file "spec_1.t" provided by the user. The list of these objects is given below: */

/* (1) the type ADT_NAT implementing sort NAT */
/* (2) the comparison function ADT_CMP_NAT for sort NAT */
/* (3) the enumeration macro ADT_ENUM_FIRST_NAT for sort NAT */
/* (4) the enumeration macro ADT_ENUM_NEXT_NAT for sort NAT */
/* (5) the printing function ADT_PRINT_NAT for sort NAT */
/* (6) the function ADT_N0 implementing constructor 0 */
/* (7) the testor function CAESAR_ADT_is_ADT_N0 for constructor 0 */
/* (8) the function ADT_SUCC implementing constructor SUCC */
/* (9) the testor function CAESAR_ADT_is_ADT_SUCC for constructor SUCC */
/* (10) the selector #1 function CAESAR_ADT_Get_1_ADT_SUCC for constructor SUCC */

/* ========================================================================= */

#ifndef ADT_ENUM_FIRST_BOOL
#define ADT_ENUM_FIRST_BOOL() (ADT_FALSE())
#endif

#ifndef ADT_ENUM_NEXT_BOOL
#define ADT_ENUM_NEXT_BOOL(CAESAR_ADT_0) ((CAESAR_ADT_0)++ < ADT_TRUE())
#endif

/* ========================================================================= */

#define CAESAR_ADT_CASE_NIL ((unsigned char) 0)
#define CAESAR_ADT_CASE_ENQUEUE ((unsigned char) 1)

typedef struct CAESAR_ADT_STRUCT_CAESAR_ADT_TYPE_QUEUE_NAT {
     unsigned char CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT:1;
     union {
	  struct {
	       ADT_NAT CAESAR_ADT_1_ENQUEUE
#ifdef CAESAR_ADT_BITS_ADT_NAT
	            CAESAR_ADT_BITS_ADT_NAT
#endif
	           ;
	       CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2_ENQUEUE
#ifdef CAESAR_ADT_BITS_CAESAR_ADT_TYPE_QUEUE_NAT
	            CAESAR_ADT_BITS_CAESAR_ADT_TYPE_QUEUE_NAT
#endif
	           ;
	  } CAESAR_ADT_FIELD_ENQUEUE;
     } CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT;
} CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT;

/* ========================================================================= */

#ifndef CAESAR_ADT_INTERFACE

int CAESAR_ADT_CMP_QUEUE_NAT (CAESAR_ADT_1, CAESAR_ADT_2)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
     if ((CAESAR_ADT_1 == NULL) || (CAESAR_ADT_2 == NULL))
	  return (CAESAR_ADT_1 == CAESAR_ADT_2);
     if (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT != CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT)
	  return 0;
     switch (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT) {
     case CAESAR_ADT_CASE_NIL:
	  return 1;
     case CAESAR_ADT_CASE_ENQUEUE:
	  return ADT_CMP_NAT (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE) && CAESAR_ADT_CMP_QUEUE_NAT (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_1).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_2).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE);
     }
     /* NOTREACHED */
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

void CAESAR_ADT_PRT_QUEUE_NAT (CAESAR_ADT_FILE, CAESAR_ADT_0)
FILE *CAESAR_ADT_FILE;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0;
{
     if (CAESAR_ADT_0 == NULL)
	  fprintf (CAESAR_ADT_FILE, "?");
     else {
	  switch (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT) {
	  case CAESAR_ADT_CASE_NIL:
	       fprintf (CAESAR_ADT_FILE, "NIL");
	       break;
	  case CAESAR_ADT_CASE_ENQUEUE:
	       fprintf (CAESAR_ADT_FILE, "ENQUEUE (");
	       ADT_PRINT_NAT (CAESAR_ADT_FILE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE);
	       fprintf (CAESAR_ADT_FILE, ", ");
	       CAESAR_ADT_PRT_QUEUE_NAT (CAESAR_ADT_FILE, CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE);
	       fprintf (CAESAR_ADT_FILE, ")");
	       break;
	  }
     }
}

#endif				/* CAESAR_ADT_INTERFACE */

/* ========================================================================= */

#ifdef CAESAR_ADT_INTERFACE

extern CAESAR_ADT_TYPE_QUEUE_NAT NIL ();

#else

CAESAR_ADT_TYPE_QUEUE_NAT NIL ()
{
     static CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0 = NULL;
     if (CAESAR_ADT_0 == NULL) {
	  CAESAR_ADT_ALLOC (CAESAR_ADT_0, CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT, CAESAR_ADT_TYPE_QUEUE_NAT, "NIL [8]", "NIL");
	  CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT = CAESAR_ADT_CASE_NIL;
     }
     return CAESAR_ADT_0;
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifdef CAESAR_ADT_INTERFACE

extern CAESAR_ADT_TYPE_QUEUE_NAT ENQUEUE ();

#else

CAESAR_ADT_TYPE_QUEUE_NAT ENQUEUE (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
     CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_0;
     CAESAR_ADT_ALLOC (CAESAR_ADT_0, CAESAR_ADT_BODY_CAESAR_ADT_TYPE_QUEUE_NAT, CAESAR_ADT_TYPE_QUEUE_NAT, "ENQUEUE [9]", "ENQUEUE");
     CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT = CAESAR_ADT_CASE_ENQUEUE;
     CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE = CAESAR_ADT_1;
     CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE = CAESAR_ADT_2;
     return CAESAR_ADT_0;
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#define CAESAR_ADT_is_NIL(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT == CAESAR_ADT_CASE_NIL)
#define CAESAR_ADT_is_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_ENUM_CAESAR_ADT_TYPE_QUEUE_NAT == CAESAR_ADT_CASE_ENQUEUE)
#define CAESAR_ADT_Get_1_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_1_ENQUEUE)
#define CAESAR_ADT_Get_2_ENQUEUE(CAESAR_ADT_0) (CAESAR_ADT_STAR_CAESAR_ADT_TYPE_QUEUE_NAT (CAESAR_ADT_0).CAESAR_ADT_UNION_CAESAR_ADT_TYPE_QUEUE_NAT.CAESAR_ADT_FIELD_ENQUEUE.CAESAR_ADT_2_ENQUEUE)

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

/* sort QUEUE_NAT is infinite: no iterator can be generated automatically for this sort; however, it is possible to specify manually an iterator for a finite subset of QUEUE_NAT by defining two macros CAESAR_ADT_ITR_FIRST_QUEUE_NAT() and CAESAR_ADT_ITR_NEXT_QUEUE_NAT() in file "spec_1.t" */

/* ========================================================================= */

 /* forward */ ADT_BOOL ADT_AND ();
 /* forward */ ADT_BOOL ADT_OR ();
 /* forward */ ADT_BOOL ADT_XOR ();
 /* forward */ ADT_BOOL ADT_IFF ();

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

 /* forward */ CAESAR_ADT_TYPE_QUEUE_NAT DEQUEUE ();
 /* forward */ ADT_NAT FIRST ();
 /* forward */ ADT_NAT LAST ();
 /* forward */ CAESAR_ADT_TYPE_QUEUE_NAT DESTROY ();

/* ========================================================================= */

#define ADT_NOT(CAESAR_ADT_1) (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_1) ? ADT_FALSE () : ADT_TRUE ())

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

#define ADT_IMPLIES(CAESAR_ADT_1, CAESAR_ADT_2) ADT_OR (CAESAR_ADT_2, ADT_NOT (CAESAR_ADT_1))

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

#define ADT_EQ_BOOL(CAESAR_ADT_1, CAESAR_ADT_2) ADT_IFF (CAESAR_ADT_1, CAESAR_ADT_2)

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

#define ADT_NE_BOOL(CAESAR_ADT_1, CAESAR_ADT_2) ADT_XOR (CAESAR_ADT_1, CAESAR_ADT_2)

/* ========================================================================= */

#define EMPTY(CAESAR_ADT_1) (CAESAR_ADT_is_NIL (CAESAR_ADT_1) ? ADT_TRUE () : ADT_FALSE ())

/* ========================================================================= */

#ifndef CAESAR_ADT_INTERFACE

#include "spec_1.f"

#define CAESAR_ADT_INCLUDE_F

#endif				/* CAESAR_ADT_INTERFACE */

/* CAUTION: there exists C functions that can not be generated automatically by CAESAR.ADT, since the corresponding LOTOS (non-constructor) operations are not defined by equations. These C functions will be considered as extern and it is assumed that their definition is contained in file "spec_1.f" provided by the user. The list of these functions is given below: */

/* (1) the function ADT_PLUS implementing operation + */
/* (2) the function ADT_MULT implementing operation * */
/* (3) the function ADT_POWER implementing operation ** */
/* (4) the function ADT_EQ_NAT implementing operation EQ */
/* (5) the function ADT_NE_NAT implementing operation NE */
/* (6) the function ADT_LT_NAT implementing operation LT */
/* (7) the function ADT_LE_NAT implementing operation LE */
/* (8) the function ADT_GT_NAT implementing operation GT */
/* (9) the function ADT_GE_NAT implementing operation GE */
/* (10) the function ADT_N1 implementing operation 1 */
/* (11) the function ADT_N2 implementing operation 2 */
/* (12) the function ADT_N3 implementing operation 3 */
/* (13) the function ADT_N4 implementing operation 4 */
/* (14) the function ADT_N5 implementing operation 5 */
/* (15) the function ADT_N6 implementing operation 6 */
/* (16) the function ADT_N7 implementing operation 7 */
/* (17) the function ADT_N8 implementing operation 8 */
/* (18) the function ADT_N9 implementing operation 9 */
/* (19) the function ADT_MINUS implementing operation - */
/* (20) the function ADT_DIV implementing operation DIV */
/* (21) the function ADT_MOD implementing operation MOD */
/* (22) the function ADT_EQ_BIS_NAT implementing operation == */
/* (23) the function ADT_NE_BIS_NAT implementing operation <> */
/* (24) the function ADT_LT_BIS_NAT implementing operation < */
/* (25) the function ADT_LE_BIS_NAT implementing operation <= */
/* (26) the function ADT_GT_BIS_NAT implementing operation > */
/* (27) the function ADT_GE_BIS_NAT implementing operation >= */
/* (28) the function ADT_MIN implementing operation MIN */
/* (29) the function ADT_MAX implementing operation MAX */
/* (30) the function ADT_GCD implementing operation GCD */
/* (31) the function ADT_SCM implementing operation SCM */

/* ========================================================================= */

#ifndef CAESAR_ADT_INTERFACE

ADT_BOOL ADT_AND (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
     if (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_2))
	  return CAESAR_ADT_1;
     else
	  return CAESAR_ADT_2;
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

ADT_BOOL ADT_OR (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
     if (CAESAR_ADT_is_ADT_TRUE (CAESAR_ADT_2))
	  return CAESAR_ADT_2;
     else
	  return CAESAR_ADT_1;
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

ADT_BOOL ADT_XOR (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
     return ADT_OR (ADT_AND (CAESAR_ADT_1, ADT_NOT (CAESAR_ADT_2)), ADT_AND (CAESAR_ADT_2, ADT_NOT (CAESAR_ADT_1)));
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

ADT_BOOL ADT_IFF (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_BOOL CAESAR_ADT_1;
ADT_BOOL CAESAR_ADT_2;
{
     return ADT_AND (ADT_IMPLIES (CAESAR_ADT_1, CAESAR_ADT_2), ADT_IMPLIES (CAESAR_ADT_2, CAESAR_ADT_1));
}

#endif				/* CAESAR_ADT_INTERFACE */

/* ========================================================================= */

#ifndef CAESAR_ADT_INTERFACE

CAESAR_ADT_TYPE_QUEUE_NAT DEQUEUE (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
     if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
	  if (CAESAR_ADT_is_NIL (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)))
	       return NIL ();
	  else if (ADT_NOT (EMPTY (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1))))
	       return ENQUEUE (CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1), DEQUEUE (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)));
	  else
	       CAESAR_ADT_ERROR ("DEQUEUE [10]", "DEQUEUE");
     else
	  CAESAR_ADT_ERROR ("DEQUEUE [10]", "DEQUEUE");
     /* NOTREACHED */
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

ADT_NAT FIRST (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
     if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
	  if (CAESAR_ADT_is_NIL (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1)))
	       return CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1);
	  else if (ADT_NOT (EMPTY (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1))))
	       return FIRST (CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_1));
	  else
	       CAESAR_ADT_ERROR ("FIRST [12]", "FIRST");
     else
	  CAESAR_ADT_ERROR ("FIRST [12]", "FIRST");
     /* NOTREACHED */
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

ADT_NAT LAST (CAESAR_ADT_1)
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_1;
{
     if (CAESAR_ADT_is_ENQUEUE (CAESAR_ADT_1))
	  return CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_1);
     else
	  CAESAR_ADT_ERROR ("LAST [13]", "LAST");
     /* NOTREACHED */
}

#endif				/* CAESAR_ADT_INTERFACE */

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

#ifndef CAESAR_ADT_INTERFACE

CAESAR_ADT_TYPE_QUEUE_NAT DESTROY (CAESAR_ADT_1, CAESAR_ADT_2)
ADT_NAT CAESAR_ADT_1;
CAESAR_ADT_TYPE_QUEUE_NAT CAESAR_ADT_2;
{
     if (CAESAR_ADT_is_NIL (CAESAR_ADT_2))
	  return CAESAR_ADT_2;
     else if (ADT_EQ_NAT (CAESAR_ADT_1, CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2)))
	  return DESTROY (CAESAR_ADT_1, CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_2));
     else if (ADT_NE_NAT (CAESAR_ADT_1, CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2)))
	  return ENQUEUE (CAESAR_ADT_Get_1_ENQUEUE (CAESAR_ADT_2), DESTROY (CAESAR_ADT_1, CAESAR_ADT_Get_2_ENQUEUE (CAESAR_ADT_2)));
     else
	  CAESAR_ADT_ERROR ("DESTROY [14]", "DESTROY");
     /* NOTREACHED */
}

#endif				/* CAESAR_ADT_INTERFACE */

/* ========================================================================= */

#ifndef CAESAR_ADT_INTERFACE

void CAESAR_ADT_INIT ()
{
}

#endif				/* CAESAR_ADT_INTERFACE */

/* ========================================================================= */