source: vis_dev/vis-2.3/src/rob/robCmd.c @ 99

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

add part of cex
File size: 47.4 KB
Line 
1
2/**CFile***********************************************************************
3
4  FileName    [robCmd.c]
5
6  PackageName [rob]
7
8  Synopsis    [Commands for the Robustness package.]
9
10  Author      [Souheib Baarir, Denis Poitrenaud,J.M Ilié ]
11
12  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. Paris VI].
13  All rights reserved.
14
15  Permission is hereby granted, without written agreement and without license
16  or royalty fees, to use, copy, modify, and distribute this software and its
17  documentation for any purpose, provided that the above copyright notice and
18  the following two paragraphs appear in all copies of this software.
19
20  IN NO EVENT SHALL THE UNIVERSITY OF PARIS VI BE LIABLE TO ANY PARTY FOR
21  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
22  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
23  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24
25  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
26  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
27  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
28  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
29  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
30
31******************************************************************************/
32
33#include "Robust.h"
34
35/*---------------------------------------------------------------------------*/
36/* Variable declarations                                                     */
37/*---------------------------------------------------------------------------*/
38static jmp_buf timeOutEnv;
39
40/**AutomaticStart*************************************************************/
41
42/*---------------------------------------------------------------------------*/
43/* Static function prototypes                                                */
44/*---------------------------------------------------------------------------*/
45
46
47/*************** Robustness functions  ******************************************/
48
49static int CommandprintmddID     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
50static int CommandRobustness     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
51static int CommandSetSafe        (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
52static int CommandSetRequired    (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
53static int CommandSetForbidden   (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
54static int CommandSetInitial     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
55static int CommandResetRequired  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
56static int CommandResetForbidden (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
57static int CommandResetSafe      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
58static int CommandResetInitial   (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
59static int CommandPrintRequired  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
60static int CommandPrintSafe      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
61static int CommandPrintForbidden (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
62static int CommandConvForbToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
63static int CommandConvReachToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
64static int CommandConvSafeToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
65static int CommandConvReqToProp  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
66static int CommandConvInitToProp (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
67static int CommandSetLtlFormula  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
68static int CommandBmcRob         (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
69static int CommandResLtlFile     (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
70static int CommandTestCount      (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
71static int CommandComposeGolden  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
72static int CommandProtectGolden  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
73static int CommandProtectOutput  (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
74static int CommandProtectRegister(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
75static int CommandTestRob        (Hrc_Manager_t ** hmgr,int  argc, char ** argv);
76
77
78/*******************************************************************************/
79
80/**AutomaticEnd***************************************************************/
81
82
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions                                          */
85/*---------------------------------------------------------------------------*/
86
87
88/**Function********************************************************************
89
90  Synopsis    [Initializes the rob package.]
91
92  SideEffects []
93
94  SeeAlso     [rob_End]
95
96******************************************************************************/
97void
98Rob_Init(void)
99{
100
101/*************** Robustness commands  ****************************************/
102  Cmd_CommandAdd("printmddID",     CommandprintmddID,       0);
103  Cmd_CommandAdd("robustness",     CommandRobustness,       0);
104  Cmd_CommandAdd("set_safe",       CommandSetSafe,          0);
105  Cmd_CommandAdd("set_forbidden",  CommandSetForbidden,     0);
106  Cmd_CommandAdd("set_required",   CommandSetRequired,      0);
107  Cmd_CommandAdd("set_init",       CommandSetInitial,       0);
108  Cmd_CommandAdd("reset_required", CommandResetRequired,    0);
109  Cmd_CommandAdd("reset_forbidden",CommandResetForbidden,   0);
110  Cmd_CommandAdd("reset_safe",     CommandResetSafe,        0);
111  Cmd_CommandAdd("reset_init",     CommandResetInitial,     0);
112  Cmd_CommandAdd("print_forbidden",CommandPrintForbidden,   0);
113  Cmd_CommandAdd("print_required", CommandPrintRequired,    0);
114  Cmd_CommandAdd("print_safe",      CommandPrintSafe,       0);
115  Cmd_CommandAdd("conv_reach_prop", CommandConvReachToProp, 0);
116  Cmd_CommandAdd("conv_safe_prop",  CommandConvSafeToProp,  0);
117  Cmd_CommandAdd("conv_forb_prop",  CommandConvForbToProp,  0);
118  Cmd_CommandAdd("conv_req_prop",   CommandConvReqToProp,   0);
119  Cmd_CommandAdd("conv_init_prop",  CommandConvInitToProp,  0);
120  Cmd_CommandAdd("add_ltl_formula", CommandSetLtlFormula,   0);
121  Cmd_CommandAdd("bmc_rob",         CommandBmcRob,          0);
122  Cmd_CommandAdd("reset_ltl_file",  CommandResLtlFile,      0);
123  Cmd_CommandAdd("Test_count"    ,  CommandTestCount,       0);
124  Cmd_CommandAdd("compose_golden",  CommandComposeGolden,   0);
125  Cmd_CommandAdd("protect_golden",  CommandProtectGolden,   0);
126  Cmd_CommandAdd("protect_outputs",  CommandProtectOutput,  0);
127  Cmd_CommandAdd("protect_registers",CommandProtectRegister,0);
128  Cmd_CommandAdd("test_rob",         CommandTestRob,        0);
129 
130/*****************************************************************************/
131
132}
133
134/*---------------------------------------------------------------------------*/
135/* Definition of internal functions                                          */
136/*---------------------------------------------------------------------------*/
137void
138Rob_End(void)
139{
140}
141
142/*---------------------------------------------------------------------------*/
143/* Definition of static functions                                            */
144/*---------------------------------------------------------------------------*/
145
146static int 
147CommandprintmddID (Hrc_Manager_t ** hmgr,
148                   int  argc, char ** argv){
149  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
150  mdd_manager      *mddManager = Fsm_FsmReadMddManager(fsm);
151  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
152  int                  arrSize = array_n( psVarsArray );
153  int i;
154
155  for ( i = 0 ; i < arrSize ; ++i ) {
156    int      mddId = array_fetch( int, psVarsArray, i );
157    mvar_type mVar = array_fetch(mvar_type, 
158                                 mdd_ret_mvar_list(mddManager),mddId);
159    printf("%s : %d\n", mVar.name, mddId);
160  }
161  return 0;
162}
163
164/*---------------------------------------------------------------------------*/
165/* Definition of static functions                                            */
166/*---------------------------------------------------------------------------*/
167
168static int 
169CommandTestCount (Hrc_Manager_t ** hmgr,
170                   int  argc, char ** argv){
171  char* fichier="./test";
172  int k= 0;//main_Count_test_(fichier);
173  printf("res= %d \n",k);
174  return 0;
175}
176
177
178// Reset to empty, the file
179// of ltl properties.
180static int 
181CommandResLtlFile (Hrc_Manager_t ** hmgr,
182                   int  argc, char ** argv){
183
184  FILE* oFile = NIL(FILE);
185  if (argc == 2) {
186    oFile = Cmd_FileOpen(argv[1],
187                         "w", NIL(char *), 0);
188  }
189  else{
190    oFile = Cmd_FileOpen("properties.ltl",
191                         "w", NIL(char *), 0);
192  }
193 
194  fclose(oFile);
195
196  return 0; 
197}
198
199// Add an ltl formula to the
200// the file of ltl properties.
201static int 
202CommandSetLtlFormula (Hrc_Manager_t ** hmgr,
203                      int  argc, char ** argv){
204
205 
206  char c;
207  int i=1;
208  FILE* oFile=NIL(FILE); 
209
210  if (argc < 2) {
211    conv_error_msg(vis_stderr, "add_ltl_formula",earg); 
212    return 1;
213  }
214
215  util_getopt_reset();
216  while ((c = util_getopt(argc, argv, "f:")) != EOF) {
217    switch(c) {
218    case 'f':
219      oFile = Cmd_FileOpen(util_optarg, 
220                           "a+", NIL(char *), 0);
221      i=3;
222      break;
223    default :
224     break;
225    }
226  }
227 
228  if (i!=3) {
229    oFile = Cmd_FileOpen("properties.ltl", 
230                         "a+", NIL(char *), 0);
231  }
232
233  if (oFile == NIL(FILE)) {
234    conv_error_msg(vis_stderr, 
235                   "add_ltl_formula",eofile);
236    return 1;
237  }     
238 
239  fprintf(oFile," %s ;\n",argv[i]);
240  fclose(oFile);
241 
242  return 0; 
243}
244
245// Convert the set of initial states
246// to a propositional formula
247// and put it in the proprerties file.
248static int 
249CommandConvInitToProp (Hrc_Manager_t ** hmgr,
250                       int  argc, char ** argv){
251
252  FILE* oFile=NIL(FILE);
253  Fsm_Fsm_t  *fsm = 
254    Fsm_HrcManagerReadCurrentFsm(*hmgr);
255
256  if(fsm == NIL(Fsm_Fsm_t))
257    return 1;
258 
259  if (argc == 2) {
260    oFile = Cmd_FileOpen(argv[1],
261                         "a+", NIL(char *), 0);
262  }
263  else{
264    oFile = Cmd_FileOpen("properties.ltl",
265                       "a+", NIL(char *), 0);
266  }
267
268  if (oFile == NIL(FILE)) {
269     conv_error_msg(vis_stderr, "conv_init_prop",eofile);
270    return 1;
271  }
272 
273  mdd_t* set = getInitial(fsm);
274  if (set == NIL(mdd_t)){
275    conv_error_msg(vis_stderr, "conv_init_prop",ecmd);
276    return 1;
277  }
278 
279   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
280                         set, "INIT", oFile);
281 
282   fclose(oFile);                     
283  return 0; 
284}
285
286// Convert the set of safe states
287// to a propotitional formula
288// and put it in the proprerties file.
289static int 
290CommandConvReachToProp (Hrc_Manager_t ** hmgr,
291                       int  argc, char ** argv){
292 
293  FILE* oFile=NIL(FILE);
294  Fsm_Fsm_t  *fsm = 
295    Fsm_HrcManagerReadCurrentFsm(*hmgr);
296 
297  if(fsm == NIL(Fsm_Fsm_t))
298    return 1;
299
300  if (argc == 2) {
301    oFile = Cmd_FileOpen(argv[1],
302                         "a+", NIL(char *), 0);
303  } else{
304    oFile = Cmd_FileOpen("properties.ltl",
305                         "a+", NIL(char *), 0);
306  }
307
308  if (oFile == NIL(FILE)) {
309     conv_error_msg(vis_stderr, 
310                    "conv_reach_prop",eofile);
311    return 1;
312  }
313 
314  mdd_t* set = getReach(fsm);
315  if (set == NIL(mdd_t)){
316    conv_error_msg(vis_stderr, 
317                   "conv_reach_prop",ecmd);
318   
319    return 1;
320  }
321 
322   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
323                         set, "REACH", oFile);
324 
325   fclose(oFile);                     
326   return 0;
327}
328
329// Convert the set of safe states
330// to a propotitional formula
331// and put it in the proprerties file.
332static int 
333CommandConvSafeToProp (Hrc_Manager_t ** hmgr,
334                       int  argc, char ** argv){
335 
336  FILE* oFile=NIL(FILE);
337  Fsm_Fsm_t  *fsm = 
338    Fsm_HrcManagerReadCurrentFsm(*hmgr);
339 
340  if(fsm == NIL(Fsm_Fsm_t))
341    return 1;
342
343  if (argc == 2) {
344    oFile = Cmd_FileOpen(argv[1],
345                         "a+", NIL(char *), 0);
346  } else{
347    oFile = Cmd_FileOpen("properties.ltl",
348                         "a+", NIL(char *), 0);
349  }
350
351  if (oFile == NIL(FILE)) {
352     conv_error_msg(vis_stderr, 
353                    "conv_safe_prop",eofile);
354    return 1;
355  }
356 
357  mdd_t* set = getSafe(fsm);
358  if (set == NIL(mdd_t)){
359    conv_error_msg(vis_stderr, 
360                   "conv_safe_prop",ecmd);
361   
362    return 1;
363  }
364 
365   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
366                         set, "SAFE", oFile);
367 
368   fclose(oFile);                     
369   return 0;
370}
371
372// Convert the set of required states
373// to a propotitional formula
374// and put it in the proprerties file.
375static int 
376CommandConvReqToProp (Hrc_Manager_t ** hmgr,
377                       int  argc, char ** argv){
378  FILE* oFile=NIL(FILE);
379  Fsm_Fsm_t  *fsm = 
380    Fsm_HrcManagerReadCurrentFsm(*hmgr);
381 
382  if(fsm == NIL(Fsm_Fsm_t))
383    return 1;
384
385  if (argc == 2) {
386    oFile = Cmd_FileOpen(argv[1],
387                         "a+", NIL(char *), 0);
388  } else{
389    oFile = Cmd_FileOpen("properties.ltl",
390                         "a+", NIL(char *), 0);
391  }
392 
393  if (oFile == NIL(FILE)) {
394     conv_error_msg(vis_stderr, 
395                    "conv_req_prop",eofile);
396    return 1;
397  }
398 
399  mdd_t* set = getRequired(fsm);
400  if (set == NIL(mdd_t)){
401    conv_error_msg(vis_stderr, 
402                   "conv_req_prop",ecmd);
403    return 1;
404  }
405 
406   mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
407                         set, "REQ", oFile);
408   fclose(oFile);
409                       
410   return 0;
411}
412
413// Convert the set of forbidden states
414// to a propotitional formula
415// and put it in the proprerties file.
416static int 
417CommandConvForbToProp (Hrc_Manager_t ** hmgr,
418                       int  argc, char ** argv){
419 FILE* oFile=NIL(FILE);
420  Fsm_Fsm_t  *fsm = 
421    Fsm_HrcManagerReadCurrentFsm(*hmgr);
422 
423  if(fsm == NIL(Fsm_Fsm_t))
424    return 1;
425
426  if (argc == 2) {
427    oFile = Cmd_FileOpen(argv[1],
428                         "a+", NIL(char *), 0);
429  } else{
430    oFile = Cmd_FileOpen("properties.ltl",
431                         "a+", NIL(char *), 0);
432  }
433
434  if (oFile == NIL(FILE)) {
435    conv_error_msg(vis_stderr, 
436                   "conv_forb_prop",eofile);
437    return 1;
438  }
439 
440  mdd_t* set = getForbidden(fsm);
441  if (set == NIL(mdd_t)){
442    conv_error_msg(vis_stderr, 
443                   "conv_forb_prop",ecmd);
444    return 1;
445  }
446 
447  mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
448                        set, "FORB", oFile);
449  fclose(oFile);       
450  return 0;
451
452}
453
454
455// This command computes the set of forbiden states
456// w.r.t a given ctl formula. This formula is read from
457// a file given as a parameter.
458static int
459CommandSetForbidden( Hrc_Manager_t ** hmgr,
460                    int  argc,
461                    char ** argv){
462  int c;
463  FILE* forFile=NIL(FILE);
464  Fsm_Fsm_t  *fsm = 
465    Fsm_HrcManagerReadCurrentFsm(*hmgr);
466 
467  if(fsm == NIL(Fsm_Fsm_t))
468    return 1;
469
470  util_getopt_reset();
471  while ((c = util_getopt(argc, argv, "h")) != EOF) {
472    switch(c) {
473      case 'h':
474      default:
475        (void)error_msg(vis_stderr,"forbiden", ecmd) ;
476        return 1;
477    }
478  }
479
480  if ((argc - util_optind == 0) || 
481      (argc - util_optind > 1) ) {
482    (void)error_msg(vis_stderr, "forbiden",enfile ) ;
483    return 1;
484  }
485 
486  forFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
487  if (forFile == NIL(FILE)) {
488    error_msg(vis_stderr, "forbiden",eofile);
489    return 1;
490  }
491 
492  fsm->RobSets.fForb=forFile;
493
494  if (fsm->RobSets.Forb != NIL(mdd_t))
495    mdd_free(fsm->RobSets.Forb);
496
497  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
498  array_t *careStatesArray = array_alloc(mdd_t *, 0);
499  array_insert(mdd_t *, careStatesArray, 0,mddOne);
500 
501  if (Fsm_FsmReadFairnessConstraint(fsm)!=
502           NIL(Fsm_Fairness_t)) {
503    Fsm_FsmComputeFairStates(fsm,
504                             careStatesArray,
505                             0, 
506                             McDcLevelNone_c,
507                             McGSH_Unassigned_c ,
508                             McBwd_c, FALSE );
509    }
510  else {
511   
512    fsm->fairnessInfo.states = 
513      mdd_one(Fsm_FsmReadMddManager(fsm));
514
515  }
516
517  fsm->RobSets.Forb=
518    evaluate(fsm,forFile, 
519             fsm->fairnessInfo.states, 
520             Fsm_FsmReadFairnessConstraint(fsm),0);
521 
522  array_free(careStatesArray);
523  mdd_free(mddOne);
524
525 
526  return 0; 
527}
528
529// This command sets the forbiden set of states to
530// mdd_zero.This means that all states are allowed.
531static int
532CommandResetForbidden( Hrc_Manager_t ** hmgr,
533                      int  argc,
534                      char ** argv){
535 
536  Fsm_Fsm_t *fsm = 
537    Fsm_HrcManagerReadCurrentFsm(*hmgr);
538
539  if(fsm == NIL(Fsm_Fsm_t))
540    return 1;
541 
542  if (fsm->RobSets.Forb != NIL(mdd_t))
543    mdd_free(fsm->RobSets.Forb);
544
545  fsm->RobSets.Forb=
546    mdd_zero(Fsm_FsmReadMddManager(fsm));
547  fsm->RobSets.fForb = NIL(FILE);
548  return 0;
549}
550
551static int
552CommandPrintForbidden( Hrc_Manager_t ** hmgr,
553                      int  argc,
554                      char ** argv){
555
556  char formula[1024] ;
557
558  Fsm_Fsm_t  *fsm = 
559    Fsm_HrcManagerReadCurrentFsm(*hmgr);
560 
561  if(fsm == NIL(Fsm_Fsm_t))
562    return 1;
563 
564  if (fsm->RobSets.fForb != NIL(FILE)){
565    fseek(fsm->RobSets.fForb,0,SEEK_SET);
566    fread (formula,sizeof(char),1024,fsm->RobSets.fForb);
567    printf("Forbiden is the set of states that satisfy: %s\n",formula);
568  }
569  else{
570     printf("Forbiden is the set of states that satisfy: FALSE \n");
571  }
572
573  return 0;
574
575}
576
577// This command computes the set of required states
578// w.r.t a given ctl formula. This formula is read from
579// a file given as a parameter.
580static int
581CommandSetRequired( Hrc_Manager_t ** hmgr,
582                    int  argc,
583                    char ** argv){ 
584
585  int c;
586  FILE* reqFile=NIL(FILE);
587  Fsm_Fsm_t  *fsm = 
588    Fsm_HrcManagerReadCurrentFsm(*hmgr);
589
590  if(fsm == NIL(Fsm_Fsm_t))
591    return 1;
592
593  util_getopt_reset();
594  while ((c = util_getopt(argc, argv, "h")) != EOF) {
595    switch(c) {
596      case 'h':
597      default:
598        (void)error_msg(vis_stderr,"required", ecmd); 
599        return 1;
600    }
601  }
602
603  if ((argc - util_optind == 0) || 
604      (argc - util_optind > 1) ) {
605    (void)error_msg(vis_stderr, "required", enfile); 
606    return 1;
607  }
608 
609  reqFile = 
610    Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
611
612  if (reqFile == NIL(FILE)) {
613    error_msg(vis_stderr, "required", eofile); 
614    return 1;
615  }
616
617  fsm->RobSets.fReq=reqFile;
618
619  if (fsm->RobSets.Req != NIL(mdd_t))
620    mdd_free(fsm->RobSets.Req);
621
622
623  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
624  array_t *careStatesArray = array_alloc(mdd_t *, 0);
625  array_insert(mdd_t *, careStatesArray, 0,mddOne);
626 
627  if (Fsm_FsmReadFairnessConstraint(fsm)!=
628           NIL(Fsm_Fairness_t)) {
629    Fsm_FsmComputeFairStates(fsm,
630                             careStatesArray,
631                             0, 
632                             McDcLevelNone_c,
633                             McGSH_Unassigned_c ,
634                             McBwd_c, FALSE );
635    }
636  else {
637   
638    fsm->fairnessInfo.states = 
639      mdd_one(Fsm_FsmReadMddManager(fsm));
640
641  }
642
643  fsm->RobSets.Req= 
644    evaluate(fsm,reqFile, 
645             fsm->fairnessInfo.states, 
646             Fsm_FsmReadFairnessConstraint(fsm),0);
647 
648  array_free(careStatesArray);
649  mdd_free(mddOne);
650
651 
652  return 0;
653 
654}
655
656// This command sets the required set of states to
657// mdd_one.This means that no restriction is given.
658static int
659CommandResetRequired( Hrc_Manager_t ** hmgr,
660                      int  argc,
661                      char ** argv){
662 
663  Fsm_Fsm_t  *fsm = 
664    Fsm_HrcManagerReadCurrentFsm(*hmgr);
665
666  if(fsm == NIL(Fsm_Fsm_t))
667    return 1;
668 
669  if (fsm->RobSets.Req != NIL(mdd_t))
670    mdd_free(fsm->RobSets.Req);
671
672  fsm->RobSets.Req=
673    mdd_one(Fsm_FsmReadMddManager(fsm));
674   fsm->RobSets.fReq = NIL(FILE);
675  return 0;
676}
677
678static int
679CommandPrintRequired( Hrc_Manager_t ** hmgr,
680                    int  argc,
681                    char ** argv){
682
683  char formula[1024] ;
684
685  Fsm_Fsm_t  *fsm = 
686    Fsm_HrcManagerReadCurrentFsm(*hmgr);
687 
688  if(fsm == NIL(Fsm_Fsm_t))
689    return 1;
690 
691  if (fsm->RobSets.fReq != NIL(FILE)){
692    fseek(fsm->RobSets.fReq,0,SEEK_SET);
693    fread (formula,sizeof(char),1024,fsm->RobSets.fReq);
694    printf("Required is the set of states that satisfy: %s\n",formula);
695  }
696  else{
697     printf("Required is the set of states that satisfy: TRUE \n");
698  }
699
700  return 0;
701
702}
703// This command computes the set of safe states
704// w.r.t a given ctl formula. This formula is read from
705// a file given as a parameter.
706static int
707CommandSetSafe( Hrc_Manager_t ** hmgr,
708                int  argc,
709                char ** argv){
710  Fsm_Fsm_t  *fsm = 
711    Fsm_HrcManagerReadCurrentFsm(*hmgr);
712  FILE *safeFile=NIL(FILE);
713  int        c;
714 
715  if(fsm == NIL(Fsm_Fsm_t))
716    return 1;
717
718  util_getopt_reset();
719  while ((c = util_getopt(argc, argv, "h")) != EOF) {
720    switch(c) {
721      case 'h':
722      default:
723        (void) error_msg(vis_stderr, "safe", ecmd); 
724        return 1;
725    }
726  }
727
728  if ((argc - util_optind == 0) || 
729      (argc - util_optind > 1) ) {
730    (void)error_msg(vis_stderr, "safe", enfile);
731    return 1;
732  }
733
734  safeFile = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
735
736  if (safeFile == NIL(FILE)) {
737    error_msg(vis_stderr, "safe", eofile);
738    return 1;
739  }
740
741
742
743  fsm->RobSets.fSafe=safeFile;
744
745  if (fsm->RobSets.Safe != NIL(mdd_t))
746    mdd_free(fsm->RobSets.Safe);
747
748  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
749  array_t *careStatesArray = array_alloc(mdd_t *, 0);
750  array_insert(mdd_t *, careStatesArray, 0,mddOne);
751 
752  if (Fsm_FsmReadFairnessConstraint(fsm)!=
753           NIL(Fsm_Fairness_t)) {
754    Fsm_FsmComputeFairStates(fsm,
755                             careStatesArray,
756                             0, 
757                             McDcLevelNone_c,
758                             McGSH_Unassigned_c ,
759                             McBwd_c, FALSE );
760    }
761  else {
762   
763    fsm->fairnessInfo.states = 
764      mdd_one(Fsm_FsmReadMddManager(fsm));
765
766  }
767
768  fsm->RobSets.Safe=
769    evaluate(fsm,safeFile, 
770             fsm->fairnessInfo.states, 
771             Fsm_FsmReadFairnessConstraint(fsm),0);
772 
773  array_free(careStatesArray);
774  mdd_free(mddOne);
775
776  return 0;
777}
778
779// This command sets the safe set of states to
780// the reachable set of states (without bit-flips).
781static int
782CommandResetSafe( Hrc_Manager_t ** hmgr,
783                  int  argc,
784                  char ** argv){
785 
786  Fsm_Fsm_t  *fsm = 
787    Fsm_HrcManagerReadCurrentFsm(*hmgr);
788
789  if(fsm == NIL(Fsm_Fsm_t))
790    return 1;
791 
792  if (fsm->RobSets.Safe != NIL(mdd_t))
793    mdd_free(fsm->RobSets.Safe);
794
795  mdd_t* inits=fsm->reachabilityInfo.initialStates;
796  mdd_t* reachs=fsm->reachabilityInfo.reachableStates;
797  fsm->reachabilityInfo.initialStates=NIL(mdd_t);
798  fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
799
800  (void)Fsm_FsmComputeInitialStates(fsm);
801  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
802                                      0,0, 0,
803                                      0, 0, Fsm_Rch_Default_c,
804                                      0,0, NIL(array_t),
805                                      0,  NIL(array_t));
806
807  fsm->RobSets.Safe=
808    mdd_dup(fsm->reachabilityInfo.reachableStates);
809
810  mdd_free(fsm->reachabilityInfo.initialStates);
811  mdd_free(fsm->reachabilityInfo.reachableStates);
812  fsm->reachabilityInfo.initialStates=inits;
813  fsm->reachabilityInfo.reachableStates=reachs;
814  fsm->RobSets.fSafe = NIL(FILE);
815 
816  return 0;
817}
818
819static int
820CommandPrintSafe( Hrc_Manager_t ** hmgr,
821                    int  argc,
822                    char ** argv){
823
824  char formula[1024] ;
825
826  Fsm_Fsm_t  *fsm = 
827    Fsm_HrcManagerReadCurrentFsm(*hmgr);
828 
829  if(fsm == NIL(Fsm_Fsm_t))
830    return 1;
831 
832  if (fsm->RobSets.fSafe != NIL(FILE)){
833    fseek(fsm->RobSets.fSafe,0,SEEK_SET);
834    fread (formula,sizeof(char),1024,fsm->RobSets.fSafe);
835    printf("Safe is the set of states that satisfy: %s\n",formula);
836  }
837  else{
838    printf("Safe is the set of states that is orginaly rechable from the design  \n");
839  }
840
841  return 0;
842
843}
844
845// This command computes the disign's initial set of states,
846// starting from the reachable states and 
847// taking into acount all bit-flips arriving on non
848// protected sequecial elements. The set of protected sequencial
849// elements are given as parameter in a given file.
850static int 
851CommandSetInitial(Hrc_Manager_t ** hmgr,
852                  int  argc,
853                  char ** argv){
854  FILE       *proFile=NIL(FILE);
855  FILE       *forFile=NIL(FILE);
856  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
857  static int  verbosityLevel=0;
858  static int  printStep=0;
859  int         formula=0;
860  long        initialTime;
861  long        finalTime;
862  int         c;
863  int         fmodel = 1;
864 
865  if(fsm == NIL(Fsm_Fsm_t))
866    return 1;
867
868  util_getopt_reset();
869  while ((c = util_getopt(argc, argv, "hg:s:v:f:m:")) != EOF) {
870    switch(c) {
871     case 'g' :
872       proFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0);
873       if (proFile == NIL(FILE)) {
874         error_msg(vis_stderr, "init", eiofile);
875        return 1;
876       }       
877      break;
878    case 'f' :
879       forFile = Cmd_FileOpen(util_optarg,"r", NIL(char *), 0);
880       if (forFile == NIL(FILE)) {
881         error_msg(vis_stderr, "init", eiofile);
882        return 1;
883       }       
884       formula=1;
885      break;
886     case 's' :
887       printStep = atoi(util_optarg); break;
888     case 'v' :
889       verbosityLevel = atoi(util_optarg); break; 
890     case 'm' :
891       
892       if (strcmp(util_optarg, "usut") == 0) {fmodel = 2;break;}
893       if (strcmp(util_optarg, "usmt") == 0) {fmodel = 3;break;}
894       if (strcmp(util_optarg, "msut") == 0) {fmodel = 4;break;}
895       if (strcmp(util_optarg, "msmt") == 0) {fmodel = 5;break;}
896       
897
898     case 'h': 
899     default : error_msg(vis_stderr, "init", eicmd); return 1;
900    }
901  }
902
903  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
904    mdd_free(fsm->reachabilityInfo.initialStates);
905    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
906  }
907
908  if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){
909    mdd_free(fsm->reachabilityInfo.reachableStates);
910    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
911  }
912
913  initialTime = util_cpu_time();
914  (void)Fsm_FsmComputeInitialStates(fsm);
915  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
916                                      0,0, 0,
917                                      0,0, Fsm_Rch_Default_c,
918                                      0,0, NIL(array_t),
919                                      0,   NIL(array_t));
920 
921  fsm->RobSets.originalreachableStates = 
922    mdd_dup(fsm->reachabilityInfo.reachableStates);
923 
924  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
925    mdd_free(fsm->reachabilityInfo.initialStates);
926    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
927  }
928
929 //mdd_free(fsm->reachabilityInfo.initialStates);
930 
931  if (fmodel == 1)
932    fsm->reachabilityInfo.initialStates= 
933      compute_error_states(fsm,fsm->reachabilityInfo.reachableStates,   
934                           verbosityLevel,printStep, proFile);
935 
936  if (fmodel == 2)
937    fsm->reachabilityInfo.initialStates= 
938      error_states_us_ut(fsm,fsm->reachabilityInfo.reachableStates,proFile);
939
940  if (fmodel == 3)
941    fsm->reachabilityInfo.initialStates= 
942      error_states_us_mt(fsm,fsm->reachabilityInfo.reachableStates, proFile);
943
944  if (fmodel == 4)
945    fsm->reachabilityInfo.initialStates= 
946      error_states_ms_ut(fsm,fsm->reachabilityInfo.reachableStates, proFile);
947
948  if (fmodel == 5){
949     (void)Fsm_FsmComputeInitialStates(fsm);
950     mdd_t* S0 = mdd_dup(fsm->reachabilityInfo.initialStates);
951      mdd_free(fsm->reachabilityInfo.initialStates);
952    fsm->reachabilityInfo.initialStates= 
953      error_states_ms_mt(fsm,S0,fsm->reachabilityInfo.reachableStates, proFile);
954    mdd_free(S0);
955  }
956   
957 
958  mdd_free(fsm->reachabilityInfo.reachableStates);
959  fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
960 
961  if(!formula) {
962    fsm->reachabilityInfo.reachableStates=
963      Fsm_FsmComputeReachableStates(fsm,0,0,
964                                  0,0, 0,
965                                  0, 0, Fsm_Rch_Default_c,
966                                  0,0, NIL(array_t),
967                                  0,  NIL(array_t));
968  }
969  else {
970    mdd_t* newinit_tmp=evaluate(fsm,forFile,NIL(mdd_t), 
971                                Fsm_FsmReadFairnessConstraint(fsm),0);
972    mdd_t* newinit=mdd_and(fsm->reachabilityInfo.initialStates,
973                           newinit_tmp,1,1);
974
975    mdd_free(newinit_tmp);
976    mdd_free(fsm->reachabilityInfo.initialStates);
977    fsm->reachabilityInfo.initialStates=newinit;
978    mdd_free(fsm->reachabilityInfo.reachableStates);
979    fsm->reachabilityInfo.reachableStates=
980      Fsm_FsmComputeReachableStates(fsm,0,0,
981                                  0,0, 0,
982                                  0, 0, Fsm_Rch_Default_c,
983                                  0,0, NIL(array_t),
984                                  0,  NIL(array_t));
985  }
986
987  finalTime = util_cpu_time();
988   
989  if(verbosityLevel){ 
990   (void) fprintf(vis_stdout,"********************************\n");
991     print_number_of_states("Error states                        = ", fsm, 
992                           fsm->reachabilityInfo.initialStates);
993     print_number_of_states("States reachable from error states  = ", fsm, 
994                           fsm->reachabilityInfo.reachableStates);
995     print_number_of_states("Reachable states whithout faults   = ", fsm, 
996                            fsm->RobSets.originalreachableStates);
997    (void) fprintf(vis_stdout, "%-50s%15g\n",
998                            "Analysis time                       = ",
999                            (double)(finalTime-initialTime)/1000.0);
1000
1001//    printf("-----------------------------------------------\n");
1002//    print_bdd(Fsm_FsmReadMddManager(fsm), fsm->reachabilityInfo.reachableStates);
1003//    bdd_print(fsm->reachabilityInfo.reachableStates);
1004//    printf("-----------------------------------------------\n");
1005  }
1006 
1007  return 0;
1008}
1009
1010// This command sets the design's initial set of states
1011// to the original one (without bit-flips). It also computes
1012// the reachable states according to this initial set. 
1013static int
1014CommandResetInitial( Hrc_Manager_t ** hmgr,
1015                     int  argc,
1016                     char ** argv){
1017 
1018  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
1019
1020  if(fsm == NIL(Fsm_Fsm_t))
1021    return 1;
1022
1023  if (fsm->reachabilityInfo.initialStates!=NIL(mdd_t)){
1024    mdd_free(fsm->reachabilityInfo.initialStates);
1025    fsm->reachabilityInfo.initialStates=NIL(mdd_t);
1026  }
1027 
1028  if (fsm->reachabilityInfo.reachableStates!=NIL(mdd_t)){
1029    mdd_free(fsm->reachabilityInfo.reachableStates);
1030    fsm->reachabilityInfo.reachableStates=NIL(mdd_t);
1031  }
1032  (void)Fsm_FsmComputeInitialStates(fsm);
1033  (void)Fsm_FsmComputeReachableStates(fsm,0,0,
1034                                      0,0, 0,
1035                                      0, 0, Fsm_Rch_Default_c,
1036                                      0,0, NIL(array_t),
1037                                      0,  NIL(array_t));
1038  return 0;
1039}
1040
1041// This command computes the design's robustness.
1042// This needs the evaluation of the diffirent ctl formulae :
1043// 1- A[!forbiden U Required & A[!forbiden U Safe]]
1044// 2- A[!forbiden U Required & E[!forbiden U Safe]]
1045// 3- E[!forbiden U Required & A[!forbiden U Safe]]
1046// 4- E[!forbiden U Required & E[!forbiden U Safe]].
1047
1048static int
1049CommandRobustness( Hrc_Manager_t ** hmgr,
1050                   int  argc,
1051                   char ** argv) { 
1052  int        c;
1053  mdd_t      *reachableStates = NIL(mdd_t);
1054  mdd_t      *initialStates;
1055  long        initialTime;
1056  long        finalTime;
1057  static int  verbosityLevel;
1058  static int  printStep;
1059  static int  timeOutPeriod;
1060  Fsm_Fsm_t  *fsm = 
1061    Fsm_HrcManagerReadCurrentFsm(*hmgr);
1062  static int reorderFlag;
1063  static int reorderThreshold;
1064  static int shellFlag;
1065  static int depthValue;
1066  static int incrementalFlag;
1067  static int approxFlag;
1068  static int ardc;
1069  static int recompute;
1070  Fsm_RchType_t rchType;
1071
1072  static int req;
1073  FILE *reqFile=NIL(FILE);
1074  static int forb;
1075  FILE *forFile=NIL(FILE);
1076  static int pro;
1077  FILE *proFile=NIL(FILE);
1078  static int fair;
1079  FILE *fairFile=NIL(FILE);
1080  static int init=0;
1081  boolean rob1 = 0;
1082
1083  FILE *guideFile = NIL(FILE); /* file of hints for guided search */
1084  array_t *guideArray = NIL(array_t);
1085
1086  Img_MethodType imgMethod;
1087  mdd_t      * error_states;
1088  mdd_t      *reach,   *notReach; /* Etats accessibles du systï¿œme original */
1089  mdd_t      *tmp1,    *tmp2;
1090  EpDouble   *error    = EpdAlloc();
1091  EpDouble   *err      = EpdAlloc();
1092  EpDouble   *nbstates = EpdAlloc();
1093  EpDouble   *rch      = EpdAlloc();
1094  EpDouble   *error0   = EpdAlloc();
1095  char        percent[1024];
1096  char        nbst[1024];
1097  mdd_t      *forbiden, *required, *notforbiden,*fairS;
1098  mdd_t      *XU_notForb_And_Safe;
1099  mdd_t      *Req_And_XU_notForb_And_Safe;
1100  mdd_t      *Setformula;
1101  mdd_t      *res,*res_r,*res_0;
1102  Fsm_Fairness_t * fairCons=NIL(Fsm_Fairness_t);
1103
1104 
1105  verbosityLevel = 0;
1106  printStep      = 0;
1107  timeOutPeriod  = 0;
1108  shellFlag = 0;
1109  depthValue = 0;
1110  incrementalFlag = 0;
1111  rchType = Fsm_Rch_Default_c;
1112  approxFlag = 0;
1113  ardc = 0;
1114  recompute = 0;
1115 
1116  if(fsm == NIL(Fsm_Fsm_t))
1117    return 1;
1118
1119  util_getopt_reset();
1120
1121  while ((c = util_getopt(argc, argv, "hs:r:v:")) != EOF) {
1122    switch(c) {
1123    case 's':
1124      printStep = atoi(util_optarg);
1125      break;
1126    case 'v':
1127      verbosityLevel = atoi(util_optarg);
1128      break; 
1129        case 'r':
1130                rob1= atoi(util_optarg);
1131                break;
1132    case 'h':
1133    default : 
1134      error_msg(vis_stderr, "rob", ercmd); return 1;
1135    }
1136  }
1137
1138  mdd_t* Forb = getForbidden(fsm);
1139  mdd_t* Req  = getRequired(fsm); 
1140  mdd_t* Safe = getSafe(fsm); 
1141  mdd_t* Init = getInitial(fsm) ;
1142  mdd_t* Orig = getReachOrg(fsm);
1143
1144  if ((Fsm_FsmReadFairnessConstraint(fsm))!=
1145      NIL(Fsm_Fairness_t)) {
1146    compute_fair(fsm,verbosityLevel);
1147  } 
1148  else {
1149    fsm->fairnessInfo.states = 
1150      mdd_one(Fsm_FsmReadMddManager(fsm)); 
1151  }
1152 
1153  get_number_of_states(fsm,fsm->reachabilityInfo.reachableStates, error); 
1154  get_number_of_states(fsm,Init, error0);
1155  get_number_of_states(fsm,Orig, rch);
1156 
1157  //Compute robustness 1
1158  if(rob1)
1159  {
1160            (void) fprintf(vis_stdout,"********************************\n");
1161            (void) fprintf(vis_stdout, 
1162                 "Dealing with  F = AG[Safe]]\n");
1163            initialTime = util_cpu_time(); 
1164                Setformula= mdd_not(evaluate_EF(fsm, Safe, fsm->fairnessInfo.states,
1165                verbosityLevel));
1166                finalTime = util_cpu_time();
1167                res_0=mdd_and(Init, Setformula, 1, 1);
1168                res_r=mdd_and(Orig,Setformula, 1, 1); 
1169                mdd_free(Setformula);
1170 
1171                get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1172                EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1173                EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1174                (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1175                         "  --Error states satisfying F                                        = ", 
1176                         nbst,percent);
1177 
1178                get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1179                EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1180                EpdDivide2(nbstates, rch);  EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1181                (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1182                  "  --Error states originaly reachable by the design and satisfying F  = ", 
1183                  nbst,percent);
1184   
1185                (void) fprintf(vis_stdout, "%-50s%15g\n",
1186                  "  Analysis time                                                      = ", 
1187                  (double)(finalTime-initialTime)/1000.0);
1188        // EG       
1189     (void) fprintf(vis_stdout,"********************************\n");   
1190     (void) fprintf(vis_stdout,
1191          "Dealing with F =  EG[Safe]] \n");
1192 
1193     initialTime = util_cpu_time();
1194
1195     Setformula=evaluate_EG(fsm, mdd_not(Safe), fsm->fairnessInfo.states,NIL(Fsm_Fairness_t),verbosityLevel);
1196     finalTime = util_cpu_time();
1197     
1198     res_0=mdd_and(Init, Setformula, 1, 1);
1199     res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
1200 
1201     get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1202     EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1203     EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1204     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1205          "  --Error states satisfying F                                        = ", 
1206          nbst,percent);
1207   
1208     get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1209     EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1210     EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100);  EpdGetString(nbstates, percent);
1211     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1212          "  --Error states originaly reachable by the design and satisfying F  = ", 
1213          nbst,percent);
1214 
1215     (void) fprintf(vis_stdout, "%-50s%15g\n",               
1216          "  Analysis time                                                      = ", 
1217          (double)(finalTime-initialTime)/1000.0);
1218
1219  } 
1220 else{
1221           (void) fprintf(vis_stdout,"********************************\n");
1222           (void) fprintf(vis_stdout, 
1223                 "Dealing with  F = A[!forbiden U Required & A[!forbiden U Safe]]\n");
1224           initialTime = util_cpu_time(); 
1225           Setformula= evaluate_Formula_AF_AF (fsm, Req,Forb,Safe, verbosityLevel );
1226           finalTime = util_cpu_time();
1227           res_0=mdd_and(Init, Setformula, 1, 1);
1228           res_r=mdd_and(Orig,Setformula, 1, 1); 
1229        mdd_free(Setformula);
1230           
1231           get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1232           EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1233           EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1234           (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1235                 "  --Error states satisfying F                                        = ", 
1236                 nbst,percent);
1237           
1238           get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1239           EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1240            EpdDivide2(nbstates, rch);  EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1241            (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1242                  "  --Error states originaly reachable by the design and satisfying F  = ", 
1243                  nbst,percent);
1244           
1245            (void) fprintf(vis_stdout, "%-50s%15g\n",
1246          "  Analysis time                                                      = ", 
1247          (double)(finalTime-initialTime)/1000.0);
1248     
1249     
1250     (void) fprintf(vis_stdout,"********************************\n");   
1251     (void) fprintf(vis_stdout,
1252          "Dealing with F =  E[!forbiden U Required & A[!forbiden U Safe]] \n");
1253 
1254     initialTime = util_cpu_time();
1255     Setformula=evaluate_Formula_EF_AF (fsm, Req,Forb,Safe, verbosityLevel );
1256     finalTime = util_cpu_time();
1257     
1258     res_0=mdd_and(Init, Setformula, 1, 1);
1259     res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
1260 
1261     get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1262     EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1263     EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1264     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1265          "  --Error states satisfying F                                        = ", 
1266          nbst,percent);
1267   
1268     get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1269     EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1270     EpdDivide2(nbstates, rch);EpdMultiply(nbstates,100);  EpdGetString(nbstates, percent);
1271     (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n", 
1272          "  --Error states originaly reachable by the design and satisfying F  = ", 
1273          nbst,percent);
1274 
1275     (void) fprintf(vis_stdout, "%-50s%15g\n",               
1276          "  Analysis time                                                      = ", 
1277          (double)(finalTime-initialTime)/1000.0);
1278    }
1279  /*
1280   (void) fprintf(vis_stdout,"********************************\n");     
1281   (void) fprintf(vis_stdout,
1282                  "Dealing with F = A[!forbiden U Required & E[!forbiden U Safe]] \n");
1283   initialTime = util_cpu_time();
1284   Setformula=evaluate_Formula_AF_EF (fsm, Req,Forb,Safe, verbosityLevel );
1285   finalTime = util_cpu_time();
1286
1287   res_0=mdd_and(Init, Setformula, 1, 1);
1288   res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
1289   
1290   get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1291   EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1292   EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1293   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n",
1294                  "  --Error states satisfying F                                        = ",
1295                  nbst,percent);
1296
1297   get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1298   EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1299   EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1300   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n",
1301                  "  --Error states originaly reachable by the design and satisfying F  = ",
1302                  nbst,percent);
1303 
1304 
1305   (void) fprintf(vis_stdout, "%-50s%15g\n",
1306                  "  Analysis time                                                      = ",
1307                  (double)(finalTime-initialTime)/1000.0);
1308   
1309   (void) fprintf(vis_stdout,"*******************************\n");     
1310   (void) fprintf(vis_stdout,
1311                  "Dealing with F = E[!forbiden U Required & E[!forbiden U Safe]] \n");
1312   initialTime = util_cpu_time();
1313   Setformula=evaluate_Formula_EF_EF (fsm, Req,Forb,Safe, verbosityLevel );
1314   finalTime = util_cpu_time();
1315
1316   res_0=mdd_and(Init, Setformula, 1, 1);
1317   res_r=mdd_and(Orig,Setformula, 1, 1); mdd_free(Setformula);
1318
1319   get_number_of_states(fsm, res_0, nbstates); mdd_free(res_0);
1320   EpdGetString(nbstates, nbst);EpdCopy(error0, err);  EpdSubtract2(err, nbstates);
1321   EpdDivide2(nbstates,error0); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1322   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n",
1323                  "  --Error states satisfying F                                        = ",
1324                  nbst,percent);
1325
1326   get_number_of_states(fsm, res_r, nbstates); mdd_free(res_r);
1327   EpdGetString(nbstates, nbst); EpdCopy(rch, err);  EpdSubtract2(err, nbstates);
1328   EpdDivide2(nbstates, rch); EpdMultiply(nbstates,100); EpdGetString(nbstates, percent);
1329   (void) fprintf(vis_stdout, "%-50s%15s (Ratio: %s\%)\n",
1330                  "  --Error states originaly reachable by the design and satisfying F  = ",
1331                  nbst,percent);
1332 
1333 
1334   (void) fprintf(vis_stdout, "%-50s%15g\n",               
1335                  "  Analysis time                                                      = ",
1336                  (double)(finalTime-initialTime)/1000.0);
1337   */
1338   mdd_free(Forb);
1339   mdd_free(Req);
1340   mdd_free(Safe); 
1341   mdd_free(Init);
1342   mdd_free(Orig);
1343   
1344   alarm(0);
1345   return (0);
1346   
1347 
1348   return 1;
1349}
1350
1351
1352// (Adpateted) Bounded model checking
1353// command for robustness properties.
1354static int
1355CommandBmcRob( Hrc_Manager_t ** hmgr,
1356               int             argc,
1357               char          ** argv){
1358  Ntk_Network_t     *network;
1359  BmcOption_t       *options;
1360  int               i;
1361  array_t           *formulaArray;
1362  array_t           *LTLformulaArray;
1363  bAig_Manager_t    *manager;
1364  array_t           *constraintArray = NIL(array_t);
1365 
1366/* Virer dans un premier temps par Denis, seule les techniques non-sat sont intégrées
1367   dans cette version.
1368*/
1369
1370
1371  // Parse command line options.
1372  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
1373      return 1;
1374  }
1375 
1376  // Read the network
1377  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1378  if (network == NIL(Ntk_Network_t)) {
1379    (void) fprintf(vis_stdout, "** bmc_rob error: No network\n");
1380    BmcOptionFree(options);
1381    return 1;
1382  }
1383
1384  manager = Ntk_NetworkReadMAigManager(network);
1385  if (manager == NIL(mAig_Manager_t)) {
1386    (void) fprintf(vis_stdout, 
1387                   "** bmc_rob error: run build_partition_maigs command first\n");
1388    BmcOptionFree(options);
1389    return 1;
1390  }
1391 
1392 
1393  // We need the bdd when building the transition
1394  // relation of the automaton
1395  if(options->inductiveStep !=0){
1396    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
1397 
1398    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
1399    if (designFsm == NIL(Fsm_Fsm_t)) {
1400      return 1;
1401    }
1402  }
1403 
1404  formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
1405  if (formulaArray == NIL(array_t)) {
1406    (void) fprintf(vis_stderr,
1407                   "** bmc error: error in parsing CTL* Fromula from file\n");
1408    BmcOptionFree(options);
1409    return 1;
1410  }
1411
1412  if (array_n(formulaArray) == 0) {
1413    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
1414    BmcOptionFree(options);
1415    Ctlsp_FormulaArrayFree(formulaArray);
1416    return 1;
1417  }
1418  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
1419  Ctlsp_FormulaArrayFree(formulaArray);
1420  if (LTLformulaArray ==  NIL(array_t)){
1421    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
1422    BmcOptionFree(options);
1423    return 1;
1424  }
1425
1426  if (options->fairFile != NIL(FILE)) {
1427    constraintArray = BmcReadFairnessConstraints(options->fairFile);
1428    if(constraintArray == NIL(array_t)){
1429      Ctlsp_FormulaArrayFree(LTLformulaArray);
1430      BmcOptionFree(options);
1431      return 1;
1432    }
1433    if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){
1434      Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray,
1435                                                  constraintArray);
1436      Ctlsp_FormulaArrayFree(constraintArray);
1437      constraintArray = NIL(array_t);
1438    }
1439  }
1440 
1441  //  Call the BMC function.
1442  for (i = 0; i < array_n(LTLformulaArray); i++) { 
1443    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
1444                                                  LTLformulaArray, i);
1445   callBmcRob(network, ltlFormula, constraintArray, options);
1446  }
1447 
1448  //  Free used memeory
1449  if (constraintArray != NIL(array_t)){
1450    Ctlsp_FormulaArrayFree(constraintArray);
1451  }
1452  Ctlsp_FormulaArrayFree(LTLformulaArray);
1453  BmcOptionFree(options);
1454  fflush(vis_stdout);
1455  fflush(vis_stderr);
1456  alarm(0);
1457
1458  return 0;
1459}
1460static int 
1461CommandComposeGolden(Hrc_Manager_t ** hmgr,
1462                   int  argc, char ** argv){
1463        printf("*** Rob3 ***\n");
1464        //Former root
1465        Hrc_Node_t  * rootNode   =  Hrc_ManagerReadRootNode(*hmgr);
1466        if(Hrc_ManagerFindModelByName(*hmgr, "rob3_model") != NIL(Hrc_Model_t))
1467        {
1468                fprintf(vis_stderr, "Composition already made, read a new design\n");
1469                return 1;
1470               
1471        }
1472        //New Root
1473        Hrc_Model_t * newRootModel = Hrc_ModelAlloc(*hmgr, "rob3_model");
1474       
1475        build_golden_faulty_compo(*hmgr,rootNode,newRootModel);
1476
1477  return 0;
1478}
1479static int 
1480CommandProtectGolden(Hrc_Manager_t ** hmgr,
1481                   int  argc, char ** argv)
1482{
1483
1484Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
1485if(rootNode == NIL(Hrc_Node_t)){
1486        printf("Please build the network first\n");
1487        return 1;
1488}
1489char * name = (char*) malloc(10);
1490sprintf(name,"golden");
1491Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name);
1492if(goldenNode == NIL(Hrc_Node_t)){
1493        printf("Compose the network with a golden name golden first\n");
1494        return 1;
1495}
1496
1497FILE * oFile =  Cmd_FileOpen("protect_golden.reg","w", NIL(char *), 0);
1498Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
1499if(fsm == NIL(Fsm_Fsm_t))
1500  return 1;
1501array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
1502mdd_manager     *mddManager = Fsm_FsmReadMddManager(fsm);
1503int nbLatches = 0;
1504int k;
1505int arrSize = array_n( psVarsArray );
1506  for ( k = 0 ; k < arrSize ; k++ ) {
1507    int      mddId = array_fetch( int, psVarsArray,k);
1508    mvar_type mVar = array_fetch(mvar_type, 
1509                                 mdd_ret_mvar_list(mddManager),mddId);
1510                if(strstr(mVar.name,"faulty") == NULL){
1511                        fprintf(oFile,"%s\n",mVar.name);
1512                        nbLatches++;
1513                }
1514        }
1515        st_generator * gen;
1516    Hrc_Latch_t * latch;       
1517        Hrc_NodeForEachLatch(rootNode, gen,name,latch){
1518                fprintf(oFile,"%s\n",name);
1519         }
1520         
1521/*
1522nbLatches += Hrc_NodeReadNumLatches(rootNode);
1523
1524        int i;
1525        Var_Variable_t * var;
1526        Hrc_NodeForEachFormalOutput(rootNode,i,var){
1527                fprintf(oFile,"%s\n", Var_VariableReadName(var));
1528         }
1529        nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode);
1530*/
1531         printf("file protect_golden.reg  created (contains %d registers)\n",nbLatches);
1532        fclose(oFile);
1533        return 0;
1534       
1535}
1536
1537static int 
1538CommandProtectOutput(Hrc_Manager_t ** hmgr,
1539                   int  argc, char ** argv){
1540        Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
1541        if(rootNode == NIL(Hrc_Node_t)){
1542                printf("Please build the network first\n");
1543                return 1;
1544        }
1545        FILE * oFile =  Cmd_FileOpen("protect_output.reg","w", NIL(char *), 0);
1546        int nbLatches = 0;
1547        int i;
1548        Var_Variable_t * var;
1549        Hrc_NodeForEachFormalOutput(rootNode,i,var){
1550                fprintf(oFile,"%s\n", Var_VariableReadName(var));
1551         }
1552        nbLatches += Hrc_NodeReadNumFormalOutputs(rootNode);
1553         printf("file protect_output  created (contains %d signals)\n",nbLatches);
1554        fclose(oFile);
1555        return 0;
1556       
1557}
1558static int 
1559CommandProtectRegister(Hrc_Manager_t ** hmgr,
1560                   int  argc, char ** argv){
1561        Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
1562        if(rootNode == NIL(Hrc_Node_t)){
1563                printf("Please build the network first");
1564                return 1;
1565        }
1566
1567        FILE * oFile =  Cmd_FileOpen("register.reg","w", NIL(char *), 0);
1568
1569        int nbLatches = generateProtectFile(rootNode, oFile,""); 
1570        char * name;
1571        st_generator * gen;
1572    Hrc_Latch_t * latch;       
1573         
1574        nbLatches += Hrc_NodeReadNumLatches(rootNode);
1575
1576        printf("file register.reg  created (contains %d registers)\n",nbLatches);
1577        fclose(oFile);
1578        return 0;
1579       
1580}
1581static int 
1582CommandTestRob(Hrc_Manager_t ** hmgr,
1583                   int  argc, char ** argv)
1584{
1585
1586
1587  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
1588  mdd_t      *initialStates = getInitial(fsm);
1589  mdd_manager      *mddManager = Fsm_FsmReadMddManager(fsm);
1590
1591FILE * oFile =  Cmd_FileOpen("init.prop","w", NIL(char *), 0);
1592
1593mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
1594                         initialStates, "INIT",oFile);
1595
1596  array_t * golden = array_alloc(int, 0);
1597  array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
1598  int                  arrSize = array_n( psVarsArray );
1599  int i;
1600  for ( i = 0 ; i < arrSize ; i++ ) {
1601    int      mddId = array_fetch( int, psVarsArray, i );
1602    mvar_type mVar = array_fetch(mvar_type, 
1603                                 mdd_ret_mvar_list(mddManager),mddId);
1604  if(strstr(mVar.name,"golden") !=NULL)
1605  {
1606    printf("-> %s\n",mVar.name);
1607    array_insert_last(int,golden,mddId);
1608  }
1609}
1610
1611mdd_print_array (golden);
1612mdd_t * tmp1 = mdd_cproject(mddManager,initialStates,golden);
1613mdd_FunctionPrintMain(Fsm_FsmReadMddManager(fsm),
1614                         tmp1, "GOLDEN",oFile);
1615   fclose(oFile);                     
1616  return 0;
1617
1618}
1619
Note: See TracBrowser for help on using the repository browser.