Commit 7bce6752 authored by Simon Prucker's avatar Simon Prucker
Browse files

nix build broken

parent 8a8efdfa
Pipeline #14698 waiting for manual action with stages
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,10 +17,13 @@ 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;
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;
......
......@@ -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 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 ";
......
......@@ -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)
......@@ -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 = 100) 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)) ))
......
......@@ -111,7 +111,9 @@ 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 a3><7 a8>p3 | (<7 a1>p7 <=> True <=> p2)"
]
let pml_testcases =
use_functor "PML" nop
......@@ -128,6 +130,31 @@ 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"
(* MULTIMODAL Tests
; 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)
......@@ -158,8 +185,10 @@ 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
; *)"Properties" >::: [prop_onestepFunc_tableau_K]
; *)"GML" >::: gml_testcases
; "Properties" >::: [prop_onestepFunc_tableau_K]
; "K onestep" >::: k_onestepFunc
; "K tableau" >::: k_onestepTab
]
;;
......
(test
(name cool_testsuite)
(modes native)
(package cool-lib)
(libraries cool-lib ounit2 cool-generators)
(action (run %{test} -output-junit-file testsuite.xml)))
......@@ -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)
......
(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)))
......@@ -9,6 +9,7 @@ buildDunePackage ({
src = ../src/generators;
buildInputs = [ ];
propagatedBuildInputs = [ qcheck cool-lib ];
# buildPhase = ''
......
{ 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";
......
......@@ -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
......@@ -120,3 +121,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)))
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