stdiagram.c

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

	}
	else if (n == Subject::IMPOSSIBLE_NAME) {
		string msg = "'" + *s + "' wrong syntax\n for an event string";
		ShowDialog(MessageDialog::ERROR, "Error", &msg);
		return False;
	}
	else if (n == Subject::DOUBLE_EDGE) {
		string msg = "there is already a transition with\n"
			"event string '" + *s + "' between this pair of states";
		ShowDialog(MessageDialog::ERROR, "Error", &msg);
		return False;
	}
	else {
		error("%s, line %d: case not handled\n", __FILE__, __LINE__);
	}
	return True;
}

bool STDiagram::SetAction(Subject *t, const string *s, unsigned nr) {
	List<GShape *> shapes;
	GetDiagramViewer()->GetShapes(t, &shapes);
	unsigned m = nr;
	// split string in different one line strings.
	string ss(*s);
	char *str = (char *)ss.getstr();
	char empty[2] = "";
	char *x = strtok(str, "\r");
	if (x == 0)
		x = empty;
	while (x != 0) {
		string *ns = new string(x);
		bool update = True;
		Subject::NameErrType result;
		if (m == nr) {
			if (t->IsEdge())
				result = ((Transition *)t)->SetAction(ns, m, True);
			else
				result = ((InitialState *)t)->SetAction(ns, m, True);
		}
		else {
			if (t->IsEdge())
				result = ((Transition *)t)->SetAction(ns, m, False);
			else
				result = ((InitialState *)t)->SetAction(ns, m, False);
			update = False;
		}
		if (result != Subject::OK) {
			string msg;
			if (result == Subject::HAS_ACTION)
				msg = "transition already has an action '" + *ns + "'";
			else
				msg = "'" + *ns + "' wrong syntax\n for an action string";
			ShowDialog(MessageDialog::ERROR, "Error", &msg);
			// make actions empty.
			*ns = "";
			if (!update) {
				for (shapes.first(); !shapes.done(); shapes.next()) {
					if (t->IsEdge())
						((TransitionArrow *)shapes.cur())->
							UpdateAction(ns, m, update);
					else
						((InitialStateBox *)shapes.cur())->
							UpdateAction(ns, m, update);
				}
			} 
			delete ns;
			return False;
		}
		// update the shapes.
		if (shapes.first())
			do {
				if (t->IsEdge())
					((TransitionArrow *)shapes.cur())->
						UpdateAction(ns, m, update);
				else
					((InitialStateBox *)shapes.cur())->
						UpdateAction(ns, m, update);
			} while (shapes.next());
		else {
			error("%s, line %d: shape does not exist\n", 
					__FILE__, __LINE__);
			return False;
		}
		m++;
		x = strtok(0, "\r");
		delete ns;
	}
	return True;
}

InitialState *STDiagram::FindInitialState(Subject *state) {
	if (state->GetClassType() == Code::INITIAL_STATE)
		return (InitialState *)state;
	List<Subject *> initStates;
	GetGraph()->GetNodes(&initStates, Code::INITIAL_STATE);
	for (initStates.first(); !initStates.done(); initStates.next()) {
		InitialState *init = (InitialState *)initStates.cur();
		if (GetGraph()->UndirectedPathExists(init, state))
			return init;
	} 
	return 0;
}

void STDiagram::CheckDocument() {
	chkbuf = "";
	unsigned total = 0;
	total += stChecks->CheckNamelessNodes(Code::INITIAL_STATE, chkbuf);
	total += stChecks->CheckNamelessNodes(Code::STATE, chkbuf);
	total += stChecks->CheckNamelessNodes(Code::DECISION_POINT, chkbuf);
	total += stChecks->CheckDoubleNodes(Code::STATE, chkbuf);
	total += stChecks->CheckDoubleNodes(Code::DECISION_POINT, chkbuf);
	total += stChecks->CheckDoubleEvents(chkbuf);
	total += stChecks->CheckEmptyEvents(chkbuf);
	total += stChecks->CheckEmptyActions(chkbuf);
	total += stChecks->CheckNoActions(chkbuf);
	total += stChecks->CheckCountEdgesFrom(Code::DECISION_POINT, 
		Code::TRANSITION, 2, INT_MAX, False, False, chkbuf);
	int sub = stChecks->CheckNodeCount(1, Code::INITIAL_STATE, chkbuf);
	total += sub;
	if (sub == 0) {
		total += stChecks->CheckReachability(
			Code::INITIAL_STATE, Code::STATE, False, chkbuf);
		total += stChecks->CheckReachability(
			Code::INITIAL_STATE, Code::DECISION_POINT, False, chkbuf);
	}
	ReportCheck(total, &chkbuf);
}


#ifdef MODELCHECK
void STDiagram::ModelCheckProperty() {
	SetStatus("action: model check document semantics");
	promptDialog->SetTitle("Model check document semantics");
	promptDialog->SetOKCallback(ModelCheckDocumentOKCB, this);
	promptDialog->Popup();
}


/* static */ void STDiagram::ModelCheckDocumentOKCB(Widget,
		XtPointer clientData, XtPointer)
{
	STDiagram *std = (STDiagram *)clientData;
	string formula, internal, clock;
	std->promptDialog->GetFormulaString(&formula);
	std->promptDialog->GetInternString(&internal);
	std->promptDialog->GetClockString(&clock);
	std->DoModelCheckDocument(&internal, &formula, &clock);
}


void STDiagram::DoModelCheckDocument(const string *internal,
			const string *formula, const string *clock)
{
	SetStatus("action: model check document semantics");
	GetMainWindow()->SetCursor(MouseCursor::WATCH);
	string tmpModel;
tmpModel = "model";
//	GetViewer()->GetPrinter()->MakeTmpFile(&tmpModel);
#if MODELCHECK_SMV
	tmpModel += ".smv";
#else
	tmpModel += ".tg";
#endif
std::cerr << "Temporary model file: " << tmpModel.getstr() << '\n';

	SaveForModelChecker(&tmpModel, internal, clock, formula);
	bool ok = ExecuteModelChecker(&tmpModel, formula);
	GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
//	unlink(tmpModel.getstr());
	if ( ! ok )
		SetStatus("model checking aborted");
	else
		SetStatus("model checking completed");
	return;
}


void STDiagram::SaveForModelChecker(const string *path, const string *internal,
			const string * clock, const string *formula) {
	/* Split internal into a list of strings */
	List<string> intevent;
	if ( internal ) {
		const char *cp = internal->getstr();
		while ( *cp ) {
			while ( *cp && isspace(*cp) )
				++cp;
			if ( ! *cp )
				break;
			const char *ep = cp;
			if ( '[' == *cp ) {
				while ( *++ep )
					if ( ']' == *ep ) {
						++ep;
						break;
					}
			} else
				while ( *++ep && ! isspace(*ep) && '[' != *ep )
					;
			string event;
			event.add(cp, ep - cp);
			intevent.add(event);
			cp = ep;
		}
	}

#if MODELCHECK_SMV
	SMV s(GetGraph());
	s.WriteSMV(path->getstr(), &intevent, formula);
#else
	Kronos kr(this);
	kr.GenerateKronos(&intevent);
	kr.SaveKronos(path->getstr(), clock->getstr());
#endif
}


bool STDiagram::ExecuteModelChecker(const string *path, const string *formula) {
#if MODELCHECK_SMV
	return False;
#else
	string tmpFormula;
tmpFormula = "/home/maics/dnjansen/kronos/formula";
//	GetViewer()->GetPrinter()->MakeTmpFile(&tmpFormula);
	tmpFormula += ".tctl";
	FILE *fp;
	if ( (fp = fopen(tmpFormula.getstr(), "w")) == NULL ||
	    fputs(formula->getstr(), fp) == EOF ) {
		string txt("error, ");
		txt += tmpFormula;
		txt += "\ncannot be written";
		(new MessageDialog(GetMainWindow()->GetWidget(), 
			MessageDialog::INFORMATION))->
			Show("Notice", &txt);
		return False;
	}
	fclose(fp);
	string command;
command = "/home/maics/dnjansen/kronos/bin/kronos";
//	read config...
	command += " -v -reach ";
	command += tmpFormula;
	command += ' ';
	command += *path;
	int status = system(command.getstr());
//	unlink(tmpFormula.getstr());
	if (status) {
		string txt = "error, " + command;
		txt += "\ncannot be executed";
		(new MessageDialog(GetMainWindow()->GetWidget(), 
			MessageDialog::INFORMATION))->
			Show("Notice", &txt);
		return False;
	}
	return True;
#endif
}
#endif


bool STDiagram::SetText(TextShape *t, const string *s) {
	const string *description = t->GetDescription();
	Subject *subj = t->GetParent()->GetSubject();
	if (*description == "Event")
		return SetEvent((Transition *)subj, s);
	else if (*description == "Action")
		return SetAction(subj, s, t->GetSequence());
	else 
		return Diagram::SetText(t, s);
}