1
//------------------------------------------------------------------------------
3
// This file is part of Toolkit for Conceptual Modeling (TCM).
4
// (c) copyright 2002, Universiteit Twente.
5
// Author: David Jansen (dnjansen@cs.utwente.nl).
6
// Rik Eshuis (eshuis@cs.utwente.nl)
7
// Jose Canete (canete@lsi.us.es)
9
// TCM is free software; you can redistribute it and/or modify
10
// it under the terms of the GNU General Public License as published by
11
// the Free Software Foundation; either version 2 of the License, or
12
// (at your option) any later version.
14
// TCM is distributed in the hope that it will be useful,
15
// but WITHOUT ANY WARRANTY; without even the implied warranty of
16
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17
// GNU General Public License for more details.
19
// You should have received a copy of the GNU General Public License
20
// along with TCM; if not, write to the Free Software
21
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
23
//-----------------------------------------------------------------------------
34
class ModelCheckDialog;
35
class SCDTransitionEdge;
36
class AbstractSequenceDiagram;
37
class ConcreteSequenceDiagram;
41
/// state transition diagram class
42
class SCDiagram: public Diagram {
43
/*@Doc: {\large {\bf scope:} TSCD} */
46
SCDiagram(Config *, SCWindow *, SCViewer *, SCGraph *);
50
virtual void Initialize();
54
Edge *CreateEdge(Subject *n1, Subject *n2);
56
NodeShape *CreateNodeShape(Node *node, int x, int y);
58
Line *CreateLine(Edge *edge, GShape *fromShape,
59
GShape *toShape, List<Point *> *line);
61
void UpdateNodeType(int n);
63
void UpdateEdgeType(int n);
69
/* virtual */ void ModelCheckProperty();
73
void ProvideFeedback(SCGraph *ah);
77
Thing *CreateThing(int classNr);
79
bool CheckEdgeConstraints(Subject *s1, Subject *s2);
81
bool CheckAndEdgeConstraints(Subject *s1, Subject *s2);
86
void DoModelCheckDocument(const string *internal,
87
const string *formula, const string *clock);
88
/// callback for model check document dialog
89
static void ModelCheckDocumentOKCB(Widget, XtPointer,
91
/// saves the current diagram in the model checker formal to *path.
92
void SaveForModelChecker(const string *path, const string *internal,
93
const string *clock, const string *formula);
94
/// calls the model checker for a diagram saved in *path.
95
bool ExecuteModelChecker(const string *path, const string *formula);
97
/// computes the current step of firing transitions.
98
List<SCDTransitionEdge *> ComputeMicroStep (SCGraph *gr, int state);
100
/// Creates the abstract representation for a sequence diagram from
101
/// NuSMV counterexample. This method should be called after the counterexample
102
/// has been produced!
103
AbstractSequenceDiagram * GenerateAbstractSequenceDiagram ();
105
bool IsBroadcast (string event, List<SCDTransitionEdge *> step);
106
/// Creates a possible layout from the abstract representation of the sequence diagram.
107
ConcreteSequenceDiagram * GenerateConcreteSeqDiag (AbstractSequenceDiagram *asd);
108
/// Generates the file with the sequence diagram.
109
void GenerateSeqDiagFile (ConcreteSequenceDiagram *csd, const string *formula);
111
void GenerateGraphNodes (ConcreteSequenceDiagram *csd, OutputFile *fp);
113
void GenerateComments (ConcreteSequenceDiagram *csd, OutputFile *fp);
115
void GenerateGraphEdges (ConcreteSequenceDiagram *csd, OutputFile *fp);
117
void GenerateObjectBoxes (ConcreteSequenceDiagram *csd, OutputFile *fp);
119
void GenerateT4Lines (ConcreteSequenceDiagram *csd, OutputFile *fp);
121
void GenerateTextBoxes (ConcreteSequenceDiagram *csd, OutputFile *fp);
123
void GenerateNote (ConcreteSequenceDiagram *csd, OutputFile *fp, const string *formula);
125
void GenerateNoteBox (ConcreteSequenceDiagram *csd, OutputFile *fp);
126
/// used for model checking
127
ModelCheckDialog *promptDialog;
129
}; // end class SCDiagram
134
* Classes for generating a Sequence Diagram. They should be moved to on a separate file.
144
PairObjEv (int object, string event) : obj(object), ev(event) {}
145
int GetObj () {return obj;}
146
string GetEv () {return ev;}
148
std::cout << "(" << obj << "," << ev.getstr() << ")" << std::endl; }
155
class InteractionParticipant
158
int GetNumberOfEvents () {return eventsToSend.count();}
159
void AddPairObjEv (int object, string event);
160
PairObjEv * GetPairObjEv (int i) {if (i<0 || i>static_cast<int>(eventsToSend.count()-1)) return NULL; else return eventsToSend[i];}
161
void SetId (int i) {id= i;}
162
int GetId () {return id;}
165
List<PairObjEv *> eventsToSend;
166
int id; //the id of the participant in the abstract sequence diagram
174
InteractionParticipant * participants; //array [numObj] of InteractionParticipant
176
InteractionRow (int n, int cs) : numObj(n), currentState(cs) {
177
participants= new InteractionParticipant[numObj];
178
for (int i=0; i< numObj; i++)
179
participants[i].SetId(i);
181
int GetNumberOfParticipants () {return numObj;}
182
int GetCurrentState () {return currentState;}
191
class AbstractSequenceDiagram
194
List<InteractionRow *> rows;
195
List<string> objNames;
198
AbstractSequenceDiagram () : numObjs(0) {}
200
void AddParticipant (string name) {objNames.add(name); numObjs++; }
201
InteractionRow * AddRow (int cs);
208
class ConcreteParticipant;
213
ConcreteParticipant *sender;
214
ConcreteParticipant *receiver;
216
int logicalId; // logical id in the seq.diag.
217
int shapeId; // shape id in the seq.diag.
218
int y; //the place of the stimulus in the temporal line
219
bool isComment; //if True, this is a false stimulus, i.e. a comment: "stable" and "microstep"
231
class ConcreteParticipant
238
List<Stimulus *> anchors;
243
class ConcreteSequenceDiagram
248
List<ConcreteParticipant *> participants;
249
List<StimulusInfo *> stimuli;
250
int lineLength; //end position of the lifelines
252
ConcreteSequenceDiagram() : counter(1) {}
254
int NextId () { counter++; return counter;}
added
removed
src/sd/bv/scdiagram.h
