[Avida-SVN] r2216 - branches/uml/source/main

[hjg at myxo.css.msu.edu]

Author: hjg
Date: 2007-11-30 15:39:12 -0500 (Fri, 30 Nov 2007)
New Revision: 2216

Modified:
   branches/uml/source/main/cMDEAbsenceProperty.cc
   branches/uml/source/main/cMDEAbsenceProperty.h
   branches/uml/source/main/cMDEExistenceProperty.cc
   branches/uml/source/main/cMDEExistenceProperty.h
   branches/uml/source/main/cMDEProperty.h
   branches/uml/source/main/cMDEUniversalProperty.cc
   branches/uml/source/main/cMDEUniversalProperty.h
   branches/uml/source/main/cUMLModel.cc
Log:


Modified: branches/uml/source/main/cMDEAbsenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.cc	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEAbsenceProperty.cc	2007-11-30 20:39:12 UTC (rev 2216)
@@ -39,6 +39,7 @@
 	outfile.open (file_name.c_str());
 	assert(outfile.is_open());
 	
+	outfile << "/* Absence property " << _expr_p << "*/" << std::endl;
 	outfile << "#define p (" << _expr_p << ")" << std::endl;
 	outfile << "never { /* !([](!p)) */" << std::endl;
 	outfile << "T0_init :    /* init */" << std::endl;
@@ -64,6 +65,9 @@
 	// print the property
 	print();
 	verify_reward = verify();
+	std::string cmd;
+	std::string work_prop = "properties_that_passed";
+
 	
 		// if this property passed, then save it to a file
 	if (verify_reward) { 

Modified: branches/uml/source/main/cMDEAbsenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.h	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEAbsenceProperty.h	2007-11-30 20:39:12 UTC (rev 2216)
@@ -27,7 +27,11 @@
 	void print(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
 	void printWitness(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
 	void evaluate();
+	std::string getPropertyType() { return "Absence"; } 
+	std::string getPropertyParameters() { return _expr_p; }
 
+
+
 private:
 	std::string _expr_p;
 };

Modified: branches/uml/source/main/cMDEExistenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.cc	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEExistenceProperty.cc	2007-11-30 20:39:12 UTC (rev 2216)
@@ -15,6 +15,7 @@
 	outfile.open (_name.c_str());
 	assert(outfile.is_open());
 	
+	outfile << "/* Existence property " << _expr_p << "*/" << std::endl;
 	outfile << "#define p (" << _expr_p << ")" << std::endl;
 	outfile << "never { /* !(<>(p)) */ " << std::endl;
 	outfile << "accept_init :    /* init */" << std::endl;

Modified: branches/uml/source/main/cMDEExistenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.h	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEExistenceProperty.h	2007-11-30 20:39:12 UTC (rev 2216)
@@ -28,7 +28,11 @@
 
 	void print(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
 	void printWitness(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
+	std::string getPropertyType() { return "Existence"; } 
+	std::string getPropertyParameters() { return _expr_p; }
 
+
+
 private:
 	std::string _expr_p;
 };

Modified: branches/uml/source/main/cMDEProperty.h
===================================================================
--- branches/uml/source/main/cMDEProperty.h	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEProperty.h	2007-11-30 20:39:12 UTC (rev 2216)
@@ -19,6 +19,8 @@
 	// A function that prints the property to a file.
 	virtual void print() = 0;
 	virtual void printWitness() = 0;
+	virtual std::string getPropertyType() = 0;
+	virtual std::string getPropertyParameters() { return ""; } 
 	
 	
 	// A function that checks to see if there is a witness trace for the property
@@ -39,9 +41,15 @@
 };
 
 struct ltcMDEProperty{ 
-	bool operator() (const cMDEProperty* p1, const cMDEProperty* p2) const
+	bool operator() (cMDEProperty* p1, cMDEProperty* p2) const
 	{
-		return (p1 < p2);
+	std::string name1, name2;
+	
+	name1 = p1->getPropertyType() + p1->getPropertyParameters();
+	name2 = p2->getPropertyType() + p2->getPropertyParameters(); 
+	// 1st less than 2nd & 2nd never equal to the first. 
+	
+		return (name1 < name2);
 	}
 };
 

Modified: branches/uml/source/main/cMDEUniversalProperty.cc
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.cc	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEUniversalProperty.cc	2007-11-30 20:39:12 UTC (rev 2216)
@@ -15,6 +15,7 @@
 	outfile.open (_name.c_str());
 	assert(outfile.is_open());
 	
+	outfile << "/* Universal property " << _expr_p << "*/" << std::endl;
 	outfile << "#define p (" << _expr_p << ")" << std::endl;
 	outfile << "never { /* ![]p */" << std::endl;
 	outfile << "T0_init :    /* init */" << std::endl;
@@ -60,6 +61,8 @@
 	// print the property
 	print();
 	verify_reward = verify();
+	std::string cmd;
+	std::string work_prop = "properties_that_passed";
 	
 	// if this property passed, then save it to a file
 	if (verify_reward) { 

Modified: branches/uml/source/main/cMDEUniversalProperty.h
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.h	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cMDEUniversalProperty.h	2007-11-30 20:39:12 UTC (rev 2216)
@@ -27,7 +27,10 @@
 	void print(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
 	void printWitness(); // { std::cout << _scope << " " << _expr_p  << std::endl; }
 	void evaluate();
+	std::string getPropertyType() { return "Universal"; } 
+	std::string getPropertyParameters() { return _expr_p; }
 
+
 private:
 	std::string _expr_p;
 };

Modified: branches/uml/source/main/cUMLModel.cc
===================================================================
--- branches/uml/source/main/cUMLModel.cc	2007-11-30 17:57:00 UTC (rev 2215)
+++ branches/uml/source/main/cUMLModel.cc	2007-11-30 20:39:12 UTC (rev 2216)
@@ -454,7 +454,7 @@
 	// a pointer to the existence property
 	std::string temp = getStateDiagram(0)->StringifyAnInt(mdeprops.size());
 	cMDEExistenceProperty* e = new cMDEExistenceProperty(s, temp);
-	mdeprops.insert (mdeprops.end(), e);
+	mdeprops.insert (e);
 	//int q = mdeprops.size();
 	return true;
 }
@@ -464,7 +464,7 @@
 	// a pointer to the absence property
 	std::string temp = getStateDiagram(0)->StringifyAnInt(mdeprops.size());
 	cMDEAbsenceProperty* e = new cMDEAbsenceProperty(s, temp);
-	mdeprops.insert (mdeprops.end(), e);
+	mdeprops.insert (e);
 	//int q = mdeprops.size();
 	return true;
 	
@@ -475,7 +475,7 @@
 	// a pointer to the universal property
 	std::string temp = getStateDiagram(0)->StringifyAnInt(mdeprops.size());
 	cMDEUniversalProperty* e = new cMDEUniversalProperty(s, temp);
-	mdeprops.insert (mdeprops.end(), e);
+	mdeprops.insert (e);
 	//int q = mdeprops.size();
 	return true;