Commit 637d0f7c authored by Simon Prucker's avatar Simon Prucker
Browse files

gml and k onestep function tests

parent 196d1de9
Pipeline #13941 waiting for manual action with stages
......@@ -682,7 +682,7 @@ let obind o f = match o with
let getExpandingFunctionProducer func = oval (obind (List.assoc_opt func implementationLookup) getTableau) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step tableau based satisfiability is not implemented for " ^ string_of_functor func)))
let oneStepSatisfiability func = print_endline "\nonestep\n" ;oval (obind (List.assoc_opt func implementationLookup) getOneStepFun) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor func)))
let oneStepSatisfiability func = oval (obind (List.assoc_opt func implementationLookup) getOneStepFun) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor func)))
end
......
......@@ -10,6 +10,7 @@ module CU = CoolUtils
module PG = Paritygame
module C = CoAlgFormula
module R_com = CoAlgReasoner
module Pexc = Printexc
module Make(T : FocusTracker) = struct
module G = CoolGraph.Make(T)
......@@ -853,17 +854,11 @@ let getNextState core =
assert (okay);
Some (sort, newbs, T.finalize focus)
let newState sort bs focus =
let (func, sl) = !sortTable.(sort) in
let producer = Logics.getExpandingFunctionProducer func in
let exp = producer sort bs focus sl in
stateMake sort bs focus exp
let insertState parent sort bs focus =
let child =
match graphFindState sort (bs, focus) with
| None ->
let s = newState sort bs focus in
let s = stateMake sort bs focus (lazylistFromList []) in
graphInsertState sort (bs, focus) s;
queueInsertState s;
s
......
......@@ -34,7 +34,7 @@ let terminal_string_of_testResult tr =
let (col,str) = colored_string_of_testResult tr in
colored_string col str
let runSatCheck logic input =
let runSatCheck ?(onestep:bool = false) logic input =
try
let nomTable name =
assert (CoAlgFormula.isNominal name);
......@@ -44,7 +44,10 @@ let runSatCheck logic input =
(* isSat leaks tons of memory. Call it in new process to allow the OS to
reclaim that memory between calls. *)
match Unix.fork () with
| 0 -> let res = CRT.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox f in
| 0 -> if onestep
then let res = CRF.isSat CoAlgMisc.Auto CR.Cool G.Adaptive logic nomTable tbox f 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
if res then exit 0 else exit 1
| -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
| _ -> match Unix.wait () with
......@@ -60,10 +63,10 @@ let truncate (input : string) =
then String.sub input 0 (tlength - 3) ^ "..."
else input
let use_functor (functors: string) (init_globals: unit->unit) (cases: (testResult*string) list) =
let use_functor ?(onestep:bool = false) (functors: string) (init_globals: unit->unit) (cases: (testResult*string) list) =
let sortTable = FP.sortTableFromString functors in
List.map (fun (expected_result,formula) ->
functors >: (truncate formula >:: fun _ctxt -> let result = let _ = init_globals () in runSatCheck sortTable formula in assert_equal expected_result result)
functors >: (truncate formula >:: fun _ctxt -> let result = let _ = init_globals () in runSatCheck ~onestep: onestep sortTable formula in assert_equal expected_result result)
) cases
(* vim: set et sw=2 sts=2 ts=8 : *)
......@@ -18,9 +18,9 @@ val nop : unit -> unit
val except : string -> 'a -> (testResult * 'a)
val notAconj : 'a -> (testResult * 'a)
val use_functor : string -> (unit -> unit) -> (testResult * string) list -> OUnit2.test list
val use_functor : ?onestep:bool -> string -> (unit -> unit) -> (testResult * string) list -> OUnit2.test list
val runSatCheck : Cool.CoAlgMisc.sortTable -> string -> testResult
val runSatCheck : ?onestep:bool -> Cool.CoAlgMisc.sortTable -> string -> testResult
val terminal_string_of_testResult : testResult -> string
......
......@@ -3,8 +3,8 @@ open Testsuite
module DL98 = DL98TestCases
module CTL = CTLTestCases
let k_testcases =
use_functor "K" nop
let k_testcases onestep =
use_functor ~onestep: onestep "K" nop
[ sat "True"
; unsat "False"
; parseerror "{Fsdf"
......@@ -26,6 +26,7 @@ let k_testcases =
; sat "<r> d & <r> e & ((<r> d & <r> e) => [r] e) & (d & e => <r> ~(d&e)) |- True"
]
let aconjunctive_testcases =
use_functor "K" nop
[ (* These formulas are aconjunctive *)
......@@ -104,6 +105,10 @@ let kOrKd_testcases =
; unsat "((False) + ([r] False))"
]
let gml_testcases =
use_functor ~onestep: true "GML" nop
[ unsat "(<8>(P & ~Q)) & (<8>(Q & ~P)) & ([17](P & Q))"]
let pml_testcases =
use_functor "PML" nop
[ sat "{>= 1/3} C & {< 1/2} D"
......@@ -131,7 +136,8 @@ let ctl_fast_testcases =
let testcases =
[ "DL98" >::: dl98_testcases
; "CTL" >::: ctl_fast_testcases
; "K" >::: k_testcases
; "K Tableau" >::: k_testcases false
; "K Onestep" >::: k_testcases true
; "KD" >::: kd_testcases
; "K*K" >::: kAndK_testcases
; "K*KD" >::: kAndKd_testcases
......@@ -142,6 +148,7 @@ let testcases =
(* ; "PML" >::: pml_testcases (\* PML is currently disabled. *\) *)
(* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
; "GML" >::: gml_testcases
]
;;
......
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