source: vis_dev/vis-2.3/src/rob/Robust.h @ 23

Last change on this file since 23 was 21, checked in by cecile, 13 years ago

un delete de trop

File size: 4.6 KB
Line 
1/**HFile***********************************************************************
2
3  FileName    [Robust.h]
4
5  PackageName [rob]
6
7  Synopsis    [Headers and strcutus for Robustness package.]
8
9  Author      [Souheib Baarir, Denis Poitrenaud,J.M Ilié ]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. 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 PARIS VI 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 CALIFORNIA 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
32
33
34#ifndef _ROB_H
35#define _ROB_H
36#include "../ntk/ntkInt.h"
37#include "../hrc/hrcInt.h"
38#include "../fsm/fsmInt.h"
39#include "../bmc/bmcInt.h"
40#include "../sat/sat.h"
41#include "../sat/satInt.h"
42
43typedef enum{ 
44  ecmd,
45  eofile,
46  earg,
47  enfile,
48  eicmd,
49  eiofile,
50  ercmd
51} type_err;
52
53// fonctions divers
54void     get_number_of_states     (Fsm_Fsm_t  *fsm, mdd_t* b, EpDouble* ep);
55array_t* determine_non_protected_registers(Fsm_Fsm_t  *fsm, FILE *f);
56mdd_t*   compute_error_states     (Fsm_Fsm_t  *fsm, mdd_t* reachable,
57                                   int verbosityLevel, int printStep,  FILE* protect);
58mdd_t*   error_states_us_ut(Fsm_Fsm_t  *fsm, mdd_t* reachable,FILE* protect);
59mdd_t* error_states_us_mt(Fsm_Fsm_t  *fsm, mdd_t *S,  FILE *protect);
60mdd_t* error_states_ms_ut(Fsm_Fsm_t  *fsm, mdd_t *S,  FILE *protect);                 
61mdd_t* error_states_ms_mt(Fsm_Fsm_t  *fsm, mdd_t* S0,mdd_t *S,  FILE *protect)
62;
63void     compute_fair             (Fsm_Fsm_t  *fsm,int  verbosityLevel);
64Hrc_Node_t  * build_golden_faulty_compo(Hrc_Manager_t * hmgr,Hrc_Node_t  * rootNode,    Hrc_Model_t * newRootModel);
65
66
67int generateProtectFile(Hrc_Node_t * goldenNode, FILE *oFile,char *
68instanceName);
69
70// fonction d'évaluation de formules CTL
71mdd_t*   evaluate_EF              (Fsm_Fsm_t  *fsm, mdd_t *target,
72                                   mdd_t* fairS, int verbosityLevel);
73mdd_t*   evaluate_EG              (Fsm_Fsm_t  *fsm, mdd_t *invariant,
74                                   mdd_t* fairS,Fsm_Fairness_t * fairCond, 
75                                   int verbosityLevel);
76mdd_t*   evaluate_EU              (Fsm_Fsm_t  *fsm, mdd_t* inv, 
77                                   mdd_t *target,mdd_t* fairS, 
78                                   int verbosityLevel);
79mdd_t*   evaluate_AU              (Fsm_Fsm_t  *fsm, mdd_t* inv, 
80                                   mdd_t *target, mdd_t* fairS,
81                                   Fsm_Fairness_t * fairCond, 
82                                   int verbosityLevel);
83mdd_t*   evaluate                 (Fsm_Fsm_t  *fsm,FILE* ctlfile,
84                                   mdd_t* fairS,
85                                   Fsm_Fairness_t * fairCond, 
86                                   int verbosityLevel);
87mdd_t*  evaluate_Formula_AF_AF    (Fsm_Fsm_t  *fsm, mdd_t* Req,
88                                   mdd_t* forb,mdd_t* Safe,
89                                   int  verbosityLevel );
90mdd_t*  evaluate_Formula_AF_EF    (Fsm_Fsm_t  *fsm, mdd_t* Req,
91                                   mdd_t* forb,mdd_t* Safe,
92                                   int  verbosityLevel );
93mdd_t*  evaluate_Formula_EF_AF    (Fsm_Fsm_t  *fsm, mdd_t* Req,
94                                   mdd_t* forb,mdd_t* Safe,
95                                   int  verbosityLevel );
96mdd_t*  evaluate_Formula_EF_EF    (Fsm_Fsm_t  *fsm, mdd_t* Req,
97                                   mdd_t* forb,mdd_t* Safe,
98                                   int  verbosityLevel );
99void    callBmcRob                ( Ntk_Network_t   *network,
100                                    Ctlsp_Formula_t *ltlFormula,
101                                    array_t         *constraintArray,
102                                    BmcOption_t     *options);
103
104// fonctions d'acces
105mdd_t*   getForbidden              (Fsm_Fsm_t  *fsm);
106mdd_t*   getRequired               (Fsm_Fsm_t  *fsm);
107mdd_t*   getSafe                   (Fsm_Fsm_t  *fsm);
108mdd_t*   getInitial                (Fsm_Fsm_t  *fsm);
109mdd_t*   getReach                  (Fsm_Fsm_t  *fsm);
110mdd_t*   getReachOrg               (Fsm_Fsm_t  *fsm );
111
112// fonction d'affichage
113void     print_number_of_states   (char* msg, Fsm_Fsm_t  *fsm, mdd_t* b);
114void     print_variables_info     (Fsm_Fsm_t  *fsm);
115void     error_msg                (FILE* f, char* t, type_err e);
116void     conv_error_msg           (FILE* f, char* cmd, type_err e);
117void     mdd_FunctionPrintMain    (mdd_manager *mgr ,mdd_t *  top, 
118                                   char * macro_name, FILE * f);
119
120#endif /* _ROB_H */
Note: See TracBrowser for help on using the repository browser.