source: vis_dev/vis-2.3/src/io/ioWriteSmv.c @ 20

Last change on this file since 20 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 7.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ioWriteSmv.c]
4
5  PackageName [io]
6
7  Synopsis    [Writes out an Smv file.]
8
9  Description [Write the current model to a file compatible with NuSMV v2.1]
10
11  Author      [Daniel Sheridan, Chao Wang]
12
13  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado. All
14  rights reserved.
15
16  Permission is hereby granted, without written agreement and without license
17  or royalty fees, to use, copy, modify, and distribute this software and its
18  documentation for any purpose, provided that the above copyright notice and
19  the following two paragraphs appear in all copies of this software.]
20
21******************************************************************************/
22
23#include "ioInt.h"
24
25/*---------------------------------------------------------------------------*/
26/* Constant declarations                                                     */
27/*---------------------------------------------------------------------------*/
28
29
30/*---------------------------------------------------------------------------*/
31/* Type declarations                                                         */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Stucture declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Variable declarations                                                     */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Macro declarations                                                        */
47/*---------------------------------------------------------------------------*/
48
49
50/**AutomaticStart*************************************************************/
51
52/*---------------------------------------------------------------------------*/
53/* Static function prototypes                                                */
54/*---------------------------------------------------------------------------*/
55
56
57/**AutomaticEnd***************************************************************/
58
59
60/*---------------------------------------------------------------------------*/
61/* Definition of exported functions                                          */
62/*---------------------------------------------------------------------------*/
63
64
65/**Function********************************************************************
66
67  Synopsis    [Prints out variable name, cleaned for NuSMV]
68
69  Description []
70
71  SideEffects []
72
73  SeeAlso     []
74
75******************************************************************************/
76void
77Io_SmvPrintVar(
78  FILE *fp,
79  Var_Variable_t *var)
80{
81  char * varname = Var_VariableReadName(var);
82  int i;
83
84  for(i=0; varname[i]; i++) {
85    if(varname[i] == '<' || 
86       varname[i] == '>' || 
87       varname[i] == '*' || 
88       varname[i] == '$') {
89      fputc('_', fp);
90    } else {
91      fputc(varname[i], fp);
92    }
93  }
94}
95
96/*---------------------------------------------------------------------------*/
97/* Definition of internal functions                                          */
98/*---------------------------------------------------------------------------*/
99
100
101/**Function********************************************************************
102
103  Synopsis    [The top-level routine for writing out an NuSMV file.]
104
105  Description [The top-level routine for writing out an NuSMV file.
106  The user has to check if the hmgr has a hierarchy read in before
107  calling this procedure.]
108
109  SideEffects []
110
111  SeeAlso     []
112
113******************************************************************************/
114void
115IoSmvWrite(
116  FILE *fp,
117  Hrc_Manager_t *hmgr)
118{ 
119  char *rootModelName;
120  Hrc_Model_t *model, *rootModel;
121  Hrc_Node_t *currentNode;
122  array_t *models;
123  int i;
124  boolean isRootModel;
125  char *rootInstanceName, *instanceName;
126 
127  currentNode = Hrc_ManagerReadCurrentNode(hmgr);
128  models = Hrc_ManagerObtainComponentModels(hmgr);
129
130  rootModelName = Hrc_NodeReadModelName(currentNode);
131  rootModel = Hrc_ManagerFindModelByName(hmgr,rootModelName);
132  rootInstanceName = Hrc_NodeReadInstanceName(currentNode);
133  assert(rootModel != NIL(Hrc_Model_t));
134 
135  for (i=0; i < array_n(models); i++){
136    model = array_fetch(Hrc_Model_t *,models,i);
137    isRootModel = (model == rootModel) ? TRUE : FALSE;
138    instanceName = (isRootModel == TRUE) ? rootInstanceName : NIL(char);
139    Hrc_ModelWriteSmv(fp,model,isRootModel,instanceName);
140  } 
141
142  array_free(models);
143}
144
145/**Function********************************************************************
146
147  Synopsis    [Prints out VAR declaration for a given variable.]
148
149  Description [Prints out VAR declaration for a given variable.]
150
151  SideEffects []
152
153  SeeAlso     []
154
155******************************************************************************/
156void
157IoSmvPrint(
158  FILE *fp,
159  Var_Variable_t *var)
160{
161  int is_enum, range, i;
162
163  is_enum = Var_VariableTestIsEnumerative(var);
164  range = Var_VariableReadNumValues(var);
165   
166  if (is_enum == 1){
167    if (range == 2){
168      (void)fprintf(fp,"VAR %s : boolean;\n",Var_VariableReadName(var));
169    }
170    else {
171      (void)fprintf(fp,"VAR %s : 0..%d;\n",Var_VariableReadName(var),range-1);
172    }
173  }
174  else {
175  /* variable var is symbolic */
176    (void)fprintf(fp,"VAR %s : {",Var_VariableReadName(var));
177    for (i=0; i < range; i++){
178      if (i == (range-1))
179        (void)fprintf(fp,"%s ",Var_VariableReadSymbolicValueFromIndex(var,i));
180      else
181        (void)fprintf(fp,"%s, ",Var_VariableReadSymbolicValueFromIndex(var,i));
182    }
183    (void)fprintf(fp,"};\n");
184  }
185}
186
187/**Function********************************************************************
188
189  Synopsis    [Prints out VAR declaration for a given variable, with the
190               special string "_bufin" appended to the variable name.]
191
192  Description [Prints out VAR declaration for a given variable.]
193
194  SideEffects []
195
196  SeeAlso     []
197
198******************************************************************************/
199void
200IoSmvPrintSpecial(
201  FILE *fp,
202  Var_Variable_t *var)
203{
204  int is_enum, range, i;
205
206  is_enum = Var_VariableTestIsEnumerative(var);
207  range = Var_VariableReadNumValues(var);
208   
209  if (is_enum == 1){
210    if (range == 2){
211      (void)fprintf(fp,"VAR %s_bufin : boolean;\n",Var_VariableReadName(var));
212    }
213    else {
214      (void)fprintf(fp,"VAR %s_bufin : 0..%d;\n",Var_VariableReadName(var),
215                    range-1);
216    }
217  }
218  else {
219  /* variable var is symbolic */
220    (void)fprintf(fp,"VAR %s_bufin : {",Var_VariableReadName(var));
221    for (i=0; i < range; i++){
222      if (i == (range-1)) 
223        (void)fprintf(fp,"%s_bufin ",
224                      Var_VariableReadSymbolicValueFromIndex(var,i));
225      else
226        (void)fprintf(fp,"%s_bufin, ",
227                      Var_VariableReadSymbolicValueFromIndex(var,i));
228    }
229    (void)fprintf(fp,"};\n");
230  }
231}
Note: See TracBrowser for help on using the repository browser.