From b7445f7e5ccfe5f05ca2109e7f0e124950523204 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Tue, 17 Dec 2013 18:00:00 +0100
Subject: [PATCH] Add pseudo rule for MultiModalKD
The rule creator for MultiModalKD does not do anything but calling the
one of MultiModalK.
---
CoAlgLogics.ml | 51 ++++++++++++++++++++++++++++++++++++++++++++++----
CoAlgMisc.ml | 1 +
2 files changed, 48 insertions(+), 4 deletions(-)
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index fd2e1ef..2126293 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -5,8 +5,10 @@
open CoAlgMisc
+module S = MiscSolver
-let mkRule_MultiModalK sort bs sl =
+(** directly return a list of rules **)
+let mkRuleList_MultiModalK sort bs sl =
assert (List.length sl = 1);
let dep f bsl = (* dependencies for formula f *)
assert (List.length bsl = 1); (* -+ *)
@@ -52,7 +54,10 @@ let mkRule_MultiModalK sort bs sl =
| "∃R.C" ∈ bs
}
*)
- let rules = bsetFold getRules bs [] in
+ bsetFold getRules bs []
+
+let mkRule_MultiModalK sort bs sl =
+ let rules = mkRuleList_MultiModalK sort bs sl in
let res = ref (Some rules) in
fun () ->
match !res with
@@ -61,8 +66,46 @@ let mkRule_MultiModalK sort bs sl =
res := None;
AllInOne rules
+(* TODO: test it with:
+ make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
+*)
let mkRule_MultiModalKD sort bs sl =
- let rules = bsetFold getRules bs [] in
+ assert (List.length sl = 1); (* TODO: Why? *)
+ let roles = S.makeBS () in
+ (* step 1: for each ∀R._ add R *)
+ let addRoleIfBox formula =
+ if lfGetType sort formula = ExF then
+ ignore (S.addBS roles (lfGetDest3 sort formula))
+ else ()
+ in
+ bsetIter (addRoleIfBox) bs;
+ (* step 2: for each ∃R._ remove R again from roles (optimization) *)
+ let rmRoleIfDiamond formula =
+ if lfGetType sort formula = ExF then
+ S.remBS roles (lfGetDest3 sort formula)
+ else ()
+ in
+ bsetIter (rmRoleIfDiamond) bs;
+ (* step 3: for each R in roles enforce one successor *)
+ let getRules r acc = (* add the rule for a concrete R *)
+ let dep r bsl =
+ bsetIter (rmRoleIfDiamond) bs;
+ in
+ acc
+ in
+ (*
+ mkRule_MultiModalKD sort bs [s1]
+ = { (λ[bs1]. { ∀R.D ∈ bs | D ∈ bs1}
+ , [(s1, {D | "∀R.D" ∈ bs)]
+ )
+ | R ∈ signature(bs) (or R ∈ roles)
+ }
+ ∪ mkRule_MultiModalK sort bs [s1]
+ *)
+ let rules = mkRuleList_MultiModalK sort bs sl in
+ (* extend rules from K with enforcing of successors *)
+ let rules = S.foldBS getRules roles rules in
+ (* TODO: replace cannonical wrapper by helper function *)
let res = ref (Some rules) in
fun () ->
match !res with
@@ -146,7 +189,7 @@ let mkRule_Fusion sort bs sl =
"plug-in" function.
*)
let getExpandingFunctionProducer = function
- | MultiModalK -> mkRule_MultiModalK
| MultiModalK -> mkRule_MultiModalKD
+ | MultiModalKD -> mkRule_MultiModalKD
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index d856373..16fef0d 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -421,6 +421,7 @@ let tboxTable = ref (Array.make 0 S.dummyBS)
let bsetMake () = S.makeBS ()
let bsetAdd bs lf = S.addBSNoChk bs lf
let bsetMem bs lf = S.memBS bs lf
+let bsetRem bs lf = S.remBS bs lf
let bsetFold fkt bs init = S.foldBS fkt bs init
let bsetIter fkt bset = S.iterBS fkt bset
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
--
GitLab