[Avida-SVN] r2449 - branches/uml/source/main
hjg at myxo.css.msu.edu
hjg at myxo.css.msu.edu
Tue Mar 11 05:58:06 PDT 2008
Author: hjg
Date: 2008-03-11 08:58:06 -0400 (Tue, 11 Mar 2008)
New Revision: 2449
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/cMDEPrecedenceProperty.cc
branches/uml/source/main/cMDEPrecedenceProperty.h
branches/uml/source/main/cMDEProperty.cc
branches/uml/source/main/cMDEProperty.h
branches/uml/source/main/cMDEResponseProperty.cc
branches/uml/source/main/cMDEResponseProperty.h
branches/uml/source/main/cMDEUniversalProperty.cc
branches/uml/source/main/cMDEUniversalProperty.h
branches/uml/source/main/cStats.cc
Log:
Added support for additional property logging and fixed property file printing.
Modified: branches/uml/source/main/cMDEAbsenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEAbsenceProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -11,9 +11,13 @@
void cMDEAbsenceProperty::print() {
+ // Create the file...
+ std::string cmd = "cp " + _promela + " " + _property_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode...
std::ofstream outfile;
-// outfile.open (_name.c_str());
- outfile.open ("property");
+ outfile.open (_property_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "#define p (" << _expr_p << ")" << std::endl;
@@ -33,10 +37,13 @@
void cMDEAbsenceProperty::printWitness() {
+ // Create the file
+ std::string cmd = "cp " + _promela + " " + _witness_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode
std::ofstream outfile;
-// std::string file_name= "w" + _name;
- std::string file_name = "witness-property";
- outfile.open (file_name.c_str());
+ outfile.open (_witness_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Absence property " << _expr_p << "*/" << std::endl;
@@ -66,12 +73,13 @@
print();
verify_reward = verify();
std::string cmd;
- std::string work_prop = "properties_that_passed";
+// std::string work_prop = "properties_that_passed";
// if this property passed, then save it to a file
if (verify_reward) {
- cmd = "cat english-property >> " + work_prop;
- system(cmd.c_str());
+// cmd = "cat english-property >> " + work_prop;
+// system(cmd.c_str());
+ printInEnglish();
}
_reward = verify_reward;
@@ -81,12 +89,13 @@
void cMDEAbsenceProperty::printInEnglish() {
std::ofstream outfile;
- std::string file_name = "english-property";
- outfile.open (file_name.c_str());
+ outfile.open (_properties.c_str(), std::ios_base::app);
assert(outfile.is_open());
+
+ outfile << _interesting << ", " << _uses_related_classes << ", ";
outfile << "Globally, it is never the case that " << _expr_p << " holds. ";
- outfile << _interesting << " " << _uses_related_classes << std::endl << std::endl;
+ outfile << std::endl << std::endl;
outfile.close();
Modified: branches/uml/source/main/cMDEAbsenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEAbsenceProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -21,7 +21,14 @@
class cMDEAbsenceProperty : public cMDEProperty{
public:
- cMDEAbsenceProperty(std::string expr) { _expr_p = expr; _reward = -1; }
+ cMDEAbsenceProperty(std::string expr) {
+ _expr_p = expr;
+ _reward = -1;
+ _property_file_name = "tmp-property.pr";
+ _witness_file_name = "tmp-witness.pr";
+ _properties = "properties_that_passed";
+ _promela = "tmp.pr";
+ }
virtual ~cMDEAbsenceProperty() {}
void print(); // { std::cout << _scope << " " << _expr_p << std::endl; }
void printWitness(); // { std::cout << _scope << " " << _expr_p << std::endl; }
Modified: branches/uml/source/main/cMDEExistenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEExistenceProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -11,11 +11,16 @@
void cMDEExistenceProperty::print() {
+ // Create the file...
+ std::string cmd = "cp " + _promela + " " + _property_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode...
std::ofstream outfile;
-// outfile.open (_name.c_str());
- outfile.open ("property");
+ outfile.open (_property_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
+ // Add the existence property to the end of the file...
outfile << "/* Existence property " << _expr_p << "*/" << std::endl;
outfile << "#define p (" << _expr_p << ")" << std::endl;
outfile << "never { /* !(<>(p)) */ " << std::endl;
@@ -24,17 +29,23 @@
outfile << ":: (!p) -> goto accept_init " << std::endl;
outfile << "fi; }" << std::endl;
+ // close the file...
outfile.close();
}
void cMDEExistenceProperty::printWitness() {
+ // Create the file
+ std::string cmd = "cp " + _promela + " " + _witness_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode
std::ofstream outfile;
- std::string file_name = "witness-property";
- outfile.open (file_name.c_str());
+ outfile.open (_witness_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
+ // Add existence witness
outfile << "#define p (" << _expr_p << ")" << std::endl;
outfile << "never { /* !([](!p)) */ " << std::endl;
outfile << "T0_init : /* init */ " << std::endl;
@@ -44,8 +55,8 @@
outfile << "fi; " << std::endl;
outfile << "accept_all : /* 1 */" << std::endl;
outfile << "skip }" << std::endl;
-
+
outfile.close();
}
@@ -53,14 +64,12 @@
void cMDEExistenceProperty::printInEnglish() {
std::ofstream outfile;
- std::string file_name = "english-property";
- outfile.open (file_name.c_str());
+ outfile.open (_properties.c_str(), std::ios_base::app);
assert(outfile.is_open());
- outfile << "Globally, " << _expr_p << " eventually holds. ";
- outfile << _interesting << " " << _uses_related_classes << std::endl << std::endl;
+ outfile << _interesting << ", " << _uses_related_classes << ", ";
+ outfile << "Globally, " << _expr_p << " eventually holds." << std::endl<< std::endl;
outfile.close();
-
}
Modified: branches/uml/source/main/cMDEExistenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEExistenceProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -22,7 +22,14 @@
class cMDEExistenceProperty : public cMDEProperty{
public:
- cMDEExistenceProperty(std::string expr) { _expr_p = expr; _reward = -1;}
+ cMDEExistenceProperty(std::string expr) {
+ _expr_p = expr;
+ _reward = -1;
+ _property_file_name = "tmp-property.pr";
+ _witness_file_name = "tmp-witness.pr";
+ _properties = "properties_that_passed";
+ _promela = "tmp.pr";
+ }
virtual ~cMDEExistenceProperty() {}
Modified: branches/uml/source/main/cMDEPrecedenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEPrecedenceProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEPrecedenceProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -10,9 +10,13 @@
#include "cMDEPrecedenceProperty.h"
void cMDEPrecedenceProperty::print() {
+ // Create the file...
+ std::string cmd = "cp " + _promela + " " + _property_file_name;
+ assert(system(cmd.c_str())!=0);
+ // Open the file in append mode...
std::ofstream outfile;
- outfile.open ("property");
+ outfile.open (_property_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Precedence property " << _expr_p << " " << _expr_q << "*/" << std::endl;
@@ -50,9 +54,13 @@
void cMDEPrecedenceProperty::printWitness() {
+ // Create the file
+ std::string cmd = "cp " + _promela + " " + _witness_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode
std::ofstream outfile;
- std::string file_name = "witness-property";
- outfile.open (file_name.c_str());
+ outfile.open (_witness_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Precedence property " << _expr_p << " " << _expr_q << "*/" << std::endl;
@@ -80,13 +88,14 @@
void cMDEPrecedenceProperty::printInEnglish() {
std::ofstream outfile;
- std::string file_name = "english-property";
- outfile.open (file_name.c_str());
+ outfile.open (_properties.c_str(), std::ios_base::app);
assert(outfile.is_open());
+
+ outfile << _interesting << ", " << _uses_related_classes << ", ";
outfile << "Globally, it is always the case that if " << _expr_p << " holds, ";
outfile << "then "<< _expr_q << " previously held. ";
- outfile << _interesting << " " << _uses_related_classes << std::endl << std::endl;
+ outfile << std::endl << std::endl;
outfile.close();
Modified: branches/uml/source/main/cMDEPrecedenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEPrecedenceProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEPrecedenceProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -26,6 +26,10 @@
_expr_p = p;
_expr_q = q;
_reward = -1;
+ _property_file_name = "tmp-property.pr";
+ _witness_file_name = "tmp-witness.pr";
+ _properties = "properties_that_passed";
+ _promela = "tmp.pr";
}
virtual ~cMDEPrecedenceProperty() {}
Modified: branches/uml/source/main/cMDEProperty.cc
===================================================================
--- branches/uml/source/main/cMDEProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -20,15 +20,15 @@
float cMDEProperty::numWitnesses() {
- std::string file_name = "tmp-witness.pr";
- std::string cmd = "cp tmp.pr "+ file_name;
+ //std::string file_name = "tmp-witness.pr";
+ std::string cmd; // = "cp tmp.pr "+ WITNESS;
int num_witness = 0;
+// if(system(cmd.c_str())!=0) return 0.0;
+// cmd = "cat witness-property >> " + file_name + " && ./spin -a " + file_name + " &> /dev/null";
+ cmd = "./spin -a " + _witness_file_name + " &> /dev/null";
if(system(cmd.c_str())!=0) return 0.0;
- cmd = "cat witness-property >> " + file_name + " && ./spin -a " + file_name + " &> /dev/null";
- if(system(cmd.c_str())!=0) return 0.0;
-
if(system("/usr/bin/gcc -DMEMLIM=512 pan.c -o pan &> /dev/null")!=0) return 0.0;
if(system("./pan -e -n -a -w19 -m100000 -c1 &> ./pan.out")!=0) return 0.0;
num_witness = (system("cat pan.out | perl -e 'while(<STDIN>) { if(/errors:\\s(\\d+)/) {exit($1);}}'"));
@@ -41,12 +41,13 @@
float cMDEProperty::verify() {
- std::string file_name = "tmp-property.pr";
- std::string cmd = "cp tmp.pr "+ file_name;
- if(system(cmd.c_str())!=0) return 0.0;
+// std::string file_name = "tmp-property.pr";
+ std::string cmd; // = "cp tmp.pr "+ _property_file_name;
+// if(system(cmd.c_str())!=0) return 0.0;
- cmd = "cat property >> " + file_name + " && ./spin -a " + file_name + " &> /dev/null";
+// cmd = "cat property >> " + file_name + " && ./spin -a " + file_name + " &> /dev/null";
+ cmd = "./spin -a " + _property_file_name + " &> /dev/null";
if(system(cmd.c_str())!=0) return 0.0;
if(system("/usr/bin/gcc -DMEMLIM=512 pan.c -o pan &> /dev/null")!=0) return 0.0;
@@ -79,8 +80,8 @@
// if this property passed, then save it to a file
if (verify_reward) {
printInEnglish();
- cmd = "cat english-property >> " + work_prop;
- system(cmd.c_str());
+// cmd = "cat english-property >> " + work_prop;
+// system(cmd.c_str());
}
_reward = verify_reward;
Modified: branches/uml/source/main/cMDEProperty.h
===================================================================
--- branches/uml/source/main/cMDEProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -25,7 +25,6 @@
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
float numWitnesses();
// A function that verifies a property
@@ -54,6 +53,12 @@
float _interesting;
bool _uses_related_classes;
+ // Name of the output filesw:
+ std::string _property_file_name; // = "tmp-property.pr";
+ std::string _witness_file_name; // = "tmp-witness.pr";
+ std::string _properties; // = "properties_that_passed";
+ std::string _promela;
+
};
struct ltcMDEProperty{
Modified: branches/uml/source/main/cMDEResponseProperty.cc
===================================================================
--- branches/uml/source/main/cMDEResponseProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEResponseProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -11,9 +11,13 @@
void cMDEResponseProperty::print() {
+ // Create the file...
+ std::string cmd = "cp " + _promela + " " + _property_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode...
std::ofstream outfile;
-// outfile.open (_name.c_str());
- outfile.open ("property");
+ outfile.open (_property_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Response property " << _expr_p << " " << _expr_q << "*/" << std::endl;
@@ -36,9 +40,13 @@
void cMDEResponseProperty::printWitness() {
+ // Create the file
+ std::string cmd = "cp " + _promela + " " + _witness_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode
std::ofstream outfile;
- std::string file_name = "witness-property";
- outfile.open (file_name.c_str());
+ outfile.open (_witness_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Response property " << _expr_p << " " << _expr_q << "*/" << std::endl;
@@ -67,14 +75,14 @@
void cMDEResponseProperty::printInEnglish() {
std::ofstream outfile;
- std::string file_name = "english-property";
- outfile.open (file_name.c_str());
+ outfile.open (_properties.c_str(), std::ios_base::app);
assert(outfile.is_open());
-
+
+ outfile << _interesting << ", " << _uses_related_classes << ", ";
outfile << "Globally, it is always the case that if " << _expr_p << " holds, ";
outfile << "then "<< _expr_q << " eventually holds. ";
- outfile << _interesting << " " << _uses_related_classes << std::endl << std::endl;
-
+ outfile << std::endl << std::endl;
+
outfile.close();
}
Modified: branches/uml/source/main/cMDEResponseProperty.h
===================================================================
--- branches/uml/source/main/cMDEResponseProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEResponseProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -26,6 +26,10 @@
_expr_p = p;
_expr_q = q;
_reward = -1;
+ _property_file_name = "tmp-property.pr";
+ _witness_file_name = "tmp-witness.pr";
+ _properties = "properties_that_passed";
+ _promela = "tmp.pr";
}
virtual ~cMDEResponseProperty() {}
Modified: branches/uml/source/main/cMDEUniversalProperty.cc
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEUniversalProperty.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -11,9 +11,13 @@
void cMDEUniversalProperty::print() {
+ // Create the file...
+ std::string cmd = "cp " + _promela + " " + _property_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode...
std::ofstream outfile;
-// outfile.open (_name.c_str());
- outfile.open ("property");
+ outfile.open (_property_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "/* Universal property " << _expr_p << "*/" << std::endl;
@@ -34,10 +38,13 @@
void cMDEUniversalProperty::printWitness() {
+ // Create the file
+ std::string cmd = "cp " + _promela + " " + _witness_file_name;
+ assert(system(cmd.c_str())!=0);
+
+ // Open the file in append mode
std::ofstream outfile;
-// std::string file_name = "w" + _name;
- std::string file_name = "witness-property";
- outfile.open (file_name.c_str());
+ outfile.open (_witness_file_name.c_str(), std::ios_base::app);
assert(outfile.is_open());
outfile << "#define p (" << _expr_p << ")" << std::endl;
@@ -63,14 +70,15 @@
// print the property
print();
verify_reward = verify();
- std::string cmd;
- std::string work_prop = "properties_that_passed";
+// std::string cmd;
+// std::string work_prop = "properties_that_passed";
// if this property passed, then save it to a file
if (verify_reward) {
+ printInEnglish();
// cmd = "cat " + _name + " >> " + work_prop;
- cmd = "cat english-property >> " + work_prop;
- system(cmd.c_str());
+// cmd = "cat english-property >> " + work_prop;
+// system(cmd.c_str());
}
_reward = verify_reward;
@@ -81,12 +89,12 @@
void cMDEUniversalProperty::printInEnglish() {
std::ofstream outfile;
- std::string file_name = "english-property";
- outfile.open (file_name.c_str());
- assert(outfile.is_open());
+ outfile.open (_properties.c_str(), std::ios_base::app);
+ assert(outfile.is_open());
+ outfile << _interesting << ", " << _uses_related_classes << ", ";
outfile << "Globally, it is always the case that " << _expr_p << " holds. ";
- outfile << _interesting << " " << _uses_related_classes << std::endl << std::endl;
+ outfile << std::endl << std::endl;
outfile.close();
}
Modified: branches/uml/source/main/cMDEUniversalProperty.h
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.h 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cMDEUniversalProperty.h 2008-03-11 12:58:06 UTC (rev 2449)
@@ -21,7 +21,13 @@
class cMDEUniversalProperty : public cMDEProperty{
public:
- cMDEUniversalProperty(std::string expr) { _expr_p = expr; _reward = -1;}
+ cMDEUniversalProperty(std::string expr) { _expr_p = expr;
+ _reward = -1;
+ _property_file_name = "tmp-property.pr";
+ _witness_file_name = "tmp-witness.pr";
+ _properties = "properties_that_passed";
+ _promela = "tmp.pr";
+ }
virtual ~cMDEUniversalProperty() {}
void print(); // { std::cout << _scope << " " << _expr_p << std::endl; }
void printWitness(); // { std::cout << _scope << " " << _expr_p << std::endl; }
Modified: branches/uml/source/main/cStats.cc
===================================================================
--- branches/uml/source/main/cStats.cc 2008-03-11 03:13:06 UTC (rev 2448)
+++ branches/uml/source/main/cStats.cc 2008-03-11 12:58:06 UTC (rev 2449)
@@ -1035,6 +1035,7 @@
df.WriteComment( "Avida uml properties\n" );
df.WriteTimeStamp();
df.Write( GetUpdate(), "update" );
+ df.Write(sum_merit.Average(), "Merit");
df.Write( m_propertySuccess, "total number of properties that passed" );
df.Write( m_propertyFailure, "total number of properties that failed" );
df.Write( m_propertyTotal, "total number of properties" );
More information about the Avida-cvs
mailing list