From 3997c2408f192e22f809cd96faa5bc552530289d Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sun, 14 Jun 2020 19:38:40 -0400 Subject: This branch is ready to be merged into master --- .../initialModels/yakindu/yakinduPatterns.vql | 227 +++++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakinduPatterns.vql (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakinduPatterns.vql') 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 -- cgit v1.2.3-54-g00ecf