atdiagram.c

这个工具集提供以下结构化分析和UML分析中所用的图形化绘图工具：ER-diagrams, data and event flow diagrams and state-transition diagr

////////////////////////////////////////////////////////////////////////////////
//
// This file is part of Toolkit for Conceptual Modeling (TCM).
// (c) copyright 1999, Vrije Universiteit Amsterdam and University of Twente.
// Author: Frank Dehne ([e-mail]).
// Author: Henk van de Zandschulp ([e-mail]).
//
// TCM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// TCM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with TCM; if not, write to the Free Software
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
////////////////////////////////////////////////////////////////////////////////
#include "atdactionstatenode.h"
#include "atddecisionstatenode.h"
#include "atdfinalstatenode.h"
#include "atdwaitstatenode.h"
#include "atdinitialstatenode.h"
#include "atdsynchronizationnode.h"
#include "atdtransitionedge.h"
#include "emptynode.h"
#include "blackdot.h"
#include "bullseye.h"
#include "note.h"
#include "notebox.h"
#include "roundedbox.h"
#include "ellipsedbox.h"
#include "solidhorizontalbar.h"
#include "solidverticalbar.h"
#include "minidiamond.h"
#include "line.h"
#include "textbox.h"
#include "comment.h"
#include "commentlink.h"
#include "atchecks.h"
#include "atdiagram.h"
#include "atgraph.h"
#include "atviewer.h"
#include "atwindow.h"

#include "system.h"  
#include "adshypergraph.h"
#include "adssemantics.h"                                           /*new*/
#include "adseliminatepseudostatenodes.h"
#include "adspropertyvaluation.h"
#include "adsproperty.h"
#include "temporalpropertydialog.h"
#include "outputfile.h"
#include "inputfile.h"
#include "adsmcoutputparse.h"
#include "adsltlformulaparse.h"
//#include "adsmcoutput.tab.h"
#include <limits.h>
#include <stdlib.h>
#include <unistd.h>


const int ATDiagram::DOT_WIDTH = 8;
 
ATDiagram::ATDiagram(Config *c, ATWindow *d, ATViewer *v, ATGraph *g): 
		Diagram(c,d,v,g) {
	UpdateNodeType(1);
	UpdateEdgeType(1);
	atChecks = new ATChecks(this,g);
}

ATDiagram::~ATDiagram() {
	delete atChecks;
}

Thing *ATDiagram::CreateThing(int classNr) {
	Grafport *g = GetDiagramViewer()->GetGrafport();
	ShapeView *v = GetDiagramViewer()->GetCurView();
	ATGraph *cg = (ATGraph *)GetGraph();
	Thing *thing = 0;

	if (classNr == Code::ELLIPSED_BOX)
		thing = new EllipsedBox(v, g, 0, 0); 
	else if (classNr == Code::ROUNDED_BOX)
		thing = new RoundedBox(v, g, 0, 0); 
	else if (classNr == Code::MINI_DIAMOND)
		thing = new MiniDiamond(v, g, 0, 0); 
	else if (classNr == Code::BLACK_DOT)
		thing = new BlackDot(v, g, 0, 0); 
	else if (classNr == Code::BULLS_EYE)
		thing = new BullsEye(v, g, 0, 0); 
	else if (classNr == Code::SOLID_HORIZONTAL_BAR)
                thing = new SolidHorizontalBar(v, g, 0, 0);
	else if (classNr == Code::SOLID_VERTICAL_BAR)
                thing = new SolidVerticalBar(v, g, 0, 0);
	else if (classNr == Code::NOTE_BOX)
                thing = new NoteBox(v, g, 0, 0);
	else if (classNr==Code::TEXT_BOX)
		thing = new TextBox(v, g, 0, 0); 

	else if (classNr == Code::VIEW)
		thing = new ShapeView(GetDiagramViewer()); 

	else if (classNr == Code::LINE)
		thing = new Line(v, g, 0, 0, 0);
	// old line (arrow) types...
	else if (classNr == Code::ARROW) {
		Line *line = new Line(v, g, 0, 0, 0);
		line->SetEnd2(LineEnd::FILLED_ARROW);
		thing = line;
	}

	else if (classNr==Code::INITIAL_STATE || classNr == Code::ATD_INITIAL_STATE_NODE)
		thing = new ATDInitialStateNode(cg);
	else if (classNr == Code::ATD_ACTION_STATE_NODE)
		thing = new ATDActionStateNode(cg);
	else if (classNr == Code::ATD_WAIT_STATE_NODE)
		thing = new ATDWaitStateNode(cg);
	else if (classNr == Code::ATD_DECISION_STATE_NODE)
		thing = new ATDDecisionStateNode(cg);
	else if (classNr == Code::ATD_SYNCHRONIZATION_NODE)
		thing = new ATDSynchronizationNode(cg);
	else if (classNr==Code::FINAL_STATE || classNr == Code::ATD_FINAL_STATE_NODE)
		thing = new ATDFinalStateNode(cg);
	else if (classNr == Code::NOTE)
		thing = new Note(cg);
	else if (classNr == Code::COMMENT)
		thing = new Comment(cg);

	// edges
	else if (classNr==Code::TRANSITION || classNr == Code::ATD_TRANSITION_EDGE)
		thing = new ATDTransitionEdge(cg, 0, 0);
	else if (classNr==Code::COMMENT_LINK)
		thing = new CommentLink(cg, 0, 0);

	else {
		error("%s, line %d: impl error: " "wrong class number %d\n", 
			__FILE__, __LINE__, classNr);
		return 0;
	}
	if (thing != 0 && HasIndexShape(thing->GetClassType()))
		((NodeShape *)thing)->SetFixedIndexLabel(False);

	return thing;
}

Node *ATDiagram::CreateNode(){
	Node *node = 0;
	ATGraph *g = (ATGraph *)GetGraph();
	if (GetNodeType() == Code::ATD_INITIAL_STATE_NODE)
		node = new ATDInitialStateNode(g);
	else if (GetNodeType() == Code::ATD_ACTION_STATE_NODE)
		node = new ATDActionStateNode(g);
	else if (GetNodeType() == Code::ATD_WAIT_STATE_NODE)
		node = new ATDWaitStateNode(g);
	else if (GetNodeType() == Code::ATD_DECISION_STATE_NODE)
		node = new ATDDecisionStateNode(g);
	else if (GetNodeType() == Code::ATD_SYNCHRONIZATION_NODE)
		node = new ATDSynchronizationNode(g);
	else if (GetNodeType() == Code::ATD_FINAL_STATE_NODE)
		node = new ATDFinalStateNode(g);
	else if (GetNodeType() == Code::NOTE)
		node = new Note(g);
	else if (GetNodeType() == Code::COMMENT)
		node = new Comment(g);
	else
		error("%s, line %d: impl error: "
			"unknown node type\n", __FILE__, __LINE__);
	return node;
}

Edge *ATDiagram::CreateEdge(Subject *node1, Subject *node2){
	// Check possible connections (node-node-edge matrix).
	if (!CheckConnection(node1, node2))
		return 0; 
	if ((GetEdgeType() == Code::ATD_TRANSITION_EDGE) &&
	    (node1->GetClassType() == Code::ATD_DECISION_STATE_NODE) && 
	    (node1 == node2)) {
		ShowDialog(MessageDialog::ERROR, "Error",
			       "This is not a valid transition");
		return 0;
	}
	Edge *edge = 0;
	ATGraph *g = (ATGraph *)GetGraph();
	if (GetEdgeType()==Code::COMMENT_LINK)
		edge = new CommentLink(g, node1, node2);
	else if (GetEdgeType() == Code::ATD_TRANSITION_EDGE)
		edge = new ATDTransitionEdge(g, node1, node2);

	else 
		error( "%s, line %d: impl error: "
			" unknown edge type\n", __FILE__, __LINE__);
	return edge;
}

NodeShape *ATDiagram::CreateNodeShape(Node *node, int x, int y) {
	NodeShape *shape = 0;
	Grafport *g = GetDiagramViewer()->GetGrafport();
	ShapeView *v = GetDiagramViewer()->GetCurView();
	int t = GetNodeShapeType();
	if (t == Code::ELLIPSED_BOX)
		shape = new EllipsedBox(v, g, x, y);
	else if (t == Code::ROUNDED_BOX)
		shape = new RoundedBox(v, g, x, y);
	else if (t == Code::MINI_DIAMOND)
		shape = new MiniDiamond(v, g, x, y);
	else if (t == Code::NOTE_BOX)
		shape = new NoteBox(v, g, x, y);
	else if (t == Code::BLACK_DOT)
		shape = new BlackDot(v, g, x, y);
	else if (t == Code::BULLS_EYE)
		shape = new BullsEye(v, g, x, y);
	else if (t == Code::SOLID_HORIZONTAL_BAR)
                shape = new SolidHorizontalBar(v, g, x, y);
	else if (t == Code::SOLID_VERTICAL_BAR)
                shape = new SolidVerticalBar(v, g, x, y);
	else if (t == Code::TEXT_BOX)
		shape = new TextBox(v, g, x, y);
	else {
		error( "%s, line %d: impl error: "
			"node shape type does not exist\n", __FILE__, __LINE__);
	}
	if (check(shape)) {
		if (HasIndexShape(t))
			shape->SetFixedIndexLabel(False);
		shape->SetSubject(node);
		shape->SetTextShape();
	}
	return shape;
}

Line *ATDiagram::CreateLine(
		Edge *edge, GShape *from, GShape *to, List<Point *> *l) {
	Grafport *g = GetDiagramViewer()->GetGrafport();
	ShapeView *v = GetDiagramViewer()->GetCurView();
	Line *line = 0;
	int t = GetLineType();
	if (t == Code::LINE)
		line = new Line(v, g, from, to, l, IsCurve());
	else
		error( "%s, line %d: impl error: "
			"line type does not exist\n", __FILE__, __LINE__);
	if (check(line)) {
		line->SetSubject(edge);
		line->SetTextShape();
		line->SetEnd1(GetLineEnd1());
		line->SetEnd2(GetLineEnd2());
	}
	return line;
}

void ATDiagram::UpdateNodeType(int num) {
	((DiagramWindow *)GetMainWindow())->SetNodeName(num);
	switch (num) {
	case 1: SetNodeType(Code::ATD_ACTION_STATE_NODE);
		SetNodeShapeType(Code::ELLIPSED_BOX);
		break;
	case 2: SetNodeType(Code::ATD_DECISION_STATE_NODE);
		SetNodeShapeType(Code::MINI_DIAMOND);
		break;
	case 3: SetNodeType(Code::ATD_SYNCHRONIZATION_NODE);
		SetNodeShapeType(Code::SOLID_HORIZONTAL_BAR);
		break;
	case 4: SetNodeType(Code::ATD_INITIAL_STATE_NODE);
                SetNodeShapeType(Code::BLACK_DOT);
                break;
	case 5: SetNodeType(Code::COMMENT);
		SetNodeShapeType(Code::TEXT_BOX);
		SetNodeLineStyle(LineStyle::INVISIBLE);
		break;
	case 6: SetNodeType(Code::ATD_WAIT_STATE_NODE);
		SetNodeShapeType(Code::ROUNDED_BOX);
		break;
	case 7: SetNodeType(Code::NOTE);
		SetNodeShapeType(Code::NOTE_BOX);
		break;
	case 8: SetNodeType(Code::ATD_SYNCHRONIZATION_NODE);
		SetNodeShapeType(Code::SOLID_VERTICAL_BAR);
		break;
	case 9: SetNodeType(Code::ATD_FINAL_STATE_NODE);
		SetNodeShapeType(Code::BULLS_EYE);
		break;
	default:
		error("%s, line %d: impl error: "
		"unknown node type selected\n", __FILE__,__LINE__);
	}
}

void ATDiagram::UpdateEdgeType(int num) {
	((DiagramWindow *)GetMainWindow())->SetEdgeName(num);
	switch(num) {
	case 1: SetEdgeType(Code::ATD_TRANSITION_EDGE);
		SetLineType(Code::LINE);
		SetEdgeLineStyle(LineStyle::SOLID);
		SetLineEnd1(LineEnd::EMPTY);
		SetLineEnd2(LineEnd::FILLED_ARROW);
		break;
	case 2: SetEdgeType(Code::COMMENT_LINK);
		SetLineType(Code::LINE);
		SetEdgeLineStyle(LineStyle::WIDE_DOTTED);
		SetLineEnd1(LineEnd::EMPTY);
                SetLineEnd2(LineEnd::EMPTY);
		break;
	default:
		error("%s, line %d: impl error: "
			"unknown edge type selected\n", __FILE__,__LINE__);
	}
}

bool ATDiagram::HasIndexNode(int code) {
	return (code == Code::ATD_ACTION_STATE_NODE ||
		code == Code::ATD_WAIT_STATE_NODE ||
		code == Code::ATD_DECISION_STATE_NODE);
}

bool ATDiagram::HasIndexShape(int code) {
	return (code==Code::ROUNDED_BOX ||
		code==Code::ELLIPSED_BOX ||
		code==Code::DIAMOND ||
		code==Code::NOTE_BOX);
}

void ATDiagram::CheckDocument() {
	chkbuf = "";
	unsigned errors = 0;
	errors += atChecks->CheckNodeCount(1, Code::ATD_INITIAL_STATE_NODE, chkbuf);
	errors += atChecks->CheckNodeCount(1, Code::ATD_FINAL_STATE_NODE, chkbuf);
	if (errors == 0)    // only useful with 1 INITIAL && 1 FINAL state
		errors += atChecks->CheckUnreachableStates(chkbuf);
	errors += atChecks->CheckNodeCount(1, INT_MAX, Code::ATD_ACTION_STATE_NODE, chkbuf);

	errors += atChecks->CheckNamelessNodes(Code::ATD_ACTION_STATE_NODE, chkbuf);
	errors += atChecks->CheckNamelessNodes(Code::ATD_WAIT_STATE_NODE, chkbuf);


	errors += atChecks->CheckCountEdgesFrom(Code::ATD_SYNCHRONIZATION_NODE, 
		Code::ATD_TRANSITION_EDGE, 2, INT_MAX, False, False, chkbuf);

	ReportCheck(errors, &chkbuf);
}




void ATDiagram::ModelCheckProperty() {

	int status = system("which NuSMV > /dev/null 2>/dev/null");
	if (status) {
		string URL = "http://www.cs.utwente.nl/~tcm/tatd.html"; // RIK: AANPASSEN
		string txt = "Model checker NuSMV cannot be found.";
		txt += "\n\nPlease check your PATH or the URL below for more information:";
		txt += "\n\n" + URL;
		(new MessageDialog(GetMainWindow()->GetWidget(), 
			MessageDialog::INFORMATION))->
			Show("Notice", &txt);
	}
	else {
        	SetStatus("action: model check property");
		tpd = new TPDialog(GetMainWindow()->GetWidget());
		tpd->Initialize();
		tpd->SetTitle("Model check property");
		tpd->SetOKCallback(&ModelCheckPropertyOKCB, this);
        	tpd->ManageSubstringToggle(True);
		tpd->ManageNameOnlyToggle(True);
		tpd->Popup();
	}
}


extern string replace(string s); // defined in adscks


void ATDiagram::ModelCheckPropertyOKCB(Widget w, XtPointer clientData, XtPointer) {
  ATDiagram *atd = (ATDiagram *)clientData;
  XtUnmanageChild(w);
  string fbuf;
  atd->GetTPDialog()->GetTextString(&fbuf);
  atd->DoModelCheckProperty(&fbuf, atd->GetTPDialog()->SensitiveOn(), atd->GetTPDialog()->SubstringOn(), atd->GetTPDialog()->NameOnlyOn() );
}

void ATDiagram::DoModelCheckProperty(const string *p, bool symbolic, bool reduction, bool sf) {
  // fill initial and final for the parser
  // initial and final are state predicates that characterise when a configuration is initial and when it is
  // final. The meaning of final depends upon the model being checked.


  GetMainWindow()->SetCursor(MouseCursor::WATCH);

  ADSHyperGraph *ah;
  ah=new ADSHyperGraph();    
  if (!ComputeHyperGraph(ah)) return;


  ::initial = (char *) malloc (strlen("I___INITIAL>0")+1); 
  strcpy(::initial,"I___INITIAL>0");

  string str=*p;
  str.replace('\r','_');


  // parse the property
  ::isfinal=0;
  ::identifier_count=0;
  ::isltl=1; // set to zero if ctl formula
  YY_BUFFER_STATE y = ::adsltlformula_scan_string(str.getstr());
  strcpy(::adsltlformula_constraint, "");
  bool b = !adsltlformulaparse();
  adsltlformula_delete_buffer(y);
  if (!b) {
    error("I cannot parse this property\n");
    return;
  }

  if (reduction){
    List <ADSVar *> varused; // ASSUMPTION: only boolean variables are used, so no integer expressions (what about nodes)
    List <Node *> nodeused;
    for (int i=0;i<identifier_count;i++){
      ADSVar *v=new ADSVar(identifier[i],::PROP);
      ADSVar *v_old= ah->FindSimilarVar(v);
      if (v_old){ // v occurs as variable in hypergraph ah
	varused.add(v_old);
      }
      
      string iname=identifier[i];
      Node *n= (ah->FindNode(iname));
      if (n){
	nodeused.add(n);
      }
    }
    if (::isfinal){
      List <Subject *> finalnodes;
      ah->GetFinalNodes(&finalnodes);
      for (finalnodes.first();!finalnodes.done();finalnodes.next()){
	nodeused.add((Node*)finalnodes.cur());
      }      
    }
    ah->RemoveLocalVariables(&varused);
    ah->RemoveNodes(nodeused,varused,reduction);
  }

  string sfinal=ah->ComputeFinalPredicate();
  string property=::ltlprop;
  property.replace("FINAL",sfinal);
    
 
  char buf[100]; // temporary filename for activity graph model
  strcpy(buf,"XXXXXX");
  (void)mkstemp(buf);
  string bufstr(buf);
  char req[100]; // temporarly filename for LTL property
  strcpy(req,"XXXXXX");
  (void)mkstemp(req);
  strcat(req,".req");
  FILE *ftemp;  // temporarly file for LTL property
  ftemp=fopen(req,"w");
  fprintf(ftemp,"%s",property.getstr()); // put the property in the temp file
  fclose(ftemp);
  string reqstr(req);