← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/sd/bv/adscks.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/adscks.c
 
1
/////////////////////////////////////////////////////////////////////////////////
 
2
// This file is part of Toolkit for Conceptual Modeling (TCM).
 
3
// (c) copyright 2001, Universiteit Twente.
 
4
// Author: Rik Eshuis (eshuis@cs.utwente.nl).
 
5
//
 
6
// TCM is free software; you can redistribute it and/or modify
 
7
// it under the terms of the GNU General Public License as published by
 
8
// the Free Software Foundation; either version 2 of the License, or
 
9
// (at your option) any later version.
 
10
//
 
11
// TCM is distributed in the hope that it will be useful,
 
12
// but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
// GNU General Public License for more details.
 
15
//
 
16
// You should have received a copy of the GNU General Public License
 
17
// along with TCM; if not, write to the Free Software
 
18
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 
19
// 02111-1307, USA.
 
20
////////////////////////////////////////////////////////////////////////////////
 
21
#include "adsclockmanager.h"
 
22
#include "adscks.h"
 
23
#include "util.h"
 
24
#include "outputfile.h"
 
25
#include "edge.h"
 
26
#include "adsvaluation.h"
 
27
#include "adstransition.h"
 
28
#include "adshypergraph.h"
 
29
#include "adspropertyvaluation.h"
 
30
#include "bag.h"
 
31
 
 
32
ADSCks::ADSCks(ADSHyperGraph *a) : Graph() {
 
33
  am=a;
 
34
}
 
35
 
 
36
ADSCks::~ADSCks() {
 
37
}
 
38
 
 
39
void ADSCks::AddNode(Node *n){
 
40
  Graph::AddNode(n);
 
41
  //    vhl.add((ADSValuation *)n,((ADSValuation *)n)->ComputeKey());
 
42
}
 
43
 
 
44
void ADSCks::AddEdge(Edge *e){
 
45
  Graph::AddEdge(e);
 
46
  //    thl.add((ADSTransition *)e,((ADSTransition *)e)->ComputeKey());
 
47
}
 
48
 
 
49
 
 
50
void ADSCks::WriteSubjects(OutputFile *f) {
 
51
  List <ADSValuation *> cksnodes;
 
52
  GetNodes((List <Subject *> *)&cksnodes);
 
53
  (*f) << "# GRAPH NODES\n\n";
 
54
  for (cksnodes.first(); !cksnodes.done(); cksnodes.next()) {
 
55
    if (check(cksnodes.cur()))
 
56
      cksnodes.cur()->Write(f);
 
57
  }
 
58
  List <ADSTransition *> cksedges;
 
59
  GetEdges((List <Subject *> *)&cksedges);
 
60
  (*f) << "# GRAPH EDGES\n\n";
 
61
  for (cksedges.first(); !cksedges.done(); cksedges.next()) {
 
62
    if (check(cksedges.cur()))
 
63
      cksedges.cur()->Write(f);
 
64
  } 
 
65
}
 
66
 
 
67
 
 
68
 
 
69
bool ADSCks::ExistsSimilarEdge( ADSTransition *e){
 
70
  //    if (thl.isin(e,e->ComputeKey())==NULL) return False;
 
71
  //   return True;
 
72
                      
 
73
  List <ADSTransition *> cksedges;
 
74
  GetEdges((List <Subject *> *)&cksedges);
 
75
  for (cksedges.first(); !cksedges.done(); cksedges.next()){
 
76
    if ((*cksedges.cur())==*e) {
 
77
      return True;
 
78
    }
 
79
  }
 
80
  return False;
 
81
       
 
82
    
 
83
}
 
84
 
 
85
ADSValuation *ADSCks::FindSimilarNode( ADSValuation *s){
 
86
  //    return vhl.isin(s,s->ComputeKey());
 
87
  
 
88
  List <ADSValuation *> cksnodes;
 
89
  GetNodes((List <Subject *> *)&cksnodes);
 
90
  for (cksnodes.first(); !cksnodes.done(); cksnodes.next()){
 
91
    if ((*cksnodes.cur())==*s) {
 
92
      return cksnodes.cur();
 
93
    }
 
94
  }
 
95
  return NULL;
 
96
  
 
97
}
 
98
 
 
99
 
 
100
 
 
101
// procedure to detect unbounded state nodes
 
102
// it is taken from the Karp-Miller algorithm
 
103
// if there exists another valuation s' such that s'->C' < s->C
 
104
// and there is a path from s to s' then
 
105
//  some state node is unbounded
 
106
bool ADSCks::GrowsInfinite(ADSValuation *s, string &str){
 
107
  Bag <Subject *> scfg;
 
108
  s->GetConfig(&scfg);
 
109
  List <ADSValuation *> cksnodes;
 
110
  GetNodes((List <Subject *> *)&cksnodes);
 
111
  for (cksnodes.first(); !cksnodes.done(); cksnodes.next()){
 
112
    Bag <Subject *> cfg;
 
113
    cksnodes.cur()->GetConfig(&cfg);
 
114
    if ((scfg.contains(cfg)) && (!cfg.contains(scfg)) && (PathExists(cksnodes.cur(),s)) ){
 
115
      List <Subject *> l;
 
116
      scfg.GetList(l);
 
117
      for (l.first();!l.done();l.next()){
 
118
        if (scfg.count(l.cur())>cfg.count(l.cur())) str=*(l.cur()->GetName());
 
119
      }
 
120
      return True; // scfg strictly contains cfg and cksnodes.cur() leads to s
 
121
    }
 
122
  }
 
123
  return False;  
 
124
}
 
125
 
 
126
/////
 
127
 
 
128
string replace(string s){
 
129
  string t=s;
 
130
  t.replace("-\r","");
 
131
  t.replace('\r','_');
 
132
  t.replace(' ','_');
 
133
  t.replace('.','_');
 
134
  t.replace('/','_');
 
135
  //  t.replace('(','_');
 
136
  //  t.replace(')','_');
 
137
  t.replace('-','_');
 
138
  t.replace('=','_');
 
139
  t.replace("\"",'_');
 
140
  return t;
 
141
}
 
142
 
 
143
 
 
144
 
 
145
 
 
146
 
 
147
 
 
148
void ADSCks::WriteSMVFile(OutputFile *ofile, bool sf){
 
149
  (*ofile) <<  "MODULE main\n\nVAR\n";
 
150
  List <Subject *> amnodes;
 
151
  am->GetNodes((List <Subject *> *)&amnodes);
 
152
  AssignNumbers();   
 
153
 
 
154
 
 
155
 
 
156
  List <ADSValuation *> cksnodes;
 
157
  GetNodes((List <Subject *> *)&cksnodes);
 
158
  int nodescount=cksnodes.count();
 
159
 
 
160
  (*ofile) << "\tc____counter : 0.." << nodescount-1 << " ;  -- program counter  \n"; // putting the program counter first gives more efficient BDD ordering 
 
161
 
 
162
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
163
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
 
164
    string s=(*(amnodes.cur()->GetName()));
 
165
    s.replace("-\r","");
 
166
    s.replace('\r','_');
 
167
    s.replace(' ','_');
 
168
    if (amnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){ 
 
169
      s="I___INITIAL";amnodes.cur()->SetName(&s);
 
170
    }
 
171
    if (amnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){ 
 
172
      string t = (int)amnodes.cur()->GetId();
 
173
      s="F___FINAL"+t; amnodes.cur()->SetName(&s);
 
174
    }
 
175
    (*ofile ) << "\t"<< replace(s) << " : 0.."<< am->GetBound(amnodes.cur()) <<";\n";
 
176
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
177
      (*ofile ) << "\tT_" << replace(s) << " : 0.."<< am->GetBound(amnodes.cur()) <<";\n";
 
178
    }
 
179
  }
 
180
  List <Prop *> pl;
 
181
  am->GetPropList(pl);
 
182
  for (pl.first();!pl.done();pl.next()){
 
183
     string s=pl.cur()->GetName(); 
 
184
     (*ofile ) << "\t" << replace(s) << " : boolean;\n";    
 
185
  }
 
186
  (*ofile) << "\tstable:boolean;\n";
 
187
 
 
188
 
 
189
  (*ofile) << "INIT\n";
 
190
  (*ofile) << "\tc____counter = 0 & \n "; // because of assign number
 
191
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
192
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
 
193
    string s=(*(amnodes.cur()->GetName()));
 
194
    (*ofile ) << "\t"<< replace(s) << " = " ;
 
195
    (amnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE)? (*ofile) << "1" : (*ofile) << "0" ;
 
196
    (*ofile) << " & \n";
 
197
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
198
      (*ofile ) << "\tT_" << replace(s) << " = 0 & \n";
 
199
    }
 
200
  }
 
201
  for (pl.first();!pl.done();pl.next()){
 
202
    string s=pl.cur()->GetName();
 
203
   (*ofile ) << "\t" << replace(s) << "= 0 & \n";    
 
204
  }
 
205
  
 
206
  (*ofile) << "\tstable= 0 \n\n";
 
207
 
 
208
  (*ofile) << "TRANS\n";
 
209
 
 
210
  // print program counter
 
211
  (*ofile) << "\tnext(c____counter) in\n\t\tcase\n";     
 
212
  for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
213
    (*ofile) << "\t\t\t c____counter = " << cksnodes.cur()->GetNumber() << " : {";
 
214
    List <ADSTransition *> akl;
 
215
    GetEdgesFrom((List <Subject *> *)&akl,cksnodes.cur());
 
216
    akl.first();
 
217
    if (akl.count()==0){
 
218
      (*ofile) << cksnodes.cur()->GetNumber() << "};\n"; // final state is self loop
 
219
    }
 
220
    else{
 
221
      akl.first();
 
222
      (*ofile) << ((ADSValuation *)akl.cur()->GetSubject2())->GetNumber();
 
223
      if (akl.count()==1){
 
224
        (*ofile) << "};\n";
 
225
      }
 
226
      else{
 
227
        akl.next();
 
228
        for (;!akl.done();akl.next()){
 
229
          (*ofile) << "," <<  ((ADSValuation *)akl.cur()->GetSubject2())->GetNumber() ;
 
230
        }
 
231
        (*ofile) << "};\n";
 
232
      }
 
233
    }
 
234
  }
 
235
  (*ofile) << "\t\tesac\n\t&\n";
 
236
 
 
237
  // print configuration variables
 
238
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
239
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
 
240
    string s=(*(amnodes.cur()->GetName()));
 
241
    (*ofile ) << "\tnext("<< replace(s) << ") in\n\t\tcase\n";
 
242
 
 
243
    for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
244
      Bag <Subject *> currentcfg;
 
245
      cksnodes.cur()->GetConfig(&currentcfg);
 
246
      List <Subject *> currentcfgl;
 
247
      currentcfg.GetSet(&currentcfgl);
 
248
      if (currentcfgl.find(amnodes.cur())>-1){
 
249
        (*ofile) << "\t\t\tnext(c____counter) = " << cksnodes.cur()->GetNumber() << ": " << currentcfg.count(amnodes.cur()) << ";\n";
 
250
      }
 
251
      else{
 
252
        (*ofile) << "\t\t\tnext(c____counter) = " << cksnodes.cur()->GetNumber() << ": 0 ;\n";
 
253
      }
 
254
    }
 
255
    (*ofile) << "\t\tesac\n\t&\n";
 
256
 
 
257
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
258
      string str=(*(amnodes.cur()->GetName())); 
 
259
      (*ofile ) << "\tnext(T_"<< replace(str) << ") in\n\t\tcase\n";    
 
260
      for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
261
        Bag <ATDActionStateNode *> term;
 
262
        cksnodes.cur()->GetTerminated(&term);
 
263
        List <ATDActionStateNode *> terml;
 
264
        term.GetSet(&terml);
 
265
        if (terml.find((ATDActionStateNode *)amnodes.cur())>-1){
 
266
          (*ofile) <<  "\t\t\tnext(c____counter) = " <<cksnodes.cur()->GetNumber() << ": "<< term.count((ATDActionStateNode *)amnodes.cur()) <<";\n";
 
267
        }
 
268
        else {
 
269
          (*ofile) <<  "\t\t\tnext(c____counter) = " <<cksnodes.cur()->GetNumber() << ": 0;\n";
 
270
        }
 
271
      }
 
272
      (*ofile) << "\t\tesac\n\t&\n";
 
273
    }
 
274
 
 
275
  }
 
276
  //
 
277
  for (pl.first();!pl.done();pl.next()){
 
278
    string s=pl.cur()->GetName();
 
279
    (*ofile ) << "\tnext("<< replace(s) << ") in\n\t\tcase\n";
 
280
    PropVal pvt(pl.cur(),true);
 
281
    for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
282
      List <PropVal *> plcur;
 
283
      cksnodes.cur()->GetPropList(&plcur);
 
284
      bool Found=False;
 
285
      for (plcur.first();!plcur.done();plcur.next()){
 
286
        if (((*(plcur.cur()))==pvt)){
 
287
          (*ofile) << "\t\t\tnext(c____counter) = "<< cksnodes.cur()->GetNumber() << ": 1; \n";
 
288
          Found=True;
 
289
          break;
 
290
        }
 
291
      }
 
292
      if (!Found){ // if not found, then false
 
293
        (*ofile) << "\t\t\tnext(c____counter) = "<< cksnodes.cur()->GetNumber() << ": 0; \n";             
 
294
      }
 
295
    }
 
296
    (*ofile) << "\t\tesac\n\t\t&\n";
 
297
  }
 
298
 
 
299
  (*ofile) << "\tnext(stable) in\n\t\tcase\n";
 
300
  for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
301
    (*ofile) << "\t\t\tnext(c____counter) = "<< cksnodes.cur()->GetNumber() << ": ";
 
302
    if (cksnodes.cur()->isStable()){
 
303
      (*ofile) << "1;\n";
 
304
    } 
 
305
    else{
 
306
      (*ofile) << "0;\n";
 
307
    }
 
308
  }
 
309
  (*ofile) << "\t\tesac\n";
 
310
 
 
311
  if (sf){
 
312
    List <ADSHyperEdge *> amedges;
 
313
    am->GetHyperEdges((List<Subject *> *)&amedges);
 
314
    for (amedges.first();!amedges.done();amedges.next()){
 
315
      List <Subject *> *source=amedges.cur()->GetSubject1();
 
316
      List <Subject *> *target=amedges.cur()->GetSubject2();
 
317
      (*ofile) << "\n";
 
318
      (*ofile) << "COMPASSION\n"; 
 
319
      (*ofile) << "(stable &";
 
320
      bool First=True;
 
321
      for (source->first();!source->done();source->next()){
 
322
        string s = *(source->cur()->GetName());
 
323
        if (!First){
 
324
          (*ofile) << " & ";
 
325
        }
 
326
        else First=False;
 
327
        (*ofile) << replace(s) << " > 0 ";
 
328
      }
 
329
      (*ofile) << ", stable & ";
 
330
      First=True;
 
331
      for (target->first();!target->done();target->next()){
 
332
        string s = *(target->cur()->GetName());
 
333
        if (!First){
 
334
          (*ofile) << " & ";
 
335
        }
 
336
        else First=False;
 
337
        (*ofile) << replace(s) << " > 0 ";
 
338
      }
 
339
      (*ofile) << " )\n";
 
340
    }
 
341
    (*ofile) << "\n\n";
 
342
  }
 
343
}
 
344
 
 
345
 
 
346
 
 
347
 
 
348
                 
 
349
 
 
350
        
 
351
void ADSCks::GetClocks(List <string> *l){
 
352
  List <ADSHyperEdge *> amedges;
 
353
  am->GetHyperEdges((List <Subject *> *)&amedges);
 
354
  for (amedges.first();!amedges.done();amedges.next()){
 
355
    if (amedges.cur()->hasClockConstraint()){
 
356
      string s=amedges.cur()->GetClockConstraint()->GetClock()->GetName();
 
357
      l->add(s);
 
358
    }
 
359
  }
 
360
}
 
361
 
 
362
 
 
363
void ADSCks::AssignNumbers(){
 
364
  List <ADSValuation *> cksnodes;
 
365
  GetNodes((List <Subject *> *)&cksnodes);
 
366
  int i=0;
 
367
  for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
368
    cksnodes.cur()->SetNumber(i);
 
369
    i++;
 
370
  }
 
371
}
 
372
 
 
373
 
 
374
// the following procedure requires that AssignNumbers has been done before
 
375
ADSValuation *ADSCks::GetADSValuation(int i){
 
376
  List <ADSValuation *> cksnodes;
 
377
  GetNodes((List <Subject *> *)&cksnodes);
 
378
  for (cksnodes.first();!cksnodes.done();cksnodes.next()){
 
379
    if (i==cksnodes.cur()->GetNumber()) return cksnodes.cur();
 
380
  }
 
381
  return NULL;
 
382
}
 
383
 
 
384
// count and print different configurations
 
385
int ADSCks::countconfigs(){
 
386
  List <ADSValuation *> configlist;
 
387
  int cfgcounter=0; 
 
388
  int stablecount=0;
 
389
  int prec=0;
 
390
  List <ADSValuation *> cksnodes;
 
391
  GetNodes((List <Subject *> *)&cksnodes);
 
392
  int ckscount=cksnodes.count();
 
393
  for (int i=0;i<ckscount;i++){
 
394
    if (!cksnodes[i]->isStable()) stablecount++;
 
395
    else{ if (CountEdgesTo(cksnodes[i])>1) prec++;}
 
396
    bool found=False;
 
397
    for (int j=i+1;j<ckscount;j++){
 
398
      if (cksnodes[i]->hassameconfig(*cksnodes[j])){ found=True;break;}
 
399
    }
 
400
    if (!found){
 
401
      cfgcounter++;
 
402
      configlist.add(cksnodes[i]);
 
403
    }
 
404
  }
 
405
  std::cout << "\nThere are "<< stablecount << " unstable states\n";
 
406
  std::cout << "\nThere are "<< prec << " states with more than one predecessor\n";
 
407
  List <ADSTransition *> cksedges;
 
408
  List <ADSValuation *> temp;
 
409
  GetEdges((List <Subject *> *)&cksedges);
 
410
  ckscount=cksedges.count();
 
411
  for (int i=0;i<ckscount;i++){
 
412
    if ((!((ADSValuation*)cksedges[i]->GetSubject1())->isStable()) &&
 
413
        (!((ADSValuation*)cksedges[i]->GetSubject2())->isStable()))
 
414
      if (temp.find((ADSValuation*)(cksedges[i]->GetSubject2()))<0)
 
415
        temp.add((ADSValuation*)(cksedges[i]->GetSubject2()));
 
416
  }
 
417
  std::cout << "\nThere are "<< temp.count() << " superstep states\n";
 
418
  std::cout << "\nThere are "<< cfgcounter << " different configruations!\n";
 
419
 
 
420
  return cfgcounter;
 
421
}
 
422