Commit 3b371362 authored by Simon Prucker's avatar Simon Prucker
Browse files

nix build fixed, unimodal gml tests, adjusted printer for GML

parent 7bce6752
Pipeline #14700 waiting for manual action with stages
......@@ -20,13 +20,14 @@ with nixpkgs; rec {
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;
......
......@@ -419,7 +419,7 @@ let rec exportFormula_buffer sb f =
| MAXEXCEPT (n, s, f1) ->
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 "]";
prio 4 f1 (* actually is prio of ~ and not of <= *)
......
......@@ -112,7 +112,9 @@ let kOrKd_testcases =
let gml_testcases =
use_functor ~onestep: true "GML" nop
[ unsat "(<8>(P & ~Q)) & (<8>(Q & ~P)) & ([17](P & Q))"
; sat "<9 a3><7 a8>p3 | (<7 a1>p7 <=> True <=> p2)"
; 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"
]
let pml_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