2 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (*external c_counter : unit -> int = "c_counter"*)
25 (* Optimize triples_conj by first extracting the intersection of the two sets,
26 which can certainly be in the intersection *)
27 let pTRIPLES_CONJ_OPT = ref true
28 (* For complement, make NegState for the negation of a single state *)
29 let pTRIPLES_COMPLEMENT_OPT = ref true
30 (* For complement, do something special for the case where the environment
31 and witnesses are empty *)
32 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
33 (* "Double negate" the arguments of the path operators *)
34 let pDOUBLE_NEGATE_OPT = ref true
35 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
36 let pNEW_INFO_OPT = ref true
37 (* Filter the result of the label function to drop entries that aren't
38 compatible with any of the available environments *)
39 let pREQUIRED_ENV_OPT = ref true
40 (* Memoize the raw result of the label function *)
41 let pSATLABEL_MEMO_OPT = ref true
42 (* Filter results according to the required states *)
43 let pREQUIRED_STATES_OPT = ref true
44 (* Drop negative witnesses at Uncheck *)
45 let pUNCHECK_OPT = ref true
46 let pANY_NEG_OPT = ref true
47 let pLazyOpt = ref true
49 (* Nico: This stack is use for graphical traces *)
50 let graph_stack = ref ([] : string list
)
51 let graph_hash = (Hashtbl.create
101)
54 let pTRIPLES_CONJ_OPT = ref false
55 let pTRIPLES_COMPLEMENT_OPT = ref false
56 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
57 let pDOUBLE_NEGATE_OPT = ref false
58 let pNEW_INFO_OPT = ref false
59 let pREQUIRED_ENV_OPT = ref false
60 let pSATLABEL_MEMO_OPT = ref false
61 let pREQUIRED_STATES_OPT = ref false
62 let pUNCHECK_OPT = ref false
63 let pANY_NEG_OPT = ref false
64 let pLazyOpt = ref false
68 let step_count = ref 0
71 if not
(!step_count = 0)
74 step_count := !step_count - 1;
75 if !step_count = 0 then raise Steps
78 let inc cell
= cell
:= !cell
+ 1
80 let satEU_calls = ref 0
81 let satAW_calls = ref 0
82 let satAU_calls = ref 0
83 let satEF_calls = ref 0
84 let satAF_calls = ref 0
85 let satEG_calls = ref 0
86 let satAG_calls = ref 0
94 Printf.sprintf
"_fresh_r_%d" c
96 (* **********************************************************************
98 * Implementation of a Witness Tree model checking engine for CTL-FVex
101 * **********************************************************************)
103 (* ********************************************************************** *)
104 (* Module: SUBST (substitutions: meta. vars and values) *)
105 (* ********************************************************************** *)
111 val eq_mvar
: mvar
-> mvar
-> bool
112 val eq_val
: value -> value -> bool
113 val merge_val
: value -> value -> value
114 val print_mvar
: mvar
-> unit
115 val print_value
: value -> unit
119 (* ********************************************************************** *)
120 (* Module: GRAPH (control flow graphs / model) *)
121 (* ********************************************************************** *)
127 val predecessors
: cfg
-> node
-> node list
128 val successors
: cfg
-> node
-> node list
129 val extract_is_loop
: cfg
-> node
-> bool
130 val print_node
: node
-> unit
131 val size
: cfg
-> int
132 val print_graph
: cfg
-> string option ->
133 (node
* string) list
-> (node
* string) list
-> string -> unit
137 module OGRAPHEXT_GRAPH
=
140 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
141 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
142 let print_node i
= Format.print_string
(Common.i_to_s i
)
146 (* ********************************************************************** *)
147 (* Module: PREDICATE (predicates for CTL formulae) *)
148 (* ********************************************************************** *)
150 module type PREDICATE
=
153 val print_predicate
: t
-> unit
157 (* ********************************************************************** *)
159 (* ---------------------------------------------------------------------- *)
160 (* Misc. useful generic functions *)
161 (* ---------------------------------------------------------------------- *)
163 let get_graph_files () = !graph_stack
164 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
174 let foldl = List.fold_left
;;
176 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
178 type 'a esc
= ESC
of 'a
| CONT
of 'a
180 let foldr = List.fold_right
;;
182 let concat = List.concat;;
186 let filter = List.filter;;
188 let partition = List.partition;;
190 let concatmap f l
= List.concat (List.map f l
);;
198 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
200 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
202 let rec some_tolist opts
=
205 | (Some x
)::rest
-> x
::(some_tolist rest
)
206 | _
::rest
-> some_tolist rest
209 let rec groupBy eq l
=
213 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
214 (x
::xs1
)::(groupBy eq xs2
)
217 let group l
= groupBy (=) l
;;
219 let rec memBy eq x l
=
222 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
225 let rec nubBy eq ls
=
228 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
229 | (x
::xs
) -> x
::(nubBy eq xs
)
235 | (x
::xs
) when (List.mem x xs
) -> nub xs
236 | (x
::xs
) -> x
::(nub xs
)
239 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
241 let setifyBy eq xs
= nubBy eq xs
;;
243 let setify xs
= nub xs
;;
245 let inner_setify xs
= List.sort compare
(nub xs
);;
247 let unionBy compare eq xs
= function
250 let rec loop = function
252 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
253 List.sort compare
(loop xs
)
256 let union xs ys
= unionBy state_compare (=) xs ys
;;
258 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
260 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
262 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
263 let supseteq xs ys
= subseteq ys xs
265 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
267 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
269 (* Fix point calculation *)
271 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
274 (* Fix point calculation on set-valued functions *)
275 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
276 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
278 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
280 (* ********************************************************************** *)
281 (* Module: CTL_ENGINE *)
282 (* ********************************************************************** *)
285 functor (SUB
: SUBST
) ->
286 functor (G
: GRAPH
) ->
287 functor (P
: PREDICATE
) ->
292 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
294 type ('pred
,'anno
) witness
=
295 (G.node
, substitution
,
296 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
297 Ast_ctl.generic_witnesstree
299 type ('pred
,'anno
) triples =
300 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
302 (* ---------------------------------------------------------------------- *)
303 (* Pretty printing functions *)
304 (* ---------------------------------------------------------------------- *)
306 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
307 let print_generic_subst = function
309 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
310 | A.NegSubst
(mvar
, v
) ->
311 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
312 Format.print_string
"[";
313 Common.print_between
(fun () -> Format.print_string
";" )
314 print_generic_subst substxs
;
315 Format.print_string
"]"
317 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
319 | A.Wit
(state
, subst
, anno
, childrens
) ->
320 Format.print_string
"wit ";
322 print_generic_substitution subst
;
323 (match childrens
with
324 [] -> Format.print_string
"{}"
326 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
327 print_generic_witnesstree childrens
; Format.close_box
())
329 Format.print_string
"!";
330 print_generic_witness wit
332 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
335 Format.print_string
"{";
337 (fun () -> Format.print_string
";"; Format.force_newline
() )
338 print_generic_witness witnesstree
;
339 Format.print_string
"}";
342 and print_generic_triple
(node
,subst
,tree
) =
344 print_generic_substitution subst
;
345 print_generic_witnesstree tree
347 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
348 Format.print_string
"<";
350 (fun () -> Format.print_string
";"; Format.force_newline
())
351 print_generic_triple xs
;
352 Format.print_string
">"
355 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
356 Printf.printf
"%s\n" str
;
357 List.iter
(function x ->
358 print_generic_triple
x; Format.print_newline
(); flush stdout
)
359 (List.sort compare l
);
362 let print_required_states = function
363 None
-> Printf.printf
"no required states\n"
365 Printf.printf
"required states: ";
368 G.print_node x; Format.print_string
" "; Format.print_flush
())
372 let mkstates states
= function
374 | Some states
-> states
376 let print_graph grp required_states res str
= function
377 A.Exists
(keep
,v
,phi
) -> ()
379 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
382 | A.Exists
(keep
,v
,phi
) -> ()
385 Printf.sprintf
"%s%s"
387 (Common.format_to_string
389 Pretty_print_ctl.pp_ctl
390 (P.print_predicate
, SUB.print_mvar
)
393 let file = (match !Flag.currentfile
with
394 None
-> "graphical_trace"
397 (if not
(List.mem
file !graph_stack) then
398 graph_stack := file :: !graph_stack);
399 let filename = Filename.temp_file
(file^
":") ".dot" in
400 Hashtbl.add
graph_hash file filename;
402 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
403 (match required_states
with
405 | Some required_states
->
406 (List.map (function s
-> (s
,"blue")) required_states
))
407 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
409 let print_graph_c grp required_states res
ctr phi
=
410 let str = "iter: "^
(string_of_int
!ctr) in
411 print_graph grp required_states res
str phi
413 (* ---------------------------------------------------------------------- *)
415 (* ---------------------------------------------------------------------- *)
418 (* ************************* *)
420 (* ************************* *)
425 | A.NegSubst
(x,_
) -> x
431 | A.NegSubst
(_
,x) -> x
434 let eq_subBy eqx eqv sub sub'
=
435 match (sub
,sub'
) with
436 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
437 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
442 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
444 let eq_subst th th'
= setequalBy eq_sub th th'
;;
446 let merge_subBy eqx
(===) (>+<) sub sub'
=
447 (* variable part is guaranteed to be the same *)
448 match (sub
,sub'
) with
449 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
451 then Some
[A.Subst
(x, v
>+< v'
)]
453 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
455 then Some
[A.Subst
(x'
,v'
)]
457 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
459 then Some
[A.Subst
(x,v
)]
461 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
464 let merged = v
>+< v'
in
465 if merged = v
&& merged = v'
466 then Some
[A.NegSubst
(x,v
>+< v'
)]
468 (* positions are compatible, but not identical. keep apart. *)
469 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
470 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
474 let merge_sub sub sub'
=
475 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
477 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
479 (* NOTE: we sort by using the generic "compare" on (meta-)variable
480 * names; we could also require a definition of compare for meta-variables
481 * or substitutions but that seems like overkill for sorting
483 let clean_subst theta
=
487 let res = compare
(dom_sub s
) (dom_sub s'
) in
491 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
492 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
493 | _
-> compare
(ran_sub s
) (ran_sub s'
)
496 let rec loop = function
498 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
499 loop (A.Subst
(x,v
)::rest
)
500 | x::xs
-> x::(loop xs
) in
503 let top_subst = [];; (* Always TRUE subst. *)
505 (* Split a theta in two parts: one with (only) "x" and one without *)
507 let split_subst theta
x =
508 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
510 exception SUBST_MISMATCH
511 let conj_subst theta theta'
=
512 match (theta
,theta'
) with
513 | ([],_
) -> Some theta'
514 | (_
,[]) -> Some theta
516 let rec classify = function
518 | [x] -> [(dom_sub x,[x])]
520 (match classify xs
with
521 ((nm
,y
)::ys
) as res ->
524 else (dom_sub x,[x])::res
525 | _
-> failwith
"not possible") in
526 let merge_all theta theta'
=
533 match (merge_sub sub sub'
) with
534 Some subs
-> subs
@ rest
535 | _
-> raise SUBST_MISMATCH
)
538 let rec loop = function
540 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
542 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
543 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
544 (match compare
x y
with
545 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
546 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
547 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
548 | _
-> failwith
"not possible") in
549 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
550 with SUBST_MISMATCH
-> None
553 (* theta' must be a subset of theta *)
554 let conj_subst_none theta theta'
=
555 match (theta
,theta'
) with
556 | (_
,[]) -> Some theta
559 let rec classify = function
561 | [x] -> [(dom_sub x,[x])]
563 (match classify xs
with
564 ((nm
,y
)::ys
) as res ->
567 else (dom_sub x,[x])::res
568 | _
-> failwith
"not possible") in
569 let merge_all theta theta'
=
576 match (merge_sub sub sub'
) with
577 Some subs
-> subs
@ rest
578 | _
-> raise SUBST_MISMATCH
)
581 let rec loop = function
583 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
584 | ([],ctheta'
) -> raise SUBST_MISMATCH
585 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
586 (match compare
x y
with
587 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
588 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
589 | 1 -> raise SUBST_MISMATCH
590 | _
-> failwith
"not possible") in
591 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
592 with SUBST_MISMATCH
-> None
597 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
598 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
601 (* Turn a (big) theta into a list of (small) thetas *)
602 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
605 (* ************************* *)
607 (* ************************* *)
609 (* Always TRUE witness *)
610 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
612 let eq_wit wit wit'
= wit
= wit'
;;
614 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
615 let res = unionBy compare
(=) wit wit'
in
616 let anynegwit = (* if any is neg, then all are *)
617 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
619 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
622 let negate_wit wit
= A.NegWit wit
(*
624 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
625 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
628 let negate_wits wits
=
629 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
632 let anynegwit = (* if any is neg, then all are *)
633 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
637 function (s
,th
,wit
) ->
638 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
641 (* ************************* *)
643 (* ************************* *)
645 (* Triples are equal when the constituents are equal *)
646 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
647 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
649 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
651 let normalize trips
=
653 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
657 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
658 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
659 let triples_conj trips trips'
=
660 let (trips
,shared
,trips'
) =
661 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
664 List.partition (function t
-> List.mem t trips'
) trips
in
666 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
667 (trips,shared
,trips'
)
668 else (trips,[],trips'
) in
669 foldl (* returns a set - setify inlined *)
671 function (s1
,th1
,wit1
) ->
674 function (s2
,th2
,wit2
) ->
676 (match (conj_subst th1 th2
) with
678 let t = (s1
,th
,union_wit wit1 wit2
) in
679 if List.mem
t rest
then rest
else t::rest
686 (* ignore the state in the right argument. always pretend it is the same as
688 (* env on right has to be a subset of env on left *)
689 let triples_conj_none trips trips'
=
690 let (trips,shared
,trips'
) =
691 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
694 List.partition (function t -> List.mem
t trips'
) trips in
696 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
697 (trips,shared
,trips'
)
698 else (trips,[],trips'
) in
699 foldl (* returns a set - setify inlined *)
701 function (s1
,th1
,wit1
) ->
704 function (s2
,th2
,wit2
) ->
705 match (conj_subst_none th1 th2
) with
707 let t = (s1
,th
,union_wit wit1 wit2
) in
708 if List.mem
t rest
then rest
else t::rest
716 let triples_conj_AW trips trips'
=
717 let (trips,shared
,trips'
) =
718 if false && !pTRIPLES_CONJ_OPT
721 List.partition (function t -> List.mem
t trips'
) trips in
723 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
724 (trips,shared
,trips'
)
725 else (trips,[],trips'
) in
726 foldl (* returns a set - setify inlined *)
728 function (s1
,th1
,wit1
) ->
731 function (s2
,th2
,wit2
) ->
733 (match (conj_subst th1 th2
) with
735 let t = (s1
,th
,union_wit wit1 wit2
) in
736 if List.mem
t rest
then rest
else t::rest
743 (* *************************** *)
744 (* NEGATION (NegState style) *)
745 (* *************************** *)
747 (* Constructive negation at the state level *)
750 | NegState
of 'a list
753 let compatible_states = function
754 (PosState s1
, PosState s2
) ->
755 if s1
= s2
then Some
(PosState s1
) else None
756 | (PosState s1
, NegState s2
) ->
757 if List.mem s1 s2
then None
else Some
(PosState s1
)
758 | (NegState s1
, PosState s2
) ->
759 if List.mem s2 s1
then None
else Some
(PosState s2
)
760 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
763 (* Conjunction on triples with "special states" *)
764 let triples_state_conj trips trips'
=
765 let (trips,shared
,trips'
) =
766 if !pTRIPLES_CONJ_OPT
769 List.partition (function t -> List.mem
t trips'
) trips in
771 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
772 (trips,shared
,trips'
)
773 else (trips,[],trips'
) in
776 function (s1
,th1
,wit1
) ->
779 function (s2
,th2
,wit2
) ->
780 match compatible_states(s1
,s2
) with
782 (match (conj_subst th1 th2
) with
784 let t = (s
,th
,union_wit wit1 wit2
) in
785 if List.mem
t rest
then rest
else t::rest
792 let triple_negate (s
,th
,wits
) =
793 let negstates = (NegState
[s
],top_subst,top_wit) in
794 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
795 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
796 negstates :: (negths @ negwits) (* all different *)
798 (* FIX ME: it is not necessary to do full conjunction *)
799 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
800 if !pTRIPLES_COMPLEMENT_OPT
802 (let cleanup (s
,th
,wit
) =
804 PosState s'
-> [(s'
,th
,wit
)]
806 assert (th
=top_subst);
807 assert (wit
=top_wit);
808 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
809 let (simple
,complex
) =
810 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
812 let (simple
,complex
) =
813 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
815 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
816 top_subst,top_wit)] in
818 else ([(NegState
[],top_subst,top_wit)],trips) in
819 let rec compl trips =
822 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
823 let compld = (compl complex
) in
824 let compld = concatmap cleanup compld in
827 let negstates (st
,th
,wits
) =
828 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
829 let negths (st
,th
,wits
) =
830 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
831 let negwits (st
,th
,wits
) =
832 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
834 [] -> map (function st
-> (st
,top_subst,top_wit)) states
840 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
841 (negstates x @ negths x @ negwits x) xs
)
844 let triple_negate (s
,th
,wits
) =
845 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
846 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
847 ([s
], negths @ negwits) (* all different *)
849 let print_compl_state str (n
,p
) =
850 Printf.printf
"%s neg: " str;
852 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
857 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
859 then map (function st
-> (st
,top_subst,top_wit)) states
861 let cleanup (neg
,pos
) =
863 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
864 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
866 let trips = List.sort
state_compare trips in
867 let all_negated = List.map triple_negate trips in
868 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
869 let (pos1conj
,pos1keep
) =
870 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
871 let (pos2conj
,pos2keep
) =
872 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
873 (Common.union_set neg1 neg2
,
874 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
875 let rec inner_loop = function
876 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
878 let rec outer_loop = function
880 | l
-> outer_loop (inner_loop l
) in
881 cleanup (outer_loop all_negated)
883 (* ********************************** *)
884 (* END OF NEGATION (NegState style) *)
885 (* ********************************** *)
887 (* now this is always true, so we could get rid of it *)
888 let something_dropped = ref true
890 let triples_union trips trips'
=
891 (*unionBy compare eq_trip trips trips';;*)
892 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
894 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
895 Then, the following says that since the first is a more restrictive
896 environment and has fewer witnesses, then it should be dropped. But having
897 fewer witnesses is not necessarily less informative than having more,
898 because fewer witnesses can mean the absence of the witness-causing thing.
899 So the fewer witnesses have to be kept around.
900 subseteq changed to = to make it hopefully work
905 something_dropped := false;
907 then (something_dropped := true; trips)
909 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
912 (match conj_subst th1 th2
with
915 then if (*subseteq*) wit1
= wit2
then 1 else 0
918 then if (*subseteq*) wit2
= wit1
then (-1) else 0
922 let rec first_loop second
= function
924 | x::xs
-> first_loop (second_loop
x second
) xs
925 and second_loop
x = function
928 match subsumes x y
with
929 1 -> something_dropped := true; all
930 | (-1) -> second_loop
x ys
931 | _
-> y
::(second_loop
x ys
) in
932 first_loop trips trips'
934 else unionBy compare
eq_trip trips trips'
937 let triples_witness x unchecked not_keep
trips =
938 let anyneg = (* if any is neg, then all are *)
939 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
940 let anynegwit = (* if any is neg, then all are *)
941 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
942 let allnegwit = (* if any is neg, then all are *)
943 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
945 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
949 function (s
,th
,wit
) as t ->
950 let (th_x
,newth
) = split_subst th
x in
953 (* one consider whether if not not_keep is true, then we should
954 fail. but it could be that the variable is a used_after and
955 then it is the later rule that should fail and not this one *)
956 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
958 (SUB.print_mvar
x; Format.print_flush
();
959 print_state ": empty witness from" [t]);
961 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
962 (* see tests/nestseq for how neg bindings can come up even
963 without eg partial matches
964 (* negated substitution only allowed with negwits.
966 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
969 (print_generic_substitution l
; Format.print_newline
();
970 failwith
"unexpected negative binding with positive witnesses")*)
973 if unchecked
or not_keep
976 if anynegwit wit
&& allnegwit wit
977 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
978 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
981 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
987 (* ---------------------------------------------------------------------- *)
988 (* SAT - Model Checking Algorithm for CTL-FVex *)
990 (* TODO: Implement _all_ operators (directly) *)
991 (* ---------------------------------------------------------------------- *)
994 (* ************************************* *)
995 (* The SAT algorithm and special helpers *)
996 (* ************************************* *)
998 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1000 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1001 let exp (s
,th
,wit
) =
1003 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1005 A.FORWARD
-> G.predecessors grp s
1006 | A.BACKWARD
-> G.successors grp s
) in
1007 setify (concatmap exp y
)
1012 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1015 None
-> true | Some reqst
-> List.mem s reqst
in
1018 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1021 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1024 (function p
-> (p
,succ grp p
))
1027 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1028 (* would a hash table be more efficient? *)
1029 let all = List.sort
state_compare all in
1030 let rec up_nodes child s
= function
1032 | (s1
,th
,wit
)::xs
->
1033 (match compare s1 child
with
1034 -1 -> up_nodes child s xs
1035 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1037 let neighbor_triples =
1040 function (s
,children
) ->
1044 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1048 match neighbor_triples with
1052 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1054 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1057 None
-> true | Some reqst
-> List.mem s reqst
in
1060 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1063 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1066 (function p
-> (p
,succ grp p
))
1069 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1070 (* would a hash table be more efficient? *)
1071 let all = List.sort
state_compare all in
1072 let rec up_nodes child s
= function
1074 | (s1
,th
,wit
)::xs
->
1075 (match compare s1 child
with
1076 -1 -> up_nodes child s xs
1077 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1079 let neighbor_triples =
1082 function (s
,children
) ->
1085 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1088 match neighbor_triples with
1090 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1092 (* drop_negwits will call setify *)
1093 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1095 let satAX dir m s reqst
= pre_forall dir m s s reqst
1098 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1099 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1105 (*let ctr = ref 0 in*)
1108 let rec f y new_info
=
1115 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1116 let res = triples_union first y
in
1117 let new_info = setdiff res y
in
1118 (*Printf.printf "iter %d res %d new_info %d\n"
1119 !ctr (List.length res) (List.length new_info);
1128 let pre = pre_exist dir m y reqst
in
1129 triples_union s2
(triples_conj s1
pre) in
1133 (* EF phi == E[true U phi] *)
1134 let satEF dir m s2 reqst
=
1136 (*let ctr = ref 0 in*)
1139 let rec f y
new_info =
1145 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1146 let first = pre_exist dir m
new_info reqst
in
1147 let res = triples_union first y
in
1148 let new_info = setdiff res y
in
1149 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1150 (if dir = A.BACKWARD then "reachable" else "real ef")
1151 !ctr (List.length res) (List.length new_info);
1152 print_state "new info" new_info;
1159 let pre = pre_exist dir m y reqst
in
1160 triples_union s2
pre in
1164 type ('
pred,'anno
) auok
=
1165 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1167 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1168 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1174 (*let ctr = ref 0 in*)
1176 if !Flag_ctl.loop_in_src_code
1181 let rec f y newinfo
=
1187 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1191 try Some
(pre_forall dir m
new_info y reqst
)
1196 match triples_conj s1
pre with
1199 (*print_state "s1" s1;
1200 print_state "pre" pre;
1201 print_state "first" first;*)
1202 let res = triples_union first y
in
1204 if not
!something_dropped
1206 else setdiff res y
in
1208 "iter %d res %d new_info %d\n"
1209 !ctr (List.length res) (List.length new_info);
1214 if !Flag_ctl.loop_in_src_code
1218 fix (function s1 -> function s2 ->
1219 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1220 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1221 subseteq s1 s2) in for popl *)
1226 let pre = pre_forall dir m y y reqst
in
1227 triples_union s2 (triples_conj s1 pre) in
1232 (* reqst could be the states of s1 *)
1234 let lstates = mkstates states reqst in
1235 let initial_removed =
1236 triples_complement lstates (triples_union s1 s2) in
1237 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1238 let rec loop base removed =
1240 triples_conj base (pre_exist dir m removed reqst) in
1242 triples_conj base (triples_complement lstates new_removed) in
1243 if supseteq new_base base
1244 then triples_union base s2
1245 else loop new_base new_removed in
1246 loop initial_base initial_removed *)
1248 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1254 This works extremely badly when the region is small and the end of the
1255 region is very ambiguous, eg free(x) ... x
1259 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1260 let ostates = Common.union_set (get_states s1) (get_states s2) in
1263 A.FORWARD -> G.successors grp
1264 | A.BACKWARD -> G.predecessors grp) in
1266 List.fold_left Common.union_set ostates (List.map succ ostates) in
1267 let negphi = triples_complement states s1 in
1268 let negpsi = triples_complement states s2 in
1269 triples_complement ostates
1270 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1273 (*let ctr = ref 0 in*)
1277 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1280 let pre = pre_forall dir m y y reqst
in
1281 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1282 triples_union s2 conj in
1283 setgfix f (triples_union s1 s2)
1286 let satAF dir m s reqst
=
1290 let rec f y newinfo
=
1295 let first = pre_forall dir m
new_info y reqst
in
1296 let res = triples_union first y
in
1297 let new_info = setdiff res y
in
1303 let pre = pre_forall dir m y y reqst
in
1304 triples_union s
pre in
1307 let satAG dir
((_
,_
,states) as m
) s reqst
=
1311 let pre = pre_forall dir m y y reqst
in
1312 triples_conj y
pre in
1315 let satEG dir
((_
,_
,states) as m
) s reqst
=
1319 let pre = pre_exist dir m y reqst
in
1320 triples_conj y
pre in
1323 (* **************************************************************** *)
1324 (* Inner And - a way of dealing with multiple matches within a node *)
1325 (* **************************************************************** *)
1326 (* applied to the result of matching a node. collect witnesses when the
1327 states and environments are the same *)
1329 let inner_and trips =
1330 let rec loop = function
1332 | (s
,th
,w
)::trips ->
1333 let (cur
,acc
) = loop trips in
1335 (s'
,_
,_
)::_
when s
= s'
->
1336 let rec loop'
= function
1338 | ((_
,th'
,w'
) as t'
)::ts'
->
1339 (match conj_subst th th'
with
1340 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1341 | None
-> t'
::(loop' ts'
)) in
1343 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1345 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1348 (* *************** *)
1349 (* Partial matches *)
1350 (* *************** *)
1352 let filter_conj states unwanted partial_matches
=
1354 triples_conj (triples_complement states (unwitify unwanted
))
1356 triples_conj (unwitify x) (triples_complement states x)
1358 let strict_triples_conj strict
states trips trips'
=
1359 let res = triples_conj trips trips'
in
1360 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1362 let fail_left = filter_conj states trips trips'
in
1363 let fail_right = filter_conj states trips'
trips in
1364 let ors = triples_union fail_left fail_right in
1365 triples_union res ors
1368 let strict_triples_conj_none strict
states trips trips'
=
1369 let res = triples_conj_none trips trips'
in
1370 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1372 let fail_left = filter_conj states trips trips'
in
1373 let fail_right = filter_conj states trips'
trips in
1374 let ors = triples_union fail_left fail_right in
1375 triples_union res ors
1378 let left_strict_triples_conj strict
states trips trips'
=
1379 let res = triples_conj trips trips'
in
1380 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1382 let fail_left = filter_conj states trips trips'
in
1383 triples_union res fail_left
1386 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1387 let res = op dir m
trips required_states
in
1388 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1390 let states = mkstates states required_states
in
1391 let fail = filter_conj states res (failop dir m
trips required_states
) in
1392 triples_union res fail
1395 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1397 let res = op dir m
trips trips' required_states
in
1398 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1400 let states = mkstates states required_states
in
1401 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1402 triples_union res fail
1405 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1406 required_states
print_graph =
1407 match op dir m
trips trips' required_states
print_graph with
1409 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1411 let states = mkstates states required_states
in
1413 filter_conj states res (failop dir m
trips' required_states
) in
1414 AUok
(triples_union res fail)
1416 | AUfailed
res -> AUfailed
res
1418 (* ********************* *)
1419 (* Environment functions *)
1420 (* ********************* *)
1422 let drop_wits required_states s phi
=
1423 match required_states
with
1425 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1428 let print_required required
=
1431 Format.print_string
"{";
1434 print_generic_substitution reqd
; Format.print_newline
())
1436 Format.print_string
"}";
1437 Format.print_newline
())
1442 let extend_required trips required
=
1443 if !Flag_ctl.partial_match
1446 if !pREQUIRED_ENV_OPT
1452 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1454 let envs = if List.mem
[] envs then [] else envs in
1455 match (envs,required
) with
1459 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1464 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1471 match conj_subst t r
with
1472 None
-> rest
| Some th
-> add th rest
)
1476 with Too_long
-> envs :: required
)
1477 | (envs,_
) -> envs :: required
1480 let drop_required v required
=
1481 if !pREQUIRED_ENV_OPT
1488 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1490 (* check whether an entry has become useless *)
1491 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1494 (* no idea how to write this function ... *)
1496 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1498 let satLabel label required p
=
1500 if !pSATLABEL_MEMO_OPT
1503 let states_subs = Hashtbl.find
memo_label p
in
1504 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1507 let triples = setify(label p
) in
1508 Hashtbl.add memo_label p
1509 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1511 else setify(label p
) in
1513 (if !pREQUIRED_ENV_OPT
1517 function ((s
,th
,_
) as t) ->
1519 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1526 let get_required_states l
=
1527 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1529 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1532 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1533 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1535 match required_states
with
1540 A.FORWARD
-> G.successors
1541 | A.BACKWARD
-> G.predecessors in
1542 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1545 let reachable_table =
1546 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1548 (* like satEF, but specialized for get_reachable *)
1549 let reachsatEF dir
(grp
,_
,_
) s2 =
1551 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1552 let union = unionBy compare
(=) in
1553 let rec f y
= function
1556 let (pre_collected
,new_info) =
1557 List.partition (function Common.Left
x -> true | _
-> false)
1560 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1561 with Not_found
-> Common.Right
x)
1566 function Common.Left
x -> union x rest
1567 | _
-> failwith
"not possible")
1571 (function Common.Right
x -> x | _
-> failwith
"not possible")
1573 let first = inner_setify (concatmap (dirop grp
) new_info) in
1574 let new_info = setdiff first y in
1575 let res = new_info @ y in
1577 List.rev
(f s2 s2) (* put root first *)
1579 let get_reachable dir m required_states
=
1580 match required_states
with
1587 if List.mem cur rest
1591 (try Hashtbl.find
reachable_table (cur
,dir
)
1594 let states = reachsatEF dir m
[cur
] in
1595 Hashtbl.add reachable_table (cur
,dir
) states;
1604 Printf.sprintf
"_c%d" c
1606 (* **************************** *)
1607 (* End of environment functions *)
1608 (* **************************** *)
1610 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1612 let rec satloop unchecked required required_states
1613 ((grp
,label,states) as m
) phi env
=
1614 let rec loop unchecked required required_states phi
=
1615 (*Common.profile_code "satloop" (fun _ -> *)
1619 | A.True
-> triples_top states
1620 | A.Pred
(p
) -> satLabel label required p
1621 | A.Uncheck
(phi1
) ->
1622 let unchecked = if !pUNCHECK_OPT then true else false in
1623 loop unchecked required required_states phi1
1625 let phires = loop unchecked required required_states phi
in
1627 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1628 triples_complement (mkstates states required_states
)
1630 | A.Or
(phi1
,phi2
) ->
1632 (loop unchecked required required_states phi1
)
1633 (loop unchecked required required_states phi2
)
1634 | A.SeqOr
(phi1
,phi2
) ->
1635 let res1 = loop unchecked required required_states phi1
in
1636 let res2 = loop unchecked required required_states phi2
in
1637 let res1neg = unwitify res1 in
1640 (triples_complement (mkstates states required_states
) res1neg)
1642 | A.And
(strict
,phi1
,phi2
) ->
1643 (* phi1 is considered to be more likely to be [], because of the
1644 definition of asttoctl. Could use heuristics such as the size of
1646 let pm = !Flag_ctl.partial_match
in
1647 (match (pm,loop unchecked required required_states phi1
) with
1648 (false,[]) when !pLazyOpt -> []
1650 let new_required = extend_required phi1res required
in
1651 let new_required_states = get_required_states phi1res
in
1652 (match (pm,loop unchecked new_required new_required_states phi2
)
1654 (false,[]) when !pLazyOpt -> []
1656 strict_triples_conj strict
1657 (mkstates states required_states
)
1659 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1660 (* phi2 can appear anywhere that is reachable *)
1661 let pm = !Flag_ctl.partial_match
in
1662 (match (pm,loop unchecked required required_states phi1
) with
1665 let new_required = extend_required phi1res required
in
1666 let new_required_states = get_required_states phi1res
in
1667 let new_required_states =
1668 get_reachable dir m
new_required_states in
1669 (match (pm,loop unchecked new_required new_required_states phi2
)
1671 (false,[]) -> phi1res
1674 [] -> (* !Flag_ctl.partial_match must be true *)
1678 let s = mkstates states required_states
in
1680 (function a
-> function b
->
1681 strict_triples_conj strict
s a
[b
])
1682 [List.hd phi2res
] (List.tl phi2res
)
1685 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1686 let s = mkstates states required_states
in
1688 (function a
-> function b
->
1689 strict_triples_conj strict
s a b
)
1693 "only one result allowed for the left arg of AndAny")))
1694 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1695 (* phi2 can appear anywhere that is reachable *)
1696 let pm = !Flag_ctl.partial_match
in
1697 (match (pm,loop unchecked required required_states phi1
) with
1700 let new_required = extend_required phi1res required
in
1701 let new_required_states = get_required_states phi1res
in
1702 let new_required_states =
1703 get_reachable dir m
new_required_states in
1704 (match (pm,loop unchecked new_required new_required_states phi2
)
1706 (false,[]) -> phi1res
1708 (* if there is more than one state, something about the
1709 environment has to ensure that the right triples of
1710 phi2 get associated with the triples of phi1.
1711 the asttoctl2 has to ensure that that is the case.
1712 these should thus be structural properties.
1713 env of phi2 has to be a proper subset of env of phi1
1714 to ensure all end up being consistent. no new triples
1715 should be generated. strict_triples_conj_none takes
1718 let s = mkstates states required_states
in
1721 function (st
,th
,_
) as phi2_elem
->
1723 triples_complement [st
] [(st
,th
,[])] in
1724 strict_triples_conj_none strict
s acc
1725 (phi2_elem
::inverse))
1727 | A.InnerAnd
(phi
) ->
1728 inner_and(loop unchecked required required_states phi
)
1730 let new_required_states =
1731 get_children_required_states dir m required_states
in
1732 satEX dir m
(loop unchecked required
new_required_states phi
)
1734 | A.AX
(dir
,strict
,phi
) ->
1735 let new_required_states =
1736 get_children_required_states dir m required_states
in
1737 let res = loop unchecked required
new_required_states phi
in
1738 strict_A1 strict
satAX satEX dir m
res required_states
1740 let new_required_states = get_reachable dir m required_states
in
1741 satEF dir m
(loop unchecked required
new_required_states phi
)
1743 | A.AF
(dir
,strict
,phi
) ->
1744 if !Flag_ctl.loop_in_src_code
1746 loop unchecked required required_states
1747 (A.AU
(dir
,strict
,A.True
,phi
))
1749 let new_required_states = get_reachable dir m required_states
in
1750 let res = loop unchecked required
new_required_states phi
in
1751 strict_A1 strict
satAF satEF dir m
res new_required_states
1753 let new_required_states = get_reachable dir m required_states
in
1754 satEG dir m
(loop unchecked required
new_required_states phi
)
1756 | A.AG
(dir
,strict
,phi
) ->
1757 let new_required_states = get_reachable dir m required_states
in
1758 let res = loop unchecked required
new_required_states phi
in
1759 strict_A1 strict
satAG satEF dir m
res new_required_states
1760 | A.EU
(dir
,phi1
,phi2
) ->
1761 let new_required_states = get_reachable dir m required_states
in
1762 (match loop unchecked required
new_required_states phi2
with
1763 [] when !pLazyOpt -> []
1765 let new_required = extend_required s2 required
in
1766 let s1 = loop unchecked new_required new_required_states phi1
in
1767 satEU dir m
s1 s2 new_required_states
1768 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1769 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1770 let new_required_states = get_reachable dir m required_states
in
1771 (match loop unchecked required
new_required_states phi2
with
1772 [] when !pLazyOpt -> []
1774 let new_required = extend_required s2 required
in
1775 let s1 = loop unchecked new_required new_required_states phi1
in
1776 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1777 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1778 (*Printf.printf "using AU\n"; flush stdout;*)
1779 let new_required_states = get_reachable dir m required_states
in
1780 (match loop unchecked required
new_required_states phi2
with
1781 [] when !pLazyOpt -> []
1783 let new_required = extend_required s2 required
in
1784 let s1 = loop unchecked new_required new_required_states phi1
in
1786 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1788 print_graph_c grp
new_required_states y ctr phi
) in
1791 | AUfailed tmp_res
->
1792 (* found a loop, have to try AW *)
1794 A[E[phi1 U phi2] & phi1 W phi2]
1795 the and is nonstrict *)
1796 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1797 (*Printf.printf "using AW\n"; flush stdout;*)
1800 (satEU dir m
s1 tmp_res
new_required_states
1801 (* no graph, for the moment *)
1804 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1805 | A.Implies
(phi1
,phi2
) ->
1806 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1807 | A.Exists
(keep
,v
,phi
) ->
1808 let new_required = drop_required v required
in
1809 triples_witness v
unchecked (not keep
)
1810 (loop unchecked new_required required_states phi
)
1811 | A.Let
(v
,phi1
,phi2
) ->
1812 (* should only be used when the properties unchecked, required,
1813 and required_states are known to be the same or at least
1814 compatible between all the uses. this is not checked. *)
1815 let res = loop unchecked required required_states phi1
in
1816 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1817 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1818 (* should only be used when the properties unchecked, required,
1819 and required_states are known to be the same or at least
1820 compatible between all the uses. this is not checked. *)
1821 (* doesn't seem to be used any more *)
1822 let new_required_states = get_reachable dir m required_states
in
1823 let res = loop unchecked required
new_required_states phi1
in
1824 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1826 let res = List.assoc v env
in
1828 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1830 | A.XX
(phi
) -> failwith
"should have been removed" in
1831 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1832 let res = drop_wits required_states
res phi
(* ) *) in
1833 print_graph grp required_states
res "" phi
;
1836 loop unchecked required required_states phi
1840 (* SAT with tracking *)
1841 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1842 ((_
,label,states) as m
) phi env
=
1843 let anno res children
= (annot lvl phi
res children
,res) in
1844 let satv unchecked required required_states phi0 env
=
1845 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1847 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1848 anno (satloop unchecked required required_states m phi env
) []
1852 A.False
-> anno [] []
1853 | A.True
-> anno (triples_top states) []
1855 Printf.printf
"label\n"; flush stdout
;
1856 anno (satLabel label required p
) []
1857 | A.Uncheck
(phi1
) ->
1858 let unchecked = if !pUNCHECK_OPT then true else false in
1859 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1860 Printf.printf
"uncheck\n"; flush stdout
;
1864 satv unchecked required required_states phi1 env
in
1865 Printf.printf
"not\n"; flush stdout
;
1866 anno (triples_complement (mkstates states required_states
) res) [child
]
1867 | A.Or
(phi1
,phi2
) ->
1869 satv unchecked required required_states phi1 env
in
1871 satv unchecked required required_states phi2 env
in
1872 Printf.printf
"or\n"; flush stdout
;
1873 anno (triples_union res1 res2) [child1
; child2
]
1874 | A.SeqOr
(phi1
,phi2
) ->
1876 satv unchecked required required_states phi1 env
in
1878 satv unchecked required required_states phi2 env
in
1880 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1881 Printf.printf
"seqor\n"; flush stdout
;
1882 anno (triples_union res1
1884 (triples_complement (mkstates states required_states
)
1888 | A.And
(strict
,phi1
,phi2
) ->
1889 let pm = !Flag_ctl.partial_match
in
1890 (match (pm,satv unchecked required required_states phi1 env
) with
1891 (false,(child1
,[])) ->
1892 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1893 | (_
,(child1
,res1)) ->
1894 let new_required = extend_required res1 required
in
1895 let new_required_states = get_required_states res1 in
1896 (match (pm,satv unchecked new_required new_required_states phi2
1898 (false,(child2
,[])) ->
1899 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1900 | (_
,(child2
,res2)) ->
1901 Printf.printf
"and\n"; flush stdout
;
1903 strict_triples_conj strict
1904 (mkstates states required_states
)
1906 anno res [child1
; child2
]))
1907 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1908 let pm = !Flag_ctl.partial_match
in
1909 (match (pm,satv unchecked required required_states phi1 env
) with
1910 (false,(child1
,[])) ->
1911 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1912 | (_
,(child1
,res1)) ->
1913 let new_required = extend_required res1 required
in
1914 let new_required_states = get_required_states res1 in
1915 let new_required_states =
1916 get_reachable dir m
new_required_states in
1917 (match (pm,satv unchecked new_required new_required_states phi2
1919 (false,(child2
,[])) ->
1920 Printf.printf
"andany\n"; flush stdout
;
1921 anno res1 [child1
;child2
]
1922 | (_
,(child2
,res2)) ->
1924 [] -> (* !Flag_ctl.partial_match must be true *)
1926 then anno [] [child1
; child2
]
1929 let s = mkstates states required_states
in
1931 (function a
-> function b
->
1932 strict_triples_conj strict
s a
[b
])
1933 [List.hd
res2] (List.tl
res2) in
1934 anno res [child1
; child2
]
1937 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1938 Printf.printf
"andany\n"; flush stdout
;
1940 let s = mkstates states required_states
in
1942 (function a
-> function b
->
1943 strict_triples_conj strict
s a b
)
1945 anno res [child1
; child2
]
1948 "only one result allowed for the left arg of AndAny")))
1949 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1950 let pm = !Flag_ctl.partial_match
in
1951 (match (pm,satv unchecked required required_states phi1 env
) with
1952 (false,(child1
,[])) ->
1953 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1954 | (_
,(child1
,res1)) ->
1955 let new_required = extend_required res1 required
in
1956 let new_required_states = get_required_states res1 in
1957 let new_required_states =
1958 get_reachable dir m
new_required_states in
1959 (match (pm,satv unchecked new_required new_required_states phi2
1961 (false,(child2
,[])) ->
1962 Printf.printf
"andany\n"; flush stdout
;
1963 anno res1 [child1
;child2
]
1964 | (_
,(child2
,res2)) ->
1966 let s = mkstates states required_states
in
1969 function (st
,th
,_
) as phi2_elem
->
1971 triples_complement [st
] [(st
,th
,[])] in
1972 strict_triples_conj_none strict
s acc
1973 (phi2_elem
::inverse))
1975 anno res [child1
; child2
]))
1976 | A.InnerAnd
(phi1
) ->
1977 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1978 Printf.printf
"uncheck\n"; flush stdout
;
1979 anno (inner_and res1) [child1
]
1981 let new_required_states =
1982 get_children_required_states dir m required_states
in
1984 satv unchecked required
new_required_states phi1 env
in
1985 Printf.printf
"EX\n"; flush stdout
;
1986 anno (satEX dir m
res required_states
) [child
]
1987 | A.AX
(dir
,strict
,phi1
) ->
1988 let new_required_states =
1989 get_children_required_states dir m required_states
in
1991 satv unchecked required
new_required_states phi1 env
in
1992 Printf.printf
"AX\n"; flush stdout
;
1993 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
1996 let new_required_states = get_reachable dir m required_states
in
1998 satv unchecked required
new_required_states phi1 env
in
1999 Printf.printf
"EF\n"; flush stdout
;
2000 anno (satEF dir m
res new_required_states) [child
]
2001 | A.AF
(dir
,strict
,phi1
) ->
2002 if !Flag_ctl.loop_in_src_code
2004 satv unchecked required required_states
2005 (A.AU
(dir
,strict
,A.True
,phi1
))
2008 (let new_required_states = get_reachable dir m required_states
in
2010 satv unchecked required
new_required_states phi1 env
in
2011 Printf.printf
"AF\n"; flush stdout
;
2013 strict_A1 strict
satAF satEF dir m
res new_required_states in
2016 let new_required_states = get_reachable dir m required_states
in
2018 satv unchecked required
new_required_states phi1 env
in
2019 Printf.printf
"EG\n"; flush stdout
;
2020 anno (satEG dir m
res new_required_states) [child
]
2021 | A.AG
(dir
,strict
,phi1
) ->
2022 let new_required_states = get_reachable dir m required_states
in
2024 satv unchecked required
new_required_states phi1 env
in
2025 Printf.printf
"AG\n"; flush stdout
;
2026 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2029 | A.EU
(dir
,phi1
,phi2
) ->
2030 let new_required_states = get_reachable dir m required_states
in
2031 (match satv unchecked required
new_required_states phi2 env
with
2033 Printf.printf
"EU\n"; flush stdout
;
2036 let new_required = extend_required res2 required
in
2038 satv unchecked new_required new_required_states phi1 env
in
2039 Printf.printf
"EU\n"; flush stdout
;
2040 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2042 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2043 failwith
"should not be used" (*
2044 let new_required_states = get_reachable dir m required_states in
2045 (match satv unchecked required new_required_states phi2 env with
2047 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2049 let new_required = extend_required res2 required in
2051 satv unchecked new_required new_required_states phi1 env in
2052 Printf.printf "AW %b\n" unchecked; flush stdout;
2054 strict_A2 strict satAW satEF dir m res1 res2
2055 new_required_states in
2056 anno res [child1; child2]) *)
2057 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2058 let new_required_states = get_reachable dir m required_states
in
2059 (match satv unchecked required
new_required_states phi2 env
with
2061 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2063 let new_required = extend_required s2 required
in
2065 satv unchecked new_required new_required_states phi1 env
in
2066 Printf.printf
"AU\n"; flush stdout
;
2068 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2069 (fun y str -> ()) in
2072 anno res [child1
; child2
]
2073 | AUfailed tmp_res
->
2074 (* found a loop, have to try AW *)
2076 A[E[phi1 U phi2] & phi1 W phi2]
2077 the and is nonstrict *)
2078 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2079 Printf.printf
"AW\n"; flush stdout
;
2082 (satEU dir m
s1 tmp_res
new_required_states
2083 (* no graph, for the moment *)
2087 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2088 anno res [child1
; child2
]))
2089 | A.Implies
(phi1
,phi2
) ->
2090 satv unchecked required required_states
2091 (A.Or
(A.Not phi1
,phi2
))
2093 | A.Exists
(keep
,v
,phi1
) ->
2094 let new_required = drop_required v required
in
2096 satv unchecked new_required required_states phi1 env
in
2097 Printf.printf
"exists\n"; flush stdout
;
2098 anno (triples_witness v
unchecked (not keep
) res) [child
]
2099 | A.Let
(v
,phi1
,phi2
) ->
2101 satv unchecked required required_states phi1 env
in
2103 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2104 anno res2 [child1
;child2
]
2105 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2106 let new_required_states = get_reachable dir m required_states
in
2108 satv unchecked required
new_required_states phi1 env
in
2110 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2111 anno res2 [child1
;child2
]
2113 Printf.printf
"Ref\n"; flush stdout
;
2114 let res = List.assoc v env
in
2117 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2120 | A.XX
(phi
) -> failwith
"should have been removed" in
2121 let res1 = drop_wits required_states
res phi
in
2125 print_required_states required_states
;
2126 print_state "after drop_wits" res1 end;
2131 let sat_verbose annotate maxlvl lvl m phi
=
2132 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2134 (* Type for annotations collected in a tree *)
2135 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2137 let sat_annotree annotate m phi
=
2138 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2139 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2143 let sat m phi = satloop m phi []
2147 let simpleanno l phi
res =
2149 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2150 print_generic_algo
(List.sort compare
res);
2151 Format.print_string
"\n------------------------------\n\n" in
2152 let pp_dir = function
2154 | A.BACKWARD
-> pp "^" in
2156 | A.False
-> pp "False"
2157 | A.True
-> pp "True"
2158 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2159 | A.Not
(phi
) -> pp "Not"
2160 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2161 | A.And
(_
,phi1
,phi2
) -> pp "And"
2162 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2163 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2164 | A.Or
(phi1
,phi2
) -> pp "Or"
2165 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2166 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2167 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2168 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2169 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2170 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2171 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2172 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2173 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2174 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2175 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2176 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2177 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2178 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2179 | A.Uncheck
(s) -> pp "Uncheck"
2180 | A.InnerAnd
(s) -> pp "InnerAnd"
2181 | A.XX
(phi1
) -> pp "XX"
2185 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2186 print a ctl formula more accurately if you want.
2187 Use the print_xxx provided in the different module to call
2188 Pretty_print_ctl.pp_ctl.
2191 let simpleanno2 l phi
res =
2193 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2194 Format.print_newline
();
2195 Format.print_string
"----------------------------------------------------";
2196 Format.print_newline
();
2197 print_generic_algo
(List.sort compare
res);
2198 Format.print_newline
();
2199 Format.print_string
"----------------------------------------------------";
2200 Format.print_newline
();
2201 Format.print_newline
();
2205 (* ---------------------------------------------------------------------- *)
2207 (* ---------------------------------------------------------------------- *)
2209 type optentry
= bool ref * string
2210 type options
= {label : optentry
; unch
: optentry
;
2211 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2213 reqenv
: optentry
; reqstates
: optentry
}
2216 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2217 unch
= (pUNCHECK_OPT,"uncheck_opt");
2218 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2219 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2220 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2221 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2222 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2223 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2227 ("label ",[options.label]);
2228 ("unch ",[options.unch
]);
2229 ("unch and label ",[options.label;options.unch
])]
2232 [("conj ", [options.conj]);
2233 ("compl1 ", [options.compl1
]);
2234 ("compl12 ", [options.compl1
;options.compl2
]);
2235 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2236 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2238 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2239 ("compl12 unch satl ",
2240 [options.compl1;options.compl2;options.unch;options.label]); *)
2241 ("conj/compl12 unch satl ",
2242 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2245 [("newinfo ", [options.newinfo
]);
2246 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2249 [("reqenv ", [options.reqenv
]);
2250 ("reqstates ", [options.reqstates
]);
2251 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2252 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2253 ("reqstates unch satl ",
2254 [options.reqstates;options.unch;options.label]);*)
2255 ("reqenv/states unch satl ",
2256 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2259 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2260 options.newinfo
;options.reqenv
;options.reqstates
]
2263 [("all ",all_options)]
2265 let all_options_but_path =
2266 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2267 options.reqenv
;options.reqstates
]
2269 let all_but_path = ("all but path ",all_options_but_path)
2272 [(satAW_calls, "satAW", ref 0);
2273 (satAU_calls, "satAU", ref 0);
2274 (satEF_calls, "satEF", ref 0);
2275 (satAF_calls, "satAF", ref 0);
2276 (satEG_calls, "satEG", ref 0);
2277 (satAG_calls, "satAG", ref 0);
2278 (satEU_calls, "satEU", ref 0)]
2282 (function (opt
,x) ->
2283 (opt
,x,ref 0.0,ref 0,
2284 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2285 [List.hd
all;all_but_path]
2286 (*(all@baseline@conjneg@path@required)*)
2290 let rec iter fn = function
2292 | n
-> let _ = fn() in
2293 (Hashtbl.clear
reachable_table;
2294 Hashtbl.clear
memo_label;
2298 let copy_to_stderr fl
=
2299 let i = open_in fl
in
2301 Printf.fprintf stderr
"%s\n" (input_line
i);
2303 try loop() with _ -> ();
2306 let bench_sat (_,_,states) fn =
2307 List.iter (function (opt
,_) -> opt
:= false) all_options;
2310 (function (name
,options,time
,trips,counter_info
) ->
2311 let iterct = !Flag_ctl.bench
in
2312 if !time
> float_of_int
timeout then time
:= -100.0;
2313 if not
(!time
= -100.0)
2316 Hashtbl.clear
reachable_table;
2317 Hashtbl.clear
memo_label;
2318 List.iter (function (opt
,_) -> opt
:= true) options;
2319 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2323 let bef = Sys.time
() in
2325 Common.timeout_function
timeout
2327 let bef = Sys.time
() in
2328 let res = iter fn iterct in
2329 let aft = Sys.time
() in
2330 time
:= !time
+. (aft -. bef);
2331 trips := !trips + !triples;
2333 (function (calls
,_,save_calls
) ->
2334 function (current_calls
,current_cfg
,current_max_cfg
) ->
2336 !current_calls
+ (!calls
- !save_calls
);
2337 if (!calls
- !save_calls
) > 0
2339 (let st = List.length
states in
2340 current_cfg
:= !current_cfg
+ st;
2341 if st > !current_max_cfg
2342 then current_max_cfg
:= st))
2343 counters counter_info
;
2348 let aft = Sys.time
() in
2350 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2354 List.iter (function (opt
,_) -> opt
:= false) options;
2359 Printf.fprintf stderr
"\n";
2363 (if not
(List.for_all
(function x -> x = res) rest
)
2365 (List.iter (print_state "a state") answers;
2366 Printf.printf
"something doesn't work\n");
2370 let iterct = !Flag_ctl.bench
in
2374 (function (name
,options,time
,trips,counter_info
) ->
2375 Printf.fprintf stderr
"%s Numbers: %f %d "
2376 name
(!time
/. (float_of_int
iterct)) !trips;
2378 (function (calls
,cfg
,max_cfg
) ->
2379 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2381 Printf.fprintf stderr
"\n")
2384 (* ---------------------------------------------------------------------- *)
2385 (* preprocessing: ignore irrelevant functions *)
2387 let preprocess (cfg
,_,_) label = function
2388 [] -> true (* no information, try everything *)
2390 let sz = G.size cfg
in
2391 let verbose_output pred = function
2393 Printf.printf
"did not find:\n";
2394 P.print_predicate
pred; Format.print_newline
()
2396 Printf.printf
"found:\n";
2397 P.print_predicate
pred; Format.print_newline
();
2398 Printf.printf
"but it was not enough\n" in
2399 let get_any verbose
x =
2401 try Hashtbl.find
memo_label x
2404 (let triples = label x in
2406 List.map (function (st,th
,_) -> (st,th
)) triples in
2407 Hashtbl.add memo_label x filtered;
2409 if verbose
then verbose_output x res;
2412 (* don't bother testing when there are more patterns than nodes *)
2413 if List.length l
> sz-2
2415 else List.for_all
(get_any false) l
in
2416 if List.exists
get_all l
2419 (if !Flag_ctl.verbose_match
2421 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2425 let filter_partial_matches trips =
2426 if !Flag_ctl.partial_match
2428 let anynegwit = (* if any is neg, then all are *)
2429 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2431 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2434 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2438 (* ---------------------------------------------------------------------- *)
2439 (* Main entry point for engine *)
2440 let sat m phi reqopt
=
2442 (match !Flag_ctl.steps
with
2443 None
-> step_count := 0
2444 | Some
x -> step_count := x);
2445 Hashtbl.clear
reachable_table;
2446 Hashtbl.clear
memo_label;
2447 let (x,label,states) = m
in
2448 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2450 ((* to drop when Yoann initialized this flag *)
2451 if List.exists
(G.extract_is_loop
x) states
2452 then Flag_ctl.loop_in_src_code
:= true;
2453 let m = (x,label,List.sort compare
states) in
2455 if(!Flag_ctl.verbose_ctl_engine
)
2457 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2458 if !Flag_ctl.bench
> 0
2462 let fn _ = satloop false [] None
m phi
[] in
2463 if !Flag_ctl.bench
> 0
2465 else Common.profile_code
"ctl" (fun _ -> fn()) in
2466 let res = filter_partial_matches res in
2468 Printf.printf "steps: start %d, stop %d\n"
2469 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2471 Printf.printf "triples: %d\n" !triples;
2472 print_state "final result" res;
2474 List.sort compare
res)
2476 (if !Flag_ctl.verbose_ctl_engine
2477 then Common.pr2
"missing something required";
2482 (* ********************************************************************** *)
2483 (* End of Module: CTL_ENGINE *)
2484 (* ********************************************************************** *)