[Examples] topological sort online basic algorithm

    - only add_edge operation

examples/topological_sorting.mlw

@@ -10,26 +10,29 @@ theory Graph
 
   function vertices graph: S.set vertex
 
+  function edges graph: S.set (vertex , vertex)
+
+  axiom edges_use_vertices:
+  forall g:graph. forall x y:vertex.
+    S.mem (x,y) (edges g) -> (S.mem x (vertices g) /\ S.mem y (vertices g))
+
   (** direct predecessors *)
   function preds graph vertex: S.set vertex
 
-  axiom preds_is_vertices:  forall g:graph. forall v:vertex.
-   S.subset (preds g v) (vertices g)
-
-  type msort = M.map vertex int
+  axiom preds_def:  forall g:graph. forall v:vertex. forall u:vertex.
+   S.mem (u,v) (edges g) <-> S.mem u (preds g v)
 
-  function defined_sort (m:msort) : S.set vertex
-  axiom defined_sort_def:
-   forall m:msort. forall v: vertex[S.mem v (defined_sort m)].
-    S.mem v (defined_sort m) <-> 0 <= M.get m v
+  (** direct successors *)
+  function succs graph vertex: S.set vertex
+  axiom succs_def:  forall g:graph. forall v:vertex. forall u:vertex.
+   S.mem (u,v) (edges g) <-> S.mem v (succs g u)
 
-  predicate partial_sort (g: graph) (m:msort) =
-    forall v:vertex. forall u:vertex.
-    S.mem u (preds g v) -> 0 <= (M.get m v)
-     -> 0 <= (M.get m u) < (M.get m v)
+  type msort = M.map vertex int
 
   predicate sort (g: graph) (m:msort) =
-    partial_sort g m /\ forall v:vertex. S.mem v (vertices g) -> 0 <= M.get m v
+    forall v:vertex. forall u:vertex.
+    S.mem (u,v) (edges g) ->
+    (M.get m u) < (M.get m v)
 
 end
 
@@ -41,6 +44,16 @@ module Static
   use set.Fset as S
   use map.Map as M
 
+  function defined_sort (m:msort) : S.set vertex
+  axiom defined_sort_def:
+   forall m:msort. forall v: vertex[S.mem v (defined_sort m)].
+    S.mem v (defined_sort m) <-> 0 <= M.get m v
+
+  predicate partial_sort (g: graph) (m:msort) =
+    forall v:vertex. forall u:vertex.
+    S.mem (u,v) (edges g) -> 0 <= (M.get m v)
+     -> 0 <= (M.get m u) < (M.get m v)
+
   type marked = (S.set vertex)
 
   exception Cycle_found
@@ -82,8 +95,6 @@ module Static
       p := S.remove u !p
       done;
     end;
-    assert { inv g !values !next };
-    assert { not (S.mem v seen) };
     values := M.set !values v !next;
     next := !next + 1
 
@@ -107,4 +118,98 @@ module Static
      done;
      !values
 
-end
\ No newline at end of file
+end
+
+module Online_graph
+  use export Graph
+
+  function add_edge graph vertex vertex: graph
+  axiom add_edge_def_preds:
+    forall g:graph. forall u v:vertex.
+      forall x.
+        preds (add_edge g u v) x =
+          if x = v then S.add u (preds g v) else preds g x
+
+  axiom add_edge_def_succs:
+    forall g:graph. forall u v:vertex.
+      forall x.
+        succs (add_edge g u v) x =
+          if x = u then S.add v (succs g u) else succs g x
+
+
+end
+
+(**
+A New Approach to Incremental Topological Ordering
+   Michael A. Bender, Jeremy T. Fineman, Seth Gilbert
+*)
+module Online_Basic
+
+  use import ref.Ref
+  use import Online_graph
+  use set.Fset as S
+  use map.Map as M
+
+  type marked = (S.set vertex)
+
+  exception Cycle_found
+
+  type t = {
+    mutable graph : graph;
+    mutable values: msort;
+ }
+
+ predicate inv (g:t) = sort g.graph g.values
+
+  let create (g:graph): t
+     requires { forall x: vertex. S.is_empty (preds g x) }
+     ensures  { result.graph = g }
+     ensures  { inv result }
+   =
+    {graph = g; values = M.const 0}
+
+  let rec dfs (g:t) (v:vertex)
+              (seen:marked) (min_depth:int) : unit
+    requires { inv g }
+    requires { S.mem v (vertices g.graph) }
+    requires { S.subset seen (vertices g.graph) }
+    raises  { Cycle_found -> true }
+    variant { S.cardinal (vertices g.graph) - S.cardinal seen }
+    ensures { min_depth <= M.get g.values v}
+    ensures { inv g }
+    ensures { forall x:vertex. S.mem x seen -> M.get (old g.values) x = M.get g.values x }
+    ensures { forall x:vertex. M.get (old g.values) x <= M.get g.values x }
+   =
+  'Init:
+   if S.mem v seen then raise Cycle_found;
+   if M.get g.values v < min_depth then
+  'Init_loop:
+    begin
+     let p = ref (succs g.graph v) in
+     let seen = S.add v seen in
+     while not (S.is_empty !p) do
+      invariant { inv g }
+      invariant { forall s:vertex. S.mem s (succs g.graph v) -> not (S.mem s !p) -> min_depth < M.get g.values s }
+      invariant { S.subset !p (succs g.graph v) }
+      invariant { forall x:vertex. S.mem x seen -> M.get (at g.values 'Init_loop) x = M.get g.values x }
+      invariant { forall x:vertex. M.get (at g.values 'Init_loop) x <= M.get g.values x }
+      variant {S.cardinal !p}
+      let u = S.choose !p in
+      dfs g u seen (min_depth + 1);
+      p := S.remove u !p
+      done;
+    end;
+    g.values <- M.set g.values v min_depth
+
+  let add_edge (g:t) (x:vertex) (y:vertex): unit
+     requires { inv g }
+     requires { S.mem x (vertices g.graph) }
+     requires { S.mem y (vertices g.graph) }
+     ensures  { inv g }
+     ensures  { g.graph = old (add_edge g.graph x y) }
+     raises   { Cycle_found -> true } =
+      dfs g y (S.singleton x) (M.get g.values x + 1);
+      g.graph <- add_edge g.graph x y;
+
+
+end