/**CFile*******************************************************************
  PackageName [mc]
  Synopsis    [Package 'mc' provides a symbolic ACTLW model checker]

  FileName    [mcMsc.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si),
               Tim Kovse (tim.kovse@uni-mb.si),
               Vladimir Smrekar (vladimir.smrekar@gmail.com)]
  Description [File mcMsc.c contains generation of MSC diagrams.
               It is included from mcDiagnostic.c.]
  SeeAlso     [mc.h, mcInt.h, mcDiagnostic.c]

  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.]
  ************************************************************************/

/* THIS FILE IS FOR TESTING, ONLY!!! */
/* File mcMsc.c is included in static function createPath */
/* near the end of file mcDiagnostic.c. */

/* SOME NOTES ON COMPOSITIONS IN CCS PARSER IN EST */

/* COMPOSITIONS ARE POSTPROCESSED WITH REGARD TO OPTIONAL PREFIXES         */
/*                                                                         */
/* COMPOSITION - composition is not postprocessed                          */
/* full COMPOSITION - return process instead of composition                */
/* trace COMPOSITION -  return min. determ. process which is trace equiv.  */
/* weak COMPOSITION - return minimal process which is weak equivalent      */
/* strong COMPOSITION - return minimal process which is strong equivalent  */
/* raw NET - composition is not postprocessed                              */
/* NET - return process instead of composition                             */
/*                                                                         */
/* THESE KEYWORDS ARE COMBINED WITH THE FOLLOWING SYMBOLS                  */
/*                                                                         */
/* // - CCS parallel composition                                           */
/* /// - multi-way composition                                             */
/* | - CCS parallel composition                                            */
/* || - LOTOS synchronisation                                              */
/* ||| - LOTOS interleaving                                                */
/*                                                                         */
/* To be able to generate MSC the resulting composition must not be        */
/* postprocessed - use 'COMPOSITION' or 'raw NET' which are equivalent.    */

/* SOME NOTES ON IMPLEMENTATION OF DIAGNOSTIC GENERATION IN EST */

/*
When diagnostic is required, model checker calls
McPrepareDiagnostic to prepare some structures.

Afterwards, function McPrintDiagnostic is called
which creates textual representation of diagnostic.

Function McPrintDiagnostic uses static function createPath,
to produce the path. Please note that McPrintDiagnostic
is recursive and one call of function McPrintDiagnostic results
in many calls of function createPath.

Function createPath gets the following parameters:
McDiagnosticType dgn - information about the system
McFunctionSequence *fseq - one part of diagnostic path
Est_String *path - not important for generation of Msc
Est_Boolean explain - not important for generation of Msc
Est_Boolean tracepath - not important for generation of Msc

Important fields in parameter dgn are:
dgn.D - transition relation of the system
dgn.init - initial state of the system

Function createPath has the following internal variables:
McFunctionSequence seq - local pointer to the part of diagnostic path
Pa_Sort *sort - set of actions (table) used in the system
Bdd_Edge f - BDD used during the calculations
Est_String act - not important for generation of Msc
*/

/* EXAMPLE */

/*
FILE crossing.ccs:

CAR = !car;CAR_WAIT
CAR_WAIT = ?isClose;CAR_WAIT + ?isOpen;!carCross;CAR

TRAIN = !train;!lower;TRAIN_WAIT
TRAIN_WAIT = ?isRed;TRAIN_WAIT + ?isGreen;!trainCross;!raise;?isOpen;TRAIN

CROSSING = !isRed;CROSSING + !isOpen;CROSSING + ?lower;!close;!green;CROSSING_CLOSE
CROSSING_CLOSE = !isGreen;CROSSING_CLOSE + !isClose;CROSSING_CLOSE + ?raise;!red;!open;CROSSING

raw net S = //(CAR,TRAIN,CROSSING)\isClose\isOpen\isRed\isGreen\lower\raise

property F1 == EEF ((EEX {carCross!} EEX {trainCross!} true) OR (EEX {trainCross!} EEX {carCross!} true));

COMMANDS:

ccs_read crossing.ccs
mc_check_actl 1 S F1 [expr $mc_diagnostic]

OUTPUT:

ACTL/ACTLW model checking on composition S

EEF ((EEX {carCross!} EEX {trainCross!} true) OR (EEX {trainCross!} EEX {carCross!} true)) ==> TRUE
MSC: CAR#1 --car!-> ENVIRONMENT
MSC: CROSSING#1 --isOpen!-> CAR#1
MSC: TRAIN#1 --train!-> ENVIRONMENT
MSC: TRAIN#1 --lower!-> CROSSING#1
MSC: CROSSING#1 --close!-> ENVIRONMENT
MSC: CROSSING#1 --green!-> ENVIRONMENT
MSC: CROSSING#1 --isGreen!-> TRAIN#1
MSC: CAR#1 --carCross!-> ENVIRONMENT
MSC: TRAIN#1 --trainCross!-> ENVIRONMENT
MSC: TRAIN#1 --trainCross!-> ENVIRONMENT
MSC: CAR#1 --carCross!-> ENVIRONMENT
Witness: (car!)(TAU)(train!)(TAU)(close!)(green!)(TAU)[(carCross!)(trainCross!),OR,(trainCross!)(carCross!)]
*/

/* ***************************************************************** */
/* === HERE IS THE START OF CODE ===                                 */
/* ***************************************************************** */

int line = 0;
int MSCLOOP = 0; /* THIS IS WRONG, MUST BE SOMEWHERE ELSE !!! */

  /* GENERATION OF MSC IS POSSIBLE ONLY WHEN THE SYSTEM IS A COMPOSITION */
  if (dgn.comp != -1) {

  /* YOU SHOULD NOT CHANGE fseq, THEREFORE WE USE A COPY OF IT */
  seq = fseq;

  /* GENERATION OF MSC IS DIVIDED INTO TWO PARTS */
  while (seq) {
    line++;

    if (Bdd_isEqv(Bdd_ITE(seq->f,McTau,bdd_termFalse),bdd_termFalse)) {

      /* PART 1: COMMUNICATION BETWEEN PROCESS AND ENVIRONMENT */

      int i;
      int A;

      /* START OF CALCULATION - DO NOT TOUCH */

      A = -1;
      f = Bdd_RelOpSimple(seq->f,"Ex xR",TRUE);

      if (MSCLOOP == 0){
         printf("0: proc -2 (:init:) creates proc -1 (ENVIRONMENT)\n");
      }


      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        if (!Bdd_isEqv(Bdd_ITE(
             pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
             f,bdd_termFalse),bdd_termFalse)) {
                A = i;
	           }

         if (MSCLOOP == 0){
            printf("0: proc -2 (:init:) creates proc ");
            printf("%i", i);
            printf(" (");
            printf(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
            printf(")");
            printf("\n");
         }
      }
      MSCLOOP = 1;

      /* END OF CALCULATION */

      /* START OF OUTPUT - MAKE YOUR CHANGES HERE */


      if (A!=-1) {
         /* SEND */
         printf("%d",line);
         printf(": proc ");
         printf("%d", A);
         printf(" (");
         printf(pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
         printf(") line ");
         printf("%d",line);
         printf(" 'pan_in' (state -)	[values: ");
         act = Pa_DecodeSortActions1(sort,f,FALSE);

         if (act[(strlen(act)-1)] == '!'){
            act[(strlen(act)-1)] = '\0';
         }
         printf(act);
         printf("!null]");
         printf("\n");

         /* RECEIVE */
         printf("%d",line);
         printf(": proc ");
         printf("-1");		/* ENVIRONMENT ID = -1 */
         printf(" (");
         printf("ENVIRONMENT");
         printf(") line ");
         printf("%d",line);
         printf(" 'pan_in' (state -)	[values: ");
         printf(act);
         free(act);
         printf("?null]");
         printf("\n");
      }

      /* END OF OUTPUT */

    } else {

      /* PART 2: COMMUNICATION BETWEEN TWO PROCESSES */

      int i;
      Est_String s;
      Bdd_Edge f1,f2,f3,fact;
      int A,B;

      /* START OF CALCULATION - DO NOT TOUCH */

      A = -1;
      B = -1;
      fact = bdd_termTrue;
      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        s = (Est_String) malloc(255);
        sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
        f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
        f2 = Bdd_RelOpComplex(seq->f,s,TRUE);
        free(s);
        if (!Bdd_isEqv(f1,f2)) {

          f = Bdd_RelOp(
                Bdd_ITE(f1,Bdd_RelOpSimple(f2,"R2S",TRUE),bdd_termFalse),
                pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
                "#AND Ex xR xS",TRUE);

          if (!Bdd_isEqv(Bdd_ITE(sort->a0,f,bdd_termFalse),bdd_termFalse)) {
            /* OUTPUT ACTION */
            A = i;
          }

          if (!Bdd_isEqv(Bdd_ITE(sort->a0,bdd_termFalse,f),bdd_termFalse)) {
            /* INPUT ACTION */
            B = i;
          }

          fact = Bdd_ITE(fact,Bdd_E(f,Bdd_GetVariable(sort->a0)),bdd_termFalse);

	}
      }

      if ((A==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,sort->a0,bdd_termFalse);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            A = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
	  }
	}
      }

      if ((B==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,bdd_termFalse,sort->a0);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            B = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
	  }
	}
      }

      /* END OF CALCULATION */

      /* START OF OUTPUT - MAKE YOUR CHANGES HERE */

      if ((A!=-1) && (B!=-1)) {
        /* INTERNAL STEPS ARE IGNORED */

         /* SEND */
         printf("%d",line);
         printf(": proc ");
         printf("%d", A);
         printf(" (");
         printf(pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
         printf(") line ");
         printf("%d",line);
         printf(" 'pan_in' (state -)	[values: ");
         act = Pa_DecodeSortActions1(sort,Bdd_ITE(fact,sort->a0,bdd_termFalse),FALSE);

         if (act[(strlen(act)-1)] == '!'){
            act[(strlen(act)-1)] = '\0';
         }
         printf(act);
         printf("!null]");
         printf("\n");

         /* RECEIVE */
         printf("%d",line);
         printf(": proc ");
         printf("%d", B);
         printf(" (");
         printf(pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);
         printf(") line ");
         printf("%d",line);
         printf(" 'pan_in' (state -)	[values: ");
         printf(act);
         free(act);
         printf("?null]");
         printf("\n");
      }
      /* END OF OUTPUT */

    }

    seq = seq->nextFunction;

  }}

/* ***************************************************************** */
/* === HERE IS THE END OF CODE ===                                   */
/* ***************************************************************** */
