open util/graph[Node]


//changing any one of these assertions to a fact,
//will not find an example!

assert {
	some s1,s2:SyncGraph | s1.edge != s2.edge
}

assert {
	some s1,s2:SyncGraph | contained[s1,s2]
}

assert {
	some s1,s2:SyncGraph | dis[inner[s1], inner[s2]]
}


pred contained[s1,s2:SyncGraph] {

	(nodes[s1] in inner[s2])
	or
	(nodes[s2] in inner[s1])

}

pred dis[n1,n2: set Node] {
	 n1 & n2 = none
}


abstract sig Node {
	depth:  Int
}
{
	depth >= 0
}

sig Task extends Node {}
{
	all t:Task { t not in leaves[Graph.edge]}
	all t:Task { t not in roots[Graph.edge]}
	
	depth > 0
}

sig Input extends Node {}
{
	Input in roots[Graph.edge]
	depth = 0
}

sig Output extends Node {}
{
	Output in leaves[Graph.edge]
	all o:Output { o  not in roots[Graph.edge] }
	depth >= 0
}

//given an edge 
//returns its nodes
fun nodes [r: Node ->Node] : set Node {
	dom[r] + ran[r]
}

fun  nodes[g: SyncGraph] : set Node {
	nodes[g.edge]
}

fun  outer[r: Node->Node] : set Node {
	leaves[r] + roots[r]
}


fun  outer[g: SyncGraph] : set Node {
	outer[g.edge]
}

fun  inner[r: Node->Node] : set Node {
	nodes[r] - leaves[r] - roots[r]
}

fun  inner[g: SyncGraph] : set Node {
	inner[g.edge]
}

one sig Graph  {

	edge: set Node->Node

}
{
	noSelfLoops[edge]
	forest[edge]
}

some sig SyncGraph {
	edge: set Node->Node 
}
{
	edge in Graph.edge
	some  inner[edge]  
	some  outer[edge]

	//all outer nodes must be at the same depth
	all n1,n2:outer[edge] | n1.depth = n2.depth
	//? maybe this should be an assertion
	all i:inner[edge], o:outer[edge] | i.depth > o.depth
}



fact {
	all n1,n2:Node 
	{ 
		 n1->n2 in Graph.edge =>
			abs[int[n1.depth] - int[n2.depth]] <= 1
	}	
}



fun abs[i:Int] : Int {	
	i >= 0 =>
		i
	else
		0 - i
}

check checkAbs {
	all i:Int | abs[i] + abs[0 - i] = abs[i] + abs[i]
	abs[0] = 0
}


check checkGraphFunctions {
	no n:inner[Graph.edge] | n in outer[Graph.edge]
	no n:inner[SyncGraph.edge] | n in outer[SyncGraph.edge]
}

pred example {

	#Input = 1
	#Output = 1
	#Task >= 2
	#SyncGraph = 2
}

run example for 1 Graph, 8 Node, 2 SyncGraph