Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / Nom2fix.ml @ 1d36cd07

History | View | Annotate | Download (9.51 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.CoalitionLogic -> CA.IMP(CA.MU("X", CA.OR(CA.AND(aktnom, subf),CA.ALLOWS([], VAR "X"))),CA.NU("X", CA.AND(CA.IMP(aktnom, subf),CA.ENFORCES([], VAR "X"))))
54
    | CoAlgMisc.Constant sl -> CA.IMP(CA.AND(aktnom, subf), CA.IMP(aktnom, subf))
55
    | CoAlgMisc.Identity -> CA.IMP(CA.MU("X", CA.OR(CA.AND(aktnom, subf),CA.ID(VAR "X"))),CA.NU("X", CA.AND(CA.IMP(aktnom, subf),CA.ID(VAR "X"))))
56
    in
57
        ret := AND(!ret, add);
58
  done;
59

    
60
  !ret
61

    
62
let calcinvnonopt f noms nomTbl sorts s =
63
  (*calc flc*)
64
  let card = Array.length sorts in
65
  let hcF = CoAlgFormula.HcFormula.create true in
66
  let fset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
67
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
68
  let atset = CoAlgFormula.HcFHt.create 64 in
69
  let nomset = Hashtbl.create 16 in
70

    
71
  let hcform = CoAlgFormula.hc_formula hcF f in
72

    
73
  CoAlgMisc.sortTable := Array.copy sorts;
74
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
75

    
76
  let (funct, l) = Array.get sorts 0 in
77

    
78
  let hashedformulaList = ref [] in
79
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
80
  
81
  let formulaList = ref [] in
82

    
83
  for i = 0 to (List.length !hashedformulaList) - 1 do
84
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
85
  done;
86
  (*end calc flc*)
87

    
88
  let ret = ref (calcforsub (List.hd !formulaList) noms funct) in
89
  for i = 1 to (List.length !formulaList) - 1 do
90
    let akt = List.nth !formulaList i in
91
    let sub = calcforsub (List.nth !formulaList i) noms funct in
92
           ret := CoAlgFormula.AND(!ret, sub);
93
  done;
94

    
95
  !ret
96

    
97
let delFix foo =
98
let rec selFixpoints fo =
99
  let n = CoAlgFormula.depthFormula fo in
100
  match fo with 
101
    | CoAlgFormula.FALSE -> CoAlgFormula.FALSE
102
    | CoAlgFormula.TRUE -> CoAlgFormula.TRUE
103
    | CoAlgFormula.AP s -> CoAlgFormula.AP s
104
    | CoAlgFormula.NOT f -> CoAlgFormula.NOT (selFixpoints f)
105
    | CoAlgFormula.OR (f1, f2) -> CoAlgFormula.OR ((selFixpoints f1), (selFixpoints f2))
106
    | CoAlgFormula.AND (f1, f2) -> CoAlgFormula.AND ((selFixpoints f1), (selFixpoints f2))
107
    | CoAlgFormula.EQU (f1, f2) -> CoAlgFormula.EQU ((selFixpoints f1), (selFixpoints f2))
108
    | CoAlgFormula.IMP (f1, f2) -> CoAlgFormula.IMP ((selFixpoints f1), (selFixpoints f2))
109
    | CoAlgFormula.EX (s, f) -> CoAlgFormula.EX (s, (selFixpoints f))
110
    | CoAlgFormula.AX (s, f) -> CoAlgFormula.AX (s, (selFixpoints f))
111
    | CoAlgFormula.ENFORCES (l, f) -> CoAlgFormula.ENFORCES(l, (selFixpoints f))
112
    | CoAlgFormula.ALLOWS (l, f) -> CoAlgFormula.ALLOWS(l, (selFixpoints f))
113
    | CoAlgFormula.MIN (i, s, f) -> CoAlgFormula.MIN(i, s, (selFixpoints f))
114
    | CoAlgFormula.MAX (i, s, f) -> CoAlgFormula.MAX(i, s, (selFixpoints f))
115
    | CoAlgFormula.MORETHAN (i, s, f) -> CoAlgFormula.MORETHAN(i, s, (selFixpoints f))
116
    | CoAlgFormula.MAXEXCEPT (i, s, f) -> CoAlgFormula.MAXEXCEPT(i, s, (selFixpoints f))
117
    | CoAlgFormula.ATLEASTPROB (r, f) -> CoAlgFormula.ATLEASTPROB(r, (selFixpoints f))
118
    | CoAlgFormula.LESSPROBFAIL (r, f) -> CoAlgFormula.LESSPROBFAIL (r, (selFixpoints f))
119
    | CoAlgFormula.ID f -> CoAlgFormula.ID (selFixpoints f)
120
    | CoAlgFormula.MU (s, f) -> 
121
        let ret = ref CoAlgFormula.FALSE in
122
        for i = 1 to n+1 do
123
          ret := CoAlgFormula.OR(f, EX("",!ret));
124
        done;
125
        !ret
126
    | CoAlgFormula.NU (s, f) -> 
127
        let ret = ref CoAlgFormula.TRUE in
128
        for i = 1 to n+1 do
129
          ret := CoAlgFormula.AND(f, AX("",!ret));
130
        done;
131
        !ret
132
    | CoAlgFormula.AF f -> CoAlgFormula.AF (selFixpoints f)
133
    | CoAlgFormula.EF f -> CoAlgFormula.EF (selFixpoints f)
134
    | CoAlgFormula.AG f -> CoAlgFormula.AG (selFixpoints f)
135
    | CoAlgFormula.EG f -> CoAlgFormula.EG (selFixpoints f)
136
    | CoAlgFormula.VAR s -> CoAlgFormula.VAR s
137
in
138
selFixpoints foo
139

    
140

    
141
let calcinv f noms nomTbl sorts s =
142
  (*calc flc*)
143
  let card = Array.length sorts in
144
  let hcF = CoAlgFormula.HcFormula.create true in
145
  let fset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
146
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
147
  let atset = CoAlgFormula.HcFHt.create 64 in
148
  let nomset = Hashtbl.create 16 in
149

    
150
  let hcform = CoAlgFormula.hc_formula hcF f in
151

    
152
  CoAlgMisc.sortTable := Array.copy sorts;
153
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
154

    
155
  let (funct, l) = Array.get sorts 0 in
156

    
157
  let hashedformulaList = ref [] in
158
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
159
  
160
  let formulaList = ref [] in
161

    
162
  for i = 0 to (List.length !hashedformulaList) - 1 do
163
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
164
  done;
165
  (*end calc flc*)
166

    
167
  let formulaListSmall = ref [] in
168

    
169
  let rem = ref false in
170

    
171
  for i = 0 to (List.length !formulaList) - 1 do
172
    for j = i + 1 to (List.length !formulaList) - 1 do
173
      rem := if CoAlgFormula.equals (List.nth !formulaList i) (CoAlgFormula.nnfNeg (List.nth !formulaList j)) then true else !rem;
174
      (*print_endline (if !rem == true then "true" else "false");
175
      print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnf (List.nth !formulaList i)));
176
      print_endline (CoAlgFormula.exportFormula (CoAlgFormula.nnfNeg (List.nth !formulaList j)));*)
177
    done;
178
    if !rem == false then formulaListSmall := (List.nth !formulaList i) :: !formulaListSmall;
179
    rem := false;
180
  done; 
181

    
182
  let ret = ref CoAlgFormula.TRUE in
183
  for i = 0 to (List.length !formulaListSmall) - 1 do
184
    let akt = List.nth !formulaListSmall i in
185
    match akt with
186
    | CoAlgFormula.AND (f1,f2)
187
    | CoAlgFormula.OR (f1,f2) -> ret := !ret;
188
    | CoAlgFormula.NOT f1 -> let sub = calcforsub f1 noms funct in
189
          ret := CoAlgFormula.AND(!ret, sub);
190
    | _ -> let sub = calcforsub (List.nth !formulaListSmall i) noms funct in
191
           ret := CoAlgFormula.AND(!ret, sub);
192
  done;
193

    
194
  !ret
195

    
196
let translate fu nomTbl sorts s opt =
197
  let f = (CA.nnf fu) in
198

    
199
  (*list of nominals*)
200
  let noms = ref [] in
201
  (*mapping from nominals to new syms*)
202
  let nomsub = ref StringMap.empty in
203

    
204
  (*first rename nominals then change type to eaformula*)
205
  let ren = rename f nomsub noms in
206
  (*print_string "using Formula: ";
207
  print_endline (CA.exportFormula ren);*)
208

    
209
  (*first calculate flc then rename nominals*)
210
  let invhelp = match opt with
211
    | true -> calcinv f noms nomTbl sorts s
212
    | false -> calcinvnonopt f noms nomTbl sorts s
213
  in
214
  let inv = rename invhelp nomsub noms in
215

    
216
  let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in
217
  (*print_string "Formula with EF/AG: ";
218
  print_endline (CA.exportFormula formula);*)
219
  let ret = CA.convertToMu formula in
220
 
221
  ret
222

    
223
(* vim: set et sw=2 sts=2 ts=8 : *)