1
////////////////////////////////////////////////////////////////////////////////
3
// This file is part of Toolkit for Conceptual Modeling (TCM).
4
// (c) copyright 1999, Vrije Universiteit Amsterdam and University of Twente.
5
// Author: Frank Dehne (frank@cs.vu.nl).
6
// Author: Henk van de Zandschulp (henkz@cs.utwente.nl).
8
// TCM is free software; you can redistribute it and/or modify
9
// it under the terms of the GNU General Public License as published by
10
// the Free Software Foundation; either version 2 of the License, or
11
// (at your option) any later version.
13
// TCM is distributed in the hope that it will be useful,
14
// but WITHOUT ANY WARRANTY; without even the implied warranty of
15
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16
// GNU General Public License for more details.
18
// You should have received a copy of the GNU General Public License
19
// along with TCM; if not, write to the Free Software
20
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
22
////////////////////////////////////////////////////////////////////////////////
23
#include "atdactionstatenode.h"
24
#include "atddecisionstatenode.h"
25
#include "atdfinalstatenode.h"
26
#include "atdwaitstatenode.h"
27
#include "atdinitialstatenode.h"
28
#include "atdsynchronizationnode.h"
29
#include "atdtransitionedge.h"
30
#include "emptynode.h"
35
#include "roundedbox.h"
36
#include "ellipsedbox.h"
37
#include "solidhorizontalbar.h"
38
#include "solidverticalbar.h"
39
#include "minidiamond.h"
43
#include "commentlink.h"
45
#include "atdiagram.h"
51
#include "adshypergraph.h"
52
#include "adssemantics.h" /*new*/
53
#include "adseliminatepseudostatenodes.h"
54
#include "adspropertyvaluation.h"
55
#include "adsproperty.h"
56
#include "temporalpropertydialog.h"
57
#include "outputfile.h"
58
#include "inputfile.h"
59
#include "adsmcoutputparse.h"
60
#include "adsltlformulaparse.h"
61
//#include "adsmcoutput.tab.h"
67
const int ATDiagram::DOT_WIDTH = 8;
69
ATDiagram::ATDiagram(Config *c, ATWindow *d, ATViewer *v, ATGraph *g):
73
atChecks = new ATChecks(this,g);
76
ATDiagram::~ATDiagram() {
80
Thing *ATDiagram::CreateThing(int classNr) {
81
Grafport *g = GetDiagramViewer()->GetGrafport();
82
ShapeView *v = GetDiagramViewer()->GetCurView();
83
ATGraph *cg = (ATGraph *)GetGraph();
86
if (classNr == Code::ELLIPSED_BOX)
87
thing = new EllipsedBox(v, g, 0, 0);
88
else if (classNr == Code::ROUNDED_BOX)
89
thing = new RoundedBox(v, g, 0, 0);
90
else if (classNr == Code::MINI_DIAMOND)
91
thing = new MiniDiamond(v, g, 0, 0);
92
else if (classNr == Code::BLACK_DOT)
93
thing = new BlackDot(v, g, 0, 0);
94
else if (classNr == Code::BULLS_EYE)
95
thing = new BullsEye(v, g, 0, 0);
96
else if (classNr == Code::SOLID_HORIZONTAL_BAR)
97
thing = new SolidHorizontalBar(v, g, 0, 0);
98
else if (classNr == Code::SOLID_VERTICAL_BAR)
99
thing = new SolidVerticalBar(v, g, 0, 0);
100
else if (classNr == Code::NOTE_BOX)
101
thing = new NoteBox(v, g, 0, 0);
102
else if (classNr==Code::TEXT_BOX)
103
thing = new TextBox(v, g, 0, 0);
105
else if (classNr == Code::VIEW)
106
thing = new ShapeView(GetDiagramViewer());
108
else if (classNr == Code::LINE)
109
thing = new Line(v, g, 0, 0, 0);
110
// old line (arrow) types...
111
else if (classNr == Code::ARROW) {
112
Line *line = new Line(v, g, 0, 0, 0);
113
line->SetEnd2(LineEnd::FILLED_ARROW);
117
else if (classNr==Code::INITIAL_STATE || classNr == Code::ATD_INITIAL_STATE_NODE)
118
thing = new ATDInitialStateNode(cg);
119
else if (classNr == Code::ATD_ACTION_STATE_NODE)
120
thing = new ATDActionStateNode(cg);
121
else if (classNr == Code::ATD_WAIT_STATE_NODE)
122
thing = new ATDWaitStateNode(cg);
123
else if (classNr == Code::ATD_DECISION_STATE_NODE)
124
thing = new ATDDecisionStateNode(cg);
125
else if (classNr == Code::ATD_SYNCHRONIZATION_NODE)
126
thing = new ATDSynchronizationNode(cg);
127
else if (classNr==Code::FINAL_STATE || classNr == Code::ATD_FINAL_STATE_NODE)
128
thing = new ATDFinalStateNode(cg);
129
else if (classNr == Code::NOTE)
130
thing = new Note(cg);
131
else if (classNr == Code::COMMENT)
132
thing = new Comment(cg);
135
else if (classNr==Code::TRANSITION || classNr == Code::ATD_TRANSITION_EDGE)
136
thing = new ATDTransitionEdge(cg, 0, 0);
137
else if (classNr==Code::COMMENT_LINK)
138
thing = new CommentLink(cg, 0, 0);
141
error("%s, line %d: impl error: " "wrong class number %d\n",
142
__FILE__, __LINE__, classNr);
145
if (thing != 0 && HasIndexShape(thing->GetClassType()))
146
((NodeShape *)thing)->SetFixedIndexLabel(False);
151
Node *ATDiagram::CreateNode(){
153
ATGraph *g = (ATGraph *)GetGraph();
154
if (GetNodeType() == Code::ATD_INITIAL_STATE_NODE)
155
node = new ATDInitialStateNode(g);
156
else if (GetNodeType() == Code::ATD_ACTION_STATE_NODE)
157
node = new ATDActionStateNode(g);
158
else if (GetNodeType() == Code::ATD_WAIT_STATE_NODE)
159
node = new ATDWaitStateNode(g);
160
else if (GetNodeType() == Code::ATD_DECISION_STATE_NODE)
161
node = new ATDDecisionStateNode(g);
162
else if (GetNodeType() == Code::ATD_SYNCHRONIZATION_NODE)
163
node = new ATDSynchronizationNode(g);
164
else if (GetNodeType() == Code::ATD_FINAL_STATE_NODE)
165
node = new ATDFinalStateNode(g);
166
else if (GetNodeType() == Code::NOTE)
168
else if (GetNodeType() == Code::COMMENT)
169
node = new Comment(g);
171
error("%s, line %d: impl error: "
172
"unknown node type\n", __FILE__, __LINE__);
176
Edge *ATDiagram::CreateEdge(Subject *node1, Subject *node2){
177
// Check possible connections (node-node-edge matrix).
178
if (!CheckConnection(node1, node2))
180
if ((GetEdgeType() == Code::ATD_TRANSITION_EDGE) &&
181
(node1->GetClassType() == Code::ATD_DECISION_STATE_NODE) &&
183
ShowDialog(MessageDialog::ERROR, "Error",
184
"This is not a valid transition");
188
ATGraph *g = (ATGraph *)GetGraph();
189
if (GetEdgeType()==Code::COMMENT_LINK)
190
edge = new CommentLink(g, node1, node2);
191
else if (GetEdgeType() == Code::ATD_TRANSITION_EDGE)
192
edge = new ATDTransitionEdge(g, node1, node2);
195
error( "%s, line %d: impl error: "
196
" unknown edge type\n", __FILE__, __LINE__);
200
NodeShape *ATDiagram::CreateNodeShape(Node *node, int x, int y) {
201
NodeShape *shape = 0;
202
Grafport *g = GetDiagramViewer()->GetGrafport();
203
ShapeView *v = GetDiagramViewer()->GetCurView();
204
int t = GetNodeShapeType();
205
if (t == Code::ELLIPSED_BOX)
206
shape = new EllipsedBox(v, g, x, y);
207
else if (t == Code::ROUNDED_BOX)
208
shape = new RoundedBox(v, g, x, y);
209
else if (t == Code::MINI_DIAMOND)
210
shape = new MiniDiamond(v, g, x, y);
211
else if (t == Code::NOTE_BOX)
212
shape = new NoteBox(v, g, x, y);
213
else if (t == Code::BLACK_DOT)
214
shape = new BlackDot(v, g, x, y);
215
else if (t == Code::BULLS_EYE)
216
shape = new BullsEye(v, g, x, y);
217
else if (t == Code::SOLID_HORIZONTAL_BAR)
218
shape = new SolidHorizontalBar(v, g, x, y);
219
else if (t == Code::SOLID_VERTICAL_BAR)
220
shape = new SolidVerticalBar(v, g, x, y);
221
else if (t == Code::TEXT_BOX)
222
shape = new TextBox(v, g, x, y);
224
error( "%s, line %d: impl error: "
225
"node shape type does not exist\n", __FILE__, __LINE__);
228
if (HasIndexShape(t))
229
shape->SetFixedIndexLabel(False);
230
shape->SetSubject(node);
231
shape->SetTextShape();
236
Line *ATDiagram::CreateLine(
237
Edge *edge, GShape *from, GShape *to, List<Point *> *l) {
238
Grafport *g = GetDiagramViewer()->GetGrafport();
239
ShapeView *v = GetDiagramViewer()->GetCurView();
241
int t = GetLineType();
243
line = new Line(v, g, from, to, l, IsCurve());
245
error( "%s, line %d: impl error: "
246
"line type does not exist\n", __FILE__, __LINE__);
248
line->SetSubject(edge);
249
line->SetTextShape();
250
line->SetEnd1(GetLineEnd1());
251
line->SetEnd2(GetLineEnd2());
256
void ATDiagram::UpdateNodeType(int num) {
257
((DiagramWindow *)GetMainWindow())->SetNodeName(num);
259
case 1: SetNodeType(Code::ATD_ACTION_STATE_NODE);
260
SetNodeShapeType(Code::ELLIPSED_BOX);
262
case 2: SetNodeType(Code::ATD_DECISION_STATE_NODE);
263
SetNodeShapeType(Code::MINI_DIAMOND);
265
case 3: SetNodeType(Code::ATD_SYNCHRONIZATION_NODE);
266
SetNodeShapeType(Code::SOLID_HORIZONTAL_BAR);
268
case 4: SetNodeType(Code::ATD_INITIAL_STATE_NODE);
269
SetNodeShapeType(Code::BLACK_DOT);
271
case 5: SetNodeType(Code::COMMENT);
272
SetNodeShapeType(Code::TEXT_BOX);
273
SetNodeLineStyle(LineStyle::INVISIBLE);
275
case 6: SetNodeType(Code::ATD_WAIT_STATE_NODE);
276
SetNodeShapeType(Code::ROUNDED_BOX);
278
case 7: SetNodeType(Code::NOTE);
279
SetNodeShapeType(Code::NOTE_BOX);
281
case 8: SetNodeType(Code::ATD_SYNCHRONIZATION_NODE);
282
SetNodeShapeType(Code::SOLID_VERTICAL_BAR);
284
case 9: SetNodeType(Code::ATD_FINAL_STATE_NODE);
285
SetNodeShapeType(Code::BULLS_EYE);
288
error("%s, line %d: impl error: "
289
"unknown node type selected\n", __FILE__,__LINE__);
293
void ATDiagram::UpdateEdgeType(int num) {
294
((DiagramWindow *)GetMainWindow())->SetEdgeName(num);
296
case 1: SetEdgeType(Code::ATD_TRANSITION_EDGE);
297
SetLineType(Code::LINE);
298
SetEdgeLineStyle(LineStyle::SOLID);
299
SetLineEnd1(LineEnd::EMPTY);
300
SetLineEnd2(LineEnd::FILLED_ARROW);
302
case 2: SetEdgeType(Code::COMMENT_LINK);
303
SetLineType(Code::LINE);
304
SetEdgeLineStyle(LineStyle::WIDE_DOTTED);
305
SetLineEnd1(LineEnd::EMPTY);
306
SetLineEnd2(LineEnd::EMPTY);
309
error("%s, line %d: impl error: "
310
"unknown edge type selected\n", __FILE__,__LINE__);
314
bool ATDiagram::HasIndexNode(int code) {
315
return (code == Code::ATD_ACTION_STATE_NODE ||
316
code == Code::ATD_WAIT_STATE_NODE ||
317
code == Code::ATD_DECISION_STATE_NODE);
320
bool ATDiagram::HasIndexShape(int code) {
321
return (code==Code::ROUNDED_BOX ||
322
code==Code::ELLIPSED_BOX ||
323
code==Code::DIAMOND ||
324
code==Code::NOTE_BOX);
327
void ATDiagram::CheckDocument() {
330
errors += atChecks->CheckNodeCount(1, Code::ATD_INITIAL_STATE_NODE, chkbuf);
331
errors += atChecks->CheckNodeCount(1, Code::ATD_FINAL_STATE_NODE, chkbuf);
332
if (errors == 0) // only useful with 1 INITIAL && 1 FINAL state
333
errors += atChecks->CheckUnreachableStates(chkbuf);
334
errors += atChecks->CheckNodeCount(1, INT_MAX, Code::ATD_ACTION_STATE_NODE, chkbuf);
336
errors += atChecks->CheckNamelessNodes(Code::ATD_ACTION_STATE_NODE, chkbuf);
337
errors += atChecks->CheckNamelessNodes(Code::ATD_WAIT_STATE_NODE, chkbuf);
340
errors += atChecks->CheckCountEdgesFrom(Code::ATD_SYNCHRONIZATION_NODE,
341
Code::ATD_TRANSITION_EDGE, 2, INT_MAX, False, False, chkbuf);
343
ReportCheck(errors, &chkbuf);
349
void ATDiagram::ModelCheckProperty() {
351
int status = system("which NuSMV > /dev/null 2>/dev/null");
353
string URL = "http://www.cs.utwente.nl/~tcm/tatd.html"; // RIK: AANPASSEN
354
string txt = "Model checker NuSMV cannot be found.";
355
txt += "\n\nPlease check your PATH or the URL below for more information:";
357
(new MessageDialog(GetMainWindow()->GetWidget(),
358
MessageDialog::INFORMATION))->
359
Show("Notice", &txt);
362
SetStatus("action: model check property");
363
tpd = new TPDialog(GetMainWindow()->GetWidget());
365
tpd->SetTitle("Model check property");
366
tpd->SetOKCallback(&ModelCheckPropertyOKCB, this);
367
tpd->ManageSubstringToggle(True);
368
tpd->ManageNameOnlyToggle(True);
374
extern string replace(string s); // defined in adscks
377
void ATDiagram::ModelCheckPropertyOKCB(Widget w, XtPointer clientData, XtPointer) {
378
ATDiagram *atd = (ATDiagram *)clientData;
381
atd->GetTPDialog()->GetTextString(&fbuf);
382
atd->DoModelCheckProperty(&fbuf, atd->GetTPDialog()->SensitiveOn(), atd->GetTPDialog()->SubstringOn(), atd->GetTPDialog()->NameOnlyOn() );
385
void ATDiagram::DoModelCheckProperty(const string *p, bool symbolic, bool reduction, bool sf) {
386
// fill initial and final for the parser
387
// initial and final are state predicates that characterise when a configuration is initial and when it is
388
// final. The meaning of final depends upon the model being checked.
391
GetMainWindow()->SetCursor(MouseCursor::WATCH);
394
ah=new ADSHyperGraph();
395
if (!ComputeHyperGraph(ah)) return;
398
::initial = (char *) malloc (strlen("I___INITIAL>0")+1);
399
strcpy(::initial,"I___INITIAL>0");
402
str.replace('\r','_');
405
// parse the property
407
::identifier_count=0;
408
::isltl=1; // set to zero if ctl formula
409
YY_BUFFER_STATE y = ::adsltlformula_scan_string(str.getstr());
410
strcpy(::adsltlformula_constraint, "");
411
bool b = !adsltlformulaparse();
412
adsltlformula_delete_buffer(y);
414
error("I cannot parse this property\n");
419
List <ADSVar *> varused; // ASSUMPTION: only boolean variables are used, so no integer expressions (what about nodes)
420
List <Node *> nodeused;
421
for (int i=0;i<identifier_count;i++){
422
ADSVar *v=new ADSVar(identifier[i],::PROP);
423
ADSVar *v_old= ah->FindSimilarVar(v);
424
if (v_old){ // v occurs as variable in hypergraph ah
428
string iname=identifier[i];
429
Node *n= (ah->FindNode(iname));
435
List <Subject *> finalnodes;
436
ah->GetFinalNodes(&finalnodes);
437
for (finalnodes.first();!finalnodes.done();finalnodes.next()){
438
nodeused.add((Node*)finalnodes.cur());
441
ah->RemoveLocalVariables(&varused);
442
ah->RemoveNodes(nodeused,varused,reduction);
445
string sfinal=ah->ComputeFinalPredicate();
446
string property=::ltlprop;
447
property.replace("FINAL",sfinal);
450
char buf[100]; // temporary filename for activity graph model
451
strcpy(buf,"XXXXXX");
454
char req[100]; // temporarly filename for LTL property
455
strcpy(req,"XXXXXX");
458
FILE *ftemp; // temporarly file for LTL property
459
ftemp=fopen(req,"w");
460
fprintf(ftemp,"%s",property.getstr()); // put the property in the temp file
467
OutputFile *ofile2= new OutputFile();
468
ofile2->Open(&bufstr);
470
ah->WriteNuSMV(ofile2,sf);
474
ComputeCKS(ah,ac,reduction);
475
ac->WriteSMVFile(ofile2,sf);
479
(*ofile2) << "\n\nLTLSPEC\n";
482
(*ofile2) << "\n\nSPEC\n";
484
(*ofile2) << property << "\n\n";
487
// Next start the model checking
488
SetStatus("Model checking...");
490
strcpy(output,"XXXXXX");
491
(void)mkstemp(output);
493
string command = "NuSMV " + bufstr + " > " + output;
494
system(command.getstr()); // do the actual model checking
497
// parse the model checker's output
498
::adsmcoutputin=fopen(output,"r");
504
b=adsmcoutputparse();
506
error("I couldn't parse the model checker's output\n");
512
mctxt="The requirement is satisfied\n";
513
ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
516
mctxt="The requirement is not satisfied; see the counter example\n";
517
ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
518
if (symbolic) ProvideFeedback(ah);
519
else ProvideFeedback(ac);
522
GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
523
unlink(output); // cleanup buf
524
unlink(req); // cleanup
525
unlink(buf); // cleanup
529
void ATDiagram::GeneralCheck() {
530
SetStatus("action: general check");
532
SetStatus("general check done");
536
void ATDiagram::DoGeneralCheck(){
537
GetMainWindow()->SetCursor(MouseCursor::WATCH);
540
ah=new ADSHyperGraph();
541
if (!ComputeHyperGraph(ah)) return;
543
// check that every run leads to a final state
544
string constraint="F G ";
545
string finalstr = ah->ComputeFinalPredicate();
546
constraint += finalstr;
548
char buf[100]; // temporary filename for activity graph model
549
strcpy(buf,"XXXXXX");
554
char req[100]; // temporarly filename for LTL property
555
strcpy(req,"XXXXXX");
558
FILE *ftemp; // temporarly file for LTL property
559
ftemp=fopen(req,"w");
560
fprintf(ftemp,"%s",constraint.getstr()); // put the property in the temp file
567
ComputeCKS(ah,ac,False);
570
OutputFile *ofile2= new OutputFile();
571
ofile2->Open(&bufstr);
572
ac->WriteSMVFile(ofile2,True);
573
(*ofile2) << "\n\nLTLSPEC\n";
574
(*ofile2) << constraint << "\n\n";
576
// Next start the model checking
577
SetStatus("Model checking...");
579
strcpy(output,"XXXXXX");
580
(void)mkstemp(output);
583
string command = "NuSMV " + bufstr + " > " + output;
584
system(command.getstr()); // do the actual model checking
587
// parse the model checker's output
588
::adsmcoutputin=fopen(output,"r");
594
bool b=adsmcoutputparse();
597
error("I couldn't parse the model checker's output\n");
601
unlink(output); // cleanup
602
unlink(req); // cleanup
603
unlink(buf); // cleanup
607
mctxt="Not every run leads to a final state node;see the counter example\n";
608
ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
613
// Now check for dead nodes and transitions
615
string nodead = ah->DeadEdgesNodesConstraints();
617
ofile2->Open(&bufstr);
618
ac->WriteSMVFile(ofile2,False);
619
(*ofile2) << "\nSPEC\n" << nodead << "\n\n";
623
command += bufstr + " > " + output;
624
system(command.getstr()); // do the actual model checking
626
// parse the model checker's output
627
::adsmcoutputin=fopen(output,"r");
633
b=adsmcoutputparse();
635
error("I couldn't parse the model checker's output\n");
639
List <Subject *> ahnodes;
640
ah->GetNodes(&ahnodes);
642
for (ahnodes.first();!ahnodes.done();ahnodes.next()){
643
if ((ahnodes.cur()->GetClassType()==Code::NOTE)|| (ahnodes.cur()->GetClassType()==Code::COMMENT)) continue;
644
if (ah->GetBound(ahnodes.cur())==0){
645
string nodename= *ahnodes.cur()->GetName();
646
deadnodes+= "\n" + nodename ;
650
if ((!mcfeedback) && (!deadnodes.length())) {
651
mctxt="The general requirement is satisfied:\n\tEvery run leads to final state nodes\n\tThere are no dead nodes\n\tThere are no dead transitions\n";
652
ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
655
if (!deadnodes.length()) // are there dead nodes?
656
mctxt="There are some dead transitions: see feedback.\n";
658
mctxt="There are some dead nodes and perhaps transitions:\nNode(s)\n\t" +deadnodes +"\n\nis/are dead.\n" + "See also the feedback.\n";
659
ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
660
if (mcfeedback) ProvideFeedback(ac);
665
unlink(output); // cleanup
666
unlink(req); // cleanup
667
unlink(buf); // cleanup
670
GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
671
SetStatus("Model checking done");
677
// the feedback is stored in ::mctrace
678
void ATDiagram::ProvideFeedback(ADSCks *ac){
681
// color all nodes gray
682
this->GetGraph()->GetNodes(&ls);
683
for (ls.first();!ls.done();ls.next()){
684
GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
685
if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
686
((NodeShape *)gs)->UpdateFillColor(new string("gray"));
688
((NodeShape *)gs)->UpdateColor(new string("gray"));
689
gs->GetName()->UpdateColor(new string("gray"));
692
// color all edges gray
694
this->GetGraph()->GetEdges(&ls);
695
for (ls.first();!ls.done();ls.next()){
696
GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
697
((NodeShape *)gs)->UpdateColor(new string("gray"));
698
gs->GetName()->UpdateColor(new string("gray"));
701
// color initial node red
703
this->GetGraph()->GetNodes(&ls,Code::ATD_INITIAL_STATE_NODE); // get all the initial nodes (ideally one, but I do not check this here)
704
for (ls.first();!ls.done();ls.next()){
705
GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
706
if (gs->GetClassType()==Code::BLACK_DOT){ // just to be sure...
707
((NodeShape *)gs)->UpdateColor(new string("red"));
711
List <ADSTransition *> amtransition;
712
ac->GetEdges((List <Subject *> *)&amtransition);
713
for (amtransition.first();!amtransition.done();amtransition.next()){
714
int sourcenum=((ADSValuation *)amtransition.cur()->GetSubject1())->GetNumber(); // get value of c___counter in source state of amtransition.cur()
715
bool foundsource=False;
717
for (i=0;i<(::mctraceindex);i++){
718
if (mctrace[i]==sourcenum){ // mctrace[i] is source of transition
723
if (!foundsource) continue; // amtransition.cur() is not part of the trace
724
int targetnum=((ADSValuation *)amtransition.cur()->GetSubject2())->GetNumber();
725
bool foundtarget=False;
727
for (j=i+1;j<(::mctraceindex);j++){
728
if (mctrace[j]==targetnum){// mctrace[j] is target of transition
733
if (!foundtarget) continue;// amtransition.cur() is not part of the trace
735
// amtransition.cur() is part of the error trace, so it should be highlighted
737
Bag <ADSHyperEdge *> step;
738
amtransition.cur()->GetStep(step); // the step taken in the current transition (possibly empty)
739
List <ADSHyperEdge *> steplist;
740
step.GetSet(&steplist);
741
for (steplist.first();!steplist.done();steplist.next()){
742
List <Subject *> simpleedges;
743
steplist.cur()->GetEdges(&simpleedges);
744
for (simpleedges.first();!simpleedges.done();simpleedges.next()){
745
GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());
746
gs->UpdateColor(new string("blue"));
747
gs->GetName()->UpdateColor(new string("blue"));
748
gs=GetDiagramViewer()->GetShape(((Edge *)simpleedges.cur())->GetSubject2()); // only the target needs to be high-lighted, the source has already been highlighted, since it is the target of another transition.
749
if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
750
((NodeShape *)gs)->UpdateFillColor(new string("red"));
752
gs->UpdateColor(new string("red"));
753
gs->GetName()->UpdateColor(new string("red"));
759
//extern string replace(string s); // defined in adscks
762
void ATDiagram::ProvideFeedback(ADSHyperGraph *ah){
764
this->GetGraph()->GetNodes(&ls,Code::ATD_INITIAL_STATE_NODE); // get all the initial nodes (ideally one, but I do not check this here)
765
for (ls.first();!ls.done();ls.next()){
766
GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
767
if (gs->GetClassType()==Code::BLACK_DOT){ // just to be sure...
768
((NodeShape *)gs)->UpdateColor(new string("red"));
772
List <Subject *> nodes;
773
this->GetGraph()->GetNodes(&nodes);
775
List <Subject *> hedges;
776
ah->GetHyperEdges(&hedges);
777
for (int j=0;j<(::statecounter-1);j++){ // j counts the current state of the error trace
779
while ((i<(::enabledindex))&&(enabledstatenumber[i]<j)) i++;
780
if (enabledstatenumber[i]>j) continue;
781
List <ADSHyperEdge *> step;
782
for (int k=i;k<(::enabledindex) && enabledstatenumber[k]==j ;k++){
783
for (hedges.first();!hedges.done();hedges.next()){
784
if ((int)hedges.cur()->GetId()==enabledhyperedge[k]){
785
step.add((ADSHyperEdge *)hedges.cur()); // the enabled hyperedges in state j
786
break; // hyperedge found, so abort loop
790
int steplen=step.count();
791
bool taken[100]; // taken[i] iff step[i] is taken
792
for (int sl1=0;sl1<steplen;sl1++){
793
List <ADSHyperEdge *> conflict;
794
step[sl1]->GetConflict(&conflict);
795
if (!conflict.count()) taken[sl1]=True;
796
// if an enabled hyperedge is taken, then in the next state j+1 its source is set to zero and its target is set to one
798
for (conflict.first();!conflict.done();conflict.next()){
799
if (step.contains(conflict.cur())){
801
int nextstateindex=0;
802
List <Subject *> target; // all the nodes set to one in state j+1
804
while ((nextstateindex<(::targetindex))&&(::targetstatenumber[nextstateindex ]<=j)) nextstateindex++ ;
806
for (;(nextstateindex<(::targetindex)) && (::targetstatenumber[nextstateindex]==j+1);nextstateindex++){
807
string s=::targetname[nextstateindex];
808
for (nodes.first();!nodes.done();nodes.next()){
809
string nodename= *(nodes.cur()->GetName());
810
if (replace(nodename)==s){ // targetname[i] is a node
811
target.add(nodes.cur());
818
List <Subject *> *target1=step[sl1]->GetSubject2();
819
List <Subject *> *target2=conflict.cur()->GetSubject2();
820
for (target1->first();!target1->done();target1->next()){
821
if ((!target2->contains(target1->cur())) &&(target.contains(target1->cur()))){ // target1->cur() uniquely identifies step[sl1]; step[sl1] is taken
827
for (target2->first();!target2->done();target2->next()){
828
if ((!target1->contains(target2->cur())) && (target.contains(target2->cur()))){ // conflict.cur() is taken
830
error("Two conflicting edges seem to be taken....\n");
838
bool showingstep=False;
839
for (int sl1=0;sl1<steplen;sl1++){
840
showingstep=showingstep || taken[sl1];
842
List <Subject *> simpleedges;
843
step[sl1]->GetEdges(&simpleedges);
844
for (simpleedges.first();!simpleedges.done();simpleedges.next()){
845
GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());
846
gs->UpdateColor(new string("blue"));
847
gs=GetDiagramViewer()->GetShape(((Edge *)simpleedges.cur())->GetSubject2()); // only the target needs to be high-lighted, the source has already been highlighted, since it is the target of another transition.
848
if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
849
((NodeShape *)gs)->UpdateFillColor(new string("red"));
851
gs->UpdateColor(new string("red"));
855
if ((!showingstep) && (steplen)){
856
error ("I could not show a step!\n");
866
bool ATDiagram::ComputeHyperGraph(ADSHyperGraph *ah){
868
Elim el; // functional class that maps graph into hypergraph
869
// if (am) delete am; // commented since otherwise a segmentation fault occurs
870
SetStatus("computing hypergraph");
871
Graph *g=(ATGraph *)this->GetGraph();
872
b=el.EliminatePseudoStateNodes(g,ah); // the actual elimination
873
ah->Initialise(); // compute conflicts between activities
874
SetStatus("hypergraph file computed");
878
void ATDiagram::ComputeCKS(ADSHyperGraph *ah, ADSCks *ac, bool reduction){
879
ADSSem adssem; // functional class that maps hypergraph to kripke structure
880
// if (cl) delete cl;
882
adssem.ComputeCKS(ah,ac,reduction); // the actual semantics
886
// the following procedure does not work yet
887
//void ATDiagram::ComputeImpCKS(ADSHyperGraph *ah, ADSCks *ac){
888
// ADSSem adssem; // functional class that maps hypergraph to kripke structure
889
// // if (cl) delete cl;
891
// // adssem.ComputeImpCKS(ah,ac); // the actual semantics
896
// make nodes and edges black
897
void ATDiagram::ClearTrace() {
898
List <Subject *> nodes;
899
this->GetGraph()->GetNodes(&nodes,Code::ATD_INITIAL_STATE_NODE);
900
for (nodes.first();!nodes.done();nodes.next()){
901
GShape *gs= GetDiagramViewer()->GetShape(nodes.cur());
902
((NodeShape *)gs)->UpdateColor(new string("black"));
904
List <Subject *> simpleedges;
905
this->GetGraph()->GetEdges(&simpleedges);
906
for (simpleedges.first();!simpleedges.done();simpleedges.next()){
907
GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());
908
gs->UpdateColor(new string("black"));
909
gs->GetName()->UpdateColor(new string("black"));
910
gs=GetDiagramViewer()->GetShape(((Edge *)simpleedges.cur())->GetSubject2()); // only the target needs to be high-lighted, the source has already been highlighted, since it is the target of another transition.
911
if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
912
((NodeShape *)gs)->UpdateFillColor(new string("black"));
914
gs->UpdateColor(new string("black"));
915
gs->GetName()->UpdateColor(new string("black"));
added
removed
src/sd/bv/atdiagram.c
