source: vis_dev/vis-2.3/src/rob/Robust.c @ 98

Last change on this file since 98 was 98, checked in by cecile, 12 years ago

add part of cex
File size: 49.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [Robust.c]
4
5  PackageName [rob]
6
7  Synopsis    [Functions for Robustness computation.]
8
9  Author      [Souheib baarir, Denis poitrenaud, J.M. Ilié]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of Paris VI.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF PARIS VI SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30*****************************************************************************/
31#include <cuPortInt.h>
32#include "Robust.h"
33
34#define         mymddGetVarById( mgr, id )      \
35    array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id))
36
37
38void
39conv_error_msg(FILE* f, char* cmd, type_err e){
40
41 
42  switch(e){
43  case eofile :fprintf(f,cmd); fprintf(f," error :");
44               fprintf(f," the output file cannot be read \n");
45               break;
46  case ecmd  :fprintf(f,cmd); fprintf(f," error :");
47               fprintf(f," the mdd is not set \n");
48               break;
49  case earg   :fprintf(f,cmd);fprintf(f," error : too many arguments\n");
50               fprintf(f,"usage: %s \" ltl_formula \" \n",cmd);
51               break;                                 
52  } 
53}
54
55void
56error_msg(FILE* f, char* cmd, type_err e){
57
58 
59  switch(e){
60  case ecmd :  fprintf(f,"usage: set_"), fprintf(f, cmd); fprintf(f," [-h] file\n");
61               fprintf(f,"  -h : print the command usage\n"); 
62               fprintf(f," file: file  file containing the ctl formula\n");
63               break;
64  case eofile :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error :");
65               fprintf(f,cmd); fprintf(f," ctl definition file cannot be read. Check permissions and path\n ");
66              break;
67  case earg   :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error : too many arguments\n"); break;
68  case enfile :fprintf(f,"set_");fprintf(f,cmd); fprintf(f," error :"); fprintf(f,cmd);
69               fprintf(f," ctl definition file not provided\n");break;
70  case eicmd : fprintf(f,"usage : set_init [-h] [-s #] [-v #] [[-m fmodel] [-g file] | -f file] \n");
71               fprintf(f,"  -h    : print the command usage\n"); 
72               fprintf(f,"  -s #  : print reachability information every printStep steps (0 for no information).\n");
73               fprintf(f,"  -v #  : verbosity level\n");
74               fprintf(f,"  -m  fmodel   :  precises the fault model, where fmodel can be one of the following :    \n");
75               fprintf(f,"                  usut   : a single fault on a single time unit     \n");
76               fprintf(f,"                  usmt   : a single fault on multiple time units    \n");
77               fprintf(f,"                  msut   : multiple falts on a sigle time unit      \n");
78               fprintf(f,"                  msmt   : multiple falts on a  multiple time units \n");
79               fprintf(f,"  -g file : compute the set of initial errors states with respect to a sequential elements protection, given in file\n");
80               fprintf(f,"  -f file : compute the set of initial errors states with respect to a ctl formula given in file\n");
81               
82            break;
83  case eiofile : fprintf(f,"set_init error : Protected/Formula definition file cannot be read. Check permissions and path\n ");
84              break;         
85  case ercmd : fprintf(f,"usage : robustness [-h] [-s #] [-v #] [-r #]\n");
86               fprintf(f,"  -h   : print the command usage\n"); 
87               fprintf(f,"  -s # : print reachability information every printStep steps (0 for no information).\n");
88               fprintf(f,"  -v # : verbosity level\n");
89               fprintf(f,"  -r # : robustness type 1 = rob1 default rob4\n");
90            break;           
91  } 
92}
93
94void get_number_of_states(Fsm_Fsm_t  *fsm, mdd_t* b, EpDouble* ep) {
95  array_t       *psVarsArray;
96  int           nvars;
97  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
98  psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
99  nvars = ComputeNumberOfBinaryStateVariables(mddManager, psVarsArray);
100
101  if (nvars <= EPD_MAX_BIN) {
102    EpdConvert(mdd_count_onset(mddManager, b, psVarsArray),ep);
103  }
104  else {
105    mdd_epd_count_onset(mddManager, b, psVarsArray, ep);
106  }
107}
108
109void print_number_of_states(char* msg, Fsm_Fsm_t  *fsm, mdd_t* b) {
110  EpDouble *ep = EpdAlloc();
111  get_number_of_states(fsm, b, ep);
112  char buff[1024];
113  EpdGetString(ep, buff); 
114 
115  EpdFree(ep);
116  (void) fprintf(vis_stdout, "%-50s%15s\n", msg, buff);
117}
118
119array_t *
120determine_non_protected_registers(Fsm_Fsm_t  *fsm, FILE *f) {
121  mdd_manager      *mddManager = Fsm_FsmReadMddManager(fsm);
122  array_t           *wordArray = array_alloc(char*, 0);
123  array_t *nonProtectedIdArray = array_alloc(int, 0);
124  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
125  int                  arrSize = array_n( psVarsArray );
126  int i, j;
127  char  word[1024];
128
129  if (!f) {
130    (void) fprintf(vis_stdout, "no register is protected \n");
131    //   return nonProtectedIdArray;
132  }
133  else{
134    fscanf(f, "%1023s", word);
135    while (!feof(f)) {
136      char *buff = (char*)malloc(strlen(word) + 1);
137      strcpy(buff, word);
138      array_insert_last(char*, wordArray, buff);
139      fscanf(f, "%1023s", word);
140    }
141    fclose(f);
142  }
143 
144  // construction du vecteur des registres non protégés
145  for ( i = 0 ; i < arrSize ; i++ ) {
146    int      mddId = array_fetch( int, psVarsArray, i );
147    mvar_type mVar = array_fetch(mvar_type, 
148                                 mdd_ret_mvar_list(mddManager),mddId);
149    int protect = 0, j;
150    for ( j = 0 ; j < array_n( wordArray ) ; j++ ) {
151      char* w = array_fetch( char*, wordArray, j );
152      int l = strlen(w);
153      //printf("%s \n",w);
154      if (l > 0 && w[l-1] == '*') {
155        if (strncmp(mVar.name, w, l-1) == 0) {
156          protect = 1;
157          break;
158        }
159      }
160      else if (strcmp(mVar.name, w) == 0) {
161        protect = 1;
162        break;
163      }
164    }
165    (void) fprintf(vis_stdout, "%-20s%10d", mVar.name, mVar.values);
166    if (protect) {
167      (void) fprintf(vis_stdout, "  protected\n");
168    }
169    else {
170      array_insert_last(int, nonProtectedIdArray, mddId);
171      (void) fprintf(vis_stdout, "  not protected\n");
172      if (mVar.values > 2)
173        (void) fprintf(vis_stdout, 
174                       "WARNING : the variable %s seems to be a control state (of %d values) and not a register\n", 
175                       mVar.name, mVar.values);
176    }
177  }
178
179  for ( i = 0 ; i < array_n( wordArray ) ; i++ )
180    free(array_fetch( char*, wordArray, i ));
181  array_free(wordArray);
182
183  return nonProtectedIdArray;
184}
185
186mdd_t* compute_error_states(Fsm_Fsm_t  *fsm, mdd_t* reachable, 
187                            int verbosityLevel, 
188                            int printStep, 
189                            FILE* protect) {
190  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
191  array_t       *nonProtectedIdArray;
192  mdd_t         *prec, *tmp1, *tmp2, *res, *reach, *old;
193  int numit = 0, arrSize;
194
195  // construction du vecteur des registres non protégés
196  nonProtectedIdArray = 
197    determine_non_protected_registers(fsm,protect);
198 
199  if (array_n(nonProtectedIdArray) == 
200     array_n( Fsm_FsmReadPresentStateVars(fsm) )) {
201    // All the registers are unprotected
202    return mdd_one(mddManager);
203  }
204
205  // calcul des états d'erreur
206  old = fsm->reachabilityInfo.initialStates;
207  reach = mdd_dup(reachable);
208  prec = mdd_zero(mddManager);
209  while (1) {
210    numit++;
211    if(verbosityLevel > 1){
212      (void) fprintf(vis_stdout, "iteration number: %15d\n", numit);
213      print_number_of_states("known error states = ", fsm, prec);
214    }
215
216    tmp1 = mdd_smooth(mddManager, reach, nonProtectedIdArray);
217    mdd_free(reach);
218    res = mdd_or(tmp1, prec, 1, 1);
219    mdd_free(tmp1);
220
221    if (mdd_lequal(res, prec, 1, 1)) {
222      if(verbosityLevel > 1)
223      (void) fprintf(vis_stdout, "number of iterations: %15d\n", numit);
224      mdd_free(prec);
225      array_free(nonProtectedIdArray);
226      fsm->reachabilityInfo.initialStates = old;
227      return res;
228    }
229
230    mdd_free(prec);prec = res;
231    fsm->reachabilityInfo.initialStates = mdd_dup(res);
232    reach = Fsm_FsmComputeReachableStates(
233                  fsm, 0,  verbosityLevel, printStep, 0, 0,
234                  0, 0, Fsm_Rch_Default_c, 0, 1, NIL(array_t),
235                  0, NIL(array_t));
236    mdd_free(fsm->reachabilityInfo.initialStates);
237  }
238
239  (void) fprintf(vis_stdout, "Oups, erreur grave\n");
240  assert(0);
241  return res;
242}
243
244mdd_t* error_states(Fsm_Fsm_t  *fsm, 
245                    mdd_t* reachable, 
246                    array_t *nonProtectedIdArray) {
247
248  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
249  mdd_t         *prec, *tmp1, *tmp2, *res, *reach, *old;
250  int numit = 0, arrSize;
251
252 
253  if (array_n(nonProtectedIdArray) == 
254      array_n( Fsm_FsmReadPresentStateVars(fsm) )) {
255    // All the registers are unprotected
256    return mdd_one(mddManager);
257  }
258
259  // calcul des états d'erreur
260  old = fsm->reachabilityInfo.initialStates;
261  reach = mdd_dup(reachable);
262  prec = mdd_zero(mddManager);
263
264  while (1) {
265   
266    tmp1 = mdd_smooth(mddManager, reach, nonProtectedIdArray);
267    mdd_free(reach);
268    res = mdd_or(tmp1, prec, 1, 1);
269    mdd_free(tmp1);
270   
271    if (mdd_lequal(res, prec, 1, 1)) {
272      mdd_free(prec);
273      fsm->reachabilityInfo.initialStates = old;
274      return res;
275    }
276   
277    mdd_free(prec);prec = res;
278    fsm->reachabilityInfo.initialStates = mdd_dup(res);
279    reach = Fsm_FsmComputeReachableStates(
280                                          fsm, 0,  0, 0, 0, 0,
281                                          0, 0, Fsm_Rch_Default_c, 
282                                          0, 1, NIL(array_t),
283                                          0, NIL(array_t));
284    mdd_free(fsm->reachabilityInfo.initialStates);
285  }
286
287  return res;
288}
289
290
291
292static array_t *
293getbddvars(  mdd_manager *mgr,
294             array_t *mvars) {
295    array_t *bdd_vars = array_alloc(bdd_t *, 0);
296    int i, j, mv_no;
297    mvar_type mv;
298    mdd_t *top;
299    bdd_t *temp;
300    array_t *mvar_list = mdd_ret_mvar_list(mgr);
301       
302       
303    if ( mvars == NIL(array_t) || array_n(mvars) == 0) {
304        printf("\nWARNING: Empty Array of MDD Variables\n");
305        return bdd_vars;
306    }
307   
308    for (i=0; i<array_n(mvars); i++) {
309        mv_no = array_fetch(int, mvars, i);
310        mv = array_fetch(mvar_type, mvar_list, mv_no);
311        if (mv.status == MDD_BUNDLED) {
312            (void) fprintf(stderr, 
313                        "\ngetbddvars: bundled variable %s used\n",mv.name);
314            fail("");
315        }
316
317        for (j=0; j<mv.encode_length; j++) {
318            temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) );
319            array_insert_last(bdd_t *, bdd_vars, temp);
320        }
321    }
322    return bdd_vars;
323 
324    for (i=0; i<array_n(bdd_vars); i++) {
325        temp = array_fetch(bdd_t *, bdd_vars, i);
326        bdd_free(temp);
327    }
328}
329
330static mdd_t*
331mdd_restrict(mdd_manager* mgr,
332             mdd_t* l,mdd_t* d){
333
334  DdNode * tmp=bdd_bdd_restrict(mgr, l->node,d->node);
335
336  if (tmp== DD_ONE((DdManager *)mgr) ) {
337    return mdd_one(mgr);
338  }
339
340  if (tmp==Cudd_Not(DD_ONE((DdManager *)mgr))) {
341    return mdd_zero(mgr);
342  }
343   
344  cuddRef(tmp);
345  return bdd_construct_bdd_t(mgr,tmp);
346}
347
348// injection effective d'une erreur dans le registre r à partir des états de S
349// return $S_{\left|r} \wedge \neg r \vee S_{\left|\neg r} \wedge r$
350static mdd_t* inj_register(mdd_manager *mddManager, mdd_t* S, mdd_t* r) {
351  mdd_t         *tmp1, *tmp2, *res;
352    tmp1 = mdd_restrict(mddManager, S, r);
353    tmp2 = mdd_and(tmp1, r, 1, 0);
354    mdd_free(tmp1);
355    res = tmp2;
356   
357    tmp2 = bdd_not(r);
358    tmp1 = mdd_restrict(mddManager, S, tmp2);
359    mdd_free(tmp2);
360    tmp2 = mdd_and(tmp1, r, 1, 1);
361    mdd_free(tmp1);
362   
363    tmp1 = mdd_or(res, tmp2, 1, 1);
364    mdd_free(res);
365    mdd_free(tmp2);
366    return tmp1;
367}
368
369// injection effective d'une erreur unique dans un des registres non protégés
370mdd_t* inj_us(mdd_manager *mddManager, array_t* bdd_not_protected, mdd_t* S) {
371  int   arrSize, i;
372  mdd_t *tmp1, *tmp2, *v, *res;
373 
374  res = mdd_zero(mddManager);
375  arrSize = array_n(bdd_not_protected);
376  for ( i = 0 ; i < arrSize ; i++ ) {
377    v = array_fetch(bdd_t *, bdd_not_protected, i);
378    tmp1 = inj_register(mddManager, S, v);
379    tmp2 = mdd_or(res, tmp1, 1, 1);
380    mdd_free(res);
381    mdd_free(tmp1);
382    res = tmp2;
383  }
384  return res;
385}
386
387// injection effective d'erreurs multiples
388// dans au moins un des registres non protégés
389mdd_t* inj_ms(mdd_manager *mddManager, 
390              array_t* bdd_not_protected, 
391              mdd_t* S) {
392  int   arrSize, i;
393  mdd_t *tmp1, *tmp2, *v, *res;
394  array_t* bdd_vars;
395 
396  res = mdd_zero(mddManager);
397  arrSize = array_n(bdd_not_protected);
398 
399  for ( i = 0 ; i < arrSize ; i++ ) {
400 
401    v = array_fetch(bdd_t *, bdd_not_protected, i);
402    tmp1 = inj_register(mddManager, S, v);
403   
404    bdd_vars = array_partial_dup(bdd_not_protected, i) ;
405    tmp2 = bdd_smooth(tmp1, bdd_vars);
406    mdd_free(tmp1);     
407    tmp1 = mdd_or(res, tmp2, 1, 1);
408    mdd_free(res);
409    mdd_free(tmp2);
410    array_free(bdd_vars);
411    res = tmp1;
412  }
413  return res;
414}
415
416/* mdd_t* error_states_us(Fsm_Fsm_t  *fsm,  */
417/*                     mdd_t* reachable,  */
418/*                     FILE* protected) { */
419
420/*   mdd_manager   *mddManager = Fsm_FsmReadMddManager(fsm); */
421/*   array_t       *nonProtectedIdArray,*bdd_vars, */
422/*                 *bdd_one_v= array_alloc(bdd_t *, 0);  */
423/*   mdd_t         *prec, *tmp1, *tmp2, *res, *reach, *old; */
424/*   int numit = 0, arrSize=0; */
425
426/*   construction du vecteur des registres non protégés */
427/*   nonProtectedIdArray =  */
428/*     determine_non_protected_registers(fsm,protected); */
429 
430/*   if (array_n(nonProtectedIdArray) ==  */
431/*       array_n( Fsm_FsmReadPresentStateVars(fsm) )) { */
432/*     All the registers are unprotected */
433/*     return mdd_one(mddManager); */
434/*   } */
435
436/*   bdd_vars = getbddvars(mddManager, nonProtectedIdArray); */
437/*   arrSize = array_n(bdd_vars); */
438
439/*   calcul des états d'erreur */
440/*   old = fsm->reachabilityInfo.initialStates; */
441/*   reach = mdd_dup(reachable); */
442/*   prec = mdd_zero(mddManager); */
443
444/*   do { */
445 
446/*     tmp1=  */
447/*     for (i=0; i<arrSize;++i){ */
448/*        v = array_fetch(bdd_t *, bdd_not_protected, i); */
449/*        array_insert(bdd_t *, bdd_one_v,0, v); */
450/*        tmp2 = bdd_smooth(tmp1, bdd_one_v); */
451/*        mdd_free(res); */
452/*        res = mdd_or(tmp1, tmp2, 1, 1); */
453/*        mdd_free(tmp1); */
454/*        tmp1=res; */
455/*     } */
456   
457/*     fsm->reachabilityInfo.initialStates = mdd_dup(res); */
458/*     reach = Fsm_FsmComputeReachableStates( */
459/*                                        fsm, 0,  0, 0, 0, 0, */
460/*                                        0, 0, Fsm_Rch_Default_c,  */
461/*                                        0, 1, NIL(array_t), */
462/*                                        0, NIL(array_t)); */
463/*     mdd_free(fsm->reachabilityInfo.initialStates); */
464/*   }while() */
465
466/*   return res; */
467
468/* } */
469
470
471
472
473
474
475
476
477
478
479
480
481// modÚle de faute unicité spaciale et unicité temporelle
482//(S doit désigner l'ensemble des états accessibles)
483mdd_t* error_states_us_ut(Fsm_Fsm_t  *fsm, 
484                          mdd_t* S, 
485                          FILE* protect) {
486  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
487  array_t     *nonProtectedIdArray, *bdd_vars;
488  mdd_t       *res;
489
490  // construction du vecteur des registres non protégés
491  nonProtectedIdArray = 
492    determine_non_protected_registers(fsm,protect);
493   
494  bdd_vars = getbddvars(mddManager, nonProtectedIdArray);
495  res = inj_us(mddManager, bdd_vars, S);
496  array_free(bdd_vars);
497  array_free(nonProtectedIdArray);
498  return res;
499}
500
501// modÚle de faute multiplicité spaciale et unicité temporelle
502// (S  doit  désigner l'ensemble des états accessibles)
503mdd_t* error_states_ms_ut(Fsm_Fsm_t  *fsm, 
504                          mdd_t* S, 
505                          FILE* protect) {
506  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
507  array_t     *nonProtectedIdArray, *bdd_vars;
508  mdd_t       *res;
509
510  // construction du vecteur des registres non protégés
511  nonProtectedIdArray = 
512    determine_non_protected_registers(fsm,protect);
513   
514  bdd_vars = getbddvars(mddManager, nonProtectedIdArray);
515  res = inj_ms(mddManager, bdd_vars, S);
516  array_free(bdd_vars);
517  array_free(nonProtectedIdArray);
518  return res;
519}
520
521
522// modÚle de faute multiplicité spaciale et multiplicité temporelle
523// (S doit  désigner l'ensemble des états accessibles)
524mdd_t* error_states_ms_mt(Fsm_Fsm_t  *fsm, 
525                          mdd_t* S0,
526                          mdd_t* S,
527                          FILE* protect) {
528  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
529   array_t     *nonProtectedIdArray, *bdd_vars;
530  mdd_t       *res,*delta_reachB;
531
532  // construction du vecteur des registres non protégés
533   
534  mdd_t *tmp = fsm->reachabilityInfo.initialStates;
535  mdd_t *tmpReach = fsm->reachabilityInfo.reachableStates;
536
537  nonProtectedIdArray = 
538    determine_non_protected_registers(fsm,protect);
539   bdd_vars = getbddvars(mddManager, nonProtectedIdArray); 
540
541  fsm->reachabilityInfo.initialStates = 
542    error_states(fsm, S,nonProtectedIdArray);
543
544  delta_reachB = Fsm_FsmComputeReachableStates( fsm, 0,  0, 0, 0, 0,
545                                                0, 0, Fsm_Rch_Default_c, 
546                                                0, 1, NIL(array_t),
547                                                0, NIL(array_t));
548  mdd_free(fsm->reachabilityInfo.initialStates);
549
550  mdd_t* restmp = mdd_or(S0, delta_reachB, 1, 1);
551 
552  fsm->reachabilityInfo.initialStates=tmp;
553  fsm->reachabilityInfo.reachableStates = tmpReach;
554
555  res = inj_ms(mddManager, bdd_vars, restmp);
556
557  mdd_free(delta_reachB);
558  mdd_free(restmp);
559  array_free(bdd_vars);
560  array_free(nonProtectedIdArray);
561  return res;
562}
563
564
565// modÚle de faute unicité spaciale et multiplicité temporelle
566// (S doit  désigner l'ensemble des états accessibles)
567/* mdd_t* error_states_us_mt(Fsm_Fsm_t  *fsm,  */
568/*                        mdd_t* S, */
569/*                        FILE* protected) { */
570/*   mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); */
571/*   array_t     *nonProtectedIdArray, *bdd_vars; */
572/*   mdd_t       *res,*delta_reachB,*tmp, */
573/*               *prec=mdd_one(Fsm_FsmReadMddManager(fsm));; */
574
575/*   // construction du vecteur des registres non protégés */
576/*   nonProtectedIdArray =  */
577/*     determine_non_protected_registers(fsm,protected); */
578/*     bdd_vars = getbddvars(mddManager, nonProtectedIdArray);  */
579 
580/*   tmp = fsm->reachabilityInfo.initialStates; */
581
582/*   res = inj_us(mddManager, bdd_vars, S); */
583 
584/*   do{ */
585
586/*     mdd_t *e,*p,*next; */
587/*     mdd_free(prec);  */
588/*     prec = mdd_dup(res); */
589/*     e = mdd_dup(res); */
590   
591/*     // compute delta(e) */
592/*     mdd_t * fromLowerBound = mdd_dup(e); */
593/*     mdd_t * fromUpperBound = mdd_dup(e); */
594/*     mdd_t * toCareSet = mdd_one(Fsm_FsmReadMddManager(fsm)); */
595/*     // Compute set of next states */
596/*     // Computes the forward image of a set, under the function vector */
597/*     // in imageInfo */
598/*     e =  Img_ImageInfoComputeFwdWithDomainVars( fsm->imageInfo , */
599/*                                              fromLowerBound, */
600/*                                              fromUpperBound, */
601/*                                              toCareSet); */
602 
603         
604/*     // compute delta*(delta(e)) */
605/*     fsm->reachabilityInfo.initialStates = mdd_dup(e); */
606/*     mdd_free(fsm->reachabilityInfo.reachableStates); */
607/*     fsm->reachabilityInfo.reachableStates=NIL(mdd_t); */
608/*     e = mdd_dup(Fsm_FsmComputeReachableStates(fsm, 0,  0, 0, 0, 0, */
609/*                                            0, 0, Fsm_Rch_Default_c,  */
610/*                                            0, 0, NIL(array_t), */
611/*                                            0, NIL(array_t))); */
612   
613   
614/*     // res = res \vee inj_us(\delta*(delta(e)))  */
615/*     // fault injection only for the set of next states */
616/*     mdd_t *tmp1, */
617/*     *e_inj= inj_us(mddManager, bdd_vars, e); */
618/*     tmp1=mdd_or(res,e_inj , 1, 1); */
619/*     mdd_free(e_inj); */
620/*     mdd_free(res); */
621/*     res=tmp1; */
622
623/*    }while(!mdd_equal(res, prec)); */
624   
625/*   fsm->reachabilityInfo.initialStates=tmp; */
626/*   array_free(bdd_vars); */
627/*   array_free(nonProtectedIdArray); */
628/*   return res; */
629/* } */
630
631
632mdd_t* error_states_us_mt(Fsm_Fsm_t  *fsm, 
633                          mdd_t *S,
634                          FILE *protect) {
635
636  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
637 
638  // construction du vecteur des registres non prot?g?s
639  array_t *nonProtectedIdArray = determine_non_protected_registers(fsm, protect);
640  array_t *bdd_vars = getbddvars(mddManager, nonProtectedIdArray); 
641  // sauvegarde des ?tats initiaux et accessibles courants
642  mdd_t *tmpInit = fsm->reachabilityInfo.initialStates;
643  mdd_t *tmpReach = mdd_dup(fsm->reachabilityInfo.reachableStates);
644  // initialisation du r?sultat ? inj_us(S)
645  mdd_t *res = inj_us(mddManager, bdd_vars, S);
646
647  mdd_t *prec = mdd_one(mddManager);
648  mdd_t *toCareSet = mdd_one(mddManager);
649
650  do {
651    mdd_free(prec); 
652    prec = mdd_dup(res);
653    // compute e = delta(res)
654    mdd_t *e = Img_ImageInfoComputeFwdWithDomainVars( fsm->imageInfo ,
655                                               res,
656                                               res,
657                                               toCareSet);
658    // compute e = delta*(e)
659    fsm->reachabilityInfo.initialStates = mdd_dup(e);
660    mdd_free(fsm->reachabilityInfo.reachableStates);
661    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
662    mdd_free(e);
663    e = mdd_dup(Fsm_FsmComputeReachableStates(fsm, 0,  0, 0, 0, 0,
664                                              0, 0, Fsm_Rch_Default_c, 
665                                              0, 0, NIL(array_t),
666                                              0, NIL(array_t)));
667    // compute res = res | inj_us(e)
668    mdd_t *e_inj = inj_us(mddManager, bdd_vars, e);
669    mdd_free(e);
670    e = mdd_or(res, e_inj , 1, 1);
671    mdd_free(res);
672    mdd_free(e_inj);
673    res = e;
674  } while(!mdd_equal(res, prec));
675 
676  mdd_free(prec);
677  mdd_free(fsm->reachabilityInfo.reachableStates);
678  fsm->reachabilityInfo.reachableStates=tmpReach;
679  fsm->reachabilityInfo.initialStates=tmpInit;
680  array_free(bdd_vars);
681  array_free(nonProtectedIdArray);
682  return res;
683}
684
685
686
687
688
689void print_variables_info(Fsm_Fsm_t  *fsm) {
690  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
691  array_t     *psVarsArray;
692  int         i, arrSize, mddId;
693  mvar_type   mVar;
694
695  psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
696  arrSize = array_n( psVarsArray );
697
698  for ( i = 0 ; i < arrSize ; i++ ) {
699    mddId = array_fetch( int, psVarsArray, i );
700    mVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager),mddId);
701    (void) fprintf(vis_stdout, "%-20s%10d\n", mVar.name, mVar.values);
702  }
703}
704
705mdd_t* evaluate_EF(Fsm_Fsm_t  *fsm, mdd_t *target,
706                   mdd_t* fairS, int verbosityLevel) {
707  mdd_t *res;
708  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
709  array_t *careStatesArray = array_alloc(mdd_t *, 0);
710  array_insert_last(mdd_t *, careStatesArray, mddOne);
711 
712  res = Mc_FsmEvaluateEUFormula(
713            fsm,                     // Fsm_Fsm_t *fsm,
714            mddOne,                  // mdd_t *invariant,
715            target,                  // mdd_t *target,
716            NIL(mdd_t),              // mdd_t *underapprox,
717            fairS,                   // mdd_t *fairStates,
718            careStatesArray,         // array_t *careStatesArray,
719            MC_NO_EARLY_TERMINATION, // Mc_EarlyTermination_t *earlyTermination,
720            NIL(array_t),            // Fsm_HintsArray_t *hintsArray,
721            Mc_None_c,               // Mc_GuidedSearch_t hintType,
722            NIL(array_t),            // array_t *onionRings,
723            verbosityLevel,          // Mc_VerbosityLevel verbosity,
724            McDcLevelNone_c,         // Mc_DcLevel dcLevel,
725            NIL(boolean) );          // boolean *fixpoint)
726           
727  array_free(careStatesArray);
728  mdd_free(mddOne);
729  return res;
730}
731
732
733mdd_t* evaluate_EG(Fsm_Fsm_t  *fsm, mdd_t *invariant,
734                   mdd_t* fairS,Fsm_Fairness_t * fairCond, 
735                   int verbosityLevel) {
736  mdd_t *res;
737  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
738  array_t *careStatesArray = array_alloc(mdd_t *, 0);
739  array_insert_last(mdd_t *, careStatesArray, mddOne);
740
741  res = Mc_FsmEvaluateEGFormula(
742           fsm,                       // Fsm_Fsm_t *fsm,
743           invariant,                 // mdd_t *invariant,notforbiden
744           NIL(mdd_t),                // mdd_t *overapprox,
745           fairS,                     // mdd_t *fairStates,
746           fairCond,                  // Fsm_Fairness_t *modelFairness,
747           careStatesArray,           // array_t *careStatesArray,
748           MC_NO_EARLY_TERMINATION,   // Mc_EarlyTermination_t *earlyTermination,
749           NIL(array_t),              // Fsm_HintsArray_t *hintsArray,
750           Mc_None_c,                 // Mc_GuidedSearch_t hintType,
751           NIL(array_t*),             // array_t **pOnionRingsArrayForDbg,
752           verbosityLevel,            // Mc_VerbosityLevel verbosity,
753           McDcLevelNone_c,           // Mc_DcLevel dcLevel,
754           NIL(boolean),              // boolean *fixpoint,
755           McGSH_old_c 
756           //    McGSH_Unassigned_c         // Mc_GSHScheduleType GSHschedule)
757                                );
758  array_free(careStatesArray);
759  mdd_free(mddOne);
760  return res;
761
762}
763
764mdd_t* evaluate(Fsm_Fsm_t  *fsm,FILE* ctlfile,mdd_t* fairS,
765                Fsm_Fairness_t * fairCond, int verbosityLevel) {
766  int i;
767  mdd_t *res;
768  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
769  array_t *careStatesArray = array_alloc(mdd_t *, 0);
770  array_insert_last(mdd_t *, careStatesArray, mddOne);
771
772  array_t * formula=Ctlp_FileParseFormulaArray(ctlfile);
773  array_t * ctlNormalFormulaArray=
774    Ctlp_FormulaArrayConvertToExistentialFormTree(formula);
775
776  Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
777                                           ctlNormalFormulaArray, 0);
778  res= Mc_FsmEvaluateFormula(fsm, 
779                             ctlFormula, 
780                             fairS, 
781                             fairCond,
782                             careStatesArray, 
783                             MC_NO_EARLY_TERMINATION , 
784                             NIL(array_t), 
785                             Mc_None_c, 
786                             verbosityLevel,
787                             McDcLevelNone_c, 
788                             0, 
789// McGSH_Unassigned_c         // Mc_GSHScheduleType GSHschedule)
790                             McGSH_old_c);
791 
792  CtlpFormulaFree(ctlFormula); 
793  free(ctlNormalFormulaArray);
794  free(formula);
795  // Ctlp_FormulaArrayFree(ctlNormalFormulaArray);
796  // Ctlp_FormulaArrayFree(formula);
797 
798  array_free(careStatesArray);
799  mdd_free(mddOne);
800  return res;
801}
802
803mdd_t* evaluate_EU(Fsm_Fsm_t  *fsm, mdd_t* inv, 
804                   mdd_t *target,mdd_t* fairS, 
805                   int verbosityLevel) {
806  mdd_t *res;
807  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
808  array_t *careStatesArray = array_alloc(mdd_t *, 0);
809  array_insert_last(mdd_t *, careStatesArray, mddOne);
810
811  res = Mc_FsmEvaluateEUFormula(
812    fsm,                     // Fsm_Fsm_t *fsm,
813    inv,                     // mdd_t *invariant,
814    target,                  // mdd_t *target,
815    NIL(mdd_t),              // mdd_t *underapprox,
816    fairS,                  // mdd_t *fairStates,
817    careStatesArray,         // array_t *careStatesArray,
818    MC_NO_EARLY_TERMINATION, // Mc_EarlyTermination_t *earlyTermination,
819    NIL(array_t),            // Fsm_HintsArray_t *hintsArray,
820    Mc_None_c,               // Mc_GuidedSearch_t hintType,
821    NIL(array_t),            // array_t *onionRings,
822    verbosityLevel,          // Mc_VerbosityLevel verbosity,
823    McDcLevelNone_c,         // Mc_DcLevel dcLevel,
824    NIL(boolean)             // boolean *fixpoint)
825  );
826  array_free(careStatesArray);
827  mdd_free(mddOne);
828  return res;
829}
830
831mdd_t* evaluate_AU(Fsm_Fsm_t  *fsm, mdd_t* inv, 
832                   mdd_t *target, mdd_t* fairS,
833                   Fsm_Fairness_t * fairCond, 
834                   int verbosityLevel) {
835 
836
837  /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
838  mdd_t* not_f = mdd_not(inv);
839  mdd_t* not_g = mdd_not(target);
840  mdd_t* not_g_and_not_f = mdd_and(not_f, not_g, 1, 1);
841  mdd_t* eg_not_g = 
842    evaluate_EG(fsm, not_g, fairS, fairCond, verbosityLevel);
843  mdd_t* e_not_g_U_not_g_and_not_f = 
844    evaluate_EU(fsm, not_g, not_g_and_not_f, fairS, verbosityLevel); 
845  mdd_t* or = mdd_or(e_not_g_U_not_g_and_not_f, eg_not_g, 1, 1);
846  mdd_t* res = mdd_not(or);
847 
848  mdd_free(not_f);
849  mdd_free(not_g);
850  mdd_free(not_g_and_not_f);
851  mdd_free(eg_not_g);
852  mdd_free(e_not_g_U_not_g_and_not_f);
853  mdd_free(or);
854  return res;
855}
856
857
858
859void
860compute_fair(Fsm_Fsm_t  *fsm,int  verbosityLevel){
861  long        initialTime;
862  long        finalTime;
863  EpDouble   *error    = EpdAlloc();
864  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
865  array_t *careStatesArray = array_alloc(mdd_t *, 0);
866  array_insert(mdd_t *, careStatesArray, 0, mddOne);
867  mdd_t      *res,*fairS;
868  mdd_t* tmpfair = Fsm_FsmComputeFairStates(fsm,
869                                            careStatesArray,
870                                            verbosityLevel, 
871                                            McDcLevelNone_c,
872                                            McGSH_Unassigned_c ,
873                                            McBwd_c, FALSE );
874
875  res=mdd_and(fsm->reachabilityInfo.initialStates,  tmpfair, 1, 1);
876       
877  if(verbosityLevel){
878    (void) fprintf(vis_stdout,"********************************\n");
879    print_number_of_states("Fair error states                              = ", fsm, res);
880  }
881  mdd_free(tmpfair);
882 
883  if (!mdd_lequal(fsm->reachabilityInfo.initialStates, res, 1, 1)) {
884   
885    (void) fprintf(vis_stdout, 
886                   "WARNING : some error states are not fair\n");
887    (void) fprintf(vis_stdout, 
888                   "WARNING : only fair error states will be taken into account\n");
889
890    // attention, il faut prendre en compte le cas ou aucun 'error state' n'est fa ir
891    mdd_free(fsm->reachabilityInfo.initialStates);
892    fsm->reachabilityInfo.initialStates = res;
893     // mise à jour des états accessibles
894    mdd_free(fsm->reachabilityInfo.reachableStates);
895    (void)Fsm_FsmComputeReachableStates(fsm,0,0,
896                                        0,0, 0,
897                                        0, 0, Fsm_Rch_Default_c,
898                                        0,0, NIL(array_t),
899                                        0,  NIL(array_t));
900      finalTime = util_cpu_time();
901   
902    (void) fprintf(vis_stdout,"********************************\n");
903    print_number_of_states("States reachable from fair error states        = ", fsm, 
904                           fsm->reachabilityInfo.reachableStates);
905  }
906  else
907    mdd_free(res);
908 
909  array_free(careStatesArray);
910  mdd_free(mddOne);
911
912}
913
914
915mdd_t* 
916getForbidden(Fsm_Fsm_t  *fsm){
917
918  assert(fsm != NIL(Fsm_Fsm_t));
919 
920  if (fsm->RobSets.Forb == NIL(mdd_t))
921    fsm->RobSets.Forb=
922      mdd_zero(Fsm_FsmReadMddManager(fsm));
923
924  return mdd_dup(fsm->RobSets.Forb);
925}
926
927mdd_t* 
928getRequired(Fsm_Fsm_t  *fsm){
929 
930  assert(fsm != NIL(Fsm_Fsm_t));
931 
932  if (fsm->RobSets.Req == NIL(mdd_t))
933    fsm->RobSets.Req=
934      mdd_one(Fsm_FsmReadMddManager(fsm));
935
936  return mdd_dup(fsm->RobSets.Req);
937}
938
939
940mdd_t* 
941getSafe( Fsm_Fsm_t  *fsm ){
942 
943  assert(fsm != NIL(Fsm_Fsm_t));
944 
945  if (fsm->RobSets.Safe == NIL(mdd_t)){
946    mdd_t* inits=fsm->reachabilityInfo.initialStates;
947    mdd_t* reachs=fsm->reachabilityInfo.reachableStates;
948    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
949    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
950
951    (void)Fsm_FsmComputeInitialStates(fsm);
952    (void)Fsm_FsmComputeReachableStates(fsm,0,0,
953                                        0,0, 0,
954                                        0, 0, Fsm_Rch_Default_c,
955                                        0,0, NIL(array_t),
956                                        0,  NIL(array_t));
957    fsm->RobSets.Safe=
958      mdd_dup(fsm->reachabilityInfo.reachableStates);
959
960    mdd_free(fsm->reachabilityInfo.initialStates);
961    mdd_free(fsm->reachabilityInfo.reachableStates);
962    fsm->reachabilityInfo.initialStates=inits;
963    fsm->reachabilityInfo.reachableStates=reachs;
964  }
965
966  return mdd_dup(fsm->RobSets.Safe); 
967
968}
969
970mdd_t* 
971getInitial(Fsm_Fsm_t  *fsm) {
972
973  assert(fsm != NIL(Fsm_Fsm_t));
974
975  if (fsm->reachabilityInfo.initialStates != NIL(mdd_t))
976    return mdd_dup(fsm->reachabilityInfo.initialStates); 
977 
978  if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){
979    mdd_free(fsm->reachabilityInfo.reachableStates);
980    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
981  }
982  (void)Fsm_FsmComputeInitialStates(fsm);
983  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
984                                      0,0, 0,
985                                      0, 0, Fsm_Rch_Default_c,
986                                      0,0, NIL(array_t),
987                                      0,  NIL(array_t));
988
989  return mdd_dup(fsm->reachabilityInfo.initialStates);
990}
991
992mdd_t* 
993getReachOrg( Fsm_Fsm_t  *fsm ){
994 
995  assert(fsm != NIL(Fsm_Fsm_t));
996 
997  if (fsm->RobSets.originalreachableStates == 
998      NIL(mdd_t)){
999    mdd_t* inits=fsm->reachabilityInfo.initialStates;
1000    mdd_t* reachs=fsm->reachabilityInfo.reachableStates;
1001    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
1002    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
1003
1004    (void)Fsm_FsmComputeInitialStates(fsm);
1005    (void)Fsm_FsmComputeReachableStates(fsm,0,0,
1006                                        0,0, 0,
1007                                        0, 0, Fsm_Rch_Default_c,
1008                                        0,0, NIL(array_t),
1009                                        0,  NIL(array_t));
1010    fsm->RobSets.originalreachableStates=
1011      mdd_dup(fsm->reachabilityInfo.reachableStates);
1012
1013    mdd_free(fsm->reachabilityInfo.initialStates);
1014    mdd_free(fsm->reachabilityInfo.reachableStates);
1015    fsm->reachabilityInfo.initialStates=inits;
1016    fsm->reachabilityInfo.reachableStates=reachs;
1017  }
1018
1019  return mdd_dup(fsm->RobSets.originalreachableStates); 
1020
1021}
1022
1023mdd_t* 
1024getReach(Fsm_Fsm_t  *fsm) {
1025
1026  assert(fsm != NIL(Fsm_Fsm_t));
1027
1028  if (fsm->reachabilityInfo.reachableStates != NIL(mdd_t))
1029    return mdd_dup(fsm->reachabilityInfo.reachableStates); 
1030 
1031  if (fsm->reachabilityInfo.initialStates == NIL(mdd_t)) {
1032    (void)Fsm_FsmComputeInitialStates(fsm);
1033  }
1034 
1035  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
1036                                      0,0, 0,
1037                                      0, 0, Fsm_Rch_Default_c,
1038                                      0,0, NIL(array_t),
1039                                      0,  NIL(array_t));
1040
1041  return mdd_dup(fsm->reachabilityInfo.reachableStates);
1042}
1043
1044
1045
1046mdd_t* 
1047evaluate_Formula_AF_AF (Fsm_Fsm_t  *fsm,
1048                        mdd_t* Req,mdd_t* forb,mdd_t* Safe,
1049                        int  verbosityLevel ){
1050 
1051  mdd_t      *notforbiden=mdd_not(forb);;
1052  mdd_t      *XU_notForb_And_Safe;
1053  mdd_t      *Req_And_XU_notForb_And_Safe;
1054  mdd_t      *Setformula;
1055
1056  XU_notForb_And_Safe = 
1057    evaluate_AU(fsm, notforbiden,Safe, 
1058                fsm->fairnessInfo.states, 
1059                fsm->fairnessInfo.constraint, 
1060                verbosityLevel);                                         
1061  Req_And_XU_notForb_And_Safe = 
1062    mdd_and(Req, XU_notForb_And_Safe, 1, 1); 
1063  mdd_free(XU_notForb_And_Safe); 
1064  Setformula=evaluate_AU(fsm, notforbiden, 
1065                         Req_And_XU_notForb_And_Safe, 
1066                         fsm->fairnessInfo.states, 
1067                         fsm->fairnessInfo.constraint, 
1068                         verbosityLevel);                                   
1069  mdd_free(Req_And_XU_notForb_And_Safe);
1070  mdd_free(notforbiden);
1071  return Setformula;
1072   
1073}
1074
1075mdd_t* 
1076evaluate_Formula_EF_AF (Fsm_Fsm_t  *fsm,
1077                        mdd_t* Req,mdd_t* forb,
1078                        mdd_t* Safe,
1079                        int  verbosityLevel ){
1080
1081  mdd_t      *notforbiden=mdd_not(forb);;
1082  mdd_t      *XU_notForb_And_Safe;
1083  mdd_t      *Req_And_XU_notForb_And_Safe;
1084  mdd_t      *Setformula;
1085  XU_notForb_And_Safe = 
1086    evaluate_AU(fsm, notforbiden, Safe, 
1087                fsm->fairnessInfo.states, 
1088                fsm->fairnessInfo.constraint, 
1089                verbosityLevel);   
1090  Req_And_XU_notForb_And_Safe =
1091    mdd_and(Req,XU_notForb_And_Safe,1,1); 
1092  mdd_free( XU_notForb_And_Safe); 
1093  Setformula=evaluate_EU(fsm, notforbiden, 
1094                         Req_And_XU_notForb_And_Safe, 
1095                         fsm->fairnessInfo.states, 
1096                         verbosityLevel); 
1097  mdd_free(Req_And_XU_notForb_And_Safe); 
1098  mdd_free(notforbiden);
1099  return Setformula;
1100   
1101}
1102 
1103
1104mdd_t* 
1105evaluate_Formula_AF_EF (Fsm_Fsm_t  *fsm,
1106                        mdd_t* Req,mdd_t* forb,mdd_t* Safe,
1107                        int  verbosityLevel ){
1108
1109  mdd_t      *notforbiden=mdd_not(forb);;
1110  mdd_t      *XU_notForb_And_Safe;
1111  mdd_t      *Req_And_XU_notForb_And_Safe;
1112  mdd_t      *Setformula;
1113
1114  XU_notForb_And_Safe = evaluate_EU(fsm, notforbiden, Safe, 
1115                                    fsm->fairnessInfo.states, 
1116                                    verbosityLevel); 
1117  Req_And_XU_notForb_And_Safe = mdd_and(Req,XU_notForb_And_Safe,1,1); 
1118  mdd_free( XU_notForb_And_Safe); 
1119  Setformula=evaluate_AU(fsm, notforbiden, 
1120                         Req_And_XU_notForb_And_Safe, 
1121                         fsm->fairnessInfo.states,
1122                         fsm->fairnessInfo.constraint, 
1123                         verbosityLevel); 
1124   mdd_free(Req_And_XU_notForb_And_Safe); 
1125   mdd_free(notforbiden);
1126  return Setformula;
1127 
1128}
1129
1130mdd_t* 
1131evaluate_Formula_EF_EF (Fsm_Fsm_t  *fsm,
1132                        mdd_t* Req,mdd_t* forb,mdd_t* Safe,
1133                        int  verbosityLevel ){
1134  mdd_t      *notforbiden=mdd_not(forb);;
1135  mdd_t      *XU_notForb_And_Safe;
1136  mdd_t      *Req_And_XU_notForb_And_Safe;
1137  mdd_t      *Setformula;
1138
1139  XU_notForb_And_Safe = evaluate_EU(fsm, notforbiden,Safe, 
1140                                    fsm->fairnessInfo.states, 
1141                                    verbosityLevel);   
1142  Req_And_XU_notForb_And_Safe =mdd_and(Req,XU_notForb_And_Safe,1,1); 
1143  mdd_free( XU_notForb_And_Safe);   
1144  Setformula=evaluate_EU(fsm, notforbiden, 
1145                         Req_And_XU_notForb_And_Safe, 
1146                         fsm->fairnessInfo.states, verbosityLevel);   
1147 
1148  mdd_free(Req_And_XU_notForb_And_Safe); 
1149  mdd_free(notforbiden);
1150  return Setformula;
1151}
1152
1153void
1154mdd_FunctionPrint(mdd_manager *mgr ,
1155                  mdd_t *  top, 
1156                  FILE  * f) {
1157  mdd_t * T;
1158  mdd_t * E;
1159  int    id;
1160  char    c=' ';
1161 
1162  static int level;
1163
1164  level++;
1165
1166  id = bdd_top_var_id(top);
1167
1168  mvar_type mv = 
1169    mymddGetVarById(mgr,id);
1170
1171  fprintf(f,"(");
1172
1173  // Pour le Then
1174  T=bdd_then(top);
1175 
1176  if(bdd_is_tautology(T,1)){
1177    fprintf(f,"%s = 1 ",mv.name);
1178    c = '+';
1179  } else
1180    if(!bdd_is_tautology(T,0)){
1181      fprintf(f,"%s = 1 * ",mv.name);
1182      mdd_FunctionPrint(mgr, T,f);
1183      c = '+';
1184    }
1185
1186  mdd_free(T);
1187 
1188  //pour le Else
1189  E=bdd_else(top);
1190  if(bdd_is_tautology(E,0)){
1191    goto fin;
1192  }
1193 
1194  if(bdd_is_tautology(E,1)){
1195    fprintf(f,"%c %s = 0",c, mv.name);
1196    goto fin;
1197  }
1198 
1199  fprintf(f,"%c %s = 0 * ",c, mv.name);
1200  mdd_FunctionPrint(mgr, E,f);
1201  mdd_free(E);
1202
1203 fin:
1204  fprintf(f,")");
1205  level--;
1206  return;
1207}
1208
1209void
1210mdd_FunctionPrintMain(mdd_manager *mgr ,
1211                      mdd_t *  top, 
1212                      char * macro_name,
1213                      FILE * f){
1214 
1215  if(bdd_is_tautology(top,0)){
1216    fprintf(f,"\\define %s (FALSE)\n",
1217            macro_name);
1218    return;
1219  }
1220 
1221  if(bdd_is_tautology(top,1)){
1222    fprintf(f,"\\define %s (TRUE)\n",
1223            macro_name);
1224    return;
1225  }
1226 
1227  fprintf(f,"\\define %s ", 
1228          macro_name);
1229  mdd_FunctionPrint(mgr,top,f);
1230  fprintf(f,"\n");
1231  return;
1232
1233} 
1234
1235void
1236callBmcRob( Ntk_Network_t   *network,
1237            Ctlsp_Formula_t *ltlFormula,
1238            array_t         *constraintArray,
1239            BmcOption_t     *options) {
1240 
1241  Ctlsp_Formula_t *negLtlFormula = 
1242    Ctlsp_LtllFormulaNegate(ltlFormula);
1243  st_table        *CoiTable      = //NIL(st_table);
1244   st_init_table(st_ptrcmp, st_ptrhash);
1245
1246  assert(ltlFormula != NIL(Ctlsp_Formula_t));
1247  assert(network != NIL(Ntk_Network_t));
1248 
1249 
1250 // Print out the given LTL formula
1251 if (options->verbosityLevel >= BmcVerbosityMax_c){
1252  fprintf(vis_stdout, "Formula: ");
1253  Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
1254  fprintf(vis_stdout, "\n");
1255    fprintf(vis_stdout, "Negated formula: ");
1256    Ctlsp_FormulaPrint(vis_stdout, negLtlFormula);
1257    fprintf(vis_stdout, "\n");
1258  }
1259
1260 
1261 // Compute the cone of influence of the LTL formula
1262 //  BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable);
1263 
1264 // CoiTable= (st_table *) Ntk_NetworkReadApplInfo(network,
1265 //                                    MVFAIG_NETWORK_APPL_KEY);
1266 
1267  Ntk_Node_t *node;
1268  lsGen gen;
1269  Ntk_NetworkForEachLatch(network, gen, node){
1270     st_insert(CoiTable, (char *) node, (char *) 0);
1271  }
1272
1273  if(options->clauses == 2){
1274    BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
1275                           constraintArray, options);
1276  }
1277  else {
1278     if(options->encoding == 0)
1279       BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
1280                                    CoiTable,
1281                                    constraintArray, options, 0);
1282     else 
1283       if(options->encoding == 1)
1284         BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
1285                                      CoiTable,
1286                                      constraintArray, options, 1);
1287       else 
1288         if(options->encoding == 2)
1289           BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
1290                                                CoiTable,
1291                                                constraintArray, options);
1292         
1293  }
1294 
1295
1296  st_free_table(CoiTable);
1297  Ctlsp_FormulaFree(negLtlFormula);
1298} 
1299
1300/*
1301void
1302callBmcRob( Ntk_Network_t   *network,
1303            Ctlsp_Formula_t *ltlFormula,
1304            array_t         *constraintArray,
1305            BmcOption_t     *options) {
1306 
1307  Ctlsp_Formula_t *negLtlFormula =
1308    Ctlsp_LtllFormulaNegate(ltlFormula);
1309  st_table        *CoiTable      = 
1310    st_init_table(st_ptrcmp, st_ptrhash);
1311
1312  assert(ltlFormula != NIL(Ctlsp_Formula_t));
1313  assert(network != NIL(Ntk_Network_t));
1314 
1315 
1316 // Print out the given LTL formula
1317  if (options->verbosityLevel >= BmcVerbosityMax_c){
1318    fprintf(vis_stdout, "Formula: ");
1319    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
1320    fprintf(vis_stdout, "\n");
1321    fprintf(vis_stdout, "Negated formula: ");
1322    Ctlsp_FormulaPrint(vis_stdout, negLtlFormula);
1323    fprintf(vis_stdout, "\n");
1324  }
1325
1326  // CoiTable= (st_table *) Ntk_NetworkReadApplInfo(network,
1327  //                                             MVFAIG_NETWORK_APPL_KEY);
1328  BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable);
1329  BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
1330                         constraintArray, options);
1331
1332  st_free_table(CoiTable);
1333  Ctlsp_FormulaFree(negLtlFormula);
1334}
1335*/
1336/*
1337bAigEdge_t
1338sat_Add_Blocking_Clauses(mAig_Manager_t *manager ,
1339                         char* filename){
1340  FILE *fin;
1341  char line[102400],
1342       word[1024];
1343  char *lp;
1344  int v,v1;
1345  int i, size, index, value,lvalue,k=0;
1346  bAigEdge_t *tv,j,result=mAig_One;
1347  FILE *blfile;
1348  bAigTimeFrame_t *timeframe=
1349        manager->timeframeWOI;
1350  int bound = timeframe->currentTimeframe;
1351
1352 
1353  if(!(fin = fopen(filename, "r"))) {
1354    fprintf(vis_stdout,
1355            "ERROR : Can't open file %s\n",
1356            filename);
1357    exit(0);
1358  }
1359
1360 
1361  for (k=0 ; k<bound; ++k){
1362    while(fgets(line, 102400, fin)) {
1363      lp = sat_RemoveSpace(line);
1364     
1365      if(lp[0] == '\n') continue;
1366   
1367      while(1) {
1368        lp = sat_RemoveSpace(lp);
1369        lp = sat_CopyWord(lp, word);
1370     
1371        if(strlen(word)) {
1372       
1373          v= atoi(word);
1374          j= (v < 0) ? -v : v;
1375               
1376          if(!st_lookup_int(timeframe->li2index,
1377                            (char *)j, &index))
1378            continue ;
1379         
1380          j = timeframe->latchInputs[k][index];
1381         
1382          if(j == bAig_One) {
1383            result = mAig_And(manager, result,
1384                              bAig_GetCanonical(manager, j));
1385          }
1386          else
1387            if (j != bAig_Zero) {
1388              tv = sat_GetCanonical(manager, j);
1389              lvalue = bAig_GetValueOfNode(manager, tv);
1390              if(lvalue == 1)
1391                result = mAig_And(manager, result,
1392                                  bAig_GetCanonical(manager, j));
1393            }         
1394        }
1395        else {
1396          break;
1397        }
1398      }
1399    }
1400   
1401    rewind(fin);
1402  }
1403 
1404 fclose(fin);
1405 return  result;
1406}
1407*/
1408bAigEdge_t
1409sat_Add_Blocking_Clauses( Ntk_Network_t   *network,
1410                          st_table        *nodeToMvfAigTable,
1411                          st_table        *coiTable ){
1412
1413  mAig_Manager_t    *manager = 
1414    Ntk_NetworkReadMAigManager(network);
1415  bAigTimeFrame_t *timeframe= 
1416    manager->timeframeWOI;
1417  int bound = 
1418    timeframe->currentTimeframe;
1419  Ntk_Node_t *node;
1420  int tmp,k,i,j,index;
1421  array_t * latchArr = array_alloc(Ntk_Node_t *, 0);
1422  MvfAig_Function_t  *mvfAig;
1423  bAigEdge_t *tv,v,result=mAig_One;
1424  lsGen gen;
1425  int lvalue;
1426
1427  Ntk_NetworkForEachLatch(network, gen, node){
1428    if (st_lookup_int(coiTable, (char *) node, &tmp)){
1429      array_insert_last(Ntk_Node_t *, latchArr, node);
1430    }
1431  }
1432 
1433  for (k=0 ; k<bound; ++k){
1434    for(i=0; i<array_n( latchArr); i++) {
1435
1436      node = array_fetch(Ntk_Node_t *, latchArr, i);
1437      mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
1438
1439      if(mvfAig == 0)   continue;
1440     
1441      for (j=0; j< array_n(mvfAig); j++) {
1442        v =  MvfAig_FunctionReadComponent(mvfAig, j);
1443                 
1444        if(!st_lookup_int(timeframe->li2index, 
1445                          (char *)v, &index)) 
1446          continue;
1447
1448        v = timeframe->latchInputs[k][index];
1449
1450        if(v == bAig_One)       {
1451          result = mAig_And(manager, result, 
1452                            bAig_GetCanonical(manager, v));
1453          break;
1454        }
1455
1456        if(v != bAig_Zero) {
1457          tv = bAig_GetCanonical(manager, v);
1458          lvalue = bAig_GetValueOfNode(manager, tv);
1459         
1460          if(lvalue == 1){     
1461            result = mAig_And(manager, result,
1462                              bAig_GetCanonical(manager, v));
1463            break;
1464          }
1465        }
1466      }
1467    }
1468  }
1469
1470  array_free(latchArr);
1471  return  result;
1472}
1473/*
1474mdd_t *
1475find_removed_latchs( Ntk_Network_t   *network,
1476                     st_table        *nodeToMvfAigTable,
1477                     st_table        *coiTable,
1478                     st_table        *hashTable,
1479                     mdd_manager     *mgr,
1480                     int             *V ){
1481
1482  mAig_Manager_t    *manager =
1483    Ntk_NetworkReadMAigManager(network);
1484  bAigTimeFrame_t *timeframe=
1485    manager->timeframeWOI;
1486  int bound =
1487    timeframe->currentTimeframe;
1488  Ntk_Node_t *node;
1489  int tmp,k,i,j,index,lvalue;
1490  array_t * latchArr = array_alloc(Ntk_Node_t *, 0);
1491  MvfAig_Function_t  *mvfAig;
1492  bAigEdge_t *tv,v,result=mAig_One;
1493  lsGen gen;
1494  mdd_t* one = mdd_one(mgr);
1495  mdd_t* zero =  mdd_zero(mgr);
1496  mdd_t* R=mdd_one(mgr);
1497  int found,t;
1498
1499  Ntk_NetworkForEachLatch(network, gen, node){
1500    if (st_lookup_int(coiTable, (char *) node, &tmp)){
1501      array_insert_last(Ntk_Node_t *, latchArr, node);
1502    }
1503  }
1504  for (k=0 ; k<bound; ++k){
1505    for(i=0; i<array_n( latchArr); i++) {
1506      found =0;
1507      node = array_fetch(Ntk_Node_t *, latchArr, i);
1508      mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
1509   
1510      if(mvfAig == 0)   continue;
1511     
1512      for (j=0; j< array_n(mvfAig); j++) {
1513        v =  MvfAig_FunctionReadComponent(mvfAig, j);
1514   
1515        if(!st_lookup_int(timeframe->li2index,
1516                          (char *)v, &index))
1517          continue;
1518       
1519        t = timeframe->latchInputs[k][index];
1520   
1521        if(!st_lookup_int(hashTable,(char *)t, &index))
1522          continue;
1523        else
1524          found=1;
1525      }
1526     
1527      if (!found){
1528        st_insert(hashTable, (char*)t,(char*) (*V)+1);(*V)++;
1529        mdd_t* value=bdd_construct_bdd_t(mgr,Cudd_IndicesToCube(mgr,V,1));
1530        mdd_t* tmp=R;
1531        R=mdd_and(R,value,1,1);
1532        mdd_free(value);
1533        mdd_free(tmp);
1534      }
1535       
1536    }
1537
1538  array_free(latchArr);
1539
1540  if(mdd_equal(R,one)){
1541    mdd_free(R);
1542    R=mdd_zero(mgr);
1543  }
1544
1545  mdd_free(one);
1546  mdd_free(zero); 
1547  return R; 
1548}
1549
1550*/
1551void
1552sat_Add_Blocking_Clauses_2(Ntk_Network_t   *network,
1553                           st_table        *nodeToMvfAigTable,
1554                           st_table        *coiTable,
1555                           FILE* cnffile
1556                           ){
1557
1558  mAig_Manager_t    *manager = 
1559    Ntk_NetworkReadMAigManager(network);
1560  bAigTimeFrame_t *timeframe= 
1561    manager->timeframeWOI;
1562  int bound = 
1563    timeframe->currentTimeframe;
1564  Ntk_Node_t *node;
1565  int tmp,k,i,j,index;
1566  array_t * latchArr = array_alloc(Ntk_Node_t *, 0);
1567  MvfAig_Function_t  *mvfAig;
1568  bAigEdge_t *tv,v,result=mAig_One;
1569  lsGen gen;
1570  int lvalue;
1571
1572  Ntk_NetworkForEachLatch(network, gen, node){
1573    if (st_lookup_int(coiTable, (char *) node, &tmp)){
1574      array_insert_last(Ntk_Node_t *, latchArr, node);
1575    }
1576  }
1577 
1578  for (k=0 ; k<bound; ++k){
1579    for(i=0; i<array_n( latchArr); i++) {
1580
1581      node = array_fetch(Ntk_Node_t *, latchArr, i);
1582      mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
1583
1584      if(mvfAig == 0)   continue;
1585     
1586      for (j=0; j< array_n(mvfAig); j++) {
1587        v =  MvfAig_FunctionReadComponent(mvfAig, j);
1588                 
1589        if(!st_lookup_int(timeframe->li2index, 
1590                          (char *)v, &index)) 
1591          continue;
1592
1593        v = timeframe->latchInputs[k][index];
1594
1595        if(v == bAig_One)       {
1596          result = mAig_And(manager, result, 
1597                            bAig_GetCanonical(manager, v));
1598          break;
1599        }
1600
1601        if(v != bAig_Zero) {
1602          tv = bAig_GetCanonical(manager, v);
1603          lvalue = bAig_GetValueOfNode(manager, tv);
1604         
1605          if(lvalue == 1){     
1606            result = mAig_And(manager, result,
1607                              bAig_GetCanonical(manager, v));
1608            break;
1609          }
1610        }
1611      }
1612    }
1613  }
1614
1615  array_free(latchArr);
1616
1617}
1618
1619
1620
1621
1622
1623
1624/**Function********************************************************************
1625 *  Synopsis    [Build a new model based on the current Hierarchy]
1626
1627  Description [Build a new hierarchy named ROB3.
1628  Composition of two instances (golden and faulty) of the current hierarchy.
1629  The inputs are the same as before.
1630  The outputs are doubled.
1631  Return the new created node.
1632  ]
1633
1634  SideEffects []
1635******************************************************************************/
1636Hrc_Node_t  * build_golden_faulty_compo(
1637Hrc_Manager_t * hmgr,
1638Hrc_Node_t* rootNode,
1639Hrc_Model_t* newRootModel
1640)
1641{
1642        int i;
1643        Var_Variable_t *var;
1644        char * name, *newName;
1645        array_t *actualOutputArray, *actualOutputArrayG;
1646        array_t *actualInputArray, *actualInputArrayG;
1647
1648        Hrc_Model_t * rootModel  =  Hrc_ManagerFindModelByName(hmgr,Hrc_NodeReadModelName(rootNode));
1649        printf("Root %s\n",  Hrc_NodeReadModelName(rootNode));
1650
1651        Hrc_Node_t * newRootNode   =  Hrc_ModelReadMasterNode(newRootModel);
1652       
1653 
1654    actualOutputArray  = array_alloc(Var_Variable_t*,Hrc_NodeReadNumFormalOutputs(rootNode));
1655    actualOutputArrayG = array_alloc(Var_Variable_t*,0);
1656        // New Outputs Faulty and Golden
1657        Hrc_NodeForEachFormalOutput(rootNode,i,var){
1658                name = Var_VariableReadName(var);
1659                newName = ALLOC(char, strlen(name) +4);
1660                sprintf(newName, "%sG", name);
1661                Var_Variable_t * vG = Var_VariableDup(var, newRootNode);
1662                Var_VariableChangeName(vG,newName);
1663                Var_Variable_t * v = Var_VariableDup(var, newRootNode);
1664                Hrc_NodeAddVariable(newRootNode,v);
1665                array_insert_last(Var_Variable_t *, actualOutputArray, v);
1666                Hrc_NodeAddVariable(newRootNode,vG);
1667                array_insert_last(Var_Variable_t *, actualOutputArrayG, vG);
1668                Var_VariableResetPO(v);
1669                Var_VariableResetPO(vG);
1670                Hrc_NodeAddFormalOutput(newRootNode,v);
1671                Hrc_NodeAddFormalOutput(newRootNode,vG);
1672      }
1673        //New Inputs
1674        Hrc_NodeForEachFormalInput(rootNode,i,var){
1675                Var_Variable_t * v = Var_VariableDup(var, newRootNode);
1676                Hrc_NodeAddVariable(newRootNode,v);
1677                Var_VariableResetPI(v);
1678                Hrc_NodeAddFormalInput(newRootNode,v);
1679
1680      }
1681
1682
1683        // Create 2 instances "golden" and "faulty" of the previous hierarchy
1684        actualInputArray = array_dup(Hrc_NodeReadFormalInputs(newRootNode));
1685        actualInputArrayG= array_dup(Hrc_NodeReadFormalInputs(newRootNode));
1686    Hrc_ModelAddSubckt(newRootModel,rootModel, "golden",actualInputArrayG, actualOutputArrayG);
1687    Hrc_ModelAddSubckt(newRootModel,rootModel, "faulty",actualInputArray, actualOutputArray);
1688    // Create the new Hierarchy
1689        newRootNode = Hrc_ModelCreateHierarchy(hmgr, newRootModel, "ROB3");
1690        //replace the hierarchy with the new one
1691        Hrc_TreeReplace(rootNode,newRootNode);
1692
1693                return newRootNode;
1694}
1695/**Function********************************************************************
1696 *  Synopsis    [Generate name of protected register]
1697
1698  Description [Generate file containing names of latches in the golden model
1699  that have to be protected. ]
1700
1701  SideEffects []
1702******************************************************************************/
1703
1704int generateProtectFile(
1705Hrc_Node_t * goldenNode, 
1706FILE *oFile,
1707char * instanceName)
1708{
1709
1710        st_generator * gen;
1711        char* name, *childName,*newName;
1712        Hrc_Latch_t * latch;
1713        Hrc_Node_t * child;
1714        int a;
1715       
1716
1717        Hrc_NodeForEachLatch(goldenNode, gen,name,latch){
1718                if( instanceName =="")
1719                        fprintf(oFile,"%s\n",name);
1720                else
1721                        fprintf(oFile,"%s.%s\n",instanceName,name);
1722         }
1723    a = Hrc_NodeReadNumLatches(goldenNode);
1724
1725        if(Hrc_NodeReadNumChildren(goldenNode) != 0){
1726                Hrc_NodeForEachChild(goldenNode,gen,childName,child){
1727                        newName = malloc(strlen(instanceName)+strlen(childName)+1);
1728                        if( instanceName =="")
1729                                sprintf(newName,"%s",childName);
1730                        else
1731                                sprintf(newName,"%s.%s",instanceName,childName);
1732                        a += generateProtectFile(child,oFile,newName);
1733                }
1734        }
1735        return a;
1736}
1737
Note: See TracBrowser for help on using the repository browser.