← Back to branch summary

~ubuntu-branches/ubuntu/utopic/tcm/utopic

« back to all changes in this revision

Viewing changes to src/sd/bv/adshypergraph.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/adshypergraph.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 "adshypergraph.h"
 
22
#include "code.h"
 
23
#include "atdactionstatenode.h"
 
24
#include "adsactivity.h"
 
25
#include "adshyperedge.h"
 
26
#include "adsvariable.h"
 
27
#include "adsproperty.h"
 
28
#include "outputfile.h"
 
29
#include "adsclock.h"
 
30
#include "node.h"
 
31
#include "adsclockconstraint.h"
 
32
#include "util.h"
 
33
#include "adssemantics.h"
 
34
 
 
35
 
 
36
 
 
37
extern string replace(string s); // defined in adscks
 
38
 
 
39
 
 
40
ADSHyperGraph::ADSHyperGraph() :HyperGraph() {
 
41
  timeoutnumber=0;
 
42
}
 
43
 
 
44
ADSHyperGraph::~ADSHyperGraph(){}
 
45
 
 
46
 
 
47
 
 
48
void ADSHyperGraph::ComputeInternalProperties(){
 
49
  intproplist.empty();
 
50
  for (updatedinactivities.first();!updatedinactivities.done();updatedinactivities.next()){
 
51
    for (propl.first();!propl.done();propl.next()){
 
52
      if (propl.cur()->GetVar()==updatedinactivities.cur()){ // note == on addr
 
53
          switch (propl.cur()->GetType()) {
 
54
          case ::INT :     propl.cur()->SetType(::INTERNAL_INT);break;
 
55
          case ::PROP :    propl.cur()->SetType(::INTERNAL_PROP);break;
 
56
          case ::STRING :  propl.cur()->SetType(::INTERNAL_STRING);break;
 
57
          default : ;
 
58
          }
 
59
          intproplist.add(propl.cur());
 
60
      }
 
61
    }
 
62
  }
 
63
  int length=propl.count();
 
64
  for (int i=0;i<length;i++){
 
65
    if (propl[i]->GetType()==EVENT){ 
 
66
      List <Subject *> edges;
 
67
      GetHyperEdges(&edges);
 
68
      for (edges.first();!edges.done();edges.next()){   
 
69
        Prop *p=((((ADSHyperEdge *)edges.cur())->GetSendEvent()));
 
70
        if ((p) && (*p==*propl[i])){ // EVENT is triggered by SENDEVENT
 
71
          propl[i]->SetType(::SENDEVENT); // then set EVENT to SENDEVENT
 
72
          continue;
 
73
        }
 
74
      } 
 
75
    }
 
76
  }
 
77
}
 
78
 
 
79
void ADSHyperGraph::ComputeInternalHyperEdges(){
 
80
  List <Subject *> edges;
 
81
  GetHyperEdges(&edges);
 
82
  for (edges.first();!edges.done();edges.next()){       
 
83
    List <Prop *> proplist;
 
84
    ((ADSHyperEdge *)edges.cur())->GetPropList(proplist);
 
85
    for (proplist.first();!proplist.done();proplist.next()){
 
86
      if (proplist.cur()->GetType()==::SENDEVENT){
 
87
        ((ADSHyperEdge *)edges.cur())->SetInternal();
 
88
      }
 
89
    }
 
90
  }
 
91
}
 
92
          
 
93
 
 
94
 
 
95
void ADSHyperGraph::ComputeExternalProperties(){
 
96
  extproplist.empty();
 
97
  for (propl.first();!propl.done();propl.next()){
 
98
    if (!(propl.cur()->isInternal())){
 
99
        extproplist.add(propl.cur());
 
100
      }    
 
101
  }
 
102
}
 
103
 
 
104
 
 
105
void ADSHyperGraph::ComputeActivities(){
 
106
  actlist.empty();
 
107
  updatedinactivities.empty();
 
108
 
 
109
  for (nodes->first();!nodes->done();nodes->next()){
 
110
    if (((ATDActionStateNode *)nodes->cur())->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
111
      string s=*(nodes->cur()->GetName());
 
112
      ADSActivity *newact=new ADSActivity(s); // create new activity
 
113
 
 
114
      // insert newact into actlist, if it was not in it already
 
115
      bool b=True;
 
116
      for (actlist.first();!actlist.done();actlist.next()){
 
117
        if (*actlist.cur()==*newact) {
 
118
          b=False; 
 
119
          delete newact;
 
120
          newact=actlist.cur();
 
121
          break;
 
122
        }
 
123
      }
 
124
      if (b) actlist.add(newact);
 
125
      ((ATDActionStateNode *)nodes->cur())->SetActivity(newact); 
 
126
    
 
127
 
 
128
      List <Subject *> *l=new List <Subject *>;
 
129
      GetHyperEdgesFrom(l,nodes->cur());
 
130
      for (l->first();!l->done();l->next()){
 
131
        List <ADSVar *> vl;
 
132
        ((ADSHyperEdge *)l->cur())->GetVarList(vl);
 
133
        for (vl.first();!vl.done();vl.next()){
 
134
          newact->AddUpdate(vl.cur());
 
135
          
 
136
          // update updatedinactivities
 
137
          bool found=False;
 
138
          for (updatedinactivities.first();!updatedinactivities.done();updatedinactivities.next()){                
 
139
            if (*updatedinactivities.cur()==*vl.cur()){
 
140
              found=True;
 
141
              break;
 
142
            }
 
143
          }
 
144
          if (!found) updatedinactivities.add(vl.cur());
 
145
        }
 
146
      }    
 
147
      
 
148
    }
 
149
  }
 
150
}
 
151
 
 
152
 
 
153
void ADSHyperGraph::ComputeInterferences(){
 
154
  int count=actlist.count();
 
155
  int i,j;
 
156
  // Begin computation of conflicts
 
157
  for (i=0;i<count;i++){
 
158
    List <ADSVar *> l1;
 
159
    actlist[i]->GetUpdateList(l1);
 
160
    
 
161
    for (j=i;j<count;j++){
 
162
      List <ADSVar *> l2;
 
163
      actlist[j]->GetUpdateList(l2);
 
164
      interference[i][j]=0;
 
165
      for (l1.first();!l1.done();l1.next()){
 
166
 
 
167
        bool b=False;
 
168
        for (l2.first();!l2.done();l2.next()){
 
169
          ADSVar *v1=l1.cur();
 
170
          ADSVar *v2=l2.cur();
 
171
          if (*v1==*v2){
 
172
            interference[i][j]=1;
 
173
            b=True;
 
174
            break;
 
175
          }
 
176
        }
 
177
        if (b) break; // conflict[i][j] already found
 
178
      }
 
179
    }
 
180
  }
 
181
}
 
182
 
 
183
bool ADSHyperGraph::GetInterference(ADSActivity *a1,ADSActivity *a2){ // action state node???
 
184
  int i1=actlist.find(a1);
 
185
  int i2=actlist.find(a2);
 
186
  if ((i1==-1) || (i2==-1)) return False;
 
187
  if (i1<i2) 
 
188
    return interference[i1][i2];
 
189
  else 
 
190
    return interference[i2][i1];
 
191
}
 
192
 
 
193
bool ADSHyperGraph::GetInterference(ATDActionStateNode *a1, ATDActionStateNode *a2){
 
194
  string a1name=*a1->GetName();
 
195
  string a2name=*a2->GetName();
 
196
  ADSActivity *a1new= new ADSActivity(a1name);
 
197
  ADSActivity *a2new= new ADSActivity(a2name);
 
198
  ADSActivity *a1old=0, *a2old=0;
 
199
  bool b1=False;
 
200
  bool b2=False;
 
201
  for (actlist.first();!actlist.done();actlist.next()){
 
202
    if (*a1new==*actlist.cur()) {a1old=actlist.cur();b1=True;}
 
203
    if (*a2new==*actlist.cur()) {a2old=actlist.cur();b2=True;}
 
204
    if (b1&&b2) break;
 
205
  }
 
206
  if (b1&&b2) 
 
207
    return GetInterference(a1old,a2old);
 
208
  else // not found? I'm confused!
 
209
    return False;
 
210
}
 
211
 
 
212
 
 
213
void ADSHyperGraph::Initialise(){
 
214
  ComputeActivities();
 
215
  ComputeInterferences();
 
216
  ComputeConflicts();
 
217
  ComputeInternalProperties();
 
218
  ComputeExternalProperties();
 
219
  ComputeInternalHyperEdges();
 
220
  ComputeNrTimeouts();
 
221
  SetInitialFinalNames();
 
222
  InitialiseBounds();
 
223
}
 
224
 
 
225
void ADSHyperGraph::Finalise(){
 
226
   UnSetInitialFinalNames();
 
227
}
 
228
 
 
229
bool ADSHyperGraph::AddProp(Prop *p){
 
230
  for (propl.first();!propl.done();propl.next()){
 
231
    if (*propl.cur()==*p) return False;
 
232
  }
 
233
  propl.add(p);
 
234
  return True;
 
235
}
 
236
 
 
237
bool ADSHyperGraph::AddVar(ADSVar *v){
 
238
  for (varl.first();!varl.done();varl.next()){
 
239
    if (*varl.cur()==*v) return False;
 
240
  }
 
241
  varl.add(v);
 
242
  return True;
 
243
}
 
244
 
 
245
 
 
246
void ADSHyperGraph::RemoveProp(Prop *p){ 
 
247
  propl.remove(p);
 
248
}
 
249
 
 
250
void ADSHyperGraph::GetPropList(List <Prop *> &p){
 
251
  p=propl;
 
252
}
 
253
 
 
254
void ADSHyperGraph::GetExtPropList(List <Prop *> &p){
 
255
  p=extproplist;
 
256
}
 
257
 
 
258
void ADSHyperGraph::GetIntPropList(List <Prop *> &p){
 
259
  p=intproplist;
 
260
}
 
261
 
 
262
void ADSHyperGraph::GetVarList(List <ADSVar *> &v){
 
263
  v=varl;
 
264
}
 
265
 
 
266
Prop *ADSHyperGraph::FindSimilarProp(Prop *p){
 
267
  for (propl.first();!propl.done();propl.next()){
 
268
    if (*propl.cur()==*p) return propl.cur();
 
269
  }
 
270
  return 0;
 
271
}  
 
272
 
 
273
ADSVar *ADSHyperGraph::FindSimilarVar(ADSVar *p){
 
274
  for (varl.first();!varl.done();varl.next()){
 
275
    if (*varl.cur()==*p) return varl.cur();
 
276
  }
 
277
  return 0;
 
278
}  
 
279
 
 
280
Node *ADSHyperGraph::FindNode(string name){
 
281
  //  List <Subject *> nodes;
 
282
  //  GetNodes(&nodes);
 
283
  for (nodes->first();!nodes->done();nodes->next()){
 
284
    if (replace(*(nodes->cur()->GetName()))==replace(name)){
 
285
      return (Node*)(nodes->cur());
 
286
    }
 
287
  }
 
288
  return NULL;
 
289
}
 
290
 
 
291
 
 
292
//ADSActivity *ADSHyperGraph::FindAct(string s){
 
293
//  ADSActivity *a = new ADSActivity(s);
 
294
//  for (actlist.first();!actlist.done();actlist.next()){
 
295
//    if (*actlist.cur()==*a) return actlist.cur();
 
296
//  }
 
297
//  return 0;
 
298
//}
 
299
 
 
300
 
 
301
 
 
302
// The now following procedure is old, since we now discretise 
 
303
// all clocks with 1, not with 1/nr of timeouts
 
304
void ADSHyperGraph::ComputeNrTimeouts(){
 
305
  //  List <Subject *> amhedges;
 
306
  //  GetHyperEdges(&amhedges);
 
307
  // for (amhedges.first(); !amhedges.done(); amhedges.next()) {
 
308
  //    if (((ADSHyperEdge *)amhedges.cur())->hasClockConstraint()) timeoutnumber++;
 
309
  //  }
 
310
  timeoutnumber=0; // discretisation with 1
 
311
}
 
312
 
 
313
void ADSHyperGraph::WriteSubjects(OutputFile *f) {
 
314
  HyperGraph::WriteSubjects(f);
 
315
  (*f) << "INTERNAL PROPERTY LIST \n";
 
316
  for (intproplist.first();!intproplist.done();intproplist.next()){
 
317
    intproplist.cur()->Write(f);
 
318
  }
 
319
  (*f) << "EXTERNAL PROPERTY LIST \n";
 
320
  for (extproplist.first();!extproplist.done();extproplist.next()){
 
321
    extproplist.cur()->Write(f);
 
322
  }
 
323
  List <Subject *> amhedges;
 
324
  GetHyperEdges(&amhedges);
 
325
  int actcount=actlist.count();
 
326
  for (int i=0;i<actcount;i++){
 
327
    (*f) << i << ":\t";
 
328
    actlist[i]->Write(f);
 
329
    for (int j=i+1;j<actcount;j++){
 
330
      if (GetInterference(actlist[i],actlist[j])){
 
331
        (*f) << "1";;
 
332
      }
 
333
      else (*f) << "0";
 
334
    }
 
335
    (*f) << "\n";
 
336
  } 
 
337
}
 
338
 
 
339
 
 
340
 
 
341
void ADSHyperGraph::UpdateBounds(Bag <Subject *> *cfg){
 
342
  List <Subject *> ls;
 
343
  cfg->GetSet(&ls);
 
344
  List <Node *> ahnodes;
 
345
  GetNodes((List <Subject *> *)&ahnodes);
 
346
  int count=ahnodes.count();
 
347
  for (int i=0;i<count;i++){ 
 
348
    int c=cfg->count(ahnodes[i]);
 
349
    if (c>bound[i]) bound[i]=c;
 
350
  }
 
351
}
 
352
 
 
353
void ADSHyperGraph::InitialiseBounds(){
 
354
  List <Node *> ahnodes;
 
355
  GetNodes((List <Subject *> *)&ahnodes);
 
356
  int ahnodescount=ahnodes.count();
 
357
  int i;
 
358
  for (i=0;i<ahnodescount;i++){
 
359
    bound[i]=0;
 
360
  }
 
361
}
 
362
 
 
363
int ADSHyperGraph::GetBound(Subject *s){
 
364
  List <Subject *> ahnodes;
 
365
  GetNodes(&ahnodes);
 
366
  int index=ahnodes.find(s);
 
367
  if (index==-1) error ("A node that does not exist cannot have a bound!\n");
 
368
  return bound[index];
 
369
}
 
370
 
 
371
 
 
372
void ADSHyperGraph::ComputeConflicts(){
 
373
  List <ADSHyperEdge *> hyperedges;
 
374
  GetHyperEdges((List <Subject *> *)&hyperedges);
 
375
  int hedgescount = hyperedges.count();
 
376
  for (int i=0;i<hedgescount;i++){
 
377
    // the same hyperedges cannot be in conflict since otherwise they would not have enabled simultaneously
 
378
    List <Subject *> *source_i=hyperedges[i]->GetSubject1();
 
379
    for (int j=i+1;j<hedgescount;j++){      
 
380
      List <Subject *> *source_j=hyperedges[j]->GetSubject1();
 
381
      for (source_j->first();!source_j->done();source_j->next()){
 
382
        if (source_i->find(source_j->cur())>-1){ // hyperedges[i] and hyperedges[j] have overlapping sources
 
383
          hyperedges[i]->AddConflict(hyperedges[j]);
 
384
          hyperedges[j]->AddConflict(hyperedges[i]);
 
385
          break; // jump out of for-loop
 
386
        }
 
387
      }
 
388
    }
 
389
  }
 
390
}
 
391
 
 
392
void ADSHyperGraph::SetInitialFinalNames(){
 
393
  List <Subject *> ahnodes;
 
394
  GetNodes(&ahnodes);
 
395
  for (ahnodes.first();!ahnodes.done();ahnodes.next()){
 
396
    string s=(*(ahnodes.cur()->GetName()));
 
397
    if (ahnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
 
398
      s="I___INITIAL";ahnodes.cur()->SetName(&s);
 
399
    }
 
400
    if (ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
 
401
      string t = (int)ahnodes.cur()->GetId();
 
402
      s="F___FINAL"+t; ahnodes.cur()->SetName(&s);
 
403
    }
 
404
  }
 
405
}    
 
406
 
 
407
void ADSHyperGraph::UnSetInitialFinalNames(){
 
408
  List <Subject *> ahnodes;
 
409
  GetNodes(&ahnodes);
 
410
  for (ahnodes.first();!ahnodes.done();ahnodes.next()){
 
411
    if ((ahnodes.cur()->GetClassType()!=Code::ATD_INITIAL_STATE_NODE)||(ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE)) continue; // skip these
 
412
    if (ahnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
 
413
      string s=""; ahnodes.cur()->SetName(&s);
 
414
    }
 
415
    if (ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
 
416
      string s=""; ahnodes.cur()->SetName(&s);
 
417
    }
 
418
  }
 
419
}    
 
420
 
 
421
 
 
422
void PrintBag(Bag <ADSHyperEdge *> *b){
 
423
  List <ADSHyperEdge *> l;
 
424
  b->GetList(l);
 
425
  for (l.first();!l.done();l.next()){
 
426
    std::cout << l.cur()->GetId() <<":\t" << b->count(l.cur()) <<"\n";
 
427
  }
 
428
}
 
429
 
 
430
bool ADSHyperGraph::isConflicting(Bag <ADSHyperEdge *> *step, ADSHyperEdge *he){
 
431
  List <ADSHyperEdge *> al; // the list of hyperedges in conflict with he
 
432
  he->GetConflict(&al); 
 
433
  for (al.first();!al.done();al.next()){
 
434
    if (step->count(al.cur())) return True;
 
435
  }
 
436
  return False;
 
437
}
 
438
 
 
439
 
 
440
 
 
441
string ADSHyperGraph::DeadEdgesNodesConstraints(){
 
442
  string constraint;
 
443
  List <ADSHyperEdge *> hyperedges;
 
444
  GetHyperEdges((List <Subject *> *)&hyperedges);
 
445
  int hedgescount = hyperedges.count();
 
446
  for (int i=0;i<hedgescount;i++){
 
447
    if (i)
 
448
      constraint += " & ";
 
449
 
 
450
    List <Subject *> *source_i=hyperedges[i]->GetSubject1();
 
451
    bool First=True;
 
452
    string sourceconstraint;
 
453
    for (source_i->first();!source_i->done();source_i->next()){
 
454
      if (!First)
 
455
        sourceconstraint+=" & ";
 
456
      else
 
457
        First=False;
 
458
      string s=(*(source_i->cur()->GetName()));
 
459
      sourceconstraint += replace(s) + " > 0 " ;
 
460
    }
 
461
 
 
462
    List <Subject *> *target_i=hyperedges[i]->GetSubject2();
 
463
    First=True;
 
464
    string targetconstraint;
 
465
    for (target_i->first();!target_i->done();target_i->next()){
 
466
      if (!First)
 
467
        targetconstraint+=" & ";
 
468
      else
 
469
        First=False;
 
470
      string s=(*(target_i->cur()->GetName()));
 
471
      targetconstraint += replace(s) + " > 0 ";
 
472
    }
 
473
    constraint += "( EF (" + sourceconstraint + " & (EX (" + targetconstraint +
 
474
"))))";
 
475
  }
 
476
 
 
477
  return constraint;
 
478
}
 
479
 
 
480
 
 
481
 
 
482
 
 
483
 
 
484
string ADSHyperGraph::ComputeFinalPredicate(){
 
485
  string final="( (";
 
486
  List <Subject *> ls;
 
487
  GetNodes(&ls); // get all the nodes
 
488
  bool First=True;
 
489
  for (ls.first();!ls.done();ls.next()){
 
490
    if ((ls.cur()->GetClassType()==Code::NOTE)||(ls.cur()->GetClassType()==Code::COMMENT)||(ls.cur()->GetClassType()==Code::ATD_DECISION_STATE_NODE)||(ls.cur()->GetClassType()==Code::ATD_SYNCHRONIZATION_NODE)||(ls.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE)) continue; // skip these
 
491
    if (!First){
 
492
      final += " & ";
 
493
    }
 
494
    else{
 
495
      First=False;
 
496
    }
 
497
    if (ls.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
 
498
      final+="I___INITIAL=0";
 
499
    }
 
500
    else{ // action or wait state node
 
501
      string stemp=(*(ls.cur()->GetName()));
 
502
      stemp.replace("-\r","");
 
503
      stemp.replace('\r','_');
 
504
      stemp.replace(' ','_');
 
505
      stemp.replace('/','_');
 
506
      stemp.replace('.','_');
 
507
      stemp.replace('-','_');
 
508
      stemp += "=0";
 
509
      final+=stemp;
 
510
    }
 
511
  }  
 
512
  final += ") & ( 0 ";
 
513
 
 
514
 
 
515
  // First=True;
 
516
  string finalexpr;
 
517
  for (ls.first();!ls.done();ls.next()){
 
518
    if (ls.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
 
519
      finalexpr += " | ";
 
520
      finalexpr+="F___FINAL";
 
521
      string index = (int)ls.cur()->GetId();
 
522
      finalexpr = finalexpr + index + ">0";
 
523
    }
 
524
  }  
 
525
 
 
526
  final += finalexpr;
 
527
  final += ") )";
 
528
  return final;
 
529
}
 
530
 
 
531
 
 
532
void ADSHyperGraph::GetFinalNodes(List <Subject *> *final){
 
533
  for (nodes->first();!nodes->done();nodes->next()){
 
534
    if (nodes->cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
 
535
      final->add(nodes->cur());
 
536
    }
 
537
  }  
 
538
}
 
539
 
 
540
 
 
541
 
 
542
// Note: only works for safe activity graphs
 
543
void ADSHyperGraph::WriteNuSMV(OutputFile *ofile, bool sf){ 
 
544
  (*ofile) <<  "MODULE main\n\nVAR\n";
 
545
  List <Subject *> amnodes;
 
546
  GetNodes(&amnodes);
 
547
  List <ADSHyperEdge *> amedges;
 
548
  GetHyperEdges((List<Subject *> *)&amedges);
 
549
 
 
550
  List <Subject *> writtennodes; // nodes written as var so far
 
551
  List <Subject *> writtenedges; // edges written as var so far
 
552
  List <Prop *> writtenprop; // edges written as var so far
 
553
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
554
    if (amnodes.cur()->GetClassType()!=Code::ATD_INITIAL_STATE_NODE) continue; // skip these nodes
 
555
    string s=(*(amnodes.cur()->GetName()));
 
556
    writtennodes.add(amnodes.cur());
 
557
    (*ofile ) << "\t"<< replace(s) << " : boolean;\n";
 
558
  }
 
559
 
 
560
  while(writtennodes.count()<amnodes.count())  {
 
561
    List <ADSHyperEdge *> newenabled;
 
562
    GetHyperEdgesFrom((List <HyperEdge *> *)&newenabled,&writtennodes);
 
563
    for (newenabled.first();!newenabled.done();newenabled.next()){
 
564
      if (!writtenedges.contains(newenabled.cur())){
 
565
        writtenedges.add(newenabled.cur());
 
566
        List <Prop *> pl;
 
567
        newenabled.cur()->GetPropList(pl);
 
568
        for (pl.first();!pl.done();pl.next()){
 
569
          if (!((pl.cur()->GetType()==PROP)||(pl.cur()->GetType()==PROP)||(pl.cur()->GetType()==EVENT))) continue; // only events and stuff
 
570
          if (!writtenprop.contains(pl.cur())){
 
571
            writtenprop.add(pl.cur());
 
572
            (*ofile) << "\t" << replace(pl.cur()->GetName()) <<  " : boolean;\n";
 
573
          }
 
574
        }
 
575
 
 
576
        if (newenabled.cur()->hasClockConstraint()){
 
577
          string name=newenabled.cur()->GetUniqueName();
 
578
          (*ofile) <<  "\t" << name << "-timer:0.." << ((GetNrTimeouts() + 1 )  * (newenabled.cur()->GetClockConstraint()->GetLimit())) << ";\n";
 
579
        }
 
580
        
 
581
 
 
582
        if ((newenabled.cur()->GetSendEvent()) && (!writtenprop.contains(newenabled.cur()->GetSendEvent()))){
 
583
          writtenprop.add(newenabled.cur()->GetSendEvent());
 
584
          (*ofile) << "\t" << replace(newenabled.cur()->GetSendEvent()->GetName()) << " : boolean;\n";
 
585
        }
 
586
      }
 
587
 
 
588
      List <Subject *> *target=newenabled.cur()->GetSubject2();
 
589
      for (target->first();!target->done();target->next()){
 
590
        if (writtennodes.contains(target->cur())) continue;
 
591
        string s=(*(target->cur()->GetName()));
 
592
        writtennodes.add(target->cur());
 
593
        (*ofile ) << "\t"<< replace(s) << " : boolean;\n";
 
594
        if (target->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
595
          (*ofile ) << "\tT_" << replace(s) << " : boolean;\n";
 
596
          for (actlist.first();!actlist.done();actlist.next()){
 
597
            if (replace(actlist.cur()->GetName())==replace(s)){
 
598
              List <ADSVar *> varlist;
 
599
              actlist.cur()->GetUpdateList(varlist);
 
600
              for (intproplist.first();!intproplist.done();intproplist.next()){
 
601
                if (writtenprop.contains(intproplist.cur())) continue;
 
602
                if (((intproplist.cur()->GetType()==INTERNAL_PROP)||(intproplist.cur()->GetType()==INTERNAL_STRING))&&(varlist.contains(intproplist.cur()->GetVar()))){   
 
603
                  (*ofile) << "\t" << replace(intproplist.cur()->GetName()) << ": boolean;\n";
 
604
                  writtenprop.add(intproplist.cur());
 
605
                }
 
606
              }
 
607
            }
 
608
          }
 
609
        }
 
610
      }
 
611
    }
 
612
  }
 
613
 
 
614
 
 
615
  (*ofile) << "\nINIT  -- state nodes\n";
 
616
  bool FirstInit=True;
 
617
  //  (*ofile) << "\tc____counter = 0 & \n "; // because of assign number
 
618
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
619
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
 
620
    if (FirstInit) FirstInit=False;
 
621
    else (*ofile) << " &\n";
 
622
    string s=(*(amnodes.cur()->GetName()));
 
623
    if ((amnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE)){
 
624
      (*ofile) << "\t" << replace(s) << "\t = TRUE";
 
625
    }
 
626
    else{
 
627
      (*ofile) << "\t" << replace(s) << "\t = FALSE" ;
 
628
    }
 
629
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
630
      (*ofile ) << " &\n\tT_" << replace(s) << "\t = FALSE" ;
 
631
    }
 
632
  }
 
633
  FirstInit=True;
 
634
  for (propl.first();!propl.done();propl.next()){
 
635
    if (FirstInit){
 
636
      FirstInit=False;
 
637
      (*ofile) << "\n\nINIT -- events etc.\n";
 
638
    }
 
639
    else (*ofile) << " &\n";
 
640
    string s=propl.cur()->GetName();
 
641
    (*ofile ) << "\t" << replace(s) << "\t = FALSE";    
 
642
  }
 
643
  (*ofile) << "\n\n";
 
644
 
 
645
 
 
646
  FirstInit=True;
 
647
  for (amedges.first();!amedges.done();amedges.next()){
 
648
    if (amedges.cur()->hasClockConstraint()){
 
649
      if (FirstInit){
 
650
        FirstInit=False;
 
651
        (*ofile) << "\n\nINIT -- timers \n";
 
652
      }
 
653
      else (*ofile) << " &\n";
 
654
      string name=amedges.cur()->GetUniqueName();
 
655
      (*ofile) << "\t" << name << "-timer = 0\n";
 
656
    }
 
657
  }
 
658
 
 
659
  for (amedges.first();!amedges.done();amedges.next()){
 
660
    (*ofile) << "DEFINE -- hyperedges \n\n";  
 
661
    string name=amedges.cur()->GetUniqueName();
 
662
    (*ofile) << "\t" << name+"-relevant := ";
 
663
    List <Subject *> *source=amedges.cur()->GetSubject1();
 
664
    bool First=True;
 
665
    for (source->first();!source->done();source->next()){
 
666
      if (First) First=False;
 
667
      else (*ofile) << " & ";
 
668
      string sourcename=*(source->cur()->GetName());
 
669
      (*ofile) << replace(sourcename) ;
 
670
    }
 
671
    (*ofile) << ";\n\t" << name+"-enabled := " << name << "-relevant ";
 
672
    if (!amedges.cur()->HasEmptyEvent()){
 
673
      (*ofile) << " & " << replace(amedges.cur()->GetEvent()) ;
 
674
    }
 
675
    for (source->first();!source->done();source->next()){
 
676
      if (source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
677
        string sourcename=*(source->cur()->GetName());
 
678
        (*ofile) << " & T_" << replace(sourcename)  ;
 
679
      }
 
680
    }
 
681
    if (!amedges.cur()->HasEmptyGuard()){
 
682
      string guard=amedges.cur()->GetGuard();
 
683
      guard.replace('[','(');
 
684
      guard.replace(']',')');
 
685
      guard.replace('~','!');
 
686
      guard.replace("IN","");
 
687
      (*ofile) << " & " << replace(guard) ;
 
688
    }
 
689
    if (amedges.cur()->hasClockConstraint()){       
 
690
      (*ofile) << " & " << name << "-timer = " << (1+GetNrTimeouts()) * (amedges.cur()->GetClockConstraint()->GetLimit()) ;
 
691
    }
 
692
    (*ofile) << ";\n"; 
 
693
 
 
694
 
 
695
    ///
 
696
    List <Subject *> *target=amedges.cur()->GetSubject2();
 
697
    (*ofile) << "\t" << name+"-taken := " << name+"-enabled ";
 
698
    for (source->first();!source->done();source->next()){
 
699
      if (!target->contains(source->cur())){
 
700
        (*ofile) << " & ";
 
701
        string sourcename=*(source->cur()->GetName());
 
702
        (*ofile) << "(next(" + replace(sourcename) + ")=FALSE)" ;
 
703
      }
 
704
    }    
 
705
 
 
706
    for (target->first();!target->done();target->next()){
 
707
      (*ofile) << " & ";
 
708
      string targetname=*(target->cur()->GetName());
 
709
      (*ofile) << "next("+replace(targetname)+")";      
 
710
      //}
 
711
    }  
 
712
    (*ofile) << ";\n";
 
713
 
 
714
    ///
 
715
    (*ofile) << "\nTRANS\n";
 
716
    (*ofile) << "\t" << "(!"+name+"-enabled)";
 
717
    List <ADSHyperEdge *> conflict;
 
718
    amedges.cur()->GetConflict(&conflict);
 
719
    (*ofile) << "| ((!" << name << "-taken) <-> ( FALSE";
 
720
    for (conflict.first();!conflict.done();conflict.next()){
 
721
      (*ofile) << " | ";
 
722
      (*ofile) << replace(conflict.cur()->GetUniqueName())<<"-taken";   
 
723
    }
 
724
    (*ofile) << " ))\n\n";    
 
725
    (*ofile) << "\n";
 
726
    
 
727
    ///
 
728
    (*ofile) << "\nDEFINE -- timers\n\n";
 
729
    if (amedges.cur()->hasClockConstraint()){
 
730
      (*ofile) << "\t" << name << "-timer_on := (!" << name << "-relevant) & next(" <<  name << "-relevant);\n";
 
731
      
 
732
      
 
733
      (*ofile) << "TRANS\n";
 
734
      (*ofile) << "\t!next(" << name << "-relevant) -> next(" <<  name << "-timer)=0\n";
 
735
 
 
736
      (*ofile) << "TRANS\n";     
 
737
      (*ofile) << "\t(" << name << "-timer_on ) -> next(" << name << "-timer) = 0\n";
 
738
      (*ofile) << "TRANS\n";
 
739
      (*ofile) << "\t( stable & " << name << "-relevant & " ;  
 
740
      (*ofile)<< "next(" << name << "-relevant)) -> (next(" <<  name << "-timer) = " << name << "-timer + 1)\n";
 
741
      (*ofile) << "TRANS\n";
 
742
      (*ofile) << "\t(!stable & " << name << "-relevant & next(" << name << "-relevant)) -> (next(" <<  name << "-timer) = " << name << "-timer )\n\n";
 
743
    }
 
744
  }
 
745
 
 
746
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
747
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
 
748
    string s = *(amnodes.cur()->GetName());
 
749
    (*ofile) << "TRANS\n\t(" << replace(s)  << " = next(" << replace(s) << "))";
 
750
    for (amedges.first();!amedges.done();amedges.next()){
 
751
      List <Subject *> *source=amedges.cur()->GetSubject1();
 
752
      if (source->contains(amnodes.cur())) 
 
753
        (*ofile) << " | " << amedges.cur()->GetUniqueName()<<"-taken"  << "\n";
 
754
      List <Subject *> *target=amedges.cur()->GetSubject2();
 
755
      if (target->contains(amnodes.cur())) 
 
756
        (*ofile) << " | " << amedges.cur()->GetUniqueName()<<"-taken"  << "\n";    
 
757
    }
 
758
    (*ofile) << "\n";
 
759
  }
 
760
  // EVENT GENERATION
 
761
  (*ofile) << "\n-- external event generation\n";
 
762
  (*ofile) <<  "ASSIGN\n";
 
763
  for (propl.first();!propl.done();propl.next()){
 
764
    if (propl.cur()->GetType()==EVENT){ // external event
 
765
      string s=propl.cur()->GetName();
 
766
      (*ofile ) << "\tnext(" << replace(s) << ") :=\n\t\tcase\n\t\t\tstable:{FALSE,TRUE};\n\t\t\t\tTRUE:FALSE;\n\t\tesac;\n"; 
 
767
    }
 
768
    if (propl.cur()->GetType()==SENDEVENT){// internal event
 
769
      string s=propl.cur()->GetName();
 
770
      (*ofile ) << "\tnext(" << replace(s) << ") :=\n";
 
771
      bool FirstSendEvent=True;
 
772
      for (amedges.first();!amedges.done();amedges.next()){
 
773
        if ((amedges.cur()->GetSendEvent())&&(*(amedges.cur()->GetSendEvent())==*propl.cur())){
 
774
          (*ofile) << "\t\t";
 
775
          if (FirstSendEvent) {FirstSendEvent=False;(*ofile) << "   ";}
 
776
          else (*ofile) << " | ";
 
777
          (*ofile) << amedges.cur()->GetUniqueName()<<"-taken" <<"\n";
 
778
        }
 
779
      }
 
780
      (*ofile) <<"\t\t;\n";
 
781
    }  
 
782
  }
 
783
  (*ofile) << "\n-- termination event generation\n";
 
784
  // termination events
 
785
  for (amnodes.first();!amnodes.done();amnodes.next()){    
 
786
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
787
      string s=*(amnodes.cur()->GetName());
 
788
      (*ofile ) << "\tnext(T_" << replace(s) << ") :=\n\t\tcase\n\t\t\t(stable & " << replace(s) <<  "):{FALSE,TRUE};\n\t\t\tTRUE:FALSE;\n\t\tesac;\n";     
 
789
    }
 
790
  }
 
791
 
 
792
  (*ofile) << "\n-- property update\n";
 
793
  for (propl.first();!propl.done();propl.next()){
 
794
    if ((propl.cur()->isInternal()&&(propl.cur()->GetType()!=SENDEVENT))){ // property is updated internally
 
795
      (*ofile) << "TRANS\n\t("<<replace(propl.cur()->GetName()) << "=next(" << replace(propl.cur()->GetName()) << "))" ;
 
796
      for (amnodes.first();!amnodes.done();amnodes.next()){
 
797
        if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
798
          string s=*(amnodes.cur()->GetName());
 
799
          //      ADSActivity *a=FindAct(s);
 
800
          ADSActivity *a=((ATDActionStateNode *)amnodes.cur())->GetActivity();
 
801
          if (a->isUpdated(propl.cur()->GetVar()))
 
802
            (*ofile) << " | next(T_" << replace(s) << ")\n"; // update on variable
 
803
        }
 
804
      }
 
805
    }
 
806
  }
 
807
 
 
808
 
 
809
  if (sf){
 
810
    // COMPASSION CONSTRAINTS
 
811
    for (amedges.first();!amedges.done();amedges.next()){
 
812
      if (amedges.cur()->GetInternal()) continue;
 
813
      if (amedges.cur()->hasClockConstraint()) continue;
 
814
      (*ofile) << "\nCOMPASSION\n"; 
 
815
      (*ofile) << "(" << amedges.cur()->GetUniqueName() << "-relevant, " << amedges.cur()->GetUniqueName() << "-taken)\n";
 
816
    }
 
817
    (*ofile) << "\n\n";
 
818
  }
 
819
 
 
820
 
 
821
  List <Subject *> finalnodes;
 
822
 
 
823
  // INTERFERENCE
 
824
  (*ofile) << "\n-- interference\n";
 
825
  int amlen=amnodes.count();
 
826
  for (int i=0;i<amlen;i++){    
 
827
    for (int j=i+1;j<amlen;j++){
 
828
      if ((amnodes[i]->GetClassType()==Code::ATD_ACTION_STATE_NODE)&&
 
829
          (amnodes[j]->GetClassType()==Code::ATD_ACTION_STATE_NODE)&&
 
830
          (GetInterference((ATDActionStateNode*)amnodes[i],(ATDActionStateNode*)amnodes[j]))){
 
831
        (*ofile) << "TRANS\n\t!(";
 
832
        string s1 = *(amnodes[i]->GetName());
 
833
        string s2 = *(amnodes[j]->GetName());
 
834
        (*ofile) << "next(" << replace(s1) << ") & next(" << replace(s2) << "))\n";
 
835
      }
 
836
    }
 
837
    if (amnodes[i]->GetClassType()==Code::ATD_FINAL_STATE_NODE){
 
838
      finalnodes.add(amnodes[i]);
 
839
    }
 
840
  }
 
841
 
 
842
  // final nodes
 
843
  if (finalnodes.count()){
 
844
//  bool FirstFinal=True;
 
845
    (*ofile) << "\n -- events cannot be generated if the configuration is final\n";
 
846
    (*ofile) << "INVAR\n";
 
847
    (*ofile) << "\t" << ComputeFinalPredicate() << "\t\t-> stable\n\n";
 
848
 
 
849
  }
 
850
 
 
851
 
 
852
  // ENABLEDNESS
 
853
  (*ofile) << "\n-- enabledness\n";
 
854
  (*ofile) << "DEFINE\n\tstable := !enabled & !events;\n";
 
855
  (*ofile) << "DEFINE\n\tenabled := \n";
 
856
  bool FirstEnabled=True; 
 
857
  for (amedges.first();!amedges.done();amedges.next()){
 
858
    (*ofile) << "\t\t";
 
859
    if (FirstEnabled){
 
860
      FirstEnabled=False; (*ofile) << "   ";
 
861
    }
 
862
    else (*ofile) << " | ";
 
863
    (*ofile) << amedges.cur()->GetUniqueName()<<"-enabled" << "\n"; 
 
864
  }
 
865
  (*ofile) << "\t\t;\n\n";
 
866
 
 
867
  (*ofile) << "DEFINE\n\tevents := FALSE \n";
 
868
  for (propl.first();!propl.done();propl.next()){
 
869
    if ((propl.cur()->GetType()==EVENT)||(propl.cur()->GetType()==SENDEVENT)){ // external or internal event
 
870
      (*ofile) << " | ";
 
871
      string s=propl.cur()->GetName();
 
872
      (*ofile ) << "\t\t" << replace(s) <<"\n"; 
 
873
    }
 
874
  }
 
875
  for (int i=0;i<amlen;i++){    
 
876
    if (amnodes[i]->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
877
      (*ofile) << " | ";
 
878
      string s = *(amnodes[i]->GetName());
 
879
      (*ofile) << "\t\tT_"<< replace(s) << "\n";
 
880
    }
 
881
  }
 
882
  (*ofile) << "\t\t ;\n\n";
 
883
 
 
884
  // 
 
885
  (*ofile) << "-- disable concurrent enabling of two hyperedges where the source and target of one are contained in the source and target of other\n";
 
886
  int elen=amedges.count();  
 
887
  for (int i=0;i<elen-1;i++){
 
888
    for (int j=i+1;j<elen;j++){
 
889
        // check if sources and targets of amedges[i] are contained in those of conflict.cur()
 
890
      //      List <Subject *> *source=amedges[i]->GetSubject1();
 
891
      bool FoundConflict=(amedges[i]->conflicts(amedges[j]));
 
892
      if (!FoundConflict){
 
893
        List <Subject *> *target=amedges[i]->GetSubject2();
 
894
        bool FoundTargets=True;
 
895
        for (target->first();!target->done();target->next()){
 
896
          if (!amedges[j]->GetSubject2()->contains(target->cur())){
 
897
            FoundTargets=False;
 
898
            break;
 
899
          }
 
900
        }
 
901
        if (FoundTargets){ // amedges[i] is contained in amedges[j]
 
902
          (*ofile) << "TRANS\n\tnext(" << amedges[i]->GetUniqueName() << "-enabled) -> ! next(" <<  amedges[j]->GetUniqueName() << "-enabled)\n";
 
903
        }
 
904
      }
 
905
               
 
906
      if (!FoundConflict){      
 
907
        List <Subject *> *target=amedges[j]->GetSubject2();
 
908
        bool FoundTargets=True;
 
909
        for (target->first();!target->done();target->next()){
 
910
          if (!amedges[i]->GetSubject2()->contains(target->cur())){
 
911
            FoundTargets=False;
 
912
            break;
 
913
          }
 
914
        }
 
915
        if (FoundTargets){ // amedges[j] is contained in amedges[i]
 
916
          (*ofile) << "TRANS\n\tnext(" <<  amedges[j]->GetUniqueName() << "-enabled) -> ! next(" << amedges[i]->GetUniqueName() << "-enabled)\n";
 
917
        }
 
918
      }
 
919
    }
 
920
  }
 
921
  (*ofile) << "\n";
 
922
}
 
923
 
 
924
 
 
925
 
 
926
 
 
927
 
 
928
 
 
929
void ADSHyperGraph::RemoveNodes(List <Node *> nodeused, List <ADSVar *> varused, bool reduction){
 
930
  List <Subject *> amhedges;
 
931
  List <Subject *> remove;
 
932
  GetHyperEdges(&amhedges);
 
933
  int hedgecount=amhedges.count();
 
934
  bool hedgeremove[200];
 
935
  for (int i=0;i<hedgecount;i++){
 
936
    hedgeremove[i]=False;
 
937
    if (isRemovableHyperEdge((ADSHyperEdge *)amhedges[i],nodeused,varused,reduction)){    
 
938
      remove.add(amhedges[i]);
 
939
      hedgeremove[i]=True;
 
940
    }    
 
941
  }
 
942
 
 
943
  for (remove.first();!remove.done();remove.next()){    
 
944
    // remove.cur() has only one source, due to the reduction rules
 
945
    Subject *node=((HyperEdge *)remove.cur())->GetSubject1()->cur();
 
946
    List <Subject *> newhedges;
 
947
    GetHyperEdges(&newhedges);
 
948
    for (newhedges.first();!newhedges.done();newhedges.next()){
 
949
      List <Subject *> *target=((HyperEdge *)newhedges.cur())->GetSubject2();
 
950
      if (!target) continue;
 
951
      if (!target->contains(node)) continue;
 
952
      // hyperedge newhedges.cur() makes remove.cur() relevant
 
953
      target->remove(node);
 
954
      List <Subject *> *newtarget=((HyperEdge *)remove.cur())->GetSubject2();
 
955
      for (newtarget->first();!newtarget->done();newtarget->next()){
 
956
        target->add(newtarget->cur());
 
957
      }
 
958
      // get the simple edges from remove.cur () and put them in newhedges.cur()
 
959
      // this is necessary for displaying the feedback of the model checker
 
960
      List <Subject *> ls;
 
961
      ((ADSHyperEdge *)remove.cur())->GetEdges(&ls); // the edges in the original activity diagram that are represented by the hyperedge
 
962
      ((ADSHyperEdge *)newhedges.cur())->AddEdges(ls);
 
963
      
 
964
    }
 
965
    
 
966
    RemoveNode((Node *)node); // hyperedge remove.cur() is removed automatically
 
967
  }
 
968
}
 
969
 
 
970
 
 
971
 
 
972
 
 
973
bool ADSHyperGraph::isRemovableHyperEdge(ADSHyperEdge *hedge, List <Node *> nodeused, List <ADSVar *> varused, bool reduction){
 
974
 
 
975
  if (hedge->isconflicting()) return False;
 
976
 
 
977
  List <Subject *> *source=hedge->GetSubject1();
 
978
  List <Subject *> *target=hedge->GetSubject2();
 
979
  
 
980
  if (source->count()>1) return False;
 
981
  source->first();
 
982
  // hedge is non conflicting hyperedge with one source
 
983
  if (!((source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE)||(source->cur()->GetClassType()==Code::ATD_WAIT_STATE_NODE))) return False;
 
984
 
 
985
  // rule1
 
986
  if (nodeused.contains((Node*)source->cur())) return False;
 
987
  bool found=False;
 
988
  for (target->first();!target->done();target->next()){
 
989
    if (nodeused.contains((Node*)target->cur())){
 
990
      found = True;
 
991
      break;
 
992
    }
 
993
  }
 
994
  if (found) return False;
 
995
  for (varused.first();!varused.done();varused.next()){
 
996
    if (hedge->refersto(varused.cur())){
 
997
      found=True;
 
998
      break;
 
999
    }
 
1000
  }
 
1001
  if (found)return False;
 
1002
 
 
1003
  // rule 2
 
1004
  if   (NodeReferredToBySomeInpredicate(source->cur())) return False;
 
1005
  for (target->first();!target->done();target->next()){
 
1006
    if (NodeReferredToBySomeInpredicate(target->cur())){
 
1007
      found=True;
 
1008
      break;
 
1009
    }
 
1010
  }
 
1011
  if (found) return False;
 
1012
 
 
1013
  // rule 3
 
1014
  if (hedge->GetClockConstraint()) return False;
 
1015
 
 
1016
  // rule 4
 
1017
  if ((source->cur()->GetClassType()==Code::ATD_WAIT_STATE_NODE) && !reduction) return False;
 
1018
 
 
1019
 // all rules checked, so both source->cur() and hedges.cur() can be removed
 
1020
  return True;
 
1021
}
 
1022
 
 
1023
 
 
1024
bool ADSHyperGraph::NodeReferredToBySomeInpredicate(Subject *n){
 
1025
  for (hedges->first();!hedges->done();hedges->next()){
 
1026
    if (((ADSHyperEdge*)hedges->cur())->inpredicaterefersto(n)) return True;
 
1027
  }
 
1028
  return False;
 
1029
}
 
1030
 
 
1031
 
 
1032
// used is list of variables used in property   
 
1033
void ADSHyperGraph::RemoveLocalVariables(List <ADSVar *> *usedinprop){
 
1034
  for (varl.first();!varl.done();varl.next()){
 
1035
    // rule 2
 
1036
    if (usedinprop->contains(varl.cur())) continue; // varl.cur() is used in property so skip
 
1037
 
 
1038
 
 
1039
    // rule 1
 
1040
    if (VarUpdatedByTwoActivities(varl.cur())) continue;
 
1041
 
 
1042
    // rule 3
 
1043
    if (VarTestedInHyperEdgeWithoutUpdate(varl.cur())) continue;
 
1044
 
 
1045
    // rule 4 checked elsewhere (eliminate pseudo nodes)
 
1046
 
 
1047
    // varl.cur() can be removed
 
1048
 
 
1049
    // remove varl.cur() from update in activity
 
1050
    for(actlist.first();!actlist.done();actlist.next()){
 
1051
      actlist.cur()->RemoveUpdate(varl.cur());      
 
1052
    }
 
1053
    for(propl.first();!propl.done();){
 
1054
      if (propl.cur()->GetVar()==varl.cur()){
 
1055
        extproplist.remove(propl.cur());
 
1056
        intproplist.remove(propl.cur());  
 
1057
        propl.removecur();
 
1058
      }    
 
1059
      else propl.next();
 
1060
    }
 
1061
    // NOTE varl.cur() is still in hyperedge's varlist
 
1062
    // so printing the hypergraph gives inaccurate information
 
1063
  }
 
1064
}
 
1065
 
 
1066
 
 
1067
// return True iff 
 
1068
// ( there is a hyperedge h such that
 
1069
// v is tested in h's guard h AND 
 
1070
// none of h's sources update v )
 
1071
bool ADSHyperGraph::VarTestedInHyperEdgeWithoutUpdate(ADSVar *v){
 
1072
  List <Subject *> edges;
 
1073
  GetHyperEdges(&edges);
 
1074
  for (edges.first();!edges.done();edges.next()){
 
1075
    if (!((ADSHyperEdge*)edges.cur())->refersto(v)) continue;
 
1076
    // the guard of edges.cur() refers to v
 
1077
    List <Subject *> *source=((HyperEdge *)edges.cur())->GetSubject1();
 
1078
    bool found=False;
 
1079
    for (source->first();!source->done();source->next()){
 
1080
      if (source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
 
1081
        if (((ATDActionStateNode *)source->cur())->GetActivity()->isUpdated(v)){
 
1082
          // v is updated by one of the sources
 
1083
          found=True;
 
1084
        }
 
1085
      }
 
1086
    }
 
1087
    if (!found){  // v is not updated by any of edges.cur()'s sources
 
1088
      return True;
 
1089
    }
 
1090
  }
 
1091
  return False;
 
1092
}
 
1093
 
 
1094
 
 
1095
// return True iff 
 
1096
// ( v is updated by two activities )
 
1097
bool ADSHyperGraph::VarUpdatedByTwoActivities(ADSVar *v){
 
1098
  int actcount=actlist.count();
 
1099
  for (int i=0;i<actcount;i++){
 
1100
    for (int j=i+1;j<actcount;j++){
 
1101
      if ((GetInterference(actlist[i],actlist[j])) &&(actlist[i]->isUpdated(v))&&(actlist[j]->isUpdated(v))){
 
1102
        actlist[i]->Write();
 
1103
        actlist[j]->Write();
 
1104
        List <Subject *> nods;
 
1105
        ATDActionStateNode *activity_i = NULL;  //init?
 
1106
        ATDActionStateNode *activity_j = NULL;  //init?
 
1107
        GetNodes(&nods, Code::ATD_ACTION_STATE_NODE);
 
1108
        for (nods.first();!nods.done();nods.next()){
 
1109
          if (((ATDActionStateNode*)nods.cur())->GetActivity()==actlist[i]){
 
1110
            activity_i=(ATDActionStateNode *)nods.cur();
 
1111
          }
 
1112
          if (((ATDActionStateNode*)nods.cur())->GetActivity()==actlist[j]){
 
1113
            activity_j=(ATDActionStateNode *)nods.cur();
 
1114
          }         
 
1115
        }
 
1116
        ADSSem test;
 
1117
        if (test.inparallel(this,(Subject *)activity_i,(Subject*)activity_j)){
 
1118
          return True;
 
1119
        }
 
1120
      }
 
1121
    }
 
1122
  }
 
1123
  return False;  
 
1124
}
 
1125
 
 
1126