atdiagram.c

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

  ADSCks *ac= NULL; 

  OutputFile *ofile2= new OutputFile();
  ofile2->Open(&bufstr);
  if (symbolic) {
    ah->WriteNuSMV(ofile2,sf);
  }
  else{
    ac= new ADSCks(ah); 
    ComputeCKS(ah,ac,reduction);
    ac->WriteSMVFile(ofile2,sf);
  }

  if (::isltl){
    (*ofile2) << "\n\nLTLSPEC\n";
  }  
  else{
    (*ofile2) << "\n\nSPEC\n";
  }
  (*ofile2) << property << "\n\n";
  ofile2->Close(); 

  // Next start the model checking
  SetStatus("Model checking...");
  char output[6];
  strcpy(output,"XXXXXX");
  (void)mkstemp(output);
  
  string command = "NuSMV " + bufstr + " > " + output;
  system(command.getstr()); // do the actual model checking
  

  // parse the model checker's output
  ::adsmcoutputin=fopen(output,"r");
  ::mctraceindex=0;
  ::statecounter=0;
  ::sourceindex=0;
  ::targetindex=0;
  ::enabledindex=0;
  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);	  
    if (symbolic) ProvideFeedback(ah);
    else ProvideFeedback(ac);
  }

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


void ATDiagram::GeneralCheck() {
        SetStatus("action: general check");
	DoGeneralCheck();
	SetStatus("general check done");
}


void ATDiagram::DoGeneralCheck(){
  GetMainWindow()->SetCursor(MouseCursor::WATCH);

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

  // check that every run leads to a final state
  string constraint="F G ";
  string finalstr = ah->ComputeFinalPredicate();
  constraint += finalstr;

  char buf[100]; // temporary filename for activity graph model
  strcpy(buf,"XXXXXX");
  (void)mkstemp(buf);
  strcat(buf,".tlv");
  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",constraint.getstr()); // put the property in the temp file
  fclose(ftemp);
  string reqstr(req);


  ADSCks *ac;
  ac= new ADSCks(ah);
  ComputeCKS(ah,ac,False);

 
  OutputFile *ofile2= new OutputFile();
  ofile2->Open(&bufstr);
  ac->WriteSMVFile(ofile2,True);
  (*ofile2) << "\n\nLTLSPEC\n";
  (*ofile2) << constraint << "\n\n";
  ofile2->Close();
  // Next start the model checking
  SetStatus("Model checking...");
  char output[6];
  strcpy(output,"XXXXXX");
  (void)mkstemp(output);
  

  string command = "NuSMV " + bufstr + " > " + output;
  system(command.getstr()); // do the actual model checking
  

  // parse the model checker's output
  ::adsmcoutputin=fopen(output,"r");
  ::mctraceindex=0;
  ::statecounter=0;
  ::sourceindex=0;
  ::targetindex=0;
  ::enabledindex=0;
  bool b=adsmcoutputparse();
  
  if (b) {
    error("I couldn't parse the model checker's output\n"); 
    return ;
  }

  unlink(output); // cleanup
  unlink(req); // cleanup
  unlink(buf); // cleanup
  
  string mctxt;
  if (mcfeedback){
    mctxt="Not every run leads to a final state node;see the counter example\n";
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);	  
    ProvideFeedback(ac);
  }


  // Now check for dead nodes and transitions

  string nodead = ah->DeadEdgesNodesConstraints();

  ofile2->Open(&bufstr);
  ac->WriteSMVFile(ofile2,False);	
  (*ofile2) << "\nSPEC\n" << nodead << "\n\n"; 
  ofile2->Close();

  command = "NuSMV ";
  command +=  bufstr + " > " + output;
  system(command.getstr()); // do the actual model checking
  
  // parse the model checker's output
  ::adsmcoutputin=fopen(output,"r");
  ::mctraceindex=0;
  ::statecounter=0;
  ::sourceindex=0;
  ::targetindex=0;
  ::enabledindex=0;
  b=adsmcoutputparse(); 
  if (b) {
    error("I couldn't parse the model checker's output\n"); 
    return ;
  }

  List <Subject *> ahnodes;
  ah->GetNodes(&ahnodes);
  string deadnodes;
  for (ahnodes.first();!ahnodes.done();ahnodes.next()){
    if ((ahnodes.cur()->GetClassType()==Code::NOTE)|| (ahnodes.cur()->GetClassType()==Code::COMMENT)) continue;
    if (ah->GetBound(ahnodes.cur())==0){
      string nodename= *ahnodes.cur()->GetName();
      deadnodes+= "\n" + nodename ;
    }
  }
  
  if ((!mcfeedback) && (!deadnodes.length())) {
    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";
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);
  }
  else{
    if (!deadnodes.length()) // are there dead nodes?
      mctxt="There are some dead transitions: see feedback.\n";
    else
      mctxt="There are some dead nodes and perhaps transitions:\nNode(s)\n\t" +deadnodes +"\n\nis/are dead.\n" + "See also the feedback.\n";
    ShowDialog(MessageDialog::MESSAGE, "Notice", &mctxt);	  
    if (mcfeedback) ProvideFeedback(ac);
    
  }


  unlink(output); // cleanup
  unlink(req); // cleanup 
  unlink(buf); // cleanup 


  GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
  SetStatus("Model checking done");
  return ;
  
}


// the feedback is stored in ::mctrace
void ATDiagram::ProvideFeedback(ADSCks *ac){
  List <Subject *> ls;

  // color all nodes gray
  this->GetGraph()->GetNodes(&ls);
  for (ls.first();!ls.done();ls.next()){
    GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
    if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
	  ((NodeShape *)gs)->UpdateFillColor(new string("gray"));
    }
    ((NodeShape *)gs)->UpdateColor(new string("gray"));
    gs->GetName()->UpdateColor(new string("gray"));
  }

  // color all edges gray
  ls.empty();
  this->GetGraph()->GetEdges(&ls);
  for (ls.first();!ls.done();ls.next()){
    GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
    ((NodeShape *)gs)->UpdateColor(new string("gray"));
    gs->GetName()->UpdateColor(new string("gray"));
  }

  // color initial node red
  ls.empty();
  this->GetGraph()->GetNodes(&ls,Code::ATD_INITIAL_STATE_NODE); // get all the initial nodes (ideally one, but I do not check this here)
  for (ls.first();!ls.done();ls.next()){
    GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
    if (gs->GetClassType()==Code::BLACK_DOT){ // just to be sure...
      ((NodeShape *)gs)->UpdateColor(new string("red"));
    }
  }
  
  List <ADSTransition *> amtransition;
  ac->GetEdges((List <Subject *> *)&amtransition);
  for (amtransition.first();!amtransition.done();amtransition.next()){
    int sourcenum=((ADSValuation *)amtransition.cur()->GetSubject1())->GetNumber(); // get value of c___counter in source state of amtransition.cur()
    bool foundsource=False;
    int i;
    for (i=0;i<(::mctraceindex);i++){
      if (mctrace[i]==sourcenum){ // mctrace[i] is source of transition
	foundsource=True;
	break;
      }
    }
    if (!foundsource) continue; // amtransition.cur() is not part of the trace
    int targetnum=((ADSValuation *)amtransition.cur()->GetSubject2())->GetNumber();
    bool foundtarget=False;
    int j;
    for (j=i+1;j<(::mctraceindex);j++){
      if (mctrace[j]==targetnum){// mctrace[j] is target of transition
	foundtarget=True;
	break;
      }
	  }
    if (!foundtarget) continue;// amtransition.cur() is not part of the trace

    // amtransition.cur() is part of the error trace, so it should be highlighted
    
    Bag <ADSHyperEdge *> step;
    amtransition.cur()->GetStep(step); // the step taken in the current transition (possibly empty)
    List <ADSHyperEdge *> steplist;
    step.GetSet(&steplist);
    for (steplist.first();!steplist.done();steplist.next()){ 
      List <Subject *> simpleedges; 
      steplist.cur()->GetEdges(&simpleedges);
      for (simpleedges.first();!simpleedges.done();simpleedges.next()){
	GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());	       
	gs->UpdateColor(new string("blue"));
	gs->GetName()->UpdateColor(new string("blue"));	      	      
	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.
	if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
	  ((NodeShape *)gs)->UpdateFillColor(new string("red"));
	}
	gs->UpdateColor(new string("red"));	     
	gs->GetName()->UpdateColor(new string("red"));
      }
    }
  }
}

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

// 
void ATDiagram::ProvideFeedback(ADSHyperGraph *ah){
  List <Subject *> ls;
  this->GetGraph()->GetNodes(&ls,Code::ATD_INITIAL_STATE_NODE); // get all the initial nodes (ideally one, but I do not check this here)
  for (ls.first();!ls.done();ls.next()){
    GShape *gs= GetDiagramViewer()->GetShape(ls.cur()); // find the corresponding shape to color it red
    if (gs->GetClassType()==Code::BLACK_DOT){ // just to be sure...
      ((NodeShape *)gs)->UpdateColor(new string("red"));
    }
  }
  
  List <Subject *> nodes;
  this->GetGraph()->GetNodes(&nodes);

  List <Subject *> hedges;
  ah->GetHyperEdges(&hedges);
  for (int j=0;j<(::statecounter-1);j++){ // j counts the current state of the error trace
    int i=0;
    while ((i<(::enabledindex))&&(enabledstatenumber[i]<j)) i++;
    if (enabledstatenumber[i]>j) continue;
    List <ADSHyperEdge *> step;
    for (int k=i;k<(::enabledindex) && enabledstatenumber[k]==j ;k++){
      for (hedges.first();!hedges.done();hedges.next()){
	if ((int)hedges.cur()->GetId()==enabledhyperedge[k]){	  
	  step.add((ADSHyperEdge *)hedges.cur()); // the enabled hyperedges in state j	 
	  break; // hyperedge found, so abort loop
	}
      }
    }  
    int steplen=step.count();
    bool taken[100]; // taken[i] iff step[i] is taken
    for (int sl1=0;sl1<steplen;sl1++){
      List <ADSHyperEdge *> conflict;
      step[sl1]->GetConflict(&conflict);
      if (!conflict.count()) taken[sl1]=True;
      // 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
      taken[sl1]=True;
      for (conflict.first();!conflict.done();conflict.next()){
	if (step.contains(conflict.cur())){

	  int nextstateindex=0;
	  List <Subject *> target; // all the nodes set to one in state j+1
	  nextstateindex=0;
	  while ((nextstateindex<(::targetindex))&&(::targetstatenumber[nextstateindex  ]<=j)) nextstateindex++   ;
	  
	  for (;(nextstateindex<(::targetindex)) && (::targetstatenumber[nextstateindex]==j+1);nextstateindex++){
	    string s=::targetname[nextstateindex];
	    for (nodes.first();!nodes.done();nodes.next()){
	      string nodename= *(nodes.cur()->GetName()); 	       	      
	      if (replace(nodename)==s){ // targetname[i] is a node
		target.add(nodes.cur());
	      }
	    }    
	  }
	  
	  bool FoundHE=False;
	  taken[sl1]=True;
	  List <Subject *> *target1=step[sl1]->GetSubject2();
	  List <Subject *> *target2=conflict.cur()->GetSubject2();
	  for (target1->first();!target1->done();target1->next()){
	    if ((!target2->contains(target1->cur())) &&(target.contains(target1->cur()))){ // target1->cur() uniquely identifies step[sl1]; step[sl1] is taken
	      taken[sl1]=True;
	      FoundHE=True; 	      
	    }
	  }

	  for (target2->first();!target2->done();target2->next()){
	    if ((!target1->contains(target2->cur())) && (target.contains(target2->cur()))){ // conflict.cur() is taken
	      if (FoundHE){ 
		error("Two conflicting edges seem to be taken....\n");
	      } 
	      taken[sl1]=False; 	      
	    }
	  }
	}
      }				  
    } // end of steplent     
    bool showingstep=False;
    for (int sl1=0;sl1<steplen;sl1++){
      showingstep=showingstep || taken[sl1];
      if (taken[sl1]) {	
	List <Subject *> simpleedges; 
	step[sl1]->GetEdges(&simpleedges);
	for (simpleedges.first();!simpleedges.done();simpleedges.next()){
	  GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());	       
	  gs->UpdateColor(new string("blue"));	      	      
	  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.
	  if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
	    ((NodeShape *)gs)->UpdateFillColor(new string("red"));
	  }
	  gs->UpdateColor(new string("red"));	     
	}
      }
    }
    if ((!showingstep) && (steplen)){
      error ("I could not show a step!\n");
    }
  }
}






bool ATDiagram::ComputeHyperGraph(ADSHyperGraph *ah){
  bool b;
  Elim el; // functional class that maps graph into hypergraph
  //  if (am) delete am; // commented since otherwise a segmentation fault occurs
  SetStatus("computing hypergraph");
  Graph *g=(ATGraph *)this->GetGraph();
  b=el.EliminatePseudoStateNodes(g,ah); // the actual elimination
  ah->Initialise(); // compute conflicts between activities
  SetStatus("hypergraph file computed");
  return b;
}

void ATDiagram::ComputeCKS(ADSHyperGraph *ah, ADSCks *ac, bool reduction){
  ADSSem adssem; // functional class that maps hypergraph to kripke structure
  // if (cl) delete cl;
  if (!ah) return;
  adssem.ComputeCKS(ah,ac,reduction); // the actual semantics
}
  

// the following procedure does not work yet
//void ATDiagram::ComputeImpCKS(ADSHyperGraph *ah, ADSCks *ac){
//  ADSSem adssem; // functional class that maps hypergraph to kripke structure
//  // if (cl) delete cl;
//  if (!ah) return;
//  //  adssem.ComputeImpCKS(ah,ac); // the actual semantics
//}
  


// make nodes and edges black
void ATDiagram::ClearTrace() {  
  List <Subject *> nodes; 
  this->GetGraph()->GetNodes(&nodes,Code::ATD_INITIAL_STATE_NODE);
  for (nodes.first();!nodes.done();nodes.next()){
      GShape *gs= GetDiagramViewer()->GetShape(nodes.cur()); 
      ((NodeShape *)gs)->UpdateColor(new string("black"));
  }
  List <Subject *> simpleedges; 
  this->GetGraph()->GetEdges(&simpleedges);
  for (simpleedges.first();!simpleedges.done();simpleedges.next()){
    GShape *gs= GetDiagramViewer()->GetShape(simpleedges.cur());	       
    gs->UpdateColor(new string("black"));
    gs->GetName()->UpdateColor(new string("black"));	      	      
    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.
    if ((gs->GetClassType()==Code::SOLID_HORIZONTAL_BAR) || (gs->GetClassType()==Code::SOLID_VERTICAL_BAR)) {
      ((NodeShape *)gs)->UpdateFillColor(new string("black"));
    }
    gs->UpdateColor(new string("black"));	     
    gs->GetName()->UpdateColor(new string("black"));
  }
}