VIATRA2/Frequently Asked Questions

General

What is Viatra2?

TODO

Is it available for free?

TODO

How do I obtain Viatra2?

TODO

How do I give feedback (bug reports, improvement ideas, experiences, observations)?

TODO

VTML metamodeling

TODO

Patterns and pattern language

Can patterns (or a single pattern) reference each other recursively?

Yes. However, the recursion should be well-founded. In certain cases, pattern systems that are not well-founded (but have a sensible fixpoint) are also acceptable, but ensuring their correct behaviour is is the responsibility of the pattern engineer.

Can patterns and gtrules be referenced from other VTCL machines?

Yes. The fully qualified name of the pattern/gtrule should be used instead of the short name. The same applies for VTCL rules.

Example:

machine1.vtcl

namespace mydomain.mysubdomain;
machine mymachine {
...
pattern mypattern(X) = {
...
rule myrule(in X) = ...
...

machine2.vtcl

machine myothermachine {
...
pattern composite(A) = {
      find mydomain.mysubdomain.mymachine.mypattern(A);
...
rule somerule(in C) = seq{
      call mydomain.mysubdomain.mymachine.myrule(C);
      forall A in C with find mydomain.mysubdomain.mymachine.mypattern(A) do ...

The pattern matcher seems to discard some occurrences of my patterns. Why?

VTCL has injective pattern matching semantics; in other words, pattern occurrences have to be isomorphic to the pattern graph. The practical implication is that no two pattern variables in the same pattern body can take the same value; such occurrences will be rejected. Patterns should be designed with this important phenomenon in mind.

The only exception is explicit variable assignment (e.g. A=B). The relaxing effect of variable assignment also applies indirectly; the assignment can be asserted in a separate pattern called using the find keyword.

Example:

 pattern fullsiblings(X, Y) = {
      person(X);
      person(Y);
      person(Parent1);
      person(Parent2);
      person.parent(PX1, X, Parent1);
      person.parent(PX2, X, Parent2);
      person.parent(PY1, Y, Parent1);
      person.parent(PY2, Y, Parent2);
 }

As Parent1 and Parent2 are not allowed to coincide due to injectivity, X and Y need two separate common parents. Therefore this pattern does not match half-siblings. Injectivity also keeps X and Y separate, so a single person with two parents does not fit the pattern either.

VTCL transformations

TODO

Graphical user interface and usage

TODO

Sensoria CASE Tool

TODO

Miscellaneous

TODO