Commit 52797e16 authored by Simon Prucker's avatar Simon Prucker
Browse files

Random seed not working

parent caa394c6
Pipeline #13949 waiting for manual action with stages
......@@ -2,6 +2,7 @@
open Cool
open OUnit2
open QCheck
open QCheck.Gen
open QCheck_ounit
module F = CoAlgFormula
module FP = FunctorParsing
......@@ -80,15 +81,17 @@ let use_functor ?(onestep:bool = false) (functors: string) (init_globals: unit->
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)
(CRF.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nom [] formula =
CRT.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nom [] formula)
let make_sorted (list:(F.formula 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. *)
let onestepFunc_equals_tableau ?(num_runs = 10) name sized_formula_gen logic =
let onestepFunc_equals_tableau ?(num_runs = 18) 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)))
( make ~print:F.string_of_formula (sized sized_formula_gen)) (fun (formula) ->
(onestepFunc_equals_tableau_predicate logic (0, formula)) ))
(* vim: set et sw=2 sts=2 ts=8 : *)
......@@ -141,10 +141,10 @@ let ctl_fast_testcases =
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 !CM.sortTable
let prop_onestepFunc_tableau_K = onestepFunc_equals_tableau "K Property" FG.formula_K (FE.sortTableFromFunctorExp k)
let testcases =
[(* "DL98" >::: dl98_testcases
[ (* "DL98" >::: dl98_testcases
; "CTL" >::: ctl_fast_testcases
; "K Tableau" >::: k_testcases false
; "K Onestep" >::: k_testcases true
......@@ -159,7 +159,7 @@ let testcases =
(* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
; "GML" >::: gml_testcases
; *)prop_onestepFunc_tableau_K
; *)"Properties" >::: [prop_onestepFunc_tableau_K]
]
;;
......
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