← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/sd/bv/scdiagram.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/scdiagram.c
 
1
////////////////////////////////////////////////////////////////////////////////
 
2
//
 
3
// This file is part of Toolkit for Conceptual Modeling (TCM).
 
4
// (c) copyright 2001, Universiteit Twente.
 
5
// Author: Frank Dehne (frank@cs.vu.nl),
 
6
// David N. Jansen (dnjansen@cs.utwente.nl)
 
7
// Rik Eshuis (eshuis@cs.utwente.nl)
 
8
// Jose Canete (canete@lsi.us.es)
 
9
//
 
10
// TCM is free software; you can redistribute it and/or modify
 
11
// it under the terms of the GNU General Public License as published by
 
12
// the Free Software Foundation; either version 2 of the License, or
 
13
// (at your option) any later version.
 
14
//
 
15
// TCM is distributed in the hope that it will be useful,
 
16
// but WITHOUT ANY WARRANTY; without even the implied warranty of
 
17
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
18
// GNU General Public License for more details.
 
19
//
 
20
// You should have received a copy of the GNU General Public License
 
21
// along with TCM; if not, write to the Free Software
 
22
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 
23
// 02111-1307, USA.
 
24
////////////////////////////////////////////////////////////////////////////////
 
25
#include "scgraph.h"
 
26
#include "scwindow.h"
 
27
#include "textbox.h"
 
28
#include "comment.h"
 
29
#include "commentlink.h"
 
30
#include "scdiagram.h"
 
31
#include "roundedbox.h"
 
32
#include "scdandstatebox.h"
 
33
#include "scdorstate.h"
 
34
#include "scdandstate.h"
 
35
#include "scdandedge.h"
 
36
#include "scdtransitionedge.h"
 
37
#include "scdandline.h"
 
38
#include "blackdot.h"
 
39
#include "bullseye.h"
 
40
#include "minidiamond.h"
 
41
#include "solidhorizontalbar.h"
 
42
#include "solidverticalbar.h"
 
43
#include "note.h"
 
44
#include "notebox.h"
 
45
#include "scddefaultstate.h"
 
46
#include "scdfinalstate.h"
 
47
#include "scddecisionstate.h"
 
48
#include "scdsynchronizationstate.h"
 
49
#include "scviewer.h"
 
50
 
 
51
#ifdef MODELCHECK
 
52
#include "modelcheckdialog.h"
 
53
//#include "scdsmv.h"
 
54
#include <ctype.h>
 
55
#endif
 
56
 
 
57
#include "outputfile.h"
 
58
 
 
59
#include "adsmcoutputparse.h"
 
60
#include "adsedgelabelparse.h"
 
61
 
 
62
#include <limits.h>
 
63
#include <stdlib.h>
 
64
#include <unistd.h>
 
65
 
 
66
SCDiagram::SCDiagram(Config *c, SCWindow *d, SCViewer *v, SCGraph *g): 
 
67
                Diagram(c,d,v,g) {
 
68
        UpdateNodeType(1);
 
69
        UpdateEdgeType(1);
 
70
//      GetReplaceDialog()->ManageNameOnlyToggle(True);
 
71
//      scChecks = new SCChecks(this,g);
 
72
#ifdef MODELCHECK
 
73
        promptDialog = new ModelCheckDialog(GetMainWindow()->GetWidget());
 
74
        promptDialog->Initialize();
 
75
#endif
 
76
}
 
77
 
 
78
 
 
79
SCDiagram::~SCDiagram() {
 
80
#ifdef MODELCHECK
 
81
        delete promptDialog;
 
82
#endif
 
83
//      delete scChecks;
 
84
}
 
85
 
 
86
 
 
87
/* virtual */ void SCDiagram::Initialize() {
 
88
        Diagram::Initialize();
 
89
        SetHierarchic(True);
 
90
}
 
91
 
 
92
 
 
93
Thing *SCDiagram::CreateThing(int classNr) {
 
94
        Grafport *g = GetDiagramViewer()->GetGrafport();
 
95
        ShapeView *v = GetDiagramViewer()->GetCurView();
 
96
        SCGraph *sg = (SCGraph *)GetGraph();
 
97
        Thing *thing = 0;
 
98
        switch ( classNr ) {
 
99
        // view
 
100
        case Code::VIEW:
 
101
                thing = new ShapeView(GetDiagramViewer());
 
102
                break;
 
103
 
 
104
        // node shapes
 
105
        case Code::ROUNDED_BOX:
 
106
                thing = new RoundedBox(v, g, 0, 0);
 
107
                break;
 
108
        case Code::SCD_AND_STATE_BOX:
 
109
                thing = new SCDAndStateBox(v, g, 0, 0);
 
110
                break;
 
111
        case Code::TEXT_BOX:
 
112
                thing = new TextBox(v, g, 0, 0); 
 
113
                break;
 
114
        case Code::BLACK_DOT:
 
115
                thing = new BlackDot(v, g, 0, 0);
 
116
                break;
 
117
        case Code::BULLS_EYE:
 
118
                thing = new BullsEye(v, g, 0, 0);
 
119
                break;
 
120
        case Code::MINI_DIAMOND:
 
121
                thing = new MiniDiamond(v, g, 0, 0);
 
122
                break;
 
123
        case Code::SOLID_HORIZONTAL_BAR:
 
124
                thing = new SolidHorizontalBar(v, g, 0, 0);
 
125
                break;
 
126
        case Code::SOLID_VERTICAL_BAR:
 
127
                thing = new SolidVerticalBar(v, g, 0, 0);
 
128
                break;
 
129
        case Code::NOTE_BOX:
 
130
                thing = new NoteBox(v, g, 0, 0);
 
131
                break;
 
132
 
 
133
        // lines
 
134
        case Code::LINE:
 
135
                thing = new Line(v, g, 0, 0, 0);
 
136
                break;
 
137
//      case Code::ARROW:
 
138
//              Line *line = new Line(v, g, 0, 0, 0);
 
139
//              line->SetEnd1(LineEnd::EMPTY);
 
140
//              line->SetEnd2(LineEnd::FILLED_ARROW);
 
141
//              thing = line;
 
142
//              break;
 
143
        case Code::SCD_AND_LINE:
 
144
                thing = new SCDAndLine(v, g, 0, 0);
 
145
                break;
 
146
 
 
147
        // nodes
 
148
        case Code::SCD_AND_STATE:
 
149
                thing = new SCDAndState(sg);
 
150
                break;
 
151
        case Code::SCD_DECISION_STATE:
 
152
                thing = new SCDDecisionState(sg);
 
153
                break;
 
154
        case Code::SCD_DEFAULT_STATE:
 
155
                thing = new SCDDefaultState(sg);
 
156
                break;
 
157
        case Code::SCD_FINAL_STATE:
 
158
                thing = new SCDFinalState(sg);
 
159
                break;
 
160
        case Code::SCD_OR_STATE:
 
161
                thing = new SCDOrState(sg);
 
162
                break;
 
163
        case Code::SCD_SYNCHRONIZATION_STATE:
 
164
                thing = new SCDSynchronizationState(sg);
 
165
                break;
 
166
        case Code::COMMENT:
 
167
                thing = new Comment(sg);
 
168
                break;
 
169
        case Code::NOTE:
 
170
                thing = new Note(sg);
 
171
                break;
 
172
 
 
173
        // edges
 
174
        case Code::SCD_TRANSITION_EDGE:
 
175
                thing = new SCDTransitionEdge(sg, 0, 0);
 
176
                break;
 
177
        case Code::SCD_AND_EDGE:
 
178
                thing = new SCDAndEdge(sg, 0, 0);
 
179
                break;
 
180
        case Code::COMMENT_LINK:
 
181
                thing = new CommentLink(sg, 0, 0);
 
182
                break;
 
183
        default:
 
184
                error("%s, line %d: impl error: "
 
185
                        "wrong class number %d\n", __FILE__, __LINE__, classNr);
 
186
        }
 
187
        return thing;
 
188
}
 
189
 
 
190
 
 
191
Node *SCDiagram::CreateNode() {
 
192
        Node *node = 0;
 
193
        SCGraph *sg = (SCGraph *)GetGraph();
 
194
        switch ( GetNodeType() ) {
 
195
        case Code::SCD_AND_STATE:
 
196
                node = new SCDAndState(sg);
 
197
                break;
 
198
        case Code::SCD_DECISION_STATE:
 
199
                node = new SCDDecisionState(sg);
 
200
                break;
 
201
        case Code::SCD_DEFAULT_STATE:
 
202
                node = new SCDDefaultState(sg);
 
203
                break;
 
204
        case Code::SCD_FINAL_STATE:
 
205
                node = new SCDFinalState(sg);
 
206
                break;
 
207
        case Code::SCD_OR_STATE:
 
208
                node = new SCDOrState(sg);
 
209
                break;
 
210
        case Code::SCD_SYNCHRONIZATION_STATE:
 
211
                node = new SCDSynchronizationState(sg);
 
212
                break;
 
213
        case Code::COMMENT:
 
214
                node = new Comment(sg);
 
215
                break;
 
216
        case Code::NOTE:
 
217
                node = new Note(sg);
 
218
                break;
 
219
        default:
 
220
                error("%s, line %d: impl error: "
 
221
                        "unknown node type\n", __FILE__, __LINE__);
 
222
        }
 
223
        return node;
 
224
}
 
225
 
 
226
 
 
227
Edge *SCDiagram::CreateEdge(Subject *subj1, Subject *subj2){
 
228
        if ( ! CheckEdgeConstraints(subj1, subj2) )
 
229
                return 0;
 
230
        Edge *edge = 0;
 
231
        SCGraph *sg = (SCGraph *)GetGraph();
 
232
        switch ( GetEdgeType() ) {
 
233
        case Code::SCD_TRANSITION_EDGE:
 
234
                edge = new SCDTransitionEdge(sg, subj1, subj2);
 
235
                break;
 
236
        case Code::SCD_AND_EDGE:
 
237
                if ( ! CheckAndEdgeConstraints(subj1, subj2) )
 
238
                        return 0;
 
239
                edge = new SCDAndEdge(sg, subj1, subj2);
 
240
                break;
 
241
        case Code::COMMENT_LINK:
 
242
                edge = new CommentLink(sg, subj1, subj2);
 
243
                break;
 
244
        default:
 
245
                error("%s, line %d: impl error: "
 
246
                        "unknown edge type\n", __FILE__, __LINE__);
 
247
        }
 
248
        return edge;
 
249
}
 
250
 
 
251
 
 
252
NodeShape *SCDiagram::CreateNodeShape(Node *node, int x, int y) {
 
253
        NodeShape *shape = 0;
 
254
        Grafport *g = GetDiagramViewer()->GetGrafport();
 
255
        ShapeView *v = GetDiagramViewer()->GetCurView();
 
256
        switch ( GetNodeShapeType() ) {
 
257
        case Code::ROUNDED_BOX:
 
258
                shape = new RoundedBox(v, g, x, y);
 
259
                break;
 
260
        case Code::SCD_AND_STATE_BOX:
 
261
                shape = new SCDAndStateBox(v, g, x, y);
 
262
                break;
 
263
        case Code::TEXT_BOX:
 
264
                shape = new TextBox(v, g, x, y);
 
265
                break;
 
266
        case Code::NOTE_BOX:
 
267
                shape = new NoteBox(v, g, x, y);
 
268
                break;
 
269
        case Code::BLACK_DOT:
 
270
                shape = new BlackDot(v, g, x, y);
 
271
                break;
 
272
        case Code::BULLS_EYE:
 
273
                shape = new BullsEye(v, g, x, y);
 
274
                break;
 
275
        case Code::MINI_DIAMOND:
 
276
                shape = new MiniDiamond(v, g, x, y);
 
277
                break;
 
278
        case Code::SOLID_HORIZONTAL_BAR:
 
279
                shape = new SolidHorizontalBar(v, g, x, y);
 
280
                break;
 
281
        case Code::SOLID_VERTICAL_BAR:
 
282
                shape = new SolidVerticalBar(v, g, x, y);
 
283
                break;
 
284
        default:
 
285
                error("%s, line %d: impl error: "
 
286
                        "node shape type does not exist\n", __FILE__, __LINE__);
 
287
        }
 
288
        if (check(shape)) {
 
289
                shape->SetSubject(node);
 
290
                shape->SetTextShape();
 
291
        }
 
292
        return shape;
 
293
}
 
294
 
 
295
 
 
296
Line *SCDiagram::CreateLine(
 
297
                Edge *edge, GShape *from, GShape *to, List<Point *> *l) {
 
298
        Line *line = 0;
 
299
        Grafport *g = GetDiagramViewer()->GetGrafport();
 
300
        ShapeView *v = GetDiagramViewer()->GetCurView();
 
301
//      *((*l)[0]) = *(from->GetPosition());
 
302
//      *((*l)[l->count()-1]) = *(to->GetPosition());
 
303
        switch ( GetLineType() ) {
 
304
        case Code::LINE:
 
305
                line = new Line(v, g, from, to, l, IsCurve());
 
306
                break;
 
307
        case Code::SCD_AND_LINE:
 
308
                line = new SCDAndLine(v, g, from, l, IsCurve());
 
309
                break;
 
310
        default:
 
311
                error("%s, line %d: impl error: "
 
312
                        "line type does not exist\n", __FILE__, __LINE__);
 
313
        }
 
314
 
 
315
        if (check(line)) {
 
316
                line->SetSubject(edge);
 
317
                line->SetTextShape();
 
318
//              line->SetEnd1(GetLineEnd1());
 
319
                line->SetEnd2(GetLineEnd2());
 
320
        }
 
321
        return line;
 
322
}
 
323
 
 
324
 
 
325
void SCDiagram::UpdateNodeType(int num) {
 
326
        ((DiagramWindow *)GetMainWindow())->SetNodeName(num);
 
327
        switch (num) {
 
328
        case 1: SetNodeType(Code::SCD_OR_STATE);
 
329
                SetNodeShapeType(Code::ROUNDED_BOX);
 
330
                break;
 
331
        case 2: SetNodeType(Code::SCD_AND_STATE);
 
332
                SetNodeShapeType(Code::SCD_AND_STATE_BOX);
 
333
                break;
 
334
        case 3: SetNodeType(Code::SCD_DEFAULT_STATE);
 
335
                SetNodeShapeType(Code::BLACK_DOT);
 
336
                break;
 
337
        case 4: SetNodeType(Code::SCD_FINAL_STATE);
 
338
                SetNodeShapeType(Code::BULLS_EYE);
 
339
                break;
 
340
        case 5: SetNodeType(Code::COMMENT);
 
341
                SetNodeShapeType(Code::TEXT_BOX);
 
342
                break;
 
343
        case 6: SetNodeType(Code::SCD_DECISION_STATE);
 
344
                SetNodeShapeType(Code::MINI_DIAMOND);
 
345
                break;
 
346
        case 7: SetNodeType(Code::SCD_SYNCHRONIZATION_STATE);
 
347
                SetNodeShapeType(Code::SOLID_HORIZONTAL_BAR);
 
348
                break;
 
349
        case 8: SetNodeType(Code::SCD_SYNCHRONIZATION_STATE);
 
350
                SetNodeShapeType(Code::SOLID_VERTICAL_BAR);
 
351
                break;
 
352
        case 9: SetNodeType(Code::NOTE);
 
353
                SetNodeShapeType(Code::NOTE_BOX);
 
354
                break;
 
355
 
 
356
        default:
 
357
                error("%s, line %d: impl error: "
 
358
                        "unknown node type selected\n", __FILE__,__LINE__);
 
359
        }
 
360
}
 
361
 
 
362
 
 
363
void SCDiagram::UpdateEdgeType(int num) {
 
364
        ((DiagramWindow *)GetMainWindow())->SetEdgeName(num);
 
365
        switch(num) {
 
366
        case 1: SetEdgeType(Code::SCD_TRANSITION_EDGE);
 
367
                SetLineType(Code::LINE);
 
368
                SetEdgeLineStyle(LineStyle::SOLID);
 
369
//              SetLineEnd1(LineEnd::EMPTY);
 
370
                SetLineEnd2(LineEnd::FILLED_ARROW);
 
371
                break;
 
372
        case 2: SetEdgeType(Code::COMMENT_LINK);
 
373
                SetLineType(Code::LINE);
 
374
                SetEdgeLineStyle(LineStyle::WIDE_DOTTED);
 
375
//              SetLineEnd1(LineEnd::EMPTY);
 
376
                SetLineEnd2(LineEnd::EMPTY);
 
377
                break;
 
378
        case 3: SetEdgeType(Code::SCD_AND_EDGE);
 
379
                SetLineType(Code::SCD_AND_LINE);
 
380
                SetEdgeLineStyle(LineStyle::DASHED);
 
381
//              SetLineEnd1(LineEnd::EMPTY);
 
382
                SetLineEnd2(LineEnd::EMPTY);
 
383
                break;
 
384
        default:
 
385
                error("%s, line %d: impl error: "
 
386
                        "unknown edge type selected\n", __FILE__,__LINE__);
 
387
        }
 
388
}
 
389
 
 
390
 
 
391
bool SCDiagram::CheckAndEdgeConstraints(Subject *subj1, Subject *subj2) {
 
392
        if ( subj1->GetClassType() != Code::SCD_AND_STATE ) {
 
393
                ShowDialog(MessageDialog::ERROR, "Error",
 
394
                        "An and-line must begin at an and-state");
 
395
                return False;
 
396
        }
 
397
        if ( subj1 != subj2 ) {
 
398
                ShowDialog(MessageDialog::ERROR, "Error",
 
399
                        "An and-line must begin and end at the same state");
 
400
                return False;
 
401
        }
 
402
 
 
403
// ----> Hier toevoegen: check that an and-edge lies inside its and-shape.
 
404
 
 
405
        return True;
 
406
}
 
407
 
 
408
 
 
409
 
 
410
bool SCDiagram::CheckEdgeConstraints(Subject *subj1, Subject *subj2) {
 
411
        // Check possible connections (subj-subj-edge matrix).
 
412
        if (!CheckConnection(subj1, subj2))
 
413
                return False;
 
414
        return True;
 
415
}
 
416
 
 
417
 
 
418
//bool SCDiagram::SetEvent(Transition *t, const string *s) {
 
419
//      List<GShape *> shapes;
 
420
//      GetDiagramViewer()->GetShapes(t, &shapes);
 
421
//      Subject::NameErrType n = t->SetEvent(s);
 
422
//      if (n == Subject::OK) {
 
423
//              if (shapes.first())
 
424
//                      do
 
425
//                              ((TransitionArrow *)shapes.cur())->UpdateEvent(s);
 
426
//                      while (shapes.next());
 
427
//              else {
 
428
//                      error("%s, line %d: shape does not exist\n", 
 
429
//                                      __FILE__, __LINE__);
 
430
//                      return False;
 
431
//              }
 
432
//              return True;
 
433
//      }
 
434
//      else if (n == Subject::IMPOSSIBLE_NAME) {
 
435
//              string msg = "'" + *s + "' wrong syntax\n for an event string";
 
436
//              ShowDialog(MessageDialog::ERROR, "Error", &msg);
 
437
//              return False;
 
438
//      }
 
439
//      else if (n == Subject::DOUBLE_EDGE) {
 
440
//              string msg = "there is already a transition with\n"
 
441
//                      "event string '" + *s + "' between this pair of states";
 
442
//              ShowDialog(MessageDialog::ERROR, "Error", &msg);
 
443
//              return False;
 
444
//      }
 
445
//      else {
 
446
//              error("%s, line %d: case not handled\n", __FILE__, __LINE__);
 
447
//      }
 
448
//      return True;
 
449
//}
 
450
 
 
451
 
 
452
//bool SCDiagram::SetAction(Subject *t, const string *s, unsigned nr) {
 
453
//      List<GShape *> shapes;
 
454
//      GetDiagramViewer()->GetShapes(t, &shapes);
 
455
//      unsigned m = nr;
 
456
//      // split string in different one line strings.
 
457
//      string ss(*s);
 
458
//      char *str = (char *)ss.getstr();
 
459
//      char empty[2] = "";
 
460
//      char *x = strtok(str, "\r");
 
461
//      if (x == 0)
 
462
//              x = empty;
 
463
//      while (x != 0) {
 
464
//              string *ns = new string(x);
 
465
//              bool update = True;
 
466
//              Subject::NameErrType result;
 
467
//              if (m == nr) {
 
468
//                      if (t->IsEdge())
 
469
//                              result = ((Transition *)t)->SetAction(ns, m, True);
 
470
//                      else
 
471
//                              result = ((InitialState *)t)->SetAction(ns, m, True);
 
472
//              }
 
473
//              else {
 
474
//                      if (t->IsEdge())
 
475
//                              result = ((Transition *)t)->SetAction(ns, m, False);
 
476
//                      else
 
477
//                              result = ((InitialState *)t)->SetAction(ns, m, False);
 
478
//                      update = False;
 
479
//              }
 
480
//              if (result != Subject::OK) {
 
481
//                      string msg;
 
482
//                      if (result == Subject::HAS_ACTION)
 
483
//                              msg = "transition already has an action '" + *ns + "'";
 
484
//                      else
 
485
//                              msg = "'" + *ns + "' wrong syntax\n for an action string";
 
486
//                      ShowDialog(MessageDialog::ERROR, "Error", &msg);
 
487
//                      // make actions empty.
 
488
//                      *ns = "";
 
489
//                      if (!update) {
 
490
//                              for (shapes.first(); !shapes.done(); shapes.next()) {
 
491
//                                      if (t->IsEdge())
 
492
//                                              ((TransitionArrow *)shapes.cur())->
 
493
//                                                      UpdateAction(ns, m, update);
 
494
//                                      else
 
495
//                                              ((InitialStateBox *)shapes.cur())->
 
496
//                                                      UpdateAction(ns, m, update);
 
497
//                              }
 
498
//                      } 
 
499
//                      delete ns;
 
500
//                      return False;
 
501
//              }
 
502
//              // update the shapes.
 
503
//              if (shapes.first())
 
504
//                      do {
 
505
//                              if (t->IsEdge())
 
506
//                                      ((TransitionArrow *)shapes.cur())->
 
507
//                                              UpdateAction(ns, m, update);
 
508
//                              else
 
509
//                                      ((InitialStateBox *)shapes.cur())->
 
510
//                                              UpdateAction(ns, m, update);
 
511
//                      } while (shapes.next());
 
512
//              else {
 
513
//                      error("%s, line %d: shape does not exist\n", 
 
514
//                                      __FILE__, __LINE__);
 
515
//                      return False;
 
516
//              }
 
517
//              m++;
 
518
//              x = strtok(0, "\r");
 
519
//              delete ns;
 
520
//      }
 
521
//      return True;
 
522
//}
 
523
 
 
524
 
 
525
//InitialState *SCDiagram::FindInitialState(Subject *state) {
 
526
//      if (state->GetClassType() == Code::INITIAL_STATE)
 
527
//              return (InitialState *)state;
 
528
//      List<Subject *> initStates;
 
529
//      GetGraph()->GetNodes(&initStates, Code::INITIAL_STATE);
 
530
//      for (initStates.first(); !initStates.done(); initStates.next()) {
 
531
//              InitialState *init = (InitialState *)initStates.cur();
 
532
//              if (GetGraph()->UndirectedPathExists(init, state))
 
533
//                      return init;
 
534
//      } 
 
535
//      return 0;
 
536
//}
 
537
 
 
538
 
 
539
void SCDiagram::CheckDocument() {
 
540
        chkbuf = "";
 
541
        unsigned total = 0;
 
542
//      total += scChecks->CheckNamelessNodes(Code::INITIAL_STATE, chkbuf);
 
543
//      total += scChecks->CheckNamelessNodes(Code::STATE, chkbuf);
 
544
//      total += scChecks->CheckNamelessNodes(Code::DECISION_POINT, chkbuf);
 
545
//      total += scChecks->CheckDoubleNodes(Code::STATE, chkbuf);
 
546
//      total += scChecks->CheckDoubleNodes(Code::DECISION_POINT, chkbuf);
 
547
//      total += scChecks->CheckDoubleEvents(chkbuf);
 
548
//      total += scChecks->CheckEmptyEvents(chkbuf);
 
549
//      total += scChecks->CheckEmptyActions(chkbuf);
 
550
//      total += scChecks->CheckNoActions(chkbuf);
 
551
//      total += scChecks->CheckCountEdgesFrom(Code::DECISION_POINT, 
 
552
//              Code::TRANSITION, 2, INT_MAX, False, False, chkbuf);
 
553
//      int sub = scChecks->CheckNodeCount(1, Code::INITIAL_STATE, chkbuf);
 
554
//      total += sub;
 
555
//      if (sub == 0) {
 
556
//              total += scChecks->CheckReachability(
 
557
//                      Code::INITIAL_STATE, Code::STATE, False, chkbuf);
 
558
//              total += scChecks->CheckReachability(
 
559
//                      Code::INITIAL_STATE, Code::DECISION_POINT, False, chkbuf);
 
560
//      }
 
561
        ReportCheck(total, &chkbuf);
 
562
}
 
563
 
 
564
 
 
565
#ifdef MODELCHECK
 
566
void SCDiagram::ModelCheckProperty() {
 
567
        SetStatus("action: model check document semantics");
 
568
        promptDialog->SetTitle("Model check document semantics");
 
569
        promptDialog->SetOKCallback(ModelCheckDocumentOKCB, this);
 
570
        promptDialog->Popup();
 
571
}
 
572
 
 
573
 
 
574
/* static */ void SCDiagram::ModelCheckDocumentOKCB(Widget,
 
575
                XtPointer clientData, XtPointer)
 
576
{
 
577
        SCDiagram *scd = (SCDiagram *)clientData;
 
578
        string formula, internal, clock;
 
579
        scd->promptDialog->GetFormulaString(&formula);
 
580
        scd->promptDialog->GetInternString(&internal);
 
581
        scd->promptDialog->GetClockString(&clock);
 
582
        scd->DoModelCheckDocument(&internal, &formula, &clock);
 
583
}
 
584
 
 
585
 
 
586
//void SCDiagram::DoModelCheckDocument(const string *internal,
 
587
//                      const string *formula, const string *clock)
 
588
//{
 
589
//      SetStatus("action: model check document semantics");
 
590
//      GetMainWindow()->SetCursor(MouseCursor::WATCH);
 
591
//      string tmpModel;
 
592
//tmpModel = "model";
 
593
////    GetViewer()->GetPrinter()->MakeTmpFile(&tmpModel);
 
594
//      tmpModel += ".smv";
 
595
//std::cerr << "Temporary model file: " << tmpModel.getstr() << "\n";
 
596
//
 
597
//      SaveForModelChecker(&tmpModel, internal, clock, formula);
 
598
//      bool ok = ExecuteModelChecker(&tmpModel, formula);
 
599
//      GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
 
600
////    unlink(tmpModel.getstr());
 
601
//      if ( ! ok )
 
602
//              SetStatus("model checking aborted");
 
603
//      else
 
604
//              SetStatus("model checking completed");
 
605
//      return;
 
606
//}
 
607
 
 
608
 
 
609
void SCDiagram::DoModelCheckDocument(const string *internal,
 
610
                        const string *formula, const string *clock)
 
611
{
 
612
        SetStatus("action: model check document semantics");
 
613
        GetMainWindow()->SetCursor(MouseCursor::WATCH);
 
614
        string tmpModel;
 
615
        tmpModel = "model";
 
616
//      GetViewer()->GetPrinter()->MakeTmpFile(&tmpModel);
 
617
        tmpModel += ".smv";
 
618
        std::cout << "Temporary model file: " << tmpModel.getstr() << '\n';
 
619
 
 
620
        OutputFile *ofile2= new OutputFile();
 
621
        ofile2->Open(&tmpModel);
 
622
        SCGraph *scg=(SCGraph *)this->GetGraph();
 
623
        scg->WriteNuSMV(ofile2,True);
 
624
        string f=*formula;
 
625
        (*ofile2) << "\nSPEC\n" << f<< "\n";
 
626
        ofile2->Close();
 
627
        
 
628
        //      SaveForModelChecker(&tmpModel, internal, clock, formula);
 
629
        //      bool ok = ExecuteModelChecker(&tmpModel, formula);
 
630
 
 
631
        GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
 
632
 
 
633
 
 
634
 
 
635
 
 
636
//      unlink(tmpModel.getstr());
 
637
        //      if ( ! ok )
 
638
        //              SetStatus("model checking aborted");
 
639
        //      else
 
640
        //              SetStatus("model checking completed");
 
641
 
 
642
 
 
643
 
 
644
 
 
645
  char output[6];
 
646
  strcpy(output,"XXXXXX");
 
647
  (void)mktemp(output); // replaces the six X's with a string that can be used to create a unique file name 
 
648
 
 
649
  string command = "NuSMV model.smv > ";
 
650
  string outputfile= output;
 
651
  outputfile += ".out";
 
652
 
 
653
  command = command + outputfile;
 
654
  std::cout << "Executing command\t" << command;
 
655
  system(command.getstr()); // do the actual model checking
 
656
  std::cout.flush();
 
657
  std::cerr.flush();
 
658
 
 
659
 
 
660
  // parse the model checker's output
 
661
  ::adsmcoutputin=fopen(outputfile.getstr(),"r");
 
662
  ::mctraceindex=0;
 
663
  ::statecounter=0;
 
664
  ::sourceindex=0;
 
665
  ::targetindex=0;
 
666
  ::enabledindex=0;
 
667
  ::eventIndex=0;
 
668
  for (int i=0; i<2000; i++) ::isStable[i]= 0;
 
669
 
 
670
  bool b=adsmcoutputparse(); 
 
671
  if (b) {
 
672
    error("I couldn't parse the model checker's output\n"); 
 
673
    return ;
 
674
  }
 
675
  
 
676
  string mctxt;
 
677
  if (!mcfeedback) {
 
678
    mctxt="The requirement is satisfied\n";
 
679
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
 
680
  }
 
681
  else{
 
682
    mctxt="The requirement is not satisfied; see the counter example\n";
 
683
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
 
684
    AbstractSequenceDiagram *asd= GenerateAbstractSequenceDiagram();
 
685
    ConcreteSequenceDiagram *csd= GenerateConcreteSeqDiag(asd);
 
686
    GenerateSeqDiagFile(csd, formula);    
 
687
  }
 
688
 
 
689
  GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
 
690
  unlink(output); // cleanup buf
 
691
  //  unlink(req);
 
692
  //  unlink(buf); // cleanup if wanted 
 
693
 
 
694
  return;
 
695
}
 
696
 
 
697
void SCDiagram::SaveForModelChecker(const string *path, const string *internal,
 
698
                        const string * clock, const string *formula) {
 
699
        /* Split internal into a list of strings */
 
700
        List<string> intevent;
 
701
        if ( internal ) {
 
702
                const char *cp = internal->getstr();
 
703
                while ( *cp ) {
 
704
                        while ( *cp && isspace(*cp) )
 
705
                                ++cp;
 
706
                        if ( ! *cp )
 
707
                                break;
 
708
                        const char *ep = cp;
 
709
                        if ( '[' == *cp ) {
 
710
                                while ( *++ep )
 
711
                                        if ( ']' == *ep ) {
 
712
                                                ++ep;
 
713
                                                break;
 
714
                                        }
 
715
                        } else
 
716
                                while ( *++ep && ! isspace(*ep) && '[' != *ep )
 
717
                                        ;
 
718
                        string event;
 
719
                        event.add(cp, ep - cp);
 
720
                        intevent.add(event);
 
721
                        cp = ep;
 
722
                }
 
723
        }
 
724
 
 
725
        //      SCDSMV s(GetGraph());
 
726
        //      s.WriteSMV(path->getstr(), &intevent, formula);
 
727
}
 
728
 
 
729
 
 
730
bool SCDiagram::ExecuteModelChecker(const string *path, const string *formula) {
 
731
        return False;
 
732
}
 
733
 
 
734
 
 
735
 
 
736
List<SCDTransitionEdge *> SCDiagram::ComputeMicroStep (SCGraph *gr, int state)
 
737
{
 
738
  /* This function takes the graph and the number of a state in the NuSMV counterexample trace. It computes the
 
739
     transitions to be fired from state to state+1, i.e., the transitions in the microstep.
 
740
     Please note that the states are numbered from 0 to ::statecounter-1.
 
741
  */
 
742
 
 
743
 
 
744
  // state refers to an state of the Kripke structure
 
745
 
 
746
  
 
747
  
 
748
  List<SCDTransitionEdge *> enabledTrans, step;
 
749
  List<Subject *> hedges;
 
750
  int i;
 
751
  int nextState;
 
752
  int st;
 
753
  int ev;
 
754
  int aux;
 
755
  int ntrans;
 
756
  bool found;
 
757
  bool fired;
 
758
 
 
759
 
 
760
 
 
761
 
 
762
  if (state >=0 && state < ::statecounter){
 
763
 
 
764
    nextState= state +1;
 
765
 
 
766
    
 
767
    i=0;
 
768
 
 
769
 
 
770
    while ((i<(::enabledindex))&&(enabledstatenumber[i]<state))
 
771
           i++;
 
772
    if (enabledstatenumber[i]>state) // if there is no enabled transition in the specified state of the Kripke Structure (KS)
 
773
      return step; //empty
 
774
 
 
775
    // Now enabledhyperedge[i] (and possibly some of its followers) is an enabled transition in KS state.
 
776
    // We collect all the corresponding SCDTransitionEdge objects in the list "enabledTrans",
 
777
    // using the information contained in enabledhyperedge (which come from the NuSMV output).
 
778
 
 
779
    gr->GetEdges(&hedges);
 
780
 
 
781
 
 
782
    for (int k=i; k<(::enabledindex) && enabledstatenumber[k]==state; k++){
 
783
       for (hedges.first();!hedges.done();hedges.next()){
 
784
        if ((int)hedges.cur()->GetId()==enabledhyperedge[k]){   
 
785
            enabledTrans.add((SCDTransitionEdge *)hedges.cur()); // the enabled hyperedges in "state"
 
786
            break; // hyperedge found, so abort loop
 
787
        }
 
788
      }
 
789
    }
 
790
 
 
791
    // Now enabledTrans contains all the enabled transitions in the specified state.
 
792
 
 
793
    ntrans= enabledTrans.count();
 
794
 
 
795
      
 
796
    for (int et=0; et< ntrans; et++){  //for each enabled transition et
 
797
 
 
798
          // We will infer if the transition is taken as in Chan's paper:
 
799
          //  - in the next state, its target is set to one
 
800
          //  - in the next state, the possible action event is set to one
 
801
 
 
802
          // First we look for the states which are true in the next state.
 
803
          // Remember that in targetname we have all the states which are true in the trace.
 
804
          found= False;
 
805
          st=0;
 
806
          while (st < targetindex && !found)
 
807
            if (targetstatenumber[st]==nextState)
 
808
              found= True;
 
809
            else
 
810
              st++;
 
811
          // Now in targetname[st] (and possibly, in some of its followers) we have a state that will been entered in the next state
 
812
          // of the KS.
 
813
          // We check if the target state of et is in the set of states which will been entered in the next state.
 
814
          found= False;
 
815
          while (st < targetindex && targetstatenumber[st]==nextState && !found)
 
816
            if (strcmp(targetname[st], enabledTrans[et]->GetSubject2()->GetName()->getstr())==0)
 
817
              found= True;
 
818
            else
 
819
              st++;
 
820
          
 
821
          if (found){
 
822
            if (enabledTrans[et]->GetSendEvent()==NULL) // the transition hasn't send event
 
823
              fired= True;
 
824
            else { // et has send event
 
825
                    
 
826
              // Now we have to check that the possible action event of et is sent in the next state.
 
827
              found= False;
 
828
              ev= 0;
 
829
              while (ev < eventIndex && !found)
 
830
                if (occurredEventStates[ev]==nextState)
 
831
                  found= True;
 
832
                else
 
833
                  ev++;
 
834
 
 
835
              // Now in occurredEvents[ev] (and possibly, in the followers) we have an event which will occur in the next state of the KS.
 
836
              // We check that the send event of et is in the set of occurred events in the next state of the KS.
 
837
              found= False;
 
838
              while (ev < eventIndex && occurredEventStates[ev]==nextState && !found)
 
839
                if (strcmp(occurredEvents[ev], enabledTrans[et]->GetSendEvent()->GetName().getstr())==0)
 
840
                  found= True;
 
841
                else
 
842
                  ev++;
 
843
              
 
844
              fired= found;
 
845
 
 
846
            }
 
847
          }
 
848
          else
 
849
            fired= False;
 
850
          
 
851
          
 
852
          if (fired) //then we add the transition to the step
 
853
            step.add (enabledTrans[et]);
 
854
    }
 
855
 
 
856
  }
 
857
  return step;
 
858
} 
 
859
 
 
860
 
 
861
 
 
862
 
 
863
AbstractSequenceDiagram * SCDiagram::GenerateAbstractSequenceDiagram ()
 
864
{
 
865
 
 
866
  AbstractSequenceDiagram *asd;
 
867
  int currentState; // current state of the Kripke structure
 
868
  int formerState; // state of the Kripke structure where the last processed event was produced
 
869
  int ev; // counter for events
 
870
  InteractionRow * row;
 
871
  SCGraph *theGraph;
 
872
  Prop *prop;
 
873
  string str;
 
874
  List<SCDTransitionEdge *> step;
 
875
 
 
876
  
 
877
  theGraph= (SCGraph *)GetGraph();
 
878
 
 
879
 
 
880
  asd= new AbstractSequenceDiagram;
 
881
  str= "Environment";
 
882
  asd->AddParticipant(str);
 
883
  str= "System";
 
884
  asd->AddParticipant(str);
 
885
 
 
886
  
 
887
  formerState= -1;
 
888
  
 
889
  for (ev=0; ev<eventIndex; ev++){
 
890
    
 
891
    // First let's see if ev is really an event (note that it can also be stable (from stable = 1),
 
892
    // events (from events = 1), and so on. If it is an event, it will be in the property list of the graph
 
893
    // and will have an appropiate type.
 
894
    prop= theGraph->EventInPropl(occurredEvents[ev]);
 
895
    if (prop && (prop->GetType()==::EV_FROM_ENV ||
 
896
                 prop->GetType()==::EV_TO_ENV ||
 
897
                 prop->GetType()==::EV_INT)){ //ok, it is an event!
 
898
        currentState= ::occurredEventStates[ev];
 
899
        if (formerState != currentState) //we need a new row!
 
900
            row= asd->AddRow(currentState); //add a new row with the correct number of columns; it also returns the row
 
901
        
 
902
        // row is the current row in which we have to include the event
 
903
        if (prop->GetType()==::EV_FROM_ENV)
 
904
            row->participants[0].AddPairObjEv(1,prop->GetName());
 
905
        else if (prop->GetType()==::EV_TO_ENV)
 
906
            row->participants[1].AddPairObjEv(0,prop->GetName());
 
907
        else{ //EV_INT
 
908
            row->participants[1].AddPairObjEv(1, prop->GetName());
 
909
            step= ComputeMicroStep (theGraph, currentState-1); //computes the fired transitions from
 
910
            // the KR states currentState-1 to currentState.
 
911
            // With this, we get the transitions that have been fired. The event ev must be in the
 
912
            // action part of some transition in the set. We have to check if it is EV_INT_BC in that
 
913
            // transition.
 
914
            if (IsBroadcast (prop->GetName(), step))
 
915
              row->participants[1].AddPairObjEv(0, prop->GetName());        
 
916
        }
 
917
        formerState= currentState;
 
918
    }
 
919
  }  
 
920
 
 
921
  return asd;
 
922
 
 
923
 
 
924
}
 
925
 
 
926
 
 
927
bool SCDiagram::IsBroadcast (string event, List<SCDTransitionEdge *> step)
 
928
{
 
929
  bool found= false;
 
930
  int i= 0;
 
931
  Prop *prop;
 
932
 
 
933
  while (i< step.count() && !found){
 
934
    if (step[i]->GetSendEvent()){ //it has send event
 
935
      prop= step[i]->GetSendEvent();
 
936
      if (prop->GetName()==event && prop->GetType()==::EV_INT_BC)
 
937
        found= true;
 
938
      else
 
939
        i++;
 
940
    }
 
941
    else
 
942
      i++;
 
943
  }
 
944
 
 
945
  return found;
 
946
}
 
947
 
 
948
 
 
949
 
 
950
 
 
951
 
 
952
ConcreteSequenceDiagram * SCDiagram::GenerateConcreteSeqDiag (AbstractSequenceDiagram *asd)
 
953
{
 
954
  ConcreteSequenceDiagram *csd;
 
955
  ConcreteParticipant *cp;
 
956
  InteractionRow *row;
 
957
  InteractionParticipant *ip;
 
958
  PairObjEv *pair;
 
959
  StimulusInfo *sinf;
 
960
  Stimulus *stim1;
 
961
  Stimulus *stim2;
 
962
  int stimY;
 
963
  int formerState, currentState;
 
964
 
 
965
  string microstep= "-----------------microstep-----------------";
 
966
  string stable=    "------------------stable-------------------";
 
967
  
 
968
 
 
969
  int i, j, k, ev;
 
970
  bool found;
 
971
 
 
972
  if (asd==NULL) return NULL;
 
973
 
 
974
  csd= new ConcreteSequenceDiagram;
 
975
 
 
976
  
 
977
  
 
978
  // First we create all the ConcreteParticipants, in the same order as in AbstractSequenceDiagram.
 
979
  // note that this is just the trivial ordering, but it is possible also to have other layouts (different orderings
 
980
  // of the participants).
 
981
  for (i=0; i< asd->numObjs; i++){
 
982
    cp= new ConcreteParticipant();
 
983
    cp->name= asd->objNames[i];
 
984
    cp->logicalId= csd->NextId();
 
985
    cp->shapeId= csd->NextId();
 
986
    cp->y= 50; //we set all the objects to a height of 50
 
987
    cp->x= 120+i*280; //this way every object will be horizontally separated by 280 units from its neighbours.
 
988
    csd->participants.add (cp);
 
989
  }
 
990
  
 
991
  // Now we travel across all the happened events.
 
992
  // We create StimulusInfo objects for the list of stimuli, and
 
993
  // we attach those stimuli to the concrete participants created
 
994
  // above.
 
995
  for (i=0; i< asd->rows.count(); i++){
 
996
    
 
997
    if (i==0){
 
998
      // A microstep begins in the diagram. We add the proper comment.
 
999
      // Note that it's simulating a false message from the first participant
 
1000
      // to the last one. This way the comment extends over all the objects.
 
1001
      // Note that we do not add the stimuli in the anchor lists of the objects,
 
1002
      // as it is not an anchor.
 
1003
      sinf= new StimulusInfo();
 
1004
      sinf->sender= csd->participants[0];
 
1005
      sinf->receiver= csd->participants[csd->participants.count()-1];
 
1006
      sinf->label= stable;
 
1007
      sinf->logicalId= csd->NextId();
 
1008
      sinf->shapeId= csd->NextId();
 
1009
      stimY= 110; // initial position in the temporal line
 
1010
      sinf->y= stimY;
 
1011
      sinf->isComment= True;
 
1012
      csd->stimuli.add (sinf);
 
1013
    }
 
1014
 
 
1015
    row= asd->rows[i];
 
1016
 
 
1017
    if (i==0)
 
1018
      formerState= currentState= row->GetCurrentState();
 
1019
    else{
 
1020
      formerState= currentState;
 
1021
      currentState= row->GetCurrentState();
 
1022
    }
 
1023
 
 
1024
 
 
1025
    found= False;
 
1026
    k= formerState+1;
 
1027
    while (k<=currentState && !found){
 
1028
      if (::isStable[k])
 
1029
        found= True;
 
1030
      else
 
1031
        k++;
 
1032
    }
 
1033
   
 
1034
    if (found){
 
1035
        sinf= new StimulusInfo();
 
1036
        sinf->sender= csd->participants[0];
 
1037
        sinf->receiver= csd->participants[csd->participants.count()-1];
 
1038
        sinf->label= stable;
 
1039
        sinf->logicalId= csd->NextId();
 
1040
        sinf->shapeId= csd->NextId();
 
1041
        stimY+=50;
 
1042
        sinf->y= stimY;
 
1043
        sinf->isComment= True;
 
1044
        csd->stimuli.add (sinf);
 
1045
    }
 
1046
 
 
1047
 
 
1048
    for (j=0; j< asd->numObjs; j++){
 
1049
      ip= &(row->participants[j]);
 
1050
      for (ev=0; ev< ip->GetNumberOfEvents(); ev++){
 
1051
        pair= ip->GetPairObjEv (ev);
 
1052
        sinf= new StimulusInfo();
 
1053
        sinf->sender= csd->participants[j];
 
1054
        sinf->receiver= csd->participants[pair->GetObj()];
 
1055
        sinf->label= pair->GetEv();
 
1056
        sinf->logicalId= csd->NextId();
 
1057
        sinf->shapeId= csd->NextId();
 
1058
        stimY+=50;
 
1059
        sinf->y= stimY;
 
1060
        sinf->isComment= False;
 
1061
        
 
1062
        stim1= new Stimulus();
 
1063
        stim2= new Stimulus();
 
1064
        stim1->isSender= True;
 
1065
        stim2->isSender= False;
 
1066
        stim1->info= sinf;
 
1067
        stim2->info= sinf;
 
1068
        
 
1069
        csd->participants[j]->anchors.add (stim1); //Sender
 
1070
        if (j!=pair->GetObj()) // if it is not an event to self
 
1071
            csd->participants[pair->GetObj()]->anchors.add (stim2); //Receiver
 
1072
 
 
1073
        csd->stimuli.add (sinf);
 
1074
      } //end of loop in ev
 
1075
    } //end of loop in j
 
1076
 
 
1077
    // We add a new comment to mark the end of the microstep or the stability of the system.
 
1078
    sinf= new StimulusInfo();
 
1079
    sinf->sender= csd->participants[0];
 
1080
    sinf->receiver= csd->participants[csd->participants.count()-1];
 
1081
    sinf->label= microstep;
 
1082
    sinf->logicalId= csd->NextId();
 
1083
    sinf->shapeId= csd->NextId();
 
1084
    stimY+=50;
 
1085
    sinf->y= stimY;
 
1086
    sinf->isComment= True;
 
1087
    csd->stimuli.add (sinf);
 
1088
  } //end of loop in i
 
1089
 
 
1090
  if (::isStable[::statecounter-1]){ //The system finishes stable
 
1091
    sinf= new StimulusInfo();
 
1092
    sinf->sender= csd->participants[0];
 
1093
    sinf->receiver= csd->participants[csd->participants.count()-1];
 
1094
    sinf->label= stable;
 
1095
    sinf->logicalId= csd->NextId();
 
1096
    sinf->shapeId= csd->NextId();
 
1097
    stimY+=50;
 
1098
    sinf->y= stimY;
 
1099
    sinf->isComment= True;
 
1100
    csd->stimuli.add (sinf);
 
1101
  }
 
1102
 
 
1103
  csd->lineLength= stimY+50;
 
1104
 
 
1105
 
 
1106
  return csd;
 
1107
}
 
1108
 
 
1109
 
 
1110
 
 
1111
void SCDiagram::GenerateSeqDiagFile (ConcreteSequenceDiagram *csd, const string *formula)
 
1112
{
 
1113
  
 
1114
  string filen= "cntex.sqd";
 
1115
  OutputFile *fp;
 
1116
 
 
1117
 
 
1118
  if (csd==NULL) return;
 
1119
 
 
1120
  fp= new OutputFile();
 
1121
  fp->Open (&filen);
 
1122
 
 
1123
  (*fp) << "Storage\n";
 
1124
  (*fp) << "{\n";
 
1125
  (*fp) << "\t{ Format 1.32 }\n";
 
1126
  (*fp) << "\t{ GeneratedFrom TSCD-version-2.10a }\n";
 
1127
  (*fp) << "\t{ WrittenBy tcm }\n";
 
1128
  (*fp) << "\t{ WrittenOn \"Sat Jul  6 17:16:35 2002\" }\n";
 
1129
  (*fp) << "\t}\n\n";
 
1130
  (*fp) << "Document\n";
 
1131
  (*fp) << "{\n";
 
1132
  (*fp) << "\t{ Type \"Sequence Diagram\" }\n";
 
1133
  (*fp) << "\t{ Name cntex.sqd }\n";
 
1134
  (*fp) << "\t{ Author tcm }\n";
 
1135
  (*fp) << "\t{ CreatedOn \"Sat Jul  6 14:14:12 2002\" }\n";
 
1136
  (*fp) << "\t{ Annotation \"\" }\n";
 
1137
  (*fp) << "}\n\n";
 
1138
  (*fp) << "Page\n";
 
1139
  (*fp) << "{\n";
 
1140
  (*fp) << "\t{ PageOrientation Portrait }\n";
 
1141
  (*fp) << "\t{ PageSize A4 }\n";
 
1142
  (*fp) << "\t{ ShowHeaders False }\n";
 
1143
  (*fp) << "\t{ ShowFooters False }\n";
 
1144
  (*fp) << "\t{ ShowNumbers False }\n";
 
1145
  (*fp) << "}\n\n";
 
1146
  (*fp) << "Scale\n";
 
1147
  (*fp) << "{\n";
 
1148
  (*fp) << "\t{ ScaleValue 1 }\n";
 
1149
  (*fp) << "}\n\n";
 
1150
  (*fp) << "# GRAPH NODES\n\n";
 
1151
 
 
1152
  GenerateGraphNodes (csd, fp);
 
1153
  GenerateComments (csd, fp);
 
1154
  GenerateNote (csd, fp, formula);
 
1155
  GenerateGraphEdges (csd, fp);
 
1156
 
 
1157
 
 
1158
  (*fp) << "# VIEWS AND GRAPHICAL SHAPES\n";
 
1159
  (*fp) << "\n";
 
1160
  (*fp) << "View 1\n";
 
1161
  (*fp) << "{\n";
 
1162
  (*fp) << "\t{ Index \"0\" }\n";
 
1163
  (*fp) << "\t{ Parent 0 }\n";
 
1164
  (*fp) << "}\n\n";
 
1165
 
 
1166
  GenerateObjectBoxes (csd, fp);
 
1167
  GenerateT4Lines (csd, fp);
 
1168
  GenerateTextBoxes (csd, fp);
 
1169
  GenerateNoteBox (csd, fp);
 
1170
 
 
1171
 
 
1172
  fp->Close();
 
1173
 
 
1174
}
 
1175
 
 
1176
 
 
1177
 
 
1178
void SCDiagram::GenerateGraphNodes (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1179
{
 
1180
  int i, j;
 
1181
  ConcreteParticipant *cp;
 
1182
 
 
1183
 
 
1184
 
 
1185
  if (csd==NULL || fp==NULL) return;
 
1186
 
 
1187
 
 
1188
  for (i=0; i< csd->participants.count(); i++){
 
1189
    cp= csd->participants[i];
 
1190
    (*fp) << "CBDObjectNode " << cp->logicalId << "\n";
 
1191
    (*fp) << "{\n";
 
1192
    (*fp) << "\t{ Name \"" << cp->name << "\" }\n";
 
1193
    (*fp) << "\t{ Annotation \"\" }\n";
 
1194
    (*fp) << "\t{ Parent 0 }\n";
 
1195
    (*fp) << "\t{ Index \"\" }\n";
 
1196
    (*fp) << "\t{ Stereotype \"<< - >>\" }\n";
 
1197
    (*fp) << "\t{ Properties \"{ - }\" }\n";
 
1198
    (*fp) << "\t{ Anchors " << cp->anchors.count() << " }\n"; //it's OK also for 0
 
1199
    for (j=0; j< cp->anchors.count(); j++){
 
1200
      (*fp) << "\t{ Anchor " << cp->anchors[j]->info->y << " ";
 
1201
      if (cp->anchors[j]->isSender)
 
1202
        (*fp) << cp->logicalId; // it puts its own number
 
1203
      else
 
1204
        (*fp) << cp->anchors[j]->info->sender->logicalId;
 
1205
      
 
1206
      (*fp) << " }\n";
 
1207
    }
 
1208
    (*fp) << "}\n";
 
1209
  }
 
1210
 
 
1211
}
 
1212
 
 
1213
 
 
1214
 
 
1215
void SCDiagram::GenerateComments (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1216
{
 
1217
  int i;
 
1218
  StimulusInfo *sinf;
 
1219
 
 
1220
  if (csd==NULL || fp==NULL) return;
 
1221
 
 
1222
 
 
1223
  // We travel across the stimuli and issue a "Comment" section in the file every
 
1224
  // time we find a stimuli with a True isComment attribute.
 
1225
 
 
1226
  for (i=0; i< csd->stimuli.count(); i++){
 
1227
    if (csd->stimuli[i]->isComment){
 
1228
      sinf= csd->stimuli[i];
 
1229
      (*fp) << "Comment " << sinf->logicalId << "\n";
 
1230
      (*fp) << "{\n";
 
1231
      (*fp) << "\t{ Name \"" << sinf->label << "\" }\n";
 
1232
      (*fp) << "\t{ Annotation \"\" }\n";
 
1233
      (*fp) << "\t{ Parent 0 }\n";
 
1234
      (*fp) << "\t{ Index \"\" }\n";
 
1235
      (*fp) << "}\n\n";
 
1236
    }
 
1237
  }
 
1238
 
 
1239
}
 
1240
 
 
1241
 
 
1242
 
 
1243
void SCDiagram::GenerateGraphEdges (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1244
{
 
1245
 
 
1246
  int i;
 
1247
  StimulusInfo *sinf;
 
1248
 
 
1249
 
 
1250
  if (csd==NULL || fp==NULL) return;
 
1251
 
 
1252
  (*fp) << "# GRAPH EDGES\n\n";
 
1253
 
 
1254
 
 
1255
  for (i=0; i< csd->stimuli.count(); i++){
 
1256
    if (!csd->stimuli[i]->isComment){ //then it is a real stimulus
 
1257
      sinf= csd->stimuli[i];
 
1258
      (*fp) << "CBDObjectLinkEdge " << sinf->logicalId << "\n";
 
1259
      (*fp) << "{\n";
 
1260
      (*fp) << "\t{ Name \"" << sinf->label << "\" }\n";
 
1261
      (*fp) << "\t{ Annotation \"\" }\n";
 
1262
      (*fp) << "\t{ Parent 0 }\n";
 
1263
      (*fp) << "\t{ Subject1 " << sinf->sender->logicalId << " }\n";
 
1264
      (*fp) << "\t{ Subject2 " << sinf->receiver->logicalId << " }\n";
 
1265
      (*fp) << "\t{ Anchor1 " << sinf->y << " " << sinf->sender->shapeId << " }\n";
 
1266
      (*fp) << "\t{ Anchor2 " << sinf->y << " " << sinf->receiver->shapeId << " }\n";
 
1267
      (*fp) << "}\n\n";
 
1268
    }
 
1269
  }
 
1270
 
 
1271
}
 
1272
 
 
1273
 
 
1274
 
 
1275
void SCDiagram::GenerateObjectBoxes (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1276
{
 
1277
  int i, len;
 
1278
  ConcreteParticipant *cp;
 
1279
 
 
1280
  if (csd==NULL || fp==NULL) return;
 
1281
 
 
1282
  for (i=0; i< csd->participants.count(); i++){
 
1283
    cp= csd->participants[i];
 
1284
    (*fp) << "SSDSingleObjectBox " << cp->shapeId << "\n";
 
1285
    (*fp) << "{\n";
 
1286
    (*fp) << "\t{ View 1 }\n";
 
1287
    (*fp) << "\t{ Subject " << cp->logicalId << " }\n";
 
1288
    (*fp) << "\t{ Position " << cp->x << " " << cp->y << " }\n";
 
1289
    (*fp) << "\t{ Size 80 40 }\n";
 
1290
    (*fp) << "\t{ Color \"black\" }\n";
 
1291
    (*fp) << "\t{ LineWidth 1 }\n";
 
1292
    (*fp) << "\t{ LineStyle Solid }\n";
 
1293
    (*fp) << "\t{ FillStyle Unfilled }\n";
 
1294
    (*fp) << "\t{ FillColor \"white\" }\n";
 
1295
    (*fp) << "\t{ FixedName False }\n";
 
1296
    (*fp) << "\t{ Font \"-*-helvetica-medium-r-normal--10*\" }\n";
 
1297
    (*fp) << "\t{ TextAlignment Center }\n";
 
1298
    (*fp) << "\t{ TextColor \"black\" }\n";
 
1299
    (*fp) << "\t{ NameUnderlined True }\n";
 
1300
 
 
1301
    /* We need to know how long will be the lifeline of each object. We have chosen that 
 
1302
       all the objects have the same length.
 
1303
    */
 
1304
    (*fp) << "\t{ EndPosition " << cp->x << " " << csd->lineLength << " }\n";
 
1305
    (*fp) << "\t{ Destructive 0 }\n";
 
1306
    (*fp) << "}\n\n";
 
1307
  }
 
1308
 
 
1309
 
 
1310
}
 
1311
 
 
1312
 
 
1313
 
 
1314
void SCDiagram::GenerateT4Lines (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1315
{
 
1316
  int i;
 
1317
  StimulusInfo *sinf;
 
1318
  int min;
 
1319
 
 
1320
 
 
1321
  if (csd==NULL || fp==NULL) return;
 
1322
 
 
1323
 
 
1324
  for (i=0; i< csd->stimuli.count(); i++){
 
1325
    sinf= csd->stimuli[i];
 
1326
    if (!sinf->isComment){
 
1327
      (*fp) << "T4Line " << sinf->shapeId << "\n";
 
1328
      (*fp) << "{\n";
 
1329
      (*fp) << "\t{ View 1 }\n";
 
1330
      (*fp) << "\t{ Subject " << sinf->logicalId << " }\n";
 
1331
      (*fp) << "\t{ FromShape " << sinf->sender->shapeId << " }\n";
 
1332
      (*fp) << "\t{ ToShape " << sinf->receiver->shapeId << " }\n";
 
1333
      (*fp) << "\t{ Curved False }\n";
 
1334
      (*fp) << "\t{ End1 Empty }\n";
 
1335
      (*fp) << "\t{ End2 FilledArrow }\n";
 
1336
      if (sinf->sender==sinf->receiver){ // event to self
 
1337
        // This kind of arrow consists of 4 points.
 
1338
        (*fp) << "\t{ Points 4 }\n";
 
1339
        (*fp) << "\t{ Point " << sinf->sender->x << " " << sinf->y << " }\n";
 
1340
        (*fp) << "\t{ Point " << (sinf->sender->x+20) << " " << sinf->y << " }\n";
 
1341
        (*fp) << "\t{ Point " << (sinf->sender->x+20) << " " << (sinf->y+10) << " }\n";
 
1342
        (*fp) << "\t{ Point " << sinf->sender->x << " " << (sinf->y+10) << " }\n";
 
1343
      }
 
1344
      else{ //event between two different participants
 
1345
        (*fp) << "\t{ Points 2 }\n";
 
1346
        (*fp) << "\t{ Point " << sinf->sender->x << " " << sinf->y << " }\n";
 
1347
        (*fp) << "\t{ Point " << sinf->receiver->x << " " << sinf->y << " }\n";
 
1348
      }
 
1349
      // The position of the name is fixed to 140 units from the smallest X of both objects
 
1350
      // and 10 units from the Y, unless it is an event to self. In that case, the offset is 20.
 
1351
      if (sinf->sender->x < sinf->receiver->x)
 
1352
        min= sinf->sender->x;
 
1353
      else
 
1354
        min= sinf->receiver->x;
 
1355
        
 
1356
      if (sinf->sender==sinf->receiver)
 
1357
         (*fp) << "\t{ NamePosition " << (min+20) << " " << (sinf->y-10) << " }\n";
 
1358
      else
 
1359
         (*fp) << "\t{ NamePosition " << (min+140) << " " << (sinf->y-10) << " }\n";
 
1360
      (*fp) << "\t{ Color \"black\" }\n";
 
1361
      (*fp) << "\t{ LineWidth 1 }\n";
 
1362
      (*fp) << "\t{ LineStyle Solid }\n";
 
1363
      (*fp) << "\t{ FixedName False }\n";
 
1364
      (*fp) << "\t{ Font \"-*-helvetica-medium-r-normal--10*\" }\n";
 
1365
      (*fp) << "\t{ TextAlignment Center }\n";
 
1366
      (*fp) << "\t{ TextColor \"black\" }\n";
 
1367
      (*fp) << "\t{ NameUnderlined False }\n";
 
1368
      (*fp) << "}\n\n";
 
1369
    }
 
1370
  }
 
1371
 
 
1372
}
 
1373
 
 
1374
 
 
1375
void SCDiagram::GenerateTextBoxes (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1376
{
 
1377
  int i;
 
1378
  StimulusInfo *sinf;
 
1379
 
 
1380
  if (csd==NULL || fp==NULL) return;
 
1381
 
 
1382
  for (i=0; i< csd->stimuli.count(); i++){
 
1383
    sinf= csd->stimuli[i];
 
1384
    if (sinf->isComment){
 
1385
      (*fp) << "TextBox " << sinf->shapeId << "\n";
 
1386
      (*fp) << "{\n";
 
1387
      (*fp) << "\t{ View 1 }\n";
 
1388
      (*fp) << "\t{ Subject " << sinf->logicalId << " }\n";
 
1389
      (*fp) << "\t{ Position " << (sinf->sender->x+140) << " " << sinf->y << " }\n";
 
1390
      (*fp) << "\t{ Size 20 20 }";
 
1391
      (*fp) << "\t{ Color \"black\" }\n";
 
1392
      (*fp) << "\t{ LineWidth 1 }\n";
 
1393
      (*fp) << "\t{ LineStyle Invisible }\n";
 
1394
      (*fp) << "\t{ FillStyle Unfilled }\n";
 
1395
      (*fp) << "\t{ FillColor \"white\" }\n";
 
1396
      (*fp) << "\t{ FixedName False }\n";
 
1397
      (*fp) << "\t{ Font \"-*-helvetica-medium-r-normal--10*\" }\n";
 
1398
      (*fp) << "\t{ TextAlignment Center }\n";
 
1399
      (*fp) << "\t{ TextColor \"black\" }\n";
 
1400
      (*fp) << "\t{ NameUnderlined False }\n";
 
1401
      (*fp) << "}\n\n";
 
1402
     }
 
1403
  }
 
1404
 
 
1405
}
 
1406
 
 
1407
 
 
1408
 
 
1409
void SCDiagram::GenerateNote (ConcreteSequenceDiagram *csd, OutputFile *fp, const string *formula)
 
1410
{
 
1411
  if (csd==NULL || fp==NULL || formula==NULL) return;
 
1412
 
 
1413
  (*fp) << "Note " << csd->NextId() << "\n";
 
1414
  (*fp) << "{\n";
 
1415
  (*fp) << "\t{ Name \"Counterexample for\\r" << *formula << "\" }\n";
 
1416
  (*fp) << "\t{ Annotation \"\" }\n";
 
1417
  (*fp) << "\t{ Parent 0 }\n";
 
1418
  (*fp) << "\t{ Index \"\" }\n";
 
1419
  (*fp) << "}\n\n";
 
1420
}
 
1421
 
 
1422
 
 
1423
 
 
1424
void SCDiagram::GenerateNoteBox (ConcreteSequenceDiagram *csd, OutputFile *fp)
 
1425
{
 
1426
  if (csd==NULL || fp==NULL) return;
 
1427
 
 
1428
  int id= csd->NextId();
 
1429
  int posx= csd->participants[csd->participants.count()-1]->x;
 
1430
  int posy= csd->participants[csd->participants.count()-1]->y;
 
1431
 
 
1432
  (*fp) << "NoteBox " << id << "\n";
 
1433
  (*fp) << "{\n";
 
1434
  (*fp) << "\t{ View 1 }\n";
 
1435
  (*fp) << "\t{ Subject " << (id-1) << " }\n";
 
1436
  (*fp) << "\t{ Position " << (posx+160) << " " << posy << " }\n";
 
1437
  (*fp) << "\t{ Size 170 82 }\n"; //Enhacement: calculate the size based on the characters of the formula.
 
1438
  (*fp) << "\t{ Color \"black\" }\n";
 
1439
  (*fp) << "\t{ LineWidth 1 }\n";
 
1440
  (*fp) << "\t{ LineStyle Solid }\n";
 
1441
  (*fp) << "\t{ FillStyle Unfilled }\n";
 
1442
  (*fp) << "\t{ FillColor \"white\" }\n";
 
1443
  (*fp) << "\t{ FixedName False }\n";
 
1444
  (*fp) << "\t{ Font \"-*-helvetica-medium-r-normal--10*\" }\n";
 
1445
  (*fp) << "\t{ TextAlignment Center }\n";
 
1446
  (*fp) << "\t{ TextColor \"black\" }\n";
 
1447
  (*fp) << "\t{ NameUnderlined False }\n";
 
1448
  (*fp) << "}\n\n";
 
1449
}
 
1450
 
 
1451
void InteractionParticipant::AddPairObjEv (int object, string event)
 
1452
{
 
1453
  PairObjEv *newPair= new PairObjEv (object, event);
 
1454
  eventsToSend.add (newPair);
 
1455
}
 
1456
 
 
1457
 
 
1458
 
 
1459
void InteractionParticipant::PrintIt ()
 
1460
{
 
1461
  std::cout << "Participant:" << std::endl;
 
1462
  for (int i=0; i< eventsToSend.count(); i++)
 
1463
    eventsToSend[i]->PrintIt();
 
1464
  std::cout << std::endl;
 
1465
 
 
1466
}
 
1467
 
 
1468
void InteractionRow::PrintIt ()
 
1469
{
 
1470
  for (int i=0; i< numObj; i++)
 
1471
    participants[i].PrintIt();
 
1472
 
 
1473
  std::cout << std::endl;
 
1474
 
 
1475
}
 
1476
 
 
1477
void AbstractSequenceDiagram::PrintIt ()
 
1478
{
 
1479
  for (int t=0; t< rows.count(); t++){
 
1480
    std::cout << "Time " << std::endl;
 
1481
    rows[t]->PrintIt();
 
1482
  }
 
1483
}
 
1484
 
 
1485
 
 
1486
InteractionRow * AbstractSequenceDiagram::AddRow (int cs)
 
1487
{
 
1488
  InteractionRow *ir= new InteractionRow (numObjs, cs);
 
1489
  rows.add (ir);
 
1490
  return ir;
 
1491
}
 
1492
 
 
1493
 
 
1494
#endif
 
1495
 
 
1496
 
 
1497
//bool SCDiagram::SetText(TextShape *t, const string *s) {
 
1498
//      const string *description = t->GetDescription();
 
1499
//      Subject *subj = t->GetParent()->GetSubject();
 
1500
//      if (*description == "Event")
 
1501
//              return SetEvent((Transition *)subj, s);
 
1502
//      else if (*description == "Action")
 
1503
//              return SetAction(subj, s, t->GetSequence());
 
1504
//      else 
 
1505
//              return Diagram::SetText(t, s);
 
1506
//}