diff --git a/Makefile.am b/Makefile.am index f4bff59..2edf815 100644 --- a/Makefile.am +++ b/Makefile.am @@ -1,6 +1,6 @@ AUTOMAKE_OPTIONS = subdir-objects ACLOCAL_AMFLAGS = -I m4 ${ACLOCAL_FLAGS} -SUBDIRS = src doc +SUBDIRS = src . tests doc confdir = @prefix@/conf diff --git a/configure.ac b/configure.ac index 7099077..da85487 100644 --- a/configure.ac +++ b/configure.ac @@ -14,6 +14,7 @@ AC_PREFIX_DEFAULT(/usr/local/bigmc) AC_CONFIG_FILES([Makefile src/Makefile src/predicates/Makefile +tests/Makefile doc/Makefile ]) diff --git a/include/mc.h b/include/mc.h index c33641d..c903b73 100644 --- a/include/mc.h +++ b/include/mc.h @@ -28,6 +28,7 @@ class mc { unsigned long steps; static map properties; map checked; + static set match_discard; public: mc(bigraph *b); ~mc(); @@ -37,6 +38,8 @@ class mc { static void add_property(string s, query *q); bool check_properties(node *n); static void *thread_wrapper( void *i ); + static void match_mark_delete( match *m ); + static void match_gc(); }; #endif diff --git a/include/parsenode.h b/include/parsenode.h index 8ec1b10..28c9a62 100644 --- a/include/parsenode.h +++ b/include/parsenode.h @@ -55,7 +55,7 @@ class parsenode { public: int type; parsenode(); - ~parsenode(); + virtual ~parsenode(); virtual string to_string(); virtual bool is_valid(); virtual vector get_children(); diff --git a/include/query.h b/include/query.h index 92964a4..3435eb2 100644 --- a/include/query.h +++ b/include/query.h @@ -102,6 +102,7 @@ class query_predicate : public query { bool check(node *n); int eval(node *n); static void register_predicate(string name, predicate *p); + static void cleanup(); }; class query_scope : public query { diff --git a/src/Makefile.am b/src/Makefile.am index a09a4e6..7fd2930 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -3,17 +3,20 @@ AM_YFLAGS = -y -d BUILT_SOURCES = bgparser.h bin_PROGRAMS = bigmc -bigmc_SOURCES = bgparser.ypp \ + +noinst_LIBRARIES = libbigmc.a + +libbigmc_a_SOURCES = bgparser.ypp \ bgscanner.ll \ parser.cpp \ report.cpp \ bigraph.cpp \ driver.cpp \ graph.cpp \ - main.cpp \ match.cpp \ mc.cpp \ node.cpp \ + globals.cpp \ parsenode.cpp \ predicate.cpp \ query.cpp \ @@ -44,6 +47,7 @@ bigmc_SOURCES = bgparser.ypp \ ../include/matcher.h \ ../include/subtree.h + noinst_HEADERS = ../include/bigmc.h \ ../include/bigraph.h \ ../include/driver.h \ @@ -61,8 +65,11 @@ noinst_HEADERS = ../include/bigmc.h \ ../include/matcher.h \ ../include/subtree.h +libbigmc_a_CPPFLAGS = -I../include bigmc_CPPFLAGS = -I../include +bigmc_SOURCES = main.cpp +bigmc_LDADD = libbigmc.a + includes = ../include SUBDIRS = predicates - diff --git a/src/bgscanner.ll b/src/bgscanner.ll index 8c5d334..2371091 100644 --- a/src/bgscanner.ll +++ b/src/bgscanner.ll @@ -95,6 +95,9 @@ IDENTR [a-zA-Z0-9_] "%outer" { return OUTER; } +"%name" { + return OUTER; + } "%active" { return ACTIVE; } diff --git a/src/bigraph.cpp b/src/bigraph.cpp index 627f896..e4dfec6 100644 --- a/src/bigraph.cpp +++ b/src/bigraph.cpp @@ -193,7 +193,7 @@ bigraph *bigraph::apply_match(match *m) { b->rules = rules; // destroy the match -- we're done with it - delete m; + mc::match_mark_delete(m); return b; } else { if(m->get_rule()->reactum->type != TREGION) { @@ -236,7 +236,7 @@ bigraph *bigraph::apply_match(match *m) { delete nr; } - delete m; + mc::match_mark_delete(m); return b; } } diff --git a/src/driver.cpp b/src/driver.cpp index b3c0737..99b399f 100644 --- a/src/driver.cpp +++ b/src/driver.cpp @@ -39,5 +39,7 @@ void driver::check(bigraph *b) { delete m; + query_predicate::cleanup(); + exit(0); } diff --git a/src/globals.cpp b/src/globals.cpp new file mode 100644 index 0000000..9f0baf0 --- /dev/null +++ b/src/globals.cpp @@ -0,0 +1,12 @@ +using namespace std; +#include +#include +#include +#include +#include + +#include + +global_config global_cfg; + + diff --git a/src/main.cpp b/src/main.cpp index 03aeb41..ccc80fa 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -7,8 +7,6 @@ using namespace std; #include -global_config global_cfg; - void print_usage(char **argv) { fprintf(stderr, "Usage: %s [options] \n" @@ -128,6 +126,8 @@ void config_read() { } } + + free(configfile); } int main(int argc, char**argv) { @@ -218,6 +218,7 @@ int main(int argc, char**argv) { } parser::cleanup(); + query_predicate::cleanup(); return 0; } diff --git a/src/match.cpp b/src/match.cpp index 451aa85..4c154f1 100644 --- a/src/match.cpp +++ b/src/match.cpp @@ -24,13 +24,7 @@ using namespace std; #include #include -#include -#include -#include -#include -#include -#include -#include +#include #include @@ -45,6 +39,7 @@ match::match(reactionrule *rl) { rule = rl; has_failed = false; has_succeeded = false; + mc::match_mark_delete(this); } match::~match() { @@ -110,7 +105,7 @@ name match::get_name(name n) { set match::failure() { has_failed = true; has_succeeded = false; - delete this; + mc::match_mark_delete(this); return set(); } @@ -180,6 +175,8 @@ string match::to_string() { s += " Failed"; } + s += "\nParameters:\n"; + for(map::iterator i = parameters.begin(); i!=parameters.end(); i++) { std::stringstream p; p << i->first; @@ -242,7 +239,7 @@ wide_match::~wide_match() { list::iterator i = submatches.begin(); while(i != submatches.end()) { - delete *i; + mc::match_mark_delete(*i); i++; } diff --git a/src/matcher.cpp b/src/matcher.cpp index 256fc33..0208938 100644 --- a/src/matcher.cpp +++ b/src/matcher.cpp @@ -44,6 +44,8 @@ set matcher::try_match(prefix *t, prefix *r, match *m) { " against redex: " << r->to_string() << endl; } + assert(m != NULL); + if(t->get_control() == r->get_control()) { if(m->root == NULL && t->active_context()) { @@ -122,6 +124,7 @@ set matcher::try_match(parallel *t, prefix *r, match *m) { } set matcher::try_match(parallel *t, parallel *r, match *m) { + // FIXME: This approach can be optimised considerably! if(DEBUG) { rinfo("matcher::try_match") << "matching: " << t->to_string() << " against redex: " << r->to_string() << endl; @@ -131,6 +134,18 @@ set matcher::try_match(parallel *t, parallel *r, match *m) { set rch = r->get_children(); map > > matches; + hole *has_hole = NULL; // Is there a top level hole? e.g. A | B | $0 + // Something like A.$0 | B | C does not count. + // This will be the hole term itself, or NULL. + + for(set::iterator i = rch.begin(); i != rch.end(); i++) { + if((*i)->type == THOLE) { + has_hole = (hole *)*i; + rch.erase(i); + break; + } + } + if(rch.size()-1 > tch.size()) return m->failure(); @@ -142,7 +157,6 @@ set matcher::try_match(parallel *t, parallel *r, match *m) { m->root = t; } - m->add_match(r,t); int sum = rch.size() * tch.size(); @@ -162,58 +176,74 @@ set matcher::try_match(parallel *t, parallel *r, match *m) { set res; do { + cout << "PERM: "; + for(int i = 0; iclone(); for(set::iterator i = rch.begin(); i != rch.end(); i++) { if((*i)->type == THOLE) { - if(xdim > ydim && holecnt == 0) { - // There are "extra" things lying around, - // push these all into the hole. - set nch; - - nch.insert(cand[xdim-1-k++]); - - for(int l = 0; ladd_param(((hole*)(*i))->index, np); - succ++; - holecnt++; - continue; - } else if (xdim == ydim || holecnt > 0) { - nn->add_param(((hole*)(*i))->index, cand[xdim-1-k++]); - succ++; - continue; - } else { - nn->failure(); - break; - } + rerror("matcher::try_match") << "A hole remains at the top-level in the redex" << + ". This is a bug. Please report it." << endl; + exit(1); } set mm = try_match(cand[xdim-1-k++],*i,nn); - if(nn->has_failed) { - delete nn; - mm.clear(); + if(mm.size() == 0) { + //delete nn; + //mm.clear(); + nn->failure(); break; } - nn->has_succeeded = false; - res = match::merge(res,mm); + //res = match::merge(res,mm); succ++; + } + + if(succ < ydim) { + cout << "fail\n"; + continue; + } + + cout << "success\n"; + + if(has_hole != NULL) { + if(xdim - ydim > 1) { + // There are "extra" things lying around, + // push these all into the hole. + // The previous loop has matched cand[size - 1] ... cand[size - 1 - k] + // elements and has incremented k once more. + // Therefore we have cand[0] ... cand[size - k] elements to put in the hole. + set nch; + + for(int l = 0; ladd_param(has_hole->index, np); + } else if (xdim - ydim == 1) { + nn->add_param(has_hole->index, cand[0]); + succ++; + } else { + nn->add_param(has_hole->index, new nil()); + } } + if(succ >= ydim) { res.insert(nn); - } + } } while(next_permutation(cand, cand+xdim)); if(res.size() == 0) return m->failure(); diff --git a/src/mc.cpp b/src/mc.cpp index c34be0e..0ccb4f8 100644 --- a/src/mc.cpp +++ b/src/mc.cpp @@ -27,6 +27,8 @@ using namespace std; #include +#include + #ifdef HAVE_PTHREAD #include @@ -42,6 +44,7 @@ struct mc_id { }; map mc::properties; +set mc::match_discard; mc::mc(bigraph *b) { node *n = new node(b,NULL,NULL); @@ -60,6 +63,8 @@ void *mc::thread_wrapper( void *i ) { while(nc->data->step(nc->id)) ; + match_gc(); + return NULL; } @@ -73,7 +78,7 @@ bool mc::check() { i->data = this; i->id = 0; thread_wrapper(i); - cout << "mc::check(): Complete!" << endl; + rinfo("mc::check") << "Complete!" << endl; cout << report(steps) << endl; return false; @@ -97,7 +102,7 @@ bool mc::check() { rinfo("mc::check") << "Worker thread #" << i << " finished" << endl; } - cout << "mc::check(): Complete!" << endl; + rinfo("mc::check") << "Complete!" << endl; cout << report(steps) << endl; #else @@ -139,7 +144,7 @@ string mc::report(int step) { // returns true while there is work to do bool mc::step(int id) { if(steps >= global_cfg.max_steps) { - cout << "mc::step(): Interrupted! Reached maximum steps: " << global_cfg.max_steps << endl; + rinfo("mc::step") << "Interrupted! Reached maximum steps: " << global_cfg.max_steps << endl; cout << report(steps) << endl; return false; } @@ -169,8 +174,9 @@ bool mc::step(int id) { return false; #else - cout << "mc::step(): Complete!" << endl; + rinfo("mc::step") << "Complete!" << endl; cout << report(step) << endl; + match_gc(); // TODO: sound the alarms and release the balloons at this point. exit(0); return false; @@ -276,13 +282,15 @@ bool mc::step(int id) { matches.clear(); + match_gc(); + if(global_cfg.report_interval > 0 && step % global_cfg.report_interval == 0) { cout << report(step) << endl; } if(!check_properties(n)) { - cout << "mc::step(): Counter-example found." << endl; + rinfo("mc::step") << "Counter-example found." << endl; return false; } @@ -295,3 +303,25 @@ bool mc::step(int id) { void mc::add_property(string s,query *q) { properties[s] = q; } + +void mc::match_mark_delete( match *m ) { + assert(m != NULL); + + match_discard.insert(m); +} + +void mc::match_gc() { + set::iterator i = match_discard.begin(); + + unsigned long count = match_discard.size(); + + while(i != match_discard.end()) { + delete *i; + i++; + } + + match_discard.clear(); + + rinfo("mc::match_gc") << "Destroyed " << count << " objects" << endl; +} + diff --git a/src/parsenode.cpp b/src/parsenode.cpp index a0522e8..4fa80ad 100644 --- a/src/parsenode.cpp +++ b/src/parsenode.cpp @@ -67,6 +67,9 @@ prefixnode::prefixnode(parsenode *p, parsenode *q) { } prefixnode::~prefixnode() { + delete prefix; + if(suffix) + delete suffix; } string prefixnode::to_string() { @@ -96,6 +99,8 @@ parallelnode::parallelnode(parsenode *l, parsenode *r) { } parallelnode::~parallelnode() { + delete lhs; + delete rhs; } string parallelnode::to_string() { @@ -122,6 +127,8 @@ regionnode::regionnode(parsenode *l, parsenode *r) { } regionnode::~regionnode() { + delete lhs; + delete rhs; } string regionnode::to_string() { @@ -148,6 +155,8 @@ reactionnode::reactionnode(parsenode *red, parsenode *reac) { } reactionnode::~reactionnode() { + delete redex; + delete reactum; } string reactionnode::to_string() { @@ -169,12 +178,13 @@ vector reactionnode::get_children() { // NAME namenode::namenode(char *id) { - nme = strdup(id); + nme = id; // TODO compute hash type = NODE_NAME; } namenode::~namenode() { + free(nme); } string namenode::to_string() { @@ -226,6 +236,8 @@ seqnode::seqnode(parsenode *l, parsenode *r) { } seqnode::~seqnode() { + delete lhs; + delete rhs; } string seqnode::to_string() { @@ -252,6 +264,7 @@ interfacenode::interfacenode(parsenode *n, bool is_outer) { } interfacenode::~interfacenode() { + delete name; } string interfacenode::to_string() { @@ -281,6 +294,7 @@ signaturenode::signaturenode(parsenode *n, bool is_active, int ar) { } signaturenode::~signaturenode() { + delete name; } string signaturenode::to_string() { @@ -321,6 +335,7 @@ controlnode::controlnode(namenode *id, parsenode *linkseq) { } controlnode::~controlnode() { + delete name; } string controlnode::to_string() { @@ -351,7 +366,7 @@ propertynode::propertynode(char *nm, parsenode *p) { } propertynode::~propertynode() { - + delete prop; } string propertynode::to_string() { @@ -368,7 +383,8 @@ binnode::binnode(parsenode *l, int opr, parsenode *r) { } binnode::~binnode() { - + delete lprop; + delete rprop; } string binnode::to_string() { @@ -416,7 +432,7 @@ notnode::notnode(parsenode *l) { } notnode::~notnode() { - + delete prop; } string notnode::to_string() { @@ -432,7 +448,7 @@ prednode::prednode(char *n, parsenode *l) { } prednode::~prednode() { - + delete prop; } string prednode::to_string() { @@ -465,7 +481,7 @@ querynode::querynode(char *n, parsenode *l) { } querynode::~querynode() { - + delete prop; } string querynode::to_string() { @@ -482,7 +498,9 @@ ifnode::ifnode(parsenode *c, parsenode *t, parsenode *f) { } ifnode::~ifnode() { - + delete cond; + delete tbranch; + delete fbranch; } string ifnode::to_string() { diff --git a/src/parser.cpp b/src/parser.cpp index 6468902..7fbd398 100644 --- a/src/parser.cpp +++ b/src/parser.cpp @@ -439,6 +439,8 @@ bigraph *parser::finish() { cerr << (*it)->to_string() << endl; break; } + + delete *it; } return b; diff --git a/src/query.cpp b/src/query.cpp index f6ebae3..537a5bc 100644 --- a/src/query.cpp +++ b/src/query.cpp @@ -197,6 +197,14 @@ int query_predicate::eval(node *n) { return p->invoke_eval(n,params); } +void query_predicate::cleanup() { + for(map::iterator i = predicates.begin(); i != predicates.end(); i++) { + if(i->second != NULL) + delete i->second; + } + + predicates.clear(); +} // query_val query_val::query_val() { diff --git a/tests/Makefile.am b/tests/Makefile.am new file mode 100644 index 0000000..f7b7bc2 --- /dev/null +++ b/tests/Makefile.am @@ -0,0 +1,17 @@ + +AM_DEFAULT_SOURCE_EXT = .cpp +AM_COLOR_TESTS=yes +AM_LDFLAGS = -lcpptest + +check_PROGRAMS = test-bigraph test-matcher + +TESTS = $(check_PROGRAMS) + +test_bigraph_SOURCES = test-bigraph.cpp +test_bigraph_CPPFLAGS = -I../include +test_bigraph_LDADD = $(top_builddir)/src/libbigmc.a + +test_matcher_SOURCES = test-matcher.cpp +test_matcher_CPPFLAGS = -I../include +test_matcher_LDADD = $(top_builddir)/src/libbigmc.a + diff --git a/tests/test-bigraph.cpp b/tests/test-bigraph.cpp new file mode 100644 index 0000000..f86198d --- /dev/null +++ b/tests/test-bigraph.cpp @@ -0,0 +1,63 @@ +#include + +#include + +class BigraphTestSuite : public Test::Suite { +public: + BigraphTestSuite() + { + TEST_ADD(BigraphTestSuite::name_test) + TEST_ADD(BigraphTestSuite::control_test) + } + +private: + void name_test(); + void control_test(); +}; + +void BigraphTestSuite::name_test() { + bigraph *b = new bigraph(1); + + name n1 = bigraph::name_from_string("abc"); + name n2 = bigraph::name_from_string("a"); + name n3 = bigraph::name_from_string("Xyz"); + + b->add_outer_name(n1); + b->add_outer_name(n2); + + TEST_ASSERT(bigraph::name_to_string(n1) == "abc"); + TEST_ASSERT(!bigraph::is_free(n2)); + TEST_ASSERT(bigraph::is_free(n3)); + + delete b; +} + +void BigraphTestSuite::control_test() { + control c1 = bigraph::control_from_string("abcdefg"); + control c2 = bigraph::control_from_string("Xyz"); + control c3 = bigraph::control_from_string("FOO"); + + TEST_ASSERT(bigraph::control_to_string(c1) == "abcdefg"); + TEST_ASSERT(bigraph::control_to_string(c2) == "Xyz"); + TEST_ASSERT(bigraph::control_to_string(c3) == "FOO"); + + bigraph *b = new bigraph(0); + + bigraph::add_control("abcdefg", true, 2); + bigraph::add_control("Xyz", false, 0); + + TEST_ASSERT(bigraph::arity(c1) == 2); + TEST_ASSERT(bigraph::arity(c2) == 0); + + TEST_ASSERT(bigraph::activity(c1)); + TEST_ASSERT(!bigraph::activity(c2)); + + delete b; +} + +int main(int argc, char **argv) { + Test::CompilerOutput output(Test::CompilerOutput::GCC); + BigraphTestSuite ts; + return ts.run(output) ? EXIT_SUCCESS : EXIT_FAILURE; +} + diff --git a/tests/test-matcher.cpp b/tests/test-matcher.cpp new file mode 100644 index 0000000..1fda830 --- /dev/null +++ b/tests/test-matcher.cpp @@ -0,0 +1,68 @@ +#include + +#include + +#include + +class MatcherTestSuite : public Test::Suite { +public: + MatcherTestSuite() + { + TEST_ADD(MatcherTestSuite::match_test) + TEST_ADD(MatcherTestSuite::anywhere_test) + TEST_ADD(MatcherTestSuite::parallel_test) + } + +private: + void match_test(); + void anywhere_test(); + void parallel_test(); +}; + +void MatcherTestSuite::match_test() { + +} + +void MatcherTestSuite::parallel_test() { + control a = bigraph::add_control("a", true, 0); + control b = bigraph::add_control("b", true, 0); + control c = bigraph::add_control("c", true, 0); + control d = bigraph::add_control("d", true, 0); + + set ch; + ch.insert(new prefix(a, vector(), new nil())); + ch.insert(new prefix(b, vector(), new nil())); + ch.insert(new prefix(c, vector(), new nil())); + ch.insert(new prefix(d, vector(), new nil())); + parallel *tm = new parallel(ch); + + set ch2; + ch2.insert(new prefix(a, vector(), new nil())); + ch2.insert(new prefix(b, vector(), new nil())); + ch2.insert(new hole(0)); + parallel *redex = new parallel(ch2); + + set matches = matcher::try_match(tm, redex, new match(new reactionrule(redex, new nil()))); + + std::cout << "matches.size(): " << matches.size() << std::endl; + + for(set::iterator i = matches.begin(); i != matches.end(); i++) { + std::cout << (*i)->to_string() << endl; + } + + TEST_ASSERT(matches.size() == 1); +} + + + +void MatcherTestSuite::anywhere_test() { + +} + +int main(int argc, char **argv) { + Test::CompilerOutput output(Test::CompilerOutput::GCC); + MatcherTestSuite ts; + return ts.run(output) ? EXIT_SUCCESS : EXIT_FAILURE; +} + +