1 (*external c_counter : unit -> int = "c_counter"*)
3 (* Optimize triples_conj by first extracting the intersection of the two sets,
4 which can certainly be in the intersection *)
5 let pTRIPLES_CONJ_OPT = ref true
6 (* For complement, make NegState for the negation of a single state *)
7 let pTRIPLES_COMPLEMENT_OPT = ref true
8 (* For complement, do something special for the case where the environment
9 and witnesses are empty *)
10 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
11 (* "Double negate" the arguments of the path operators *)
12 let pDOUBLE_NEGATE_OPT = ref true
13 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
14 let pNEW_INFO_OPT = ref true
15 (* Filter the result of the label function to drop entries that aren't
16 compatible with any of the available environments *)
17 let pREQUIRED_ENV_OPT = ref true
18 (* Memoize the raw result of the label function *)
19 let pSATLABEL_MEMO_OPT = ref true
20 (* Filter results according to the required states *)
21 let pREQUIRED_STATES_OPT = ref true
22 (* Drop negative witnesses at Uncheck *)
23 let pUNCHECK_OPT = ref true
24 let pANY_NEG_OPT = ref true
25 let pLazyOpt = ref true
27 (* Nico: This stack is use for graphical traces *)
28 let graph_stack = ref ([] : string list
)
29 let graph_hash = (Hashtbl.create
101)
32 let pTRIPLES_CONJ_OPT = ref false
33 let pTRIPLES_COMPLEMENT_OPT = ref false
34 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
35 let pDOUBLE_NEGATE_OPT = ref false
36 let pNEW_INFO_OPT = ref false
37 let pREQUIRED_ENV_OPT = ref false
38 let pSATLABEL_MEMO_OPT = ref false
39 let pREQUIRED_STATES_OPT = ref false
40 let pUNCHECK_OPT = ref false
41 let pANY_NEG_OPT = ref false
42 let pLazyOpt = ref false
46 let step_count = ref 0
49 if not
(!step_count = 0)
52 step_count := !step_count - 1;
53 if !step_count = 0 then raise Steps
56 let inc cell
= cell
:= !cell
+ 1
58 let satEU_calls = ref 0
59 let satAW_calls = ref 0
60 let satAU_calls = ref 0
61 let satEF_calls = ref 0
62 let satAF_calls = ref 0
63 let satEG_calls = ref 0
64 let satAG_calls = ref 0
72 Printf.sprintf
"_fresh_r_%d" c
74 (* **********************************************************************
76 * Implementation of a Witness Tree model checking engine for CTL-FVex
79 * **********************************************************************)
81 (* ********************************************************************** *)
82 (* Module: SUBST (substitutions: meta. vars and values) *)
83 (* ********************************************************************** *)
89 val eq_mvar
: mvar
-> mvar
-> bool
90 val eq_val
: value -> value -> bool
91 val merge_val
: value -> value -> value
92 val print_mvar
: mvar
-> unit
93 val print_value
: value -> unit
97 (* ********************************************************************** *)
98 (* Module: GRAPH (control flow graphs / model) *)
99 (* ********************************************************************** *)
105 val predecessors
: cfg
-> node
-> node list
106 val successors
: cfg
-> node
-> node list
107 val extract_is_loop
: cfg
-> node
-> bool
108 val print_node
: node
-> unit
109 val size
: cfg
-> int
110 val print_graph
: cfg
-> string option ->
111 (node
* string) list
-> (node
* string) list
-> string -> unit
115 module OGRAPHEXT_GRAPH
=
118 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
119 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
120 let print_node i
= Format.print_string
(Common.i_to_s i
)
124 (* ********************************************************************** *)
125 (* Module: PREDICATE (predicates for CTL formulae) *)
126 (* ********************************************************************** *)
128 module type PREDICATE
=
131 val print_predicate
: t
-> unit
135 (* ********************************************************************** *)
137 (* ---------------------------------------------------------------------- *)
138 (* Misc. useful generic functions *)
139 (* ---------------------------------------------------------------------- *)
141 let get_graph_files () = !graph_stack
142 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
152 let foldl = List.fold_left
;;
154 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
156 type 'a esc
= ESC
of 'a
| CONT
of 'a
158 let foldr = List.fold_right
;;
160 let concat = List.concat;;
164 let filter = List.filter;;
166 let partition = List.partition;;
168 let concatmap f l
= List.concat (List.map f l
);;
176 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
178 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
180 let rec some_tolist opts
=
183 | (Some x
)::rest
-> x
::(some_tolist rest
)
184 | _
::rest
-> some_tolist rest
187 let rec groupBy eq l
=
191 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
192 (x
::xs1
)::(groupBy eq xs2
)
195 let group l
= groupBy (=) l
;;
197 let rec memBy eq x l
=
200 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
203 let rec nubBy eq ls
=
206 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
207 | (x
::xs
) -> x
::(nubBy eq xs
)
213 | (x
::xs
) when (List.mem x xs
) -> nub xs
214 | (x
::xs
) -> x
::(nub xs
)
217 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
219 let setifyBy eq xs
= nubBy eq xs
;;
221 let setify xs
= nub xs
;;
223 let inner_setify xs
= List.sort compare
(nub xs
);;
225 let unionBy compare eq xs
= function
228 let rec loop = function
230 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
231 List.sort compare
(loop xs
)
234 let union xs ys
= unionBy state_compare (=) xs ys
;;
236 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
238 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
240 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
241 let supseteq xs ys
= subseteq ys xs
243 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
245 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
247 (* Fix point calculation *)
249 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
252 (* Fix point calculation on set-valued functions *)
253 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
254 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
256 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
258 (* ********************************************************************** *)
259 (* Module: CTL_ENGINE *)
260 (* ********************************************************************** *)
263 functor (SUB
: SUBST
) ->
264 functor (G
: GRAPH
) ->
265 functor (P
: PREDICATE
) ->
270 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
272 type ('pred
,'anno
) witness
=
273 (G.node
, substitution
,
274 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
275 Ast_ctl.generic_witnesstree
277 type ('pred
,'anno
) triples =
278 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
280 (* ---------------------------------------------------------------------- *)
281 (* Pretty printing functions *)
282 (* ---------------------------------------------------------------------- *)
284 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
285 let print_generic_subst = function
287 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
288 | A.NegSubst
(mvar
, v
) ->
289 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
290 Format.print_string
"[";
291 Common.print_between
(fun () -> Format.print_string
";" )
292 print_generic_subst substxs
;
293 Format.print_string
"]"
295 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
297 | A.Wit
(state
, subst
, anno
, childrens
) ->
298 Format.print_string
"wit ";
300 print_generic_substitution subst
;
301 (match childrens
with
302 [] -> Format.print_string
"{}"
304 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
305 print_generic_witnesstree childrens
; Format.close_box
())
307 Format.print_string
"!";
308 print_generic_witness wit
310 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
313 Format.print_string
"{";
315 (fun () -> Format.print_string
";"; Format.force_newline
() )
316 print_generic_witness witnesstree
;
317 Format.print_string
"}";
320 and print_generic_triple
(node
,subst
,tree
) =
322 print_generic_substitution subst
;
323 print_generic_witnesstree tree
325 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
326 Format.print_string
"<";
328 (fun () -> Format.print_string
";"; Format.force_newline
())
329 print_generic_triple xs
;
330 Format.print_string
">"
333 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
334 Printf.printf
"%s\n" str
;
335 List.iter
(function x ->
336 print_generic_triple
x; Format.print_newline
(); flush stdout
)
337 (List.sort compare l
);
340 let print_required_states = function
341 None
-> Printf.printf
"no required states\n"
343 Printf.printf
"required states: ";
346 G.print_node x; Format.print_string
" "; Format.print_flush
())
350 let mkstates states
= function
352 | Some states
-> states
354 let print_graph grp required_states res str
= function
355 A.Exists
(keep
,v
,phi
) -> ()
357 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
360 | A.Exists
(keep
,v
,phi
) -> ()
363 Printf.sprintf
"%s%s"
365 (Common.format_to_string
367 Pretty_print_ctl.pp_ctl
368 (P.print_predicate
, SUB.print_mvar
)
371 let file = (match !Flag.currentfile
with
372 None
-> "graphical_trace"
375 (if not
(List.mem
file !graph_stack) then
376 graph_stack := file :: !graph_stack);
377 let filename = Filename.temp_file
(file^
":") ".dot" in
378 Hashtbl.add
graph_hash file filename;
380 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
381 (match required_states
with
383 | Some required_states
->
384 (List.map (function s
-> (s
,"blue")) required_states
))
385 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
387 let print_graph_c grp required_states res
ctr phi
=
388 let str = "iter: "^
(string_of_int
!ctr) in
389 print_graph grp required_states res
str phi
391 (* ---------------------------------------------------------------------- *)
393 (* ---------------------------------------------------------------------- *)
396 (* ************************* *)
398 (* ************************* *)
403 | A.NegSubst
(x,_
) -> x
409 | A.NegSubst
(_
,x) -> x
412 let eq_subBy eqx eqv sub sub'
=
413 match (sub
,sub'
) with
414 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
415 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
420 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
422 let eq_subst th th'
= setequalBy eq_sub th th'
;;
424 let merge_subBy eqx
(===) (>+<) sub sub'
=
425 (* variable part is guaranteed to be the same *)
426 match (sub
,sub'
) with
427 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
429 then Some
[A.Subst
(x, v
>+< v'
)]
431 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
433 then Some
[A.Subst
(x'
,v'
)]
435 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
437 then Some
[A.Subst
(x,v
)]
439 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
442 let merged = v
>+< v'
in
443 if merged = v
&& merged = v'
444 then Some
[A.NegSubst
(x,v
>+< v'
)]
446 (* positions are compatible, but not identical. keep apart. *)
447 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
448 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
452 let merge_sub sub sub'
=
453 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
455 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
457 (* NOTE: we sort by using the generic "compare" on (meta-)variable
458 * names; we could also require a definition of compare for meta-variables
459 * or substitutions but that seems like overkill for sorting
461 let clean_subst theta
=
465 let res = compare
(dom_sub s
) (dom_sub s'
) in
469 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
470 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
471 | _
-> compare
(ran_sub s
) (ran_sub s'
)
474 let rec loop = function
476 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
477 loop (A.Subst
(x,v
)::rest
)
478 | x::xs
-> x::(loop xs
) in
481 let top_subst = [];; (* Always TRUE subst. *)
483 (* Split a theta in two parts: one with (only) "x" and one without *)
485 let split_subst theta
x =
486 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
488 exception SUBST_MISMATCH
489 let conj_subst theta theta'
=
490 match (theta
,theta'
) with
491 | ([],_
) -> Some theta'
492 | (_
,[]) -> Some theta
494 let rec classify = function
496 | [x] -> [(dom_sub x,[x])]
498 (match classify xs
with
499 ((nm
,y
)::ys
) as res ->
502 else (dom_sub x,[x])::res
503 | _
-> failwith
"not possible") in
504 let merge_all theta theta'
=
511 match (merge_sub sub sub'
) with
512 Some subs
-> subs
@ rest
513 | _
-> raise SUBST_MISMATCH
)
516 let rec loop = function
518 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
520 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
521 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
522 (match compare
x y
with
523 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
524 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
525 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
526 | _
-> failwith
"not possible") in
527 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
528 with SUBST_MISMATCH
-> None
531 (* theta' must be a subset of theta *)
532 let conj_subst_none theta theta'
=
533 match (theta
,theta'
) with
534 | (_
,[]) -> Some theta
537 let rec classify = function
539 | [x] -> [(dom_sub x,[x])]
541 (match classify xs
with
542 ((nm
,y
)::ys
) as res ->
545 else (dom_sub x,[x])::res
546 | _
-> failwith
"not possible") in
547 let merge_all theta theta'
=
554 match (merge_sub sub sub'
) with
555 Some subs
-> subs
@ rest
556 | _
-> raise SUBST_MISMATCH
)
559 let rec loop = function
561 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
562 | ([],ctheta'
) -> raise SUBST_MISMATCH
563 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
564 (match compare
x y
with
565 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
566 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
567 | 1 -> raise SUBST_MISMATCH
568 | _
-> failwith
"not possible") in
569 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
570 with SUBST_MISMATCH
-> None
575 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
576 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
579 (* Turn a (big) theta into a list of (small) thetas *)
580 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
583 (* ************************* *)
585 (* ************************* *)
587 (* Always TRUE witness *)
588 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
590 let eq_wit wit wit'
= wit
= wit'
;;
592 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
593 let res = unionBy compare
(=) wit wit'
in
594 let anynegwit = (* if any is neg, then all are *)
595 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
597 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
600 let negate_wit wit
= A.NegWit wit
(*
602 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
603 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
606 let negate_wits wits
=
607 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
610 let anynegwit = (* if any is neg, then all are *)
611 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
615 function (s
,th
,wit
) ->
616 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
619 (* ************************* *)
621 (* ************************* *)
623 (* Triples are equal when the constituents are equal *)
624 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
625 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
627 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
629 let normalize trips
=
631 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
635 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
636 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
637 let triples_conj trips trips'
=
638 let (trips
,shared
,trips'
) =
639 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
642 List.partition (function t
-> List.mem t trips'
) trips
in
644 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
645 (trips,shared
,trips'
)
646 else (trips,[],trips'
) in
647 foldl (* returns a set - setify inlined *)
649 function (s1
,th1
,wit1
) ->
652 function (s2
,th2
,wit2
) ->
654 (match (conj_subst th1 th2
) with
656 let t = (s1
,th
,union_wit wit1 wit2
) in
657 if List.mem
t rest
then rest
else t::rest
664 (* ignore the state in the right argument. always pretend it is the same as
666 (* env on right has to be a subset of env on left *)
667 let triples_conj_none trips trips'
=
668 let (trips,shared
,trips'
) =
669 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
672 List.partition (function t -> List.mem
t trips'
) trips in
674 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
675 (trips,shared
,trips'
)
676 else (trips,[],trips'
) in
677 foldl (* returns a set - setify inlined *)
679 function (s1
,th1
,wit1
) ->
682 function (s2
,th2
,wit2
) ->
683 match (conj_subst_none th1 th2
) with
685 let t = (s1
,th
,union_wit wit1 wit2
) in
686 if List.mem
t rest
then rest
else t::rest
694 let triples_conj_AW trips trips'
=
695 let (trips,shared
,trips'
) =
696 if false && !pTRIPLES_CONJ_OPT
699 List.partition (function t -> List.mem
t trips'
) trips in
701 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
702 (trips,shared
,trips'
)
703 else (trips,[],trips'
) in
704 foldl (* returns a set - setify inlined *)
706 function (s1
,th1
,wit1
) ->
709 function (s2
,th2
,wit2
) ->
711 (match (conj_subst th1 th2
) with
713 let t = (s1
,th
,union_wit wit1 wit2
) in
714 if List.mem
t rest
then rest
else t::rest
721 (* *************************** *)
722 (* NEGATION (NegState style) *)
723 (* *************************** *)
725 (* Constructive negation at the state level *)
728 | NegState
of 'a list
731 let compatible_states = function
732 (PosState s1
, PosState s2
) ->
733 if s1
= s2
then Some
(PosState s1
) else None
734 | (PosState s1
, NegState s2
) ->
735 if List.mem s1 s2
then None
else Some
(PosState s1
)
736 | (NegState s1
, PosState s2
) ->
737 if List.mem s2 s1
then None
else Some
(PosState s2
)
738 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
741 (* Conjunction on triples with "special states" *)
742 let triples_state_conj trips trips'
=
743 let (trips,shared
,trips'
) =
744 if !pTRIPLES_CONJ_OPT
747 List.partition (function t -> List.mem
t trips'
) trips in
749 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
750 (trips,shared
,trips'
)
751 else (trips,[],trips'
) in
754 function (s1
,th1
,wit1
) ->
757 function (s2
,th2
,wit2
) ->
758 match compatible_states(s1
,s2
) with
760 (match (conj_subst th1 th2
) with
762 let t = (s
,th
,union_wit wit1 wit2
) in
763 if List.mem
t rest
then rest
else t::rest
770 let triple_negate (s
,th
,wits
) =
771 let negstates = (NegState
[s
],top_subst,top_wit) in
772 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
773 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
774 negstates :: (negths @ negwits) (* all different *)
776 (* FIX ME: it is not necessary to do full conjunction *)
777 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
778 if !pTRIPLES_COMPLEMENT_OPT
780 (let cleanup (s
,th
,wit
) =
782 PosState s'
-> [(s'
,th
,wit
)]
784 assert (th
=top_subst);
785 assert (wit
=top_wit);
786 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
787 let (simple
,complex
) =
788 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
790 let (simple
,complex
) =
791 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
793 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
794 top_subst,top_wit)] in
796 else ([(NegState
[],top_subst,top_wit)],trips) in
797 let rec compl trips =
800 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
801 let compld = (compl complex
) in
802 let compld = concatmap cleanup compld in
805 let negstates (st
,th
,wits
) =
806 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
807 let negths (st
,th
,wits
) =
808 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
809 let negwits (st
,th
,wits
) =
810 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
812 [] -> map (function st
-> (st
,top_subst,top_wit)) states
818 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
819 (negstates x @ negths x @ negwits x) xs
)
822 let triple_negate (s
,th
,wits
) =
823 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
824 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
825 ([s
], negths @ negwits) (* all different *)
827 let print_compl_state str (n
,p
) =
828 Printf.printf
"%s neg: " str;
830 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
835 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
837 then map (function st
-> (st
,top_subst,top_wit)) states
839 let cleanup (neg
,pos
) =
841 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
842 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
844 let trips = List.sort
state_compare trips in
845 let all_negated = List.map triple_negate trips in
846 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
847 let (pos1conj
,pos1keep
) =
848 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
849 let (pos2conj
,pos2keep
) =
850 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
851 (Common.union_set neg1 neg2
,
852 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
853 let rec inner_loop = function
854 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
856 let rec outer_loop = function
858 | l
-> outer_loop (inner_loop l
) in
859 cleanup (outer_loop all_negated)
861 (* ********************************** *)
862 (* END OF NEGATION (NegState style) *)
863 (* ********************************** *)
865 (* now this is always true, so we could get rid of it *)
866 let something_dropped = ref true
868 let triples_union trips trips'
=
869 (*unionBy compare eq_trip trips trips';;*)
870 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
872 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
873 Then, the following says that since the first is a more restrictive
874 environment and has fewer witnesses, then it should be dropped. But having
875 fewer witnesses is not necessarily less informative than having more,
876 because fewer witnesses can mean the absence of the witness-causing thing.
877 So the fewer witnesses have to be kept around.
878 subseteq changed to = to make it hopefully work
883 something_dropped := false;
885 then (something_dropped := true; trips)
887 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
890 (match conj_subst th1 th2
with
893 then if (*subseteq*) wit1
= wit2
then 1 else 0
896 then if (*subseteq*) wit2
= wit1
then (-1) else 0
900 let rec first_loop second
= function
902 | x::xs
-> first_loop (second_loop
x second
) xs
903 and second_loop
x = function
906 match subsumes x y
with
907 1 -> something_dropped := true; all
908 | (-1) -> second_loop
x ys
909 | _
-> y
::(second_loop
x ys
) in
910 first_loop trips trips'
912 else unionBy compare
eq_trip trips trips'
915 let triples_witness x unchecked not_keep
trips =
916 let anyneg = (* if any is neg, then all are *)
917 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
918 let anynegwit = (* if any is neg, then all are *)
919 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
920 let allnegwit = (* if any is neg, then all are *)
921 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
923 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
927 function (s
,th
,wit
) as t ->
928 let (th_x
,newth
) = split_subst th
x in
931 (* one consider whether if not not_keep is true, then we should
932 fail. but it could be that the variable is a used_after and
933 then it is the later rule that should fail and not this one *)
934 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
936 (SUB.print_mvar
x; Format.print_flush
();
937 print_state ": empty witness from" [t]);
939 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
940 (* see tests/nestseq for how neg bindings can come up even
941 without eg partial matches
942 (* negated substitution only allowed with negwits.
944 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
947 (print_generic_substitution l
; Format.print_newline
();
948 failwith
"unexpected negative binding with positive witnesses")*)
951 if unchecked
or not_keep
954 if anynegwit wit
&& allnegwit wit
955 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
956 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
959 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
965 (* ---------------------------------------------------------------------- *)
966 (* SAT - Model Checking Algorithm for CTL-FVex *)
968 (* TODO: Implement _all_ operators (directly) *)
969 (* ---------------------------------------------------------------------- *)
972 (* ************************************* *)
973 (* The SAT algorithm and special helpers *)
974 (* ************************************* *)
976 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
978 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
981 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
983 A.FORWARD
-> G.predecessors grp s
984 | A.BACKWARD
-> G.successors grp s
) in
985 setify (concatmap exp y
)
990 let pre_forall dir
(grp
,_
,states
) y all reqst
=
993 None
-> true | Some reqst
-> List.mem s reqst
in
996 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
999 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1002 (function p
-> (p
,succ grp p
))
1005 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1006 (* would a hash table be more efficient? *)
1007 let all = List.sort
state_compare all in
1008 let rec up_nodes child s
= function
1010 | (s1
,th
,wit
)::xs
->
1011 (match compare s1 child
with
1012 -1 -> up_nodes child s xs
1013 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1015 let neighbor_triples =
1018 function (s
,children
) ->
1022 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1026 match neighbor_triples with
1030 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1032 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1035 None
-> true | Some reqst
-> List.mem s reqst
in
1038 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1041 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1044 (function p
-> (p
,succ grp p
))
1047 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1048 (* would a hash table be more efficient? *)
1049 let all = List.sort
state_compare all in
1050 let rec up_nodes child s
= function
1052 | (s1
,th
,wit
)::xs
->
1053 (match compare s1 child
with
1054 -1 -> up_nodes child s xs
1055 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1057 let neighbor_triples =
1060 function (s
,children
) ->
1063 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1066 match neighbor_triples with
1068 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1070 (* drop_negwits will call setify *)
1071 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1073 let satAX dir m s reqst
= pre_forall dir m s s reqst
1076 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1077 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1078 (*Printf.printf "EU\n";
1079 let ctr = ref 0 in*)
1084 (*let ctr = ref 0 in*)
1087 let rec f y new_info
=
1093 print_graph y ctr;*)
1094 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1095 let res = triples_union first y
in
1096 let new_info = setdiff res y
in
1097 (*Printf.printf "iter %d res %d new_info %d\n"
1098 !ctr (List.length res) (List.length new_info);
1099 print_state "res" res;
1100 print_state "new_info" new_info;
1108 print_graph y ctr;*)
1109 let pre = pre_exist dir m y reqst
in
1110 triples_union s2
(triples_conj s1
pre) in
1114 (* EF phi == E[true U phi] *)
1115 let satEF dir m s2 reqst
=
1117 (*let ctr = ref 0 in*)
1120 let rec f y
new_info =
1126 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1127 let first = pre_exist dir m
new_info reqst
in
1128 let res = triples_union first y
in
1129 let new_info = setdiff res y
in
1130 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1131 (if dir = A.BACKWARD then "reachable" else "real ef")
1132 !ctr (List.length res) (List.length new_info);
1133 print_state "new info" new_info;
1140 let pre = pre_exist dir m y reqst
in
1141 triples_union s2
pre in
1145 type ('
pred,'anno
) auok
=
1146 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1148 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1149 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1155 (*let ctr = ref 0 in*)
1157 if !Flag_ctl.loop_in_src_code
1162 let rec f y newinfo
=
1168 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1172 try Some
(pre_forall dir m
new_info y reqst
)
1177 match triples_conj s1
pre with
1180 (*print_state "s1" s1;
1181 print_state "pre" pre;
1182 print_state "first" first;*)
1183 let res = triples_union first y
in
1185 if not
!something_dropped
1187 else setdiff res y
in
1189 "iter %d res %d new_info %d\n"
1190 !ctr (List.length res) (List.length new_info);
1195 if !Flag_ctl.loop_in_src_code
1199 fix (function s1 -> function s2 ->
1200 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1201 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1202 subseteq s1 s2) in for popl *)
1207 let pre = pre_forall dir m y y reqst
in
1208 triples_union s2 (triples_conj s1 pre) in
1213 (* reqst could be the states of s1 *)
1215 let lstates = mkstates states reqst in
1216 let initial_removed =
1217 triples_complement lstates (triples_union s1 s2) in
1218 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1219 let rec loop base removed =
1221 triples_conj base (pre_exist dir m removed reqst) in
1223 triples_conj base (triples_complement lstates new_removed) in
1224 if supseteq new_base base
1225 then triples_union base s2
1226 else loop new_base new_removed in
1227 loop initial_base initial_removed *)
1229 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1235 This works extremely badly when the region is small and the end of the
1236 region is very ambiguous, eg free(x) ... x
1240 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1241 let ostates = Common.union_set (get_states s1) (get_states s2) in
1244 A.FORWARD -> G.successors grp
1245 | A.BACKWARD -> G.predecessors grp) in
1247 List.fold_left Common.union_set ostates (List.map succ ostates) in
1248 let negphi = triples_complement states s1 in
1249 let negpsi = triples_complement states s2 in
1250 triples_complement ostates
1251 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1254 (*let ctr = ref 0 in*)
1258 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1261 let pre = pre_forall dir m y y reqst
in
1262 (*print_state "pre" pre;*)
1263 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1264 triples_union s2 conj in
1265 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1266 (* drop wits on s1 represents that we don't want any witnesses from
1267 the case that infinitely loops, only from the case that gets
1268 out of the loop. s1 is like a guard. To see the problem, consider
1269 an example where both s1 and s2 match some code after the loop.
1270 we only want the witness from s2. *)
1271 setgfix f (triples_union (nub(drop_wits s1)) s2)
1274 let satAF dir m s reqst
=
1278 let rec f y newinfo
=
1283 let first = pre_forall dir m
new_info y reqst
in
1284 let res = triples_union first y
in
1285 let new_info = setdiff res y
in
1291 let pre = pre_forall dir m y y reqst
in
1292 triples_union s
pre in
1295 let satAG dir
((_
,_
,states) as m
) s reqst
=
1299 let pre = pre_forall dir m y y reqst
in
1300 triples_conj y
pre in
1303 let satEG dir
((_
,_
,states) as m
) s reqst
=
1307 let pre = pre_exist dir m y reqst
in
1308 triples_conj y
pre in
1311 (* **************************************************************** *)
1312 (* Inner And - a way of dealing with multiple matches within a node *)
1313 (* **************************************************************** *)
1314 (* applied to the result of matching a node. collect witnesses when the
1315 states and environments are the same *)
1317 let inner_and trips =
1318 let rec loop = function
1320 | (s
,th
,w
)::trips ->
1321 let (cur
,acc
) = loop trips in
1323 (s'
,_
,_
)::_
when s
= s'
->
1324 let rec loop'
= function
1326 | ((_
,th'
,w'
) as t'
)::ts'
->
1327 (match conj_subst th th'
with
1328 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1329 | None
-> t'
::(loop' ts'
)) in
1331 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1333 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1336 (* *************** *)
1337 (* Partial matches *)
1338 (* *************** *)
1340 let filter_conj states unwanted partial_matches
=
1342 triples_conj (triples_complement states (unwitify unwanted
))
1344 triples_conj (unwitify x) (triples_complement states x)
1346 let strict_triples_conj strict
states trips trips'
=
1347 let res = triples_conj trips trips'
in
1348 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1350 let fail_left = filter_conj states trips trips'
in
1351 let fail_right = filter_conj states trips'
trips in
1352 let ors = triples_union fail_left fail_right in
1353 triples_union res ors
1356 let strict_triples_conj_none strict
states trips trips'
=
1357 let res = triples_conj_none trips trips'
in
1358 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1360 let fail_left = filter_conj states trips trips'
in
1361 let fail_right = filter_conj states trips'
trips in
1362 let ors = triples_union fail_left fail_right in
1363 triples_union res ors
1366 let left_strict_triples_conj strict
states trips trips'
=
1367 let res = triples_conj trips trips'
in
1368 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1370 let fail_left = filter_conj states trips trips'
in
1371 triples_union res fail_left
1374 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1375 let res = op dir m
trips required_states
in
1376 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1378 let states = mkstates states required_states
in
1379 let fail = filter_conj states res (failop dir m
trips required_states
) in
1380 triples_union res fail
1383 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1385 let res = op dir m
trips trips' required_states
in
1386 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1388 let states = mkstates states required_states
in
1389 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1390 triples_union res fail
1393 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1394 required_states
print_graph =
1395 match op dir m
trips trips' required_states
print_graph with
1397 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1399 let states = mkstates states required_states
in
1401 filter_conj states res (failop dir m
trips' required_states
) in
1402 AUok
(triples_union res fail)
1404 | AUfailed
res -> AUfailed
res
1406 (* ********************* *)
1407 (* Environment functions *)
1408 (* ********************* *)
1410 let drop_wits required_states s phi
=
1411 match required_states
with
1413 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1416 let print_required required
=
1419 Format.print_string
"{";
1422 print_generic_substitution reqd
; Format.print_newline
())
1424 Format.print_string
"}";
1425 Format.print_newline
())
1430 let extend_required trips required
=
1431 if !Flag_ctl.partial_match
1434 if !pREQUIRED_ENV_OPT
1440 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1442 let envs = if List.mem
[] envs then [] else envs in
1443 match (envs,required
) with
1447 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1452 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1459 match conj_subst t r
with
1460 None
-> rest
| Some th
-> add th rest
)
1464 with Too_long
-> envs :: required
)
1465 | (envs,_
) -> envs :: required
1468 let drop_required v required
=
1469 if !pREQUIRED_ENV_OPT
1476 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1478 (* check whether an entry has become useless *)
1479 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1482 (* no idea how to write this function ... *)
1484 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1486 let satLabel label required p
=
1488 if !pSATLABEL_MEMO_OPT
1491 let states_subs = Hashtbl.find
memo_label p
in
1492 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1495 let triples = setify(label p
) in
1496 Hashtbl.add memo_label p
1497 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1499 else setify(label p
) in
1501 (if !pREQUIRED_ENV_OPT
1505 function ((s
,th
,_
) as t) ->
1507 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1514 let get_required_states l
=
1515 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1517 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1520 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1521 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1523 match required_states
with
1528 A.FORWARD
-> G.successors
1529 | A.BACKWARD
-> G.predecessors in
1530 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1533 let reachable_table =
1534 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1536 (* like satEF, but specialized for get_reachable *)
1537 let reachsatEF dir
(grp
,_
,_
) s2 =
1539 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1540 let union = unionBy compare
(=) in
1541 let rec f y
= function
1544 let (pre_collected
,new_info) =
1545 List.partition (function Common.Left
x -> true | _
-> false)
1548 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1549 with Not_found
-> Common.Right
x)
1554 function Common.Left
x -> union x rest
1555 | _
-> failwith
"not possible")
1559 (function Common.Right
x -> x | _
-> failwith
"not possible")
1561 let first = inner_setify (concatmap (dirop grp
) new_info) in
1562 let new_info = setdiff first y in
1563 let res = new_info @ y in
1565 List.rev
(f s2 s2) (* put root first *)
1567 let get_reachable dir m required_states
=
1568 match required_states
with
1575 if List.mem cur rest
1579 (try Hashtbl.find
reachable_table (cur
,dir
)
1582 let states = reachsatEF dir m
[cur
] in
1583 Hashtbl.add reachable_table (cur
,dir
) states;
1592 Printf.sprintf
"_c%d" c
1594 (* **************************** *)
1595 (* End of environment functions *)
1596 (* **************************** *)
1598 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1600 let rec satloop unchecked required required_states
1601 ((grp
,label,states) as m
) phi env
=
1602 let rec loop unchecked required required_states phi
=
1603 (*Common.profile_code "satloop" (fun _ -> *)
1607 | A.True
-> triples_top states
1608 | A.Pred
(p
) -> satLabel label required p
1609 | A.Uncheck
(phi1
) ->
1610 let unchecked = if !pUNCHECK_OPT then true else false in
1611 loop unchecked required required_states phi1
1613 let phires = loop unchecked required required_states phi
in
1615 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1616 triples_complement (mkstates states required_states
)
1618 | A.Or
(phi1
,phi2
) ->
1620 (loop unchecked required required_states phi1
)
1621 (loop unchecked required required_states phi2
)
1622 | A.SeqOr
(phi1
,phi2
) ->
1623 let res1 = loop unchecked required required_states phi1
in
1624 let res2 = loop unchecked required required_states phi2
in
1625 let res1neg = unwitify res1 in
1628 (triples_complement (mkstates states required_states
) res1neg)
1630 | A.And
(strict
,phi1
,phi2
) ->
1631 (* phi1 is considered to be more likely to be [], because of the
1632 definition of asttoctl. Could use heuristics such as the size of
1634 let pm = !Flag_ctl.partial_match
in
1635 (match (pm,loop unchecked required required_states phi1
) with
1636 (false,[]) when !pLazyOpt -> []
1638 let new_required = extend_required phi1res required
in
1639 let new_required_states = get_required_states phi1res
in
1640 (match (pm,loop unchecked new_required new_required_states phi2
)
1642 (false,[]) when !pLazyOpt -> []
1644 strict_triples_conj strict
1645 (mkstates states required_states
)
1647 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1648 (* phi2 can appear anywhere that is reachable *)
1649 let pm = !Flag_ctl.partial_match
in
1650 (match (pm,loop unchecked required required_states phi1
) with
1653 let new_required = extend_required phi1res required
in
1654 let new_required_states = get_required_states phi1res
in
1655 let new_required_states =
1656 get_reachable dir m
new_required_states in
1657 (match (pm,loop unchecked new_required new_required_states phi2
)
1659 (false,[]) -> phi1res
1662 [] -> (* !Flag_ctl.partial_match must be true *)
1666 let s = mkstates states required_states
in
1668 (function a
-> function b
->
1669 strict_triples_conj strict
s a
[b
])
1670 [List.hd phi2res
] (List.tl phi2res
)
1673 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1674 let s = mkstates states required_states
in
1676 (function a
-> function b
->
1677 strict_triples_conj strict
s a b
)
1681 "only one result allowed for the left arg of AndAny")))
1682 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1683 (* phi2 can appear anywhere that is reachable *)
1684 let pm = !Flag_ctl.partial_match
in
1685 (match (pm,loop unchecked required required_states phi1
) with
1688 let new_required = extend_required phi1res required
in
1689 let new_required_states = get_required_states phi1res
in
1690 let new_required_states =
1691 get_reachable dir m
new_required_states in
1692 (match (pm,loop unchecked new_required new_required_states phi2
)
1694 (false,[]) -> phi1res
1696 (* if there is more than one state, something about the
1697 environment has to ensure that the right triples of
1698 phi2 get associated with the triples of phi1.
1699 the asttoctl2 has to ensure that that is the case.
1700 these should thus be structural properties.
1701 env of phi2 has to be a proper subset of env of phi1
1702 to ensure all end up being consistent. no new triples
1703 should be generated. strict_triples_conj_none takes
1706 let s = mkstates states required_states
in
1709 function (st
,th
,_
) as phi2_elem
->
1711 triples_complement [st
] [(st
,th
,[])] in
1712 strict_triples_conj_none strict
s acc
1713 (phi2_elem
::inverse))
1715 | A.InnerAnd
(phi
) ->
1716 inner_and(loop unchecked required required_states phi
)
1718 let new_required_states =
1719 get_children_required_states dir m required_states
in
1720 satEX dir m
(loop unchecked required
new_required_states phi
)
1722 | A.AX
(dir
,strict
,phi
) ->
1723 let new_required_states =
1724 get_children_required_states dir m required_states
in
1725 let res = loop unchecked required
new_required_states phi
in
1726 strict_A1 strict
satAX satEX dir m
res required_states
1728 let new_required_states = get_reachable dir m required_states
in
1729 satEF dir m
(loop unchecked required
new_required_states phi
)
1731 | A.AF
(dir
,strict
,phi
) ->
1732 if !Flag_ctl.loop_in_src_code
1734 loop unchecked required required_states
1735 (A.AU
(dir
,strict
,A.True
,phi
))
1737 let new_required_states = get_reachable dir m required_states
in
1738 let res = loop unchecked required
new_required_states phi
in
1739 strict_A1 strict
satAF satEF dir m
res new_required_states
1741 let new_required_states = get_reachable dir m required_states
in
1742 satEG dir m
(loop unchecked required
new_required_states phi
)
1744 | A.AG
(dir
,strict
,phi
) ->
1745 let new_required_states = get_reachable dir m required_states
in
1746 let res = loop unchecked required
new_required_states phi
in
1747 strict_A1 strict
satAG satEF dir m
res new_required_states
1748 | A.EU
(dir
,phi1
,phi2
) ->
1749 let new_required_states = get_reachable dir m required_states
in
1750 (match loop unchecked required
new_required_states phi2
with
1751 [] when !pLazyOpt -> []
1753 let new_required = extend_required s2 required
in
1754 let s1 = loop unchecked new_required new_required_states phi1
in
1755 satEU dir m
s1 s2 new_required_states
1756 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1757 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1758 let new_required_states = get_reachable dir m required_states
in
1759 (match loop unchecked required
new_required_states phi2
with
1760 [] when !pLazyOpt -> []
1762 let new_required = extend_required s2 required
in
1763 let s1 = loop unchecked new_required new_required_states phi1
in
1764 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1765 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1766 (*Printf.printf "using AU\n"; flush stdout;*)
1767 let new_required_states = get_reachable dir m required_states
in
1768 (match loop unchecked required
new_required_states phi2
with
1769 [] when !pLazyOpt -> []
1771 let new_required = extend_required s2 required
in
1772 let s1 = loop unchecked new_required new_required_states phi1
in
1774 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1776 print_graph_c grp
new_required_states y ctr phi
) in
1779 | AUfailed tmp_res
->
1780 (* found a loop, have to try AW *)
1782 A[E[phi1 U phi2] & phi1 W phi2]
1783 the and is nonstrict *)
1784 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1785 (*Printf.printf "using AW\n"; flush stdout;*)
1788 (satEU dir m
s1 tmp_res
new_required_states
1789 (* no graph, for the moment *)
1792 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1794 | A.Implies
(phi1
,phi2
) ->
1795 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1796 | A.Exists
(keep
,v
,phi
) ->
1797 let new_required = drop_required v required
in
1798 triples_witness v
unchecked (not keep
)
1799 (loop unchecked new_required required_states phi
)
1800 | A.Let
(v
,phi1
,phi2
) ->
1801 (* should only be used when the properties unchecked, required,
1802 and required_states are known to be the same or at least
1803 compatible between all the uses. this is not checked. *)
1804 let res = loop unchecked required required_states phi1
in
1805 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1806 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1807 (* should only be used when the properties unchecked, required,
1808 and required_states are known to be the same or at least
1809 compatible between all the uses. this is not checked. *)
1810 (* doesn't seem to be used any more *)
1811 let new_required_states = get_reachable dir m required_states
in
1812 let res = loop unchecked required
new_required_states phi1
in
1813 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1815 let res = List.assoc v env
in
1817 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1819 | A.XX
(phi
) -> failwith
"should have been removed" in
1820 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1821 let res = drop_wits required_states
res phi
(* ) *) in
1822 print_graph grp required_states
res "" phi
;
1825 loop unchecked required required_states phi
1829 (* SAT with tracking *)
1830 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1831 ((_
,label,states) as m
) phi env
=
1832 let anno res children
= (annot lvl phi
res children
,res) in
1833 let satv unchecked required required_states phi0 env
=
1834 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1836 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1837 anno (satloop unchecked required required_states m phi env
) []
1841 A.False
-> anno [] []
1842 | A.True
-> anno (triples_top states) []
1844 Printf.printf
"label\n"; flush stdout
;
1845 anno (satLabel label required p
) []
1846 | A.Uncheck
(phi1
) ->
1847 let unchecked = if !pUNCHECK_OPT then true else false in
1848 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1849 Printf.printf
"uncheck\n"; flush stdout
;
1853 satv unchecked required required_states phi1 env
in
1854 Printf.printf
"not\n"; flush stdout
;
1855 anno (triples_complement (mkstates states required_states
) res) [child
]
1856 | A.Or
(phi1
,phi2
) ->
1858 satv unchecked required required_states phi1 env
in
1860 satv unchecked required required_states phi2 env
in
1861 Printf.printf
"or\n"; flush stdout
;
1862 anno (triples_union res1 res2) [child1
; child2
]
1863 | A.SeqOr
(phi1
,phi2
) ->
1865 satv unchecked required required_states phi1 env
in
1867 satv unchecked required required_states phi2 env
in
1869 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1870 Printf.printf
"seqor\n"; flush stdout
;
1871 anno (triples_union res1
1873 (triples_complement (mkstates states required_states
)
1877 | A.And
(strict
,phi1
,phi2
) ->
1878 let pm = !Flag_ctl.partial_match
in
1879 (match (pm,satv unchecked required required_states phi1 env
) with
1880 (false,(child1
,[])) ->
1881 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1882 | (_
,(child1
,res1)) ->
1883 let new_required = extend_required res1 required
in
1884 let new_required_states = get_required_states res1 in
1885 (match (pm,satv unchecked new_required new_required_states phi2
1887 (false,(child2
,[])) ->
1888 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1889 | (_
,(child2
,res2)) ->
1890 Printf.printf
"and\n"; flush stdout
;
1892 strict_triples_conj strict
1893 (mkstates states required_states
)
1895 anno res [child1
; child2
]))
1896 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1897 let pm = !Flag_ctl.partial_match
in
1898 (match (pm,satv unchecked required required_states phi1 env
) with
1899 (false,(child1
,[])) ->
1900 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1901 | (_
,(child1
,res1)) ->
1902 let new_required = extend_required res1 required
in
1903 let new_required_states = get_required_states res1 in
1904 let new_required_states =
1905 get_reachable dir m
new_required_states in
1906 (match (pm,satv unchecked new_required new_required_states phi2
1908 (false,(child2
,[])) ->
1909 Printf.printf
"andany\n"; flush stdout
;
1910 anno res1 [child1
;child2
]
1911 | (_
,(child2
,res2)) ->
1913 [] -> (* !Flag_ctl.partial_match must be true *)
1915 then anno [] [child1
; child2
]
1918 let s = mkstates states required_states
in
1920 (function a
-> function b
->
1921 strict_triples_conj strict
s a
[b
])
1922 [List.hd
res2] (List.tl
res2) in
1923 anno res [child1
; child2
]
1926 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1927 Printf.printf
"andany\n"; flush stdout
;
1929 let s = mkstates states required_states
in
1931 (function a
-> function b
->
1932 strict_triples_conj strict
s a b
)
1934 anno res [child1
; child2
]
1937 "only one result allowed for the left arg of AndAny")))
1938 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1939 let pm = !Flag_ctl.partial_match
in
1940 (match (pm,satv unchecked required required_states phi1 env
) with
1941 (false,(child1
,[])) ->
1942 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1943 | (_
,(child1
,res1)) ->
1944 let new_required = extend_required res1 required
in
1945 let new_required_states = get_required_states res1 in
1946 let new_required_states =
1947 get_reachable dir m
new_required_states in
1948 (match (pm,satv unchecked new_required new_required_states phi2
1950 (false,(child2
,[])) ->
1951 Printf.printf
"andany\n"; flush stdout
;
1952 anno res1 [child1
;child2
]
1953 | (_
,(child2
,res2)) ->
1955 let s = mkstates states required_states
in
1958 function (st
,th
,_
) as phi2_elem
->
1960 triples_complement [st
] [(st
,th
,[])] in
1961 strict_triples_conj_none strict
s acc
1962 (phi2_elem
::inverse))
1964 anno res [child1
; child2
]))
1965 | A.InnerAnd
(phi1
) ->
1966 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1967 Printf.printf
"uncheck\n"; flush stdout
;
1968 anno (inner_and res1) [child1
]
1970 let new_required_states =
1971 get_children_required_states dir m required_states
in
1973 satv unchecked required
new_required_states phi1 env
in
1974 Printf.printf
"EX\n"; flush stdout
;
1975 anno (satEX dir m
res required_states
) [child
]
1976 | A.AX
(dir
,strict
,phi1
) ->
1977 let new_required_states =
1978 get_children_required_states dir m required_states
in
1980 satv unchecked required
new_required_states phi1 env
in
1981 Printf.printf
"AX\n"; flush stdout
;
1982 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
1985 let new_required_states = get_reachable dir m required_states
in
1987 satv unchecked required
new_required_states phi1 env
in
1988 Printf.printf
"EF\n"; flush stdout
;
1989 anno (satEF dir m
res new_required_states) [child
]
1990 | A.AF
(dir
,strict
,phi1
) ->
1991 if !Flag_ctl.loop_in_src_code
1993 satv unchecked required required_states
1994 (A.AU
(dir
,strict
,A.True
,phi1
))
1997 (let new_required_states = get_reachable dir m required_states
in
1999 satv unchecked required
new_required_states phi1 env
in
2000 Printf.printf
"AF\n"; flush stdout
;
2002 strict_A1 strict
satAF satEF dir m
res new_required_states in
2005 let new_required_states = get_reachable dir m required_states
in
2007 satv unchecked required
new_required_states phi1 env
in
2008 Printf.printf
"EG\n"; flush stdout
;
2009 anno (satEG dir m
res new_required_states) [child
]
2010 | A.AG
(dir
,strict
,phi1
) ->
2011 let new_required_states = get_reachable dir m required_states
in
2013 satv unchecked required
new_required_states phi1 env
in
2014 Printf.printf
"AG\n"; flush stdout
;
2015 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2018 | A.EU
(dir
,phi1
,phi2
) ->
2019 let new_required_states = get_reachable dir m required_states
in
2020 (match satv unchecked required
new_required_states phi2 env
with
2022 Printf.printf
"EU\n"; flush stdout
;
2025 let new_required = extend_required res2 required
in
2027 satv unchecked new_required new_required_states phi1 env
in
2028 Printf.printf
"EU\n"; flush stdout
;
2029 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2031 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2032 failwith
"should not be used" (*
2033 let new_required_states = get_reachable dir m required_states in
2034 (match satv unchecked required new_required_states phi2 env with
2036 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2038 let new_required = extend_required res2 required in
2040 satv unchecked new_required new_required_states phi1 env in
2041 Printf.printf "AW %b\n" unchecked; flush stdout;
2043 strict_A2 strict satAW satEF dir m res1 res2
2044 new_required_states in
2045 anno res [child1; child2]) *)
2046 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2047 let new_required_states = get_reachable dir m required_states
in
2048 (match satv unchecked required
new_required_states phi2 env
with
2050 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2052 let new_required = extend_required s2 required
in
2054 satv unchecked new_required new_required_states phi1 env
in
2055 Printf.printf
"AU\n"; flush stdout
;
2057 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2058 (fun y str -> ()) in
2061 anno res [child1
; child2
]
2062 | AUfailed tmp_res
->
2063 (* found a loop, have to try AW *)
2065 A[E[phi1 U phi2] & phi1 W phi2]
2066 the and is nonstrict *)
2067 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2068 Printf.printf
"AW\n"; flush stdout
;
2071 (satEU dir m
s1 tmp_res
new_required_states
2072 (* no graph, for the moment *)
2076 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2077 anno res [child1
; child2
]))
2078 | A.Implies
(phi1
,phi2
) ->
2079 satv unchecked required required_states
2080 (A.Or
(A.Not phi1
,phi2
))
2082 | A.Exists
(keep
,v
,phi1
) ->
2083 let new_required = drop_required v required
in
2085 satv unchecked new_required required_states phi1 env
in
2086 Printf.printf
"exists\n"; flush stdout
;
2087 anno (triples_witness v
unchecked (not keep
) res) [child
]
2088 | A.Let
(v
,phi1
,phi2
) ->
2090 satv unchecked required required_states phi1 env
in
2092 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2093 anno res2 [child1
;child2
]
2094 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2095 let new_required_states = get_reachable dir m required_states
in
2097 satv unchecked required
new_required_states phi1 env
in
2099 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2100 anno res2 [child1
;child2
]
2102 Printf.printf
"Ref\n"; flush stdout
;
2103 let res = List.assoc v env
in
2106 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2109 | A.XX
(phi
) -> failwith
"should have been removed" in
2110 let res1 = drop_wits required_states
res phi
in
2114 print_required_states required_states
;
2115 print_state "after drop_wits" res1 end;
2120 let sat_verbose annotate maxlvl lvl m phi
=
2121 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2123 (* Type for annotations collected in a tree *)
2124 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2126 let sat_annotree annotate m phi
=
2127 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2128 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2132 let sat m phi = satloop m phi []
2136 let simpleanno l phi
res =
2138 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2139 print_generic_algo
(List.sort compare
res);
2140 Format.print_string
"\n------------------------------\n\n" in
2141 let pp_dir = function
2143 | A.BACKWARD
-> pp "^" in
2145 | A.False
-> pp "False"
2146 | A.True
-> pp "True"
2147 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2148 | A.Not
(phi
) -> pp "Not"
2149 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2150 | A.And
(_
,phi1
,phi2
) -> pp "And"
2151 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2152 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2153 | A.Or
(phi1
,phi2
) -> pp "Or"
2154 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2155 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2156 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2157 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2158 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2159 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2160 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2161 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2162 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2163 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2164 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2165 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2166 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2167 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2168 | A.Uncheck
(s) -> pp "Uncheck"
2169 | A.InnerAnd
(s) -> pp "InnerAnd"
2170 | A.XX
(phi1
) -> pp "XX"
2174 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2175 print a ctl formula more accurately if you want.
2176 Use the print_xxx provided in the different module to call
2177 Pretty_print_ctl.pp_ctl.
2180 let simpleanno2 l phi
res =
2182 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2183 Format.print_newline
();
2184 Format.print_string
"----------------------------------------------------";
2185 Format.print_newline
();
2186 print_generic_algo
(List.sort compare
res);
2187 Format.print_newline
();
2188 Format.print_string
"----------------------------------------------------";
2189 Format.print_newline
();
2190 Format.print_newline
();
2194 (* ---------------------------------------------------------------------- *)
2196 (* ---------------------------------------------------------------------- *)
2198 type optentry
= bool ref * string
2199 type options
= {label : optentry
; unch
: optentry
;
2200 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2202 reqenv
: optentry
; reqstates
: optentry
}
2205 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2206 unch
= (pUNCHECK_OPT,"uncheck_opt");
2207 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2208 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2209 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2210 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2211 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2212 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2216 ("label ",[options.label]);
2217 ("unch ",[options.unch
]);
2218 ("unch and label ",[options.label;options.unch
])]
2221 [("conj ", [options.conj]);
2222 ("compl1 ", [options.compl1
]);
2223 ("compl12 ", [options.compl1
;options.compl2
]);
2224 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2225 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2227 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2228 ("compl12 unch satl ",
2229 [options.compl1;options.compl2;options.unch;options.label]); *)
2230 ("conj/compl12 unch satl ",
2231 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2234 [("newinfo ", [options.newinfo
]);
2235 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2238 [("reqenv ", [options.reqenv
]);
2239 ("reqstates ", [options.reqstates
]);
2240 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2241 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2242 ("reqstates unch satl ",
2243 [options.reqstates;options.unch;options.label]);*)
2244 ("reqenv/states unch satl ",
2245 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2248 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2249 options.newinfo
;options.reqenv
;options.reqstates
]
2252 [("all ",all_options)]
2254 let all_options_but_path =
2255 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2256 options.reqenv
;options.reqstates
]
2258 let all_but_path = ("all but path ",all_options_but_path)
2261 [(satAW_calls, "satAW", ref 0);
2262 (satAU_calls, "satAU", ref 0);
2263 (satEF_calls, "satEF", ref 0);
2264 (satAF_calls, "satAF", ref 0);
2265 (satEG_calls, "satEG", ref 0);
2266 (satAG_calls, "satAG", ref 0);
2267 (satEU_calls, "satEU", ref 0)]
2271 (function (opt
,x) ->
2272 (opt
,x,ref 0.0,ref 0,
2273 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2274 [List.hd
all;all_but_path]
2275 (*(all@baseline@conjneg@path@required)*)
2279 let rec iter fn = function
2281 | n
-> let _ = fn() in
2282 (Hashtbl.clear
reachable_table;
2283 Hashtbl.clear
memo_label;
2287 let copy_to_stderr fl
=
2288 let i = open_in fl
in
2290 Printf.fprintf stderr
"%s\n" (input_line
i);
2292 try loop() with _ -> ();
2295 let bench_sat (_,_,states) fn =
2296 List.iter (function (opt
,_) -> opt
:= false) all_options;
2299 (function (name
,options,time
,trips,counter_info
) ->
2300 let iterct = !Flag_ctl.bench
in
2301 if !time
> float_of_int
timeout then time
:= -100.0;
2302 if not
(!time
= -100.0)
2305 Hashtbl.clear
reachable_table;
2306 Hashtbl.clear
memo_label;
2307 List.iter (function (opt
,_) -> opt
:= true) options;
2308 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2312 let bef = Sys.time
() in
2314 Common.timeout_function
timeout
2316 let bef = Sys.time
() in
2317 let res = iter fn iterct in
2318 let aft = Sys.time
() in
2319 time
:= !time
+. (aft -. bef);
2320 trips := !trips + !triples;
2322 (function (calls
,_,save_calls
) ->
2323 function (current_calls
,current_cfg
,current_max_cfg
) ->
2325 !current_calls
+ (!calls
- !save_calls
);
2326 if (!calls
- !save_calls
) > 0
2328 (let st = List.length
states in
2329 current_cfg
:= !current_cfg
+ st;
2330 if st > !current_max_cfg
2331 then current_max_cfg
:= st))
2332 counters counter_info
;
2337 let aft = Sys.time
() in
2339 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2343 List.iter (function (opt
,_) -> opt
:= false) options;
2348 Printf.fprintf stderr
"\n";
2352 (if not
(List.for_all
(function x -> x = res) rest
)
2354 (List.iter (print_state "a state") answers;
2355 Printf.printf
"something doesn't work\n");
2359 let iterct = !Flag_ctl.bench
in
2363 (function (name
,options,time
,trips,counter_info
) ->
2364 Printf.fprintf stderr
"%s Numbers: %f %d "
2365 name
(!time
/. (float_of_int
iterct)) !trips;
2367 (function (calls
,cfg
,max_cfg
) ->
2368 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2370 Printf.fprintf stderr
"\n")
2373 (* ---------------------------------------------------------------------- *)
2374 (* preprocessing: ignore irrelevant functions *)
2376 let preprocess (cfg
,_,_) label = function
2377 [] -> true (* no information, try everything *)
2379 let sz = G.size cfg
in
2380 let verbose_output pred = function
2382 Printf.printf
"did not find:\n";
2383 P.print_predicate
pred; Format.print_newline
()
2385 Printf.printf
"found:\n";
2386 P.print_predicate
pred; Format.print_newline
();
2387 Printf.printf
"but it was not enough\n" in
2388 let get_any verbose
x =
2390 try Hashtbl.find
memo_label x
2393 (let triples = label x in
2395 List.map (function (st,th
,_) -> (st,th
)) triples in
2396 Hashtbl.add memo_label x filtered;
2398 if verbose
then verbose_output x res;
2401 (* don't bother testing when there are more patterns than nodes *)
2402 if List.length l
> sz-2
2404 else List.for_all
(get_any false) l
in
2405 if List.exists
get_all l
2408 (if !Flag_ctl.verbose_match
2410 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2414 let filter_partial_matches trips =
2415 if !Flag_ctl.partial_match
2417 let anynegwit = (* if any is neg, then all are *)
2418 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2420 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2423 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2427 (* ---------------------------------------------------------------------- *)
2428 (* Main entry point for engine *)
2429 let sat m phi reqopt
=
2431 (match !Flag_ctl.steps
with
2432 None
-> step_count := 0
2433 | Some
x -> step_count := x);
2434 Hashtbl.clear
reachable_table;
2435 Hashtbl.clear
memo_label;
2436 let (x,label,states) = m
in
2437 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2439 ((* to drop when Yoann initialized this flag *)
2440 if List.exists
(G.extract_is_loop
x) states
2441 then Flag_ctl.loop_in_src_code
:= true;
2442 let m = (x,label,List.sort compare
states) in
2444 if(!Flag_ctl.verbose_ctl_engine
)
2446 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2447 if !Flag_ctl.bench
> 0
2451 let fn _ = satloop false [] None
m phi
[] in
2452 if !Flag_ctl.bench
> 0
2454 else Common.profile_code
"ctl" (fun _ -> fn()) in
2455 let res = filter_partial_matches res in
2457 Printf.printf "steps: start %d, stop %d\n"
2458 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2460 Printf.printf "triples: %d\n" !triples;
2461 print_state "final result" res;
2463 List.sort compare
res)
2465 (if !Flag_ctl.verbose_ctl_engine
2466 then Common.pr2
"missing something required";
2471 (* ********************************************************************** *)
2472 (* End of Module: CTL_ENGINE *)
2473 (* ********************************************************************** *)