scdiagram.c

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

//			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 *SCDiagram::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 SCDiagram::CheckDocument() {
	chkbuf = "";
	unsigned total = 0;
//	total += scChecks->CheckNamelessNodes(Code::INITIAL_STATE, chkbuf);
//	total += scChecks->CheckNamelessNodes(Code::STATE, chkbuf);
//	total += scChecks->CheckNamelessNodes(Code::DECISION_POINT, chkbuf);
//	total += scChecks->CheckDoubleNodes(Code::STATE, chkbuf);
//	total += scChecks->CheckDoubleNodes(Code::DECISION_POINT, chkbuf);
//	total += scChecks->CheckDoubleEvents(chkbuf);
//	total += scChecks->CheckEmptyEvents(chkbuf);
//	total += scChecks->CheckEmptyActions(chkbuf);
//	total += scChecks->CheckNoActions(chkbuf);
//	total += scChecks->CheckCountEdgesFrom(Code::DECISION_POINT, 
//		Code::TRANSITION, 2, INT_MAX, False, False, chkbuf);
//	int sub = scChecks->CheckNodeCount(1, Code::INITIAL_STATE, chkbuf);
//	total += sub;
//	if (sub == 0) {
//		total += scChecks->CheckReachability(
//			Code::INITIAL_STATE, Code::STATE, False, chkbuf);
//		total += scChecks->CheckReachability(
//			Code::INITIAL_STATE, Code::DECISION_POINT, False, chkbuf);
//	}
	ReportCheck(total, &chkbuf);
}


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


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


//void SCDiagram::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);
//	tmpModel += ".smv";
//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 SCDiagram::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);
	tmpModel += ".smv";
	std::cout << "Temporary model file: " << tmpModel.getstr() << '\n';

	OutputFile *ofile2= new OutputFile();
        ofile2->Open(&tmpModel);
	SCGraph *scg=(SCGraph *)this->GetGraph();
        scg->WriteNuSMV(ofile2,True);
	string f=*formula;
	(*ofile2) << "\nSPEC\n" << f<< "\n";
        ofile2->Close();
        
	//	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");




  char output[6];
  strcpy(output,"XXXXXX");
  (void)mktemp(output); // replaces the six X's with a string that can be used to create a unique file name 
 
  string command = "NuSMV model.smv > ";
  string outputfile= output;
  outputfile += ".out";

  command = command + outputfile;
  std::cout << "Executing command\t" << command;
  system(command.getstr()); // do the actual model checking
  std::cout.flush();
  std::cerr.flush();


  // parse the model checker's output
  ::adsmcoutputin=fopen(outputfile.getstr(),"r");
  ::mctraceindex=0;
  ::statecounter=0;
  ::sourceindex=0;
  ::targetindex=0;
  ::enabledindex=0;
  ::eventIndex=0;
  for (int i=0; i<2000; i++) ::isStable[i]= 0;

  bool b=adsmcoutputparse(); 
  if (b) {
    error("I couldn't parse the model checker's output\n"); 
    return ;
  }
  
  string mctxt;
  if (!mcfeedback) {
    mctxt="The requirement is satisfied\n";
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
  }
  else{
    mctxt="The requirement is not satisfied; see the counter example\n";
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
    AbstractSequenceDiagram *asd= GenerateAbstractSequenceDiagram();
    ConcreteSequenceDiagram *csd= GenerateConcreteSeqDiag(asd);
    GenerateSeqDiagFile(csd, formula);    
  }

  GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
  unlink(output); // cleanup buf
  //  unlink(req);
  //  unlink(buf); // cleanup if wanted	

  return;
}

void SCDiagram::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;
		}
	}

	//	SCDSMV s(GetGraph());
	//	s.WriteSMV(path->getstr(), &intevent, formula);
}


bool SCDiagram::ExecuteModelChecker(const string *path, const string *formula) {
	return False;
}



List<SCDTransitionEdge *> SCDiagram::ComputeMicroStep (SCGraph *gr, int state)
{
  /* This function takes the graph and the number of a state in the NuSMV counterexample trace. It computes the
     transitions to be fired from state to state+1, i.e., the transitions in the microstep.
     Please note that the states are numbered from 0 to ::statecounter-1.
  */


  // state refers to an state of the Kripke structure

  
  
  List<SCDTransitionEdge *> enabledTrans, step;
  List<Subject *> hedges;
  int i;
  int nextState;
  int st;
  int ev;
  int aux;
  int ntrans;
  bool found;
  bool fired;




  if (state >=0 && state < ::statecounter){

    nextState= state +1;

    
    i=0;


    while ((i<(::enabledindex))&&(enabledstatenumber[i]<state))
           i++;
    if (enabledstatenumber[i]>state) // if there is no enabled transition in the specified state of the Kripke Structure (KS)
      return step; //empty

    // Now enabledhyperedge[i] (and possibly some of its followers) is an enabled transition in KS state.
    // We collect all the corresponding SCDTransitionEdge objects in the list "enabledTrans",
    // using the information contained in enabledhyperedge (which come from the NuSMV output).

    gr->GetEdges(&hedges);


    for (int k=i; k<(::enabledindex) && enabledstatenumber[k]==state; k++){
       for (hedges.first();!hedges.done();hedges.next()){
	if ((int)hedges.cur()->GetId()==enabledhyperedge[k]){	
	    enabledTrans.add((SCDTransitionEdge *)hedges.cur()); // the enabled hyperedges in "state"
	    break; // hyperedge found, so abort loop
	}
      }
    }

    // Now enabledTrans contains all the enabled transitions in the specified state.

    ntrans= enabledTrans.count();

      
    for (int et=0; et< ntrans; et++){  //for each enabled transition et

          // We will infer if the transition is taken as in Chan's paper:
	  //  - in the next state, its target is set to one
	  //  - in the next state, the possible action event is set to one
 
          // First we look for the states which are true in the next state.
          // Remember that in targetname we have all the states which are true in the trace.
          found= False;
	  st=0;
	  while (st < targetindex && !found)
	    if (targetstatenumber[st]==nextState)
	      found= True;
	    else
	      st++;
	  // Now in targetname[st] (and possibly, in some of its followers) we have a state that will been entered in the next state
	  // of the KS.
	  // We check if the target state of et is in the set of states which will been entered in the next state.
	  found= False;
	  while (st < targetindex && targetstatenumber[st]==nextState && !found)
	    if (strcmp(targetname[st], enabledTrans[et]->GetSubject2()->GetName()->getstr())==0)
	      found= True;
	    else
	      st++;
	  
	  if (found){
	    if (enabledTrans[et]->GetSendEvent()==NULL) // the transition hasn't send event
	      fired= True;
	    else { // et has send event
	            
	      // Now we have to check that the possible action event of et is sent in the next state.
	      found= False;
	      ev= 0;
	      while (ev < eventIndex && !found)
	        if (occurredEventStates[ev]==nextState)
		  found= True;
	        else
		  ev++;

	      // Now in occurredEvents[ev] (and possibly, in the followers) we have an event which will occur in the next state of the KS.
	      // We check that the send event of et is in the set of occurred events in the next state of the KS.
	      found= False;
	      while (ev < eventIndex && occurredEventStates[ev]==nextState && !found)
		if (strcmp(occurredEvents[ev], enabledTrans[et]->GetSendEvent()->GetName().getstr())==0)
		  found= True;
	        else
		  ev++;
	      
	      fired= found;

	    }
	  }
	  else
	    fired= False;
	  
	  
	  if (fired) //then we add the transition to the step
	    step.add (enabledTrans[et]);
    }

  }
  return step;
} 




AbstractSequenceDiagram * SCDiagram::GenerateAbstractSequenceDiagram ()
{

  AbstractSequenceDiagram *asd;
  int currentState; // current state of the Kripke structure
  int formerState; // state of the Kripke structure where the last processed event was produced
  int ev; // counter for events
  InteractionRow * row;
  SCGraph *theGraph;
  Prop *prop;
  string str;
  List<SCDTransitionEdge *> step;

  
  theGraph= (SCGraph *)GetGraph();


  asd= new AbstractSequenceDiagram;
  str= "Environment";
  asd->AddParticipant(str);
  str= "System";
  asd->AddParticipant(str);

  
  formerState= -1;
  
  for (ev=0; ev<eventIndex; ev++){
    
    // First let's see if ev is really an event (note that it can also be stable (from stable = 1),
    // events (from events = 1), and so on. If it is an event, it will be in the property list of the graph
    // and will have an appropiate type.
    prop= theGraph->EventInPropl(occurredEvents[ev]);
    if (prop && (prop->GetType()==::EV_FROM_ENV ||
                 prop->GetType()==::EV_TO_ENV ||
                 prop->GetType()==::EV_INT)){ //ok, it is an event!
        currentState= ::occurredEventStates[ev];
        if (formerState != currentState) //we need a new row!
	    row= asd->AddRow(currentState); //add a new row with the correct number of columns; it also returns the row
        
        // row is the current row in which we have to include the event
        if (prop->GetType()==::EV_FROM_ENV)
	    row->participants[0].AddPairObjEv(1,prop->GetName());
        else if (prop->GetType()==::EV_TO_ENV)
	    row->participants[1].AddPairObjEv(0,prop->GetName());
        else{ //EV_INT
	    row->participants[1].AddPairObjEv(1, prop->GetName());
	    step= ComputeMicroStep (theGraph, currentState-1); //computes the fired transitions from
	    // the KR states currentState-1 to currentState.
	    // With this, we get the transitions that have been fired. The event ev must be in the
	    // action part of some transition in the set. We have to check if it is EV_INT_BC in that
	    // transition.
	    if (IsBroadcast (prop->GetName(), step))
	      row->participants[1].AddPairObjEv(0, prop->GetName());	    
        }
	formerState= currentState;
    }
  }  

  return asd;


}


bool SCDiagram::IsBroadcast (string event, List<SCDTransitionEdge *> step)
{
  bool found= false;
  int i= 0;
  Prop *prop;

  while (i< step.count() && !found){
    if (step[i]->GetSendEvent()){ //it has send event
      prop= step[i]->GetSendEvent();
      if (prop->GetName()==event && prop->GetType()==::EV_INT_BC)
	found= true;
      else
	i++;
    }
    else
      i++;
  }

  return found;
}





ConcreteSequenceDiagram * SCDiagram::GenerateConcreteSeqDiag (AbstractSequenceDiagram *asd)
{
  ConcreteSequenceDiagram *csd;
  ConcreteParticipant *cp;
  InteractionRow *row;
  InteractionParticipant *ip;
  PairObjEv *pair;
  StimulusInfo *sinf;
  Stimulus *stim1;
  Stimulus *stim2;
  int stimY;
  int formerState, currentState;

  string microstep= "-----------------microstep-----------------";
  string stable=    "------------------stable-------------------";
  

  int i, j, k, ev;
  bool found;

  if (asd==NULL) return NULL;

  csd= new ConcreteSequenceDiagram;

  
  
  // First we create all the ConcreteParticipants, in the same order as in AbstractSequenceDiagram.
  // note that this is just the trivial ordering, but it is possible also to have other layouts (different orderings
  // of the participants).
  for (i=0; i< asd->numObjs; i++){
    cp= new ConcreteParticipant();
    cp->name= asd->objNames[i];
    cp->logicalId= csd->NextId();
    cp->shapeId= csd->NextId();
    cp->y= 50; //we set all the objects to a height of 50
    cp->x= 120+i*280; //this way every object will be horizontally separated by 280 units from its neighbours.
    csd->participants.add (cp);
  }
  
  // Now we travel across all the happened events.
  // We create StimulusInfo objects for the list of stimuli, and
  // we attach those stimuli to the concrete participants created
  // above.
  for (i=0; i< asd->rows.count(); i++){
    
    if (i==0){
      // A microstep begins in the diagram. We add the proper comment.
      // Note that it's simulating a false message from the first participant
      // to the last one. This way the comment extends over all the objects.
      // Note that we do not add the stimuli in the anchor lists of the objects,
      // as it is not an anchor.
      sinf= new StimulusInfo();
      sinf->sender= csd->participants[0];
      sinf->receiver= csd->participants[csd->participants.count()-1];
      sinf->label= stable;