Unverified Commit 07e699ea authored by Merlin's avatar Merlin 💧
Browse files

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

parents 21904a3f bf8f44d8
Pipeline #17712 waiting for manual action with stages
in 2 minutes and 24 seconds
......@@ -6,7 +6,8 @@ let
nix-bundle = import sources.nix-bundle { inherit nixpkgs; };
licenseReport = drv : (import "${sources.bundlers}/report" { inherit drv; pkgs = nixpkgs; }).runtimeReport;
versions = import ./nix/version.nix;
fact-wrapper = nixpkgs.callPackage ./nix/fact-wrapper.nix { };
factplusplus = nixpkgs.callPackage ./nix/fact++.nix {}; #should be removes once merged into upsatream
fact-wrapper = nixpkgs.callPackage ./nix/fact-wrapper.nix { inherit factplusplus; };
cool-benchmark-scripts = nixpkgs.stdenv.mkDerivation {
name = "cool-benchmark-scripts";
src = ./benchmarks;
......
......@@ -1740,6 +1740,55 @@ let const_big_and formulas = match formulas with
| [] -> TRUE
| h :: tl -> List.fold_left const_and h tl
module type MasterMod = sig
type arg
val master_ax : arg -> formula -> formula
val master_ex : arg -> formula -> formula
end
module CLMaster = struct
type arg = int list
let master_ax coal f = ENFORCES (coal, f)
let master_ex coal f = ALLOWS (coal, f)
end
module KMaster = struct
type arg = string
let master_ax rel f = AX (rel, f)
let master_ex rel f = EX (rel, f)
end
module type TLSyntax = sig
include MasterMod
val au : arg -> formula -> formula -> formula
val ar : arg -> formula -> formula -> formula
val ab : arg -> formula -> formula -> formula
val af : arg -> formula -> formula
val ag : arg -> formula -> formula
val eu : arg -> formula -> formula -> formula
val er : arg -> formula -> formula -> formula
val eb : arg -> formula -> formula -> formula
val ef : arg -> formula -> formula
val eg : arg -> formula -> formula
end
module MakeTLSyntax (MM : MasterMod) = struct
include MM
let name = "#tlfp#"
let au arg f1 f2 = MU (name, (OR (f2, (AND (f1, (MM.master_ax arg (VAR name)))))))
let ar arg f1 f2 = NU (name, (AND (f2, (OR (f1, (MM.master_ax arg (VAR name)))))))
let ab arg f1 f2 = NOT (MU (name, (OR (f2, (AND ((NOT f1), (MM.master_ex arg (VAR name))))))))
let af arg f1 = MU (name, (OR (f1, (MM.master_ax arg (VAR name)))))
let ag arg f1 = NU (name, (AND (f1, (MM.master_ax arg (VAR name)))))
let eu arg f1 f2 = MU (name, (OR (f2, (AND (f1, (MM.master_ex arg (VAR name)))))))
let er arg f1 f2 = NU (name, (AND (f2, (OR (f1, (MM.master_ex arg (VAR name)))))))
let eb arg f1 f2 = NOT (MU (name, (OR (f2, (AND ((NOT f1), (MM.master_ax arg (VAR name))))))))
let ef arg f1 = MU (name, (OR (f1, (MM.master_ex arg (VAR name)))))
let eg arg f1 = NU (name, (AND (f1, (MM.master_ex arg (VAR name)))))
end
module ATLSyntax = MakeTLSyntax(CLMaster)
module CTLSyntax = MakeTLSyntax(KMaster)
(** Hash-consed formulae, which are in negation normal form,
such that structural and physical equality coincide.
......@@ -2384,29 +2433,18 @@ let checkClosed f = match freeVariables f with
| frees -> raise (CoAlgException (Printf.sprintf "%s is not closed because the variables '%s' occur freely" (string_of_formula f) (List.fold_right (fun el accu -> el ^ " " ^ accu) (List.tl frees) (List.hd frees))))
let convertToMu formula =
let name = Stream.next gensym in
let helper formula =
match formula with
| AF f1 ->
MU (name, (OR (f1, (const_ax (VAR name)))))
| EF f1 ->
MU (name, (OR (f1, (const_ex (VAR name)))))
| AG f1 ->
NU (name, (AND (f1, (const_ax (VAR name)))))
| EG f1 ->
NU (name, (AND (f1, (const_ex (VAR name)))))
| AU (f1, f2) ->
MU (name, (OR (f2, (AND (f1, (const_ax (VAR name)))))))
| EU (f1, f2) ->
MU (name, (OR (f2, (AND (f1, (const_ex (VAR name)))))))
| AR (f1, f2) ->
NU (name, (AND (f2, (OR (f1, (const_ex (VAR name)))))))
| ER (f1, f2) ->
NU (name, (AND (f2, (OR (f1, (const_ex (VAR name)))))))
| AB (f1, f2) ->
NOT (MU (name, (OR (f2, (AND ((NOT f1), (const_ex (VAR name))))))))
| EB (f1, f2) ->
NOT (MU (name, (OR (f2, (AND ((NOT f1), (const_ax (VAR name))))))))
| AF f1 -> CTLSyntax.af default_relation f1
| EF f1 -> CTLSyntax.ef default_relation f1
| AG f1 -> CTLSyntax.ag default_relation f1
| EG f1 -> CTLSyntax.eg default_relation f1
| AU (f1, f2) -> CTLSyntax.au default_relation f1 f2
| EU (f1, f2) -> CTLSyntax.eu default_relation f1 f2
| AR (f1, f2) -> CTLSyntax.ar default_relation f1 f2
| ER (f1, f2) -> CTLSyntax.er default_relation f1 f2
| AB (f1, f2) -> CTLSyntax.ab default_relation f1 f2
| EB (f1, f2) -> CTLSyntax.eb default_relation f1 f2
| _ -> formula
in
convert_post helper formula
......
......@@ -168,6 +168,32 @@ val const_maxexcept : int -> ?rel:string -> formula -> formula
val const_big_or : formula list -> formula
val const_big_and : formula list -> formula
module type MasterMod = sig
type arg
val master_ax : arg -> formula -> formula
val master_ex : arg -> formula -> formula
end
module type TLSyntax = sig
include MasterMod
val au : arg -> formula -> formula -> formula
val ar : arg -> formula -> formula -> formula
val ab : arg -> formula -> formula -> formula
val af : arg -> formula -> formula
val ag : arg -> formula -> formula
val eu : arg -> formula -> formula -> formula
val er : arg -> formula -> formula -> formula
val eb : arg -> formula -> formula -> formula
val ef : arg -> formula -> formula
val eg : arg -> formula -> formula
end
module MakeTLSyntax (MM : MasterMod) : TLSyntax with type arg = MM.arg
module ATLSyntax : TLSyntax with type arg = int list
module CTLSyntax : TLSyntax with type arg = string
type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
and hcFormula_node =
| HCTRUE
......
......@@ -49,6 +49,9 @@ rule lex = parse
| "EX" {FormulaParser.EX}
| 'E' {FormulaParser.E}
| 'A' {FormulaParser.A}
| 'F' {FormulaParser.F}
| 'X' {FormulaParser.X}
| 'G' {FormulaParser.G}
| 'B' {FormulaParser.B}
| 'U' {FormulaParser.U}
| 'R' {FormulaParser.R}
......
......@@ -18,7 +18,7 @@
%token EF AF
%token EG AG
%token EX AX
%token E A
%token E A F X G
%token B U R
%token O
%token MY NY
......@@ -121,6 +121,7 @@ fmla:
| f = modality a = fmla {f a}
| Not a = fmla {fun ctx -> CoAlgFormula.NOT (a ctx)}
| a = ctlSplitFormula {a}
| a = atlFormula {a}
| a = Identifyer {fun ctx -> if (List.mem a ctx) then CoAlgFormula.VAR a else CoAlgFormula.AP a}
| True {fun _ -> CoAlgFormula.TRUE}
| False {fun _ -> CoAlgFormula.FALSE}
......@@ -148,5 +149,41 @@ fmla:
}
;
%inline atlPathQuant:
| c = dia(dia(curlied(Nat0*))) { (`a, c) }
| c = box(box(curlied(Nat0*))) { (`e, c) }
;
%inline atlFormula:
| p = atlPathQuant pf = ctlPathFmla { fun ctx ->
let open CoAlgFormula.ATLSyntax in
match p, pf ctx with
| (`a, c),(x, `u, y) -> au c x y
| (`a, c),(x, `r, y) -> ar c x y
| (`a, c),(x, `b, y) -> ab c x y
| (`e, c),(x, `u, y) -> eu c x y
| (`e, c),(x, `r, y) -> er c x y
| (`e, c),(x, `b, y) -> eb c x y
}
| p = atlPathQuant X f = fmla { fun ctx ->
let open CoAlgFormula.ATLSyntax in
match p with
| (`a, c) -> master_ax c (f ctx)
| (`e, c) -> master_ex c (f ctx)
}
| p = atlPathQuant F f = fmla { fun ctx ->
let open CoAlgFormula.ATLSyntax in
match p with
| (`a, c) -> af c (f ctx)
| (`e, c) -> ef c (f ctx)
}
| p = atlPathQuant G f = fmla { fun ctx ->
let open CoAlgFormula.ATLSyntax in
match p with
| (`a, c) -> ag c (f ctx)
| (`e, c) -> eg c (f ctx)
}
%%
{ stdenv, lib, fetchFromBitbucket, cmake, jdk }:
stdenv.mkDerivation rec {
pname = "factplusplus";
version = "1.6.5";
name = "${pname}-${version}";
src = fetchFromBitbucket {
owner = "dtsarkov";
repo = "factplusplus";
rev = "Release-${version}";
sha256 = "wzK1QJsNN0Q73NM+vjaE/vLuGf8J1Zu5ZPAkZNiKnME=";
};
buildInputs = [ jdk ];
nativeBuiltInputs = [ cmake ];
configurePhase = ''
sed -i 's/OS = MACOSX/OS = LINUX/g' Makefile.include
printf '%s\n%s\n' '#include <iostream>' "$(cat Kernel/AtomicDecomposer.cpp)" > Kernel/AtomicDecomposer.cpp
'';
installPhase = ''
mkdir -p $out/bin
mkdir -p $out/lib
install -m 755 FaCT++.{C,JNI,KE,Kernel}/obj/*.{so,o} $out/lib/
install -m 755 FaCT++/obj/FaCT++ $out/bin/FaCT++
'';
meta = with lib; {
description = "FaCT++ reasoner";
homepage = http://owl.cs.manchester.ac.uk/tools/fact/;
maintainers = [ maintainers.mgttlinger ];
license = licenses.gpl2Plus;
platforms = platforms.linux;
};
}
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