← Back to branch summary

~ubuntu-branches/ubuntu/intrepid/tcm/intrepid

« back to all changes in this revision

Viewing changes to src/sd/bv/smv.c

  • Committer: Bazaar Package Importer
  • Author(s): Otavio Salvador
  • Date: 2003-07-03 20:08:21 UTC
  • Revision ID: james.westby@ubuntu.com-20030703200821-se4xtqx25e5miczi
Tags: upstream-2.20
Import upstream version 2.20

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/sd/bv/smv.c
 
1
/* This file generates quick-and-dirty NuSMV output */
 
2
 
 
3
#include "smv.h"
 
4
#include "transition.h"
 
5
#include "initialstate.h"
 
6
#include "util.h"
 
7
#include <ctype.h>
 
8
#include <stdio.h>
 
9
#include <string.h>
 
10
 
 
11
SMV::SMV(Graph *st) {
 
12
        graph = st;
 
13
}
 
14
 
 
15
 
 
16
SMV::~SMV() {
 
17
}
 
18
 
 
19
 
 
20
void SMV::WriteSMV(const char *filename, List<string> *internal,
 
21
                        const string *formula) {
 
22
        /* Generate the data structure needed for conversion to SMV format
 
23
           and write it to disk. */
 
24
        FILE *fp;
 
25
 
 
26
        fp = fopen(filename, "w");
 
27
        if ( ! fp )
 
28
                return /* False */;
 
29
        fprintf(fp, "MODULE main\n\nVAR\n-- state variables\n\tI___INITIAL : boolean ;\n");
 
30
 
 
31
        /* for every state, there is a variable state_<number> */
 
32
        List<Subject *> states;
 
33
        List<string> names;
 
34
        graph->GetNodes(&states, Code::INITIAL_STATE);
 
35
        graph->GetNodes(&states, Code::STATE);
 
36
        graph->GetNodes(&states, Code::DECISION_POINT);
 
37
        for ( states.first() ; ! states.done() ; states.next() ) {
 
38
                fprintf(fp, "\tstate_%d : boolean ;\n", states.cur()->GetId());
 
39
                AddNames(&names, NULL, states.cur()->GetName());
 
40
        }
 
41
 
 
42
        fprintf(fp, "-- event variables\n");
 
43
        /* for every event, there is a variable ev_<name> */
 
44
        List<Subject *>trans;
 
45
        List<string> evnames, externevnames;
 
46
        graph->GetEdges(&trans, Code::TRANSITION);
 
47
 
 
48
        for ( trans.first() ; ! trans.done() ; trans.next() ) {
 
49
                Transition *tr = dynamic_cast<Transition *>(trans.cur());
 
50
                if ( ! check(tr) )
 
51
                        continue;
 
52
                AddNames(&evnames, NULL, tr->GetEvent());
 
53
                AddNames(&externevnames, NULL, tr->GetEvent());
 
54
                for ( int i = tr->NrActions() ; i-- > 0 ; ) {
 
55
                        const string *act = tr->GetAction(i);
 
56
                        if ( evnames.find(*act) < 0 )
 
57
                                evnames.add(*act);
 
58
                }
 
59
        }
 
60
        for ( evnames.first() ; ! evnames.done() ; evnames.next() ) {
 
61
                fprintf(fp, "\tev_%s : boolean ;\n", evnames.cur().getstr());
 
62
                if ( externevnames.find(evnames.cur()) < 0 )
 
63
                        internal->add(evnames.cur());
 
64
        }
 
65
        externevnames.empty();
 
66
 
 
67
        /* The initial state: I___INITIAL is true, all other states and events
 
68
           are false */
 
69
        fprintf(fp, "INIT\n\tI___INITIAL");
 
70
        for ( states.first() ; ! states.done() ; states.next() )
 
71
                fprintf(fp, "\n\t& ! state_%d", states.cur()->GetId());
 
72
        for ( evnames.first() ; ! evnames.done() ; evnames.next() )
 
73
                fprintf(fp, "\n\t& ! ev_%s", evnames.cur().getstr());
 
74
        fprintf(fp, "\n");
 
75
 
 
76
        /* definition of propositional symbols as disjunctions of states */
 
77
        fprintf(fp, "DEFINE\n");
 
78
        for ( names.first() ; ! names.done() ; names.next() ) {
 
79
                string *name = &(names.cur());
 
80
                fprintf(fp, "\t%s := FALSE", names.cur().getstr() );
 
81
                for ( states.first() ; ! states.done() ; states.next() ) {
 
82
                        const string *n = states.cur()->GetName();
 
83
                        const char *found = strstr(n->getstr(), name->getstr());
 
84
                        if ( found && (n->getstr() == found
 
85
                                            || isspace(found[-1]))
 
86
                                        && ('\0' == found[name->length()]
 
87
                                            || isspace(found[name->length()])) )
 
88
                                fprintf(fp,"\n\t\t| state_%d",
 
89
                                        states.cur()->GetId());
 
90
 
 
91
                }
 
92
                fprintf(fp, " ;\n");
 
93
        }
 
94
        names.empty();
 
95
 
 
96
        /* definition of transition enabledness as conditions on source state */
 
97
        for ( trans.first() ; ! trans.done() ; trans.next() ) {
 
98
                Transition *tr = dynamic_cast<Transition *>(trans.cur());
 
99
                if ( ! check(tr) )
 
100
                        continue;
 
101
                fprintf(fp, "\ttrans_%d_enabled := state_%d", tr->GetId(),
 
102
                                        tr->GetSubject1()->GetId());
 
103
                List<string> events, guards;
 
104
                AddNames(&events, &guards, tr->GetEvent());
 
105
                for ( events.first() ; ! events.done() ; events.next() )
 
106
                        fprintf(fp, "\n\t\t& ev_%s", events.cur().getstr());
 
107
                events.empty();
 
108
                for ( guards.first() ; ! guards.done() ; guards.next() )
 
109
                        fprintf(fp, "\n\t\t& %s", guards.cur().getstr());
 
110
                guards.empty();
 
111
                fprintf(fp, " ;\n");
 
112
                fprintf(fp, "\ttrans_%d_taken := trans_%d_enabled\n"
 
113
                                        "\t\t& next(state_%d)",
 
114
                                        tr->GetId(), tr->GetId(),
 
115
                                        tr->GetSubject2()->GetId());
 
116
                if ( tr->GetSubject1() != tr->GetSubject2() )
 
117
                        fprintf(fp, "\n\t\t& next(! state_%d)",
 
118
                                                tr->GetSubject1()->GetId());
 
119
 
 
120
                for ( int i = tr->NrActions() ; i-- > 0 ; )
 
121
                        fprintf(fp, "\n\t\t& next(ev_%s)",
 
122
                                                tr->GetAction(i)->getstr());
 
123
                fprintf(fp, " ;\n");
 
124
        }
 
125
 
 
126
        /* definition of initial transition */
 
127
        fprintf(fp, "\tinit_enabled := I___INITIAL ;\n\tinit_taken := init_enabled");
 
128
        for ( states.first() ; ! states.done() && Code::INITIAL_STATE == states.cur()->GetClassType() ; states.next() ) {
 
129
                InitialState *is = dynamic_cast<InitialState *>(states.cur());
 
130
                if ( ! check(is) )
 
131
                        continue;
 
132
                fprintf(fp, "\n\t\t& next(state_%d)", states.cur()->GetId());
 
133
                for ( int i = is->NrActions() ; i-- > 0 ; )
 
134
                        fprintf(fp, "\n\t\t& next(ev_%s)", is->GetAction(i));
 
135
        }
 
136
        fprintf(fp, " ;\n");
 
137
 
 
138
        /* definition of stable state
 
139
           (For a step semantics, change this definition to: stable := 1 ; */
 
140
        fprintf(fp,"\tstable := ! init_enabled");
 
141
        for ( trans.first() ; ! trans.done() ; trans.next() )
 
142
                fprintf(fp,"\n\t\t& ! trans_%d_enabled", trans.cur()->GetId());
 
143
        fprintf(fp, " ;\n");
 
144
 
 
145
        /* definition of the transition relation */
 
146
        fprintf(fp, "\nTRANS\n\tnext(! I___INITIAL)\n");
 
147
 
 
148
        /* if a transition is enabled, it is taken -- unless a conflicting
 
149
           transition is taken */
 
150
        for ( trans.first() ; ! trans.done() ; trans.next() ) {
 
151
                Transition *tr = dynamic_cast<Transition *>(trans.cur());
 
152
                if ( ! check(tr) )
 
153
                        continue;
 
154
                fprintf(fp, "\t& (trans_%d_enabled -> (trans_%d_taken",
 
155
                                        tr->GetId(), tr->GetId());
 
156
                List<Subject *> conflict;
 
157
                graph->GetEdgesFrom(&conflict, tr->GetSubject1(),
 
158
                                        Code::TRANSITION);
 
159
                conflict.first();
 
160
                if ( ! conflict.done() && (tr != conflict.cur()
 
161
                                                || (conflict.next(),
 
162
                                                ! conflict.done())) ) {
 
163
                        fprintf(fp, " <-> ");
 
164
                        for ( ;; ) {
 
165
                                fprintf(fp, "! trans_%d_taken",
 
166
                                                conflict.cur()->GetId());
 
167
                                conflict.next();
 
168
                                if ( conflict.done() || (tr == conflict.cur()
 
169
                                                        && (conflict.next(),
 
170
                                                        conflict.done())) )
 
171
                                        break;
 
172
                                fprintf(fp, " & ");
 
173
                        }
 
174
                }
 
175
                conflict.empty();
 
176
                fprintf(fp, "))\n");
 
177
        }
 
178
        fprintf(fp, "\t& (init_enabled -> init_taken)\n");
 
179
 
 
180
        /* states only change by taking an edge */
 
181
        for ( states.first() ; ! states.done() ; states.next() ) {
 
182
                List<Subject *> edges;
 
183
                graph->GetEdgesFrom(&edges, states.cur(), Code::TRANSITION);
 
184
                graph->GetEdgesTo(&edges, states.cur(), Code::TRANSITION);
 
185
                fprintf(fp, "\t& (state_%d = next(state_%d)",
 
186
                                        states.cur()->GetId(),
 
187
                                        states.cur()->GetId());
 
188
                for ( edges.first() ; ! edges.done() ; edges.next() )
 
189
                        fprintf(fp, " | trans_%d_taken", edges.cur()->GetId());
 
190
                if ( Code::INITIAL_STATE == states.cur()->GetClassType() )
 
191
                        fprintf(fp, " | init_taken");
 
192
                fprintf(fp, ")\n");
 
193
        }
 
194
        states.empty();
 
195
 
 
196
        /* internal events only happen when specific transitions are taken */
 
197
        /* other events only happen when specific transitions are taken or the
 
198
           state is stable. */
 
199
        for ( evnames.first() ; ! evnames.done() ; evnames.next() ) {
 
200
                string *ev = &(evnames.cur());
 
201
                fprintf(fp, "\t& (next(! ev_%s)", ev->getstr());
 
202
                for ( trans.first() ; ! trans.done() ; trans.next() ) {
 
203
                        Transition *tr =
 
204
                                dynamic_cast<Transition *>(trans.cur());
 
205
                        if ( ! check(tr) )
 
206
                                continue;
 
207
                        if ( tr->HasAction(ev) )
 
208
                                fprintf(fp, " | trans_%d_taken", tr->GetId());
 
209
                }
 
210
                if ( ! internal->contains(*ev) )
 
211
                        fprintf(fp, " | stable");
 
212
                fprintf(fp, ")\n");
 
213
        }
 
214
        trans.empty();
 
215
 
 
216
        /* timeouts must happen infinitely often */
 
217
        fprintf(fp, "\nFAIRNESS\n\tev_timeout\n");
 
218
 
 
219
        /* a timeout never happens at the same time as another event */
 
220
        evnames.first();
 
221
        if ( ! evnames.done() && ("timeout" != evnames.cur()
 
222
                                || (evnames.next(), ! evnames.done())) ) {
 
223
                fprintf(fp, "\nINVAR\n\t");
 
224
                for ( ;; ) {
 
225
                                fprintf(fp, "ev_%s", evnames.cur().getstr());
 
226
                        evnames.next();
 
227
                        if ( evnames.done() || ("timeout" == evnames.cur()
 
228
                                                        && (evnames.next(),
 
229
                                                        evnames.done())) )
 
230
                                break;
 
231
                        fprintf(fp, "\n\t| ");
 
232
                }
 
233
                evnames.empty();
 
234
                fprintf(fp, " -> ! ev_timeout\n");
 
235
        }
 
236
 
 
237
        fprintf(fp, "\nSPEC\n\t%s\n", formula->getstr());
 
238
        fclose(fp);
 
239
}
 
240
 
 
241
 
 
242
void SMV::AddNames(List<string> *names, List<string> *guards,
 
243
                                const string *statename) {
 
244
        /* Extracts single words and guards from statename. */
 
245
        const char *cp = statename->getstr();
 
246
        while ( *cp ) {
 
247
                while ( *cp && isspace(*cp) )
 
248
                        ++cp;
 
249
                if ( ! *cp )
 
250
                        break;
 
251
                const char *ep = cp;
 
252
                if ( '[' == *cp ) {
 
253
                        cp++;
 
254
                        while ( *++ep ) {
 
255
                                if ( ']' == *ep ) {
 
256
                                        if ( guards ) {
 
257
                                                string name;
 
258
                                                name.add(cp, ep - cp);
 
259
                                                if ( guards->find(name) < 0 )
 
260
                                                        guards->add(name);
 
261
                                        }
 
262
                                        ++ep;
 
263
                                        break;
 
264
                                }
 
265
                        }
 
266
                } else {
 
267
                        while ( *++ep && ! isspace(*ep) && '[' != *ep )
 
268
                                ;
 
269
                        if ( names ) {
 
270
                                string name;
 
271
                                name.add(cp, ep - cp);
 
272
                                if ( names->find(name) < 0 )
 
273
                                        names->add(name);
 
274
                        }
 
275
                }
 
276
                cp = ep;
 
277
        }
 
278
}