Commit 8a8efdfa authored by Simon Prucker's avatar Simon Prucker
Browse files

Property based test for parsing and simplification of structured trees

parent e1e3dd81
Pipeline #14272 waiting for manual action with stages
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
@author Florian Widmann @author Florian Widmann
*) *)
module HC = HashConsing module HC = HashConsing
module A = AltGenlex module A = AltGenlex
module L = List module L = List
...@@ -2538,4 +2537,80 @@ module HcFHt = Hashtbl.Make( ...@@ -2538,4 +2537,80 @@ module HcFHt = Hashtbl.Make(
end end
) )
let rec parseFormulaToTree formula =
let open CoolUtils.Tree in
match formula with
| TRUE -> Leaf TRUE
| FALSE -> Leaf FALSE
| AP a -> Leaf (AP a)
| NOT f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> NOT (List.hd fList)), (getHeight child) + 1)
| AT (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AT (s, List.hd fList)), (getHeight child) + 1)
| OR (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> OR (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AND (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AND (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EQU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EQU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| IMP (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> IMP (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EX (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EX (s, List.hd fList)), (getHeight child) + 1)
| AX (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AX (s, List.hd fList)), (getHeight child) + 1)
| ENFORCES (iL, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ENFORCES (iL, List.hd fList)), (getHeight child) + 1)
| ALLOWS (iL, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ALLOWS (iL, List.hd fList)), (getHeight child) + 1)
| MIN (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MIN (i, s, List.hd fList)), (getHeight child) + 1)
| MAX (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MAX (i, s, List.hd fList)), (getHeight child) + 1)
| MORETHAN (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MORETHAN (i, s, List.hd fList)), (getHeight child) + 1)
| MAXEXCEPT (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MAXEXCEPT (i, s, List.hd fList)), (getHeight child) + 1)
| ATLEASTPROB (r, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ATLEASTPROB (r, List.hd fList)), (getHeight child) + 1)
| LESSPROBFAIL (r, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> LESSPROBFAIL (r, List.hd fList)), (getHeight child) + 1)
| CONST s -> Leaf (CONST s)
| CONSTN s -> Leaf (CONSTN s)
| ID f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ID (List.hd fList)), (getHeight child) + 1)
| NORM (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> NORM (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| NORMN (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> NORMN (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| CHC (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> CHC (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| FUS (b, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> FUS (b, List.hd fList)), (getHeight child) + 1)
| MU (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MU (s, List.hd fList)), (getHeight child) + 1)
| NU (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> NU (s, List.hd fList)), (getHeight child) + 1)
| VAR s -> Leaf (VAR s)
| AF f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AF (List.hd fList)), (getHeight child) + 1)
| EF f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EF (List.hd fList)), (getHeight child) + 1)
| AG f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AG (List.hd fList)), (getHeight child) + 1)
| EG f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EG (List.hd fList)), (getHeight child) + 1)
| AU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AR (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AR (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| ER (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> ER (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -188,4 +188,6 @@ val hc_freeIn2 : string -> hcFormula -> bool ...@@ -188,4 +188,6 @@ val hc_freeIn2 : string -> hcFormula -> bool
module HcFHt : (Hashtbl.S with type key = hcFormula) module HcFHt : (Hashtbl.S with type key = hcFormula)
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -178,6 +178,9 @@ module Tree = struct ...@@ -178,6 +178,9 @@ module Tree = struct
match aTree with match aTree with
| Leaf _ -> (expectedHeight = 0) | Leaf _ -> (expectedHeight = 0)
| Node (_, _, height) -> (height = expectedHeight) | Node (_, _, height) -> (height = expectedHeight)
let getHeight aTree = match aTree with
| Leaf _ -> 0
| Node (_, _, h) -> h
let rec simplify atree = match atree with let rec simplify atree = match atree with
| Leaf _ -> None | Leaf _ -> None
| Node (aTreeList, func, height) -> | Node (aTreeList, func, height) ->
...@@ -190,11 +193,9 @@ module Tree = struct ...@@ -190,11 +193,9 @@ module Tree = struct
match aTree with match aTree with
| Leaf a -> Leaf a | Leaf a -> Leaf a
| Node (_, _, depth) -> if (depth = maxDepth) | Node (_, _, depth) -> if (depth = maxDepth)
then then match simplify aTree with
begin | None -> aTree
foundDeepest := true; | Some aT -> (foundDeepest := true; aT)
Option.get (simplify aTree)
end
else aTree else aTree
in in
let newChildren = let newChildren =
......
...@@ -106,6 +106,7 @@ module Tree : ...@@ -106,6 +106,7 @@ module Tree :
val simplify : 'a tree -> 'a tree option val simplify : 'a tree -> 'a tree option
val parse_back : 'a tree -> 'a val parse_back : 'a tree -> 'a
val getHeight : 'a tree -> int
end end
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -88,7 +88,7 @@ let make_sorted (list:(F.formula list)) = ...@@ -88,7 +88,7 @@ let make_sorted (list:(F.formula list)) =
List.map (fun (f:F.formula) -> (0, f)) list List.map (fun (f:F.formula) -> (0, f)) list
(* Needs the formula as a sortedTable, sort set to 0 as by default. To be checked what's up with that. *) (* Needs the formula as a sortedTable, sort set to 0 as by default. To be checked what's up with that. *)
let onestepFunc_equals_tableau ?(num_runs = 50) name sized_formula_gen logic = let onestepFunc_equals_tableau ?(num_runs = 5) name sized_formula_gen logic =
"onestep func = tableau" >: to_ounit2_test ~rand: (Random.State.make_self_init ()) (Test.make ~count:num_runs ~name:name "onestep func = tableau" >: to_ounit2_test ~rand: (Random.State.make_self_init ()) (Test.make ~count:num_runs ~name:name
( make ~print:F.string_of_formula (sized sized_formula_gen)) (fun (formula) -> ( make ~print:F.string_of_formula (sized sized_formula_gen)) (fun (formula) ->
(onestepFunc_equals_tableau_predicate logic (0, formula)) )) (onestepFunc_equals_tableau_predicate logic (0, formula)) ))
......
...@@ -144,7 +144,7 @@ let k = funel_of_functor CM.MultiModalK ...@@ -144,7 +144,7 @@ let k = funel_of_functor CM.MultiModalK
let prop_onestepFunc_tableau_K = onestepFunc_equals_tableau "K Property" FG.formula_K (FE.sortTableFromFunctorExp k) let prop_onestepFunc_tableau_K = onestepFunc_equals_tableau "K Property" FG.formula_K (FE.sortTableFromFunctorExp k)
let testcases = let testcases =
[ (* "DL98" >::: dl98_testcases [ (*"DL98" >::: dl98_testcases
; "CTL" >::: ctl_fast_testcases ; "CTL" >::: ctl_fast_testcases
; "K Tableau" >::: k_testcases false ; "K Tableau" >::: k_testcases false
; "K Onestep" >::: k_testcases true ; "K Onestep" >::: k_testcases true
......
open OUnit2 open Cool
open Cool.CoAlgFormula open Cool.CoAlgFormula
open QCheck
open QCheck.Gen
open QCheck_ounit
open OUnit2
let isMuAconjunctive_test _ = let isMuAconjunctive_test _ =
let with_formula str action = action (importFormula str) str in let with_formula str action = action (importFormula str) str in
...@@ -9,6 +15,13 @@ let isMuAconjunctive_test _ = ...@@ -9,6 +15,13 @@ let isMuAconjunctive_test _ =
with_formula "μ x. μ y. ([r] x & <r> y)" (fun f f_str -> with_formula "μ x. μ y. ([r] x & <r> y)" (fun f f_str ->
assert_bool f_str (not (isMuAconjunctive f))) assert_bool f_str (not (isMuAconjunctive f)))
let tests = "CoAlgFormula" >: ("isMuAconjunctive" >:: isMuAconjunctive_test) let treeParserAndSimplify_predicate formula =
Some (CoolUtils.Tree.parse_back (CoAlgFormula.parseFormulaToTree formula)) = Some formula
let treeParserAndSimplify_prop =
"treeParserAndSimplify" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 ( make (sized Formula_gen.formula_K)) treeParserAndSimplify_predicate)
let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop]
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -2,6 +2,6 @@ ...@@ -2,6 +2,6 @@
(name cool_unit_tests) (name cool_unit_tests)
(modes native) (modes native)
(package cool-lib) (package cool-lib)
(libraries cool-lib ounit2) (libraries cool-lib ounit2 qcheck cool-generators)
(action (run %{test} -output-junit-file unit_tests.xml))) (action (run %{test} -output-junit-file unit_tests.xml)))
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