1
2
3structure holCheckTools =
4struct
5local
6
7open Globals HolKernel Parse
8open pairSyntax
9open ctlSyntax muSyntax ctl2muTools commonTools
10
11val dpfx = "hct_"
12
13in
14
15fun find_aps f = HOLset.listItems(HOLset.addList(HOLset.empty Term.compare,
16                                                 List.map rand ((ctlSyntax.find_BPROPs f)@(muSyntax.find_APs f))))
17
18(*FIXME: we need to be smarter about extracting ap's
19         e.g. currently for 2x2 ttt, m, ~m and ~~m become three abs vars, whereas the concrete ks had only m *)
20fun mk_abs_APs' f state =
21    let val _ = dbgTools.DEN dpfx "maA'"(*DBG*)
22        val is_mu = ((String.compare(fst(dest_type(type_of f)),"mu"))=EQUAL)
23        val muf = if is_mu then f else ctl2muTools.ctl2mu f
24        val prop_tms = prop_subtmset muf 1
25        val ap = List.map (fn p => prop2ap p state) prop_tms (*FIXME: don't use abstraction if number of AP's is too high *)
26        val aps = List.map mu_AP ap
27        val _ = List.app (fn (p,a) => (dbgTools.DTM (dpfx^"mA'_p") p;dbgTools.DTM (dpfx^"mA'_a") a)) (ListPair.zip(prop_tms,ap))
28        val apsubs = mk_subst prop_tms aps (* used to convert formulas in fl to use the new APs *)
29        val _ = List.app (dbgTools.DTM (dpfx^"maA'_ap")) ap
30        val _ = dbgTools.DEX dpfx "maA'"(*DBG*)
31    in (ap,apsubs) end
32
33(* find all the atomic propositions in the list of properties in fl *)
34(* note we need to provide special provision in mk_abs_APs' for logics other than mu-calculus *)
35(* return NONE if the number of atomic propositions is >= number of concrete state vars since abs won't help in that case*)
36fun mk_abs_APs fl state =
37    let val _ = dbgTools.DEN (dpfx^"_maA") (*DBG*)
38        val _ = profTools.bgt (dpfx^"maA") (*PRF*)
39        val (apl,apsubs) = (List.concat##List.concat) (ListPair.unzip (List.map (fn f => mk_abs_APs' (snd f) state) fl))
40        val apl = HOLset.listItems (HOLset.addList(HOLset.empty Term.compare,apl))
41        val cl = List.length (strip_pair state)
42        val al = List.length apl
43        val _ = dbgTools.DNM (dpfx^"_maA_cnum") cl (*DBG*)
44        val _ = dbgTools.DNM (dpfx^"_maA_anum") al (*DBG*)
45        val _ = dbgTools.DEN (dpfx^"_maA") (*DBG*)
46        val _ = profTools.ent (dpfx^"maA") (*PRF*)
47    in (if al >= cl then NONE else SOME apl,apsubs) end
48
49
50end
51end
52