The graph is represented by a pair (vertices
, successor
)
vertices
: this constant is the set of graph vertices
successor
: this function gives for each vertex the set of vertices directly joinable from it
module RandomSearch use import int.Int use import list.List use import list.Append use import list.Mem as L use import list.Elements as E use import init_graph.GraphSetSucc use import init_graph.GraphSetSuccPath predicate white_vertex (x: vertex) (v: set vertex) = not (mem x v) predicate nodeflip (x: vertex) (v1 v2: set vertex) = white_vertex x v1 /\ not (white_vertex x v2) predicate whitepath (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) = path x l z /\ (forall y. L.mem y l -> white_vertex y v) /\ white_vertex z v predicate whitereachable (x z: vertex) (v: set vertex) = exists l. whitepath x l z v predicate whiteaccess (r s: set vertex) (v: set vertex) = forall z. mem z s -> exists x. mem x r /\ whitereachable x z v predicate path_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) = path x l z /\ match l with | Nil -> true | Cons _ l' -> x <> z /\ not (L.mem x l') end lemma path_suffix_fst_not_twice: forall x z l "induction". path x l z -> exists l1 l2. l = l1 ++ l2 /\ path_fst_not_twice x l2 z lemma path_path_fst_not_twice: forall x z l. path x l z -> exists l'. path_fst_not_twice x l' z /\ subset (E.elements l') (E.elements l) predicate whitepath_fst_not_twice (x: vertex) (l: list vertex) (z: vertex) (v: set vertex) = whitepath x l z v /\ path_fst_not_twice x l z lemma whitepath_decomposition: forall x l1 l2 z y v. whitepath x (l1 ++ (Cons y l2)) z v -> whitepath x l1 y v /\ whitepath y (Cons y l2) z v lemma whitepath_mem_decomposition_r: forall x l z y v. whitepath x l z v -> L.mem y (l ++ (Cons z Nil)) -> exists l': list vertex. whitepath y l' z v lemma whitepath_whitepath_fst_not_twice: forall x z l v. whitepath x l z v -> exists l'. whitepath_fst_not_twice x l' z v lemma path_cons_inversion: forall x z l. path x (Cons x l) z -> exists y. edge x y /\ path y l z lemma whitepath_cons_inversion: forall x z l v. whitepath x (Cons x l) z v -> exists y. edge x y /\ whitepath y l z v lemma whitepath_cons_fst_not_twice_inversion: forall x z l v. whitepath_fst_not_twice x (Cons x l) z v -> x <> z -> (exists y. edge x y /\ whitepath y l z (add x v)) lemma whitepath_fst_not_twice_inversion : forall x z l v. whitepath_fst_not_twice x l z v -> x <> z -> (exists y l'. edge x y /\ whitepath y l' z (add x v)) lemma abc : forall z x:'a, r v. mem z (diff r v) -> z = x \/ mem z (diff r (add x v)) lemma whitereachable1 : forall x y l z v. whitepath y l z (add x v) -> whitepath y l z v lemma whitereachable2 : forall x y l z v. not (mem x v) -> whitepath y l z v -> edge x y -> whitepath x (Cons x l) z v (* lemma assert_proof : forall x v r roots'. mem x vertices -> not (mem x v) -> whiteaccess (union roots' (successors x)) (diff r (add x v)) (add x v) -> whiteaccess (add x roots') (diff r v) v *)
let rec random_search roots visited variant {(cardinal vertices - cardinal visited), (cardinal roots)} = requires {subset roots vertices } requires {subset visited vertices } ensures {subset visited result} ensures {forall z. mem z (diff result visited) -> exists x l. mem x roots /\ whitepath x l z visited } if is_empty roots then visited else let x = choose roots in let roots' = remove x roots in if mem x visited then random_search roots' visited else let r = random_search (union roots' (successors x)) (add x visited) in (*----------- nodeflip_whitepath -----------*) (* case 1: nodeflip z visited r /\ z = x *) assert {forall z. z = x -> whitepath x Nil z visited}; (* case 2: nodeflip z visited r /\ z <> x *) assert {forall z. mem z (diff r (add x visited)) -> (exists y l. mem y roots' /\ whitepath y l z (add x visited)) \/ (exists y l. edge x y /\ whitepath y l z (add x visited)) }; r end
Generated by why3doc 0.86.1