Property based test for K if onestepFunc equals tableau (with a slight type error)

lib/src/FunctorParsing.ml

@@ -101,7 +101,6 @@ let functorExpFromString str : functorExp =
     | None -> ();
     result
 
-
 let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable =
     let logicName2Functor str params = match (CM.unaryfunctor_of_string str params) with
     | Some x -> x

lib/tests/testsuite/Testsuite.ml

 
 open Cool
 open OUnit2
+open QCheck
+open QCheck_ounit
+module F = CoAlgFormula
 module FP = FunctorParsing
 module G = CoolGraph
 module CR = CoAlgReasoner
@@ -34,20 +37,14 @@ let terminal_string_of_testResult tr =
     let (col,str) = colored_string_of_testResult tr in
     colored_string col str
 
-let runSatCheck ?(onestep:bool = false) logic input =
+
+let run_check_in_new_process ?(onestep:bool = false) nomTable logic tbox formula = 
   try
-      let nomTable name =
-        assert (CoAlgFormula.isNominal name);
-        Some 0
-      in
-      let (tbox, f) = CoAlgFormula.importQuery input in
-      (* isSat leaks tons of memory. Call it in new process to allow the OS to
-         reclaim that memory between calls. *)
-      match Unix.fork () with
+    match Unix.fork () with
       | 0 -> if onestep
-              then  let res = CRF.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox f in
+              then  let res = CRF.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox formula in
                       if res then exit 0 else exit 1
-              else  let res = CRT.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox f in
+              else  let res = CRT.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox formula in
                       if res then exit 0 else exit 1
       | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
       | _ -> match Unix.wait () with
@@ -57,6 +54,18 @@ let runSatCheck ?(onestep:bool = false) logic input =
   with | Stream.Error _ -> ParseError
        | CoAlgFormula.CoAlgException s -> Exception s
 
+
+let runSatCheck ?(onestep:bool = false) logic input =
+      let nomTable name =
+        assert (CoAlgFormula.isNominal name);
+        Some 0
+      in
+      let (tbox, f) = CoAlgFormula.importQuery input in
+      (* isSat leaks tons of memory. Call it in new process to allow the OS to
+         reclaim that memory between calls. 
+         => But even better: Fix the leaks*)
+      run_check_in_new_process ~onestep:onestep nomTable logic tbox f
+
 let truncate (input : string) =
   let tlength = 80 in
   if tlength < String.length input
@@ -69,4 +78,17 @@ let use_functor ?(onestep:bool = false) (functors: string) (init_globals: unit->
       functors >: (truncate formula >:: fun _ctxt -> let result = let _ = init_globals () in runSatCheck ~onestep: onestep sortTable formula in assert_equal expected_result result)
     ) cases
 
+let onestepFunc_equals_tableau_predicate logic formula =
+  let nom = (fun _ -> Some 0) in
+  (run_check_in_new_process ~onestep: true nom logic [] formula = run_check_in_new_process ~onestep: false nom logic [] formula)
+
+let make_sorted (list:(F.formula list)) =
+  List.map (fun (f:F.formula) -> (0, f)) list
+
+let onestepFunc_equals_tableau ?(num_runs = 10) name sized_formula_gen logic =
+  "onestep func = tableau" >: to_ounit2_test (Test.make ~count:num_runs ~name:name
+    (list_of_size (num_runs -- num_runs).gen @@ make ~print:F.string_of_formula  (QCheck.Gen.sized sized_formula_gen))  (fun (formulas) ->
+      List.for_all (onestepFunc_equals_tableau_predicate logic ) (make_sorted formulas)))
+
+
 (* vim: set et sw=2 sts=2 ts=8 : *)

lib/tests/testsuite/Testsuite.mli

@@ -24,4 +24,6 @@ val runSatCheck : ?onestep:bool -> Cool.CoAlgMisc.sortTable -> string -> testRes
 
 val terminal_string_of_testResult : testResult -> string
 
+val onestepFunc_equals_tableau: ?num_runs:int -> string -> (Cool.CoAlgFormula.formula QCheck.Gen.sized) -> Cool.CoAlgMisc.sortTable -> OUnit2.test
+
 (* vim: set et sw=2 sts=2 ts=8 : *)

lib/tests/testsuite/cool_testsuite.ml

+open Cool
 open OUnit2
 open Testsuite
 module DL98 = DL98TestCases
 module CTL = CTLTestCases
+module FE = FunctorParsing
+module CM = CoAlgMisc
+module FG = Formula_gen
 
 let k_testcases onestep =
   use_functor ~onestep: onestep "K" nop
@@ -133,6 +137,12 @@ let ctl_slow_testcases =        (* include the fast tests as well *)
 let ctl_fast_testcases =
   use_functor "KD" nop CTL.fastTests
 
+
+let funel_of_functor f = FE.Unary [CM.string_of_functor f]
+let k = funel_of_functor CM.MultiModalK
+  
+let prop_onestepFunc_tableau_K = onestepFunc_equals_tableau "K" FG.formula_K k
+
 let testcases =
   [ "DL98" >::: dl98_testcases
   ; "CTL" >::: ctl_fast_testcases
@@ -149,6 +159,7 @@ let testcases =
   (* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
   ; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
   ; "GML" >::: gml_testcases
+  ; "K_onestepFunc_tableau" >::: prop_onestepFunc_tableau_K
   ]
 ;;
 

lib/tests/testsuite/dune

@@ -2,5 +2,5 @@
  (name cool_testsuite)
  (modes native)
  (package cool-lib)
- (libraries cool-lib ounit2)
+ (libraries cool-lib ounit2 cool-generators)
  (action (run %{test} -output-junit-file testsuite.xml)))