Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Paper for TTC 2017 - State Elimination Case #40

Open
hoechp opened this issue May 23, 2017 · 1 comment
Open

Paper for TTC 2017 - State Elimination Case #40

hoechp opened this issue May 23, 2017 · 1 comment

Comments

@hoechp
Copy link
Contributor

hoechp commented May 23, 2017

A little bit of info, that could be helpful:
20170523_084613
20170523_084618
20170523_084623
20170523_084739
20170523_084743
20170523_084745
20170523_084747
20170523_084750
20170523_084756

@hoechp
Copy link
Contributor Author

hoechp commented May 23, 2017

Here's the first 19 GTR (if you want to elaborate on the GTR syntax or something):

private static PatternGraph getNewInitialPattern() { // #1.1
	// gtr for new initial state:
	PatternGraph gtr = new PatternGraph("new initial state");
	PatternNode initialNode = new PatternNode("#{initial}").addPatternAttribute(new PatternAttribute().setAction("-").setName("initial"));
	PatternNode newInitialNode = new PatternNode().setAction("+").addPatternAttribute(new PatternAttribute().setAction("+").setName("newInitial").setValue(true));
	PatternNode noExistingNewInitialNode = new PatternNode("#{newInitial}").setAction("!=");
	gtr.addPatternNode(initialNode, newInitialNode, noExistingNewInitialNode);
	newInitialNode.addPatternEdge("+", "e", initialNode);
	return gtr;
}

private static PatternGraph getNewFinalPattern() { // #1.2
	// gtr for new final state:
	PatternGraph gtr = new PatternGraph("new final state");
	PatternNode finalNode = new PatternNode("#{final}").addPatternAttribute(new PatternAttribute().setAction("-").setName("final"));
	PatternNode newFinalNode = new PatternNode().setAction("+").addPatternAttribute(new PatternAttribute().setAction("+").setName("newFinal").setValue(true));
	PatternNode noExistingNewFinalNode = new PatternNode("#{newFinal}").setAction("!=");
	gtr.addPatternNode(finalNode, newFinalNode, noExistingNewFinalNode);
	finalNode.addPatternEdge("+", "e", newFinalNode);
	return gtr;
}

private static PatternGraph getAddToFinalPattern() { // #1.3
	// gtr for adding to new final state:
	PatternGraph gtr = new PatternGraph("adding to the existing new final state");
	PatternNode otherFinalNode = new PatternNode("#{final}").addPatternAttribute(new PatternAttribute().setAction("-").setName("final"));
	PatternNode existingNewFinalNode = new PatternNode("#{newFinal}");
	gtr.addPatternNode(otherFinalNode, existingNewFinalNode);
	otherFinalNode.addPatternEdge("+", "e", existingNewFinalNode);
	return gtr;
}

private static PatternGraph getMergeEdgesPattern() { // #1.4
	// gtr for merging multiple edges between the same two nodes:
	PatternGraph gtr = new PatternGraph("merge multiple labels between the same two nodes");
	PatternNode a = new PatternNode();
	PatternNode b = new PatternNode();
	gtr.addPatternNode(a, b);
	a.addPatternEdge("-", "#{x}, #{y}", b);
	a.addPatternEdge("+", "#{x} + '+' + #{y}", b);
	return gtr;
}

private static PatternGraph getMarkStateForEliminationPattern() { // #2.1
	// gtr for marking a state for elimination
	PatternGraph gtr = new PatternGraph("mark state for elimination");
	PatternNode p = new PatternNode();
	PatternNode k = new PatternNode("!(#{newFinal} || #{newInitial} || #{eliminate})");
	PatternNode q = new PatternNode();
	PatternNode noOtherMarkedOne = new PatternNode("#{eliminate}").setAction("!=");
	k.addPatternAttribute(new PatternAttribute().setAction("+").setName("eliminate").setValue(true));
	gtr.addPatternNode(p, k, q);
	gtr.addPatternNode(noOtherMarkedOne);
	return gtr;
}

private static PatternGraph getMarkWithCurrentPattern() { // #2.2.1
	// gtr for marking the current state for elimination preparation
	PatternGraph gtr = new PatternGraph("mark current working state (p->k->q)");
	PatternNode noAlreadyMarkedAsCurrentState = new PatternNode("#{current}").setAction("!=");
	PatternNode p = new PatternNode("!(#{current}) && !(#{past})").addPatternAttribute(new PatternAttribute().setAction("+").setName("current").setValue(true));
	PatternNode k = new PatternNode("#{eliminate} == 1");
	PatternNode q = new PatternNode();
	gtr.addPatternNode(noAlreadyMarkedAsCurrentState, p, k, q);
	p.addPatternEdge("==", "#{a}", k);
	k.addPatternEdge("==", "#{b}", q);
	return gtr;
}

private static PatternGraph getMarkFallbackWithCurrentPattern() { // #2.2.1
	// gtr for marking the current state for elimination preparation
	PatternGraph gtr = new PatternGraph("mark current working state (p<->k)");
	PatternNode noAlreadyMarkedAsCurrentState = new PatternNode("#{current}").setAction("!=");
	PatternNode p = new PatternNode("!(#{current}) && !(#{past})").addPatternAttribute(new PatternAttribute().setAction("+").setName("current").setValue(true));
	PatternNode k = new PatternNode("#{eliminate} == 1");
	gtr.addPatternNode(noAlreadyMarkedAsCurrentState, p, k);
	p.addPatternEdge("==", "#{a}", k);
	k.addPatternEdge("==", "#{b}", p);
	return gtr;
}

private static PatternGraph getPrepareStateWithPqPkKkKqPattern() { // #2.3.1
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with pq, pk, kk, kq)");
	PatternNode p = new PatternNode("#{current}");
	PatternNode k = new PatternNode("#{eliminate}");
	PatternNode q = new PatternNode("!(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	gtr.addPatternNode(p, k, q);
	/* CASE 1: there's pq, pk, kk and kq */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kq}", q);
	k.addPatternEdge("==", "#{kk}", k);
	p.addPatternEdge("-", "#{pq}", q);
	p.addPatternEdge("+", "'(' + #{pq} + ')+((' + #{pk} + ')(' + #{kk} + ')*(' + #{kq} + '))'", q);
	return gtr;
}

private static PatternGraph getPrepareStateWithPkKkKqPattern() { // #2.3.2
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with just pk, kk, kq)");
	PatternNode p = new PatternNode("#{current}");
	PatternNode k = new PatternNode("#{eliminate}");
	PatternNode q = new PatternNode("!(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	gtr.addPatternNode(p, k, q);
	/* CASE 2: there's just pk, kk and kq */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kk}", k);
	k.addPatternEdge("==", "#{kq}", q);
	p.addPatternEdge("+", "'(' + #{pk} + ')(' + #{kk} + ')*(' + #{kq} + ')'", q);
	return gtr;
}

private static PatternGraph getPrepareStateWithPqPkKqPattern() { // #2.3.3
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with just pq, pk, kq)");
	PatternNode p = new PatternNode("#{current}");
	PatternNode k = new PatternNode("#{eliminate}");
	PatternNode q = new PatternNode("!(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	gtr.addPatternNode(p, k, q);
	/* CASE 3: there's just pq, pk and kq */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kq}", q);
	p.addPatternEdge("-", "#{pq}", q);
	p.addPatternEdge("+", "'(' + #{pq} + ')+((' + #{pk} + ')(' + #{kq} + '))'", q);
	return gtr;
}

private static PatternGraph getPrepareStateWithPkKqPattern() { // #2.3.4
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with just pk, kq)");
	PatternNode p = new PatternNode("#{current}");
	PatternNode k = new PatternNode("#{eliminate}");
	PatternNode q = new PatternNode("!(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	gtr.addPatternNode(p, k, q);
	/* CASE 4: there's just pk and kq */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kq}", q);
	p.addPatternEdge("+", "'(' + #{pk} + ')(' + #{kq} + ')'", q);
	return gtr;
}

private static PatternGraph getPrepareStateWithPpPkKkKpPattern() { // #2.3.5
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with pp, pk, kk, kp)");
	PatternNode p = new PatternNode("#{current} && !(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	PatternNode k = new PatternNode("#{eliminate}");
	gtr.addPatternNode(p, k);
	/* CASE 5: there's pp, pk, kk and kp */
	p.addPatternEdge("-", "#{pp}", p);
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kk}", k);
	k.addPatternEdge("==", "#{kp}", p);
	p.addPatternEdge("+", "'((' + #{pp} + ')*((' + #{pk} + ')(' + #{kk} + ')*(' + #{kp} + '))*)*'", p);
	return gtr;
}

private static PatternGraph getPrepareStateWithPpPkKpPattern() { // #2.3.6
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with just pp, pk, kp)");
	PatternNode p = new PatternNode("#{current} && !(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	PatternNode k = new PatternNode("#{eliminate}");
	gtr.addPatternNode(p, k);
	/* CASE 5: there's pp, pk, kk and kp */
	p.addPatternEdge("-", "#{pp}", p);
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kp}", p);
	p.addPatternEdge("+", "'((' + #{pp} + ')*((' + #{pk} + ')(' + #{kp} + '))*)*'", p);
	return gtr;
}

private static PatternGraph getPrepareStateWithPkKkKpPattern() { // #2.3.7
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("##### prepare elimination of state (with just pk, kk, kp)");
	PatternNode p = new PatternNode("#{current} && !(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	PatternNode k = new PatternNode("#{eliminate}");
	gtr.addPatternNode(p, k);
	/* CASE 5: there's pp, pk, kk and kp */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kk}", k);
	k.addPatternEdge("==", "#{kp}", p);
	p.addPatternEdge("+", "'((' + #{pk} + ')(' + #{kk} + ')*(' + #{kp} + '))*'", p);
	return gtr;
}

private static PatternGraph getPrepareStateWithPkKpPattern() { // #2.3.8
	// gtr for adding new calculated labels
	PatternGraph gtr = new PatternGraph("prepare elimination of state (with just pk, kp)");
	PatternNode p = new PatternNode("#{current} && !(#{used})").addPatternAttribute(new PatternAttribute().setAction("+").setName("used").setValue(true));
	PatternNode k = new PatternNode("#{eliminate}");
	gtr.addPatternNode(p, k);
	/* CASE 5: there's pp, pk, kk and kp */
	p.addPatternEdge("==", "#{pk}", k);
	k.addPatternEdge("==", "#{kp}", p);
	p.addPatternEdge("+", "'((' + #{pk} + ')(' + #{kp} + '))*'", p);
	return gtr;
}

private static PatternGraph getUnmarkCurrentPattern() { // #2.4
	PatternGraph gtr = new PatternGraph("remove mark of current working state");
	PatternNode n = new PatternNode("#{current}");
	n.addPatternAttribute(new PatternAttribute().setAction("-").setName("current"));
	n.addPatternAttribute(new PatternAttribute().setAction("+").setName("past").setValue(true));
	gtr.addPatternNode(n);
	return gtr;
}

private static PatternGraph getRemoveMarksPattern() { // #2.5
	// gtr for removing marks
	PatternGraph gtr = new PatternGraph("remove mark of used state");
	PatternNode n = new PatternNode("#{used}").addPatternAttribute(new PatternAttribute().setAction("-").setName("used"));
	gtr.addPatternNode(n);
	return gtr;
}

private static PatternGraph getEliminateMarkedStatePattern() { // #2.6
	// gtr for eliminating the previously marked state
	PatternGraph gtr = new PatternGraph("eliminate state itself");
	PatternNode k = new PatternNode("#{eliminate}").setAction("-");
	gtr.addPatternNode(k);
	return gtr;
}

private static PatternGraph getUnmarkPastPattern() { // #2.7
	PatternGraph gtr = new PatternGraph("remove mark of past working state");
	PatternNode n = new PatternNode("#{past}");
	n.addPatternAttribute(new PatternAttribute().setAction("-").setName("past"));
	gtr.addPatternNode(n);
	return gtr;
}

By now, there's a 20th GTR - initially I thought there could be only one initial state, but there's at least one file it seems (the one in task-extension1), where there can be multiple ones - so I added a GTR for that, too. Forgot to commit, though - the code is at home right now, where more tests are running through the day, while I'm at work. And see #36 for some of the first test results, that are already available!

I didn't verify each of the results. Though I know the exact solution for like the first one and it was correct - so I'm pretty sure, they're right. Gotta check that evaluation framework, though. If I only had more time... And I'm also trying to keep improving performance and maybe also solve the task-extension2 before time runs out.

Hope this is useful. If I missed out on major info, send me an e-mail!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants