Merge branch 'onestep' of git8.cs.fau.de:software/cool into onestep

default.nix

 let
   sources = import ./nix/sources.nix { };
   withStatic = p: p.overrideAttrs (o: { dontDisableStatic = true; });
+  withoutTests = p: p.override { doCheck = false; };
   nixpkgs = import sources.nixpkgs { };
   versions = import ./nix/version.nix;
   ocamline = nixpkgs.ocamlPackages.buildDunePackage {
@@ -16,13 +17,17 @@ with nixpkgs; rec {
   cool-lib = ocamlPackages.callPackage ./nix/cool-lib.nix {
     inherit versions ocamline;
     minisat = pkgs.minisat;
+    cool-generators = withoutTests cool-generators;
   };
   cool = ocamlPackages.callPackage ./nix/cool.nix {
-    inherit versions cool-lib cool-generators;
+    inherit versions;
     minisat = pkgs.minisat;
+    cool-generators = withoutTests cool-generators;
+    cool-lib = withoutTests cool-lib;
   };
   cool-generators = ocamlPackages.callPackage ./nix/cool-generators.nix {
-    inherit versions cool-lib;
+    inherit versions;
+    cool-lib = withoutTests cool-lib;
   };
   cool-static = cool.override (o: {
       doCheck = false;

dune → dune-workspace

+(lang dune 2.8)
 ;; This disables a few warnings
 ;; 6: missing label applications as they most likely are intentional
 ;; 8: unused value as somethimes code is left over or for future use

lib/src/CoAlgFormula.ml

@@ -410,18 +410,18 @@ let rec exportFormula_buffer sb f =
       Buffer.add_string sb "}";
       prio 4 f1
   | MORETHAN (n, s, f1) ->
-      Buffer.add_string sb "{>";
+      Buffer.add_string sb "<";
       Buffer.add_string sb (string_of_int n);
       Buffer.add_string sb " ";
       Buffer.add_string sb s;
-      Buffer.add_string sb "}";
+      Buffer.add_string sb ">";
       prio 4 f1
   | MAXEXCEPT (n, s, f1) ->
-      Buffer.add_string sb "{<=";
+      Buffer.add_string sb "[";
       Buffer.add_string sb (string_of_int n);
-      Buffer.add_string sb " ~ ";
+      Buffer.add_string sb " ";
       Buffer.add_string sb s;
-      Buffer.add_string sb "}";
+      Buffer.add_string sb "]";
       prio 4 f1 (* actually is prio of ~ and not of <= *)
   | ID (f1) ->
       Buffer.add_string sb "O ";

lib/src/CoAlgLogics.ml

@@ -573,92 +573,65 @@ let mkRule_Fusion sort bs focus sl : stateExpander =
 
 let oneStepSat_MultiModalK (u: bset list) sv =
   let (sort, v) = sv in
-  let boxargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = AxF)) in
-  let reducedU = List.filter (fun bs -> bsetIsSubOrEqual boxargs bs) u in
-  let diamondargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = ExF)) in
-  let existsInU lf = 
-    List.exists (fun bs -> bsetMem bs lf) reducedU in
-  let res = bsetForall diamondargs existsInU in
-  res
+  let boxes = bsetFilter v (fun lf -> (lfGetType sort lf) = AxF) in
+  let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf) = ExF) in
+  let boxargsForRel rel = bsetMap (lfGetDest1 sort) (bsetFilter boxes (fun r -> (lfGetDest3 sort r) = rel)) in
+  (*Make reduced U. Will be applied for each relation*)
+  let redU args = List.filter (fun bs -> bsetIsSubOrEqual args bs) u in
+  (*check if reducedU contains formula for every diamond per relation*)
+  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))
 
 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) 
     then false
   else
-  let filterUnsatDiamond lf = 
-     ((lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find counters lf))) in
+  let filterUnsatDiamond lf = (lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find  counters lf)) in
   let filteredV = bsetFilter v filterUnsatDiamond in
   if (bsetIsSubOrEqual filteredV (bsetMake())) then true
-  else 
-  let filterCoreLabels bset = 
+  else
+  let filterCoreLabels bset =
     bsetExists filteredV (fun lf -> bsetMem bset (lfGetDest1 sort lf)) in
   let filteredU = List.filter filterCoreLabels currentU in
-  if filteredU = [] then false
+  if filteredU = [] then false (* ensures early termination and guards the List.hd below *)
   else
-  let u = List.hd filteredU in
-  let updateCountersAdd lf = 
-    let modalArg = lfGetDest1 sort lf in
-    let newVal = (Hashtbl.find counters lf) + 1 in
-    match lfGetType sort lf with
-    | MoreThanF -> if bsetMem u modalArg then Hashtbl.add counters lf newVal
-    | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.add counters lf newVal
-    | _ -> ()
-  in
-  let updateCountersRem lf = 
-    let modalArg = lfGetDest1 sort lf in
-    match lfGetType sort lf with
-    | MoreThanF -> if bsetMem u modalArg then Hashtbl.remove counters lf
-    | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.remove counters lf
-    | _ -> ()
-  in
-  bsetIter updateCountersAdd v;
-  if ((oneStepGMLRec counters sort v filteredU)) then true
-  else begin
-    bsetIter updateCountersRem v;
-    if (oneStepGMLRec counters sort v (List.tl filteredU)) then true
-    else false
-  end
-
-let rec oneStepGMLRec2 currentA sort v u =
-  let boxLimitReached lf = 
-    let m = lfGetDestNum sort lf in
-    let arg = lfGetDest1 sort lf in
-    let countBoxes res a =
-      if not (bsetMem a arg) then res + 1 else res in
-    List.fold_left countBoxes 0 currentA > m in
-  let boxes = bsetFilter v (fun lf -> lfGetType sort lf = MaxExceptF) in
-  if (bsetExists boxes boxLimitReached) then false
-  else begin
-    let diamondNotSat lf = 
-      let m = lfGetDestNum sort lf in
-      let arg = lfGetDest1 sort lf in
-      let countDiamonds res a = 
-        if bsetMem a arg then res + 1 else res in
-      List.fold_left countDiamonds 0 currentA <= m in
-    let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf = MoreThanF) && (diamondNotSat lf)) in
-    if (bsetIsSubOrEqual diamonds (bsetMake())) then true
+    let u = List.hd filteredU in
+    let updateCountersAdd lf = 
+      let modalArg = lfGetDest1 sort lf in
+      let newVal = (Hashtbl.find counters lf) + 1 in
+      match lfGetType sort lf with
+      | MoreThanF -> if bsetMem u modalArg then Hashtbl.add counters lf newVal
+      | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.add counters lf newVal
+      | _ -> ()
+    in
+    let updateCountersRem lf = 
+      let modalArg = lfGetDest1 sort lf in
+      match lfGetType sort lf with
+      | MoreThanF -> if bsetMem u modalArg then Hashtbl.remove counters lf
+      | MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.remove counters lf
+      | _ -> ()
+    in
+    bsetIter updateCountersAdd v;
+    if ((oneStepGMLRec counters sort v filteredU)) then true
     else begin
-      let filterCoreLabels bset = 
-        bsetExists diamonds (fun lf -> (lfGetType sort lf = MoreThanF) && (bsetMem bset (lfGetDest1 sort lf))) in
-      let filteredU = List.filter filterCoreLabels u in 
-      if filteredU = [] then false
-      else begin
-        let aToAdd = List.hd filteredU in
-        let remainingU = List.tl filteredU in
-        (oneStepGMLRec2 currentA sort v remainingU) || (oneStepGMLRec2 (aToAdd::currentA) sort v filteredU)
-      end
+      bsetIter updateCountersRem v;
+      if (oneStepGMLRec counters sort v (List.tl filteredU)) then true
+      else false
     end
-  end
-  
-
 
 let oneStepSat_GML u sv =
   let (sort, v) = sv in
-  let counters = Hashtbl.create (bsetLen v) in
-  bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
-  oneStepGMLRec counters sort v u
+  let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in
+  let reled_v = List.map (fun rel -> (rel, bsetFilter v (fun lf -> lfGetDest3 sort lf = rel))) rels in
+  List.for_all (fun (_rel, sub_v) ->
+      let counters = Hashtbl.create (bsetLen sub_v) in
+      bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
+      oneStepGMLRec counters sort sub_v u
+    ) reled_v
+
+                    
+  
 
 
 let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK))

lib/tests/testsuite/Testsuite.ml

@@ -2,10 +2,11 @@
 open Cool
 open OUnit2
 open QCheck
-open QCheck.Gen
+(*open QCheck.Gen*)
 open QCheck_ounit
 module F = CoAlgFormula
 module FP = FunctorParsing
+module FG = Formula_gen
 module G = CoolGraph
 module CR = CoAlgReasoner
 module CRT = CoAlgReasonerOneStepTableau.Make(FocusTracking.PartialPermutationTracker)
@@ -76,7 +77,7 @@ let truncate (input : string) =
 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 ~onestep: onestep 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 ~printer:terminal_string_of_testResult expected_result result)
     ) cases
 
 let onestepFunc_equals_tableau_predicate logic formula =
@@ -88,9 +89,9 @@ 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 = 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
-    ( make ~print:F.string_of_formula  (sized sized_formula_gen))  (fun (formula) ->
+let onestepFunc_equals_tableau ?(num_runs = 1000) name sized_formula_gen logic =
+  "onestep func = tableau" >: to_ounit2_test ~rand: (Random.State.make_self_init ()) (Test.make ~count:num_runs ~name:name ~max_fail:1 
+    ( make ~print:F.string_of_formula ~shrink:QCheck.Shrink.nil (sized_formula_gen 2))  (fun (formula) ->
       (onestepFunc_equals_tableau_predicate logic (0, formula)) ))
 
 

lib/tests/testsuite/cool_testsuite.ml

@@ -11,8 +11,8 @@ let k_testcases onestep =
   use_functor ~onestep: onestep "K" nop
     [ sat        "True"
     ; unsat      "False"
-    ; parseerror "{Fsdf"
-    (*; parseerror  "Fsdf}" *)
+    (*; parseerror "{Fsdf"
+    ; parseerror  "Fsdf}" *)
     ; unsat      "<r> True & [r] False"
     ; unsat      "c |- <r> ~c"
     ; sat        "c |- [r] ~c"
@@ -20,6 +20,8 @@ let k_testcases onestep =
     ; unsat      "<x> (<s> False) | <r> ((<r> c) & (<s> False))"
     ; unsat      "<x> (<s> False) | <r> ((<r> c) & (<s> False))"
     ; sat        "<r> a & <r> b |- [r] c"
+    ; sat        "< > a & < > b |- [ ] c"
+    ; sat        "<r> a <=> [r]b"
     ; unsat      "<r> a & <r> b |- [r] (~a & ~b)"
     ; unsat      "<r> a & <r> b |- [r] ~b"
     ; sat        "<r> a & <r> ~a |- [r] b"
@@ -56,8 +58,8 @@ let kd_testcases =
   use_functor "KD" nop
     [ sat       "True"
     ; unsat      "False"
-    ; parseerror "{Fsdf"
-    (*; parseerror "Fsdf}" *)
+    (*; parseerror "{Fsdf"
+    ; parseerror "Fsdf}" *)
     ; unsat      "<r> True & [r] False"
     ; unsat      "C |- <r> ~C"
     ; unsat      "C |- [r] ~C"
@@ -111,7 +113,12 @@ let kOrKd_testcases =
 
 let gml_testcases =
   use_functor ~onestep: true "GML" nop
-    [ unsat "(<8>(P & ~Q)) & (<8>(Q & ~P)) & ([17](P & Q))"]
+    [ unsat "(<8>(P & ~Q)) & (<8>(Q & ~P)) & ([17](P & Q))"
+    ; sat   "<9 a1><7 a1>p3 | (<7 a1>p7 <=> True <=> p2)"
+    ; unsat "<10 a1>([8 a1]True | [7 a1]p8 <=> [0 a1]p3 & ~True)"
+    ; unsat "<3 a1>~p & [0 a1]p"
+    ; sat   "<3 a1>~p & [0 a2]p"
+    ]
 
 let pml_testcases =
   use_functor "PML" nop
@@ -128,6 +135,30 @@ let pmlOrK_testcases =
     ; sat "({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
     ]
 
+let k_onestepFunc =
+  use_functor ~onestep: true "K" nop
+    [ sat   "[a1]False"
+
+    
+    ; unsat "[a1]False & <a2>False"
+    ; sat   "[a1]~p1 & <a2>p1"
+    ; sat   "[a1]False & <a6>p1"
+    ; sat   "[a1]False & <a2>True"
+    ; sat   "[a1]False <=> <a2>True" 
+    ; sat   "[a5]False <=> <a70>True"
+    ]
+
+let k_onestepTab =
+  use_functor "K" nop
+    [ sat   "[a1]False"
+    
+    ; unsat "[a1]False & <a2>False"
+    ; sat   "[a1]False & <a2>True"
+    ; sat   "[a1]False <=> <a2>True"
+    ; sat   "[a1]~p1 & <a2>p1"
+    ; sat   "[a5]False <=> <a70>True"
+    ]
+
 let dl98_testcases =
   use_functor "K" nop (DL98.satCasesList @ DL98.unsatCasesList)
 
@@ -144,7 +175,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 testcases =
-  [  (*"DL98" >::: dl98_testcases
+  [  "DL98" >::: dl98_testcases
   ; "CTL" >::: ctl_fast_testcases
   ; "K Tableau" >::: k_testcases false
   ; "K Onestep" >::: k_testcases true
@@ -155,11 +186,11 @@ let testcases =
    (*;"Nominals" >::: nominal_testcases*)
   ; "CL" >::: cl_testcases
   ; "CL" >::: cl_testcases_2agents
-  (* ; "PML" >::: pml_testcases (\* PML is currently disabled. *\) *)
-  (* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
+  (* ; "PML" >::: pml_testcases (\* PML is currently disabled. *\)
+   ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. *\) *)
   ; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
   ; "GML" >::: gml_testcases
-  ; *)"Properties" >::: [prop_onestepFunc_tableau_K]
+  ; "Properties" >::: [prop_onestepFunc_tableau_K]
   ]
 ;;
 

lib/tests/testsuite/dune

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

lib/tests/unit_tests/CoAlgFormula_tests.ml

@@ -16,7 +16,9 @@ let isMuAconjunctive_test _ =
    assert_bool f_str (not (isMuAconjunctive f)))
 
 let treeParserAndSimplify_predicate formula =
-  Some (CoolUtils.Tree.parse_back (CoAlgFormula.parseFormulaToTree formula)) = Some formula
+  let module T = CoolUtils.Tree in
+  let tree = CoAlgFormula.parseFormulaToTree formula in
+  (Some (T.parse_back tree) = Some formula) && (T.simplify tree != Some tree)
 
 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)

lib/tests/unit_tests/dune

 (test
  (name cool_unit_tests)
  (modes native)
- (package cool-lib)
+ (allow_overlapping_dependencies)
  (libraries cool-lib ounit2 qcheck cool-generators)
  (action (run %{test} -output-junit-file unit_tests.xml)))
 

nix/cool-generators.nix

@@ -9,6 +9,7 @@ buildDunePackage ({
 
   src = ../src/generators;
 
+  buildInputs = [ ];
   propagatedBuildInputs = [ qcheck cool-lib ];
 
   # buildPhase = ''

nix/cool-lib.nix

-{ lib, buildDunePackage, ounit, ocamlgraph, fetchgit, pgsolver, glibc, zlib, minisat, ocamline, profile ? null, versions, doCheck ? true }:
+{ lib, buildDunePackage, qcheck, ounit, cool-generators, ocamlgraph, fetchgit, pgsolver, glibc, zlib, minisat, ocamline, profile ? null, versions, doCheck ? true }:
 
 buildDunePackage ({
   pname = "cool-lib";
@@ -18,7 +18,7 @@ buildDunePackage ({
   #   runHook postBuild
   # '';
 
-  checkInputs = [ ounit ];
+  checkInputs = [ ounit qcheck cool-generators ];
 
   OUNIT_CI = "true";
 

src/exes/gen_exec/Gen_exec.ml

@@ -12,7 +12,7 @@ let anon_fun _ = print_endline usage_msg; raise (Exc "No anonymous arguments all
 let functors = ["K"; "CL"; "GML"; "Prop"]
 let matchFunctor f = 
   match f with
-  | "K" -> FG.kFormula
+  | "K" -> FG.kFormula ~unimodal: false
   | "CL" -> FG.clFormula
   | "GML" -> FG.gmlFormula
   | "Prop" -> FG.propFormula
@@ -24,7 +24,7 @@ let matchFixpoint f =
   | "Mu" -> (fun x -> (U.curry (FG.formula_fp x) []))
   | "CTL" -> FG.formula_ctl
   | _ -> fix
-let logic = ref FG.kFormula
+let logic = ref (FG.kFormula ~unimodal: false)
 let amount = ref 1
 let size = ref 5
 let fp = ref fix

src/generators/Formula_gen.ml

@@ -5,6 +5,7 @@ module F = CoAlgFormula
 module U = CoolUtils
 
 open QCheck.Gen
+module I = QCheck.Iter
 
 let prefixNum prefix = map (fun x -> prefix ^ string_of_int x) small_nat
 
@@ -28,13 +29,21 @@ let propFormula formula n =
          ]
 
 let relName = prefixNum "a"
-
-let boxFormula formula n = map2 (fun x y -> F.AX (x, y)) relName (formula (n-1))
-let diaFormula formula n = map2 (fun x y -> F.EX (x, y)) relName (formula (n-1))
-
-let kFormula formula n =
+let unimod_relName = return "unimod"
+
+let boxFormula ?(unimodal: bool = false) formula n = 
+  if unimodal
+    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 = 
+  if unimodal
+    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 =
   if n > 0
-  then frequency [(2, propFormula formula n) ; (1, boxFormula formula n); (1, diaFormula formula n)]
+  then frequency [(2, propFormula formula n) ; (1, boxFormula ~unimodal: unimodal formula n); (1, diaFormula ~unimodal: unimodal formula n)]
   else propFormula formula n
 
 (*generate random subset of Agent array*)
@@ -120,3 +129,19 @@ let ctlFormula baseFormula formula depth =
                 (1, ebFormula formula (depth-1));
                 (10, baseFormula formula (depth-1))]
 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*)
+
+let pseudoShrinker formula =
+  let module T = CoolUtils.Tree in
+  I.of_list [T.parse_back (Option.get (T.simplify (F.parseFormulaToTree formula)))]
+
+
+let formulaShrinker formula =
+  let module T = CoolUtils.Tree in
+  let rec fTreeShrinker fTreeOption = 
+    match fTreeOption with
+      | None -> []
+      | Some fTree -> print_endline "Shrink"; fTree:: (fTreeShrinker (T.simplify fTree))  
+  in I.of_list (fTreeShrinker (Some (F.parseFormulaToTree formula)))
+