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

  FileName    [mcTree.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si)]
  Description [The file mcTree.c contains functions for diagnostic tree.]
  SeeAlso     [mc.h, mcInt.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 "mcInt.h"

/*-----------------------------------------------------------------------*/
/* Type declarations                                                     */
/*-----------------------------------------------------------------------*/

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

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

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

static Bdd_Edge Reachable(Bdd_Edge D, Bdd_Edge init);

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

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

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

/**Function****************************************************************
  Synopsis    []
  Description [EE[phi {chi} U {chi'} phi']]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEEU(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge valid)
{
  Bdd_Edge td,tree;
  Bdd_Edge sup1,sup2;

  /* calculation of TREE */

  td = Bdd_RelOp(a1,valid,"#AND R2S",TRUE);
  td = Bdd_ITE(valid,td,bdd_termFalse);
  td = Bdd_ITE(td,McDgn.D,bdd_termFalse);        /* td = [valid -a1-> valid] */
  Bdd_Fortify(td);

  td = Reachable(td,McDgn.init);

  sup1 = Bdd_RelOpSimple(td,"Ex xA xR S2R",TRUE);
  sup1 = Bdd_ITE(sup1,bdd_termTrue,Bdd_ITE(McDgn.init,valid,bdd_termFalse));

  sup2 = Bdd_RelOp(a2,s2,"#AND R2S",TRUE);
  sup2 = Bdd_ITE(sup1,sup2,bdd_termFalse);
  sup2 = Bdd_ITE(sup2,McDgn.D,bdd_termFalse);

  tree = Bdd_ITE(td,bdd_termTrue,sup2);
  Bdd_Fortify(tree);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [AA[phi {chi} W {chi'} phi']]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAAW(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge valid)
{
  Bdd_Edge td,tree;
  Bdd_Edge sall,invalid;
  Bdd_Edge sup,sup1,sup2,D1not,D2not_ras;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(McDgn.D,bdd_termFalse)) return bdd_termFalse; /* CAREFULLY !!! */

  sup1 = Bdd_RelOpSimple(McDgn.D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(McDgn.D,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);
  Bdd_Fortify(sall);                 /* sall = the set of all states */

  invalid = Bdd_ITE(valid,bdd_termFalse,sall);
  Bdd_Fortify(invalid);

  sup = Bdd_ITE(a1,s1,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  D1not = Bdd_ITE(sup,bdd_termFalse,McDgn.D);
  Bdd_Fortify(D1not);                    /* D1not = delta_not(a1,s1) */

  sup = Bdd_ITE(a2,s2,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  D2not_ras = Bdd_ITE(sup,bdd_termFalse,McDgn.D);
  Bdd_Fortify(D2not_ras);                /* D2not = delta_not(a2,s2) */

  /* calculation of TREE */

  td = Bdd_RelOp(a1,invalid,"#AND R2S",TRUE);
  td = Bdd_ITE(invalid,td,bdd_termFalse);
  td = Bdd_ITE(td,D2not_ras,bdd_termFalse);
  Bdd_Fortify(td);

  td = Reachable(td,McDgn.init);

  sup1 = Bdd_RelOpSimple(td,"Ex xA xR S2R",TRUE);
  sup1 = Bdd_ITE(sup1,bdd_termTrue,Bdd_ITE(McDgn.init,invalid,bdd_termFalse));

  sup2 = Bdd_ITE(D1not,sup1,bdd_termFalse);
  sup2 = Bdd_ITE(D2not_ras,sup2,bdd_termFalse);

  tree = Bdd_ITE(td,bdd_termTrue,sup2);
  Bdd_Fortify(tree);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [EEG phi {chi}]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEEG(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge td,tree;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(McDgn.D,bdd_termFalse)) return bdd_termFalse; /* CAREFULLY !!! */

  /* calculation of TREE */

  td = Bdd_RelOp(a,valid,"#AND R2S",TRUE);
  td = Bdd_ITE(valid,td,bdd_termFalse);
  td = Bdd_ITE(td,McDgn.D,bdd_termFalse);        /* td = [valid -a-> valid] */
  Bdd_Fortify(td);

  tree = Reachable(td,McDgn.init);
  Bdd_Fortify(tree);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [AAF {chi} phi]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAAF(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge td,tree;
  Bdd_Edge sall,invalid;
  Bdd_Edge sup,sup1,sup2,Dnot_ras;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(McDgn.D,bdd_termFalse)) return bdd_termFalse; /* CAREFULLY !!! */

  sup1 = Bdd_RelOpSimple(McDgn.D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(McDgn.D,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);
  Bdd_Fortify(sall);                     /* sall = the set of all states */

  invalid = Bdd_ITE(valid,bdd_termFalse,sall);
  Bdd_Fortify(invalid);

  /* calculation of TREE */

  sup = Bdd_ITE(a,s,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  Dnot_ras = Bdd_ITE(sup,bdd_termFalse,McDgn.D);
  Bdd_Fortify(Dnot_ras);                        /* Dnot = delta_not(a,s) */

  /* calculation of TREE */

  td = Bdd_RelOpSimple(invalid,"R2S",TRUE);
  td = Bdd_ITE(invalid,td,bdd_termFalse);
  td = Bdd_ITE(td,Dnot_ras,bdd_termFalse);
  Bdd_Fortify(td);

  tree = Reachable(td,McDgn.init);
  Bdd_Fortify(tree);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [AA[phi {chi} U {chi'} phi']]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAAU(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2,
          Bdd_Edge formAAW, Bdd_Edge formAAF)
{
  Bdd_Edge tree;
  Bdd_Edge treeAAW,treeAAF;

  treeAAW = McTreeAAW(s1,a1,a2,s2,formAAW);
  treeAAF = McTreeAAF(a2,s2,formAAF);

  tree =  Bdd_ITE(treeAAW,bdd_termTrue,treeAAF);
  Bdd_Fortify(tree);

  return tree;
}


/**Function****************************************************************
  Synopsis    []
  Description [EE[phi {chi} W {chi'} phi']]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEEW(Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2, Bdd_Edge s2,
          Bdd_Edge formEEU, Bdd_Edge formEEG)
{
  Bdd_Edge tree;
  Bdd_Edge treeEEU,treeEEG;

  treeEEU = McTreeEEU(s1,a1,a2,s2,formEEU);
  treeEEG = McTreeEEG(s1,a1,formEEG);

  tree =  Bdd_ITE(treeEEU,bdd_termTrue,treeEEG);
  Bdd_Fortify(tree);

  return tree;
}


/**Function****************************************************************
  Synopsis    []
  Description [EEX {chi} phi, <chi> phi]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEEX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge tree;

  tree =  McTreeEEU(bdd_termTrue,bdd_termFalse,a,s,valid);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [AAX {chi} phi]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAAX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge tree;

  tree =  McTreeAAW(bdd_termTrue,bdd_termFalse,a,s,valid);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description [EEF {chi} phi]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEEF(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge tree;

  tree =  McTreeEEU(bdd_termTrue,bdd_termTrue,a,s,valid);

  return tree;
}


/**Function****************************************************************
  Synopsis    []
  Description [AAG phi {chi}]
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAAG(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  Bdd_Edge tree;

  tree =  McTreeAAW(s,a,bdd_termFalse,bdd_termFalse,valid);

  return tree;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEU(Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEF(Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeEG(Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAU(Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAX(Bdd_Edge a, Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAF(Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeAG(Bdd_Edge s, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeHME(Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2, Bdd_Edge valid)
{
  return bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This is experimental!]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
McTreeHMA(Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2, Bdd_Edge valid)
{
  return bdd_termNull;
}

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

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

Bdd_Edge
Reachable(Bdd_Edge D, Bdd_Edge init)
{
  Bdd_Edge Z,last,sup;

  Z = init;
  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    Bdd_IncCounter();
    Bdd_Fresh(Z);

    last = Z;
    sup = Bdd_RelOp(Z,D,"#AND Ex xA xR S2R",TRUE);
    Z = Bdd_ITE(Z,bdd_termTrue,sup);
  }

  Z = Bdd_ITE(Z,D,bdd_termFalse);
  Bdd_Fortify(Z);

  return Z;
}
