1 files changed, 227 insertions, 0 deletions

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakinduPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakinduPatterns.vql
new file mode 100644
index 00000000..f52113ca
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakinduPatterns.vql
@@ -0,0 +1,227 @@
+package ca.mcgill.ecse.dslreasoner.yakindu.queries
+
+import epackage "hu.bme.mit.inf.yakindumm"
+
+/////////
+// Entry
+/////////
+
+pattern entryInRegion(r1 : Region, e1 : Entry) {
+        Region.vertices(r1, e1);
+}
+
+@Constraint(severity="error", message="error", key = {r1})
+pattern noEntryInRegion(r1 : Region) {
+        neg find entryInRegion(r1, _);
+}
+
+@Constraint(severity="error", message="error", key = {r})
+pattern multipleEntryInRegion(r : Region) {
+        find entryInRegion(r, e1);
+        find entryInRegion(r, e2);
+        e1 != e2;
+}
+
+pattern transition(t : Transition, src : Vertex, trg : Vertex) {
+        Transition.source(t, src);
+        Transition.target(t, trg);
+}
+
+@Constraint(severity="error", message="error", key = {e})
+pattern incomingToEntry(t : Transition, e : Entry) {
+        find transition(t, _, e);
+}
+
+@Constraint(severity="error", message="error", key = {e})
+pattern noOutgoingTransitionFromEntry(e : Entry) {
+        neg find transition(_, e, _);
+}
+
+@Constraint(severity="error", message="error", key = {e})
+pattern multipleTransitionFromEntry(e : Entry, t1 : Transition, t2: Transition) {
+        Entry.outgoingTransitions(e,t1);
+        Entry.outgoingTransitions(e,t2);
+        t1!=t2;
+}
+
+/////////
+// Exit
+/////////
+
+@Constraint(severity="error", message="error", key = {e})
+pattern outgoingFromExit(t : Transition, e : Exit) {
+        Exit.outgoingTransitions(e,t);
+}
+
+/////////
+// Final
+/////////
+
+@Constraint(severity="error", message="error", key = {f})
+pattern outgoingFromFinal(t : Transition, f : FinalState) {
+        FinalState.outgoingTransitions(f,t);
+}
+
+/////////
+// State vs Region
+/////////
+
+@Constraint(severity="error", message="error", key = {region})
+pattern noStateInRegion(region: Region) {
+        neg find StateInRegion(region,_);
+}
+pattern StateInRegion(region: Region, state: State) {
+        Region.vertices(region,state);
+}
+
+/////////
+// Choice
+/////////
+
+@Constraint(severity="error", message="error", key = {c})
+pattern choiceHasNoOutgoing(c : Choice) {
+        neg find transition(_, c, _);
+}
+
+@Constraint(severity="error", message="error", key = {c})
+pattern choiceHasNoIncoming(c: Choice) {
+        neg find transition(_, _, c);
+}
+
+/////////
+// Synchronization
+/////////
+
+@Constraint(severity="error", message="error", key = {s})
+pattern synchHasNoOutgoing(s : Synchronization) {
+        neg find transition(_, s, _);
+}
+
+@Constraint(severity="error", message="error", key = {s})
+pattern synchHasNoIncoming(s : Synchronization) {
+        neg find transition(_, _, s);
+}
+
+@Constraint(severity="error", message="error", key = {s})
+pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) {
+        find transition(t1, v1, s);
+        find transition(t2, v2, s);
+        t1!=t2;
+        Region.vertices(r, v1);
+        Region.vertices(r, v2);
+} or {
+        find transition(t1, s, v1);
+        find transition(t2, s, v2);
+        t1!=t2;
+        Region.vertices(r, v1);
+        Region.vertices(r, v2);
+}
+
+@Constraint(severity="error", message="error", key = {s})
+pattern notSynchronizingStates(s : Synchronization) {
+        neg find hasMultipleOutgoingTrainsition(s);
+        neg find hasMultipleIncomingTrainsition(s);
+}
+
+pattern hasMultipleOutgoingTrainsition(v : Synchronization) {
+        find transition(_, v, trg1);
+        find transition(_, v, trg2);
+        trg1 != trg2;
+}
+
+pattern hasMultipleIncomingTrainsition(v : Synchronization) {
+        find transition(_, src1, v);
+        find transition(_, src2, v);
+        src1 != src2;
+}
+
+@Constraint(severity="error", message="error", key = {s})
+pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) {
+        find transition(_, v1, s);
+        find transition(_, v2, s);
+        CompositeElement.regions.vertices(r1, v1);
+        CompositeElement.regions.vertices(r2, v2);
+        r1 != r2;
+} or {
+        find transition(_, s, v1);
+        find transition(_, s, v2);
+        CompositeElement.regions.vertices(r1, v1);
+        CompositeElement.regions.vertices(r2, v2);
+        r1 != r2;
+}
+
+///////////////////////////////
+// Extra
+//
+//@Constraint(severity="error", message="error", key = {s})
+//pattern SynchronizedRegionDoesNotHaveParent(s : Synchronization, v : Vertex) {
+//      find transition(_, v, s);
+//      neg find child(_,v);
+//} or {
+//      find transition(_, s, v);
+//      neg find child(_,v);
+//}
+
+pattern child(parent: CompositeElement, child: Vertex) {
+        CompositeElement.regions.vertices(parent, child);
+}
+
+@Constraint(severity="error", message="error", key = {s})
+pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Vertex) {
+        find transition(_, v, s);
+        find child(c,v);
+        neg find hasMultipleRegions(c);
+} or {
+        find transition(_, s, v);
+        find child(c,v);
+        neg find hasMultipleRegions(c);
+}
+
+
+pattern hasMultipleRegions(composite: CompositeElement) {
+        CompositeElement.regions(composite,region1);
+        CompositeElement.regions(composite,region2);
+        region1 != region2;
+}
+
+/**
+ * Simplifying model generation
+ */
+@Constraint(severity="error", message="error", key = {s})
+pattern synchThree(s: Synchronization) {
+        Transition.target(t1,s);
+        Transition.target(t2,s);
+        Transition.target(t3,s);
+        t1!=t2;
+        t2!=t3;
+        t1!=t3;
+} or {
+        Transition.source(t1,s);
+        Transition.source(t2,s);
+        Transition.source(t3,s);
+        t1!=t2;
+        t2!=t3;
+        t1!=t3;
+}
+
+/**
+ * Simplifying model generation
+ */
+@Constraint(severity="error", message="error", key = {s1,s2})
+pattern twoSynch(s1 : Synchronization, s2 : Synchronization) {
+        Synchronization(s1);
+        Synchronization(s2);
+        s1 != s2;
+}
+
+/**
+ * Model generation task: at least one synch
+ */
+@Constraint(severity="error", message="error", key = {s})
+pattern noSynch(s:Statechart) {
+        Statechart(s);
+        neg find synch(_);
+}
+pattern synch(s:Synchronization) {
+        Synchronization(s);
+}
\ No newline at end of file