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