[Avida-SVN] r2212 - branches/uml/source/main
hjg at myxo.css.msu.edu
hjg at myxo.css.msu.edu
Wed Nov 28 04:21:59 PST 2007
Author: hjg
Date: 2007-11-28 07:21:58 -0500 (Wed, 28 Nov 2007)
New Revision: 2212
Added:
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.cc
branches/uml/source/main/cMDEProperty.h
branches/uml/source/main/cMDEUniversalProperty.cc
branches/uml/source/main/cMDEUniversalProperty.h
Log:
property files.
Added: branches/uml/source/main/cMDEAbsenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.cc (rev 0)
+++ branches/uml/source/main/cMDEAbsenceProperty.cc 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,68 @@
+/*
+ * cMDEAbsenceProperty.cc
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#include "cMDEAbsenceProperty.h"
+
+void cMDEAbsenceProperty::print() {
+
+ std::ofstream outfile;
+ outfile.open (_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* !([](!p)) */" << std::endl;
+ outfile << "T0_init : /* init */" << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (1) -> goto T0_init " << std::endl;
+ outfile << ":: (p) -> goto accept_all" << std::endl;
+ outfile << "fi;" << std::endl;
+ outfile << "accept_all : /* 1 */" << std::endl;
+ outfile << "skip " << std::endl;
+ outfile << "}" << std::endl;
+
+ outfile.close();
+
+}
+
+void cMDEAbsenceProperty::printWitness() {
+
+
+
+ std::ofstream outfile;
+ std::string file_name= "w" + _name;
+ outfile.open (file_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* !([](!p)) */" << std::endl;
+ outfile << "T0_init : /* init */" << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (1) -> goto T0_init " << std::endl;
+ outfile << ":: (p) -> goto accept_all" << std::endl;
+ outfile << "fi;" << std::endl;
+ outfile << "accept_all : /* 1 */" << std::endl;
+ outfile << "skip " << std::endl;
+ outfile << "}" << std::endl;
+
+
+
+ outfile.close();
+
+}
+
+
+void cMDEAbsenceProperty::evaluate()
+{
+ float verify_reward = 0;
+
+ // print the property
+ print();
+ verify_reward = verify();
+ _reward = verify_reward;
+}
Added: branches/uml/source/main/cMDEAbsenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEAbsenceProperty.h (rev 0)
+++ branches/uml/source/main/cMDEAbsenceProperty.h 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,35 @@
+/*
+ * cMDEAbsenceProperty.h
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#ifndef _C_MDEABSENCEPROPERTY_H_
+#define _C_MDEABSENCEPROPERTY_H_
+
+#include "cMDEProperty.h"
+#include <string>
+#include <fstream>
+#include <iostream>
+
+
+/* Used to represent properties of the form: Globally, it is never the case that P holds */
+
+class cMDEAbsenceProperty : public cMDEProperty{
+
+public:
+ cMDEAbsenceProperty(std::string expr, std::string q) { _expr_p = expr;
+ _name = ("Absence" + q); _reward = -1; }
+ virtual ~cMDEAbsenceProperty() {}
+ void print(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+ void printWitness(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+ void evaluate();
+
+private:
+ std::string _expr_p;
+};
+
+#endif
Added: branches/uml/source/main/cMDEExistenceProperty.cc
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.cc (rev 0)
+++ branches/uml/source/main/cMDEExistenceProperty.cc 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,50 @@
+/*
+ * cMDEExistenceProperty.cc
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#include "cMDEExistenceProperty.h"
+
+void cMDEExistenceProperty::print() {
+
+ std::ofstream outfile;
+ outfile.open (_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* !(<>(p)) */ " << std::endl;
+ outfile << "accept_init : /* init */" << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (!p) -> goto accept_init " << std::endl;
+ outfile << "fi; }" << std::endl;
+
+ outfile.close();
+
+}
+
+void cMDEExistenceProperty::printWitness() {
+
+ std::ofstream outfile;
+ std::string file_name = "w" + _name;
+ outfile.open (file_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* !([](!p)) */ " << std::endl;
+ outfile << "T0_init : /* init */ " << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (1) -> goto T0_init" << std::endl;
+ outfile << ":: (p) -> goto accept_all " << std::endl;
+ outfile << "fi; " << std::endl;
+ outfile << "accept_all : /* 1 */" << std::endl;
+ outfile << "skip }" << std::endl;
+
+
+ outfile.close();
+
+}
+
Added: branches/uml/source/main/cMDEExistenceProperty.h
===================================================================
--- branches/uml/source/main/cMDEExistenceProperty.h (rev 0)
+++ branches/uml/source/main/cMDEExistenceProperty.h 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,36 @@
+/*
+ * cMDEExistenceProperty.h
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#ifndef _C_MDEEXISTENCEPROPERTY_H_
+#define _C_MDEEXISTENCEPROPERTY_H_
+
+#include "cMDEProperty.h"
+#include <string>
+#include <fstream>
+#include <iostream>
+
+
+/* Used to represent properties of the form: Globally, P eventually holds */
+
+class cMDEExistenceProperty : public cMDEProperty{
+
+public:
+ cMDEExistenceProperty(std::string expr, std::string q) { _expr_p = expr;
+ _name = ("Existence" + q); _reward = -1;}
+
+ virtual ~cMDEExistenceProperty() {}
+
+ void print(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+ void printWitness(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+
+private:
+ std::string _expr_p;
+};
+
+#endif
Added: branches/uml/source/main/cMDEProperty.cc
===================================================================
--- branches/uml/source/main/cMDEProperty.cc (rev 0)
+++ branches/uml/source/main/cMDEProperty.cc 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,67 @@
+/*
+ * cMDEProperty.cc
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#include "cMDEProperty.h"
+
+float cMDEProperty::numWitnesses() {
+
+ float num_witness = 0;
+ // const int max_witness = 1;
+
+ std::string file_name = "tmp-witness" + _name + ".pr";
+ std::string cmd = "cp tmp.pr "+ file_name;
+
+ if(system(cmd.c_str())!=0) return 0.0;
+
+ cmd = "cat w" + _name + " >> " + 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);}}'"));
+
+ return num_witness;
+}
+
+
+float cMDEProperty::verify() {
+ std::string file_name = "tmp-" + _name + ".pr";
+ std::string cmd = "cp tmp.pr "+ file_name;
+ if(system(cmd.c_str())!=0) return 0.0;
+
+
+ cmd = "cat " + _name + " >> " + 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 -a &> ./pan.out")!=0) return 0.0;
+ if(system("cat pan.out | perl -e 'while(<STDIN>) { if(/errors:\\s(\\d+)/) {exit($1);}}'")!=0) return 0.0;
+ return 1.0;
+}
+
+
+void cMDEProperty::evaluate() {
+ float wit_reward = 0;
+ float verify_reward = 0;
+
+ // print the witness property
+ printWitness();
+ // call numWitnesses
+ wit_reward = numWitnesses();
+
+ // call verify
+ if (wit_reward > 0) {
+ // print the property
+ print();
+ verify_reward = verify();
+ }
+ _reward = wit_reward + verify_reward;
+
+}
+
Added: branches/uml/source/main/cMDEProperty.h
===================================================================
--- branches/uml/source/main/cMDEProperty.h (rev 0)
+++ branches/uml/source/main/cMDEProperty.h 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,39 @@
+#ifndef _C_MDEPROPERTY_H_
+#define _C_MDEPROPERTY_H_
+/*
+ * cMDEProperty.h
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+#include <string>
+#include <iostream>
+
+
+class cMDEProperty{
+
+public:
+ virtual ~cMDEProperty() {}
+ // A function that prints the property to a file.
+ virtual void print() = 0;
+ virtual void printWitness() = 0;
+ // A function that checks to see if there is a witness trace for the property
+ float numWitnesses();
+ // A function that verifies a property
+ float verify();
+ // A function that evaluates a property
+ virtual void evaluate();
+ std::string getMDEPropertyName() { return _name; }
+ void setEvaluationInformation (float eval) { _reward = eval; }
+ float getEvaluationInformation() { return _reward; }
+
+protected:
+ std::string _name;
+ std::string _scope;
+ float _reward;
+
+};
+
+#endif
Added: branches/uml/source/main/cMDEUniversalProperty.cc
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.cc (rev 0)
+++ branches/uml/source/main/cMDEUniversalProperty.cc 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,67 @@
+/*
+ * cMDEUniversalProperty.cc
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+
+#include "cMDEUniversalProperty.h"
+
+void cMDEUniversalProperty::print() {
+
+ std::ofstream outfile;
+ outfile.open (_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* ![]p */" << std::endl;
+ outfile << "T0_init : /* init */" << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (1) -> goto T0_init " << std::endl;
+ outfile << ":: (!p) -> goto accept_all" << std::endl;
+ outfile << "fi;" << std::endl;
+ outfile << "accept_all : /* 1 */" << std::endl;
+ outfile << "skip " << std::endl;
+ outfile << "}" << std::endl;
+
+ outfile.close();
+
+}
+
+void cMDEUniversalProperty::printWitness() {
+
+ std::ofstream outfile;
+ std::string file_name = "w" + _name;
+ outfile.open (file_name.c_str());
+ assert(outfile.is_open());
+
+ outfile << "#define p (" << _expr_p << ")" << std::endl;
+ outfile << "never { /* !([](p)) */" << std::endl;
+ outfile << "T0_init : /* init */" << std::endl;
+ outfile << "if " << std::endl;
+ outfile << ":: (! ((p))) -> goto accept_all" << std::endl;
+ outfile << ":: (1) -> goto T0_init" << std::endl;
+ outfile << "fi;" << std::endl;
+ outfile << "accept_all : " << std::endl;
+ outfile << "skip " << std::endl;
+ outfile << "}" << std::endl;
+
+ outfile.close();
+
+}
+
+
+void cMDEUniversalProperty::evaluate()
+{
+ float verify_reward = 0;
+
+ // print the property
+ print();
+ verify_reward = verify();
+ _reward = verify_reward;
+}
+
+
+
Added: branches/uml/source/main/cMDEUniversalProperty.h
===================================================================
--- branches/uml/source/main/cMDEUniversalProperty.h (rev 0)
+++ branches/uml/source/main/cMDEUniversalProperty.h 2007-11-28 12:21:58 UTC (rev 2212)
@@ -0,0 +1,36 @@
+/*
+ * cMDEUniversalProperty.h
+ *
+ *
+ * Created by Heather Goldsby on 11/20/07.
+ * Copyright 2007 __MyCompanyName__. All rights reserved.
+ *
+ */
+#ifndef _C_MDEUNIVERSALPROPERTY_H_
+#define _C_MDEUNIVERSALPROPERTY_H_
+#include "cMDEProperty.h"
+
+#include <string>
+#include <fstream>
+#include <iostream>
+
+
+
+/* Used to represent properties of the form: Globally, it is always the case that P holds */
+
+class cMDEUniversalProperty : public cMDEProperty{
+
+public:
+ cMDEUniversalProperty(std::string expr, std::string q) { _expr_p = expr;
+ _name = ("Universal" + q); _reward = -1;}
+ virtual ~cMDEUniversalProperty() {}
+ void print(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+ void printWitness(); // { std::cout << _scope << " " << _expr_p << std::endl; }
+ void evaluate();
+
+private:
+ std::string _expr_p;
+};
+
+#endif
+
More information about the Avida-cvs
mailing list