/**CFile*******************************************************************
  PackageName [versis]
  Synopsis    [Package 'versis' provides basic tools for formal
               verification of concurrent systems]

  FileName    [versisThread.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [The file versisThread.c contains functions needed if using
               threads.]
  SeeAlso     [versis.h, versisInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "versisInt.h"

#ifdef USETHREADS

#include <pthread.h>
#include <sched.h>

/*-----------------------------------------------------------------------*/
/* Constant declarations                                                 */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of thread functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
VersisCompose_Thr(void *args)
{
  struct funparam {
    Est_String name;
    int type;
    Est_String process;
    Est_String actions;
    Est_Boolean onthefly;
    int *thread_done;
  };

  Est_String name;
  int type;
  Est_String process;
  Est_String actions;
  Est_Boolean onthefly;

  name = ((struct funparam *) args)->name;
  type = ((struct funparam *) args)->type;
  process = ((struct funparam *) args)->process;
  actions = ((struct funparam *) args)->actions;
  onthefly = ((struct funparam *) args)->onthefly;

  Versis_Compose(name,type,process,actions,onthefly);

  *((struct funparam *) args)->thread_done = 1;

  return;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
VersisEquivalence_Thr(void *args)
{
  struct funparam {
    int type;
    int par1;
    Est_String name1;
    int par2;
    Est_String name2;
    Est_Boolean *r;
    int *thread_done;
  };

  int type;
  int par1;
  Est_String name1;
  int par2;
  Est_String name2;
  Est_Boolean r;

  type = ((struct funparam *) args)->type;
  par1 = ((struct funparam *) args)->par1;
  name1 = ((struct funparam *) args)->name1;
  par2 = ((struct funparam *) args)->par2;
  name2 = ((struct funparam *) args)->name2;

  r = Versis_Equivalence(type,par1,name1,par2,name2);

  *((struct funparam *) args)->r = r;
  *((struct funparam *) args)->thread_done = 1;

  return;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
VersisMinimization_Thr(void *args)
{
  struct funparam {
    int type;
    int par;
    Est_String name;
    int *thread_done;
  };

  int type;
  int par;
  Est_String name;

  type = ((struct funparam *) args)->type;
  par = ((struct funparam *) args)->par;
  name = ((struct funparam *) args)->name;

  Versis_Minimization(type,par,name);

  *((struct funparam *) args)->thread_done = 1;

  return;
}

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Versis_Compose_Thr(Est_String name, int type, int numP, Est_String process,
                   int numA, Est_String actions, Est_Boolean onthefly)
{
  struct {
    Est_String name;
    int type;
    Est_String process;
    Est_String actions;
    Est_Boolean onthefly;
    int *thread_done;
  } funparam;

  pthread_t thread;
  pthread_attr_t attr;
  struct sched_param param;

  int thread_done;

  /*
  pthread_attr_init(&attr);
  pthread_attr_setstacksize(&attr,262144);
  pthread_attr_setinheritsched(&attr,PTHREAD_EXPLICIT_SCHED);
  pthread_attr_setschedpolicy(&attr,SCHED_OTHER);
  param.sched_priority = sched_get_priority_min(SCHED_OTHER);
  pthread_attr_setschedparam(&attr, &param);
  */

  funparam.name = name;
  funparam.type = type;
  funparam.process = process;
  funparam.actions = actions;
  funparam.onthefly = onthefly;
  funparam.thread_done = &thread_done;

  /* POSIX */
  thread_done = 0;
  if (pthread_create(&thread,NULL,(void *)&VersisCompose_Thr,&funparam)) {
    printf("Error: pthread_create\n");
  } else {
    sched_yield();
    while (!thread_done) {
#ifdef TCLOUT
      Tcl_DoOneEvent(TCL_DONT_WAIT);
#endif
    }
    if (pthread_join(thread,NULL)) {
      printf("Error: pthread_join\n");
    }
  }

  return;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
Versis_Equivalence_Thr(int type, int par1, Est_String name1,
                       int par2, Est_String name2)
{
  struct {
    int type;
    int par1;
    Est_String name1;
    int par2;
    Est_String name2;
    Est_Boolean *r;
    int *thread_done;
  } funparam;

  pthread_t thread;
  pthread_attr_t attr;
  struct sched_param param;

  Est_Boolean r;
  int thread_done;

  /*
  pthread_attr_init(&attr);
  pthread_attr_setstacksize(&attr,262144);
  pthread_attr_setinheritsched(&attr,PTHREAD_EXPLICIT_SCHED);
  pthread_attr_setschedpolicy(&attr,SCHED_OTHER);
  param.sched_priority = sched_get_priority_min(SCHED_OTHER);
  pthread_attr_setschedparam(&attr, &param);
  */

  funparam.type = type;
  funparam.par1 = par1;
  funparam.name1 = name1;
  funparam.par2 = par2;
  funparam.name2 = name2;
  funparam.r = &r;
  funparam.thread_done = &thread_done;

  /* POSIX */
  thread_done = 0;
  if (pthread_create(&thread,NULL,(void *)&Versis_Equivalence_Thr,&funparam)) {
    printf("Error: pthread_create\n");
  } else {
    sched_yield();
    while (!thread_done) {
#ifdef TCLOUT
      Tcl_DoOneEvent(TCL_DONT_WAIT);
#endif
    }
    if (pthread_join(thread,NULL)) {
      printf("Error: pthread_join\n");
    }
  }

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Versis_Minimization.]
  Description [type = 0,1,2 - Strong, Weak, Trace]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Versis_Minimization_Thr(int type, int par, Est_String name)
{
  struct {
    int type;
    int par;
    Est_String name;
    int *thread_done;
  } funparam;

  pthread_t thread;
  pthread_attr_t attr;
  struct sched_param param;

  int thread_done;

  /*
  pthread_attr_init(&attr);
  pthread_attr_setstacksize(&attr,262144);
  pthread_attr_setinheritsched(&attr,PTHREAD_EXPLICIT_SCHED);
  pthread_attr_setschedpolicy(&attr,SCHED_OTHER);
  param.sched_priority = sched_get_priority_min(SCHED_OTHER);
  pthread_attr_setschedparam(&attr, &param);
  */

  funparam.type = type;
  funparam.par = par;
  funparam.name = name;
  funparam.thread_done = &thread_done;

  /* POSIX */
  thread_done = 0;
  if (pthread_create(&thread,NULL,(void *)&VersisMinimization_Thr,&funparam)) {
    printf("Error: pthread_create\n");
  } else {
    sched_yield();
    while (!thread_done) {
#ifdef TCLOUT
      Tcl_DoOneEvent(TCL_DONT_WAIT);
#endif
    }
    if (pthread_join(thread,NULL)) {
     printf("Error: pthread_join\n");
    }
  }

  return;
}

#else /* USETHREADS */

void
Versis_Compose_Thr(Est_String name, int type, int numP, Est_String process,
                   int numA, Est_String actions, Est_Boolean onthefly)
{
  return;
}

Est_Boolean
Versis_Equivalence_Thr(int type, int par1, Est_String name1,
                       int par2, Est_String name2)
{
  return FALSE;
}

void
Versis_Minimization_Thr(int type, int par, Est_String name)
{
  return;
}

#endif /* USETHREADS */
