23 
23 
 CoAlgFormula.IMP (f1, f2) > CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2))

24 
24 
 CoAlgFormula.EX (s, f) > CoAlgFormula.EX (s, (rename_formula1 f))

25 
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))

26 
34 
 CoAlgFormula.ID f > CoAlgFormula.ID (rename_formula1 f)

27 
35 
 CoAlgFormula.MU (s, f) > CoAlgFormula.MU (s, (rename_formula1 f))

28 
36 
 CoAlgFormula.NU (s, f) > CoAlgFormula.NU (s, (rename_formula1 f))

...  ...  
35 
43 
rename_formula1 f

36 
44 

37 
45 
(*calculates inner term of inv for one subformula*)

38 

let calcforsub subf noms =


46 
let calcforsub subf noms funct =

39 
47 
let ret = ref CoAlgFormula.TRUE in

40 
48 
for i = 0 to (List.length !noms)  1 do

41 
49 
let aktnom = CoAlgFormula.AP(List.nth !noms i) in

42 

ret := CoAlgFormula.IMP(CoAlgFormula.EF(CoAlgFormula.AND(subf, aktnom)),CoAlgFormula.AG(CoAlgFormula.IMP(aktnom, subf)));


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);

43 
59 
done;

44 
60 

45 
61 
!ret

...  ...  
58 
74 
CoAlgMisc.sortTable := Array.copy sorts;

59 
75 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;

60 
76 


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

61 
78 

62 
79 
let hashedformulaList = ref [] in

63 
80 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0);

...  ...  
69 
86 
done;

70 
87 
(*end calc flc*)

71 
88 

72 

let ret = ref (calcforsub (List.hd !formulaList) noms) in


89 
let ret = ref (calcforsub (List.hd !formulaList) noms funct) in

73 
90 
for i = 1 to (List.length !formulaList)  1 do

74 

let sub = calcforsub (List.nth !formulaList i) noms in

75 

ret := CoAlgFormula.AND(!ret, sub);


91 
let akt = List.nth !formulaList i in


92 
match akt with


93 
 CoAlgFormula.AND (f1,f2)


94 
 CoAlgFormula.OR (f1,f2) > ret := !ret;


95 
 _ > let sub = calcforsub (List.nth !formulaList i) noms funct in


96 
ret := CoAlgFormula.AND(!ret, sub);

76 
97 
done;

77 
98 

78 
99 
!ret

...  ...  
92 
113 

93 
114 
(*first calculate flc then rename nominals*)

94 
115 
let invhelp = calcinv f noms nomTbl sorts s in

95 

(*print_string "invhelp: ";

96 

print_endline (CoAlgFormula.exportFormula invhelp);*)

97 


98 
116 
let inv = rename invhelp nomsub noms in

99 

(*print_string "inv: ";

100 

print_endline (CoAlgFormula.exportFormula inv);*)

101 
117 

102 
118 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in


119 
print_string "Formula with EF/AG: ";


120 
print_endline (CA.exportFormula formula);

103 
121 
let ret = CA.convertToMu formula in

104 
122 

105 
123 
ret
