domain Functionality
{
   primitive Task ::= (id: String).

   [Closed] 
   primitive Conflict ::= (t1: Task, t2: Task).
}

domain Network
{
   primitive Node ::= (id: String).

   [Closed(fromNode, toNode)] [Unique(fromNode, toNode -> cap)] 
   primitive Channel ::= (fromNode: Node, toNode: Node, cap: PosInteger).
   
   // Ensure each node has 2 input/output channels at max
   bigFanIn  := n is Node, count(Channel(_,n,_)) > 2.
   bigFanOut := n is Node, count(Channel(n,_,_)) > 2.

   // Ensure that capacities are balanced
   mustBal ::= (Node).
   mustBal(n) :- Channel(_,n,_), Channel(n,_,_).
   clog := mustBal(n), sum(Channel(_,n,_),2) != sum(Channel(n,_,_),2).

   conforms := !(bigFanIn | bigFanOut | clog).        
}

domain Mapping extends Functionality, Network
{
   [Closed] [Function(fromTask -> toNode)] 
   primitive Binding ::= (fromTask: Task, toNode: Node).
   
   // Check if two conflicting tasks are deployed to the same node
   inConflict := Binding(t1, n), Binding(t2, n), Conflict(t1, t2).

   conforms := !inConflict.
}

partial model Ex of Mapping
{
   t1 is Task("UI") 
   t2 is Task("Voice Recognition") 
   t3 is Task("Network Controller")
   Conflict(t1, t2) 
   Conflict(t2,t3)

   n1 is Node("DSP") 
   n2 is Node("GPU") 
   n3 is Node("CPU")
   c1 is Channel c2 is Channel c3 is Channel
   c4 is Channel c5 is Channel c6 is Channel
   c7 is Channel c8 is Channel c9 is Channel
}