// topological sorting
// Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>, 2022

// vertices 0..N
val N:ℕ; 

// the basic types
type Vertex = ℕ[N];
type Edge = Record[from:Vertex,to:Vertex];
type Graph = Record[V:Set[Vertex],E:Set[Edge]]
  with ∀e ∈ value.E. (e.from ∈ value.V ∧ e.to ∈ value.V);
type VertexSeq = Array[N+1,Vertex];
type Number = ℕ[N+1];

// s is a path of length n in graph G
pred path(s:VertexSeq,n:Number,G:Graph) ⇔
  true
;

// graph G is acyclic
pred acyclic(G:Graph) ⇔ 
  true
;

// all elements of V occur among the first n vertices of path s 
pred covers(s:VertexSeq,n:Number,V:Set[Vertex]) ⇔
  true
;
  
// the first n vertices of s are topologically sorted w.r.t. edge set E
pred sorted(s:VertexSeq,n:Number,E:Set[Edge]) ⇔ 
  true
;

// returns a topological sort of G
proc topologicalSort(G:Graph):VertexSeq
  requires acyclic(G);
  ensures covers(result,|G.V|,G.V);
  ensures sorted(result,|G.V|,G.E);
{
  var seq:VertexSeq = Array[N+1,Vertex](0);
  var i:Number ≔ 0;
  var V0:Set[Vertex] = G.V;
  var E0:Set[Edge] = G.E;
  while V0 ≠ ∅[Vertex] do
    invariant i = |G.V\V0|;
    invariant covers(seq,i,G.V\V0);
    invariant sorted(seq,i,G.E);
    invariant V0 ⊆ G.V;
    invariant E0 = { e | e ∈ G.E with e.from ∈ V0 ∧ e.to ∈ V0 }; 
    invariant ¬∃v∈V0,j:Number with j < i. ⟨from:v,to:seq[j]⟩ ∈ G.E;
    decreases |V0|;
  {
    choose v ∈ V0 with ¬∃e ∈ E0. (e.to = v);
    seq[i] ≔ v;
    V0 ≔ V0\{ v };
    E0 ≔ E0\{ e | e ∈ E0 with e.from = v };
    i ≔ i+1;
  }
  return seq;
}