1 | /**CHeaderFile***************************************************************** |
---|
2 | |
---|
3 | FileName [mark.h] |
---|
4 | |
---|
5 | PackageName [mark] |
---|
6 | |
---|
7 | Synopsis [Data structures used in Markovian analysis.] |
---|
8 | |
---|
9 | Description [Data structures used in Markovian analysis.] |
---|
10 | |
---|
11 | SeeAlso [markInt.h] |
---|
12 | |
---|
13 | Author [Balakrishna Kumthekar] |
---|
14 | |
---|
15 | Copyright [This file was created at the University of Colorado at |
---|
16 | Boulder. The University of Colorado at Boulder makes no warranty |
---|
17 | about the suitability of this software for any purpose. It is |
---|
18 | presented on an AS IS basis.] |
---|
19 | |
---|
20 | ******************************************************************************/ |
---|
21 | #ifndef _MARK |
---|
22 | #define _MARK |
---|
23 | |
---|
24 | #include "fsm.h" |
---|
25 | #include "util.h" |
---|
26 | #include "st.h" |
---|
27 | #include "bdd.h" |
---|
28 | |
---|
29 | /*---------------------------------------------------------------------------*/ |
---|
30 | /* Constant declarations */ |
---|
31 | /*---------------------------------------------------------------------------*/ |
---|
32 | |
---|
33 | |
---|
34 | /*---------------------------------------------------------------------------*/ |
---|
35 | /* Type declarations */ |
---|
36 | /*---------------------------------------------------------------------------*/ |
---|
37 | |
---|
38 | |
---|
39 | /*---------------------------------------------------------------------------*/ |
---|
40 | /* Structure declarations */ |
---|
41 | /*---------------------------------------------------------------------------*/ |
---|
42 | |
---|
43 | /**Enum************************************************************************ |
---|
44 | |
---|
45 | Synopsis [Different methods of solving for steady state probabilities. |
---|
46 | For more details consult |
---|
47 | |
---|
48 | G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis |
---|
49 | of Large Finite State Machines", IEEE Trans. on CAD, December 1996. ] |
---|
50 | |
---|
51 | SeeAlso [Mark_StartMethod] |
---|
52 | |
---|
53 | ******************************************************************************/ |
---|
54 | typedef enum { |
---|
55 | Solve_Default_c, /* Default method. It is Solve_FPMethod_c. */ |
---|
56 | Solve_GenMethod_c, |
---|
57 | Solve_FPMethod_c, /* This is the only one that is currently supported */ |
---|
58 | Solve_CKMethod_c |
---|
59 | } Mark_SolveMethod; |
---|
60 | |
---|
61 | |
---|
62 | /**Enum************************************************************************ |
---|
63 | |
---|
64 | Synopsis [Different methods of chosing the reset state. For more details |
---|
65 | consult |
---|
66 | |
---|
67 | G. D. Hachtel, E. Macii, A. Pardo and F. Somenzi, "Markovian Analysis |
---|
68 | of Large Finite State Machines", IEEE Trans. on CAD, December 1996.] |
---|
69 | |
---|
70 | SeeAlso [Markov_SolveMethod] |
---|
71 | |
---|
72 | ******************************************************************************/ |
---|
73 | typedef enum { |
---|
74 | Start_Default_c, /* Default method. It is Start_Reset_c. */ |
---|
75 | Start_Reset_c, |
---|
76 | Start_EquiProb_c |
---|
77 | } Mark_StartMethod; |
---|
78 | |
---|
79 | /*---------------------------------------------------------------------------*/ |
---|
80 | /* Variable declarations */ |
---|
81 | /*---------------------------------------------------------------------------*/ |
---|
82 | |
---|
83 | |
---|
84 | /*---------------------------------------------------------------------------*/ |
---|
85 | /* Macro declarations */ |
---|
86 | /*---------------------------------------------------------------------------*/ |
---|
87 | |
---|
88 | /**AutomaticStart*************************************************************/ |
---|
89 | |
---|
90 | /*---------------------------------------------------------------------------*/ |
---|
91 | /* Function prototypes */ |
---|
92 | /*---------------------------------------------------------------------------*/ |
---|
93 | |
---|
94 | EXTERN bdd_node ** Mark_FsmComputeStateProbs(Fsm_Fsm_t *fsm, Mark_SolveMethod solveMethod, Mark_StartMethod startMethod, st_table *inputProb, int roundOff); |
---|
95 | EXTERN bdd_node ** Mark_ComputeStateProbsWithTr(bdd_manager *ddManager, bdd_node *TR, bdd_node *reachable, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **zVars, st_table *inputProb, int nVars, int nPi, int roundOff, Mark_SolveMethod method, Mark_StartMethod start); |
---|
96 | EXTERN bdd_node * Mark_addInProb(bdd_manager *manager, bdd_node *tr, bdd_node *cube, st_table *probTable); |
---|
97 | EXTERN void Mark_Init(void); |
---|
98 | EXTERN void Mark_End(void); |
---|
99 | |
---|
100 | /**AutomaticEnd***************************************************************/ |
---|
101 | |
---|
102 | #endif /* _MARK */ |
---|