diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql')
-rw-r--r-- | Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | 75 |
1 files changed, 53 insertions, 22 deletions
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) { | |||
22 | e1 != e2; | 22 | e1 != e2; |
23 | } | 23 | } |
24 | 24 | ||
25 | @Constraint(severity="error", message="error", key = {sct}) | ||
26 | pattern unsat_multipleEntryInRegion(sct : Statechart) { | ||
27 | Statechart(sct); | ||
28 | neg find multipleEntryInRegion(_); | ||
29 | } | ||
30 | |||
25 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { | 31 | pattern transition(t : Transition, src : Vertex, trg : Vertex) { |
26 | Transition.source(t, src); | 32 | Transition.source(t, src); |
27 | Transition.target(t, trg); | 33 | Transition.target(t, trg); |
28 | } | 34 | } |
29 | 35 | ||
36 | pattern transitionFrom(t : Transition, src : Vertex) { | ||
37 | Transition.source(t, src); | ||
38 | } | ||
39 | |||
40 | pattern transitionTo(t : Transition, trg : Vertex) { | ||
41 | Transition.target(t, trg); | ||
42 | } | ||
43 | |||
30 | @Constraint(severity="error", message="error", key = {e}) | 44 | @Constraint(severity="error", message="error", key = {e}) |
31 | pattern incomingToEntry(t : Transition, e : Entry) { | 45 | pattern incomingToEntry(t : Transition, e : Entry) { |
32 | find transition(t, _, e); | 46 | find transitionTo(t, e); |
33 | } | 47 | } |
34 | 48 | ||
35 | @Constraint(severity="error", message="error", key = {e}) | 49 | @Constraint(severity="error", message="error", key = {e}) |
36 | pattern noOutgoingTransitionFromEntry(e : Entry) { | 50 | pattern noOutgoingTransitionFromEntry(e : Entry) { |
37 | neg find transition(_, e, _); | 51 | neg find transitionFrom(_, e); |
38 | } | 52 | } |
39 | 53 | ||
40 | @Constraint(severity="error", message="error", key = {e}) | 54 | @Constraint(severity="error", message="error", key = {e}) |
@@ -80,12 +94,12 @@ pattern StateInRegion(region: Region, state: State) { | |||
80 | 94 | ||
81 | @Constraint(severity="error", message="error", key = {c}) | 95 | @Constraint(severity="error", message="error", key = {c}) |
82 | pattern choiceHasNoOutgoing(c : Choice) { | 96 | pattern choiceHasNoOutgoing(c : Choice) { |
83 | neg find transition(_, c, _); | 97 | neg find transitionFrom(_, c); |
84 | } | 98 | } |
85 | 99 | ||
86 | @Constraint(severity="error", message="error", key = {c}) | 100 | @Constraint(severity="error", message="error", key = {c}) |
87 | pattern choiceHasNoIncoming(c: Choice) { | 101 | pattern choiceHasNoIncoming(c: Choice) { |
88 | neg find transition(_, _, c); | 102 | neg find transitionTo(_, c); |
89 | } | 103 | } |
90 | 104 | ||
91 | ///////// | 105 | ///////// |
@@ -94,27 +108,33 @@ pattern choiceHasNoIncoming(c: Choice) { | |||
94 | 108 | ||
95 | @Constraint(severity="error", message="error", key = {s}) | 109 | @Constraint(severity="error", message="error", key = {s}) |
96 | pattern synchHasNoOutgoing(s : Synchronization) { | 110 | pattern synchHasNoOutgoing(s : Synchronization) { |
97 | neg find transition(_, s, _); | 111 | neg find transitionFrom(_, s); |
98 | } | 112 | } |
99 | 113 | ||
100 | @Constraint(severity="error", message="error", key = {s}) | 114 | @Constraint(severity="error", message="error", key = {s}) |
101 | pattern synchHasNoIncoming(s : Synchronization) { | 115 | pattern synchHasNoIncoming(s : Synchronization) { |
102 | neg find transition(_, _, s); | 116 | neg find transitionTo(_, s); |
103 | } | 117 | } |
104 | 118 | ||
105 | @Constraint(severity="error", message="error", key = {s}) | 119 | @Constraint(severity="error", message="error", key = {s}) |
106 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 120 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, t1 : Transition, t2 : Transition) { |
107 | find transition(t1, v1, s); | 121 | find SynchronizedIncomingInSameRegionHelper1(r, s, t1); |
108 | find transition(t2, v2, s); | 122 | find SynchronizedIncomingInSameRegionHelper1(r, s, t2); |
109 | t1!=t2; | 123 | t1!=t2; |
110 | Region.vertices(r, v1); | ||
111 | Region.vertices(r, v2); | ||
112 | } or { | 124 | } or { |
113 | find transition(t1, s, v1); | 125 | find SynchronizedIncomingInSameRegionHelper2(r, s, t1); |
114 | find transition(t2, s, v2); | 126 | find SynchronizedIncomingInSameRegionHelper2(r, s, t2); |
115 | t1!=t2; | 127 | t1!=t2; |
128 | } | ||
129 | |||
130 | pattern SynchronizedIncomingInSameRegionHelper1(r : Region, s : Synchronization, t1 : Transition) { | ||
131 | find transition(t1, v1, s); | ||
132 | Region.vertices(r, v1); | ||
133 | } | ||
134 | |||
135 | pattern SynchronizedIncomingInSameRegionHelper2(r : Region, s : Synchronization, t1 : Transition) { | ||
136 | find transition(t1, s, v1); | ||
116 | Region.vertices(r, v1); | 137 | Region.vertices(r, v1); |
117 | Region.vertices(r, v2); | ||
118 | } | 138 | } |
119 | 139 | ||
120 | @Constraint(severity="error", message="error", key = {s}) | 140 | @Constraint(severity="error", message="error", key = {s}) |
@@ -136,18 +156,24 @@ pattern hasMultipleIncomingTrainsition(v : Synchronization) { | |||
136 | } | 156 | } |
137 | 157 | ||
138 | @Constraint(severity="error", message="error", key = {s}) | 158 | @Constraint(severity="error", message="error", key = {s}) |
139 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 159 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, r1 : CompositeElement, r2 : CompositeElement) { |
140 | find transition(_, v1, s); | 160 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r1); |
141 | find transition(_, v2, s); | 161 | find SynchronizedRegionsAreNotSiblingsHelper1(s, r2); |
142 | CompositeElement.regions.vertices(r1, v1); | ||
143 | CompositeElement.regions.vertices(r2, v2); | ||
144 | r1 != r2; | 162 | r1 != r2; |
145 | } or { | 163 | } or { |
164 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r1); | ||
165 | find SynchronizedRegionsAreNotSiblingsHelper2(s, r2); | ||
166 | r1 != r2; | ||
167 | } | ||
168 | |||
169 | pattern SynchronizedRegionsAreNotSiblingsHelper1(s : Synchronization, r1 : CompositeElement) { | ||
146 | find transition(_, s, v1); | 170 | find transition(_, s, v1); |
147 | find transition(_, s, v2); | ||
148 | CompositeElement.regions.vertices(r1, v1); | 171 | CompositeElement.regions.vertices(r1, v1); |
149 | CompositeElement.regions.vertices(r2, v2); | 172 | } |
150 | r1 != r2; | 173 | |
174 | pattern SynchronizedRegionsAreNotSiblingsHelper2(s : Synchronization, r1 : CompositeElement) { | ||
175 | find transition(_, v1, s); | ||
176 | CompositeElement.regions.vertices(r1, v1); | ||
151 | } | 177 | } |
152 | 178 | ||
153 | /////////////////////////////// | 179 | /////////////////////////////// |
@@ -177,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve | |||
177 | neg find hasMultipleRegions(c); | 203 | neg find hasMultipleRegions(c); |
178 | } | 204 | } |
179 | 205 | ||
206 | //@Constraint(severity="error", message="error", key = {sct}) | ||
207 | //pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) { | ||
208 | // Statechart(sct); | ||
209 | // neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _); | ||
210 | //} | ||
180 | 211 | ||
181 | pattern hasMultipleRegions(composite: CompositeElement) { | 212 | pattern hasMultipleRegions(composite: CompositeElement) { |
182 | CompositeElement.regions(composite,region1); | 213 | CompositeElement.regions(composite,region1); |