why3doc index index
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 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 lemma path_decomp_with_last_occ: forall x z l1 l2 y. path x (l1 ++ (Cons y l2)) z -> y <> z -> exists l3 l4. l1 ++ (Cons y l2) = l3 ++ (Cons y l4) /\ not L.mem y l4 lemma whitepath_decomp_with_last_occ: forall x z l1 l2 y v. whitepath x (l1 ++ (Cons y l2)) z v -> y <> z -> exists l. whitepath y (Cons y l) z v /\ not L.mem y l lemma whitepath_add_def: (* crazy *) forall x y l' z v. whitepath y l' z (add x v) <-> y <> x /\ not L.mem x l' /\ z <> x /\ whitepath y l' z v lemma whitepath_enhance: forall x z l v. whitepath x (Cons x l) z v -> x <> z -> not L.mem x l -> exists y l'. edge x y /\ whitepath y l' z (add x v)
let rec random_search r v variant {(cardinal vertices - cardinal v), (cardinal r)} = requires {subset r vertices } requires {subset v vertices } ensures {subset v result} ensures {forall z y l. mem y r -> whitepath y l z v -> mem z (diff result v)} if is_empty r then v else let x = choose r in let r' = remove x r in if mem x v then random_search r' v else let v' = random_search (union r' (successors x)) (add x v) in (*----------- whitepath_nodeflip -----------*) assert {forall z y l. mem y r -> whitepath y l z v -> z <> x -> whitepath y l z (add x v) \/ exists x' l'. mem x' (successors x) /\ whitepath x' l' z (add x v) } ; v' let random_search_main (roots: set vertex) = requires {subset roots vertices} ensures {forall z y l. mem y roots -> path y l z -> mem z result} random_search roots empty end
Generated by why3doc 0.88.0