Commit eaf2e953 authored by Simon Prucker's avatar Simon Prucker
Browse files

Refactoring for merge

parent 8097da76
Pipeline #15194 failed with stages
in 58 minutes and 32 seconds
...@@ -188,6 +188,9 @@ val hc_freeIn2 : string -> hcFormula -> bool ...@@ -188,6 +188,9 @@ val hc_freeIn2 : string -> hcFormula -> bool
module HcFHt : (Hashtbl.S with type key = hcFormula) module HcFHt : (Hashtbl.S with type key = hcFormula)
(**
Parses a formula into a tree representation, where each node contains a connective. The tree structure then supports simplification and recombination of formulae.
**)
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree 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 : *)
...@@ -582,6 +582,9 @@ let oneStepSat_MultiModalK (u: bset list) sv = ...@@ -582,6 +582,9 @@ let oneStepSat_MultiModalK (u: bset list) sv =
let existsInU rel lf = List.exists (fun bs -> bsetMem bs lf) (redU (boxargsForRel rel)) in let existsInU rel lf = List.exists (fun bs -> bsetMem bs lf) (redU (boxargsForRel rel)) in
bsetForall diamonds (fun lf -> existsInU (lfGetDest3 sort lf) (lfGetDest1 sort lf)) bsetForall diamonds (fun lf -> existsInU (lfGetDest3 sort lf) (lfGetDest1 sort lf))
(**
Recursive helper function for handling One-Step satisfiability of GML formulae for one individual relation.
**)
let rec oneStepGMLRec counters sort v currentU = let rec oneStepGMLRec counters sort v currentU =
let isExceedingBox lf = (lfGetType sort lf = MaxExceptF) && ((lfGetDestNum sort lf) < (Hashtbl.find counters lf)) in let isExceedingBox lf = (lfGetType sort lf = MaxExceptF) && ((lfGetDestNum sort lf) < (Hashtbl.find counters lf)) in
if (bsetExists v isExceedingBox) if (bsetExists v isExceedingBox)
...@@ -620,6 +623,9 @@ let rec oneStepGMLRec counters sort v currentU = ...@@ -620,6 +623,9 @@ let rec oneStepGMLRec counters sort v currentU =
else false else false
end end
(**
Checks One-Step satisfaction for GML formulae by setting up counters for each relation and then recursively handling all boxes and diamonds for one relation independently.
**)
let oneStepSat_GML u sv = let oneStepSat_GML u sv =
let (sort, v) = sv in let (sort, v) = sv in
let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in
...@@ -633,7 +639,9 @@ let oneStepSat_GML u sv = ...@@ -633,7 +639,9 @@ let oneStepSat_GML u sv =
(**
Records the available sat-checking mechanisms for the individual functors, first tableau, second one-step.
**)
let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK)) let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK))
; (MultiModalKD, This mkRule_MultiModalKD) ; (MultiModalKD, This mkRule_MultiModalKD)
; (Monotone, This mkRule_Monotone) ; (Monotone, This mkRule_Monotone)
......
...@@ -18,12 +18,15 @@ val nop : unit -> unit ...@@ -18,12 +18,15 @@ val nop : unit -> unit
val except : string -> 'a -> (testResult * 'a) val except : string -> 'a -> (testResult * 'a)
val notAconj : 'a -> (testResult * 'a) val notAconj : 'a -> (testResult * 'a)
(*The onestep parameter is used to test correct sat solving using onestep reasoning*)
val use_functor : ?onestep:bool -> string -> (unit -> unit) -> (testResult * string) list -> OUnit2.test list val use_functor : ?onestep:bool -> string -> (unit -> unit) -> (testResult * string) list -> OUnit2.test list
(*The onestep parameter can be set to use onestep satisfiability instead of tableau (which is currently faster)*)
val runSatCheck : ?onestep:bool -> Cool.CoAlgMisc.sortTable -> string -> testResult val runSatCheck : ?onestep:bool -> Cool.CoAlgMisc.sortTable -> string -> testResult
val terminal_string_of_testResult : testResult -> string val terminal_string_of_testResult : testResult -> string
(**Asserts that the onestep and tableau satisfaction functions return the same result for functors, which support both (K).*)
val onestepFunc_equals_tableau: ?num_runs:int -> string -> (Cool.CoAlgFormula.formula QCheck.Gen.sized) -> Cool.CoAlgMisc.sortTable -> OUnit2.test 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 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -140,8 +140,6 @@ let pmlOrK_testcases = ...@@ -140,8 +140,6 @@ let pmlOrK_testcases =
let k_onestepFunc = let k_onestepFunc =
use_functor ~onestep: true "K" nop use_functor ~onestep: true "K" nop
[ sat "[a1]False" [ sat "[a1]False"
; unsat "[a1]False & <a2>False" ; unsat "[a1]False & <a2>False"
; sat "[a1]~p1 & <a2>p1" ; sat "[a1]~p1 & <a2>p1"
; sat "[a1]False & <a6>p1" ; sat "[a1]False & <a6>p1"
...@@ -153,7 +151,6 @@ let k_onestepFunc = ...@@ -153,7 +151,6 @@ let k_onestepFunc =
let k_onestepTab = let k_onestepTab =
use_functor "K" nop use_functor "K" nop
[ sat "[a1]False" [ sat "[a1]False"
; unsat "[a1]False & <a2>False" ; unsat "[a1]False & <a2>False"
; sat "[a1]False & <a2>True" ; sat "[a1]False & <a2>True"
; sat "[a1]False <=> <a2>True" ; sat "[a1]False <=> <a2>True"
......
...@@ -24,11 +24,18 @@ let treeParserAndSimplify_prop = ...@@ -24,11 +24,18 @@ 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) "treeParserAndSimplify" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 ( make (sized Formula_gen.formula_K)) treeParserAndSimplify_predicate)
let printAndParseInverse_predicate formula = let printAndParseInverse_predicate formula =
importFormula (string_of_formula formula) = formula importFormula (string_of_formula (importFormula (string_of_formula formula))) = importFormula (string_of_formula formula)
let printAndParseInverse_prop = let printAndParseInverse_prop =
"printAndParseInverse" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 "printAndParseInverse" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000
(make (oneof [(sized Formula_gen.formula_GML); (sized Formula_gen.formula_CL)])) printAndParseInverse_predicate) (make (oneof [sized Formula_gen.formula_GML; sized Formula_gen.formula_CL]
(*
[(sized ((fun x -> (CoolUtils.curry (Formula_gen.formula_fp x) [])) Formula_gen.gmlFormula));
(sized ((fun x -> (CoolUtils.curry (Formula_gen.formula_fp x) [])) Formula_gen.clFormula));
(sized (Formula_gen.formula_ctl Formula_gen.gmlFormula));
(sized (Formula_gen.formula_ctl Formula_gen.clFormula))]
*)
)) printAndParseInverse_predicate)
let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop; "printAndParseInverse" >: printAndParseInverse_prop ] let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop; "printAndParseInverse" >: printAndParseInverse_prop ]
......
...@@ -189,11 +189,11 @@ let check_implementation logic onestep = ...@@ -189,11 +189,11 @@ let check_implementation logic onestep =
| "ot" | "to" -> onestep | "ot" | "to" -> onestep
| "o" -> let _ = (print_endline "\nOnly onestep implementation available") in true | "o" -> let _ = (print_endline "\nOnly onestep implementation available") in true
| "t" -> let _ = (print_endline "\nOnly tableau implementation available") in false | "t" -> let _ = (print_endline "\nOnly tableau implementation available") in false
| _ -> raise (Not_Implemented (logic ^ "is not implemented!")) | _ -> raise (Not_Implemented (logic ^ " is not implemented!"))
let choiceSat opts = let choiceSat opts =
let verb = opts.verbose in let verb = opts.verbose in
let _onestep = check_implementation Sys.argv.(2) opts.onestep let onestep = check_implementation Sys.argv.(2) opts.onestep
in in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in let sorts = (FE.sortTableFromString Sys.argv.(2)) in
...@@ -215,7 +215,7 @@ let choiceSat opts = ...@@ -215,7 +215,7 @@ let choiceSat opts =
incr counter; incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
flush stdout; flush stdout;
if _onestep if onestep
then printRes (O_Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f) then printRes (O_Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
else printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f) else printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
else () else ()
......
...@@ -12,7 +12,7 @@ let anon_fun _ = print_endline usage_msg; raise (Exc "No anonymous arguments all ...@@ -12,7 +12,7 @@ let anon_fun _ = print_endline usage_msg; raise (Exc "No anonymous arguments all
let functors = ["K"; "CL"; "GML"; "Prop"] let functors = ["K"; "CL"; "GML"; "Prop"]
let matchFunctor f = let matchFunctor f =
match f with match f with
| "K" -> FG.kFormula ~unimodal: false | "K" -> FG.kFormula
| "CL" -> FG.clFormula | "CL" -> FG.clFormula
| "GML" -> FG.gmlFormula | "GML" -> FG.gmlFormula
| "Prop" -> FG.propFormula | "Prop" -> FG.propFormula
......
...@@ -28,22 +28,18 @@ let propFormula formula n = ...@@ -28,22 +28,18 @@ let propFormula formula n =
impl (formula (n/2)) (formula (n/2)) impl (formula (n/2)) (formula (n/2))
] ]
let relName = prefixNum "a" let relName = ref (prefixNum "a")
let unimod_relName = return "unimod" let set_unimodal () = relName := return "unimod"
let boxFormula ?(unimodal: bool = false) formula n = let boxFormula formula n =
if unimodal map2 (fun x y -> F.AX (x, y)) !relName (formula (n-1))
then map2 (fun x y -> F.AX (x, y)) unimod_relName (formula (n-1))
else map2 (fun x y -> F.AX (x, y)) relName (formula (n-1))
let diaFormula ?(unimodal: bool = false) formula n = let diaFormula formula n =
if unimodal map2 (fun x y -> F.EX (x, y)) !relName (formula (n-1))
then map2 (fun x y -> F.EX (x, y)) unimod_relName (formula (n-1))
else map2 (fun x y -> F.EX (x, y)) relName (formula (n-1))
let kFormula ?(unimodal: bool = false) formula n = let kFormula formula n =
if n > 0 if n > 0
then frequency [(2, propFormula formula n) ; (1, boxFormula ~unimodal: unimodal formula n); (1, diaFormula ~unimodal: unimodal formula n)] then frequency [(2, propFormula formula n) ; (1, boxFormula formula n); (1, diaFormula formula n)]
else propFormula formula n else propFormula formula n
(*generate random subset of Agent array*) (*generate random subset of Agent array*)
...@@ -62,8 +58,8 @@ let clFormula formula n = ...@@ -62,8 +58,8 @@ let clFormula formula n =
else propFormula formula n else propFormula formula n
let succs = 0 -- 10 let succs = 0 -- 10
let morethanF formula n = map3 (fun i r f -> F.MORETHAN (i, r, f)) succs relName (formula (n-1)) let morethanF formula n = map3 (fun i r f -> F.MORETHAN (i, r, f)) succs !relName (formula (n-1))
let maxexceptF formula n = map3 (fun i r f -> F.MAXEXCEPT (i, r, f)) succs relName (formula (n-1)) let maxexceptF formula n = map3 (fun i r f -> F.MAXEXCEPT (i, r, f)) succs !relName (formula (n-1))
let gmlFormula formula n = let gmlFormula formula n =
if n > 0 if n > 0
then frequency [(2, propFormula formula n); (1, morethanF formula n); (1, maxexceptF formula n)] then frequency [(2, propFormula formula n); (1, morethanF formula n); (1, maxexceptF formula n)]
...@@ -132,9 +128,9 @@ let formula_ctl baseFormula = fix (ctlFormula baseFormula) ...@@ -132,9 +128,9 @@ let formula_ctl baseFormula = fix (ctlFormula baseFormula)
(*Shrinker for formulas by parsing the formula to a tree, simplifying it stepwise and puting the versions into a list*) (*Shrinker for formulas by parsing the formula to a tree, simplifying it stepwise and puting the versions into a list*)
let pseudoShrinker formula = (*let pseudoShrinker formula =
let module T = CoolUtils.Tree in let module T = CoolUtils.Tree in
I.of_list [T.parse_back (Option.get (T.simplify (F.parseFormulaToTree formula)))] I.of_list (Option.to_list (Option.map T.parse_back (T.simplify (F.parseFormulaToTree formula))))*)
let formulaShrinker formula = let formulaShrinker 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