diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-07 17:26:07 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-07 17:26:07 +0200 |
commit | 6a3ff9bb588bf47242a56b91e35479dbba38eb19 (patch) | |
tree | 0432ecd0edafb99dc9f017d0a8cfee31a931583a /Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo | |
parent | Fix concurrency bug in AlloyHandler (diff) | |
download | VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.tar.gz VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.tar.zst VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.zip |
Scope unsat benchmarks
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo')
-rw-r--r-- | Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql | 11 |
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}) | ||
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); |
@@ -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 | ||
201 | pattern hasMultipleRegions(composite: CompositeElement) { | 212 | pattern hasMultipleRegions(composite: CompositeElement) { |
202 | CompositeElement.regions(composite,region1); | 213 | CompositeElement.regions(composite,region1); |