diff options
author | 2020-11-03 22:52:26 -0500 | |
---|---|---|
committer | 2020-11-03 22:52:26 -0500 | |
commit | 945f487a08b643392a5d5918c631640b9a0e4605 (patch) | |
tree | b537c456e395950ce98daaabb9468c7c17d5a72b /Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph | |
parent | Fix numeric-solver-at-end (diff) | |
download | VIATRA-Generator-945f487a08b643392a5d5918c631640b9a0e4605.tar.gz VIATRA-Generator-945f487a08b643392a5d5918c631640b9a0e4605.tar.zst VIATRA-Generator-945f487a08b643392a5d5918c631640b9a0e4605.zip |
add realistic solver
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph')
3 files changed, 94 insertions, 106 deletions
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF index 73ebb2c7..81ee8677 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF | |||
@@ -10,9 +10,7 @@ Export-Package: hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm, | |||
10 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl, | 10 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl, |
11 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.util, | 11 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.util, |
12 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu, | 12 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu, |
13 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated, | 13 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated |
14 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.util, | ||
15 | hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.util | ||
16 | Require-Bundle: org.eclipse.viatra.query.runtime, | 14 | Require-Bundle: org.eclipse.viatra.query.runtime, |
17 | org.eclipse.core.runtime, | 15 | org.eclipse.core.runtime, |
18 | org.eclipse.emf.ecore;visibility:=reexport, | 16 | org.eclipse.emf.ecore;visibility:=reexport, |
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml index 993ec75d..5fd865dc 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml | |||
@@ -18,18 +18,8 @@ | |||
18 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.StateInRegion"/> | 18 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.StateInRegion"/> |
19 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoOutgoing"/> | 19 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoOutgoing"/> |
20 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoIncoming"/> | 20 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoIncoming"/> |
21 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchHasNoOutgoing"/> | ||
22 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchHasNoIncoming"/> | ||
23 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedIncomingInSameRegion"/> | ||
24 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.notSynchronizingStates"/> | ||
25 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleOutgoingTrainsition"/> | ||
26 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleIncomingTrainsition"/> | ||
27 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedRegionsAreNotSiblings"/> | ||
28 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.child"/> | 21 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.child"/> |
29 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedRegionDoesNotHaveMultipleRegions"/> | ||
30 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleRegions"/> | 22 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleRegions"/> |
31 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchThree"/> | ||
32 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.twoSynch"/> | ||
33 | </group> | 23 | </group> |
34 | </extension> | 24 | </extension> |
35 | <extension id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated" point="org.eclipse.viatra.query.runtime.queryspecification"> | 25 | <extension id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated" point="org.eclipse.viatra.query.runtime.queryspecification"> |
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..69689899 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 | |||
@@ -92,63 +92,63 @@ pattern choiceHasNoIncoming(c: Choice) { | |||
92 | // Synchronization | 92 | // Synchronization |
93 | ///////// | 93 | ///////// |
94 | 94 | ||
95 | @Constraint(severity="error", message="error", key = {s}) | 95 | //@Constraint(severity="error", message="error", key = {s}) |
96 | pattern synchHasNoOutgoing(s : Synchronization) { | 96 | //pattern synchHasNoOutgoing(s : Synchronization) { |
97 | neg find transition(_, s, _); | 97 | // neg find transition(_, s, _); |
98 | } | 98 | //} |
99 | 99 | // | |
100 | @Constraint(severity="error", message="error", key = {s}) | 100 | //@Constraint(severity="error", message="error", key = {s}) |
101 | pattern synchHasNoIncoming(s : Synchronization) { | 101 | //pattern synchHasNoIncoming(s : Synchronization) { |
102 | neg find transition(_, _, s); | 102 | // neg find transition(_, _, s); |
103 | } | 103 | //} |
104 | 104 | // | |
105 | @Constraint(severity="error", message="error", key = {s}) | 105 | //@Constraint(severity="error", message="error", key = {s}) |
106 | pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 106 | //pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) { |
107 | find transition(t1, v1, s); | 107 | // find transition(t1, v1, s); |
108 | find transition(t2, v2, s); | 108 | // find transition(t2, v2, s); |
109 | t1!=t2; | 109 | // t1!=t2; |
110 | Region.vertices(r, v1); | 110 | // Region.vertices(r, v1); |
111 | Region.vertices(r, v2); | 111 | // Region.vertices(r, v2); |
112 | } or { | 112 | //} or { |
113 | find transition(t1, s, v1); | 113 | // find transition(t1, s, v1); |
114 | find transition(t2, s, v2); | 114 | // find transition(t2, s, v2); |
115 | t1!=t2; | 115 | // t1!=t2; |
116 | Region.vertices(r, v1); | 116 | // Region.vertices(r, v1); |
117 | Region.vertices(r, v2); | 117 | // Region.vertices(r, v2); |
118 | } | 118 | //} |
119 | 119 | // | |
120 | @Constraint(severity="error", message="error", key = {s}) | 120 | //@Constraint(severity="error", message="error", key = {s}) |
121 | pattern notSynchronizingStates(s : Synchronization) { | 121 | //pattern notSynchronizingStates(s : Synchronization) { |
122 | neg find hasMultipleOutgoingTrainsition(s); | 122 | // neg find hasMultipleOutgoingTrainsition(s); |
123 | neg find hasMultipleIncomingTrainsition(s); | 123 | // neg find hasMultipleIncomingTrainsition(s); |
124 | } | 124 | //} |
125 | 125 | // | |
126 | pattern hasMultipleOutgoingTrainsition(v : Synchronization) { | 126 | //pattern hasMultipleOutgoingTrainsition(v : Synchronization) { |
127 | find transition(_, v, trg1); | 127 | // find transition(_, v, trg1); |
128 | find transition(_, v, trg2); | 128 | // find transition(_, v, trg2); |
129 | trg1 != trg2; | 129 | // trg1 != trg2; |
130 | } | 130 | //} |
131 | 131 | // | |
132 | pattern hasMultipleIncomingTrainsition(v : Synchronization) { | 132 | //pattern hasMultipleIncomingTrainsition(v : Synchronization) { |
133 | find transition(_, src1, v); | 133 | // find transition(_, src1, v); |
134 | find transition(_, src2, v); | 134 | // find transition(_, src2, v); |
135 | src1 != src2; | 135 | // src1 != src2; |
136 | } | 136 | //} |
137 | 137 | // | |
138 | @Constraint(severity="error", message="error", key = {s}) | 138 | //@Constraint(severity="error", message="error", key = {s}) |
139 | pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) { | 139 | //pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) { |
140 | find transition(_, v1, s); | 140 | // find transition(_, v1, s); |
141 | find transition(_, v2, s); | 141 | // find transition(_, v2, s); |
142 | CompositeElement.regions.vertices(r1, v1); | 142 | // CompositeElement.regions.vertices(r1, v1); |
143 | CompositeElement.regions.vertices(r2, v2); | 143 | // CompositeElement.regions.vertices(r2, v2); |
144 | r1 != r2; | 144 | // r1 != r2; |
145 | } or { | 145 | //} or { |
146 | find transition(_, s, v1); | 146 | // find transition(_, s, v1); |
147 | find transition(_, s, v2); | 147 | // find transition(_, s, v2); |
148 | CompositeElement.regions.vertices(r1, v1); | 148 | // CompositeElement.regions.vertices(r1, v1); |
149 | CompositeElement.regions.vertices(r2, v2); | 149 | // CompositeElement.regions.vertices(r2, v2); |
150 | r1 != r2; | 150 | // r1 != r2; |
151 | } | 151 | //} |
152 | 152 | ||
153 | /////////////////////////////// | 153 | /////////////////////////////// |
154 | // Extra | 154 | // Extra |
@@ -166,16 +166,16 @@ pattern child(parent: CompositeElement, child: Vertex) { | |||
166 | CompositeElement.regions.vertices(parent, child); | 166 | CompositeElement.regions.vertices(parent, child); |
167 | } | 167 | } |
168 | 168 | ||
169 | @Constraint(severity="error", message="error", key = {s}) | 169 | //@Constraint(severity="error", message="error", key = {s}) |
170 | pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Vertex) { | 170 | //pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Vertex) { |
171 | find transition(_, v, s); | 171 | // find transition(_, v, s); |
172 | find child(c,v); | 172 | // find child(c,v); |
173 | neg find hasMultipleRegions(c); | 173 | // neg find hasMultipleRegions(c); |
174 | } or { | 174 | //} or { |
175 | find transition(_, s, v); | 175 | // find transition(_, s, v); |
176 | find child(c,v); | 176 | // find child(c,v); |
177 | neg find hasMultipleRegions(c); | 177 | // neg find hasMultipleRegions(c); |
178 | } | 178 | //} |
179 | 179 | ||
180 | 180 | ||
181 | pattern hasMultipleRegions(composite: CompositeElement) { | 181 | pattern hasMultipleRegions(composite: CompositeElement) { |
@@ -187,32 +187,32 @@ pattern hasMultipleRegions(composite: CompositeElement) { | |||
187 | /** | 187 | /** |
188 | * Simplifying model generation | 188 | * Simplifying model generation |
189 | */ | 189 | */ |
190 | @Constraint(severity="error", message="error", key = {s}) | 190 | //@Constraint(severity="error", message="error", key = {s}) |
191 | pattern synchThree(s: Synchronization) { | 191 | //pattern synchThree(s: Synchronization) { |
192 | Transition.target(t1,s); | 192 | // Transition.target(t1,s); |
193 | Transition.target(t2,s); | 193 | // Transition.target(t2,s); |
194 | Transition.target(t3,s); | 194 | // Transition.target(t3,s); |
195 | t1!=t2; | 195 | // t1!=t2; |
196 | t2!=t3; | 196 | // t2!=t3; |
197 | t1!=t3; | 197 | // t1!=t3; |
198 | } or { | 198 | //} or { |
199 | Transition.source(t1,s); | 199 | // Transition.source(t1,s); |
200 | Transition.source(t2,s); | 200 | // Transition.source(t2,s); |
201 | Transition.source(t3,s); | 201 | // Transition.source(t3,s); |
202 | t1!=t2; | 202 | // t1!=t2; |
203 | t2!=t3; | 203 | // t2!=t3; |
204 | t1!=t3; | 204 | // t1!=t3; |
205 | } | 205 | //} |
206 | 206 | // | |
207 | /** | 207 | ///** |
208 | * Simplifying model generation | 208 | // * Simplifying model generation |
209 | */ | 209 | // */ |
210 | @Constraint(severity="error", message="error", key = {s1,s2}) | 210 | //@Constraint(severity="error", message="error", key = {s1,s2}) |
211 | pattern twoSynch(s1 : Synchronization, s2 : Synchronization) { | 211 | //pattern twoSynch(s1 : Synchronization, s2 : Synchronization) { |
212 | Synchronization(s1); | 212 | // Synchronization(s1); |
213 | Synchronization(s2); | 213 | // Synchronization(s2); |
214 | s1 != s2; | 214 | // s1 != s2; |
215 | } | 215 | //} |
216 | 216 | ||
217 | /** | 217 | /** |
218 | * Model generation task: at least one synch | 218 | * Model generation task: at least one synch |