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

default.nix

@@ -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;

lib/src/CoAlgFormula.ml

@@ -1753,6 +1753,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.
@@ -2381,29 +2430,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

lib/src/CoAlgFormula.mli

@@ -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

lib/src/FormulaLexer.mll

@@ -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}

lib/src/FormulaParser.mly

@@ -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)
+                                      }
+
 %%
 

nix/fact++.nix

+{ 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;
+  };
+}