adshypergraph.c

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

    // the same hyperedges cannot be in conflict since otherwise they would not have enabled simultaneously
    List <Subject *> *source_i=hyperedges[i]->GetSubject1();
    for (int j=i+1;j<hedgescount;j++){      
      List <Subject *> *source_j=hyperedges[j]->GetSubject1();
      for (source_j->first();!source_j->done();source_j->next()){
	if (source_i->find(source_j->cur())>-1){ // hyperedges[i] and hyperedges[j] have overlapping sources
	  hyperedges[i]->AddConflict(hyperedges[j]);
	  hyperedges[j]->AddConflict(hyperedges[i]);
	  break; // jump out of for-loop
	}
      }
    }
  }
}

void ADSHyperGraph::SetInitialFinalNames(){
  List <Subject *> ahnodes;
  GetNodes(&ahnodes);
  for (ahnodes.first();!ahnodes.done();ahnodes.next()){
    string s=(*(ahnodes.cur()->GetName()));
    if (ahnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
      s="I___INITIAL";ahnodes.cur()->SetName(&s);
    }
    if (ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
      string t = (int)ahnodes.cur()->GetId();
      s="F___FINAL"+t; ahnodes.cur()->SetName(&s);
    }
  }
}    
 
void ADSHyperGraph::UnSetInitialFinalNames(){
  List <Subject *> ahnodes;
  GetNodes(&ahnodes);
  for (ahnodes.first();!ahnodes.done();ahnodes.next()){
    if ((ahnodes.cur()->GetClassType()!=Code::ATD_INITIAL_STATE_NODE)||(ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE)) continue; // skip these
    if (ahnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
      string s=""; ahnodes.cur()->SetName(&s);
    }
    if (ahnodes.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
      string s=""; ahnodes.cur()->SetName(&s);
    }
  }
}    
 

void PrintBag(Bag <ADSHyperEdge *> *b){
  List <ADSHyperEdge *> l;
  b->GetList(l);
  for (l.first();!l.done();l.next()){
    std::cout << l.cur()->GetId() <<":\t" << b->count(l.cur()) <<"\n";
  }
}

bool ADSHyperGraph::isConflicting(Bag <ADSHyperEdge *> *step, ADSHyperEdge *he){
  List <ADSHyperEdge *> al; // the list of hyperedges in conflict with he
  he->GetConflict(&al); 
  for (al.first();!al.done();al.next()){
    if (step->count(al.cur())) return True;
  }
  return False;
}

 
 
string ADSHyperGraph::DeadEdgesNodesConstraints(){
  string constraint;
  List <ADSHyperEdge *> hyperedges;
  GetHyperEdges((List <Subject *> *)&hyperedges);
  int hedgescount = hyperedges.count();
  for (int i=0;i<hedgescount;i++){
    if (i)
      constraint += " & ";
 
    List <Subject *> *source_i=hyperedges[i]->GetSubject1();
    bool First=True;
    string sourceconstraint;
    for (source_i->first();!source_i->done();source_i->next()){
      if (!First)
        sourceconstraint+=" & ";
      else
        First=False;
      string s=(*(source_i->cur()->GetName()));
      sourceconstraint += replace(s) + " > 0 " ;
    }
 
    List <Subject *> *target_i=hyperedges[i]->GetSubject2();
    First=True;
    string targetconstraint;
    for (target_i->first();!target_i->done();target_i->next()){
      if (!First)
        targetconstraint+=" & ";
      else
        First=False;
      string s=(*(target_i->cur()->GetName()));
      targetconstraint += replace(s) + " > 0 ";
    }
    constraint += "( EF (" + sourceconstraint + " & (EX (" + targetconstraint +
"))))";
  }
 
  return constraint;
}





string ADSHyperGraph::ComputeFinalPredicate(){
  string final="( (";
  List <Subject *> ls;
  GetNodes(&ls); // get all the nodes
  bool First=True;
  for (ls.first();!ls.done();ls.next()){
    if ((ls.cur()->GetClassType()==Code::NOTE)||(ls.cur()->GetClassType()==Code::COMMENT)||(ls.cur()->GetClassType()==Code::ATD_DECISION_STATE_NODE)||(ls.cur()->GetClassType()==Code::ATD_SYNCHRONIZATION_NODE)||(ls.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE)) continue; // skip these
    if (!First){
      final += " & ";
    }
    else{
      First=False;
    }
    if (ls.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE){
      final+="I___INITIAL=0";
    }
    else{ // action or wait state node
      string stemp=(*(ls.cur()->GetName()));
      stemp.replace("-\r","");
      stemp.replace('\r','_');
      stemp.replace(' ','_');
      stemp.replace('/','_');
      stemp.replace('.','_');
      stemp.replace('-','_');
      stemp += "=0";
      final+=stemp;
    }
  }  
  final += ") & ( 0 ";


  // First=True;
  string finalexpr;
  for (ls.first();!ls.done();ls.next()){
    if (ls.cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
      finalexpr += " | ";
      finalexpr+="F___FINAL";
      string index = (int)ls.cur()->GetId();
      finalexpr = finalexpr + index + ">0";
    }
  }  

  final += finalexpr;
  final += ") )";
  return final;
}


void ADSHyperGraph::GetFinalNodes(List <Subject *> *final){
  for (nodes->first();!nodes->done();nodes->next()){
    if (nodes->cur()->GetClassType()==Code::ATD_FINAL_STATE_NODE){
      final->add(nodes->cur());
    }
  }  
}



// Note: only works for safe activity graphs
void ADSHyperGraph::WriteNuSMV(OutputFile *ofile, bool sf){ 
  (*ofile) <<  "MODULE main\n\nVAR\n";
  List <Subject *> amnodes;
  GetNodes(&amnodes);
  List <ADSHyperEdge *> amedges;
  GetHyperEdges((List<Subject *> *)&amedges);

  List <Subject *> writtennodes; // nodes written as var so far
  List <Subject *> writtenedges; // edges written as var so far
  List <Prop *> writtenprop; // edges written as var so far
  for (amnodes.first();!amnodes.done();amnodes.next()){    
    if (amnodes.cur()->GetClassType()!=Code::ATD_INITIAL_STATE_NODE) continue; // skip these nodes
    string s=(*(amnodes.cur()->GetName()));
    writtennodes.add(amnodes.cur());
    (*ofile ) << "\t"<< replace(s) << " : boolean;\n";
  }

  while(writtennodes.count()<amnodes.count())  {
    List <ADSHyperEdge *> newenabled;
    GetHyperEdgesFrom((List <HyperEdge *> *)&newenabled,&writtennodes);
    for (newenabled.first();!newenabled.done();newenabled.next()){
      if (!writtenedges.contains(newenabled.cur())){
	writtenedges.add(newenabled.cur());
	List <Prop *> pl;
	newenabled.cur()->GetPropList(pl);
	for (pl.first();!pl.done();pl.next()){
	  if (!((pl.cur()->GetType()==PROP)||(pl.cur()->GetType()==PROP)||(pl.cur()->GetType()==EVENT))) continue; // only events and stuff
	  if (!writtenprop.contains(pl.cur())){
	    writtenprop.add(pl.cur());
	    (*ofile) << "\t" << replace(pl.cur()->GetName()) <<  " : boolean;\n";
	  }
	}

	if (newenabled.cur()->hasClockConstraint()){
	  string name=newenabled.cur()->GetUniqueName();
	  (*ofile) <<  "\t" << name << "-timer:0.." << ((GetNrTimeouts() + 1 )  * (newenabled.cur()->GetClockConstraint()->GetLimit())) << ";\n";
	}
	

	if ((newenabled.cur()->GetSendEvent()) && (!writtenprop.contains(newenabled.cur()->GetSendEvent()))){
	  writtenprop.add(newenabled.cur()->GetSendEvent());
	  (*ofile) << "\t" << replace(newenabled.cur()->GetSendEvent()->GetName()) << " : boolean;\n";
	}
      }

      List <Subject *> *target=newenabled.cur()->GetSubject2();
      for (target->first();!target->done();target->next()){
	if (writtennodes.contains(target->cur())) continue;
	string s=(*(target->cur()->GetName()));
	writtennodes.add(target->cur());
	(*ofile ) << "\t"<< replace(s) << " : boolean;\n";
	if (target->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
	  (*ofile ) << "\tT_" << replace(s) << " : boolean;\n";
	  for (actlist.first();!actlist.done();actlist.next()){
	    if (replace(actlist.cur()->GetName())==replace(s)){
	      List <ADSVar *> varlist;
	      actlist.cur()->GetUpdateList(varlist);
	      for (intproplist.first();!intproplist.done();intproplist.next()){
		if (writtenprop.contains(intproplist.cur())) continue;
		if (((intproplist.cur()->GetType()==INTERNAL_PROP)||(intproplist.cur()->GetType()==INTERNAL_STRING))&&(varlist.contains(intproplist.cur()->GetVar()))){	  
		  (*ofile) << "\t" << replace(intproplist.cur()->GetName()) << ": boolean;\n";
		  writtenprop.add(intproplist.cur());
		}
	      }
	    }
	  }
	}
      }
    }
  }


  (*ofile) << "\nINIT  -- state nodes\n";
  bool FirstInit=True;
  //  (*ofile) << "\tc____counter = 0 & \n "; // because of assign number
  for (amnodes.first();!amnodes.done();amnodes.next()){    
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
    if (FirstInit) FirstInit=False;
    else (*ofile) << " &\n";
    string s=(*(amnodes.cur()->GetName()));
    if ((amnodes.cur()->GetClassType()==Code::ATD_INITIAL_STATE_NODE)){
      (*ofile) << "\t" << replace(s) << "\t = TRUE";
    }
    else{
      (*ofile) << "\t" << replace(s) << "\t = FALSE" ;
    }
    if (amnodes.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      (*ofile ) << " &\n\tT_" << replace(s) << "\t = FALSE" ;
    }
  }
  FirstInit=True;
  for (propl.first();!propl.done();propl.next()){
    if (FirstInit){
      FirstInit=False;
      (*ofile) << "\n\nINIT -- events etc.\n";
    }
    else (*ofile) << " &\n";
    string s=propl.cur()->GetName();
    (*ofile ) << "\t" << replace(s) << "\t = FALSE";    
  }
  (*ofile) << "\n\n";


  FirstInit=True;
  for (amedges.first();!amedges.done();amedges.next()){
    if (amedges.cur()->hasClockConstraint()){
      if (FirstInit){
	FirstInit=False;
	(*ofile) << "\n\nINIT -- timers \n";
      }
      else (*ofile) << " &\n";
      string name=amedges.cur()->GetUniqueName();
      (*ofile) << "\t" << name << "-timer = 0\n";
    }
  }

  for (amedges.first();!amedges.done();amedges.next()){
    (*ofile) << "DEFINE -- hyperedges \n\n";  
    string name=amedges.cur()->GetUniqueName();
    (*ofile) << "\t" << name+"-relevant := ";
    List <Subject *> *source=amedges.cur()->GetSubject1();
    bool First=True;
    for (source->first();!source->done();source->next()){
      if (First) First=False;
      else (*ofile) << " & ";
      string sourcename=*(source->cur()->GetName());
      (*ofile) << replace(sourcename) ;
    }
    (*ofile) << ";\n\t" << name+"-enabled := " << name << "-relevant ";
    if (!amedges.cur()->HasEmptyEvent()){
      (*ofile) << " & " << replace(amedges.cur()->GetEvent()) ;
    }
    for (source->first();!source->done();source->next()){
      if (source->cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
	string sourcename=*(source->cur()->GetName());
	(*ofile) << " & T_" << replace(sourcename)  ;
      }
    }
    if (!amedges.cur()->HasEmptyGuard()){
      string guard=amedges.cur()->GetGuard();
      guard.replace('[','(');
      guard.replace(']',')');
      guard.replace('~','!');
      guard.replace("IN","");
      (*ofile) << " & " << replace(guard) ;
    }
    if (amedges.cur()->hasClockConstraint()){       
      (*ofile) << " & " << name << "-timer = " << (1+GetNrTimeouts()) * (amedges.cur()->GetClockConstraint()->GetLimit()) ;
    }
    (*ofile) << ";\n"; 


    ///
    List <Subject *> *target=amedges.cur()->GetSubject2();
    (*ofile) << "\t" << name+"-taken := " << name+"-enabled ";
    for (source->first();!source->done();source->next()){
      if (!target->contains(source->cur())){
	(*ofile) << " & ";
	string sourcename=*(source->cur()->GetName());
	(*ofile) << "(next(" + replace(sourcename) + ")=FALSE)" ;
      }
    }    

    for (target->first();!target->done();target->next()){
      (*ofile) << " & ";
      string targetname=*(target->cur()->GetName());
      (*ofile) << "next("+replace(targetname)+")";      
      //}
    }  
    (*ofile) << ";\n";

    ///
    (*ofile) << "\nTRANS\n";
    (*ofile) << "\t" << "(!"+name+"-enabled)";
    List <ADSHyperEdge *> conflict;
    amedges.cur()->GetConflict(&conflict);
    (*ofile) << "| ((!" << name << "-taken) <-> ( FALSE";
    for (conflict.first();!conflict.done();conflict.next()){
      (*ofile) << " | ";
      (*ofile) << replace(conflict.cur()->GetUniqueName())<<"-taken";	
    }
    (*ofile) << " ))\n\n";    
    (*ofile) << "\n";
    
    ///
    (*ofile) << "\nDEFINE -- timers\n\n";
    if (amedges.cur()->hasClockConstraint()){
      (*ofile) << "\t" << name << "-timer_on := (!" << name << "-relevant) & next(" <<  name << "-relevant);\n";
      
      
      (*ofile) << "TRANS\n";
      (*ofile) << "\t!next(" << name << "-relevant) -> next(" <<  name << "-timer)=0\n";

      (*ofile) << "TRANS\n";     
      (*ofile) << "\t(" << name << "-timer_on ) -> next(" << name << "-timer) = 0\n";
      (*ofile) << "TRANS\n";
      (*ofile) << "\t( stable & " << name << "-relevant & " ;  
      (*ofile)<< "next(" << name << "-relevant)) -> (next(" <<  name << "-timer) = " << name << "-timer + 1)\n";
      (*ofile) << "TRANS\n";
      (*ofile) << "\t(!stable & " << name << "-relevant & next(" << name << "-relevant)) -> (next(" <<  name << "-timer) = " << name << "-timer )\n\n";
    }
  }

  for (amnodes.first();!amnodes.done();amnodes.next()){    
    if ((amnodes.cur()->GetClassType()==Code::NOTE)||(amnodes.cur()->GetClassType()==Code::COMMENT)) continue; // skip these 
    string s = *(amnodes.cur()->GetName());
    (*ofile) << "TRANS\n\t(" << replace(s)  << " = next(" << replace(s) << "))";
    for (amedges.first();!amedges.done();amedges.next()){
      List <Subject *> *source=amedges.cur()->GetSubject1();
      if (source->contains(amnodes.cur()))