Commit dbcce612 authored by Thorsten Wißmann's avatar Thorsten Wißmann
Browse files

Implement fuzzy formula conversion to K or GML

parent 0247525c
......@@ -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.
......
......@@ -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
......
Supports Markdown
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