Commits

Anonymous committed 900f584

fixed unit test for evaluation

Comments (0)

Files changed (1)

tests/ctl_result.cc

+#include <iostream>
+#include <string>
+#include <fstream>
+
+#include <gtest/gtest.h>
+
+#include "kripke-parser.hh"
+#include "ctl-eval.hh"
+#include "ctl-parser.hh"
+
+bool ctl_eval(const std::string& fn, const std::string& ctl) {
+
+	std::ifstream in (fn);
+	in.unsetf(std::ios::skipws);
+
+	spirit::istream_iterator begin(in);
+	spirit::istream_iterator end;
+
+	bdd_init(1000, 1000);
+	bdd_gbc_hook(0);
+
+	KripkeBDD kripke;
+	KripkeFile<spirit::istream_iterator> kripke_grammar(kripke);
+
+	bool parsed = qi::phrase_parse(
+		begin, end,
+		kripke_grammar,
+		qi::space
+	);
+
+	kripke.simplify();
+
+	if (!parsed || begin != end) {
+		bdd_done();
+		return false;
+	}
+
+	Expr ctl_ast;
+	std::string sctl(ctl);
+	std::string::iterator beg = sctl.begin();
+	std::string::iterator ed = sctl.end();
+	CTLFormula<std::string::iterator> formula;
+	bool parsedd = qi::phrase_parse(
+		beg, ed,
+		formula,
+		qi::space,
+		ctl_ast
+	);
+
+	if (!parsedd || beg != ed) {
+		bdd_done();
+		return false;
+	}
+	CTLEval ev(kripke);
+	bdd res = boost::apply_visitor(ev, ctl_ast);
+	bool fres = (res & fdd_ithvar(0, 0)) != bddfalse;
+	bdd_done();
+
+	return fres;
+}
+
+TEST(CTLEval, very_simple) {
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","a"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","b"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","c"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","not(a)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","not(c)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","and(a,b)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","or(a,c)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","eu(a,not(c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","ax(a)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","ax(and(b,c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","ex(c)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","au(a,b)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","au(ex(c),au(b,c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","and(a,or(b,c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","implies(a,b)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","au(a,implies(b,c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","eg(a)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","ag(a)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","ef(b)"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/very_simple","af(c)"));
+}
+
+TEST(CTLEval, simple) {
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "a"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "b"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "not(c)"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "and(and(a,b),not(c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/simple", "ex(and(and(b,a),c))"));
+	EXPECT_FALSE(ctl_eval("tests/kripke/simple", "ax(and(and(a,b),c))"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "implies(a,b)"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "af(b)"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "ef(b)"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "eu(b,not(c))"));
+	EXPECT_TRUE(ctl_eval("tests/kripke/simple", "au(b,not(c))"));
+}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.