adshypergraph.c

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

	(*ofile) << " | " << amedges.cur()->GetUniqueName()<<"-taken"  << "\n";
      List <Subject *> *target=amedges.cur()->GetSubject2();
      if (target->contains(amnodes.cur())) 
	(*ofile) << " | " << amedges.cur()->GetUniqueName()<<"-taken"  << "\n";    
    }
    (*ofile) << "\n";
  }
  // EVENT GENERATION
  (*ofile) << "\n-- external event generation\n";
  (*ofile) <<  "ASSIGN\n";
  for (propl.first();!propl.done();propl.next()){
    if (propl.cur()->GetType()==EVENT){ // external event
      string s=propl.cur()->GetName();
      (*ofile ) << "\tnext(" << replace(s) << ") :=\n\t\tcase\n\t\t\tstable:{FALSE,TRUE};\n\t\t\t\tTRUE:FALSE;\n\t\tesac;\n"; 
    }
    if (propl.cur()->GetType()==SENDEVENT){// internal event
      string s=propl.cur()->GetName();
      (*ofile ) << "\tnext(" << replace(s) << ") :=\n";
      bool FirstSendEvent=True;
      for (amedges.first();!amedges.done();amedges.next()){
	if ((amedges.cur()->GetSendEvent())&&(*(amedges.cur()->GetSendEvent())==*propl.cur())){
	  (*ofile) << "\t\t";
	  if (FirstSendEvent) {FirstSendEvent=False;(*ofile) << "   ";}
	  else (*ofile) << " | ";
	  (*ofile) << amedges.cur()->GetUniqueName()<<"-taken" <<"\n";
	}
      }
      (*ofile) <<"\t\t;\n";
    }  
  }
  (*ofile) << "\n-- termination event generation\n";
  // termination events
  for (amnodes.first();!amnodes.done();amnodes.next()){    
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      string s=*(amnodes.cur()->GetName());
      (*ofile ) << "\tnext(T_" << replace(s) << ") :=\n\t\tcase\n\t\t\t(stable & " << replace(s) <<  "):{FALSE,TRUE};\n\t\t\tTRUE:FALSE;\n\t\tesac;\n";     
    }
  }

  (*ofile) << "\n-- property update\n";
  for (propl.first();!propl.done();propl.next()){
    if ((propl.cur()->isInternal()&&(propl.cur()->GetType()!=SENDEVENT))){ // property is updated internally
      (*ofile) << "TRANS\n\t("<<replace(propl.cur()->GetName()) << "=next(" << replace(propl.cur()->GetName()) << "))" ;
      for (amnodes.first();!amnodes.done();amnodes.next()){
	if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
	  string s=*(amnodes.cur()->GetName());
	  //	  ADSActivity *a=FindAct(s);
	  ADSActivity *a=((ATDActionStateNode *)amnodes.cur())->GetActivity();
	  if (a->isUpdated(propl.cur()->GetVar()))
	    (*ofile) << " | next(T_" << replace(s) << ")\n"; // update on variable
	}
      }
    }
  }


  if (sf){
    // COMPASSION CONSTRAINTS
    for (amedges.first();!amedges.done();amedges.next()){
      if (amedges.cur()->GetInternal()) continue;
      if (amedges.cur()->hasClockConstraint()) continue;
      (*ofile) << "\nCOMPASSION\n"; 
      (*ofile) << "(" << amedges.cur()->GetUniqueName() << "-relevant, " << amedges.cur()->GetUniqueName() << "-taken)\n";
    }
    (*ofile) << "\n\n";
  }


  List <Subject *> finalnodes;

  // INTERFERENCE
  (*ofile) << "\n-- interference\n";
  int amlen=amnodes.count();
  for (int i=0;i<amlen;i++){    
    for (int j=i+1;j<amlen;j++){
      if ((amnodes[i]->GetClassType()==Code::ATD_ACTION_STATE_NODE)&&
	  (amnodes[j]->GetClassType()==Code::ATD_ACTION_STATE_NODE)&&
	  (GetInterference((ATDActionStateNode*)amnodes[i],(ATDActionStateNode*)amnodes[j]))){
	(*ofile) << "TRANS\n\t!(";
	string s1 = *(amnodes[i]->GetName());
	string s2 = *(amnodes[j]->GetName());
	(*ofile) << "next(" << replace(s1) << ") & next(" << replace(s2) << "))\n";
      }
    }
    if (amnodes[i]->GetClassType()==Code::ATD_FINAL_STATE_NODE){
      finalnodes.add(amnodes[i]);
    }
  }

  // final nodes
  if (finalnodes.count()){
//  bool FirstFinal=True;
    (*ofile) << "\n -- events cannot be generated if the configuration is final\n";
    (*ofile) << "INVAR\n";
    (*ofile) << "\t" << ComputeFinalPredicate() << "\t\t-> stable\n\n";

  }


  // ENABLEDNESS
  (*ofile) << "\n-- enabledness\n";
  (*ofile) << "DEFINE\n\tstable := !enabled & !events;\n";
  (*ofile) << "DEFINE\n\tenabled := \n";
  bool FirstEnabled=True; 
  for (amedges.first();!amedges.done();amedges.next()){
    (*ofile) << "\t\t";
    if (FirstEnabled){
      FirstEnabled=False; (*ofile) << "   ";
    }
    else (*ofile) << " | ";
    (*ofile) << amedges.cur()->GetUniqueName()<<"-enabled" << "\n"; 
  }
  (*ofile) << "\t\t;\n\n";

  (*ofile) << "DEFINE\n\tevents := FALSE \n";
  for (propl.first();!propl.done();propl.next()){
    if ((propl.cur()->GetType()==EVENT)||(propl.cur()->GetType()==SENDEVENT)){ // external or internal event
      (*ofile) << " | ";
      string s=propl.cur()->GetName();
      (*ofile ) << "\t\t" << replace(s) <<"\n"; 
    }
  }
  for (int i=0;i<amlen;i++){    
    if (amnodes[i]->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      (*ofile) << " | ";
      string s = *(amnodes[i]->GetName());
      (*ofile) << "\t\tT_"<< replace(s) << "\n";
    }
  }
  (*ofile) << "\t\t ;\n\n";

  // 
  (*ofile) << "-- disable concurrent enabling of two hyperedges where the source and target of one are contained in the source and target of other\n";
  int elen=amedges.count();  
  for (int i=0;i<elen-1;i++){
    for (int j=i+1;j<elen;j++){
	// check if sources and targets of amedges[i] are contained in those of conflict.cur()
      //      List <Subject *> *source=amedges[i]->GetSubject1();
      bool FoundConflict=(amedges[i]->conflicts(amedges[j]));
      if (!FoundConflict){
	List <Subject *> *target=amedges[i]->GetSubject2();
	bool FoundTargets=True;
	for (target->first();!target->done();target->next()){
	  if (!amedges[j]->GetSubject2()->contains(target->cur())){
	    FoundTargets=False;
	    break;
	  }
	}
	if (FoundTargets){ // amedges[i] is contained in amedges[j]
	  (*ofile) << "TRANS\n\tnext(" << amedges[i]->GetUniqueName() << "-enabled) -> ! next(" <<  amedges[j]->GetUniqueName() << "-enabled)\n";
	}
      }
       	       
      if (!FoundConflict){	
	List <Subject *> *target=amedges[j]->GetSubject2();
	bool FoundTargets=True;
	for (target->first();!target->done();target->next()){
	  if (!amedges[i]->GetSubject2()->contains(target->cur())){
	    FoundTargets=False;
	    break;
	  }
	}
	if (FoundTargets){ // amedges[j] is contained in amedges[i]
	  (*ofile) << "TRANS\n\tnext(" <<  amedges[j]->GetUniqueName() << "-enabled) -> ! next(" << amedges[i]->GetUniqueName() << "-enabled)\n";
	}
      }
    }
  }
  (*ofile) << "\n";
}






void ADSHyperGraph::RemoveNodes(List <Node *> nodeused, List <ADSVar *> varused, bool reduction){
  List <Subject *> amhedges;
  List <Subject *> remove;
  GetHyperEdges(&amhedges);
  int hedgecount=amhedges.count();
  bool hedgeremove[200];
  for (int i=0;i<hedgecount;i++){
    hedgeremove[i]=False;
    if (isRemovableHyperEdge((ADSHyperEdge *)amhedges[i],nodeused,varused,reduction)){    
      remove.add(amhedges[i]);
      hedgeremove[i]=True;
    }    
  }

  for (remove.first();!remove.done();remove.next()){    
    // remove.cur() has only one source, due to the reduction rules
    Subject *node=((HyperEdge *)remove.cur())->GetSubject1()->cur();
    List <Subject *> newhedges;
    GetHyperEdges(&newhedges);
    for (newhedges.first();!newhedges.done();newhedges.next()){
      List <Subject *> *target=((HyperEdge *)newhedges.cur())->GetSubject2();
      if (!target) continue;
      if (!target->contains(node)) continue;
      // hyperedge newhedges.cur() makes remove.cur() relevant
      target->remove(node);
      List <Subject *> *newtarget=((HyperEdge *)remove.cur())->GetSubject2();
      for (newtarget->first();!newtarget->done();newtarget->next()){
	target->add(newtarget->cur());
      }
      // get the simple edges from remove.cur () and put them in newhedges.cur()
      // this is necessary for displaying the feedback of the model checker
      List <Subject *> ls;
      ((ADSHyperEdge *)remove.cur())->GetEdges(&ls); // the edges in the original activity diagram that are represented by the hyperedge
      ((ADSHyperEdge *)newhedges.cur())->AddEdges(ls);
      
    }
    
    RemoveNode((Node *)node); // hyperedge remove.cur() is removed automatically
  }
}




bool ADSHyperGraph::isRemovableHyperEdge(ADSHyperEdge *hedge, List <Node *> nodeused, List <ADSVar *> varused, bool reduction){

  if (hedge->isconflicting()) return False;

  List <Subject *> *source=hedge->GetSubject1();
  List <Subject *> *target=hedge->GetSubject2();
  
  if (source->count()>1) return False;
  source->first();
  // hedge is non conflicting hyperedge with one source
  if (!((source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE)||(source->cur()->GetClassType()==Code::ATD_WAIT_STATE_NODE))) return False;
 
  // rule1
  if (nodeused.contains((Node*)source->cur())) return False;
  bool found=False;
  for (target->first();!target->done();target->next()){
    if (nodeused.contains((Node*)target->cur())){
      found = True;
      break;
    }
  }
  if (found) return False;
  for (varused.first();!varused.done();varused.next()){
    if (hedge->refersto(varused.cur())){
      found=True;
      break;
    }
  }
  if (found)return False;

  // rule 2
  if   (NodeReferredToBySomeInpredicate(source->cur())) return False;
  for (target->first();!target->done();target->next()){
    if (NodeReferredToBySomeInpredicate(target->cur())){
      found=True;
      break;
    }
  }
  if (found) return False;

  // rule 3
  if (hedge->GetClockConstraint()) return False;

  // rule 4
  if ((source->cur()->GetClassType()==Code::ATD_WAIT_STATE_NODE) && !reduction) return False;

 // all rules checked, so both source->cur() and hedges.cur() can be removed
  return True;
}


bool ADSHyperGraph::NodeReferredToBySomeInpredicate(Subject *n){
  for (hedges->first();!hedges->done();hedges->next()){
    if (((ADSHyperEdge*)hedges->cur())->inpredicaterefersto(n)) return True;
  }
  return False;
}


// used is list of variables used in property	
void ADSHyperGraph::RemoveLocalVariables(List <ADSVar *> *usedinprop){
  for (varl.first();!varl.done();varl.next()){
    // rule 2
    if (usedinprop->contains(varl.cur())) continue; // varl.cur() is used in property so skip


    // rule 1
    if (VarUpdatedByTwoActivities(varl.cur())) continue;

    // rule 3
    if (VarTestedInHyperEdgeWithoutUpdate(varl.cur())) continue;

    // rule 4 checked elsewhere (eliminate pseudo nodes)

    // varl.cur() can be removed

    // remove varl.cur() from update in activity
    for(actlist.first();!actlist.done();actlist.next()){
      actlist.cur()->RemoveUpdate(varl.cur());      
    }
    for(propl.first();!propl.done();){
      if (propl.cur()->GetVar()==varl.cur()){
	extproplist.remove(propl.cur());
	intproplist.remove(propl.cur());  
	propl.removecur();
      }    
      else propl.next();
    }
    // NOTE varl.cur() is still in hyperedge's varlist
    // so printing the hypergraph gives inaccurate information
  }
}


// return True iff 
// ( there is a hyperedge h such that
// v is tested in h's guard h AND 
// none of h's sources update v )
bool ADSHyperGraph::VarTestedInHyperEdgeWithoutUpdate(ADSVar *v){
  List <Subject *> edges;
  GetHyperEdges(&edges);
  for (edges.first();!edges.done();edges.next()){
    if (!((ADSHyperEdge*)edges.cur())->refersto(v)) continue;
    // the guard of edges.cur() refers to v
    List <Subject *> *source=((HyperEdge *)edges.cur())->GetSubject1();
    bool found=False;
    for (source->first();!source->done();source->next()){
      if (source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
	if (((ATDActionStateNode *)source->cur())->GetActivity()->isUpdated(v)){
	  // v is updated by one of the sources
	  found=True;
	}
      }
    }
    if (!found){  // v is not updated by any of edges.cur()'s sources
      return True;
    }
  }
  return False;
}


// return True iff 
// ( v is updated by two activities )
bool ADSHyperGraph::VarUpdatedByTwoActivities(ADSVar *v){
  int actcount=actlist.count();
  for (int i=0;i<actcount;i++){
    for (int j=i+1;j<actcount;j++){
      if ((GetInterference(actlist[i],actlist[j])) &&(actlist[i]->isUpdated(v))&&(actlist[j]->isUpdated(v))){
	actlist[i]->Write();
	actlist[j]->Write();
	List <Subject *> nods;
	ATDActionStateNode *activity_i = NULL;	//init?
	ATDActionStateNode *activity_j = NULL;	//init?
	GetNodes(&nods, Code::ATD_ACTION_STATE_NODE);
	for (nods.first();!nods.done();nods.next()){
	  if (((ATDActionStateNode*)nods.cur())->GetActivity()==actlist[i]){
	    activity_i=(ATDActionStateNode *)nods.cur();
	  }
	  if (((ATDActionStateNode*)nods.cur())->GetActivity()==actlist[j]){
	    activity_j=(ATDActionStateNode *)nods.cur();
	  }	    
	}
	ADSSem test;
	if (test.inparallel(this,(Subject *)activity_i,(Subject*)activity_j)){
	  return True;
	}
      }
    }
  }
  return False;  
}