From dbcce6121a9d72ca2974e6f7a73e27ceab5fde7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Mon, 5 May 2014 13:16:29 +0200
Subject: [PATCH] Implement fuzzy formula conversion to K or GML
---
src/lib/CoAlgFormula.ml | 68 ++++++++++++++++++++++++++++++++++++++++
src/lib/CoAlgFormula.mli | 11 +++++--
2 files changed, 77 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 3e5c6e1..8bcaef8 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -16,6 +16,9 @@ module Str = String
*)
exception CoAlgException of string
+exception ConversionException
+
+
(** Indicates the sort of a sorted formula
*)
type sort = int
@@ -90,6 +93,71 @@ let rec sizeFormula f =
let sizeSortedFormula f = sizeFormula (snd f)
+let rec iter func formula =
+ func formula;
+ let proc = iter func in (* proc = "process" *)
+ match formula with
+ | TRUE | FALSE | AP _ -> ()
+ | NOT a | AT (_,a)
+ | EX (_,a) | AX (_,a) -> proc a
+ | OR (a,b) | AND (a,b)
+ | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
+ | ENFORCES (_,a) | ALLOWS (_,a)
+ | MIN (_,_,a) | MAX (_,_,a)
+ | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
+ | CHC (a,b) | CHCN (a,b) -> (proc a ; proc b)
+ | FUS (_,a) -> proc a
+
+let rec convert_post func formula = (* run over all subformulas in post order *)
+ let c = convert_post func in (* some shorthand *)
+ (* replace parts of the formula *)
+ let formula = (match formula with
+ (* 0-ary constructors *)
+ | TRUE | FALSE | AP _ -> formula
+ (* unary *)
+ | NOT a -> NOT (c a)
+ | AT (s,a) -> AT (s,c a)
+ (* binary *)
+ | OR (a,b) -> OR (c a, c b)
+ | AND (a,b) -> AND (c a, c b)
+ | EQU (a,b) -> EQU (c a, c b)
+ | IMP (a,b) -> IMP (c a, c b)
+ | EX (s,a) -> EX (s,c a)
+ | AX (s,a) -> AX (s,c a)
+ | ENFORCES (s,a) -> ENFORCES (s,c a)
+ | ALLOWS (s,a) -> ALLOWS (s,c a)
+ | MIN (n,s,a) -> MIN (n,s,c a)
+ | MAX (n,s,a) -> MAX (n,s,c a)
+ | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
+ | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
+ | CHC (a,b) -> CHC (c a, c b)
+ | CHCN (a,b) -> CHCN (c a, c b)
+ | FUS (s,a) -> FUS (s, c a)) in
+ func formula
+
+let convertToK formula = (* tries to convert a formula to a pure K formula *)
+ let helper formula = match formula with
+ | ENFORCES _ | ALLOWS _ -> raise ConversionException
+ | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
+ | MAX (0,s,a) -> AX (s, NOT a)
+ | MAXEXCEPT (0,s,a) -> AX (s, a)
+ | AX _ | EX _
+ | CHC _ | CHCN _ | FUS _ -> formula
+ | _ -> raise ConversionException
+ in
+ convert_post helper formula
+
+let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
+ let helper formula = match formula with
+ | ENFORCES _ | ALLOWS _ -> raise ConversionException
+ | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
+ | CHC _ | CHCN _ | FUS _ -> formula
+ | AX (r,a) -> MAXEXCEPT (0,r,a)
+ | EX (r,a) -> MORETHAN (0,r,a)
+ | _ -> raise ConversionException
+ in
+ convert_post helper formula
+
(** Appends a string representation of a formula to a string buffer.
Parentheses are ommited where possible
where the preference rules are defined as usual.
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 308e8b9..87a6c6c 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -6,6 +6,8 @@
exception CoAlgException of string
+exception ConversionException
+
type sort = int
type formula =
@@ -25,13 +27,18 @@ type formula =
| MIN of int * string * formula (* some more intuitive diamond for GML *)
| MAX of int * string * formula (* some more intuitive box for GML *)
| MORETHAN of int * string * formula (* diamond of GML *)
- | MAXEXCEPT of int * string * formula (* box of GML *)
+ | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
type sortedFormula = sort * formula
+val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *)
+val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *)
+val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *)
+val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *)
+
val isNominal : string -> bool
val sizeFormula : formula -> int
@@ -82,7 +89,7 @@ val is_min : formula -> bool
val is_max : formula -> bool
val is_choice : formula -> bool
val is_fusion : formula -> bool
-
+
val const_true : formula
val const_false : formula
val const_ap : string -> formula
--
GitLab