cool / src / lib / Nom2fix.ml @ 2d58f46f
History  View  Annotate  Download (6.44 KB)
1 
module CA = CoAlgFormula 

2 
module StringMap = Map.Make(String) 
3  
4 
type nomTbl = string > CoAlgFormula.sort option 
5 
let gensym = Stream.from (fun i > Some (Printf.sprintf "#gensym%x#" i)) 
6  
7  
8 
let rename f nomsub noms = 
9 
let rec rename_formula1 f = 
10 
let name = Stream.next gensym in 
11 
match f with 
12 
 CoAlgFormula.FALSE > CoAlgFormula.FALSE 
13 
 CoAlgFormula.TRUE > CoAlgFormula.TRUE 
14 
 CoAlgFormula.AP s > 
15 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms; 
16 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub; 
17 
if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub) 
18 
else CoAlgFormula.AP s 
19 
 CoAlgFormula.NOT f > CoAlgFormula.NOT (rename_formula1 f) 
20 
 CoAlgFormula.OR (f1, f2) > CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2)) 
21 
 CoAlgFormula.AND (f1, f2) > CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2)) 
22 
 CoAlgFormula.EQU (f1, f2) > CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2)) 
23 
 CoAlgFormula.IMP (f1, f2) > CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2)) 
24 
 CoAlgFormula.EX (s, f) > CoAlgFormula.EX (s, (rename_formula1 f)) 
25 
 CoAlgFormula.AX (s, f) > CoAlgFormula.AX (s, (rename_formula1 f)) 
26 
 CoAlgFormula.ENFORCES (l, f) > CoAlgFormula.ENFORCES(l, (rename_formula1 f)) 
27 
 CoAlgFormula.ALLOWS (l, f) > CoAlgFormula.ALLOWS(l, (rename_formula1 f)) 
28 
 CoAlgFormula.MIN (i, s, f) > CoAlgFormula.MIN(i, s, (rename_formula1 f)) 
29 
 CoAlgFormula.MAX (i, s, f) > CoAlgFormula.MAX(i, s, (rename_formula1 f)) 
30 
 CoAlgFormula.MORETHAN (i, s, f) > CoAlgFormula.MORETHAN(i, s, (rename_formula1 f)) 
31 
 CoAlgFormula.MAXEXCEPT (i, s, f) > CoAlgFormula.MAXEXCEPT(i, s, (rename_formula1 f)) 
32 
 CoAlgFormula.ATLEASTPROB (r, f) > CoAlgFormula.ATLEASTPROB(r, (rename_formula1 f)) 
33 
 CoAlgFormula.LESSPROBFAIL (r, f) > CoAlgFormula.LESSPROBFAIL (r, (rename_formula1 f)) 
34 
 CoAlgFormula.ID f > CoAlgFormula.ID (rename_formula1 f) 
35 
 CoAlgFormula.MU (s, f) > CoAlgFormula.MU (s, (rename_formula1 f)) 
36 
 CoAlgFormula.NU (s, f) > CoAlgFormula.NU (s, (rename_formula1 f)) 
37 
 CoAlgFormula.AF f > CoAlgFormula.AF (rename_formula1 f) 
38 
 CoAlgFormula.EF f > CoAlgFormula.EF (rename_formula1 f) 
39 
 CoAlgFormula.AG f > CoAlgFormula.AG (rename_formula1 f) 
40 
 CoAlgFormula.EG f > CoAlgFormula.EG (rename_formula1 f) 
41 
 CoAlgFormula.VAR s > CoAlgFormula.VAR s 
42 
in 
43 
rename_formula1 f 
44  
45 
(*calculates inner term of inv for one subformula*) 
46 
let calcforsub subf noms funct = 
47 
let ret = ref CoAlgFormula.TRUE in 
48 
for i = 0 to (List.length !noms)  1 do 
49 
let aktnom = CoAlgFormula.AP(List.nth !noms i) in 
50 
let add = match funct with 
51 
 CoAlgMisc.MultiModalK 
52 
 CoAlgMisc.MultiModalKD > CoAlgFormula.IMP(CoAlgFormula.EF(CoAlgFormula.AND(subf, aktnom)),CoAlgFormula.AG(CoAlgFormula.IMP(aktnom, subf))) 
53 
(* CoAlgMisc.Monotone >*) 
54 
(* CoAlgMisc.CoalitionLogic > CoAlgFormula.IMP(CoAlgFormula.MU(x, CoAlgFormula.OR(CoAlgFormula.AND(subf, aktnom), ))) 
55 
 CoAlgMisc.GML > 
56 
 CoAlgMisc.PML >*) 
57 
in 
58 
ret := AND(!ret, add); 
59 
done; 
60  
61 
!ret 
62  
63 
let calcinvnonopt f noms nomTbl sorts s = 
64 
(*calc flc*) 
65 
let card = Array.length sorts in 
66 
let hcF = CoAlgFormula.HcFormula.create true in 
67 
let fset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
68 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
69 
let atset = CoAlgFormula.HcFHt.create 64 in 
70 
let nomset = Hashtbl.create 16 in 
71  
72 
let hcform = CoAlgFormula.hc_formula hcF f in 
73  
74 
CoAlgMisc.sortTable := Array.copy sorts; 
75 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform; 
76  
77 
let (funct, l) = Array.get sorts 0 in 
78  
79 
let hashedformulaList = ref [] in 
80 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0); 
81 

82 
let formulaList = ref [] in 
83  
84 
for i = 0 to (List.length !hashedformulaList)  1 do 
85 
formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList); 
86 
done; 
87 
(*end calc flc*) 
88  
89 
let ret = ref (calcforsub (List.hd !formulaList) noms funct) in 
90 
for i = 1 to (List.length !formulaList)  1 do 
91 
let akt = List.nth !formulaList i in 
92 
let sub = calcforsub (List.nth !formulaList i) noms funct in 
93 
ret := CoAlgFormula.AND(!ret, sub); 
94 
done; 
95  
96 
!ret 
97  
98  
99 
let calcinv f noms nomTbl sorts s = 
100 
(*calc flc*) 
101 
let card = Array.length sorts in 
102 
let hcF = CoAlgFormula.HcFormula.create true in 
103 
let fset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
104 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
105 
let atset = CoAlgFormula.HcFHt.create 64 in 
106 
let nomset = Hashtbl.create 16 in 
107  
108 
let hcform = CoAlgFormula.hc_formula hcF f in 
109  
110 
CoAlgMisc.sortTable := Array.copy sorts; 
111 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform; 
112  
113 
let (funct, l) = Array.get sorts 0 in 
114  
115 
let hashedformulaList = ref [] in 
116 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0); 
117 

118 
let formulaList = ref [] in 
119  
120 
for i = 0 to (List.length !hashedformulaList)  1 do 
121 
formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList); 
122 
done; 
123 
(*end calc flc*) 
124  
125 
let ret = ref (calcforsub (List.hd !formulaList) noms funct) in 
126 
for i = 1 to (List.length !formulaList)  1 do 
127 
let akt = List.nth !formulaList i in 
128 
match akt with 
129 
 CoAlgFormula.NOT f1 > ret := !ret; 
130 
 CoAlgFormula.AND (f1,f2) 
131 
 CoAlgFormula.OR (f1,f2) > ret := !ret; 
132 
 _ > let sub = calcforsub (List.nth !formulaList i) noms funct in 
133 
ret := CoAlgFormula.AND(!ret, sub); 
134 
done; 
135  
136 
!ret 
137  
138 
let translate fu nomTbl sorts s opt = 
139 
let f = (CA.nnf fu) in 
140  
141 
(*list of nominals*) 
142 
let noms = ref [] in 
143 
(*mapping from nominals to new syms*) 
144 
let nomsub = ref StringMap.empty in 
145  
146 
(*first rename nominals then change type to eaformula*) 
147 
let ren = rename f nomsub noms in 
148 
(*print_string "using Formula: "; 
149 
print_endline (CA.exportFormula ren);*) 
150  
151 
(*first calculate flc then rename nominals*) 
152 
let invhelp = match opt with 
153 
 true > calcinv f noms nomTbl sorts s 
154 
 false > calcinvnonopt f noms nomTbl sorts s 
155 
in 
156 
let inv = rename invhelp nomsub noms in 
157  
158 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in 
159 
(*print_string "Formula with EF/AG: "; 
160 
print_endline (CA.exportFormula formula);*) 
161 
let ret = CA.convertToMu formula in 
162 

163 
ret 
164  
165 
(* vim: set et sw=2 sts=2 ts=8 : *) 