aboutsummaryrefslogtreecommitdiffstats
path: root/Domains/hu.bme.mit.inf.dslreasoner.domains.alloyexamples/patterns/hu/bme/mit/inf/dslreasoner/domains/alloyexamples/FileSystem.vql
blob: c785c2fcd5d306cd6c24d779037b86191e5fbd61 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
package hu.bme.mit.inf.dslreasoner.domains.alloyexamples

import epackage "FS"

pattern patternContent(o1: Dir, o2: FSObject) {
	Dir.contents(o1,o2);
}

@QueryBasedFeature
pattern live(this: FileSystem, l: FSObject) {
	FileSystem.root(this,l);
} or {
	FileSystem.root(this,root);
	find patternContent+(root,l);
}

@Constraint(key={child}, severity="error", message="error")
pattern contentInNotLive(parent : Dir, child: FSObject) {
	Dir.contents(parent,child);
	neg find live(_,parent);
} or {
	Dir.contents(parent,child);
	neg find live(_,child);
}

pattern dir(d: Dir) {
	Dir(d);
}

@Constraint(key={fs}, severity="error", message="error")
pattern rootIsNotDir(fs: FileSystem) {
	FileSystem.root(fs, root);
	neg find dir(root);
}