// A domain is a unit of structural abstraction. 
// It contains ADTs and a logic program that defines the structure of the abstraction.
//
// This specific domain describes the structure of a software component model.
domain Software
{
    // The root element of the software component model
    primitive System ::= (name : String).

    // Data type constructors with labeled arguments
    // The owner field refers to either the System or other Components.
    //
    // Predefined attribute annotations reduce size of specification:
    // - The "Closed" attribute requires that all instances of Subsystem
    //   that are used as the second argument of Component, also exists
    //   as a fact in the facts of a model.
    // - The "Unique" attribute adds a check that for all instances of
    //   Component, there is a unique mapping of names to owners.
    [Closed(owner)] [Unique(name -> owner)]
    primitive Component ::= (name : String, owner : Subsystem).

    [Closed(fromSys, toSys)]
    primitive Link ::= (name : String, fromSys : Subsystem, toSys : Subsystem).

    // Arbitrary unions for polymorphism and recursive data types
    Subsystem ::= System + Component.

    // The special "conforms" query defines the rules of the abstractions.
    conforms := count(System(_)) = 1.
}

// Another independent domain definition, defining a simplified
// version of a hardware model.
domain Hardware 
{
    primitive Node ::= (name : String).

    [Closed(fromNode, toNode)]
    primitive Channel ::= (fromNode : Node, toNode : Node).
    
    // A derived data type constructor. Type definitions can also omit
    // the specification of labels for each position.
    canSend ::= (Node, Node).
    // Rules generate derived facts based on constraints on other facts.
    canSend(x, x) :- x is Node.
    canSend(x, y) :- Channel(x, y).
    // Fixed-point computation handles recursion
    canSend(x, z) :- canSend(x, y), canSend(y, z).
}

// This domain extends the domains Software and Hardware and specifies
// additional constraints on how a valid deployment of software components
// to hardware nodes must look like.
// Extended domains inherit a specification and can add new data types. 
// Product domains merge type systems and logic programs while conjuncting constraints.
domain Partitioning extends Software, Hardware
{
    // Only existing Components may be deployed to existing nodes. Additionally
    // this annotation requires, that all Components must be deployed.
    [Closed(sys,node)] [Total(sys)]
    primitive Deployment ::= (sys : Component, node : Node).
    
    // Negation-as-failure allows a rule to check for the absence of a fact. 
    cannotSend := Deployment(c1, n1), Deployment(c2, n2), Link(_, c1, c2), fail canSend(n1, n2).

    // Inherited constraints of Software and Hardware are implicitly added 
    // to the conforms query of this domain.
    conforms := !cannotSend.
}

// Although the partial model contains no specific unknowns, some terms are missing 
// for a valid model satisfying all constraints.
// FORMULA automatically adds the required number of instances for the 
// type Deployment prior to model finding.
partial model PartitioningProblem of Partitioning
{
    root is System("root")
    c1 is Component("comp1", root)
    c2 is Component("comp2", root)
    Link("connect", c1, c2)

    n1 is Node("node1")
    n2 is Node("node2")
    Channel(n1,n2)
}