module Contender

sig Graph {
	nodes : set Node,
	edges : set Edge,
}{ edges.(source+target) in nodes }

sig Node {}

sig Edge {
	source : set Node,
	target : set Node
}

fact { no disj G1,G2:Graph | some G1.nodes & G2.nodes or some G1.edges & G2.edges }

one sig G1,G2 extends Graph {}
one sig N1,N2,N3 ,N4,O1,O2 extends Node {}
one sig E1,E3 extends Edge {}

fact { 
	N1+N2+N3+N4 = G1.nodes
	O1+O2 = G2.nodes
	E1+E3 = G1.edges
	E1->N1 + E3->N3 = source
	E1->N2 + E3->N4 = target
}

-- compute the set of all reachable nodes in a graph.
-- this is the obvious formulation of this property.
fun Graph::allTargets1[n:Node] : set Node { n.*(~source.target)  }

-- predictable but undesirable
fact1A: run { none = G1.allTargets1[none] } for 0

-- predictable
fact1B: run { 
	N1+N2 = G1.allTargets1[N1] 
	not N1 in G1.allTargets1[N2] 
	N3+N4 = G1.allTargets1[N3]
	not N3 in G1.allTargets1[N4]
} for 0

-- predicatable but undesirable
fact1C: run { O1 = G1.allTargets1[O1] } for 0

-- because of undesirable properties of this formulation,
-- we want to find a better formulation that more precisely captures our intent.

-- is this a contender?
fun Graph::allTargets2[n:one this.nodes] : some this.nodes { n.*(~source.target)  }

-- still undesirable
fact2A: run { none = G1.allTargets2[none] } for 0

-- predictable
fact2B: run { 
	N1+N2 = G1.allTargets2[N1] 
	not N1 in G1.allTargets2[N2] 
	N3+N4 = G1.allTargets2[N3]
	not N3 in G1.allTargets2[N4]
} for 0

-- still undesirable
fact2C: run { O1 = G1.allTargets1[O1] } for 0

-- definitely undesirable
fact2D: run { 
	N1+N2+N3+N4 = G1.allTargets2[N1+N3]
	N1+N2+N3+N4+O1 = G1.allTargets2[N1+N3+O1] 
} for 0

-- allTargets2 communicates a bit more information than allTargets3 below
-- unfortunately, allTargets2 and allTargets3 seem undistinguishable to the type system.

fun Graph::allTargets3[n:this.nodes] : some this.nodes { n.*(~source.target)  }