| package org.eclipse.emf.henshin.sam.invcheck.filter; |
| |
| import java.util.HashSet; |
| import java.util.Map; |
| import java.util.Set; |
| |
| import org.eclipse.core.runtime.Assert; |
| import org.eclipse.emf.ecore.EObject; |
| import org.eclipse.emf.henshin.sam.invcheck.InvariantCheckerPlugin; |
| import org.eclipse.emf.henshin.sam.invcheck.InvariantCheckerUtil; |
| import org.eclipse.emf.henshin.sam.invcheck.adapter.SamGraphInvCheckGraphAdapter; |
| import org.eclipse.emf.henshin.sam.invcheck.algorithm.ContextGenerator; |
| import org.eclipse.emf.henshin.sam.invcheck.algorithm.NACTranslator; |
| import org.eclipse.emf.henshin.sam.invcheck.nac.NegativeApplicationCondition; |
| import org.eclipse.emf.henshin.sam.model.samannotation.Annotation; |
| import org.eclipse.emf.henshin.sam.model.samgraph.Edge; |
| import org.eclipse.emf.henshin.sam.model.samgraph.Graph; |
| import org.eclipse.emf.henshin.sam.model.samgraph.Node; |
| import org.eclipse.emf.henshin.sam.model.samgraph.SamgraphPackage; |
| import org.eclipse.emf.henshin.sam.model.samgraphcondition.GraphCondition; |
| import org.eclipse.emf.henshin.sam.model.samgraphcondition.LogicalGCCoupling; |
| import org.eclipse.emf.henshin.sam.model.samgraphcondition.NegatedCondition; |
| import org.eclipse.emf.henshin.sam.model.samgraphcondition.Quantification; |
| import org.eclipse.emf.henshin.sam.model.samgraphcondition.SamgraphconditionPackage; |
| import org.eclipse.emf.henshin.sam.model.samrules.GTS; |
| import org.eclipse.emf.henshin.sam.model.samrules.RuleGraph; |
| import org.eclipse.emf.henshin.sam.model.samrules.SamrulesPackage; |
| import org.eclipse.emf.henshin.sam.model.samtrace.Match; |
| import org.eclipse.emf.henshin.sam.model.samtrace.SamtraceFactory; |
| import org.eclipse.emf.henshin.sam.model.samtypegraph.TypeGraphCondition; |
| import org.eclipse.emf.henshin.sam.paf.FilterSkeleton; |
| import org.eclipse.emf.henshin.sam.paf.annotation.ResultDictEntry; |
| |
| public class GeneralContextFilter extends FilterSkeleton<GraphVerificationData, GraphVerificationData> { |
| |
| private ContextGenerator prover; |
| |
| private NACTranslator nacT; |
| |
| @ResultDictEntry(entryName = "discarded") |
| private int discarded = 0; |
| |
| @ResultDictEntry(entryName = "passed") |
| private int passed = 0; |
| |
| private Set<RuleGraph> constraints; |
| private Set<Graph> resConstraints; |
| |
| public void produce() { |
| try { |
| RuleGraph sgp; |
| if (SamrulesPackage.eINSTANCE.getRuleGraph().isSuperTypeOf(this.currentInput.sourceGraph.eClass()) |
| && ((RuleGraph) this.currentInput.sourceGraph).getCondition() != null) { |
| sgp = (RuleGraph) this.currentInput.sourceGraph; |
| } else { |
| this.defaultOutputPipe.queue(this.currentInput); |
| passed++; |
| return; |
| } |
| Match newSGPMatch = InvariantCheckerUtil.copyAsRuleGraph(sgp); |
| RuleGraph newSGP = null; |
| for (Map.Entry<Node, Node> entry : newSGPMatch.getNodeMatching()) { |
| if (entry.getValue() != null) { |
| newSGP = (RuleGraph) entry.getValue().eContainer(); |
| } |
| } |
| Match initialMatching = SamtraceFactory.eINSTANCE.createMatch(); |
| boolean partial = true; |
| for (NegativeApplicationCondition nac : SamGraphInvCheckGraphAdapter.getInstance(sgp).getNacs()) { |
| if (nac.getAnnotations().isEmpty()) { |
| partial = false; |
| } |
| for (Annotation ann : nac.getAnnotations()) { |
| if (ann.getSource().equals(InvariantCheckerPlugin.NAC_BOUND_ITEM)) { |
| if (SamgraphPackage.eINSTANCE.getNode().isSuperTypeOf(ann.getTarget().eClass())) { |
| Node n = (Node) ann.getTarget(); |
| if (!initialMatching.getNodeMatching().containsKey(n)) { |
| initialMatching.getNodeMatching().put(n, newSGPMatch.getNodeMatching().get(n)); |
| } |
| } else if (SamgraphPackage.eINSTANCE.getEdge().isSuperTypeOf(ann.getTarget().eClass())) { |
| Edge e = (Edge) ann.getTarget(); |
| if (!initialMatching.getEdgeMatching().containsKey(e)) { |
| initialMatching.getEdgeMatching().put(e, newSGPMatch.getEdgeMatching().get(e)); |
| } |
| } |
| } |
| } |
| } |
| RuleGraph finalSGP = null; |
| nacT.setPattern(sgp); |
| nacT.setMergedGraph(newSGP); |
| nacT.setInitialMatching(initialMatching); |
| nacT.reset(); |
| // partial = false; |
| if (partial) { |
| finalSGP = nacT.translate(); |
| if (finalSGP == null) { |
| throw new RuntimeException("problem in context generation"); |
| } |
| } else { |
| finalSGP = sgp; |
| } |
| prover.setProofGoal(finalSGP); |
| |
| if (prover.proof()) { |
| // System.out.println("proven"); |
| discarded++; |
| return; |
| } else { |
| // System.out.println("not proven"); |
| passed++; |
| this.defaultOutputPipe.queue(this.currentInput); |
| } |
| |
| } catch (InterruptedException ie) { |
| this.running = false; |
| } |
| |
| } |
| |
| @Override |
| protected void initData() { |
| this.prover = new ContextGenerator(); |
| |
| Assert.isNotNull(this.getFilterDispatcher()); |
| Assert.isNotNull(this.getFilterDispatcher().getFilterInput()); |
| |
| final EObject theEObject = this.getFilterDispatcher().getFilterInput(); |
| Assert.isTrue(theEObject.eClass() == SamrulesPackage.eINSTANCE.getGTS()); |
| final GTS theGTS = (GTS) theEObject; |
| this.constraints = new HashSet<RuleGraph>(); |
| this.resConstraints = new HashSet<Graph>(); |
| |
| for (TypeGraphCondition g : theGTS.getTypes().get(0).getConditions()) { |
| if (g.eClass() == SamgraphconditionPackage.eINSTANCE.getNegatedCondition()) { |
| NegatedCondition nc = (NegatedCondition) g; |
| if (nc.getOperand().eClass() == SamgraphconditionPackage.eINSTANCE.getQuantification()) { |
| Quantification q = (Quantification) nc.getOperand(); |
| Graph graph = q.getContext(); |
| if (/* !nc.getName().equals("noFire-noSend") && */SamrulesPackage.eINSTANCE.getRuleGraph() |
| .isSuperTypeOf(graph.eClass()) && ((RuleGraph) graph).getCondition() != null) { |
| this.constraints.add((RuleGraph) graph); |
| } else { |
| this.resConstraints.add(graph); |
| } |
| } |
| } else if (g.eClass() == SamgraphconditionPackage.eINSTANCE.getLogicalGCCoupling()) { |
| LogicalGCCoupling lgc = (LogicalGCCoupling) g; |
| for (GraphCondition gc : lgc.getOperands()) { |
| if (gc.eClass() == SamgraphconditionPackage.eINSTANCE.getNegatedCondition()) { |
| NegatedCondition neg = (NegatedCondition) gc; |
| if (neg.getOperand().eClass() == SamgraphconditionPackage.eINSTANCE.getQuantification()) { |
| Quantification q = (Quantification) neg.getOperand(); |
| Graph graph = q.getContext(); |
| if (/* !neg.getName().equals("noFire-noSend") && */SamrulesPackage.eINSTANCE.getRuleGraph() |
| .isSuperTypeOf(graph.eClass()) && ((RuleGraph) graph).getCondition() != null) { |
| this.constraints.add((RuleGraph) graph); |
| } else { |
| this.resConstraints.add(graph); |
| } |
| } |
| } |
| } |
| } |
| } |
| prover.setGenerationConstraints(this.constraints); |
| prover.setRestrictingConstraints(this.resConstraints); |
| |
| } |
| |
| @Override |
| protected void initFilter() { |
| super.initFilter(); |
| this.filterName = "GeneralContexetFilter"; |
| this.nacT = new NACTranslator(); |
| } |
| } |