Modification grammaire CTL, ajout du mot cle RESET_COND pour

specifier une condition de RESET.
Correction de differents BUGs dans mocha (quantification universelle
systematique sur les entrees lors de l'interpretation des formules CTL)
Mise a jour des mans

alliance/src/ctl/man5/ctl.5

@@ -67,7 +67,13 @@ support also the imply boolean operator '->' and the equivalence operator '<=>'.
 -- be careful, the assumption condition is not applied 
 -- to the initial conditions.
 
-   INITIAL  init1 := (reset='1');
+   RESET_COND init1 := (reset='1');
+
+-- It is also possible to describe the first state
+-- with the INITIAL keywork, as follows:
+--
+-- INITIAL init1 := ((A_CS=A_E0) AND (B_CS=B_E0));
+--
 
 -- formulae description statement part
 

alliance/src/ctl/src/ctl.h

@@ -60,7 +60,8 @@
 # define CTL_DECLAR_DEFINE          2
 # define CTL_DECLAR_ASSUME          3
 # define CTL_DECLAR_INITIAL         4
-# define CTL_MAX_DECLAR_TYPE        5
+# define CTL_DECLAR_RESET           5
+# define CTL_MAX_DECLAR_TYPE        6
 
 /*------------------------------------------------------\
 |                                                       |
@@ -87,6 +88,7 @@
 # define GetCtlNumDeclDef( F )   ((F)->HASH_DECLAR[ CTL_DECLAR_DEFINE   ]->NUMBER_ELEM)
 # define GetCtlNumDeclAss( F )   ((F)->HASH_DECLAR[ CTL_DECLAR_ASSUME   ]->NUMBER_ELEM)
 # define GetCtlNumDeclInit( F )  ((F)->HASH_DECLAR[ CTL_DECLAR_INITIAL  ]->NUMBER_ELEM)
+# define GetCtlNumDeclReset( F ) ((F)->HASH_DECLAR[ CTL_DECLAR_RESET    ]->NUMBER_ELEM)
 
 /*------------------------------------------------------\
 |                                                       |
@@ -102,6 +104,8 @@
     (searchctlsym( (F), (N), (I), CTL_DECLAR_ASSUME   ))
 # define searchctlsyminit( F, N, I ) \
     (searchctlsym( (F), (N), (I), CTL_DECLAR_INITIAL  ))
+# define searchctlsymreset( F, N, I ) \
+    (searchctlsym( (F), (N), (I), CTL_DECLAR_RESET ))
 # define searchctlsymall( F, N, I ) \
     (searchctlsym( (F), (N), (I), CTL_DECLAR_ALL ))
 
@@ -119,6 +123,8 @@
     (searchctldecl( (F), (N), CTL_DECLAR_ASSUME   ))
 # define searchctldeclinit( F, N ) \
     (searchctldecl( (F), (N), CTL_DECLAR_INITIAL  ))
+# define searchctldeclreset( F, N ) \
+    (searchctldecl( (F), (N), CTL_DECLAR_RESET  ))
 # define searchctldeclall( F, N ) \
     (searchctldecl( (F), (N), CTL_DECLAR_ALL ))
 
@@ -306,6 +312,7 @@
   extern ctldecl_list *addctldecldef __P((ctlfig_list *Figure, vexexpr *Atom));
   extern ctldecl_list *addctldeclass __P((ctlfig_list *Figure, vexexpr *Atom));
   extern ctldecl_list *addctldeclinit __P((ctlfig_list *Figure, vexexpr *Atom));
+  extern ctldecl_list *addctldeclreset __P((ctlfig_list *Figure, vexexpr *Atom));
 
   extern  ctlline_list *addctlline __P((ctlfig_list *Figure, ctlline_list **HeadLine, long Line));
   extern  ctlline_list *addctlfileline __P((ctlfig_list *Figure, ctlline_list **HeadLine, char *File, long Line));

alliance/src/ctl/src/ctladd.c

@@ -74,7 +74,8 @@
     "VARIABLE",
     "DEFINE",
     "ASSUME",
-    "INITIAL"
+    "INITIAL",
+    "RESET"
   };
 
 /*------------------------------------------------------------\
@@ -350,6 +351,35 @@ ctldecl_list *addctldeclinit( Figure, Atom )
   return( Initial );
 }
 
+/*------------------------------------------------------------\
+|                                                             |
+|                     Ctl Add Declaration Reset               |
+|                                                             |
+\------------------------------------------------------------*/
+
+ctldecl_list *addctldeclreset( Figure, Atom )
+
+   ctlfig_list   *Figure;
+   vexexpr       *Atom;
+{
+  ctldecl_list *Initial;
+  char         *Name;
+
+  if ( ! IsVexNodeAtom( Atom ) ) Name = getvexarrayname( Atom );
+  else                           Name = GetVexAtomValue( Atom );
+
+  Initial = searchctldeclall( Figure, Name );
+
+  if ( Initial != (ctldecl_list *)0 )
+  {
+    ctlerror( CTL_DECLAR_EXIST_ERROR, Name, 0 );
+  }
+
+  Initial = loc_addctldecl( Figure, Atom, CTL_DECLAR_RESET );
+
+  return( Initial );
+}
+
 /*------------------------------------------------------------\
 |                                                             |
 |                         Ctl Add File Line                   |

alliance/src/mocha/man1/moka.1

@@ -23,8 +23,8 @@ In particular VHDL type MUX_BIT and WOR_BIT aren't not supported.
 First of all \fBmoka\fP build the fonction transition of the FSM using
 a Reduced Ordered Binary Decision Diagrams representation.
 .br
-It then applies the initial condition to find the first state (keyword INITIAL
+It then applies the initial conditions to find the first state (keyword INITIAL
-in the CTL(5) file format).
+and/or RESET_COND in the CTL(5) file format).
 .br
 After it computes a symbolic simulation of the FSM in order
 to find all reachable states. This computation takes into account the 
@@ -215,7 +215,7 @@ END FSM;
    VARIABLE    ack      : BIT;
    VARIABLE    req      : BIT;
 
-   INITIAL  init1 := (reset='1');
+   RESET_COND init1 := (reset='1');
    ASSUME     ass1  := (reset='0');
 
 begin

alliance/src/mocha/src/mocha_beh.c

@@ -171,6 +171,7 @@ void MochaPostTreatVerifyBeh( MochaFigure, FlagVerbose )
   MochaFigure->HASH_BEH_OUT = BehOutHashTable;
 }
 
+
 /*------------------------------------------------------------\
 |                                                             |
 |                        MochaCompileBeh                      |

alliance/src/mocha/src/mocha_check.c

@@ -24,7 +24,6 @@
 | 675 Mass Ave, Cambridge, MA 02139, USA.                     |
 |                                                             |
 \------------------------------------------------------------*/
-
 /*------------------------------------------------------------\
 |                                                             |
 | Tool    :                     MOCHA                         |
@@ -146,26 +145,43 @@ void MochaCheckViewTransFunc( VarFunc )
   MochaCheckViewBddNode( VarFunc->FUNC );
 }
 
+/*------------------------------------------------------------\
+|                                                             |
+|                      MochaCheckViewBddStateNode             |
+|                                                             |
+\------------------------------------------------------------*/
+
+static void MochaCheckViewBddStateNode( BddNode )
+   
+   bddnode *BddNode;
+{
+  ablexpr *Expr;
+     
+  Expr = convertbddcircuitabl( (bddcircuit *)0, BddNode );
+  viewablexpr( Expr, ABL_VIEW_VHDL );
+  freeablexpr( Expr );
+}
+
 /*------------------------------------------------------------\
 |                                                             |
 |                      MochaCheckViewState                    |
 |                                                             |
 \------------------------------------------------------------*/
 
-static int MochaCheckViewState( MochaFigure, BddNode )
+static int MochaCheckViewState( MochaFigure, BddStateSet )
 
   mochafig_list *MochaFigure;
-  bddnode       *BddNode;
+  bddnode       *BddStateSet;
 {
   mochafsm_list   *MochaFsm;
   mochastate_list *MochaState;
   bddnode         *BddState;
-  bddnode         *BddStateSet;
   bddnode         *BddReached;
   bddnode         *BddFirst;
   bddnode         *BddFsm;
   bddnode         *BddAssume;
   bddnode         *BddCheck;
+  bddnode         *BddOther;
   bddassoc        *BddAssoc;
   bddassoc        *BddRegAssoc;
   int              First;
@@ -177,18 +193,13 @@ static int MochaCheckViewState( MochaFigure, BddNode )
   BddFirst    = MochaFigure->BDD_FIRST_STATE;
   BddAssume   = MochaFigure->BDD_ASSUME;
 
-  BddStateSet = applybddnode( (bddsystem *)0, ABL_AND, BddNode    , BddAssume   );
-  BddStateSet = existbddnodemissassoc( (bddsystem *)0, BddStateSet, BddRegAssoc );
-  BddStateSet = applybddnode( (bddsystem *)0, ABL_AND, 
-                              decbddrefext( BddStateSet ), BddReached );
-
   if ( BddStateSet == BddLocalSystem->ZERO )
   {
     fprintf( stdout, "\t    > state set empty !\n" );
     return ( 0 );
   }
 
-  if ( BddNode == BddReached ) 
+  if ( BddStateSet == BddReached ) 
   {
     fprintf( stdout, "\t    > all reachable states\n" );
     return ( 1 );
@@ -200,17 +211,12 @@ static int MochaCheckViewState( MochaFigure, BddNode )
   if ( BddCheck == BddFirst ) First = 1;
   else                        First = 0;
 
-
-  if ( MochaFigure->FSM == (mochafsm_list *)0 )
-  {
-    return( First );
-  }
-
   fprintf( stdout, "\t    > states set:\n" );
 
   while ( BddStateSet != BddLocalSystem->ZERO )
   {
     BddCheck = satisfybddnodeassoc( (bddsystem *)0, BddStateSet, BddRegAssoc ); 
+    BddOther = incbddrefext( BddCheck );
 
     fprintf( stdout, "\t       " );
 
@@ -221,20 +227,32 @@ static int MochaCheckViewState( MochaFigure, BddNode )
       BddAssoc = MochaFsm->BDD_ASSOC_STATE;
       BddFsm   = existbddnodemissassoc( (bddsystem *)0, BddCheck, BddAssoc );
 
+      BddOther = existbddnodeassoc( (bddsystem *)0, 
+                                    decbddrefext( BddOther ), BddAssoc );
+
       for ( MochaState  = MochaFsm->STATE;
             MochaState != (mochastate_list *)0;
             MochaState  = MochaState->NEXT )
       {
-        BddState = applybddnode( (bddsystem *)0, ABL_AND, BddFsm, MochaState->BDD_STATE );
+        BddState = applybddnode( (bddsystem *)0, ABL_AND,
+                                 BddFsm, MochaState->BDD_STATE );
         decbddrefext( BddState );
 
         if ( BddState == MochaState->BDD_STATE )
         {
-          fprintf( stdout, "%s[%s] ", MochaFsm->NAME, MochaState->NAME  ); break;
+          fprintf( stdout, "%s[%s] ", MochaFsm->NAME, MochaState->NAME );
+          break;
         }
       }
     }
 
+    if ( ( BddOther != BddLocalSystem->ONE  ) &&
+         ( BddOther != BddLocalSystem->ZERO ) )
+    {
+      MochaCheckViewBddStateNode( BddOther );
+      decbddrefext( BddOther );
+    }
+
     if ( BddCheck == BddFirst )
     {
       fprintf( stdout, " (first state)\n" );
@@ -390,12 +408,15 @@ static void MochaCheckComputeFirstState( MochaFigure )
   ctldecl_list  *CtlDeclar;
   biablarray    *BiAblArray;
   ablarray      *AblArray;
+  bddassoc      *BddRegAssoc;
   bddnode       *BddNode;
   bddnode       *BddCurrentSet;
   bddnode       *BddReg;
   bddnode       *BddInit;
+  bddnode       *BddReset;
   bddnode       *BddAssume;
   ablexpr       *AblInit;
+  ablexpr       *AblReset;
   ablexpr       *AblAssume;
   bereg_list    *BehReg;
   binode_list   *BiNode;
@@ -403,6 +424,7 @@ static void MochaCheckComputeFirstState( MochaFigure )
 
   BehFigure   = MochaFigure->BEH_FIGURE;
   CtlFigure   = MochaFigure->CTL_FIGURE;
+  BddRegAssoc = MochaFigure->BDD_ASSOC_REG;
 
   setbddlocalcircuit( MochaFigure->BDD_CIRCUIT );
 /*
@@ -447,10 +469,46 @@ static void MochaCheckComputeFirstState( MochaFigure )
     MochaPrintf( stdout, "The initial condition is equal to zero !\n" );
     autexit( 1 );
   }
+/*
+** Should verify :  TO BE DONE
+**
+** a) BddInit Describe only one state (by using Bdd satisfy method)
+** b) BddInit support contains only registers atom (BehReg)
+*/
+
+/*
+** Convert the reset conditions to a Bdd node
+*/
+  BddReset = BddLocalSystem->ONE;
+
+  for ( CtlDeclar  = CtlFigure->DECLAR[ CTL_DECLAR_RESET ];
+        CtlDeclar != (ctldecl_list *)0;
+        CtlDeclar  = CtlDeclar->NEXT )
+  {
+    BiAblArray = MOCHA_CTL_BIABLA( CtlDeclar );
+    AblArray   = BiAblArray->EXPR;
+    AblReset   = AblArray->ARRAY[ 0 ];
+
+    BddNode  = addbddcircuitabl( (bddcircuit *)0, AblReset  );
+    BddReset = applybddnode( (bddsystem *)0, ABL_AND, 
+                              decbddrefext( BddInit  ), decbddrefext( BddNode ) );
+  }
+
+  if ( BddReset == BddLocalSystem->ZERO )
+  {
+    MochaPrintf( stdout, "The reset condition is equal to zero !\n" );
+    autexit( 1 );
+  }
+/*
+** Should verify :  TO BE DONE
+**
+** a) BddReset support contains only primary input atom
+*/
+
 /*
 ** Search the initial state !
 */
-  BddCurrentSet = BddLocalSystem->ONE;
+  BddCurrentSet = BddInit;
 
   for ( BehReg  = BehFigure->BEREG;
         BehReg != (bereg_list *)0;
@@ -462,15 +520,13 @@ static void MochaCheckComputeFirstState( MochaFigure )
 /*
 ** Search the initial value of the state registers
 */
-    BddNode = cofactorbddnode( (bddsystem *)0, BiNode->VALNODE, BddInit );
+    BddNode = cofactorbddnode( (bddsystem *)0, BiNode->VALNODE, BddReset );
 
     if ( BddNode == BddLocalSystem->ONE  ) BitZero = 0;
     else
     if ( BddNode != BddLocalSystem->ZERO )
     {
-      MochaPrintf( stdout, "Invalid initial conditions: %s not initialized !\n", BehReg->NAME );
+      decbddrefext( BddNode ); continue;
-      MochaCheckViewBddNode( BddNode );
-      autexit( 1 );
     }
 
     if ( BitZero ) BddNode = applybddnodenot( (bddsystem *)0, BddReg );
@@ -486,6 +542,15 @@ static void MochaCheckComputeFirstState( MochaFigure )
   testbddcircuit( (bddcircuit *)0 );
 # endif
 
+  BddNode = satisfybddnodeassoc( (bddsystem *)0, BddCurrentSet, BddRegAssoc ); 
+  decbddrefext( BddNode );
+
+  if ( BddNode != BddCurrentSet )
+  {
+    MochaPrintf( stdout, "Bad initial/reset condition, all registers are not initialized !\n" );
+    autexit( 1 );
+  }
+
   MochaFigure->BDD_FIRST_STATE = BddCurrentSet;
 }
 
@@ -526,6 +591,8 @@ static void MochaCheckComputeReachableStates( MochaFigure )
     decbddrefext( BddCurrentSet );
 
     BddNode   = applybddnodenot( (bddsystem *)0, BddReachedSet );
+
+
     BddNewSet = applybddnode( (bddsystem *)0, ABL_AND,
                               decbddrefext( BddNode ), decbddrefext( BddNewSet ) );
 
@@ -543,7 +610,7 @@ static void MochaCheckComputeReachableStates( MochaFigure )
   testbddcircuit( (bddcircuit *)0 );
 # endif
 
-  if ( MochaFigure->DEBUG )
+  if ( MochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "First state " );
     MochaCheckViewBddNode( MochaFigure->BDD_FIRST_STATE );
@@ -600,6 +667,57 @@ static bddnode *MochaCheckCtlAblBoolean( Expr )
   return( BddFirst );
 }
 
+/*------------------------------------------------------------\
+|                                                             |
+|                    MochaCheckCtlBddQuantify                 |
+|                                                             |
+\------------------------------------------------------------*/
+
+static bddnode *MochaCheckCtlBddQuantify( BddNode )
+
+  bddnode *BddNode;
+{
+  bddnode      *BddReached; 
+  bddnode      *BddAssume;
+  bddnode      *BddAssumeNot;
+  btrtransfunc *BtrTransFunc;
+  bddassoc     *BddAssoc;
+  bddnode      *BddNew;
+
+  BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
+  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
+  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
+  BddAssume    = MochaMochaFigure->BDD_ASSUME;
+
+  if ( MochaMochaFigure->FLAG_DEBUG )
+  {
+    fprintf( stdout, "BDD FORALL[\n" );
+    MochaCheckViewBddNode( BddNode );
+    fprintf( stdout, "]\n" );
+  }
+
+  BddNew = applybddnode( (bddsystem *)0, ABL_AND, BddNode, BddAssume );
+
+  BddAssumeNot = applybddnodenot( (bddsystem *)0, BddAssume );
+
+  BddNew = applybddnode( (bddsystem *)0, ABL_OR,
+                         decbddrefext( BddNew ), decbddrefext( BddAssumeNot ) );
+
+  BddNew = forallbddnodemissassoc( (bddsystem *)0,
+                                   decbddrefext( BddNew ), BddAssoc );
+
+  BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
+                           decbddrefext( BddNew ), BddReached );
+
+  if ( MochaMochaFigure->FLAG_DEBUG )
+  {
+    fprintf( stdout, "-> " );
+    MochaCheckViewBddNode( BddNew );
+    fprintf( stdout, "\n" );
+  }
+
+  return( BddNew );
+}
 
 /*------------------------------------------------------------\
 |                                                             |
@@ -612,38 +730,26 @@ static bddnode *MochaCheckCtlBddEX( BddNode )
   bddnode *BddNode;
 {
   bddnode      *BddNew;
-  bddnode      *BddReached; 
-  bddnode      *BddAssume;
   btrtransfunc *BtrTransFunc;
-  bddassoc     *BddAssoc;
 
   BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
-  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
-  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
-  BddAssume    = MochaMochaFigure->BDD_ASSUME;
-
   BddNew       = preimagebtrtransfunc( BtrTransFunc, BddNode );
 
-# if 0
+  if ( MochaMochaFigure->FLAG_DEBUG )
-  fprintf( stdout, "EX[\n" );
+  {
+    fprintf( stdout, "BDD EX[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
-# endif
+  }
 
-  BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+  BddNew = MochaCheckCtlBddQuantify( decbddrefext( BddNew ) );
-                         decbddrefext( BddNew ), BddAssume );
 
-  BddNew = existbddnodemissassoc( (bddsystem *)0,
+  if ( MochaMochaFigure->FLAG_DEBUG )
-                                   decbddrefext( BddNew ), BddAssoc );
+  {
-
-  BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
-                           decbddrefext( BddNew ), BddReached );
-
-# if 0
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddNew );
     fprintf( stdout, "\n" );
-# endif
+  }
 
   return( BddNew );
 }
@@ -660,43 +766,31 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
 {
   bddnode      *BddOld;
   bddnode      *BddNew;
-  bddnode      *BddReached; 
-  bddnode      *BddAssume;
   btrtransfunc *BtrTransFunc;
-  bddassoc     *BddAssoc;
 
   BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
-  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
-  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
-  BddAssume    = MochaMochaFigure->BDD_ASSUME;
   BddOld       = BddLocalSystem->ONE;
   BddNew       = incbddrefext( BddNode );
 
-# if 0
+  if (  MochaMochaFigure->FLAG_DEBUG )
-  fprintf( stdout, "EX[\n" );
+  {
+    fprintf( stdout, "BDD EG[\n" );
+
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
-# endif
+  }
 
   while ( BddNew != BddOld )
   {
     BddOld = BddNew;
 
     BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
-
-    BddNew = applybddnode( (bddsystem *)0, ABL_AND, 
-                           decbddrefext( BddNew ), BddAssume );
-
     BddNew = applybddnode( (bddsystem *)0, ABL_AND,
                             decbddrefext( BddNew ), BddNode );
 
-    BddNew = existbddnodemissassoc( (bddsystem *)0,
+    BddNew = MochaCheckCtlBddQuantify( decbddrefext( BddNew ) );
-                                    decbddrefext( BddNew ), BddAssoc );
 
-    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+# ifdef DEBUG
-                            decbddrefext( BddNew ), BddReached );
-
-# if 0
     fprintf( stdout, "MochaCheckCtlBddEG:\n" );
     MochaCheckViewBddNode( BddNew );
 # endif
@@ -704,11 +798,12 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
     decbddrefext( BddOld );
   }
 
-# if 0
+  if ( MochaMochaFigure->FLAG_DEBUG )
+  {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddNew );
     fprintf( stdout, "\n" );
-# endif
+  }
 
   return( BddNew );
 }
@@ -726,25 +821,20 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
 {
   bddnode      *BddOld;
   bddnode      *BddNew;
-  bddnode      *BddReached; 
-  bddnode      *BddAssume;
   btrtransfunc *BtrTransFunc;
-  bddassoc     *BddAssoc;
 
   BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
-  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
-  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
-  BddAssume    = MochaMochaFigure->BDD_ASSUME;
   BddOld       = BddLocalSystem->ZERO;
   BddNew       = incbddrefext( BddNodeQ );
 
-# if 0
+  if ( MochaMochaFigure->FLAG_DEBUG )
-  fprintf( stdout, "EU[\n" );
+  {
+    fprintf( stdout, "BDD EU[\n" );
     MochaCheckViewBddNode( BddNodeP );
     fprintf( stdout, ", \n" );
     MochaCheckViewBddNode( BddNodeQ );
     fprintf( stdout, "]\n" );
-# endif
+  }
 
   while ( BddNew != BddOld )
   {
@@ -752,22 +842,15 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
 
     BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
 
-    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
-                            decbddrefext( BddNew ), BddAssume );
-
     BddNew = applybddnode( (bddsystem *)0, ABL_AND,
                             decbddrefext( BddNew ), BddNodeP );
 
     BddNew = applybddnode( (bddsystem *)0, ABL_OR,
                            decbddrefext( BddNew ), BddNodeQ );
 
-    BddNew = existbddnodemissassoc( (bddsystem *)0,
+    BddNew = MochaCheckCtlBddQuantify( decbddrefext( BddNew ) );
-                                     decbddrefext( BddNew ), BddAssoc );
 
-    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+# ifdef DEBUG
-                            decbddrefext( BddNew ), BddReached );
-
-# if 0
     fprintf( stdout, "MochaCheckCtlBddEU:\n" );
     MochaCheckViewBddNode( BddNew );
 # endif
@@ -775,11 +858,12 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
     decbddrefext( BddOld );
   }
 
-# if 0
+  if ( MochaMochaFigure->FLAG_DEBUG )
+  {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddNew );
     fprintf( stdout, "\n" );
-# endif
+  }
 
   return( BddNew );
 }
@@ -796,7 +880,6 @@ static bddnode *MochaCheckCtlAblAF( Expr )
 {
   bddnode *BddNode;
   bddnode *BddResult;
-  bddnode *BddReached; 
 
   /* AF p <=> ! EG( ! p ) */
 
@@ -804,23 +887,22 @@ static bddnode *MochaCheckCtlAblAF( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "AF[\n" );
+    fprintf( stdout, "ABL AF[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddNode   = applybddnodenot( (bddsystem *)0, decbddrefext( BddNode ) );
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEG( BddNode );
   decbddrefext( BddNode );
   BddResult = applybddnodenot( (bddsystem *)0, decbddrefext( BddResult ) );
+  BddResult = MochaCheckCtlBddQuantify( decbddrefext( BddResult ) );
 
-  BddReached = MochaMochaFigure->BDD_REACHED_STATE;
+  if ( MochaMochaFigure->FLAG_DEBUG )
-  BddResult  = applybddnode( (bddsystem *)0, ABL_AND,
-                              decbddrefext( BddResult ), BddReached ); 
-
-  if ( MochaMochaFigure->DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -842,7 +924,6 @@ static bddnode *MochaCheckCtlAblAG( Expr )
 {
   bddnode *BddNode;
   bddnode *BddResult;
-  bddnode *BddReached; 
 
   /* AG p <=> ! EF( ! p ) <=> ! EU( 1, ! p ) */
 
@@ -850,23 +931,22 @@ static bddnode *MochaCheckCtlAblAG( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "AG[\n" );
+    fprintf( stdout, "ABL AG[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddNode   = applybddnodenot( (bddsystem *)0, decbddrefext( BddNode ) );
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEU( BddLocalSystem->ONE, BddNode );
   decbddrefext( BddNode );
   BddResult = applybddnodenot( (bddsystem *)0, decbddrefext( BddResult ) );
+  BddResult = MochaCheckCtlBddQuantify( decbddrefext( BddResult ) );
 
-  BddReached = MochaMochaFigure->BDD_REACHED_STATE;
+  if ( MochaMochaFigure->FLAG_DEBUG )
-  BddResult  = applybddnode( (bddsystem *)0, ABL_AND,
-                              decbddrefext( BddResult ), BddReached ); 
-
-  if ( MochaMochaFigure->DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -888,7 +968,6 @@ static bddnode *MochaCheckCtlAblAX( Expr )
 {
   bddnode *BddNode;
   bddnode *BddResult;
-  bddnode *BddReached; 
 
   /* AX p <=> ! EX( ! p ) */
 
@@ -896,23 +975,22 @@ static bddnode *MochaCheckCtlAblAX( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "AX[\n" );
+    fprintf( stdout, "ABL AX[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddNode   = applybddnodenot( (bddsystem *)0, decbddrefext( BddNode ) );
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEX( BddNode );
   decbddrefext( BddNode );
   BddResult = applybddnodenot( (bddsystem *)0, decbddrefext( BddResult ) );
+  BddResult = MochaCheckCtlBddQuantify( decbddrefext( BddResult ) );
 
-  BddReached = MochaMochaFigure->BDD_REACHED_STATE;
+  if ( MochaMochaFigure->FLAG_DEBUG )
-  BddResult  = applybddnode( (bddsystem *)0, ABL_AND,
-                              decbddrefext( BddResult ), BddReached ); 
-
-  if ( MochaMochaFigure->DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -938,33 +1016,40 @@ static bddnode *MochaCheckCtlAblAU( Expr )
   bddnode *BddResult1;
   bddnode *BddResult2;
   bddnode *BddResult;
-  bddnode *BddReached; 
 
   /* AU( p, q ) <=> ! EU( ! q, ! p * ! q ) * ! EG( ! q ) */
 
   Expr      = ABL_CDR( Expr );
   BddNode1  = MochaCheckCtlAbl( ABL_CAR( Expr ) );
+
   Expr      = ABL_CDR( Expr );
   BddNode2  = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "AU[\n" );
+    fprintf( stdout, "ABL AU[\n" );
     MochaCheckViewBddNode( BddNode1 );
     fprintf( stdout, ",\n" );
     MochaCheckViewBddNode( BddNode2 );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode1 = MochaCheckCtlBddQuantify( decbddrefext( BddNode1 ) );
+  BddNode2 = MochaCheckCtlBddQuantify( decbddrefext( BddNode2 ) );
+
   BddNode1  = applybddnodenot( (bddsystem *)0, decbddrefext( BddNode1 ) );
   BddNode2  = applybddnodenot( (bddsystem *)0, decbddrefext( BddNode2 ) );
+  BddNode3  = applybddnode( (bddsystem *)0, ABL_AND, BddNode1, BddNode2 );
+
+  BddNode1 = MochaCheckCtlBddQuantify( decbddrefext( BddNode1 ) );
+  BddNode2 = MochaCheckCtlBddQuantify( decbddrefext( BddNode2 ) );
+  BddNode3 = MochaCheckCtlBddQuantify( decbddrefext( BddNode3 ) );
 
   /* ! EG( ! q ) */
   BddResult1 = MochaCheckCtlBddEG( BddNode2 );
   BddResult1 = applybddnodenot( (bddsystem *)0, decbddrefext( BddResult1 ) );
 
   /* ! EU( ! q, ! p * ! q ) */
-  BddNode3  = applybddnode( (bddsystem *)0, ABL_AND, BddNode1, BddNode2 );
   BddResult2 = MochaCheckCtlBddEU( BddNode2, BddNode3 );
   BddResult2 = applybddnodenot( (bddsystem *)0, decbddrefext( BddResult2 ) );
 
@@ -976,11 +1061,9 @@ static bddnode *MochaCheckCtlAblAU( Expr )
                             decbddrefext( BddResult1 ),
                             decbddrefext( BddResult2 ) );
 
-  BddReached = MochaMochaFigure->BDD_REACHED_STATE;
+  BddResult = MochaCheckCtlBddQuantify( decbddrefext( BddResult ) );
-  BddResult  = applybddnode( (bddsystem *)0, ABL_AND,
-                              decbddrefext( BddResult ), BddReached ); 
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -1009,17 +1092,18 @@ static bddnode *MochaCheckCtlAblEF( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "EF[\n" );
+    fprintf( stdout, "ABL EF[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEU( BddLocalSystem->ONE, BddNode );
   decbddrefext( BddNode );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -1046,17 +1130,18 @@ static bddnode *MochaCheckCtlAblEX( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "EX[\n" );
+    fprintf( stdout, "ABL EX[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEX( BddNode );
   decbddrefext( BddNode );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -1083,17 +1168,18 @@ static bddnode *MochaCheckCtlAblEG( Expr )
 
   BddNode = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "EG[\n" );
+    fprintf( stdout, "ABL EG[\n" );
     MochaCheckViewBddNode( BddNode );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode   = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
   BddResult = MochaCheckCtlBddEG( BddNode );
   decbddrefext( BddNode );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -1122,21 +1208,23 @@ static bddnode *MochaCheckCtlAblEU( Expr )
   Expr      = ABL_CDR( Expr );
   BddNode2  = MochaCheckCtlAbl( ABL_CAR( Expr ) );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
-    fprintf( stdout, "EU[\n" );
+    fprintf( stdout, "ABL EU[\n" );
     MochaCheckViewBddNode( BddNode1 );
     fprintf( stdout, ",\n" );
     MochaCheckViewBddNode( BddNode2 );
     fprintf( stdout, "]\n" );
   }
 
+  BddNode1  = MochaCheckCtlBddQuantify( decbddrefext( BddNode1 ) );
+  BddNode2  = MochaCheckCtlBddQuantify( decbddrefext( BddNode2 ) );
   BddResult = MochaCheckCtlBddEU( BddNode1, BddNode2 );
 
   decbddrefext( BddNode1 );
   decbddrefext( BddNode2 );
 
-  if ( MochaMochaFigure->DEBUG )
+  if ( MochaMochaFigure->FLAG_DEBUG )
   {
     fprintf( stdout, "-> " );
     MochaCheckViewBddNode( BddResult );
@@ -1259,24 +1347,28 @@ static void MochaCheckCtlFormulae( MochaFigure, FlagVerbose )
 
   MochaMochaFigure = MochaFigure;
 
-# ifdef DEBUG
+  if ( MochaMochaFigure->FLAG_DEBUG )
+  {
     fprintf( stdout, "Reachable states:\n" );
     MochaCheckViewBddNode( BddReached );
 
     fprintf( stdout, "First state:\n" );
     MochaCheckViewBddNode( BddFirst );
-# endif
+  }
 
   for ( CtlForm  = CtlFigure->FORM;
         CtlForm != (ctlform_list *)0;
         CtlForm  = CtlForm->NEXT )
   {
     fprintf( stdout, "\t    Checking formula %s\n", CtlForm->NAME );
+    fprintf( stdout, "\t    " );
+    viewvexexprln( CtlForm->VEX_EXPR );
 
     BiAblArray = MOCHA_CTL_BIABLA( CtlForm );
     AblArray   = BiAblArray->EXPR;
 
     BddNode = MochaCheckCtlAbl( AblArray->ARRAY[ 0 ] );
+    BddNode = MochaCheckCtlBddQuantify( decbddrefext( BddNode ) );
 
     if ( ! MochaCheckViewState( MochaFigure, BddNode ) )
     {

alliance/src/mocha/src/mocha_ctl.c

@@ -720,7 +720,8 @@ static ablarray *MochaCtlVex2AblArray( Expr )
     if ( ( Oper >= VEX_AF ) &&
          ( Oper <= VEX_EU ) )
     {
-      MochaPrintf( stdout, "CTL operator must not be used in INITIAL or ASSUME expressions : " );
+      MochaPrintf( stdout,
+                   "CTL operator can not be used in INITIAL, RESET or ASSUME expressions : " );
       viewvexexprboundln( Expr );
       autexit( 1 );
     }
@@ -991,6 +992,7 @@ static void MochaCtlFigureVex2AblArray( MochaFigure )
   for ( DeclType  = CTL_DECLAR_DEFINE; DeclType < CTL_MAX_DECLAR_TYPE; DeclType++ )
   {
     if ( ( DeclType == CTL_DECLAR_ASSUME  ) ||
+         ( DeclType == CTL_DECLAR_RESET   ) ||
          ( DeclType == CTL_DECLAR_INITIAL ) ) MochaCtlNoCtlOper = 1;
     else                                      MochaCtlNoCtlOper = 0;
 
@@ -1057,9 +1059,10 @@ void MochaCompileCtl( MochaFigure, FileName, FlagVerbose )
 
   CtlFigure  = loadctlfig( FileName );
 
-  if ( CtlFigure->DECLAR[ CTL_DECLAR_INITIAL ] == (ctldecl_list *)0 )
+  if ( ( CtlFigure->DECLAR[ CTL_DECLAR_INITIAL ] == (ctldecl_list *)0 ) &&
+       ( CtlFigure->DECLAR[ CTL_DECLAR_RESET   ] == (ctldecl_list *)0 ) ) 
   {
-    MochaPrintf( stdout, "Missing initial condition in CTL figure %s\n", CtlFigure->NAME  );
+    MochaPrintf( stdout, "Missing initial/reset condition in CTL figure %s\n", CtlFigure->NAME  );
     autexit( 1 );
   }
 

alliance/src/mocha/src/mocha_main.c

@@ -179,7 +179,7 @@ int main( argc, argv )
        ( CtlFileName  == (char *)0 ) ) MochaUsage();
 
   MochaFigure = MochaAddFigure( DescFileName );
-  MochaFigure->DEBUG = FlagDebug;
+  MochaFigure->FLAG_DEBUG = FlagDebug;
 
   if ( FlagFsm )
   {

alliance/src/mocha/src/mocha_shared.c

@@ -52,7 +52,7 @@
 # include "vex.h"
 # include "ctl.h"
 # include "ctp.h"
-# include "beh.h"
+# include "abe.h"
 
 # include <stdio.h>
 # include <stdlib.h>

alliance/src/mocha/src/mocha_shared.h

@@ -105,7 +105,7 @@
      bddnode              *BDD_FIRST_STATE;
      bddnode              *BDD_ASSUME;
      bddnode              *BDD_REACHED_STATE;
-     short                 DEBUG;
+     short                 FLAG_DEBUG;
 
    } mochafig_list;