From cb12f8a525d1db35a8bc64c53d52b6c4337c77e9 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 26 Jan 2016 16:30:21 +0100
Subject: [PATCH] Calculate deferral when building FL-Closure
---
src/lib/CoAlgMisc.ml | 57 ++++++++++++++++++++++++++------------------
1 file changed, 34 insertions(+), 23 deletions(-)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 34b70ff..106569f 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -781,13 +781,19 @@ let lfToAt _ lf = lf
TODO: variable sort needs to match epected sort
*)
-let rec detClosure nomTbl hcF fset atset nomset s f =
+let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
+ let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
+ let detClosure_ = detClosure newvars in
+ let deferral = if List.length newvars > 0
+ then (List.hd newvars)
+ else "ε" in
if s < 0 || s >= Array.length fset then
let sstr = string_of_int s in
raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
else ();
if C.HcFHt.mem fset.(s) f then ()
else
+ let () = C.HcFHt.add vset.(s) f deferral in
let () = C.HcFHt.add fset.(s) f () in
let (func, sortlst) = !sortTable.(s) in
match f.HC.node with
@@ -815,37 +821,37 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
| Some sort -> sort
in
let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
- detClosure nomTbl hcF fset atset nomset s1 hcnom;
- detClosure nomTbl hcF fset atset nomset s1 f1
+ detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
+ detClosure_ nomTbl hcF fset vset atset nomset s1 f1
| C.HCOR (f1, f2)
| C.HCAND (f1, f2) ->
- detClosure nomTbl hcF fset atset nomset s f1;
- detClosure nomTbl hcF fset atset nomset s f2
+ detClosure_ nomTbl hcF fset vset atset nomset s f1;
+ detClosure_ nomTbl hcF fset vset atset nomset s f2
| C.HCEX (_, f1)
| C.HCAX (_, f1) ->
if (func <> MultiModalK && func <> MultiModalKD)
|| List.length sortlst <> 1
then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCENFORCES (_, f1)
| C.HCALLOWS (_, f1) ->
if func <> CoalitionLogic || List.length sortlst <> 1
then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCMORETHAN (_,_,f1)
| C.HCMAXEXCEPT (_,_,f1) ->
if func <> GML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCATLEASTPROB (_,f1)
| C.HCLESSPROBFAIL (_,f1) ->
if func <> PML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
(*
TODO: add ¬ f1 to the closure!
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
@@ -868,37 +874,39 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
then raise (C.CoAlgException "Identity operator applied to
formula of wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
| C.HCNORM (f1, f2)
| C.HCNORMN(f1, f2) ->
if func <> DefaultImplication || List.length sortlst <> 1 then
raise (C.CoAlgException "Default Implication applied to
formulae of wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
| C.HCCHC (f1, f2) ->
if func <> Choice || List.length sortlst <> 2 then
raise (C.CoAlgException "Choice formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
| C.HCFUS (first, f1) ->
if func <> Fusion || List.length sortlst <> 2 then
raise (C.CoAlgException "Fusion formula is used in wrong sort.")
else ();
let s1 = List.nth sortlst (if first then 0 else 1) in
- detClosure nomTbl hcF fset atset nomset s1 f1
+ detClosure_ nomTbl hcF fset vset atset nomset s1 f1
(*
FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
*)
| C.HCMU (name, f1) ->
+ let () = C.HcFHt.replace vset.(s) f name in
let unfold = C.hc_replace hcF name f f1 in
- detClosure nomTbl hcF fset atset nomset s unfold
+ let appendvars = List.append newvars [name] in
+ detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
| C.HCNU (name, f1) ->
let unfold = C.hc_replace hcF name f f1 in
- detClosure nomTbl hcF fset atset nomset s unfold
+ detClosure_ nomTbl hcF fset vset atset nomset s unfold
let detClosureAt hcF atset name f () =
@@ -1096,16 +1104,19 @@ let ppFormulae nomTbl tbox (s, f) =
let hctrue = C.hc_formula hcF C.TRUE in
let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
+ let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
let atset = C.HcFHt.create 64 in
let nomset = Hashtbl.create 16 in
for i = 0 to card-1 do
- detClosure nomTbl hcF fset atset nomset i hcfalse;
- detClosure nomTbl hcF fset atset nomset i hctrue;
+ detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
+ detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
done;
- detClosure nomTbl hcF fset atset nomset s hcf;
- detClosure nomTbl hcF fset atset nomset s nhcf;
- List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox;
- List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox;
+ detClosure [] nomTbl hcF fset vset atset nomset s hcf;
+ detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
+ List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ hctbox;
+ List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ nhctbox;
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
--
GitLab