Kumbang Constraint Language

Boolean connectives - a, b, ai are boolean values:


not a (negation): true if a is false
a1 and a2 and ... and an (conjunction): all ai are true
a1 or a2 or ... or an (disjunction): at one of ai is true
a => b (implication): (not a) or b
a <=> b (equivalence): a => b and b => a

References:

References to parts of components and features, and interfaces of components can be made. The references have the following syntax:

StructureReference ::= ReferenceItem ('.' ReferenceItem)* ['->' ReferenceItem]
ReferenceItem ::= PartName [':' TypeName]
PartName ::= Identifier
TypeName ::= Identifier

Intuitively, a reference item consists of a list of part names separated by dots ('.'). Each part name may in addition be qualified by a type name. Finally, the end of the reference may contain a left arrow ('->') and be followed by an interface name that can also be qualified by a type name.
In feature types, it is possible to make references to the component hierarchy. Such references are prefixed with 'component-root.'

Predicates:

- ref is a reference (either a part reference or an interface reference), intref, intref2 is an interface reference, type is a type:

NOTE: predicates are by default existentially quantified

present(ref): true if an instance referenced by ref is in the configuration
instance_of(ref, type): true if ref is an instance (either direct or indirect) of type
has_instances(type): true if the type has instances in the configuration
has_part_of_type(type): true if the instance has a transitive part of type type
has_part_of_type(ref, type): true if an instance referenced by ref has a transitive part of type type
connected(intref): true if an interface referred to by intref is connected, either by it's tip or tail
connected(intref, intref2): true if an interface referred to by intref is connected to an interface referred to by intref2

Other functions:

-ref is a part reference, attr is a name of an attribute

value(attr): the value of attribute attr
value(ref, attr): the set of values that instances referenced by ref have by the name attr
cardinality(ref): the number of instances referred to by ref

for_all(X:ref)(present(X) => ...): universal quantification (present(X) needed if ref is a many-instantiated part reference)
exists(X:ref)(...): existential quantification


Constant values:

positive integers
constant symbols

Comparison operators:

- a and b are (sets of) values, either returned by value or cardinality functions or constant values
- comparison operators are by default existentially quantified

=, !=: equals, does not equal (for all values)
<, <=, >, >=: less than, less than or equal, greates than, greater than or equal (only for integer values)

Arithmetic operators:

*, / (integer division), mod (modulo)
+, -