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 (* How could we accomadate subterm constraints here??? *)
453 let merge_sub sub sub'
=
454 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
456 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
458 (* NOTE: we sort by using the generic "compare" on (meta-)variable
459 * names; we could also require a definition of compare for meta-variables
460 * or substitutions but that seems like overkill for sorting
462 let clean_subst theta
=
466 let res = compare
(dom_sub s
) (dom_sub s'
) in
470 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
471 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
472 | _
-> compare
(ran_sub s
) (ran_sub s'
)
475 let rec loop = function
477 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
478 loop (A.Subst
(x,v
)::rest
)
479 | x::xs
-> x::(loop xs
) in
482 let top_subst = [];; (* Always TRUE subst. *)
484 (* Split a theta in two parts: one with (only) "x" and one without *)
486 let split_subst theta
x =
487 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
489 exception SUBST_MISMATCH
490 let conj_subst theta theta'
=
491 match (theta
,theta'
) with
492 | ([],_
) -> Some theta'
493 | (_
,[]) -> Some theta
495 let rec classify = function
497 | [x] -> [(dom_sub x,[x])]
499 (match classify xs
with
500 ((nm
,y
)::ys
) as res ->
503 else (dom_sub x,[x])::res
504 | _
-> failwith
"not possible") in
505 let merge_all theta theta'
=
512 match (merge_sub sub sub'
) with
513 Some subs
-> subs
@ rest
514 | _
-> raise SUBST_MISMATCH
)
517 let rec loop = function
519 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
521 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
522 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
523 (match compare
x y
with
524 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
525 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
526 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
527 | _
-> failwith
"not possible") in
528 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
529 with SUBST_MISMATCH
-> None
532 (* theta' must be a subset of theta *)
533 let conj_subst_none theta theta'
=
534 match (theta
,theta'
) with
535 | (_
,[]) -> Some theta
538 let rec classify = function
540 | [x] -> [(dom_sub x,[x])]
542 (match classify xs
with
543 ((nm
,y
)::ys
) as res ->
546 else (dom_sub x,[x])::res
547 | _
-> failwith
"not possible") in
548 let merge_all theta theta'
=
555 match (merge_sub sub sub'
) with
556 Some subs
-> subs
@ rest
557 | _
-> raise SUBST_MISMATCH
)
560 let rec loop = function
562 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
563 | ([],ctheta'
) -> raise SUBST_MISMATCH
564 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
565 (match compare
x y
with
566 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
567 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
568 | 1 -> raise SUBST_MISMATCH
569 | _
-> failwith
"not possible") in
570 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
571 with SUBST_MISMATCH
-> None
576 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
577 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
580 (* Turn a (big) theta into a list of (small) thetas *)
581 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
584 (* ************************* *)
586 (* ************************* *)
588 (* Always TRUE witness *)
589 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
591 let eq_wit wit wit'
= wit
= wit'
;;
593 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
594 let res = unionBy compare
(=) wit wit'
in
595 let anynegwit = (* if any is neg, then all are *)
596 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
598 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
601 let negate_wit wit
= A.NegWit wit
(*
603 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
604 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
607 let negate_wits wits
=
608 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
611 let anynegwit = (* if any is neg, then all are *)
612 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
616 function (s
,th
,wit
) ->
617 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
620 (* ************************* *)
622 (* ************************* *)
624 (* Triples are equal when the constituents are equal *)
625 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
626 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
628 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
630 let normalize trips
=
632 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
636 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
637 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
638 let triples_conj trips trips'
=
639 let (trips
,shared
,trips'
) =
640 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
643 List.partition (function t
-> List.mem t trips'
) trips
in
645 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
646 (trips,shared
,trips'
)
647 else (trips,[],trips'
) in
648 foldl (* returns a set - setify inlined *)
650 function (s1
,th1
,wit1
) ->
653 function (s2
,th2
,wit2
) ->
655 (match (conj_subst th1 th2
) with
657 let t = (s1
,th
,union_wit wit1 wit2
) in
658 if List.mem
t rest
then rest
else t::rest
665 (* ignore the state in the right argument. always pretend it is the same as
667 (* env on right has to be a subset of env on left *)
668 let triples_conj_none trips trips'
=
669 let (trips,shared
,trips'
) =
670 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
673 List.partition (function t -> List.mem
t trips'
) trips in
675 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
676 (trips,shared
,trips'
)
677 else (trips,[],trips'
) in
678 foldl (* returns a set - setify inlined *)
680 function (s1
,th1
,wit1
) ->
683 function (s2
,th2
,wit2
) ->
684 match (conj_subst_none th1 th2
) with
686 let t = (s1
,th
,union_wit wit1 wit2
) in
687 if List.mem
t rest
then rest
else t::rest
695 let triples_conj_AW trips trips'
=
696 let (trips,shared
,trips'
) =
697 if false && !pTRIPLES_CONJ_OPT
700 List.partition (function t -> List.mem
t trips'
) trips in
702 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
703 (trips,shared
,trips'
)
704 else (trips,[],trips'
) in
705 foldl (* returns a set - setify inlined *)
707 function (s1
,th1
,wit1
) ->
710 function (s2
,th2
,wit2
) ->
712 (match (conj_subst th1 th2
) with
714 let t = (s1
,th
,union_wit wit1 wit2
) in
715 if List.mem
t rest
then rest
else t::rest
722 (* *************************** *)
723 (* NEGATION (NegState style) *)
724 (* *************************** *)
726 (* Constructive negation at the state level *)
729 | NegState
of 'a list
732 let compatible_states = function
733 (PosState s1
, PosState s2
) ->
734 if s1
= s2
then Some
(PosState s1
) else None
735 | (PosState s1
, NegState s2
) ->
736 if List.mem s1 s2
then None
else Some
(PosState s1
)
737 | (NegState s1
, PosState s2
) ->
738 if List.mem s2 s1
then None
else Some
(PosState s2
)
739 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
742 (* Conjunction on triples with "special states" *)
743 let triples_state_conj trips trips'
=
744 let (trips,shared
,trips'
) =
745 if !pTRIPLES_CONJ_OPT
748 List.partition (function t -> List.mem
t trips'
) trips in
750 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
751 (trips,shared
,trips'
)
752 else (trips,[],trips'
) in
755 function (s1
,th1
,wit1
) ->
758 function (s2
,th2
,wit2
) ->
759 match compatible_states(s1
,s2
) with
761 (match (conj_subst th1 th2
) with
763 let t = (s
,th
,union_wit wit1 wit2
) in
764 if List.mem
t rest
then rest
else t::rest
771 let triple_negate (s
,th
,wits
) =
772 let negstates = (NegState
[s
],top_subst,top_wit) in
773 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
774 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
775 negstates :: (negths @ negwits) (* all different *)
777 (* FIX ME: it is not necessary to do full conjunction *)
778 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
779 if !pTRIPLES_COMPLEMENT_OPT
781 (let cleanup (s
,th
,wit
) =
783 PosState s'
-> [(s'
,th
,wit
)]
785 assert (th
=top_subst);
786 assert (wit
=top_wit);
787 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
788 let (simple
,complex
) =
789 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
791 let (simple
,complex
) =
792 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
794 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
795 top_subst,top_wit)] in
797 else ([(NegState
[],top_subst,top_wit)],trips) in
798 let rec compl trips =
801 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
802 let compld = (compl complex
) in
803 let compld = concatmap cleanup compld in
806 let negstates (st
,th
,wits
) =
807 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
808 let negths (st
,th
,wits
) =
809 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
810 let negwits (st
,th
,wits
) =
811 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
813 [] -> map (function st
-> (st
,top_subst,top_wit)) states
819 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
820 (negstates x @ negths x @ negwits x) xs
)
823 let triple_negate (s
,th
,wits
) =
824 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
825 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
826 ([s
], negths @ negwits) (* all different *)
828 let print_compl_state str (n
,p
) =
829 Printf.printf
"%s neg: " str;
831 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
836 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
838 then map (function st
-> (st
,top_subst,top_wit)) states
840 let cleanup (neg
,pos
) =
842 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
843 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
845 let trips = List.sort
state_compare trips in
846 let all_negated = List.map triple_negate trips in
847 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
848 let (pos1conj
,pos1keep
) =
849 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
850 let (pos2conj
,pos2keep
) =
851 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
852 (Common.union_set neg1 neg2
,
853 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
854 let rec inner_loop = function
855 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
857 let rec outer_loop = function
859 | l
-> outer_loop (inner_loop l
) in
860 cleanup (outer_loop all_negated)
862 (* ********************************** *)
863 (* END OF NEGATION (NegState style) *)
864 (* ********************************** *)
866 (* now this is always true, so we could get rid of it *)
867 let something_dropped = ref true
869 let triples_union trips trips'
=
870 (*unionBy compare eq_trip trips trips';;*)
871 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
873 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
874 Then, the following says that since the first is a more restrictive
875 environment and has fewer witnesses, then it should be dropped. But having
876 fewer witnesses is not necessarily less informative than having more,
877 because fewer witnesses can mean the absence of the witness-causing thing.
878 So the fewer witnesses have to be kept around.
879 subseteq changed to = to make it hopefully work
884 something_dropped := false;
886 then (something_dropped := true; trips)
888 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
891 (match conj_subst th1 th2
with
894 then if (*subseteq*) wit1
= wit2
then 1 else 0
897 then if (*subseteq*) wit2
= wit1
then (-1) else 0
901 let rec first_loop second
= function
903 | x::xs
-> first_loop (second_loop
x second
) xs
904 and second_loop
x = function
907 match subsumes x y
with
908 1 -> something_dropped := true; all
909 | (-1) -> second_loop
x ys
910 | _
-> y
::(second_loop
x ys
) in
911 first_loop trips trips'
913 else unionBy compare
eq_trip trips trips'
916 let triples_witness x unchecked not_keep
trips =
917 let anyneg = (* if any is neg, then all are *)
918 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
919 let anynegwit = (* if any is neg, then all are *)
920 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
921 let allnegwit = (* if any is neg, then all are *)
922 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
924 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
928 function (s
,th
,wit
) as t ->
929 let (th_x
,newth
) = split_subst th
x in
932 (* one consider whether if not not_keep is true, then we should
933 fail. but it could be that the variable is a used_after and
934 then it is the later rule that should fail and not this one *)
935 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
937 (SUB.print_mvar
x; Format.print_flush
();
938 print_state ": empty witness from" [t]);
940 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
941 (* see tests/nestseq for how neg bindings can come up even
942 without eg partial matches
943 (* negated substitution only allowed with negwits.
945 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
948 (print_generic_substitution l
; Format.print_newline
();
949 failwith
"unexpected negative binding with positive witnesses")*)
952 if unchecked
or not_keep
955 if anynegwit wit
&& allnegwit wit
956 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
957 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
960 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
966 (* ---------------------------------------------------------------------- *)
967 (* SAT - Model Checking Algorithm for CTL-FVex *)
969 (* TODO: Implement _all_ operators (directly) *)
970 (* ---------------------------------------------------------------------- *)
973 (* ************************************* *)
974 (* The SAT algorithm and special helpers *)
975 (* ************************************* *)
977 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
979 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
982 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
984 A.FORWARD
-> G.predecessors grp s
985 | A.BACKWARD
-> G.successors grp s
) in
986 setify (concatmap exp y
)
991 let pre_forall dir
(grp
,_
,states
) y all reqst
=
994 None
-> true | Some reqst
-> List.mem s reqst
in
997 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1000 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1003 (function p
-> (p
,succ grp p
))
1006 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1007 (* would a hash table be more efficient? *)
1008 let all = List.sort
state_compare all in
1009 let rec up_nodes child s
= function
1011 | (s1
,th
,wit
)::xs
->
1012 (match compare s1 child
with
1013 -1 -> up_nodes child s xs
1014 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1016 let neighbor_triples =
1019 function (s
,children
) ->
1023 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1027 match neighbor_triples with
1031 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1033 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1036 None
-> true | Some reqst
-> List.mem s reqst
in
1039 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1042 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1045 (function p
-> (p
,succ grp p
))
1048 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1049 (* would a hash table be more efficient? *)
1050 let all = List.sort
state_compare all in
1051 let rec up_nodes child s
= function
1053 | (s1
,th
,wit
)::xs
->
1054 (match compare s1 child
with
1055 -1 -> up_nodes child s xs
1056 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1058 let neighbor_triples =
1061 function (s
,children
) ->
1064 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1067 match neighbor_triples with
1069 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1071 (* drop_negwits will call setify *)
1072 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1074 let satAX dir m s reqst
= pre_forall dir m s s reqst
1077 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1078 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1079 (*Printf.printf "EU\n";
1080 let ctr = ref 0 in*)
1085 (*let ctr = ref 0 in*)
1088 let rec f y new_info
=
1094 print_graph y ctr;*)
1095 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1096 let res = triples_union first y
in
1097 let new_info = setdiff res y
in
1098 (*Printf.printf "iter %d res %d new_info %d\n"
1099 !ctr (List.length res) (List.length new_info);
1100 print_state "res" res;
1101 print_state "new_info" new_info;
1109 print_graph y ctr;*)
1110 let pre = pre_exist dir m y reqst
in
1111 triples_union s2
(triples_conj s1
pre) in
1115 (* EF phi == E[true U phi] *)
1116 let satEF dir m s2 reqst
=
1118 (*let ctr = ref 0 in*)
1121 let rec f y
new_info =
1127 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1128 let first = pre_exist dir m
new_info reqst
in
1129 let res = triples_union first y
in
1130 let new_info = setdiff res y
in
1131 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1132 (if dir = A.BACKWARD then "reachable" else "real ef")
1133 !ctr (List.length res) (List.length new_info);
1134 print_state "new info" new_info;
1141 let pre = pre_exist dir m y reqst
in
1142 triples_union s2
pre in
1146 type ('
pred,'anno
) auok
=
1147 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1149 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1150 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1156 (*let ctr = ref 0 in*)
1158 if !Flag_ctl.loop_in_src_code
1163 let rec f y newinfo
=
1169 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1173 try Some
(pre_forall dir m
new_info y reqst
)
1178 match triples_conj s1
pre with
1181 (*print_state "s1" s1;
1182 print_state "pre" pre;
1183 print_state "first" first;*)
1184 let res = triples_union first y
in
1186 if not
!something_dropped
1188 else setdiff res y
in
1190 "iter %d res %d new_info %d\n"
1191 !ctr (List.length res) (List.length new_info);
1196 if !Flag_ctl.loop_in_src_code
1200 fix (function s1 -> function s2 ->
1201 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1202 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1203 subseteq s1 s2) in for popl *)
1208 let pre = pre_forall dir m y y reqst
in
1209 triples_union s2 (triples_conj s1 pre) in
1214 (* reqst could be the states of s1 *)
1216 let lstates = mkstates states reqst in
1217 let initial_removed =
1218 triples_complement lstates (triples_union s1 s2) in
1219 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1220 let rec loop base removed =
1222 triples_conj base (pre_exist dir m removed reqst) in
1224 triples_conj base (triples_complement lstates new_removed) in
1225 if supseteq new_base base
1226 then triples_union base s2
1227 else loop new_base new_removed in
1228 loop initial_base initial_removed *)
1230 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1236 This works extremely badly when the region is small and the end of the
1237 region is very ambiguous, eg free(x) ... x
1241 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1242 let ostates = Common.union_set (get_states s1) (get_states s2) in
1245 A.FORWARD -> G.successors grp
1246 | A.BACKWARD -> G.predecessors grp) in
1248 List.fold_left Common.union_set ostates (List.map succ ostates) in
1249 let negphi = triples_complement states s1 in
1250 let negpsi = triples_complement states s2 in
1251 triples_complement ostates
1252 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1255 (*let ctr = ref 0 in*)
1259 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1262 let pre = pre_forall dir m y y reqst
in
1263 (*print_state "pre" pre;*)
1264 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1265 triples_union s2 conj in
1266 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1267 (* drop wits on s1 represents that we don't want any witnesses from
1268 the case that infinitely loops, only from the case that gets
1269 out of the loop. s1 is like a guard. To see the problem, consider
1270 an example where both s1 and s2 match some code after the loop.
1271 we only want the witness from s2. *)
1272 setgfix f (triples_union (nub(drop_wits s1)) s2)
1275 let satAF dir m s reqst
=
1279 let rec f y newinfo
=
1284 let first = pre_forall dir m
new_info y reqst
in
1285 let res = triples_union first y
in
1286 let new_info = setdiff res y
in
1292 let pre = pre_forall dir m y y reqst
in
1293 triples_union s
pre in
1296 let satAG dir
((_
,_
,states) as m
) s reqst
=
1300 let pre = pre_forall dir m y y reqst
in
1301 triples_conj y
pre in
1304 let satEG dir
((_
,_
,states) as m
) s reqst
=
1308 let pre = pre_exist dir m y reqst
in
1309 triples_conj y
pre in
1312 (* **************************************************************** *)
1313 (* Inner And - a way of dealing with multiple matches within a node *)
1314 (* **************************************************************** *)
1315 (* applied to the result of matching a node. collect witnesses when the
1316 states and environments are the same *)
1318 let inner_and trips =
1319 let rec loop = function
1321 | (s
,th
,w
)::trips ->
1322 let (cur
,acc
) = loop trips in
1324 (s'
,_
,_
)::_
when s
= s'
->
1325 let rec loop'
= function
1327 | ((_
,th'
,w'
) as t'
)::ts'
->
1328 (match conj_subst th th'
with
1329 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1330 | None
-> t'
::(loop' ts'
)) in
1332 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1334 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1337 (* *************** *)
1338 (* Partial matches *)
1339 (* *************** *)
1341 let filter_conj states unwanted partial_matches
=
1343 triples_conj (triples_complement states (unwitify unwanted
))
1345 triples_conj (unwitify x) (triples_complement states x)
1347 let strict_triples_conj strict
states trips trips'
=
1348 let res = triples_conj trips trips'
in
1349 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1351 let fail_left = filter_conj states trips trips'
in
1352 let fail_right = filter_conj states trips'
trips in
1353 let ors = triples_union fail_left fail_right in
1354 triples_union res ors
1357 let strict_triples_conj_none strict
states trips trips'
=
1358 let res = triples_conj_none trips trips'
in
1359 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1361 let fail_left = filter_conj states trips trips'
in
1362 let fail_right = filter_conj states trips'
trips in
1363 let ors = triples_union fail_left fail_right in
1364 triples_union res ors
1367 let left_strict_triples_conj strict
states trips trips'
=
1368 let res = triples_conj trips trips'
in
1369 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1371 let fail_left = filter_conj states trips trips'
in
1372 triples_union res fail_left
1375 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1376 let res = op dir m
trips required_states
in
1377 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1379 let states = mkstates states required_states
in
1380 let fail = filter_conj states res (failop dir m
trips required_states
) in
1381 triples_union res fail
1384 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1386 let res = op dir m
trips trips' required_states
in
1387 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1389 let states = mkstates states required_states
in
1390 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1391 triples_union res fail
1394 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1395 required_states
print_graph =
1396 match op dir m
trips trips' required_states
print_graph with
1398 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1400 let states = mkstates states required_states
in
1402 filter_conj states res (failop dir m
trips' required_states
) in
1403 AUok
(triples_union res fail)
1405 | AUfailed
res -> AUfailed
res
1407 (* ********************* *)
1408 (* Environment functions *)
1409 (* ********************* *)
1411 let drop_wits required_states s phi
=
1412 match required_states
with
1414 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1417 let print_required required
=
1420 Format.print_string
"{";
1423 print_generic_substitution reqd
; Format.print_newline
())
1425 Format.print_string
"}";
1426 Format.print_newline
())
1431 let extend_required trips required
=
1432 if !Flag_ctl.partial_match
1435 if !pREQUIRED_ENV_OPT
1441 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1443 let envs = if List.mem
[] envs then [] else envs in
1444 match (envs,required
) with
1448 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1453 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1460 match conj_subst t r
with
1461 None
-> rest
| Some th
-> add th rest
)
1465 with Too_long
-> envs :: required
)
1466 | (envs,_
) -> envs :: required
1469 let drop_required v required
=
1470 if !pREQUIRED_ENV_OPT
1477 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1479 (* check whether an entry has become useless *)
1480 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1483 (* no idea how to write this function ... *)
1485 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1487 let satLabel label required p
=
1489 if !pSATLABEL_MEMO_OPT
1492 let states_subs = Hashtbl.find
memo_label p
in
1493 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1496 let triples = setify(label p
) in
1497 Hashtbl.add memo_label p
1498 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1500 else setify(label p
) in
1502 (if !pREQUIRED_ENV_OPT
1506 function ((s
,th
,_
) as t) ->
1508 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1515 let get_required_states l
=
1516 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1518 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1521 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1522 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1524 match required_states
with
1529 A.FORWARD
-> G.successors
1530 | A.BACKWARD
-> G.predecessors in
1531 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1534 let reachable_table =
1535 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1537 (* like satEF, but specialized for get_reachable *)
1538 let reachsatEF dir
(grp
,_
,_
) s2 =
1540 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1541 let union = unionBy compare
(=) in
1542 let rec f y
= function
1545 let (pre_collected
,new_info) =
1546 List.partition (function Common.Left
x -> true | _
-> false)
1549 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1550 with Not_found
-> Common.Right
x)
1555 function Common.Left
x -> union x rest
1556 | _
-> failwith
"not possible")
1560 (function Common.Right
x -> x | _
-> failwith
"not possible")
1562 let first = inner_setify (concatmap (dirop grp
) new_info) in
1563 let new_info = setdiff first y in
1564 let res = new_info @ y in
1566 List.rev
(f s2 s2) (* put root first *)
1568 let get_reachable dir m required_states
=
1569 match required_states
with
1576 if List.mem cur rest
1580 (try Hashtbl.find
reachable_table (cur
,dir
)
1583 let states = reachsatEF dir m
[cur
] in
1584 Hashtbl.add reachable_table (cur
,dir
) states;
1593 Printf.sprintf
"_c%d" c
1595 (* **************************** *)
1596 (* End of environment functions *)
1597 (* **************************** *)
1599 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1601 let rec satloop unchecked required required_states
1602 ((grp
,label,states) as m
) phi env
=
1603 let rec loop unchecked required required_states phi
=
1604 (*Common.profile_code "satloop" (fun _ -> *)
1608 | A.True
-> triples_top states
1609 | A.Pred
(p
) -> satLabel label required p
1610 | A.Uncheck
(phi1
) ->
1611 let unchecked = if !pUNCHECK_OPT then true else false in
1612 loop unchecked required required_states phi1
1614 let phires = loop unchecked required required_states phi
in
1616 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1617 triples_complement (mkstates states required_states
)
1619 | A.Or
(phi1
,phi2
) ->
1621 (loop unchecked required required_states phi1
)
1622 (loop unchecked required required_states phi2
)
1623 | A.SeqOr
(phi1
,phi2
) ->
1624 let res1 = loop unchecked required required_states phi1
in
1625 let res2 = loop unchecked required required_states phi2
in
1626 let res1neg = unwitify res1 in
1629 (triples_complement (mkstates states required_states
) res1neg)
1631 | A.And
(strict
,phi1
,phi2
) ->
1632 (* phi1 is considered to be more likely to be [], because of the
1633 definition of asttoctl. Could use heuristics such as the size of
1635 let pm = !Flag_ctl.partial_match
in
1636 (match (pm,loop unchecked required required_states phi1
) with
1637 (false,[]) when !pLazyOpt -> []
1639 let new_required = extend_required phi1res required
in
1640 let new_required_states = get_required_states phi1res
in
1641 (match (pm,loop unchecked new_required new_required_states phi2
)
1643 (false,[]) when !pLazyOpt -> []
1645 strict_triples_conj strict
1646 (mkstates states required_states
)
1648 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1649 (* phi2 can appear anywhere that is reachable *)
1650 let pm = !Flag_ctl.partial_match
in
1651 (match (pm,loop unchecked required required_states phi1
) with
1654 let new_required = extend_required phi1res required
in
1655 let new_required_states = get_required_states phi1res
in
1656 let new_required_states =
1657 get_reachable dir m
new_required_states in
1658 (match (pm,loop unchecked new_required new_required_states phi2
)
1660 (false,[]) -> phi1res
1663 [] -> (* !Flag_ctl.partial_match must be true *)
1667 let s = mkstates states required_states
in
1669 (function a
-> function b
->
1670 strict_triples_conj strict
s a
[b
])
1671 [List.hd phi2res
] (List.tl phi2res
)
1674 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1675 let s = mkstates states required_states
in
1677 (function a
-> function b
->
1678 strict_triples_conj strict
s a b
)
1682 "only one result allowed for the left arg of AndAny")))
1683 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1684 (* phi2 can appear anywhere that is reachable *)
1685 let pm = !Flag_ctl.partial_match
in
1686 (match (pm,loop unchecked required required_states phi1
) with
1689 let new_required = extend_required phi1res required
in
1690 let new_required_states = get_required_states phi1res
in
1691 let new_required_states =
1692 get_reachable dir m
new_required_states in
1693 (match (pm,loop unchecked new_required new_required_states phi2
)
1695 (false,[]) -> phi1res
1697 (* if there is more than one state, something about the
1698 environment has to ensure that the right triples of
1699 phi2 get associated with the triples of phi1.
1700 the asttoctl2 has to ensure that that is the case.
1701 these should thus be structural properties.
1702 env of phi2 has to be a proper subset of env of phi1
1703 to ensure all end up being consistent. no new triples
1704 should be generated. strict_triples_conj_none takes
1707 let s = mkstates states required_states
in
1710 function (st
,th
,_
) as phi2_elem
->
1712 triples_complement [st
] [(st
,th
,[])] in
1713 strict_triples_conj_none strict
s acc
1714 (phi2_elem
::inverse))
1716 | A.InnerAnd
(phi
) ->
1717 inner_and(loop unchecked required required_states phi
)
1719 let new_required_states =
1720 get_children_required_states dir m required_states
in
1721 satEX dir m
(loop unchecked required
new_required_states phi
)
1723 | A.AX
(dir
,strict
,phi
) ->
1724 let new_required_states =
1725 get_children_required_states dir m required_states
in
1726 let res = loop unchecked required
new_required_states phi
in
1727 strict_A1 strict
satAX satEX dir m
res required_states
1729 let new_required_states = get_reachable dir m required_states
in
1730 satEF dir m
(loop unchecked required
new_required_states phi
)
1732 | A.AF
(dir
,strict
,phi
) ->
1733 if !Flag_ctl.loop_in_src_code
1735 loop unchecked required required_states
1736 (A.AU
(dir
,strict
,A.True
,phi
))
1738 let new_required_states = get_reachable dir m required_states
in
1739 let res = loop unchecked required
new_required_states phi
in
1740 strict_A1 strict
satAF satEF dir m
res new_required_states
1742 let new_required_states = get_reachable dir m required_states
in
1743 satEG dir m
(loop unchecked required
new_required_states phi
)
1745 | A.AG
(dir
,strict
,phi
) ->
1746 let new_required_states = get_reachable dir m required_states
in
1747 let res = loop unchecked required
new_required_states phi
in
1748 strict_A1 strict
satAG satEF dir m
res new_required_states
1749 | A.EU
(dir
,phi1
,phi2
) ->
1750 let new_required_states = get_reachable dir m required_states
in
1751 (match loop unchecked required
new_required_states phi2
with
1752 [] when !pLazyOpt -> []
1754 let new_required = extend_required s2 required
in
1755 let s1 = loop unchecked new_required new_required_states phi1
in
1756 satEU dir m
s1 s2 new_required_states
1757 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1758 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1759 let new_required_states = get_reachable dir m required_states
in
1760 (match loop unchecked required
new_required_states phi2
with
1761 [] when !pLazyOpt -> []
1763 let new_required = extend_required s2 required
in
1764 let s1 = loop unchecked new_required new_required_states phi1
in
1765 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1766 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1767 (*Printf.printf "using AU\n"; flush stdout;*)
1768 let new_required_states = get_reachable dir m required_states
in
1769 (match loop unchecked required
new_required_states phi2
with
1770 [] when !pLazyOpt -> []
1772 let new_required = extend_required s2 required
in
1773 let s1 = loop unchecked new_required new_required_states phi1
in
1775 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1777 print_graph_c grp
new_required_states y ctr phi
) in
1780 | AUfailed tmp_res
->
1781 (* found a loop, have to try AW *)
1783 A[E[phi1 U phi2] & phi1 W phi2]
1784 the and is nonstrict *)
1785 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1786 (*Printf.printf "using AW\n"; flush stdout;*)
1789 (satEU dir m
s1 tmp_res
new_required_states
1790 (* no graph, for the moment *)
1793 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1795 | A.Implies
(phi1
,phi2
) ->
1796 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1797 | A.Exists
(keep
,v
,phi
) ->
1798 let new_required = drop_required v required
in
1799 triples_witness v
unchecked (not keep
)
1800 (loop unchecked new_required required_states phi
)
1801 | A.Let
(v
,phi1
,phi2
) ->
1802 (* should only be used when the properties unchecked, required,
1803 and required_states are known to be the same or at least
1804 compatible between all the uses. this is not checked. *)
1805 let res = loop unchecked required required_states phi1
in
1806 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1807 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1808 (* should only be used when the properties unchecked, required,
1809 and required_states are known to be the same or at least
1810 compatible between all the uses. this is not checked. *)
1811 (* doesn't seem to be used any more *)
1812 let new_required_states = get_reachable dir m required_states
in
1813 let res = loop unchecked required
new_required_states phi1
in
1814 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1816 let res = List.assoc v env
in
1818 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1820 | A.XX
(phi
) -> failwith
"should have been removed" in
1821 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1822 let res = drop_wits required_states
res phi
(* ) *) in
1823 print_graph grp required_states
res "" phi
;
1826 loop unchecked required required_states phi
1830 (* SAT with tracking *)
1831 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1832 ((_
,label,states) as m
) phi env
=
1833 let anno res children
= (annot lvl phi
res children
,res) in
1834 let satv unchecked required required_states phi0 env
=
1835 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1837 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1838 anno (satloop unchecked required required_states m phi env
) []
1842 A.False
-> anno [] []
1843 | A.True
-> anno (triples_top states) []
1845 Printf.printf
"label\n"; flush stdout
;
1846 anno (satLabel label required p
) []
1847 | A.Uncheck
(phi1
) ->
1848 let unchecked = if !pUNCHECK_OPT then true else false in
1849 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1850 Printf.printf
"uncheck\n"; flush stdout
;
1854 satv unchecked required required_states phi1 env
in
1855 Printf.printf
"not\n"; flush stdout
;
1856 anno (triples_complement (mkstates states required_states
) res) [child
]
1857 | A.Or
(phi1
,phi2
) ->
1859 satv unchecked required required_states phi1 env
in
1861 satv unchecked required required_states phi2 env
in
1862 Printf.printf
"or\n"; flush stdout
;
1863 anno (triples_union res1 res2) [child1
; child2
]
1864 | A.SeqOr
(phi1
,phi2
) ->
1866 satv unchecked required required_states phi1 env
in
1868 satv unchecked required required_states phi2 env
in
1870 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1871 Printf.printf
"seqor\n"; flush stdout
;
1872 anno (triples_union res1
1874 (triples_complement (mkstates states required_states
)
1878 | A.And
(strict
,phi1
,phi2
) ->
1879 let pm = !Flag_ctl.partial_match
in
1880 (match (pm,satv unchecked required required_states phi1 env
) with
1881 (false,(child1
,[])) ->
1882 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1883 | (_
,(child1
,res1)) ->
1884 let new_required = extend_required res1 required
in
1885 let new_required_states = get_required_states res1 in
1886 (match (pm,satv unchecked new_required new_required_states phi2
1888 (false,(child2
,[])) ->
1889 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1890 | (_
,(child2
,res2)) ->
1891 Printf.printf
"and\n"; flush stdout
;
1893 strict_triples_conj strict
1894 (mkstates states required_states
)
1896 anno res [child1
; child2
]))
1897 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1898 let pm = !Flag_ctl.partial_match
in
1899 (match (pm,satv unchecked required required_states phi1 env
) with
1900 (false,(child1
,[])) ->
1901 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1902 | (_
,(child1
,res1)) ->
1903 let new_required = extend_required res1 required
in
1904 let new_required_states = get_required_states res1 in
1905 let new_required_states =
1906 get_reachable dir m
new_required_states in
1907 (match (pm,satv unchecked new_required new_required_states phi2
1909 (false,(child2
,[])) ->
1910 Printf.printf
"andany\n"; flush stdout
;
1911 anno res1 [child1
;child2
]
1912 | (_
,(child2
,res2)) ->
1914 [] -> (* !Flag_ctl.partial_match must be true *)
1916 then anno [] [child1
; child2
]
1919 let s = mkstates states required_states
in
1921 (function a
-> function b
->
1922 strict_triples_conj strict
s a
[b
])
1923 [List.hd
res2] (List.tl
res2) in
1924 anno res [child1
; child2
]
1927 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1928 Printf.printf
"andany\n"; flush stdout
;
1930 let s = mkstates states required_states
in
1932 (function a
-> function b
->
1933 strict_triples_conj strict
s a b
)
1935 anno res [child1
; child2
]
1938 "only one result allowed for the left arg of AndAny")))
1939 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1940 let pm = !Flag_ctl.partial_match
in
1941 (match (pm,satv unchecked required required_states phi1 env
) with
1942 (false,(child1
,[])) ->
1943 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1944 | (_
,(child1
,res1)) ->
1945 let new_required = extend_required res1 required
in
1946 let new_required_states = get_required_states res1 in
1947 let new_required_states =
1948 get_reachable dir m
new_required_states in
1949 (match (pm,satv unchecked new_required new_required_states phi2
1951 (false,(child2
,[])) ->
1952 Printf.printf
"andany\n"; flush stdout
;
1953 anno res1 [child1
;child2
]
1954 | (_
,(child2
,res2)) ->
1956 let s = mkstates states required_states
in
1959 function (st
,th
,_
) as phi2_elem
->
1961 triples_complement [st
] [(st
,th
,[])] in
1962 strict_triples_conj_none strict
s acc
1963 (phi2_elem
::inverse))
1965 anno res [child1
; child2
]))
1966 | A.InnerAnd
(phi1
) ->
1967 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1968 Printf.printf
"uncheck\n"; flush stdout
;
1969 anno (inner_and res1) [child1
]
1971 let new_required_states =
1972 get_children_required_states dir m required_states
in
1974 satv unchecked required
new_required_states phi1 env
in
1975 Printf.printf
"EX\n"; flush stdout
;
1976 anno (satEX dir m
res required_states
) [child
]
1977 | A.AX
(dir
,strict
,phi1
) ->
1978 let new_required_states =
1979 get_children_required_states dir m required_states
in
1981 satv unchecked required
new_required_states phi1 env
in
1982 Printf.printf
"AX\n"; flush stdout
;
1983 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
1986 let new_required_states = get_reachable dir m required_states
in
1988 satv unchecked required
new_required_states phi1 env
in
1989 Printf.printf
"EF\n"; flush stdout
;
1990 anno (satEF dir m
res new_required_states) [child
]
1991 | A.AF
(dir
,strict
,phi1
) ->
1992 if !Flag_ctl.loop_in_src_code
1994 satv unchecked required required_states
1995 (A.AU
(dir
,strict
,A.True
,phi1
))
1998 (let new_required_states = get_reachable dir m required_states
in
2000 satv unchecked required
new_required_states phi1 env
in
2001 Printf.printf
"AF\n"; flush stdout
;
2003 strict_A1 strict
satAF satEF dir m
res new_required_states in
2006 let new_required_states = get_reachable dir m required_states
in
2008 satv unchecked required
new_required_states phi1 env
in
2009 Printf.printf
"EG\n"; flush stdout
;
2010 anno (satEG dir m
res new_required_states) [child
]
2011 | A.AG
(dir
,strict
,phi1
) ->
2012 let new_required_states = get_reachable dir m required_states
in
2014 satv unchecked required
new_required_states phi1 env
in
2015 Printf.printf
"AG\n"; flush stdout
;
2016 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2019 | A.EU
(dir
,phi1
,phi2
) ->
2020 let new_required_states = get_reachable dir m required_states
in
2021 (match satv unchecked required
new_required_states phi2 env
with
2023 Printf.printf
"EU\n"; flush stdout
;
2026 let new_required = extend_required res2 required
in
2028 satv unchecked new_required new_required_states phi1 env
in
2029 Printf.printf
"EU\n"; flush stdout
;
2030 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2032 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2033 failwith
"should not be used" (*
2034 let new_required_states = get_reachable dir m required_states in
2035 (match satv unchecked required new_required_states phi2 env with
2037 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2039 let new_required = extend_required res2 required in
2041 satv unchecked new_required new_required_states phi1 env in
2042 Printf.printf "AW %b\n" unchecked; flush stdout;
2044 strict_A2 strict satAW satEF dir m res1 res2
2045 new_required_states in
2046 anno res [child1; child2]) *)
2047 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2048 let new_required_states = get_reachable dir m required_states
in
2049 (match satv unchecked required
new_required_states phi2 env
with
2051 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2053 let new_required = extend_required s2 required
in
2055 satv unchecked new_required new_required_states phi1 env
in
2056 Printf.printf
"AU\n"; flush stdout
;
2058 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2059 (fun y str -> ()) in
2062 anno res [child1
; child2
]
2063 | AUfailed tmp_res
->
2064 (* found a loop, have to try AW *)
2066 A[E[phi1 U phi2] & phi1 W phi2]
2067 the and is nonstrict *)
2068 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2069 Printf.printf
"AW\n"; flush stdout
;
2072 (satEU dir m
s1 tmp_res
new_required_states
2073 (* no graph, for the moment *)
2077 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2078 anno res [child1
; child2
]))
2079 | A.Implies
(phi1
,phi2
) ->
2080 satv unchecked required required_states
2081 (A.Or
(A.Not phi1
,phi2
))
2083 | A.Exists
(keep
,v
,phi1
) ->
2084 let new_required = drop_required v required
in
2086 satv unchecked new_required required_states phi1 env
in
2087 Printf.printf
"exists\n"; flush stdout
;
2088 anno (triples_witness v
unchecked (not keep
) res) [child
]
2089 | A.Let
(v
,phi1
,phi2
) ->
2091 satv unchecked required required_states phi1 env
in
2093 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2094 anno res2 [child1
;child2
]
2095 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2096 let new_required_states = get_reachable dir m required_states
in
2098 satv unchecked required
new_required_states phi1 env
in
2100 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2101 anno res2 [child1
;child2
]
2103 Printf.printf
"Ref\n"; flush stdout
;
2104 let res = List.assoc v env
in
2107 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2110 | A.XX
(phi
) -> failwith
"should have been removed" in
2111 let res1 = drop_wits required_states
res phi
in
2115 print_required_states required_states
;
2116 print_state "after drop_wits" res1 end;
2121 let sat_verbose annotate maxlvl lvl m phi
=
2122 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2124 (* Type for annotations collected in a tree *)
2125 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2127 let sat_annotree annotate m phi
=
2128 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2129 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2133 let sat m phi = satloop m phi []
2137 let simpleanno l phi
res =
2139 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2140 print_generic_algo
(List.sort compare
res);
2141 Format.print_string
"\n------------------------------\n\n" in
2142 let pp_dir = function
2144 | A.BACKWARD
-> pp "^" in
2146 | A.False
-> pp "False"
2147 | A.True
-> pp "True"
2148 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2149 | A.Not
(phi
) -> pp "Not"
2150 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2151 | A.And
(_
,phi1
,phi2
) -> pp "And"
2152 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2153 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2154 | A.Or
(phi1
,phi2
) -> pp "Or"
2155 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2156 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2157 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2158 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2159 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2160 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2161 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2162 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2163 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2164 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2165 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2166 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2167 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2168 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2169 | A.Uncheck
(s) -> pp "Uncheck"
2170 | A.InnerAnd
(s) -> pp "InnerAnd"
2171 | A.XX
(phi1
) -> pp "XX"
2175 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2176 print a ctl formula more accurately if you want.
2177 Use the print_xxx provided in the different module to call
2178 Pretty_print_ctl.pp_ctl.
2181 let simpleanno2 l phi
res =
2183 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2184 Format.print_newline
();
2185 Format.print_string
"----------------------------------------------------";
2186 Format.print_newline
();
2187 print_generic_algo
(List.sort compare
res);
2188 Format.print_newline
();
2189 Format.print_string
"----------------------------------------------------";
2190 Format.print_newline
();
2191 Format.print_newline
();
2195 (* ---------------------------------------------------------------------- *)
2197 (* ---------------------------------------------------------------------- *)
2199 type optentry
= bool ref * string
2200 type options
= {label : optentry
; unch
: optentry
;
2201 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2203 reqenv
: optentry
; reqstates
: optentry
}
2206 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2207 unch
= (pUNCHECK_OPT,"uncheck_opt");
2208 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2209 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2210 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2211 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2212 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2213 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2217 ("label ",[options.label]);
2218 ("unch ",[options.unch
]);
2219 ("unch and label ",[options.label;options.unch
])]
2222 [("conj ", [options.conj]);
2223 ("compl1 ", [options.compl1
]);
2224 ("compl12 ", [options.compl1
;options.compl2
]);
2225 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2226 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2228 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2229 ("compl12 unch satl ",
2230 [options.compl1;options.compl2;options.unch;options.label]); *)
2231 ("conj/compl12 unch satl ",
2232 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2235 [("newinfo ", [options.newinfo
]);
2236 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2239 [("reqenv ", [options.reqenv
]);
2240 ("reqstates ", [options.reqstates
]);
2241 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2242 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2243 ("reqstates unch satl ",
2244 [options.reqstates;options.unch;options.label]);*)
2245 ("reqenv/states unch satl ",
2246 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2249 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2250 options.newinfo
;options.reqenv
;options.reqstates
]
2253 [("all ",all_options)]
2255 let all_options_but_path =
2256 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2257 options.reqenv
;options.reqstates
]
2259 let all_but_path = ("all but path ",all_options_but_path)
2262 [(satAW_calls, "satAW", ref 0);
2263 (satAU_calls, "satAU", ref 0);
2264 (satEF_calls, "satEF", ref 0);
2265 (satAF_calls, "satAF", ref 0);
2266 (satEG_calls, "satEG", ref 0);
2267 (satAG_calls, "satAG", ref 0);
2268 (satEU_calls, "satEU", ref 0)]
2272 (function (opt
,x) ->
2273 (opt
,x,ref 0.0,ref 0,
2274 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2275 [List.hd
all;all_but_path]
2276 (*(all@baseline@conjneg@path@required)*)
2280 let rec iter fn = function
2282 | n
-> let _ = fn() in
2283 (Hashtbl.clear
reachable_table;
2284 Hashtbl.clear
memo_label;
2288 let copy_to_stderr fl
=
2289 let i = open_in fl
in
2291 Printf.fprintf stderr
"%s\n" (input_line
i);
2293 try loop() with _ -> ();
2296 let bench_sat (_,_,states) fn =
2297 List.iter (function (opt
,_) -> opt
:= false) all_options;
2300 (function (name
,options,time
,trips,counter_info
) ->
2301 let iterct = !Flag_ctl.bench
in
2302 if !time
> float_of_int
timeout then time
:= -100.0;
2303 if not
(!time
= -100.0)
2306 Hashtbl.clear
reachable_table;
2307 Hashtbl.clear
memo_label;
2308 List.iter (function (opt
,_) -> opt
:= true) options;
2309 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2313 let bef = Sys.time
() in
2315 Common.timeout_function
timeout
2317 let bef = Sys.time
() in
2318 let res = iter fn iterct in
2319 let aft = Sys.time
() in
2320 time
:= !time
+. (aft -. bef);
2321 trips := !trips + !triples;
2323 (function (calls
,_,save_calls
) ->
2324 function (current_calls
,current_cfg
,current_max_cfg
) ->
2326 !current_calls
+ (!calls
- !save_calls
);
2327 if (!calls
- !save_calls
) > 0
2329 (let st = List.length
states in
2330 current_cfg
:= !current_cfg
+ st;
2331 if st > !current_max_cfg
2332 then current_max_cfg
:= st))
2333 counters counter_info
;
2338 let aft = Sys.time
() in
2340 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2344 List.iter (function (opt
,_) -> opt
:= false) options;
2349 Printf.fprintf stderr
"\n";
2353 (if not
(List.for_all
(function x -> x = res) rest
)
2355 (List.iter (print_state "a state") answers;
2356 Printf.printf
"something doesn't work\n");
2360 let iterct = !Flag_ctl.bench
in
2364 (function (name
,options,time
,trips,counter_info
) ->
2365 Printf.fprintf stderr
"%s Numbers: %f %d "
2366 name
(!time
/. (float_of_int
iterct)) !trips;
2368 (function (calls
,cfg
,max_cfg
) ->
2369 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2371 Printf.fprintf stderr
"\n")
2374 (* ---------------------------------------------------------------------- *)
2375 (* preprocessing: ignore irrelevant functions *)
2377 let preprocess (cfg
,_,_) label = function
2378 [] -> true (* no information, try everything *)
2380 let sz = G.size cfg
in
2381 let verbose_output pred = function
2383 Printf.printf
"did not find:\n";
2384 P.print_predicate
pred; Format.print_newline
()
2386 Printf.printf
"found:\n";
2387 P.print_predicate
pred; Format.print_newline
();
2388 Printf.printf
"but it was not enough\n" in
2389 let get_any verbose
x =
2391 try Hashtbl.find
memo_label x
2394 (let triples = label x in
2396 List.map (function (st,th
,_) -> (st,th
)) triples in
2397 Hashtbl.add memo_label x filtered;
2399 if verbose
then verbose_output x res;
2402 (* don't bother testing when there are more patterns than nodes *)
2403 if List.length l
> sz-2
2405 else List.for_all
(get_any false) l
in
2406 if List.exists
get_all l
2409 (if !Flag_ctl.verbose_match
2411 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2415 let filter_partial_matches trips =
2416 if !Flag_ctl.partial_match
2418 let anynegwit = (* if any is neg, then all are *)
2419 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2421 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2424 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2428 (* ---------------------------------------------------------------------- *)
2429 (* Main entry point for engine *)
2430 let sat m phi reqopt
=
2432 (match !Flag_ctl.steps
with
2433 None
-> step_count := 0
2434 | Some
x -> step_count := x);
2435 Hashtbl.clear
reachable_table;
2436 Hashtbl.clear
memo_label;
2437 let (x,label,states) = m
in
2438 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2440 ((* to drop when Yoann initialized this flag *)
2441 if List.exists
(G.extract_is_loop
x) states
2442 then Flag_ctl.loop_in_src_code
:= true;
2443 let m = (x,label,List.sort compare
states) in
2445 if(!Flag_ctl.verbose_ctl_engine
)
2447 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2448 if !Flag_ctl.bench
> 0
2452 let fn _ = satloop false [] None
m phi
[] in
2453 if !Flag_ctl.bench
> 0
2455 else Common.profile_code
"ctl" (fun _ -> fn()) in
2456 let res = filter_partial_matches res in
2458 Printf.printf "steps: start %d, stop %d\n"
2459 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2461 Printf.printf "triples: %d\n" !triples;
2462 print_state "final result" res;
2464 List.sort compare
res)
2466 (if !Flag_ctl.verbose_ctl_engine
2467 then Common.pr2
"missing something required";
2472 (* ********************************************************************** *)
2473 (* End of Module: CTL_ENGINE *)
2474 (* ********************************************************************** *)