/**
  *
  *                      OOAS Compiler
  *
  *       Copyright 2015, AIT Austrian Institute of Technology.
  * This code is based on the C# Version of the OOAS Compiler, which is
  * copyright 2015 by the Institute of Software Technology, Graz University
  * of Technology with portions copyright by the AIT Austrian Institute of
  * Technology. All rights reserved.
  *
  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
  *
  * If you modify the file please update the list of contributors below to in-
  * clude your name. Please also stick to the coding convention of using TABs
  * to do the basic (block-level) indentation and spaces for anything after
  * that. (Enable the display of special chars and it should be pretty obvious
  * what this means.) Also, remove all trailing whitespace.
  *
  * Contributors:
  *               Willibald Krenn (AIT)
  *               Stephan Zimmerer (AIT)
  *               Markus Demetz (AIT)
  *               Christoph Czurda (AIT)
  *
  */


package org.momut.ooas.codegen.cadp;

import java.util.ArrayList;
import java.util.Date;
import java.util.List;

import org.momut.ooas.Version;
import org.momut.ooas.ast.identifiers.AttributeIdentifier;
import org.momut.ooas.ast.identifiers.FunctionIdentifier;
import org.momut.ooas.ast.identifiers.Identifier;
import org.momut.ooas.ast.identifiers.IdentifierKind;
import org.momut.ooas.ast.identifiers.MainModule;
import org.momut.ooas.ast.identifiers.MethodIdentifier;
import org.momut.ooas.ast.identifiers.NamedActionIdentifier;
import org.momut.ooas.ast.identifiers.ParameterIdentifier;
import org.momut.ooas.ast.identifiers.TypeIdentifier;
import org.momut.ooas.ast.statements.Block;
import org.momut.ooas.ast.types.FunctionType;
import org.momut.ooas.ast.types.OoActionSystemType;
import org.momut.ooas.ast.types.Type;
import org.momut.ooas.ast.types.FunctionType.FunctionTypeEnum;
import org.momut.ooas.codegen.OoasCodeEmitter;
import org.momut.ooas.parser.ParserState;
import org.momut.ooas.visitors.OoaCompleteAstTraversalVisitor;


/*
 * OoaCADPVisitor
 *
 */

public final class OoaCADPVisitor extends OoaCompleteAstTraversalVisitor
{
	final static int s_codeGenVersion = 10;

	private OoasCodeEmitter m_output;
	private final List<AttributeIdentifier> m_statevector;
	private final int GraphImplementationVersion = 24;
	private final List<NamedActionIdentifier> actions = new ArrayList<NamedActionIdentifier>();
	private final List<MethodIdentifier> methods = new ArrayList<MethodIdentifier>();
//	private final String m_AttributePre;
	public int m_internalActionNumber = 0;

	public static int getUIntHashCode(Object o) {
		int hash = o.hashCode();
		if (hash >= 0)
			return hash;
		if (hash == Integer.MIN_VALUE)
			hash +=1;
		return -hash;
	}

	/// <summary>
	/// Dumps a comment containing all the version information
	/// </summary>
	private void DumpHeader(OoasCodeEmitter m_output)
	{
		m_output.AppendLine();
		m_output.AppendLine("/* Argos Generated");
		m_output.AppendLine(Version.asString());
		m_output.AppendLine(String.format(" Code-Gen Version: %s", s_codeGenVersion));
		m_output.Append("        Generated: "); m_output.AppendLine((new Date()).toString());
		m_output.AppendLine("------------------------------------------------------------------------");
		m_output.AppendLine();
		m_output.AppendLine("    assumed data-type sizes:");
		for( final String x : CadpType.sizeOfTypes().keySet())
		m_output.AppendLine(String.format("%s: %s", new Object[] { x, CadpType.sizeOfTypes().get(x).toString() }));
		m_output.AppendLine("");
		m_output.AppendLine("------------------------------------------------------------------------");
		m_output.AppendLine("------------------------------------------------------------------------");
		m_output.AppendLine("*/");
	}

	/// <summary>
	/// Prints out general definitions, includes
	/// </summary>
	private void DumpDefinitions(OoasCodeEmitter m_output)
	{
		// write Graph version and include header
		m_output.AppendLine("/*define next symbol if you want to see named internal actions (otherwise they are mapped to 'i')*/");
		m_output.AppendLine("#define ALL_ACTIONS_VISIBLE");
		m_output.AppendLine("/*define next symbol if you need to re-eval internal (hidden) states - attention: memory leaks*/");
		m_output.AppendLine("//#define UNLIMITED_REEVAL");
		m_output.AppendLine(String.format("#define CAESAR_GRAPH_IMPLEMENTATION %s", GraphImplementationVersion));
		m_output.AppendLine("#include \"caesar_graph.h\"");
		m_output.AppendLine("#include \"argos_runtime.h\"");
		m_output.AppendLine("#if defined(unix) || defined(__MACH__)");
		m_output.AppendLine("#define UNIXPACK __attribute__((__packed__))");
		m_output.AppendLine("#undef WINDOWSPACK");
		m_output.AppendLine("#include <netinet/in.h>");
		m_output.AppendLine("#else");
		m_output.AppendLine("#include <winsock.h>");
		m_output.AppendLine("#define WINDOWSPACK");
		m_output.AppendLine("#define UNIXPACK");
		m_output.AppendLine("#endif");

		m_output.AppendLine("  typedef unsigned long CAESAR_TYPE_WORD;");
		m_output.AppendLine("  #define CAESAR_WORD_SIZE (sizeof (CAESAR_TYPE_WORD))");
		m_output.AppendLine("  #define CAESAR_FULL_MASK ((CAESAR_TYPE_WORD) ~0)");

		m_output.AppendLine("");
		m_output.AppendLine("unsigned char  CALC_INVALID = 0;");

		m_output.AppendLine("");
		m_output.AppendLine("void CAESAR_TERMINATE (int CAESAR_ABORT)");
		m_output.AppendLine("{printf(\"aborted...\"); abort();}");
		m_output.AppendLine("");
	}
	/// <summary>
	/// Prints out compiler String
	/// </summary>
	private void DumpCompilerString()
	{
		m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_GRAPH_COMPILER ()");
		lp();
		m_output.AppendLine("  return (\"ARGOS\");");
		rp();
	}

	/// <summary>
	/// Prints out compiler version
	/// </summary>
	private void DumpCompilerVersion()
	{
		m_output.AppendLine("CAESAR_TYPE_VERSION CAESAR_GRAPH_VERSION ()");
		lp();
		m_output.AppendLine("            return (" + Version.s_releaseMajor + "." + Version.s_releaseMinor + ");");
		rp();
	}
	/// <summary>
	/// Exports a function returning the maximum number of formats for states.
	/// Exports a const for the default format.
	/// Exports a function CAESAR_FORMAT_STATE (default cadp implementation).
	/// </summary>
	private void DumpFormat()
	{
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_MAX_FORMAT_STATE ()");
		lp();
		m_output.AppendLine(" return (0);");
		rp();

		line();
		m_output.AppendLine("static CAESAR_TYPE_NATURAL CAESAR_CURRENT_STATE_FORMAT = 0;");


		line();
		m_output.AppendLine("void CAESAR_FORMAT_STATE (CAESAR_TYPE_NATURAL CAESAR_FORMAT)");
		lp();
		m_output.AppendLine("  if (CAESAR_FORMAT > CAESAR_MAX_FORMAT_STATE ()) ");
		m_output.AppendLine("    printf(\"#233 bug during simulation:\\n     unknown state printing format\\n\");");
		m_output.AppendLine("  else");
		m_output.AppendLine("    CAESAR_CURRENT_STATE_FORMAT = CAESAR_FORMAT;");
		m_output.AppendLine("}");
	}


	/// <summary>
	/// Exports a function to print a state header. (standard cadp implementation)
	/// </summary>
	private void DumpStateHeader()
	{
		m_output.AppendLine("void CAESAR_PRINT_STATE_HEADER (CAESAR_TYPE_FILE CAESAR_FILE)");
		m_output.AppendLine("{");
		m_output.AppendLine("  switch (CAESAR_CURRENT_STATE_FORMAT) {");
		m_output.AppendLine("  case 0:");
		m_output.Append("    fprintf (CAESAR_FILE, \"\\t marquage = {\");");
		m_output.AppendLine("    fprintf (CAESAR_FILE, \"unite 0}\\n\");");
		m_output.AppendLine("    break;");
		m_output.AppendLine("  default:");
		m_output.AppendLine("  {");
		m_output.AppendLine("    printf(\"#233 bug during simulation:\\n     unknown state printing format\\n\");");
		m_output.AppendLine("  }");
		m_output.AppendLine("  break;");
		m_output.AppendLine("  }");
		m_output.AppendLine("}");
	}




	/// <summary>
	/// Main Routine, dumps an action system
	/// </summary>
	/// <param name="ooActionSystemType">action system to write out</param>
	private void Dump(OoActionSystemType ooActionSystemType)
	{


		// write name of type we print out.
		m_output.AppendLine();
		m_output.Append("/* Type: "); m_output.Append(ooActionSystemType.identifier().tokenText());
		m_output.AppendLine(" */");
		m_output.AppendLine();

		// export state variables
		DefineCadpState(ooActionSystemType);

		// export compiler String function
		line();
		DumpCompilerString();

		// export compiler version function
		line();
		DumpCompilerVersion();

		// export state comparison function
		line();
		DefineCompareCadpStates();

		// export a state hash function
		line();
		DefineCadpStateHash();


		line();
		DumpFormat();

		line();
		DumpStateHeader();

		line();
		DefineCadpPrintState();

		line();
		DefineCadpPrintDeltaState();


		line();
		DefineCadpLabel(ooActionSystemType);  // populates actions list

		line();
		m_output.AppendLine();
		m_output.AppendLine("typedef struct CAESAR_STRUCT_ALIGNMENT_LABEL {");
		m_output.AppendLine("  char CAESAR_BYTE;");
		m_output.AppendLine("  CAESAR_BODY_LABEL CAESAR_L;");
		m_output.AppendLine("} CAESAR_BODY_ALIGNMENT_LABEL;");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_ALIGNMENT_LABEL = sizeof (CAESAR_BODY_ALIGNMENT_LABEL) - sizeof (CAESAR_BODY_LABEL);");


		line();
		m_output.AppendLine();
		m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_VISIBLE_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
		m_output.AppendLine("{");
		m_output.AppendLine("  return 1;");
		m_output.AppendLine("}");


		line();
		m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_GATE_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
		lp();
		m_output.AppendLine(String.format("  if(CAESAR_L->CAESAR_TRANSITION_NUMBER < %1$s)", this.actions.size()));
		m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
		m_output.AppendLine("    return CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION ? CAESAR_GATE[INTERNAL_ACTION_NUMBER] : CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
		m_output.AppendLine("#else");
		m_output.AppendLine("    return CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
		m_output.AppendLine("#endif");
		m_output.AppendLine("  else");
		m_output.AppendLine("    {printf(\"#233 bug during simulation:\\n     unknown gate number\\n\"); CAESAR_TERMINATE(1);}");
		m_output.AppendLine(" return \"\";");
		rp();


		line();
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_CARDINAL_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
		lp();
		m_output.AppendLine(String.format("  if(CAESAR_L->CAESAR_TRANSITION_NUMBER < %1$s)", this.actions.size()));
		m_output.AppendLine("    return CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
		m_output.AppendLine("  else");
		m_output.AppendLine("    {printf(\"#233 bug during simulation:\\n     unknown gate number\\n\"); CAESAR_TERMINATE(1);}");
		m_output.AppendLine("return 0;");
		rp();


		line();
		DefineCadpGetStringLabel();


		line();
		DefineCadpCompareLabel();

		line();
		DefineCadpHashLabel();


		line();
		DefineCadpPrintLabel();


		line();
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_MAX_FORMAT_LABEL ()");
		lp();
		m_output.AppendLine("  return (0);");
		rp();
		m_output.AppendLine();
		m_output.AppendLine("static CAESAR_TYPE_NATURAL CAESAR_CURRENT_LABEL_FORMAT = 0;");



		line();
		m_output.AppendLine("void CAESAR_FORMAT_LABEL (CAESAR_TYPE_NATURAL CAESAR_FORMAT)");
		lp();
		m_output.AppendLine("  if (CAESAR_FORMAT > CAESAR_MAX_FORMAT_LABEL ()){");
		lp();
		m_output.AppendLine("    printf(\"#234 bug during simulation:\\n     unknown label printing format\\n\");");
		rp();
		rp(); m_output.Append(" else  CAESAR_CURRENT_LABEL_FORMAT = CAESAR_FORMAT;");
		rp();



		line();
		m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_INFORMATION_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
		lp();
		m_output.AppendLine("  static char CAESAR_RESULT [11];");
		m_output.AppendLine("  switch (CAESAR_CURRENT_LABEL_FORMAT) ");
		m_output.AppendLine("  {");
		m_output.AppendLine("    case 0:");
		m_output.AppendLine("      sprintf (CAESAR_RESULT, \"%u\", CAESAR_L->CAESAR_TRANSITION_NUMBER);");
		m_output.AppendLine("      return (CAESAR_RESULT);");
		m_output.AppendLine("    default:");
		m_output.AppendLine("    {");
		m_output.AppendLine("      printf(\"#234 bogue pendant la simulation :\\n     format d'impression inconnu pour les etiquettes\\n\");");
		m_output.AppendLine("    }");
		m_output.AppendLine("    return (\"\");");
		m_output.AppendLine("  }");
		rp();


		///
		///   START STATE
		///
		line();
		line();
		DefineCadpStartState();


		///
		///   Dump Methods
		///
		for (final MethodIdentifier method: methods)
		{
			line();
			m_output.AppendLine(String.format("  /* Code for method '%1$s' */", method.tokenText()));
			DefineCadpAction(method, -1);
		}




		///
		///   Dump Actions
		///
		int actnum = 0;
		for (final NamedActionIdentifier action : actions)
		{
			line();
			m_output.AppendLine(String.format("  /* Code for action '%1$s' */", action.tokenText()));
			DefineCadpAction(action, actnum);
			actnum++;
		}


		///
		///   ITERATE STATE
		///
		line();
		line();
		DefineCadpIterateState(ooActionSystemType);



		line();
		m_output.AppendLine("void CAESAR_INIT_GRAPH ()");
		lp();
		m_output.AppendLine("  CAESAR_CHECK_VERSION (2.4, 2.4);");
		rp();
		m_output.AppendLine();
	}

	@Override
	public  void visit(MainModule mainModule)
	{
		// define complex types
		DumpTypes(mainModule);

		// export action system
		Dump(mainModule.instance());
	}




//	private String GetIdentifierString(TypeIdentifier typeIdentifier)
//	{
//		return CadpIdentifier.GetIdentifierString(typeIdentifier);
//	}



	private void DumpTypes(MainModule mainModule)
	{
		for (final Identifier x: mainModule.symbolTable().symbolList())
		{
			if (x.kind() == IdentifierKind.TypeIdentifier)/* &&
				((TypeIdentifier)x).type.kind != TypeKind.OoActionSystemType)*/
			{
				final TypeIdentifier aTypeId = (TypeIdentifier)x;
				CadpType.EmitType(aTypeId.type());
			}
		}
	}

	public OoaCADPVisitor(ParserState aState)
	{
		super(aState);
		m_output = new OoasCodeEmitter();
		m_statevector = new ArrayList<AttributeIdentifier>();
//		m_AttributePre = "";

		// clear helpers
		CadpExpression.emittedOperations.clear();
	}


	@Override
	public  String toString()
	{
		final OoasCodeEmitter result = new OoasCodeEmitter();
		DumpHeader(result);           // comments, version
		DumpDefinitions(result);      // includes, definitions

		result.AppendLine(CadpType.GetTypeDefintions());
		result.AppendLine(cadpstate.toString());
		result.AppendLine(CadpExpression.GetHelperCode());
		result.AppendLine(m_output.toString());

		return result.toString();
	}






	private void line()
	{
		m_output.AppendLine();
		m_output.AppendLine("//----------------------------------------------------------------------");
	}
	private void rp()
	{
		m_output.AppendLine("}");
	}
	private void lp()
	{
		m_output.AppendLine("{");
	}


	public static String DumpType(Type atype)
	{
		final CadpType newtype = new CadpType();
		atype.Accept(newtype);
		return newtype.ToString();
	}


	/// <summary>
	/// Dumps a state variable (attribute)
	/// </summary>
	private void DumpAttribute(AttributeIdentifier attributeIdentifier)
	{
		m_output.Append(DumpType(attributeIdentifier.type()));
		m_output.Append(" ");
		m_output.Append(attributeIdentifier.tokenText());
		m_statevector.add(attributeIdentifier);
	}

	private final OoasCodeEmitter cadpstate = new OoasCodeEmitter();

	/// <summary>
	/// Exports the state of the ooActionSystem
	/// </summary>
	private void DefineCadpState(OoActionSystemType ooActionSystemType)
	{
		final OoasCodeEmitter tmp = m_output;
		m_output = cadpstate;

		m_output.AppendLine("typedef struct CAESAR_STRUCT_STATE CAESAR_BODY_STATE;");
		m_output.AppendLine("#ifdef WINDOWSPACK");
		m_output.AppendLine("#pragma pack(1)");
		m_output.AppendLine("#endif");
		m_output.AppendLine("struct CAESAR_STRUCT_STATE {");
		m_output.AppendLine("struct CAESAR_STRUCT_STATE *_predecessor;");
		m_output.AppendLine("struct STATE_LIST          *_successors;");
		m_output.AppendLine("char *_statenum;");
		m_output.AppendLine("char _hidden;");
		for (final Identifier sym: ooActionSystemType.symbols().symbolList())
		{
			if (sym.kind() == IdentifierKind.AttributeIdentifier)
			{
				DumpAttribute((AttributeIdentifier)sym);
				m_output.AppendLine(";");
			}
		}
		m_output.AppendLine("} UNIXPACK;");

		m_output = tmp;

		// now define the hash sizes, malloc and free routines, and aligned state
		m_output.AppendLine();
		m_output.AppendLine("#undef CAESAR_SIZE_STATE");
		m_output.AppendLine("#undef CAESAR_HASH_SIZE_STATE");
		m_output.AppendLine("#undef CAESAR_CREATE_STATE");
		m_output.AppendLine("#undef CAESAR_DELETE_STATE");
		m_output.AppendLine("");

		m_output.AppendLine();
		m_output.AppendLine("#define CAESAR_SIZE_STATE() (sizeof (CAESAR_BODY_STATE))");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_SIZE_STATE = CAESAR_SIZE_STATE();");

		m_output.AppendLine();
		m_output.AppendLine("#define CAESAR_HASH_SIZE_STATE() (CAESAR_SIZE_STATE ())");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_HASH_SIZE_STATE = CAESAR_HASH_SIZE_STATE();");

		m_output.AppendLine("#define CAESAR_CREATE_STATE(CAESAR_S)\\");
		m_output.AppendLine("   { CAESAR_CREATE (*(CAESAR_S), CAESAR_SIZE_STATE(), CAESAR_TYPE_STATE); ((struct CAESAR_STRUCT_STATE*)(*(CAESAR_S)))->_hidden = 0; }");

		m_output.AppendLine("");
		m_output.AppendLine("#define CAESAR_DELETE_STATE(CAESAR_S)\\");
		m_output.AppendLine("   { DELETE_STATES(((struct CAESAR_STRUCT_STATE*)*(CAESAR_S))->_successors); CAESAR_DELETE(*(CAESAR_S)); *(CAESAR_S) = NULL; }");

		m_output.AppendLine();
		m_output.AppendLine("typedef struct CAESAR_STRUCT_ALIGNMENT_STATE {");
		m_output.AppendLine("  char CAESAR_BYTE;");
		m_output.AppendLine("  CAESAR_BODY_STATE CAESAR_S;");
		m_output.AppendLine("} CAESAR_BODY_ALIGNMENT_STATE;");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_ALIGNMENT_STATE = sizeof (CAESAR_BODY_ALIGNMENT_STATE) - sizeof (CAESAR_BODY_STATE);");

		line();

		DefineCadpStateHelpers(ooActionSystemType);

		line();
	}

	private void DefineCadpStateHelpers(OoActionSystemType ooActionSystemType)
	{
		m_output.AppendLine("#include \"argos_runtime_helpers.c\"");
		m_output.AppendLine("");


//		final IScope ascope = ooActionSystemType.GetParentScope();
//		final MainModule mainscope = (MainModule)ascope;

	}



	/// <summary>
	/// Exports a function that compares two states.
	/// </summary>
	private void DefineCompareCadpStates()
	{
		m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_COMPARE_STATE (CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_STATE CAESAR_S2)");
		lp();
		m_output.AppendLine("  CAESAR_TYPE_BOOLEAN CAESAR_RESULT;");
		m_output.AppendLine("  if ((char*)CAESAR_S1 == (char*)CAESAR_S2) return 1;");
		m_output.AppendLine("  if (CAESAR_S1->_hidden != CAESAR_S2->_hidden)");
		m_output.AppendLine("    return 0;");
		m_output.AppendLine("  else  if (CAESAR_S1->_hidden == 0)");
		m_output.AppendLine(String.format("    CAESAR_RESULT = (memcmp (((char *) CAESAR_S1) + 3* %1$s, ((char *) CAESAR_S2)+3* %1$s , CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"/*, CadpType.sizeOfTypes["pointer"]*/));
		m_output.AppendLine("  else");
		m_output.AppendLine("  {");
		m_output.AppendLine(String.format("/*    CAESAR_RESULT = (memcmp (((char *) CAESAR_S1)+3* %1$s, ((char *) CAESAR_S2)+3* %1$s, CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"/*CadpType.sizeOfTypes["pointer"]*/));
		m_output.AppendLine("    if (CAESAR_RESULT) {");
		m_output.AppendLine("    char succequal;");
		m_output.AppendLine("    COMPARE_STATES(CAESAR_S1->_successors,CAESAR_S2->_successors,succequal);");
		m_output.AppendLine("    CAESAR_RESULT = CAESAR_RESULT && succequal;}*/");
		m_output.AppendLine("    CAESAR_RESULT = 0;");
		/*m_output.AppendLine("");
            m_output.AppendLine(String.format("    CAESAR_RESULT = CAESAR_S1->_statenum == CAESAR_S2->_statenum && (memcmp (((char *) CAESAR_S1)+3* %1$s, ((char *) CAESAR_S2)+3* %1$s, CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"));*/
		m_output.AppendLine("  }");
		m_output.AppendLine("  return (CAESAR_RESULT);");
		rp();
	}

	/// <summary>
	/// Exports a hash function. Standard CADP implementation.
	/// </summary>
	private void DefineCadpStateHash()
	{
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HASH_STATE (CAESAR_TYPE_STATE CAESAR_ST, CAESAR_TYPE_NATURAL CAESAR_MODULUS)");
		lp();
		m_output.AppendLine("  /* we do not care about the pre/succ/... pointers here */");
		m_output.AppendLine("int beg_offset = 3 * sizeof(unsigned char*);");
		m_output.AppendLine("  CAESAR_TYPE_STATE CAESAR_S = (CAESAR_TYPE_STATE) ((unsigned char*)CAESAR_ST + beg_offset);");
		m_output.AppendLine("  CAESAR_TYPE_NATURAL CAESAR_RESULT;");
		m_output.AppendLine("  CAESAR_TYPE_WORD CAESAR_SHIFT_LOW, CAESAR_SHIFT_HIGH;");
		m_output.AppendLine("  CAESAR_TYPE_WORD *CAESAR_LOW, *CAESAR_HIGH;");
		m_output.AppendLine("  CAESAR_SHIFT_LOW = ((CAESAR_TYPE_WORD) CAESAR_S) % CAESAR_WORD_SIZE;");
		m_output.AppendLine("  CAESAR_LOW = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_S - CAESAR_SHIFT_LOW);");
		m_output.AppendLine("  CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_S + CAESAR_HASH_SIZE_STATE () - beg_offset);");
		m_output.AppendLine("  CAESAR_SHIFT_HIGH = ((CAESAR_TYPE_WORD) CAESAR_HIGH) % CAESAR_WORD_SIZE;");
		m_output.AppendLine("  CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_HIGH - CAESAR_SHIFT_HIGH);");
		m_output.AppendLine("  if (CAESAR_LOW == CAESAR_HIGH) {");
		m_output.AppendLine("		CAESAR_RESULT = htonl (*CAESAR_LOW);");
		m_output.AppendLine("		if (CAESAR_SHIFT_LOW)");
		m_output.AppendLine("			CAESAR_RESULT &= CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW);");
		m_output.AppendLine("		if (CAESAR_SHIFT_HIGH)");
		m_output.AppendLine("			CAESAR_RESULT &= CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH));");
		m_output.AppendLine("	}");
		m_output.AppendLine("	else");
		m_output.AppendLine("	{");
		m_output.AppendLine("		CAESAR_RESULT = 0;");
		m_output.AppendLine("		if (CAESAR_SHIFT_LOW) {");
		m_output.AppendLine("			CAESAR_RESULT = htonl (*(CAESAR_LOW++)) & (CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW));");
		m_output.AppendLine("		}");
		m_output.AppendLine("		while (CAESAR_LOW < CAESAR_HIGH) {");
		m_output.AppendLine("			CAESAR_RESULT ^= htonl (*(CAESAR_LOW++));");
		m_output.AppendLine("		}");
		m_output.AppendLine("		if (CAESAR_SHIFT_HIGH) {");
		m_output.AppendLine("			CAESAR_RESULT ^= htonl (*CAESAR_LOW) & (CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH)));");
		m_output.AppendLine("		}");
		m_output.AppendLine("	}");
		m_output.AppendLine("	if (CAESAR_SHIFT_LOW) ");
		m_output.AppendLine("		CAESAR_RESULT = ((CAESAR_RESULT >> ((CAESAR_WORD_SIZE - CAESAR_SHIFT_LOW) * 8)) | (CAESAR_RESULT << (CAESAR_SHIFT_LOW * 8)));");
		m_output.AppendLine("  CAESAR_RESULT = CAESAR_RESULT % CAESAR_MODULUS;");
		m_output.AppendLine("  return (CAESAR_RESULT);");
		rp();
	}

	/// <summary>
	/// Exports a function to print the state
	/// </summary>
	private void DefineCadpPrintState()
	{
		m_output.AppendLine("void CAESAR_PRINT_STATE (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_STATE CAESAR_S)");
		m_output.AppendLine("{");
		m_output.AppendLine("  switch (CAESAR_CURRENT_STATE_FORMAT) {");
		m_output.AppendLine("  case 0:");
		m_output.AppendLine("    fprintf (CAESAR_FILE, \"{\\n_hidden: %s,\\n\", CAESAR_S->_hidden == 0 ? \"0\": \"1\");");
		int i = 0;
		for (final AttributeIdentifier x: m_statevector)
		{
			CadpType.EmitType(x.type());
			if (i != 0)
				m_output.AppendLine("    fprintf (CAESAR_FILE, \",\\n\");");

			i++;
			m_output.AppendLine(String.format("    fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
			m_output.AppendLine(String.format("    %1$s%2$s(CAESAR_FILE, CAESAR_S->%3$s);", CadpType.printString,
					CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText()));
		}
		m_output.Append("    fprintf (CAESAR_FILE, \"\\n}\");");
		m_output.AppendLine("    break;");
		m_output.AppendLine("  default:");
		m_output.AppendLine("  {");
		m_output.AppendLine("    printf(\"#233 bug during simulation:\\n     unknown state printing format\\n\");");
		m_output.AppendLine("  }");
		m_output.AppendLine("  break;");
		m_output.AppendLine("  }");
		m_output.AppendLine("}");
	}

	/// <summary>
	/// Exports a function to print the delta state..
	/// </summary>
	private void DefineCadpPrintDeltaState()
	{
		m_output.AppendLine("void CAESAR_DELTA_STATE (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_STATE CAESAR_S2)");
		m_output.AppendLine("{");
		m_output.AppendLine("  switch (CAESAR_CURRENT_STATE_FORMAT) {");
		m_output.AppendLine("  case 0:");

		m_output.AppendLine("    fprintf (CAESAR_FILE, \"{_hidden: %s, \", CAESAR_S1->_hidden == 0 ? \"0\": \"1\");");
		int i = 0;
		for (final AttributeIdentifier x: m_statevector)
		{
			if (i != 0)
				m_output.AppendLine("    fprintf (CAESAR_FILE, \", \");");

			i++;
			m_output.AppendLine(String.format("    fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
			m_output.AppendLine(String.format("    %1$s%2$s(CAESAR_FILE, CAESAR_S1->%3$s);", CadpType.printString,
					CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText()));
		}
		m_output.Append("    fprintf (CAESAR_FILE, \"}\");");



		m_output.Append("    fprintf (CAESAR_FILE, \" --->> \");");



		m_output.AppendLine("    fprintf (CAESAR_FILE, \"{_hidden: %s, \", CAESAR_S2->_hidden == 0 ? \"0\": \"1\");");
		i = 0;
		for (final AttributeIdentifier x: m_statevector)
		{
			if (i != 0)
				m_output.AppendLine("    fprintf (CAESAR_FILE, \", \");");

			i++;
			m_output.AppendLine(String.format("    fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
			m_output.AppendLine(String.format("    %1$s%2$s(CAESAR_FILE, CAESAR_S2->%3$s);", CadpType.printString,
					CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText()));
		}
		m_output.Append("    fprintf (CAESAR_FILE, \"}\");");


		m_output.AppendLine("  break;");
		m_output.AppendLine("  default:");
		m_output.AppendLine("  {");
		m_output.AppendLine("    printf(\"#233 bug during simulation:\\n     unknown state printing format\\n\");");
		m_output.AppendLine("  }");
		m_output.AppendLine("  break;");
		m_output.AppendLine("  }");
		m_output.AppendLine("}");
	}

	/// <summary>
	/// Defines CADP label data type and helper information
	/// </summary>
	private void DefineCadpLabel(OoActionSystemType ooActionSystemType)
	{
		m_output.AppendLine("typedef unsigned int CAESAR_TYPE_PACKED_TRANSITION_NUMBER;");
		m_output.AppendLine("typedef unsigned char CAESAR_TYPE_UNIQUE_GATE_AND_PROFILE_NUMBER;");

		m_output.AppendLine("typedef struct CAESAR_STRUCT_LABEL {");
		m_output.AppendLine("  CAESAR_TYPE_PACKED_TRANSITION_NUMBER CAESAR_TRANSITION_NUMBER;");

		int i = 0;
		final StringBuilder param = new StringBuilder();
		for (final Identifier sym: ooActionSystemType.symbols().symbolList())
		{
			if (sym.kind() == IdentifierKind.NamedActionIdentifier)
			{
				final NamedActionIdentifier namedAction = (NamedActionIdentifier)sym;

				if (((FunctionType)namedAction.type()).parameter().size() > 0)
				{
					param.append("    struct {"); param.append(System.lineSeparator());
					int parnum = 0;
					for (final Type parameter: ((FunctionType)namedAction.type()).parameter())
					{
						param.append(String.format("        %1$s PARAM_%2$s;", DumpType(parameter), parnum));
						param.append(System.lineSeparator());
						parnum++;
					}
					param.append(String.format("    } CAESAR_PROFILE_%1$s;", i));
					param.append(System.lineSeparator());
				}
				actions.add(namedAction);
				i++;
			}
			else if (sym.kind() == IdentifierKind.MethodIdentifier)
			{
				methods.add((MethodIdentifier)sym);
			}
		}
		m_output.AppendLine("    union {");
		if (param.length() > 0)
			m_output.Append(param.toString());
		m_output.AppendLine(" } CAESAR_UNION;");
		m_output.AppendLine("} CAESAR_BODY_LABEL;");
		m_output.AppendLine();
		m_internalActionNumber = actions.size();

		m_output.AppendLine(String.format("#define INTERNAL_ACTION_NUMBER %1$s", m_internalActionNumber));
		m_output.AppendLine("#define INTERNAL_ACTION 0");
		m_output.AppendLine("#define OBSERVABLE_ACTION 1");
		m_output.AppendLine("#define CONTROLLABLE_ACTION 2");

		final StringBuilder gatelist = new StringBuilder(String.format("CAESAR_TYPE_STRING CAESAR_GATE[%1$s] = {", (actions.size() + 1)));
		final StringBuilder cardlist = new StringBuilder(String.format("CAESAR_TYPE_NATURAL CAESAR_CARDINAL[%1$s] = {", (actions.size() + 1)));
		final StringBuilder intObsCtrList = new StringBuilder(String.format("CAESAR_TYPE_NATURAL CAESAR_GATEKIND[%1$s] = {", (actions.size() + 1)));
		int j = 0;
		for (final NamedActionIdentifier action: actions)
		{
			if (j != 0)
			{
				gatelist.append(", ");
				cardlist.append(", ");
				intObsCtrList.append(", ");
			}
			j++;
			gatelist.append(String.format("\"%1$s\"", action.tokenText()));
			cardlist.append(((FunctionType)action.type()).parameter().size());
			if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Observable)
				intObsCtrList.append("OBSERVABLE_ACTION");
			else if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Controllable)
				intObsCtrList.append("CONTROLLABLE_ACTION");
			else
				intObsCtrList.append("INTERNAL_ACTION");
		}
		gatelist.append(",\"i\"};");
		cardlist.append(",0};");
		intObsCtrList.append(",INTERNAL_ACTION};");

		m_output.AppendLine("/* Names of actions (= gates) */");
		m_output.AppendLine(gatelist.toString());
		m_output.AppendLine("/* Number of parameters of actions (= cardinality) */");
		m_output.AppendLine(cardlist.toString());
		m_output.AppendLine("/* Internal (0), Observable (1), or Controllable (2) action? */");
		m_output.AppendLine(intObsCtrList.toString());

		m_output.AppendLine("#undef CAESAR_SIZE_LABEL");
		m_output.AppendLine("#define CAESAR_SIZE_LABEL() (sizeof (CAESAR_BODY_LABEL))");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_SIZE_LABEL = CAESAR_SIZE_LABEL();");
		m_output.AppendLine("#undef CAESAR_HASH_SIZE_LABEL");
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_HASH_SIZE_LABEL;");
		m_output.AppendLine("#define CAESAR_HASH_SIZE_LABEL() CAESAR_HINT_HASH_SIZE_LABEL");
	}

	/// <summary>
	/// Method that exports the CAESAR_STRING_LABEL function
	/// </summary>
	private void DefineCadpGetStringLabel()
	{

		m_output.AppendLine("CAESAR_TYPE_FILE CAESAR_BUFFER = NULL;");
		m_output.AppendLine("");
		m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_STRING_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
		lp();

		m_output.AppendLine("  CAESAR_TYPE_STRING CAESAR_RESULT;");
		m_output.AppendLine("");
		m_output.AppendLine("	#define CAESAR_LABEL_HASH_SIZE 10007");
		m_output.AppendLine("	typedef struct CAESAR_STRUCT_LABEL_STRING {");
		m_output.AppendLine("		CAESAR_BODY_LABEL CAESAR_LABEL;");
		m_output.AppendLine("		CAESAR_TYPE_STRING CAESAR_STRING;");
		m_output.AppendLine("	} CAESAR_BODY_LABEL_STRING, *CAESAR_TYPE_LABEL_STRING;");
		m_output.AppendLine("	static CAESAR_TYPE_LABEL_STRING CAESAR_LABEL_STRING_TABLE = NULL;");
		m_output.AppendLine("	/*static CAESAR_TYPE_FILE CAESAR_BUFFER = NULL;*/");
		m_output.AppendLine("	CAESAR_TYPE_NATURAL CAESAR_N;");
		m_output.AppendLine("	CAESAR_TYPE_LABEL_STRING CAESAR_ITEM;");
		m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
		m_output.AppendLine("	static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_HIT = 0;");
		m_output.AppendLine("	static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_MISS = 0;");
		m_output.AppendLine("	static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_CONFLICT = 0;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("");

		m_output.AppendLine("    /* If action has no params, then label is name of action */");
		m_output.AppendLine("    //if (CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER] == 0)");
		m_output.AppendLine("    //   CAESAR_RESULT = CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
		m_output.AppendLine("    //else");
		m_output.AppendLine("    {");
		m_output.AppendLine("        /* otherwise.. (standard CADP) */");

		m_output.AppendLine("		if (CAESAR_LABEL_STRING_TABLE == NULL) {");
		m_output.AppendLine("			CAESAR_CREATE (CAESAR_LABEL_STRING_TABLE, CAESAR_LABEL_HASH_SIZE * sizeof (CAESAR_BODY_LABEL_STRING), CAESAR_TYPE_LABEL_STRING);");
		m_output.AppendLine("			if (CAESAR_LABEL_STRING_TABLE == NULL)");
		m_output.AppendLine("			{");
		m_output.AppendLine("				printf(\"#211 bug during simulation:\\n     out of memory when allocating string table\\n\");");
		m_output.AppendLine("				printf(\"     abandon\\n\");");
		m_output.AppendLine("				CAESAR_TERMINATE (1);");
		m_output.AppendLine("				exit(1);");
		m_output.AppendLine("			}");
		m_output.AppendLine("			for (CAESAR_N = 0; CAESAR_N < CAESAR_LABEL_HASH_SIZE; CAESAR_N++)");
		m_output.AppendLine("				CAESAR_LABEL_STRING_TABLE [CAESAR_N].CAESAR_STRING = NULL;");
		m_output.AppendLine("		}");
		m_output.AppendLine("		CAESAR_ITEM = CAESAR_LABEL_STRING_TABLE + CAESAR_HASH_LABEL (CAESAR_L, CAESAR_LABEL_HASH_SIZE);");
		m_output.AppendLine("		if ((CAESAR_ITEM->CAESAR_STRING != NULL) && CAESAR_COMPARE_LABEL (&(CAESAR_ITEM->CAESAR_LABEL), CAESAR_L)) {");
		m_output.AppendLine("			CAESAR_RESULT = CAESAR_ITEM->CAESAR_STRING;");
		m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
		m_output.AppendLine("			CAESAR_LABEL_STRING_TABLE_HIT++;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("		} else {");
		m_output.AppendLine("			if (CAESAR_ITEM->CAESAR_STRING == NULL) {");
		m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
		m_output.AppendLine("				CAESAR_LABEL_STRING_TABLE_MISS++;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("			} else {");
		m_output.AppendLine("				CAESAR_DELETE (CAESAR_ITEM->CAESAR_STRING);");
		m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
		m_output.AppendLine("				CAESAR_LABEL_STRING_TABLE_CONFLICT++;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("			}");
		m_output.AppendLine("			CAESAR_ITEM->CAESAR_LABEL = *CAESAR_L;");
		m_output.AppendLine("			if (CAESAR_BUFFER == NULL) {");
		m_output.AppendLine("				CAESAR_BUFFER = (CAESAR_TYPE_FILE) tmpfile ();");
		m_output.AppendLine("				if (CAESAR_BUFFER == NULL)");
		m_output.AppendLine("				{");
		m_output.AppendLine("					printf(\"#212 bug during simulation :\\n     cannot allocate tmpfile\\n\");");
		m_output.AppendLine("					printf(\"     aborting.\\n\");");
		m_output.AppendLine("					CAESAR_TERMINATE (1);");
		m_output.AppendLine("					exit(1);");
		m_output.AppendLine("				}");
		m_output.AppendLine("			}");
		m_output.AppendLine("			CAESAR_PRINT_LABEL (CAESAR_BUFFER, CAESAR_L);");
		m_output.AppendLine("			CAESAR_N = ftell (CAESAR_BUFFER) + 1;");
		m_output.AppendLine("			rewind (CAESAR_BUFFER);");
		m_output.AppendLine("			CAESAR_CREATE (CAESAR_ITEM->CAESAR_STRING, CAESAR_N, CAESAR_TYPE_STRING);");
		m_output.AppendLine("			if (CAESAR_ITEM->CAESAR_STRING == NULL)");
		m_output.AppendLine("			{");
		m_output.AppendLine("				printf(\"#213 bug during simulation :\\n     out of memory\\n\");");
		m_output.AppendLine("				printf(\"     aborting\\n\");");
		m_output.AppendLine("				CAESAR_TERMINATE (1);");
		m_output.AppendLine("				exit(1);");
		m_output.AppendLine("			}");
		m_output.AppendLine("			if (fgets (CAESAR_ITEM->CAESAR_STRING, CAESAR_N, CAESAR_BUFFER) == NULL)");
		m_output.AppendLine("			{");
		m_output.AppendLine("				printf(\"#214 bug during simulation :\\n   fgets  \\n\");");
		m_output.AppendLine("				printf(\"     aborting.\\n\");");
		m_output.AppendLine("				CAESAR_TERMINATE (1);");
		m_output.AppendLine("				exit(1);");
		m_output.AppendLine("			}");
		m_output.AppendLine("			rewind (CAESAR_BUFFER);");
		m_output.AppendLine("			CAESAR_RESULT = CAESAR_ITEM->CAESAR_STRING;");
		m_output.AppendLine("		}");
		m_output.AppendLine("	}");
		m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
		m_output.AppendLine("	fprintf (stderr, \"label table statistics: hit=%u miss=%u conflict=%u total=%u\\n\", CAESAR_LABEL_STRING_TABLE_HIT, CAESAR_LABEL_STRING_TABLE_MISS, CAESAR_LABEL_STRING_TABLE_CONFLICT, CAESAR_LABEL_STRING_TABLE_HIT + CAESAR_LABEL_STRING_TABLE_MISS+CAESAR_LABEL_STRING_TABLE_CONFLICT);");
		m_output.AppendLine("#endif");
		m_output.AppendLine("  return CAESAR_RESULT;");
		rp();
	}

	/// <summary>
	/// Method that exports the CAESAR_COMPARE_LABEL function
	/// </summary>
	private void DefineCadpCompareLabel()
	{
		m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_COMPARE_LABEL (CAESAR_TYPE_LABEL CAESAR_L1, CAESAR_TYPE_LABEL CAESAR_L2)");
		lp();
		m_output.AppendLine("  CAESAR_TYPE_PACKED_TRANSITION_NUMBER CAESAR_N1, CAESAR_N2;");
		m_output.AppendLine("  CAESAR_N1 = CAESAR_L1->CAESAR_TRANSITION_NUMBER;");
		m_output.AppendLine("  CAESAR_N2 = CAESAR_L2->CAESAR_TRANSITION_NUMBER;");
		m_output.AppendLine("");
		m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
		m_output.AppendLine("if (CAESAR_GATEKIND[CAESAR_N1] == INTERNAL_ACTION && CAESAR_GATEKIND[CAESAR_N2] == INTERNAL_ACTION)");
		m_output.AppendLine("    return 1;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("");
		m_output.AppendLine("  /* if the labels encode different actions, then they are different.. */");
		m_output.AppendLine("  if (CAESAR_N1 != CAESAR_N2)");
		m_output.AppendLine("    return 0;");
		m_output.AppendLine("  /* if it is the same action, then compare the parameters */ ");
		m_output.AppendLine("  if (CAESAR_CARDINAL[CAESAR_N1] == 0)");
		m_output.AppendLine("    return 1;  /*no params, hence the same*/");
		m_output.AppendLine("  switch(CAESAR_N1)");
		m_output.AppendLine("  {");

		int num = 0;
		for (final NamedActionIdentifier action: actions)
		{
			if (((FunctionType)action.type()).parameter().size() > 0)
			{
				m_output.AppendLine(String.format("    case %1$s:", num));
				m_output.Append("      return ");
				int paramnr = 0;
				for (final Type param: ((FunctionType)action.type()).parameter())
				{
					if (paramnr != 0)
						m_output.AppendLine(" && ");
					if (CadpType.IsNumeric(param))

						m_output.Append(
								String.format("CAESAR_L1->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s == CAESAR_L2->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s", num, paramnr));
					else
						m_output.Append(
								String.format("0 == memcmp(&(CAESAR_L1->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s),&(CAESAR_L2->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s),sizeof(%3$s))", num, paramnr, CadpType.DumpType(param)));

					paramnr++;
				}
				m_output.AppendLine(";");
			}
			num++;
		}
		m_output.AppendLine("  }");
		m_output.AppendLine("  printf(\"#211 bug during simulation :\\n     CAESAR_COMPARE_LABEL\\n\");");
		m_output.AppendLine("  printf(\"     aborting\\n\");");
		m_output.AppendLine("  CAESAR_TERMINATE (1);");
		m_output.AppendLine("  exit(1);");
		rp();
	}

	/// <summary>
	/// Method that exports the CAESAR_HASH_LABEL function
	/// </summary>
	private void DefineCadpHashLabel()
	{
		m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HASH_LABEL (CAESAR_TYPE_LABEL CAESAR_L, CAESAR_TYPE_NATURAL CAESAR_MODULUS)");
		lp();
		m_output.AppendLine("  CAESAR_TYPE_NATURAL CAESAR_RESULT;");
		m_output.AppendLine("  CAESAR_TYPE_NATURAL CAESAR_SIZE;");
		m_output.AppendLine("");
		m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
		m_output.AppendLine("  if (CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION)");
		m_output.AppendLine("    return INTERNAL_ACTION_NUMBER % CAESAR_MODULUS;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("");
		m_output.AppendLine("  /* if action has no params, then hash is trans num */");
		m_output.AppendLine("  if (CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER] == 0)");
		m_output.AppendLine("     return CAESAR_L->CAESAR_TRANSITION_NUMBER % CAESAR_MODULUS;");
		m_output.AppendLine("  /* otherwise it gets more complicated.. */");
		m_output.AppendLine("  switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
		m_output.AppendLine("  {");

		int num = 0;
		for (final NamedActionIdentifier action : actions)
		{
			if (((FunctionType)action.type()).parameter().size() > 0)
			{
				m_output.AppendLine(String.format("    case %1$s:", num));
//				int paramnr = 0;
				for (@SuppressWarnings("unused") final Type param: ((FunctionType)action.type()).parameter())
				{
					m_output.AppendLine(
							String.format("      CAESAR_SIZE = sizeof (CAESAR_L->CAESAR_UNION.CAESAR_PROFILE_%1$s);", num));
					m_output.AppendLine("      break;");
//					paramnr++;
				}
			}
			num++;
		}
		m_output.AppendLine("    default:");
		m_output.AppendLine("      return CAESAR_L->CAESAR_TRANSITION_NUMBER % CAESAR_MODULUS;");
		m_output.AppendLine("  }");
		m_output.AppendLine("  {");
		m_output.AppendLine("    CAESAR_TYPE_WORD CAESAR_SHIFT_LOW, CAESAR_SHIFT_HIGH;");
		m_output.AppendLine("    CAESAR_TYPE_WORD *CAESAR_LOW, *CAESAR_HIGH;");
		m_output.AppendLine("    CAESAR_SHIFT_LOW = ((CAESAR_TYPE_WORD) (&(CAESAR_L->CAESAR_UNION))) % CAESAR_WORD_SIZE;");
		m_output.AppendLine("    CAESAR_LOW = (CAESAR_TYPE_WORD *) ((unsigned char *) (&(CAESAR_L->CAESAR_UNION)) - CAESAR_SHIFT_LOW);");
		m_output.AppendLine("    CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) (&(CAESAR_L->CAESAR_UNION)) + CAESAR_SIZE);");
		m_output.AppendLine("    CAESAR_SHIFT_HIGH = ((CAESAR_TYPE_WORD) CAESAR_HIGH) % CAESAR_WORD_SIZE;");
		m_output.AppendLine("    CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_HIGH - CAESAR_SHIFT_HIGH);");
		m_output.AppendLine("    if (CAESAR_LOW == CAESAR_HIGH) {");
		m_output.AppendLine("      CAESAR_RESULT = htonl (*CAESAR_LOW);");
		m_output.AppendLine("      if (CAESAR_SHIFT_LOW)");
		m_output.AppendLine("        CAESAR_RESULT &= CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW);");
		m_output.AppendLine("        if (CAESAR_SHIFT_HIGH)");
		m_output.AppendLine("          CAESAR_RESULT &= CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH));");
		m_output.AppendLine("    } else {");
		m_output.AppendLine("      CAESAR_RESULT = 0;");
		m_output.AppendLine("      if (CAESAR_SHIFT_LOW) {");
		m_output.AppendLine("        CAESAR_RESULT ^= htonl (*(CAESAR_LOW++)) & (CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW));");
		m_output.AppendLine("      }");
		m_output.AppendLine("      while (CAESAR_LOW < CAESAR_HIGH) {");
		m_output.AppendLine("        CAESAR_RESULT ^= htonl (*(CAESAR_LOW++));");
		m_output.AppendLine("      }");
		m_output.AppendLine("      if (CAESAR_SHIFT_HIGH) {");
		m_output.AppendLine("        CAESAR_RESULT ^= htonl (*CAESAR_LOW) & (CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH)));");
		m_output.AppendLine("      }");
		m_output.AppendLine("    }");
		m_output.AppendLine("    if (CAESAR_SHIFT_LOW) {");
		m_output.AppendLine("      CAESAR_RESULT = ((CAESAR_RESULT >> ((CAESAR_WORD_SIZE - CAESAR_SHIFT_LOW) * 8)) | (CAESAR_RESULT << (CAESAR_SHIFT_LOW * 8)));");
		m_output.AppendLine("    }");
		m_output.AppendLine("    CAESAR_RESULT = (CAESAR_RESULT ^ CAESAR_L->CAESAR_TRANSITION_NUMBER) % CAESAR_MODULUS;");
		m_output.AppendLine("  }");
		m_output.AppendLine("  return (CAESAR_RESULT);");
		rp();
	}

	/// <summary>
	/// Method that exports the CAESAR_PRINT_LABEL function
	/// </summary>
	private void DefineCadpPrintLabel()
	{
		m_output.AppendLine("void CAESAR_PRINT_LABEL (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_LABEL CAESAR_L)");
		lp();

		m_output.AppendLine("  char* actionTag = \"\";");
		m_output.AppendLine("  switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
		m_output.AppendLine("  {");
		int gatenum = 0;
		for (final NamedActionIdentifier action: actions)
		{
			m_output.AppendLine(String.format("    case %1$s:", gatenum));
			String controbsmark = "";
			if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Controllable)
				controbsmark = "ctr ";
			else if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Observable)
				controbsmark = "obs ";
			m_output.AppendLine(String.format("      actionTag = \"%1$s\";", controbsmark));
			m_output.AppendLine("break;");
			gatenum++;
		}
		m_output.AppendLine("  }");

		m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
		m_output.AppendLine("  fprintf(CAESAR_FILE, \"%s%s\", actionTag, CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION ? CAESAR_GATE[INTERNAL_ACTION_NUMBER] : CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER]);");
		m_output.AppendLine("#else");
		m_output.AppendLine("  fprintf(CAESAR_FILE, \"%s%s\", actionTag, CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER]);");
		m_output.AppendLine("#endif");

		m_output.AppendLine("  switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
		m_output.AppendLine("  {");

		gatenum = 0;
		for (final NamedActionIdentifier action : actions)
		{
			if (((FunctionType)action.type()).parameter().size() > 0)
			{
				m_output.AppendLine(String.format("    case %1$s:", gatenum));
				m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
				m_output.AppendLine("if (CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] != INTERNAL_ACTION)");
				m_output.AppendLine("#endif");
				m_output.AppendLine("{");
				m_output.AppendLine("      fprintf(CAESAR_FILE,\"  (\");");
				int paramnum = 0;
				for (final ParameterIdentifier paramname : action.parameter())
				{
					final Type param = paramname.type();
					CadpType.EmitType(param);
					m_output.AppendLine(String.format("      fprintf(CAESAR_FILE,\"%1$s: \");", paramname.tokenText()));
					m_output.AppendLine(String.format("      %1$s%4$s(CAESAR_FILE, CAESAR_L->CAESAR_UNION.CAESAR_PROFILE_%2$s.PARAM_%3$s);",
							CadpType.printString, gatenum, paramnum, CadpIdentifier.GetIdentifierString(param.identifier())));
					m_output.AppendLine("      fprintf(CAESAR_FILE,\" \");");
					paramnum++;
				}
				m_output.AppendLine("      fprintf(CAESAR_FILE,\")\");");
				m_output.AppendLine("}");
				m_output.AppendLine("      break;");
			}
			gatenum++;
		}
		m_output.AppendLine("  }");
		rp();
	}

	/// <summary>
	/// Method that exports the CAESAR_START_STATE function
	/// </summary>
	private void DefineCadpStartState()
	{
		m_output.AppendLine("void CAESAR_START_STATE (CAESAR_TYPE_STATE CAESAR_S)");
		lp();
		m_output.AppendLine("  memset ((char *) CAESAR_S, 0, CAESAR_SIZE_STATE());");
		m_output.AppendLine(" Model_Reset();");
		for (final AttributeIdentifier x: m_statevector)
		{
			m_output.Append("  CAESAR_S->");
			m_output.Append(x.tokenText());
			m_output.Append("=");
			final CadpType targettype = new CadpType();
			x.type().Accept(targettype);
			//m_output.Append(String.format("(%1$s) ",targettype.ToString()));
			final CadpExpression myvis = new CadpExpression(new CadpActionInfo(null, -1, 0, "", "", "CAESAR_S"));
			x.initializer().Accept(myvis);
			m_output.Append(myvis.toString());
			m_output.AppendLine(";");
		}
		rp();
	}


	public static String FunctionHeader(FunctionIdentifier fun)
	{
		return FunctionHeader(fun, fun.tokenText());
	}


	public static String FunctionHeader(FunctionIdentifier fun, String functionName)
	{
		final StringBuilder paramStr = new StringBuilder("CAESAR_TYPE_STATE CAESAR_S1");
		for (final ParameterIdentifier param : fun.parameter())
		{
			//CadpType.EmitType(param.type);
			paramStr.append(", ");
			paramStr.append(String.format("%1$s %2$s", DumpType(param.type()), CadpIdentifier.GetIdentifierString(param)));
		}
		if (((FunctionType)fun.type()).returnType() != null)
		{
			//CadpType.EmitType(((FunctionType)fun.type).returnType);
			paramStr.append(", ");
			paramStr.append(String.format("%1$s *param_result", DumpType(((FunctionType)fun.type()).returnType())));
		}
		return String.format("struct STATE_LIST* %1$s (%2$s)", functionName, paramStr.toString());
	}

	public static String FunctionHeader(FunctionType fun, String functionName)
	{
		final StringBuilder paramStr = new StringBuilder("CAESAR_TYPE_STATE CAESAR_S1");
		int i = 0;
		for (final Type param : fun.parameter())
		{
			//CadpType.EmitType(param);
			paramStr.append(", ");
			paramStr.append(String.format("%1$s param_%2$s", DumpType(param), i));
			i++;
		}
		if (fun.returnType() != null)
		{
			//CadpType.EmitType(((FunctionType)fun).returnType);
			paramStr.append(", ");
			paramStr.append(String.format("%1$s *param_result", DumpType(fun.returnType())));
		}
		return String.format("struct STATE_LIST* %1$s (%2$s)", functionName, paramStr.toString());
	}

	public static final String StateVariablePrefix = "((CAESAR_TYPE_STATE)elem->aState)";


	/// <summary>
	/// Exports a named action.
	/// </summary>
	private void DefineCadpAction(FunctionIdentifier action, int actionnumber)
	{
		// we only want to have about 100 statements in one function so that we do not overload the
		// stack frame with local variables. Hence we need to come up with a splitting of the
		// statement list... We do some easy thing here and only split on the top-level sequential block.
		final CadpActionInfo info = new CadpActionInfo(action, 10, actionnumber, "worklist", "newstatelist", "((CAESAR_TYPE_STATE)elem->aState)");
		final CadpStatement visitor = new CadpStatement(info);
		action.body().Accept(visitor);

		// print out any helper code
		final String helperMethods = info.m_helperMethods.toString();
		m_output.AppendLine(helperMethods);
		m_output.AppendLine();

		// print header of procedure
		m_output.AppendLine(FunctionHeader(action));

		lp();

		for (final Identifier sym: action.symbolTable().symbolList())
		{
			if (sym.kind() == IdentifierKind.LocalVariableIdentifier)
			{
				// FIXME: We need another structure for the state vars defined here, analogue to
				// the main system state thing. Just emitting a local variable here won't cut it.
				//throw new NotImplementedException("Local variables not supported by the CADP backend.");
				final CadpIdentifier ident = new CadpIdentifier(OoaCADPVisitor.StateVariablePrefix);
				sym.Accept(ident);
				m_output.AppendLine(String.format("  %1$s %2$s; /*local variable*/", DumpType(sym.type()), ident.toString()));
			}
		}

		m_output.AppendLine("  struct STATE_LIST *worklist = NULL;");
		m_output.AppendLine("  struct STATE_LIST *newstatelist = NULL;");
		m_output.AppendLine("  LIST_INSERT_STATE(worklist,CAESAR_S1);");
		m_output.AppendLine("  struct STATE_LIST *_initial_worklist = worklist;");

		m_output.AppendLine(visitor.toString());


		m_output.AppendLine("  /* delete all intermediate states. */");
		m_output.AppendLine("  ITERATE_STATES(newstatelist,  ((CAESAR_TYPE_STATE)elem->aState)->_predecessor = CAESAR_S1;);");

		if (actionnumber >= 0)
		{
			m_output.AppendLine(String.format("  if ( newstatelist != NULL) {"));
			m_output.AppendLine("  CAESAR_TYPE_LABEL label;");
			m_output.AppendLine("  CAESAR_CREATE (label, CAESAR_SIZE_LABEL(), CAESAR_TYPE_LABEL);");
			m_output.AppendLine(String.format("  label->CAESAR_TRANSITION_NUMBER = %1$s;", actionnumber));
			int paramnumber = 0;
			for (final ParameterIdentifier param : action.parameter())
			{
				m_output.AppendLine(String.format("label->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s = %3$s;", actionnumber, paramnumber, CadpIdentifier.GetIdentifierString(param)));
				paramnumber++;
			}
			m_output.AppendLine(" ITERATE_STATES(newstatelist,elem->aLabel = label;);");

			m_output.AppendLine("  } /* newstatelist != NULL */");
		}

		m_output.AppendLine("  free(_initial_worklist);");

		m_output.AppendLine("  return newstatelist;");
		rp();
	}

	/// <summary>
	/// Exports method that calculates all reachable states from an initial state by
	/// evaluating the do-od block once.
	/// </summary>
	private void DefineCadpCalculateOneIteration(Block doOdBlock)
	{
		m_output.AppendLine("void OneIteration(struct STATE_LIST *worklist, struct STATE_LIST *newstatelist)");
		m_output.AppendLine("{");
		final CadpStatement visitor = new CadpStatement(new CadpActionInfo(null, -1, 0, "worklist", "newstatelist", "((CAESAR_TYPE_STATE)elem->aState)"), true);
		doOdBlock.Accept(visitor);
		m_output.AppendLine(visitor.toString());
		m_output.AppendLine("");
		m_output.AppendLine("  worklist = newstatelist;");
		m_output.AppendLine("  newstatelist = NULL;");
		m_output.AppendLine("  /* end states are not hidden */ ");
		m_output.AppendLine("  ITERATE_STATES(worklist,  ((CAESAR_TYPE_STATE)elem->aState)->_hidden = 0;);");
		m_output.AppendLine("  /* setup tree and remove dead-ends */ ");
		m_output.AppendLine("  mark_tree(worklist);    /*mark&sweep dead ends*/");
		m_output.AppendLine("  sweep_states(ARGOS_ALL_STATES);");
		m_output.AppendLine("  unmark_tree(worklist);");
		m_output.AppendLine("  connect_tree(ARGOS_ALL_STATES); /*setup successor relation*/");
		m_output.AppendLine("  free_allStateList(&ARGOS_ALL_STATES); /*free allstatelist and worklist*/");
		m_output.AppendLine("}");
	}

	/// <summary>
	/// Method that exports the CAESAR_ITERATE_STATE function
	/// </summary>
	private void DefineCadpIterateState(OoActionSystemType system)
	{
		if (system.doOdBlock() != null)
			DefineCadpCalculateOneIteration(system.doOdBlock());

		line();

		m_output.AppendLine("void CAESAR_ITERATE_STATE (CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_LABEL CAESAR_L, CAESAR_TYPE_STATE CAESAR_S2, void (*CAESAR_LOOP) (CAESAR_TYPE_STATE, CAESAR_TYPE_LABEL, CAESAR_TYPE_STATE))");
		lp();

		m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
		m_output.AppendLine("  if (CAESAR_S1->_successors == NULL && CAESAR_S1->_hidden == 1)");
		m_output.AppendLine("  {");
		m_output.AppendLine("      printf(\"Re-evaluation of internal state not possible: Re-compile with UNLIMITED_REEVAL defined.\\n\");");
		m_output.AppendLine("      /*if you want to have this feature, you must not free the successors below. leak!*/");
		m_output.AppendLine("      abort();");
		m_output.AppendLine("  }");
		m_output.AppendLine("#endif");

		m_output.AppendLine("  if (CAESAR_S1->_successors == NULL && CAESAR_S1->_hidden == 0)");
		m_output.AppendLine("  {");
		if (system.doOdBlock() != null)
		{
			m_output.AppendLine("  struct STATE_LIST *worklist = NULL;");
			m_output.AppendLine("  struct STATE_LIST *newstatelist = NULL;");
			m_output.AppendLine("  LIST_INSERT_STATE(worklist,CAESAR_S1);");
			m_output.AppendLine("  struct STATE_LIST *initial_worklist = worklist;");
			m_output.AppendLine("  OneIteration(worklist, newstatelist);");
			m_output.AppendLine("  free(initial_worklist);");
		}
		m_output.AppendLine("  } /* done calculating successors.. */");

		m_output.AppendLine("  if (CAESAR_S1->_successors != NULL)");
		m_output.AppendLine("  {");
		m_output.AppendLine("    struct STATE_LIST *elem = CAESAR_S1->_successors;");
		m_output.AppendLine("    struct STATE_LIST *nelem = NULL;");
		m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
		m_output.AppendLine("    CAESAR_S1->_successors = NULL;");
		m_output.AppendLine("#endif");
		m_output.AppendLine("    while (elem != NULL)");
		m_output.AppendLine("    {");
		m_output.AppendLine("      if (elem->aLabel == NULL) {");
		//INTERNAL_ACTION_NUMBER
		m_output.AppendLine("        CAESAR_TYPE_LABEL label;");
		m_output.AppendLine("        CAESAR_CREATE (label, CAESAR_SIZE_LABEL(), CAESAR_TYPE_LABEL);");
		m_output.AppendLine("        label->CAESAR_TRANSITION_NUMBER = INTERNAL_ACTION_NUMBER;");
		m_output.AppendLine("        elem->aLabel = label;");
		m_output.AppendLine("      }");
		m_output.AppendLine("      memcpy(CAESAR_S2,elem->aState,CAESAR_SIZE_STATE());");
		/*
                        m_output.AppendLine("      if (CAESAR_S2->_hidden == 1 && (int)CAESAR_S2->_statenum < 0)");
                        m_output.AppendLine("      {");
                        m_output.AppendLine("          printf(\"statenum not initialized: %d\\n\", (int)CAESAR_S2->_statenum);");
                        m_output.AppendLine("          abort();");
                        m_output.AppendLine("      }");
		 */
		m_output.AppendLine("      CAESAR_S2->_predecessor = NULL;");

		m_output.AppendLine("      memcpy(CAESAR_L,elem->aLabel,CAESAR_SIZE_LABEL());");
		m_output.AppendLine("      CAESAR_LOOP(CAESAR_S1, CAESAR_L, CAESAR_S2);");
		m_output.AppendLine("      nelem = elem->next;");
		m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
		m_output.AppendLine("      free(elem->aLabel);");
		m_output.AppendLine("      free(elem->aState); /*leaky: we must not free the successor list because of hidden states*/");
		m_output.AppendLine("      free(elem);");
		m_output.AppendLine("#endif");
		m_output.AppendLine("      elem = nelem;");
		m_output.AppendLine("    }");
		m_output.AppendLine("  }");
		rp();
	}

}