aboutsummaryrefslogtreecommitdiffstats
path: root/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
diff options
context:
space:
mode:
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.vql11
1 files changed, 11 insertions, 0 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 98a10cde..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,6 +22,12 @@ pattern multipleEntryInRegion(r : Region) {
22 e1 != e2; 22 e1 != e2;
23} 23}
24 24
25@Constraint(severity="error", message="error", key = {sct})
26pattern unsat_multipleEntryInRegion(sct : Statechart) {
27 Statechart(sct);
28 neg find multipleEntryInRegion(_);
29}
30
25pattern transition(t : Transition, src : Vertex, trg : Vertex) { 31pattern 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);
@@ -197,6 +203,11 @@ pattern SynchronizedRegionDoesNotHaveMultipleRegions(s : Synchronization, v : Ve
197 neg find hasMultipleRegions(c); 203 neg find hasMultipleRegions(c);
198} 204}
199 205
206//@Constraint(severity="error", message="error", key = {sct})
207//pattern unsat_SynchronizedRegionDoesNotHaveMultipleRegions(sct : Statechart) {
208// Statechart(sct);
209// neg find SynchronizedRegionDoesNotHaveMultipleRegions(_, _);
210//}
200 211
201pattern hasMultipleRegions(composite: CompositeElement) { 212pattern hasMultipleRegions(composite: CompositeElement) {
202 CompositeElement.regions(composite,region1); 213 CompositeElement.regions(composite,region1);