File system tutorial

The goal of this tutorial is to give a brief overview of the partial modeling and model generation features of the Refinery framework. The running example will be the modeling of files, directories, and repositories.

Partial models

Types and relations

• First, let us introduce some basic types: Dir, File, and FileSystem, along with the relations between them: element and root. There is a scope expression at the end, which we will ignore for now.

class FileSystem {
    contains File[1] root
}

class File.

class Dir extends File {
    contains File[] element
}

scope node = 10.

Try in Refinery

• Notice that the syntax is essentially identical to Xcore.
• Review the partial model visualization. You should get something like this:

• Add some statements about a partial model:

class FileSystem {
    contains File[1] root
}

class File.

class Dir extends File {
    contains File[] element
}

Dir(resources).
element(resources, img).
File(img).

scope node = 10.

Partial models

• Notice that the instance model elements are coexisting with <type>::new nodes representing the prototypes of newly created objects.

• Check the disabled equals and exist predicates. check the visual annotation of those predicates in the visualization (dashed line, shadow).

Information merging

• For the object img, we didn’t specify if it is a directory or not. Therefore, it will typically be a folder.

• If we want to state that img is not a directory, we need to a negative statement:

!Dir(img).

• Statements are merged with respect to the refinement relation of 4-valued logic.

• If we add, a statement both negatively and positively, it will create an inconsistency:

element(resources, img).
!element(resources, img).

• Inconsistent models parts in a partial model typically make the problem trivially unsatisfiable.

• However, the model can be saved if the inconsistent part may not exist…

!File(File::new).

Default values

• A large amount of statements can be expressed by using *.
• The default keyword defines lower priority statements that need to be considered unless other statement specifies otherwise. No information merging is happening.

Constraints

Let’s extend the metamodel with a new class SymLink:

class FileSystem {
    contains File[1] root
}

class File.

class Dir extends File {
    contains File[0..10] element
}

class SymLink extends File {
    File[1] target
}

Dir(resources).
element(resources, img).
element(resources, link).
target(link, img).

scope node = 10.

• Add some simple constraints:

% Simple constraints:
pred hasReference(f) <-> target(_, f).
error pred selfLoop(s) <-> target(s, s).
target(x,x).

• There are no empty directories in a git repository, so let’s forbid them!

error pred emptyDir(d) <-> Dir(d), !element(d,_).

• End result:

class FileSystem {
    contains File[1] root
}

class File.

class Dir extends File {
    contains File[0..10] element
}

class SymLink extends File {
    File[1] target
}

Dir(resources).
element(resources, img).
!Dir(img).
element(resources, link).
target(link,img).

% Simple constraints:
pred hasReference(f) <-> target(_, f).
error pred selfLoop(s) <-> target(s, s).

% Object equality with ==:
error pred emptyDir(d) <-> Dir(d), !element(d, _).
pred importantFile(f) <-> target(l1, f), target(l2, f), l1 != l2.

% Transitive closure, and
pred containsFile(fs, file) <->
    FileSystem(fs),
    root(fs, file)
;
    FileSystem(fs),
    root(fs, rootDir),
    element+(rootDir, file).

% Predicate reuse
error conflictBetweenTwoFileSystem(fs1, fs2, l, t) <->
    containsFile(fs1, l),
    containsFile(fs2, t),
    fs1 != fs2,
    target(l, t).

scope node = 40..50, FileSystem = 2, importantFile = 1..*.