run-1-1-13-5-2269.cl1

**FIXME**
component Z3 {
    type Relation;
}
*********

component Virt {
    let <<has affinity with>> : Z3.Relation.Equivalence;
    let <<has antiaffinity with>> : Z3.Relation.Symmetric;
    let <<can have affinity with>> : Z3.Relation.Equivalence;
    let <<can have antiaffinity with>> : Z3.Relation.Symmetric;
}

component Node {
    let virts : Virt*;
}

component Group {
    let nodes : Node*;
    let virts : Virt*;
    let fallbacks : Boolean;
    let is_restricted : Boolean;

    for all (node : Node, virt : Virt)
    {
        ** Physical membership
        (nodes <<has>> node and virts <<has>> virt) => node.virts <<can have>> virt;

        ** Restriction
        (nodes !<<has>> node and virts <<has>> virt and is_restricted) => node.virts !<<can have>> virt;
    };
}

component Cluster {
    let nodes : Node*;
    let groups : Group*;

    for all (group : Group, virt : Virt)
    {
        (groups <<has>> group and group.virts <<has>> virt) =>
            exists (node : Node)
            {
                 nodes <<has>> node;
                 node.virts <<has>> virt;
            };

        ** Non-restriction
        for all (node : Node)
        {
            (groups <<has>> group and nodes <<has>> node and group.virts <<has>> virt and !group.is_restricted) => node.virts <<can have>> virt;
        };
    };
}

** Node affinity
for all (node_1 : Node, node_2 : Node, virt_1 : Virt, virt_2 : Virt)
{
    (virt_1 != virt_2 and node_1.virts <<can have>> virt_1 and node_2.virts <<can have>> virt_2 and virt_1 <<has affinity with>> virt_2) => (node_1 = node_2);
    (node_1.virts <<has>> virt_1 and node_2.virts <<has>> virt_2 and virt_1 <<can have affinity with>> virt_2) => (node_1 = node_2);
};

** Node antiaffinity
for all (node_1 : Node, node_2 : Node, virt_1 : Virt, virt_2 : Virt)
{
    (node_1.virts <<can have>> virt_1 and node_2.virts <<can have>> virt_2 and virt_1 <<has antiaffinity with>> virt_2) => (node_1 != node_2);
    (node_1.virts <<has>> virt_1 and node_2.virts <<has>> virt_2 and virt_1 <<can have antiaffinity with>> virt_2) => (node_1 != node_2);
};

let node0 = Node();
let virt0 = Virt();
let virt1 = Virt();
let virt2 = Virt();
let virt3 = Virt();
let virt4 = Virt();
let virt5 = Virt();
let virt6 = Virt();
let virt7 = Virt();
let virt8 = Virt();
let virt9 = Virt();
let virt10 = Virt();
let virt11 = Virt();
let virt12 = Virt();
let group0 = Group { nodes <- ([node0]:Node*); virts <- ([virt0; virt1; virt2; virt3; virt4; virt5; virt6; virt7; virt8; virt9; virt10; virt11; virt12]:Virt*); is_restricted <- true; };
let cluster = Cluster { nodes <- [node0]; groups <- [group0]; };
assert(virt0 <<has antiaffinity with>> virt1);
assert(virt1 <<can have affinity with>> virt3);
assert(virt5 <<has affinity with>> virt11);
assert(virt2 <<can have affinity with>> virt12);
assert(virt0 <<can have affinity with>> virt7);