diff options
author | 2019-10-07 00:35:42 -0400 | |
---|---|---|
committer | 2020-06-07 19:42:47 -0400 | |
commit | b503c81bee920c18806af25393d0a90b8f77dba6 (patch) | |
tree | 9b70f606bfa7fa450457c04714e045e5ac5f6199 /Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | |
parent | VAMPIRE: fix model generation (diff) | |
download | VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.gz VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.zst VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.zip |
VAMPIRE: Implement Vampire measurement code
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 | 122 |
1 files changed, 61 insertions, 61 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..09fb45c8 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 | |||
@@ -88,67 +88,67 @@ pattern choiceHasNoIncoming(c: Choice) { | |||
88 | neg find transition(_, _, c); | 88 | neg find transition(_, _, c); |
89 | } | 89 | } |
90 | 90 | ||
91 | ///////// | 91 | /////////// |
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 |