#include "pns.h"
#include "spnbox.h"
#include "codegen.h" 
#include"insert.h"

int verb;

int inline is_verbose() { return verb; }




void br_filter(char *p) {  // removes beginning and end braces
  int n;
  if(!p)
    return;
  n = strlen(p);
  if(!n)
    return;
  n--;
  if(p[0] == '{' && p[n] == '}') {
    p[0] = ' ';
    p[n] = ' ';
  }
}


int is_empty(char *p) { // returns 1 if p has only space and tab characters
  int i;
  if(!p) return 1;
  for(i = 0; p[i]; i++)
    if(p[i] != ' ' && p[i] != '\t')
      break;
  return ! p[i];
}

int th_filter(char** ap, char* pattern) { // remove pattern from strings
  char* p = *ap, *p2 = 0;
  int i, n;
  if(!p || !pattern) return 0;
  n = strlen(pattern);
  for(i = 0; p[i]; i++) {
    if(p[i] == ' ' || p[i] == '\t')
      continue;
    if(!strncmp(p+i, pattern, n)) {
      if(!is_empty(p+i+n)) // else p2 remains equal to zero
        asprintf(&p2, "%s", p+i+n); 
      free(*ap);
      *ap = p2;
      return 1;
    }
    break;
  }
  return 0;
}


void main_filter(char **inc, char **newinc, char **main, char *pattern) {
  // Copy/append to newinc everything in *inc up to 'pattern'. 
  // Copy/append to *main everything in *inc following 'pattern'.
  // If newinc is zero, keep in inc everything up to 'pattern'. 
  // If newinc is nonzero, dealloc *inc and set it to zero.

  int i, n;
  char *p, *p2;

  if(!inc) return;
  p = *inc;
  if(!p || !pattern) return;
  n = strlen(pattern);
  for(i = 0; p[i]; i++) {
    if(p[i] == ' ' || p[i] == '\t')
      continue;
    if(!strncmp(p+i, pattern, n)) // then 'pattern' has been found
      break;
  }

  if(main && p[i]) { // p[i] is nonzero if 'pattern' was found
    if(*main) { // append to text in *main
      asprintf(&p2, "%s\n\n%s", *main, p+i+n); 
      free(*main);
      *main = p2;
    }
    else // write text to *main
      asprintf(main, "%s", p+i+n);
  }

  p[i] = 0; // keep in inc everything up to 'pattern'
  if(newinc) {
    if(!*newinc)
      *newinc = *inc;
    else { // append to text in newinc
      asprintf(&p2, "%s\n\n%s", *newinc, *inc);
      free(*newinc);
      *newinc = p2;
      free(*inc);
    } 
    *inc = 0;
  }
}


void sp_filter(specs *sp) {  
  // Removes beginning and end braces. Processes embedded instructions.
  // Sets default values for fields not processed by the translator.
  int i, j;
  pns *pn;
  arcs *pa;
  if(!sp)
    return;
  if(!sp->process_array)
    return;

  // Default values

  for(i = 0; i < sp->process_num; i++) {
    if(!sp->process_array[i])
      continue;

    br_filter(sp->process_array[i]->build);
    br_filter(sp->process_array[i]->include.text);

    // Is this a thread?
    if(th_filter(&(sp->process_array[i]->build),"<thread>"))
      sp->process_array[i]->thread = 1;
    // Is this a supervisor component?
    if(th_filter(&(sp->process_array[i]->build),"<supervisor>"))
      sp->process_array[i]->supervisor = 1;
    // Process the <main> instructions if any
    if(sp->process_array[i]->supervisor)
      main_filter(&(sp->process_array[i]->include.text), &(sp->include.text), \
		  &(sp->main.text), "<main>");
    else 
      main_filter(&(sp->process_array[i]->include.text), 0, 		\
		  &(sp->process_array[i]->main.text), "<main>");
    pn = sp->process_array[i]->pn; 
    if(pn) {
      if(pn->segment) 
	for(j = 0; j < pn->pnum; j++)
	  br_filter(pn->segment[j].text);
      if(pn->select) 
	for(j = 0; j < pn->pnum; j++)
	  br_filter(pn->select[j].text);
      if(pn->arc_list) 
	for(j = 0; j < pn->tnum; j++)
	  for(pa = pn->arc_list[j]; pa; pa = pa->next)
	    br_filter(pa->condition.text);
    }
  }
}


int main(int na, char* argv[]) {

  int i, j, l1, l2, UCcnt, UOcnt, LVcnt, *Tuc, *Tuo, *Tlive, *UClst, *UOlst, *LVlst;
  int labelcount = 0, finish = 0, plcnum, spcnum;
  char* input, *build = 0, *scplaces = 0;
  FILE* f;
  specs *sp;
  syncc *snc;
  pns pn, pn1, *apnsv;
  process **plant_array, **spv_array;
  matrix L, C, H, *H2;
  int *B;
  struct myinsert ins;
  linenf_r lin_res, lin_res2;
  dp_p LVparams;
  dp_r LVresult;
  struct synclist *syncl, *syncl2;
  struct sync_element *syn_el, *syn_el2;
  struct label_lst* lls;
  TrData** TInf;

  // These are flags
  unsigned char no_main = 0, signals = 0, sleep = 0, single_ch = 0, templ = 0;

char help[] = "\
This is version 1.2 of the concurrency tool suite (ct). The program generates \
\nautomatically concurrency control code based on a specification file.\
\n\
\nUsage: ct [options] [specification file] [-b list]\
\n\
\n'list' stands for a list of files and compiler options that should be\
\ncopied to the command line used to build the executable file.\
\n\
\nOptions:\
\n -d<number>  Comment on execution progress. More information displayed for\
\n             higher values of <number>, where <number> = 1 ... 20.\
\n -m          Do not generate a main function.\
\n -s<number>  Depending on the value of <number> the supervisor can be built\
\n             as follows:\
\n             0: The supervisor waits actively for events. \
\n             1: The supervisor is built as in option 0 except it enters a \
\n                sleep state (for a finite amount of time) when no events\
\n                are detected. \
\n             2: The supervisor blocks when no events occur. This option is \
\n                best when the number of concurrent processes or threads is \
\n                small. The supervisor has the least computational overhead \
\n                under this option. \
\n -t          Under this option customized template files can be used for \
\n             code generation. The program will look into the current \
\n             directory for the template files SupervisorTemplate.c and \
\n             ProcessTemplate.c and will use them for code generation in \
\n             the place of the default templates. The default templates can \
\n             be found in the newcodegen directory of the source files of \
\n             this program. The include file spcommon.h that is used by the \
\n             default templates can be found in the same place. \
\n\
\nExamples: ct manf.sp\
\n          ct -d3 input.sp\n";

// About single channel (option 2) all plant components write to the same pipe.
// Use this option if it is unlikely that the pipe would keep getting full 
// (i.e. if there are not many processes). Otherwise, fairness depends on 
// whether the OS is fair in deciding which requests to serve when the pipe 
// keeps getting full and there are competing requests to write to the pipe.


  // 1. INITIALIZATION

  ins = InitInsert(512); // used to store command line parameters 
  verb = 0;
  input = 0;

  if(na <= 1) {
    puts(help);
    finish = 1;
  }

  for(i = 1; i < na && !finish; i++) {
    if(!strcmp(argv[i], "--help")) {
      finish = 1;
      puts(help);
      break;
    }
    if(argv[i][0] == '-') {
      switch(argv[i][1]) {
      case 'd': verb = atoi(argv[i]+2);
  	        break;
      case 'm': no_main = 1;
	        break;
      case 's': j = atoi(argv[i]+2);
	        switch(j) {
                case 0: sleep = 0; break;
		case 1: sleep = 1; break;
		case 2: single_ch = 1; break;
		case 3: signals = 1; break;
		default: fprintf(stderr,"Unexpected parameter %s.\n", argv[i]);
		}
                break;
      case 'b': if(argv[i][2])
		  ins = FSInsert(ins, " %s", argv[i]+2);
	        for(i = i + 1; i < na; i++)
		  ins = FSInsert(ins, " %s", argv[i]);
	        break;
      case 't': templ = 1;
	        break;
      default:  fprintf(stderr, "Unknown option %s.\n", argv[i]);
      }
    }
    else {
      if(input)
	fprintf(stderr, "Unexpected parameter %s.\n", argv[i]);
      else
	input = argv[i];
    }
  }

  if(!input) {
    fprintf(stderr, "No input file specified.");
    finish = 1;
  }
  else {
    f = fopen(input,"r");
    if(!f) {
      fprintf(stderr, "The file %s cannot be opened.\n", input);
      finish = 1;
    }
    else { 
      if(verb && !finish) 
	fprintf(stderr, "Using the input file %s ...\n", input);
      fclose(f);
    }
  }

  build = GetInsertBuf(&ins);

  if(finish) { // Terminate if errors were encountered
    if(build) free(build);
    return 0;
  }

  // 2. TRANSLATE SPECIFICATION

  sp = ScanInput(input);

  // 2.1. Check translator result

  if(!sp)  
    return 1;

  if(sp->process_num <= 0) {
    fprintf(stderr, "No processes defined! Nothing to do.\n");
    dealloc_specs(sp);
    if(build) free(build);
    return 0; 
  }

  // Set settings not detected by translator

  sp->signals = signals;
  sp->sleep = sleep;
  sp->singlechannel = single_ch;
  sp->nomain = no_main;
  sp->templ = templ;

  // sp_filter is no longer needed. Included here for compatibility with some
  // features of the old specification format.
  sp_filter(sp); // detect settings and remove extra braces

  if(is_verbose() >= 3) { // For debugging
    for(i = 0; i < sp->process_num; i++) {
      printf("\n\n======================================================");
      if(sp->process_array[i]->supervisor)
	printf("\nSUPERVISOR COMPONENT: ");
      else if(sp->process_array[i]->thread)
	printf("\nTHREAD NAME: ");
      else
	printf("\nPROCESS NAME: ");
      printf("%s (%s)\n", sp->process_array[i]->instance, sp->process_array[i]->name);
      displaypn(*(sp->process_array[i]->pn), stdout);
    }
  }

  for(i = 0; i < sp->process_num; i++)
    if(!sp->process_array[i]->supervisor)
      break;

  if(i >= sp->process_num) {
    fprintf(stderr, "No plant components defined! Nothing to do.\n");
    dealloc_specs(sp);
    if(build) free(build);
    return 0; 
  }


  // 2.2 Label the PNs

  for(i = 0; i < sp->process_num; i++) 
    updatepn(sp->process_array[i]->pn, "freelabel", &labelcount);
  
  // 2.2.1 Deal with synchronization constraints

  for(i = 1; i; ) /* i = 0 indicates when loop may end */
    for(i = 0, snc = sp->synclist; snc; snc = snc->next) {
      l1 = snc->pn1->t[snc->t1].l; l2 = snc->pn2->t[snc->t2].l;
      if(l1 != l2) {
	i = 1;
	j = (l1 > l2)?l1:l2;
	snc->pn1->t[snc->t1].l = j; snc->pn2->t[snc->t2].l = j;
      }
    }

  // 2.3 Obtain SC specification. Currently:
  // extract the L, C, H, and b matrices (more complex specs to be done later)
  // the function calculates also the composed PN

  extractLHCB(sp, &pn, &L, &H, &C, &B, &scplaces);

  if(is_verbose() >= 3) { // For debugging
    printf("\n\n======================================================");
    printf("\nCONSTRAINTS OF *COMPOSED* PETRI NET:\n");
    printLHCB(&pn, &L, &H, &C, B, -1, stdout);
  }

  // 3. SUPERVISORY CONTROL

  // 3.1 Enforce SC specs (linear constraints supported currently)

  Tuc = tcalloc(pn.tnum, sizeof(*Tuc));
  Tuo = tcalloc(pn.tnum, sizeof(*Tuo));
  Tlive = tcalloc(pn.tnum, sizeof(*Tlive));
  if(pn.t)
    for(i = 0; i < pn.tnum; i++) {
      Tuc[i] = pn.t[i].uncontrollable;
      Tuo[i] = pn.t[i].unobservable;
      Tlive[i] = pn.t[i].live;
    }

  UCcnt = findIndices(Tuc, pn.tnum, sizeof(*Tuc), &UClst);
  UOcnt = findIndices(Tuo, pn.tnum, sizeof(*Tuo), &UOlst);
  LVcnt = findIndices(Tlive, pn.tnum, sizeof(*Tlive), &LVlst);

  lin_res = linenf(&pn.out, &pn.in, &L, B, pn.marking, &H, &C, \
		   UCcnt, UClst, UOcnt, UOlst);

  if(is_verbose() >= 3) { // For debugging
    printf("\n\n======================================================");
    printf("\nADMISSIBLE CONSTRAINTS: \n");
    i = NumberOfRows(lin_res.Lf);
    H2 = extract_H(&lin_res.Dfm, &lin_res.Dfp, i);
    printLHCB(&pn, &lin_res.Lf, H2, &lin_res.Cf, lin_res.bf, -1, stdout);
    if(H2) {
      DeallocateMatrix(H2);
      free(H2);
    }
  }

  // Check whether SC was successful

  if(strcmp(lin_res.how, "OK"))
    merror(0, "MAIN FUNCTION: SC has failed. Relax the specification\n\
    such as by reducing the number of uncontrollable and unobservable transitions");

  // 3.2. Enforce liveness

  // - Liveness enforcement is applied to the closed-loop
  // - Check whether the initial marking satisfies the constraints. 
  // - The result of liveness enforcement is enforced on the closed-loop
  //   with linenf and no uncontro. and unobs. transitions, since the result
  //   is guaranteed to be admissible. 
  // - The supervisor is extracted from the closed-loop reported by linenf via
  //   getSupervisor

  // For future work: 
  // - calculate initial marking constraints: check marking constraints satisfied by initial marking of plant.
  // - check if responsiveness is guaranteed.
  // - To help convergence, invariants from previous constraints should be 
  //   communicated by means of the L, B parameters of the function dp. 


  if(LVcnt) { // If T-liveness enforcement has been requested
    if(is_verbose() >= 3) { // For debugging
      printf("\n\n======================================================");
      printf("\n\nLiveness enforcement has been requested. This may take a while ...\n");
    }
    // Initialize parameters
    memset(&LVparams, 0, sizeof(LVparams));
    LVparams.Dm = lin_res.Dfm; LVparams.Dp = lin_res.Dfp;
    LVparams.Tuc = UClst; LVparams.TucCount = UCcnt;
    LVparams.Tuo = UOlst; LVparams.TuoCount = UOcnt;
    LVparams.IncludeT = LVlst; LVparams.IncludeCount = LVcnt;
    LVparams.option = 12 + (is_verbose() >= 4);

    LVresult = dp(&LVparams); // apply the T-liveness enforcement procedure
    if(strcmp(LVresult.how, "OK"))
      merror(0, "MAIN FUNCTION: Liveness enforcement has failed. Relax the specification\nsuch as by reducing the number of uncontrollable and unobservable transitions.\nSee also the log file of the liveness enforcement algorithm.");

    // Verify L*m0 >= B
    if(!TestLCB(&LVresult.Lf, lin_res.ms0, 0,0, GREATER_OR_EQUAL, LVresult.Bf))
      merror(0, "MAIN FUNCTION: Liveness enforcement has failed due to insufficient initial \nmarking (the initial marking does not satisfy the L*m >= B constraints). \nRelax the specification such as by increasing the initial marking and \nreducing the number of uncontrollable and unobservable transitions. See also \nthe log file of the liveness enforcement algorithm.");

    // Verify L0*m0 >= b0
    if(!TestLCB(&LVresult.L0f, lin_res.ms0,0,0,GREATER_OR_EQUAL, LVresult.B0f))
      merror(0, "MAIN FUNCTION: Liveness enforcement has failed due to insufficient initial \nmarking (the initial marking does not satisfy the L0*m >= B0 constraints). \nRelax the specification such as by increasing the initial marking and \nreducing the number of uncontrollable and unobservable transitions. See also \nthe log file of the liveness enforcement algorithm.");

    // Convert L*m >= B to L*m <= B (the input expected by linenf)
    InvertSignOfMatrix(&LVresult.Lf); // L = -L
    InvertSignOfVector(LVresult.Bf, NumberOfRows(LVresult.Lf)); // B = -B

    lin_res2 = linenf(&lin_res.Dfm, &lin_res.Dfp, &LVresult.Lf, LVresult.Bf,\
		      lin_res.ms0, 0, 0, 0, 0, 0, 0); 
    // no uncontr. and unobs. transitions have to be passed to linenf 
    // since constraints are admissible

    DeallocateDp(&LVresult); DeallocateLinenf(&lin_res);

    lin_res = lin_res2;
  }

  free(Tuc); free(Tuo); free(Tlive); free(UClst); free(UOlst); free(LVlst);

  // 3.3 Extract supervisor as a pn

  //apnsv = getSupervisor(&pn, &lin_res.Dfm, &lin_res.Dfp, lin_res.ms0);

  apnsv = getSupervisor2(&pn, &lin_res.Dfm, &lin_res.Dfp, lin_res.ms0, \
			 scplaces);

  if(is_verbose() >= 3) { // For debugging
    printf("\n\n======================================================");
    printf("\nCOMPOSED PLANT PN PLUS PREDEFINED SUPERVISOR COMPONENTS\n");
    displaypn(pn, stdout);
    printf("\n\n======================================================");
    if(apnsv) {
      //printf("\nSC GENERATED SUPERVISOR\n");
      printf("\nSUPERVISOR (INCLUDING PREDEFINED SUPERVISOR COMPONENTS)\n");
      displaypn(*apnsv, stdout);
    }
    else
      printf("\nNO GENERATED SUPERVISOR\n");
  }
  deallocpn(&pn);
  if(scplaces)
    free(scplaces);


  // 4. GENERATE CODE

  // 4.1 Separate supervisor components from plant components 

  spv_array = tcalloc(sp->process_num, sizeof(*spv_array));
  plant_array = tcalloc(sp->process_num, sizeof(*plant_array));
  for(i = 0, plcnum = 0, spcnum = 0; i < sp->process_num; i++) {
    if(sp->process_array[i]->supervisor) {
      spv_array[spcnum] = sp->process_array[i];
      spcnum++;
    }
    else {
      plant_array[plcnum] = sp->process_array[i];
      plcnum++;
    }
  }

  /* //Commented since unnecessary unless version 1 of getSupervisor is used

  // 4.2 Compose supervisor components with SC generated supervisor. 

  pn = pn_composition(spv_array, spcnum);
  pn1 = composepn(apnsv, &pn);
  if(apnsv)
    free(apnsv);
  deallocpn(&pn); // free intermediary result
  apnsv = &pn1;

  if(is_verbose() >= 3 && spcnum) { 
    // If spcnum != 0, then SC supervisor and final supervisor are different. 
    printf("\n\n======================================================");
    if(apnsv) {
      printf("\nFINAL SUPERVISOR\n");
      displaypn(*apnsv, stdout);
    }
  }

  */

  // 4.3 Obtain a synclist structure with the sync data for plant processes

  /* May be deleted after testing the change
  lls = get_label_list(sp->process_array, sp->process_num);
  syncl = get_synclist(lls, sp->process_array);
  TInf = get_TrData(apnsv, sp->process_array, sp->process_num, lls);
  */

  lls = get_label_list(plant_array, plcnum);
  syncl = get_synclist(lls, plant_array);
  TInf = get_TrData(apnsv, plant_array, plcnum, lls);

  // Call the code generation function

  /*CodeGenerator(apnsv, sp->name, sp->process_array, sp->process_num,	\
		  syncl, TInf, build); 
  */

  if(build) {
    if(sp->sbuildparam) 
      free(sp->sbuildparam);
    sp->sbuildparam = build;
  }

  CodeGenerator(apnsv, sp, plant_array, plcnum, syncl, TInf);


  // 5. TERMINATE

  if(apnsv) {
    deallocpn(apnsv);
    //free(apnsv);
  }
  free(plant_array);
  free(spv_array);
  dealloc_specs(sp);
  free_label_list(lls);
  free_synclist(syncl);
  free_TrData(TInf, plcnum);

  return 0;
}



/* Future improvements for deadlock prevention.

   Currently deadlock prevention does not account for determinism. Thus, 
   some potential deadlocks may remain undetected. 

   The following function could be defined in the future to help the deadlock 
   prevention procedure converge. Additionally, a function for initial 
   markings could be developed.

matrix getLB(matrix Lf, matrix Cf, int *Bf, int** B) {
  // Outputs a matrix L such that L*m <= B contains the rows of 
  // Lf*m + Cf*v <= Bf on which Cf is zero. B is also allocated and 
  // initialized. 

}

*/
