Commit 1c6b0483 authored by Ludwig Dietel's avatar Ludwig Dietel
Browse files

final cleanup for coalgebraic EL

parent f04c7b24
......@@ -22,10 +22,7 @@ let checkFormula sorts tbox sort subsumee subsumer =
CoAlgLogics.model true;
CoAlgReasoner.buildModel (CoAlgMisc.graphGetRoot ());
CoAlgLogics.model false;
(* Switch to satisfiability mode *)
CoAlgMisc.graphIterCores (fun core -> print_endline (CoAlgMisc.coreToString core));
CoAlgMisc.graphIterStates (fun state -> print_endline (CoAlgMisc.stateToString state));
print_endline "=== compute Extensions ===";
(* Switch to satisfiability mode *)
CoAlgReasoner.computeExtensions ();
CoAlgReasoner.modelCheck (CoAlgMisc.graphGetRoot ()) lfsubsumer
......@@ -41,7 +38,7 @@ let isSubsumed ?(verbose = false) sorts tbox queries =
| CoAlgFormula.INCLUSION(f1, f2) ->
if verbose then print_endline "Subsumption Checking in polynomial-time" else ();
checkFormula sorts tbox s f1 f2
| CoAlgFormula.DEFINITION(f1, f2) ->
| CoAlgFormula.EQUALITY(f1, f2) ->
if verbose then print_endline "Equivalence Checking per reduction to Subsumption Checking" else ();
(checkFormula sorts tbox s f1 f2) && (checkFormula sorts tbox s f2 f1)
in
......
......@@ -76,7 +76,7 @@ type formula =
(** Defines (unsorted) coalgebraic axioms for the TBox.
*)
type axiom =
| DEFINITION of formula * formula
| EQUALITY of formula * formula
| INCLUSION of formula * formula
exception ConversionException of formula
......@@ -1524,7 +1524,7 @@ let rec simplify f =
let exportSortedAxiom = function
| (s, INCLUSION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " [= " ^ (exportFormula f2)
| (s, DEFINITION(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " := " ^ (exportFormula f2)
| (s, EQUALITY(f1, f2)) -> (string_of_int s) ^ ": " ^ (exportFormula f1) ^ " := " ^ (exportFormula f2)
(** Destructs a nominal.
@param s the input stream
......@@ -1552,7 +1552,7 @@ let importAxiomQuery s =
let f = match Stream.peek ts with
| Some (A.Kwd ":=") ->
Stream.junk ts;
(nr, DEFINITION(f1, simplify (nnf (parse_formula [] ts))))
(nr, EQUALITY(f1, simplify (nnf (parse_formula [] ts))))
| Some (A.Kwd "[=") ->
Stream.junk ts;
(nr, INCLUSION(f1, simplify (nnf (parse_formula [] ts))))
......
......@@ -58,7 +58,7 @@ type formula =
(** Defines (unsorted) coalgebraic axioms for the TBox.
*)
type axiom =
| DEFINITION of formula * formula
| EQUALITY of formula * formula
| INCLUSION of formula * formula
exception ConversionException of formula
......
......@@ -260,16 +260,6 @@ let mkRule_Monotone sort bs defer sl : stateExpander =
let rules = mkRuleList_Monotone sort bs defer sl in
lazylistFromList rules
(**
Coalgebraic Monotone Modal Logic
Game logic
*)
let mkRule_MultiModalM sort bs defer sl : stateExpander =
let rules = [] in
lazylistFromList rules
(* CoalitionLogic: helper functions *)
(*val subset : bitset -> bitset -> bool*)
let bsetlen (a: bset) : int =
......@@ -725,7 +715,6 @@ let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
| Monotone -> mkRule_Monotone
| MultiModalM -> mkRule_MultiModalM
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
| PML -> mkRule_PML
......
......@@ -81,7 +81,6 @@ type functors =
| MultiModalK
| MultiModalKD
| Monotone
| MultiModalM
| CoalitionLogic
| GML
| PML
......@@ -104,13 +103,11 @@ let unaryfunctor2name : (functorName*string) list =
[ (NPa MultiModalK , "MultiModalK")
; (NPa MultiModalKD , "MultiModalKD")
; (NPa Monotone , "Monotone")
; (NPa MultiModalM , "MultiModalM")
; (NPa GML , "GML")
; (NPa PML , "PML")
; (NPa CoalitionLogic , "CoalitionLogic")
; (NPa MultiModalK , "K")
; (NPa MultiModalKD , "KD")
; (NPa MultiModalM , "M")
; (NPa CoalitionLogic , "CL")
; (Pa NameConstant , "Const")
; (Pa NameConstant , "Constant")
......@@ -968,7 +965,7 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
detClosure_ nomTbl hcF fset vset atset nomset s f2
| C.HCEX (_, f1)
| C.HCAX (_, f1) ->
if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone && func <> MultiModalM)
if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone)
|| List.length sortlst <> 1
then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
else ();
......@@ -1337,44 +1334,42 @@ let ppELFormulae tbox sort subsumee subsumer =
raise (C.CoAlgException "Number of sorts must be positive.")
else ();
let hcF = C.HcFormula.create true in
(*let rec makeHcTBox = function
| [] -> []
| (s, CoAlgFormula.DEFINITION(CoAlgFormula.AP(_) as name, value)) :: ts -> (s, C.hc_formula hcF name, C.hc_formula hcF value) :: (makeHcTBox ts)
| (s, CoAlgFormula.INCLUSION(CoAlgFormula.AP(str) as name, value)) :: ts -> (s, C.hc_formula hcF name, C.hc_formula hcF (CoAlgFormula.AND(CoAlgFormula.AP(str ^ "*"), value))) :: (makeHcTBox ts)
| _ -> raise (CoAlgFormula.CoAlgException "TBox is not definitorial")
in
let hctbox = makeHcTBox tbox in*)
List.iter (fun ax -> print_endline (CoAlgFormula.exportSortedAxiom ax)) tbox;
let rec normalizeAxiom name counter = function
| CoAlgFormula.AND(f1, f2) ->
let (counter, current1, todos1) = normalizeAxiom name counter f1 in
let (counter, current2, todos2) = normalizeAxiom name counter f2 in
(counter, List.rev_append current1 current2, List.rev_append todos1 todos2)
(* Bekić principle *)
| CoAlgFormula.NU (symbol, f1) ->
(counter, [CoAlgFormula.AP(symbol)], [CoAlgFormula.EQUALITY(CoAlgFormula.AP(symbol), f1)])
(* Fixpointvariable *)
| CoAlgFormula.VAR(symbol) ->
(counter, [CoAlgFormula.AP(symbol)], [])
| CoAlgFormula.AX(f, CoAlgFormula.VAR(symbol)) ->
(counter, [CoAlgFormula.AX(f, CoAlgFormula.AP(symbol))], [])
| CoAlgFormula.EX(f, CoAlgFormula.VAR(symbol)) ->
(counter, [CoAlgFormula.EX(f, CoAlgFormula.AP(symbol))], [])
(** Bekić principle *)
| CoAlgFormula.NU (symbol, f1) ->
print_endline (symbol ^ " . " ^ (CoAlgFormula.exportFormula f1));
(counter, [CoAlgFormula.AP(symbol)], [CoAlgFormula.DEFINITION(CoAlgFormula.AP(symbol), f1)])
| CoAlgFormula.AND(f1, f2) ->
let (counter, current1, todos1) = normalizeAxiom name counter f1 in
let (counter, current2, todos2) = normalizeAxiom name counter f2 in
(counter, List.rev_append current1 current2, List.rev_append todos1 todos2)
(* Good ones *)
| CoAlgFormula.ALLOWS(f, CoAlgFormula.VAR(symbol)) ->
(counter, [CoAlgFormula.ALLOWS(f, CoAlgFormula.AP(symbol))], [])
| CoAlgFormula.ALLOWS(f, CoAlgFormula.VAR(symbol)) ->
(counter, [CoAlgFormula.ALLOWS(f, CoAlgFormula.AP(symbol))], [])
(* Good ones - nothing to do *)
| CoAlgFormula.AP(_)
| CoAlgFormula.AX(_, CoAlgFormula.AP(_))
| CoAlgFormula.EX(_, CoAlgFormula.AP(_)) as ap -> (counter, [ap], [])
(* Bad ones *)
| CoAlgFormula.AX(str, f) -> (succ counter, [CoAlgFormula.AX(str, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.DEFINITION(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| CoAlgFormula.EX(str, f) -> (succ counter, [CoAlgFormula.EX(str, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.DEFINITION(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| _ -> raise (CoAlgFormula.CoAlgException "TBox is not strange")
| CoAlgFormula.EX(_, CoAlgFormula.AP(_))
| CoAlgFormula.ALLOWS(_, CoAlgFormula.AP(_))
| CoAlgFormula.ENFORCES(_, CoAlgFormula.AP(_)) as ap -> (counter, [ap], [])
(* Bad ones - create new axiom *)
| CoAlgFormula.AX(str, f) -> (succ counter, [CoAlgFormula.AX(str, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.EQUALITY(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| CoAlgFormula.EX(str, f) -> (succ counter, [CoAlgFormula.EX(str, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.EQUALITY(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| CoAlgFormula.ALLOWS (s, f) -> (succ counter, [CoAlgFormula.ALLOWS(s, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.EQUALITY(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| CoAlgFormula.ENFORCES(s, f) -> (succ counter, [CoAlgFormula.ENFORCES(s, CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)))], [CoAlgFormula.EQUALITY(CoAlgFormula.AP(name ^ "*" ^ (string_of_int counter)), f)])
| f -> raise (CoAlgFormula.CoAlgException((CoAlgFormula.exportFormula f) ^ " is not allowed in TBox"))
in
(* watch out: GFP Semantics*)
let rec normalizeTBox = function
| CoAlgFormula.DEFINITION(CoAlgFormula.AP(name) as apname, definition)
| CoAlgFormula.EQUALITY(CoAlgFormula.AP(name) as apname, definition)
| CoAlgFormula.INCLUSION(CoAlgFormula.AP(name) as apname, definition) ->
let (_, current, todos) = normalizeAxiom name 0 definition in
List.rev_append [(apname, current)] (List.fold_left (fun acc f -> List.rev_append acc (normalizeTBox f)) [] todos)
......@@ -1382,29 +1377,9 @@ let ppELFormulae tbox sort subsumee subsumer =
in
let sharp = CoAlgFormula.AP("#") in
let ntbox = List.fold_left (fun acc (s, f) -> List.rev_append acc (normalizeTBox f)) [] ((0, CoAlgFormula.INCLUSION(sharp, subsumee)) :: tbox) in
(*List.iter (fun (name, value) -> (print_string ((CoAlgFormula.exportFormula name) ^ " := "); List.iter (fun va -> print_string ((CoAlgFormula.exportFormula va) ^ ", ")) value; print_newline())) ntbox;*)
let ntbox = List.fold_left (fun acc (s, f) -> List.rev_append acc (normalizeTBox f)) [] ((0, CoAlgFormula.INCLUSION(sharp, subsumee)) :: tbox) in
let hcntbox = List.map (fun (name, value) -> (0, C.hc_formula hcF name, List.map (fun va -> C.hc_formula hcF va) value)) ntbox in
let nhcntbox = List.map (fun (name, value) -> (0, C.hc_formula hcF (CoAlgFormula.NOT(name)), List.map (fun va -> C.hc_formula hcF (C.nnf (CoAlgFormula.NOT(va)))) value)) ntbox in
(* ALT
let hctbox = List.map (fun (s, f) -> (match f with
| CoAlgFormula.DEFINITION(CoAlgFormula.AP(_) as name, value) -> (s, C.hc_formula hcF name, C.hc_formula hcF value)
| CoAlgFormula.INCLUSION(CoAlgFormula.AP(str) as name, value) -> (s, C.hc_formula hcF name, C.hc_formula hcF (CoAlgFormula.AND(CoAlgFormula.AP(str ^ "*"), value)))
| _ -> raise (CoAlgFormula.CoAlgException "TBox is not definitorial")
)) tbox in
let nhctbox = List.map (fun (s, f) -> (match f with
| CoAlgFormula.DEFINITION(CoAlgFormula.AP(_) as name, value) -> (s, C.hc_formula hcF (C.NOT(name)), C.hc_formula hcF (C.simplify (C.nnf (C.NOT(value)))))
| CoAlgFormula.INCLUSION(CoAlgFormula.AP(str) as name, value) -> (s, C.hc_formula hcF (C.NOT(name)), C.hc_formula hcF (C.simplify (C.nnf (C.NOT(CoAlgFormula.AND(CoAlgFormula.AP(str ^ "*"), value))))))
| _ -> raise (CoAlgFormula.CoAlgException "TBox is not definitorial")
)) tbox in
let hcsubsumee = C.hc_formula hcF subsumee in*)
let hcsharp = C.hc_formula hcF sharp in
let hcsubsumer = C.hc_formula hcF subsumer in
let nhcsubsumer = C.hc_formula hcF (C.simplify (C.nnf (C.NOT subsumer))) in
......@@ -1426,16 +1401,8 @@ let nhctbox = List.map (fun (s, f) -> (match f with
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 sort hcsubsumee;*)
detClosure [] nomTbl hcF fset vset atset nomset sort hcsubsumer;
List.iter (fun (s, a, f) -> detClosure [] nomTbl hcF fset vset atset nomset s a; List.iter (fun fs -> detClosure [] nomTbl hcF fset vset atset nomset s fs) f) hcntbox;
(*List.iter (fun (s, a, f) -> detClosure [] nomTbl hcF fset vset atset nomset s a; List.iter (fun fs -> detClosure [] nomTbl hcF fset vset atset nomset s fs) f) nhcntbox;
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;*)
(*print_endline "=== neg. Formeln ===";
Array.iter (fun x -> C.HcFHt.iter (fun x _ -> print_endline (CoAlgFormula.exportFormula x.fml)) x) nfset;
print_endline "=== Formeln ===";
Array.iter (fun x -> C.HcFHt.iter (fun x _ -> print_endline (CoAlgFormula.exportFormula x.fml)) x) fset;*)
let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
for i = 0 to card-1 do
......@@ -1475,7 +1442,6 @@ let nhctbox = List.map (fun (s, f) -> (match f with
let htR = Hashtbl.create 128 in
Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
(*Hashtbl.iter (initTablesAt hcF htF) nomset;*)
S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
......@@ -1492,10 +1458,13 @@ let nhctbox = List.map (fun (s, f) -> (match f with
) hcntbox;
Array.iteri (fun sort tbl ->
let g = Hashtbl.fold (fun key value g ->
let g = bsetFold (fun lf g -> if Hashtbl.mem tbl lf then begin bsetRem value lf; G.add_edge g key lf end else g) value g in
Hashtbl.remove !tboxDefs.(sort) key;
Hashtbl.add !tboxDefs.(sort) key value;
g
bsetFold (fun lf g ->
if Hashtbl.mem tbl lf
then begin
bsetRem value lf;
G.add_edge g key lf
end else g
) value g
) tbl G.empty in
let ar = Com.scc_array g in
for n = 0 to (Array.length ar) - 1 do
......@@ -1505,16 +1474,8 @@ let nhctbox = List.map (fun (s, f) -> (match f with
with
Not_found -> raise (CoAlgFormula.CoAlgException "TBox name not found")
) (bsetMakeRealEmpty ()) ar.(n) in
List.iter (fun lf -> Hashtbl.remove !tboxDefs.(sort) lf; Hashtbl.add !tboxDefs.(sort) lf newbs) ar.(n)
List.iter (fun lf -> Hashtbl.replace !tboxDefs.(sort) lf newbs) ar.(n)
done
) !tboxDefs;
print_endline "=== Axiome ===";
Array.iteri (fun sort tbl ->
print_endline ("Sorte " ^ (string_of_int sort) ^ ":");
Hashtbl.iter (fun key value -> print_endline ((CoAlgFormula.exportFormula (lfGetFormula sort key)) ^ "\t:= " ^ (bsetToString sort value))) tbl
(*(" ^ (string_of_int key) ^ ")\t*)
) !tboxDefs;
negativeFormulas := Array.map (fun x ->
......@@ -1522,7 +1483,6 @@ let nhctbox = List.map (fun (s, f) -> (match f with
C.HcFHt.iter (fun x _ -> bsetAdd negbs (C.HcFHt.find htF.(sort) x)) x;
negbs
) nfset;
(*Array.iteri (fun s x -> print_endline ("Sorte " ^ (string_of_int s) ^ ": " (bsetToString s x))) !negativeFormulas;*)
let sharpbs = bsetMake () in
bsetAdd sharpbs (C.HcFHt.find htF.(sort) hcsharp);
......
......@@ -13,7 +13,6 @@ type functors =
| MultiModalK
| MultiModalKD
| Monotone
| MultiModalM
| CoalitionLogic
| GML
| PML
......
......@@ -1099,11 +1099,8 @@ else ()
(* (Materialisator: C_φ,) r_φ ⊧ ψ *)
let rec modelCheck core lfsubsumer =
let sort = coreGetSort core in
(*print_endline ((CoAlgMisc.bsetToString sort (CoAlgMisc.coreGetBs core)) ^ " |= " ^ (CoAlgFormula.exportFormula (lfGetFormula sort lfsubsumer)));*)
print_endline ((coreToString core) ^ " |= " ^ (CoAlgFormula.exportFormula (lfGetFormula sort lfsubsumer)));
try
let extension = Hashtbl.find !tboxExtensions.(sort) lfsubsumer in
print_endline ((CoAlgFormula.exportFormula (lfGetFormula sort lfsubsumer)) ^ " found in TBox extension");
Hashtbl.find extension (coreGetBs core)
with
Not_found ->
......@@ -1118,15 +1115,13 @@ let rec modelCheck core lfsubsumer =
else false
| _ ->
if (coreGetChildren core) = []
then (print_endline ("halo" ^ (coreToString core)); false)
then false
else begin
(*assert (List.length (coreGetChildren core) = 1);*)
let state = List.hd (coreGetChildren core) in
let statebs = stateGetBs state in
if bsetMem statebs lfsubsumer
then true
else begin
print_endline ("[" ^ (CoAlgMisc.bsetToString sort (CoAlgMisc.coreGetBs core)) ^ " -> " ^ (CoAlgMisc.bsetToString sort (CoAlgMisc.stateGetBs state)) ^ "] |= " ^ (CoAlgFormula.exportFormula (lfGetFormula sort lfsubsumer)));
(* conjunctive one-step consequence problem: φ ⊑1 ♡ψ ⇔ φ ∧ ¬(♡ψ) is sat *)
match lfGetNeg sort lfsubsumer with
| None ->
......@@ -1135,11 +1130,9 @@ let rec modelCheck core lfsubsumer =
bsetAdd statebs nlfsubsumer;
let state = newState sort statebs !dummy in
expandState state;
print_endline ((CoAlgMisc.bsetToString sort (CoAlgMisc.stateGetBs state)) ^ " sat?");
bsetRem statebs nlfsubsumer;
List.fold_left (fun acc (_, corelist) ->
List.fold_left (fun acc core ->
print_endline ("match: " ^ (CoAlgMisc.bsetToString sort (CoAlgMisc.coreGetBs core)));
let corebs = coreGetBs core in
bsetFold (fun lf acc ->
if isNeg sort lf
......@@ -1150,7 +1143,6 @@ let rec modelCheck core lfsubsumer =
| Some nlf -> begin
bsetRem corebs lf;
(* modality is unary *)
(*print_endline ("folding: " ^ (CoAlgMisc.bsetToString sort (CoAlgMisc.coreGetBs core)) ^ " |= " ^ (CoAlgFormula.exportFormula (lfGetFormula sort nlf)));*)
match graphFindCore sort (corebs, !dummy) with
| None ->
acc || (modelCheck core nlf)
......@@ -1178,12 +1170,8 @@ let print_extensions extension =
(* Calculate Extensions *)
let computeExtensions newExt =
assert (!tboxExtensions = newExt);
(*print_endline "=== Start TBox computation ===";
print_extensions !tboxExtensions;*)
Array.iteri (fun sort htbl ->
print_endline ("Sorte: " ^ (string_of_int sort));
Hashtbl.iter (fun var def ->
print_endline ((CoAlgFormula.exportFormula (lfGetFormula sort var)) ^ "\t:=\t" ^ (CoAlgMisc.bsetToString sort def));
let currentExtension = Hashtbl.find newExt.(sort) var in
Hashtbl.iter (fun bs boole ->
if boole
......@@ -1198,9 +1186,6 @@ let computeExtensions newExt =
) currentExtension
) htbl
) !CoAlgMisc.tboxDefs;
(*print_endline "=== End TBox computation ===";
print_extensions !tboxExtensions;
print_extensions newExt;*)
!tboxExtensions = newExt
(**
......@@ -1236,9 +1221,7 @@ let computeExtensions () =
) htbl
) !tboxExtensions;
assert (!tboxExtensions = newExt)
done;
print_endline ("=== Ready computed after " ^ (string_of_int !n) ^ " steps ===");
print_extensions !tboxExtensions
done
let isRootSat () =
match coreGetStatus (graphGetRoot ()) with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment