2 files changed, 53 insertions, 292 deletions

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql
deleted file mode 100644
index 58f66fe2..00000000
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/mutated/mutated.vql
+++ /dev/null
@@ -1,270 +0,0 @@
-package hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated

-

-import epackage "hu.bme.mit.inf.yakindumm"

-

-/////////

-// Entry

-/////////

-

-pattern entryInRegion_M0(r1 : Region, e1 : Entry) {

-        Region.vertices(r1, e1);

-}

-pattern entryInRegion_M1(r1 : Region, e1) {

-        Region.vertices(r1, e1);

-}

-pattern entryInRegion_M2(r1 : Region, e1: Entry) {

-        // For positive constraint

-        Region(r1);Entry(e1);

-}

-

-

-//@Constraint(severity="error", message="error", key = {r1})

-pattern noEntryInRegion_M0(r1 : Region) {

-        neg find entryInRegion_M0(r1, _);

-}

-pattern noEntryInRegion_M1(r1 : Region) {

-        neg find entryInRegion_M1(r1, _);

-}

-pattern noEntryInRegion_M2(r1 : Region) {

-        neg find entryInRegion_M2(r1, _);

-}

-pattern noEntryInRegion_M3(r1 : Region) {

-        find entryInRegion_M0(r1, _);

-}

-pattern noEntryInRegion_M4(r1 : Region) {

-        find entryInRegion_M1(r1, _);

-}

-pattern noEntryInRegion_M5(r1 : Region) {

-        find entryInRegion_M2(r1, _);

-}

-

-//@Constraint(severity="error", message="error", key = {r})

-pattern multipleEntryInRegion_M0(r : Region) {

-        find entryInRegion_M0(r, e1);

-        find entryInRegion_M0(r, e2);

-        e1 != e2;

-}

-pattern multipleEntryInRegion_M1(r : Region) {

-        find entryInRegion_M1(r, e1);

-        find entryInRegion_M0(r, e2);

-        e1 != e2;

-}

-pattern multipleEntryInRegion_M2(r : Region) {

-        find entryInRegion_M2(r, e1);

-        find entryInRegion_M0(r, e2);

-        e1 != e2;

-}

-pattern multipleEntryInRegion_M3(r : Region) {

-        find entryInRegion_M0(r, e1);

-        find entryInRegion_M1(r, e2);

-        e1 != e2;

-}

-pattern multipleEntryInRegion_M4(r : Region) {

-        find entryInRegion_M2(r, e1);

-        find entryInRegion_M2(r, e2);

-        e1 != e2;

-}

-pattern multipleEntryInRegion_M5(r : Region) {

-        find entryInRegion_M0(r, e1);

-        find entryInRegion_M0(r, e2);

-}

-

-

-pattern transition_M0(t : Transition, src : Vertex, trg : Vertex) {

-        Transition.source(t, src);

-        Transition.target(t, trg);

-}

-pattern transition_M1(t : Transition, src : Vertex, trg : Vertex) {

-        Transition.source(t, src);

-        Vertex(trg);

-}

-pattern transition_M2(t : Transition, src : Vertex, trg : Vertex) {

-        Vertex(src);

-        Transition.target(t, trg);

-}

-pattern transition_M3(t : Transition, src : Vertex, trg : Vertex) {

-        Transition.source(t_x, src);

-        Transition.target(t, trg);

-}

-pattern transition_M4(t : Transition, src : Vertex, trg : Vertex) {

-        Transition.source(t, src);

-        Transition.target(t_x, trg);

-}

-

-//@Constraint(severity="error", message="error", key = {e})

-pattern incomingToEntry_M0(t : Transition, e : Entry) {

-        find transition_M0(t, _, e);

-}

-pattern incomingToEntry_1(t : Transition, e) {

-        find transition_M0(t, _, e);

-}

-pattern incomingToEntry_2(t : Transition, e : Entry) {

-        find transition_M1(t, _, e);

-}

-pattern incomingToEntry_3(t : Transition, e : Entry) {

-        find transition_M2(t, _, e);

-}

-pattern incomingToEntry_4(t : Transition, e : Entry) {

-        find transition_M3(t, _, e);

-}

-pattern incomingToEntry_5(t : Transition, e : Entry) {

-        find transition_M4(t, _, e);

-}

-

-pattern noOutgoingTransitionFromEntry_M0(e : Entry) {

-        neg find transition_M0(_, e, _);

-}

-

-pattern noOutgoingTransitionFromEntry_M1(e) {

-        Vertex(e);

-        neg find transition_M0(_, e, _);

-}

-pattern noOutgoingTransitionFromEntry_M2(e : Entry) {

-        neg find transition_M1(_, e, _);

-}

-pattern noOutgoingTransitionFromEntry_M3(e : Entry) {

-        neg find transition_M2(_, e, _);

-}

-pattern noOutgoingTransitionFromEntry_M4(e : Entry) {

-        neg find transition_M3(_, e, _);

-}

-pattern noOutgoingTransitionFromEntry_M5(e : Entry) {

-        neg find transition_M4(_, e, _);

-}

-

-

-//@Constraint(severity="error", message="error", key = {e})

-pattern multipleTransitionFromEntry_M0(e : Entry, t1 : Transition, t2: Transition) {

-        Entry.outgoingTransitions(e,t1);

-        Entry.outgoingTransitions(e,t2);

-        t1!=t2;

-}

-pattern multipleTransitionFromEntry_M1(e, t1 : Transition, t2: Transition) {

-        Entry.outgoingTransitions(e,t1);

-        Entry.outgoingTransitions(e,t2);

-        t1!=t2;

-}

-pattern multipleTransitionFromEntry_M2(e : Entry, t1 : Transition, t2: Transition) {

-        Transition(t1);

-        Entry.outgoingTransitions(e,t2);

-        t1!=t2;

-}

-pattern multipleTransitionFromEntry_M3(e : Entry, t1 : Transition, t2: Transition) {

-        Entry.outgoingTransitions(e,t1);

-        Transition(t2);

-        t1!=t2;

-}

-pattern multipleTransitionFromEntry_M4(e : Entry, t1 : Transition, t2: Transition) {

-        Entry.outgoingTransitions(e,t1);

-        Entry.outgoingTransitions(e,t2);

-}

-

-/////////

-// Exit

-/////////

-

-//@Constraint(severity="error", message="error", key = {e})

-pattern outgoingFromExit_M0(t : Transition, e : Exit) {

-        Exit.outgoingTransitions(e,t);

-}

-pattern outgoingFromExit_M1(t : Transition, e) {

-        Vertex.outgoingTransitions(e,t);

-}

-pattern outgoingFromExit_M2(t : Transition, e : Exit) {

-        Transition(t);

-        Exit(e);

-}

-

-/////////

-// Final

-/////////

-

-//@Constraint(severity="error", message="error", key = {f})

-pattern outgoingFromFinal_M0(t : Transition, f : FinalState) {

-        FinalState.outgoingTransitions(f,t);

-}

-pattern outgoingFromFinal_M1(t : Transition, f) {

-        Vertex.outgoingTransitions(f,t);

-}

-pattern outgoingFromFinal_M2(t : Transition, f : FinalState) {

-        Transition(t);

-        FinalState(f);

-}

-

-/////////

-// State vs Region

-/////////

-

-//@Constraint(severity="error", message="error", key = {region})

-pattern noStateInRegion_M0(region: Region) {

-        neg find StateInRegion_M0(region,_);

-}

-pattern noStateInRegion_M1(region: Region) {

-        neg find StateInRegion_M1(region,_);

-}

-pattern noStateInRegion_M2(region: Region) {

-        neg find StateInRegion_M2(region,_);

-}

-pattern noStateInRegion_M3(region: Region) {

-        find StateInRegion_M0(region,_);

-}

-

-pattern StateInRegion_M0(region: Region, state: State) {

-        Region.vertices(region,state);

-}

-pattern StateInRegion_M1(region: Region, state) {

-        Region.vertices(region,state);

-}

-pattern StateInRegion_M2(region: Region, state:State) {

-        Region(region);State(state);

-}

-

-/////////

-// Choice

-/////////

-

-@Constraint(severity="error", message="error", key = {c})

-pattern choiceHasNoOutgoing_M0(c : Choice) {

-        neg find transition_M0(_, c, _);

-}

-pattern choiceHasNoOutgoing_M1(c:Vertex) {

-        neg find transition_M0(_, c, _);

-}

-pattern choiceHasNoOutgoing_M2(c : Choice) {

-        neg find transition_M1(_, c, _);

-}

-pattern choiceHasNoOutgoing_M3(c : Choice) {

-        neg find transition_M2(_, c, _);

-}

-pattern choiceHasNoOutgoing_M4(c : Choice) {

-        neg find transition_M3(_, c, _);

-}

-pattern choiceHasNoOutgoing_M5(c : Choice) {

-        neg find transition_M4(_, c, _);

-}

-pattern choiceHasNoOutgoing_M6(c : Choice) {

-        find transition_M0(_, c, _);

-}

-

-@Constraint(severity="error", message="error", key = {c})

-pattern choiceHasNoIncoming_M0(c: Choice) {

-        neg find transition_M0(_, _, c);

-}

-pattern choiceHasNoIncoming_M1(c:Vertex) {

-        neg find transition_M0(_, _, c);

-}

-pattern choiceHasNoIncoming_M2(c: Choice) {

-        neg find transition_M1(_, _, c);

-}

-pattern choiceHasNoIncoming_M3(c: Choice) {

-        neg find transition_M2(_, _, c);

-}

-pattern choiceHasNoIncoming_M4(c: Choice) {

-        neg find transition_M3(_, _, c);

-}

-pattern choiceHasNoIncoming_M5(c: Choice) {

-        neg find transition_M4(_, _, c);

-}

-pattern choiceHasNoIncoming_M6(c: Choice) {

-        find transition_M0(_, _, c);

-}

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
index f4bfa3c1..49fb5b2f 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
@@ -22,19 +22,33 @@ pattern multipleEntryInRegion(r : Region) {
         e1 != e2;

 }

 

+@Constraint(severity="error", message="error", key = {sct})

+pattern unsat_multipleEntryInRegion(sct : Statechart) {

+        Statechart(sct);

+        neg find multipleEntryInRegion(_);

+}

+

 pattern transition(t : Transition, src : Vertex, trg : Vertex) {

         Transition.source(t, src);

         Transition.target(t, trg);

 }

 

+pattern transitionFrom(t : Transition, src : Vertex) {

+        Transition.source(t, src);

+}

+

+pattern transitionTo(t : Transition, trg : Vertex) {

+        Transition.target(t, trg);

+}

+

 @Constraint(severity="error", message="error", key = {e})

 pattern incomingToEntry(t : Transition, e : Entry) {

-        find transition(t, _, e);

+        find transitionTo(t, e);

 }

 

 @Constraint(severity="error", message="error", key = {e})

 pattern noOutgoingTransitionFromEntry(e : Entry) {

-        neg find transition(_, e, _);

+        neg find transitionFrom(_, e);

 }

 

 @Constraint(severity="error", message="error", key = {e})

@@ -80,12 +94,12 @@ pattern StateInRegion(region: Region, state: State) {
 

 @Constraint(severity="error", message="error", key = {c})

 pattern choiceHasNoOutgoing(c : Choice) {

-        neg find transition(_, c, _);

+        neg find transitionFrom(_, c);

 }

 

 @Constraint(severity="error", message="error", key = {c})

 pattern choiceHasNoIncoming(c: Choice) {

-        neg find transition(_, _, c);

+        neg find transitionTo(_, c);

 }

 

 /////////

@@ -94,27 +108,33 @@ pattern choiceHasNoIncoming(c: Choice) {
 

 @Constraint(severity="error", message="error", key = {s})

 pattern synchHasNoOutgoing(s : Synchronization) {

-        neg find transition(_, s, _);

+        neg find transitionFrom(_, s);

 }

 

 @Constraint(severity="error", message="error", key = {s})

 pattern synchHasNoIncoming(s : Synchronization) {

-        neg find transition(_, _, s);

+        neg find transitionTo(_, 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);

+pattern SynchronizedIncomingInSameRegion(s : Synchronization, t1 : Transition, t2 : Transition) {

+        find SynchronizedIncomingInSameRegionHelper1(r, s, t1);

+        find SynchronizedIncomingInSameRegionHelper1(r, s, t2);

         t1!=t2;

-        Region.vertices(r, v1);

-        Region.vertices(r, v2);

 } or {

-        find transition(t1, s, v1);

-        find transition(t2, s, v2);

+        find SynchronizedIncomingInSameRegionHelper2(r, s, t1);

+        find SynchronizedIncomingInSameRegionHelper2(r, s, t2);

         t1!=t2;

+}

+

+pattern SynchronizedIncomingInSameRegionHelper1(r : Region, s : Synchronization, t1 : Transition) {

+        find transition(t1, v1, s);

+        Region.vertices(r, v1);

+}

+

+pattern SynchronizedIncomingInSameRegionHelper2(r : Region, s : Synchronization, t1 : Transition) {

+        find transition(t1, s, v1);

         Region.vertices(r, v1);

-        Region.vertices(r, v2);

 }

 

 @Constraint(severity="error", message="error", key = {s})

@@ -136,18 +156,24 @@ pattern hasMultipleIncomingTrainsition(v : Synchronization) {
 }

 

 @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);

+pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, r1 : CompositeElement, r2 : CompositeElement) {

+        find SynchronizedRegionsAreNotSiblingsHelper1(s, r1);

+        find SynchronizedRegionsAreNotSiblingsHelper1(s, r2);

         r1 != r2;

 } or {

+        find SynchronizedRegionsAreNotSiblingsHelper2(s, r1);

+        find SynchronizedRegionsAreNotSiblingsHelper2(s, r2);

+        r1 != r2;

+}

+

+pattern SynchronizedRegionsAreNotSiblingsHelper1(s : Synchronization, r1 : CompositeElement) {

         find transition(_, s, v1);

-        find transition(_, s, v2);

         CompositeElement.regions.vertices(r1, v1);

-        CompositeElement.regions.vertices(r2, v2);

-        r1 != r2;

+}

+

+pattern SynchronizedRegionsAreNotSiblingsHelper2(s : Synchronization, r1 : CompositeElement) {

+        find transition(_, v1, s);

+        CompositeElement.regions.vertices(r1, v1);

 }

 

 ///////////////////////////////

@@ -177,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve
         neg find hasMultipleRegions(c);

 }

 

+//@Constraint(severity="error", message="error", key = {sct})

+//pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) {

+//      Statechart(sct);

+//      neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _);

+//}

 

 pattern hasMultipleRegions(composite: CompositeElement) {

         CompositeElement.regions(composite,region1);