Add prism model checker

3 years ago · 2d3bfa5832
parent d579a46c16
commit 2d3bfa5832
3 changed files with 182 additions and 0 deletions
--- a/default.nix
+++ b/default.nix
@ -24,6 +24,8 @@ let
    vividSky = callPackage ./x-plane/vivid-sky.nix {};

    pdfchain = callPackage ./pdfchain { };
+    prism = callPackage ./prism.nix {};
+    lp_solve_java = callPackage ./lp_solve_java.nix {};
    # z3 = callPackage ./z3 { };
    # stormChecker = callPackage ./storm-checker { ltoSupport = false; tbbSupport = false; mathsatSupport = false; z3Support = false; };
    # carl = callPackage ./carl { };
--- a/lp_solve_java.nix
+++ b/lp_solve_java.nix
@ -0,0 +1,44 @@
+{ stdenv, fetchurl, jdk, lp_solve, unzip }:
+
+stdenv.mkDerivation rec {
+
+  name = "lp_solve_java-${version}";
+  version = "5.5.2.0";
+
+  src = fetchurl {
+    url = "mirror://sourceforge/project/lpsolve/lpsolve/${version}/lp_solve_${version}_java.zip";
+    sha256 = "1jfnl849i8fbfv3pmqspp6x1piq8ssyfgrg4bldzb564w0hwsk8a";
+  };
+
+  buildInputs = [ jdk lp_solve unzip ];
+
+  propagatedBuildInputs = [ lp_solve ];
+
+  phases = [ "unpackPhase" "buildPhase" "installPhase" ];
+
+  fname = "lpsolve55j";
+
+  buildPhase = ''
+    $CXX -fpic -DPIC -I ${jdk}/include -I ${jdk}/include/linux -I ${lp_solve}/include -I ./src/c -c \
+      src/c/lpsolve5j.cpp -o $fname.o
+    $CXX -shared -Wl,-soname,lib$fname.so -o lib$fname.so $fname.o -L ${lp_solve}/lib -lc -llpsolve55
+
+    (cd ./src/java
+     javac lpsolve/*.java #*/
+     jar -cf ../../$fname.jar lpsolve/*.class #*/
+    )
+  '';
+
+  installPhase = ''
+    mkdir -p $out/lib
+    cp lib$fname.so $fname.jar $out/lib
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Java bindings for the Mixed Integer Linear Programming solver lp_solve";
+    homepage = lp_solve.meta.homepage;
+    license = lp_solve.meta.license;
+    maintainers = with maintainers; [ spacefrogg ];
+    platforms = platforms.unix;
+  };
+}
--- a/prism.nix
+++ b/prism.nix
@ -0,0 +1,136 @@
+{ stdenv, lib, fetchFromGitHub, jdk, lp_solve, lp_solve_java, makeWrapper
+#, ltl2dstar, ltl2ba
+, makeDesktopItem, python27 }:
+
+let
+  src = fetchFromGitHub {
+    owner = "prismmodelchecker";
+    repo = "prism";
+    rev = "c2f637e177853b38fb8d9530e801e56d620e4466";
+    sha256 = "13xra91y542w808363wnqk9l7psnasy8c0sbkgmvxa6813i1i2i0";
+  };
+
+  version = "4.4-git";
+
+  cuddPrism = stdenv.mkDerivation rec {
+    name = "cudd-prism-${version}";
+    inherit version src;
+
+    buildInputs = [ jdk ];
+
+    configurePhase = "true";
+
+    buildPhase = ''
+      (
+      cd ./cudd
+      make clean JAVA_DIR="${jdk}"
+      )
+      (
+      cd ./prism
+      # will become cuddpackage
+      make cuddpackageforce JAVA_DIR="${jdk}"
+      )
+    '';
+
+    installPhase = ''
+      mkdir -p $out/{lib,include}
+      cd ./cudd
+      for dir in cudd dddmp epd mtr st util; do
+        cp ./$dir/lib$dir.a $out/lib
+        cp ./$dir/$dir.h $out/include
+      done
+      cp ./cudd/cuddInt.h $out/include
+    '';
+
+    meta.description = "Build of a Prism-adapted version of the CUDD library";
+  };
+
+in stdenv.mkDerivation {
+  pname = "prism";
+  inherit version src;
+
+  buildInputs = [ jdk lp_solve_java cuddPrism lp_solve makeWrapper python27 ];
+
+  patchPhase = ''
+    (cd ./prism
+    substituteInPlace ./Makefile \
+      --replace "CFLAGS=\"\$(CFLAGS)\"" "CFLAGS=\"\$(CFLAGS) \$(NIX_CFLAGS_COMPILE)\"" \
+      --replace "CPPFLAGS=\"\$(CPPFLAGS)\"" "CPPFLAGS=\"\$(CPPFLAGS) \$(NIX_CFLAGS)\"" \
+      --replace "LDFLAGS=\"\$(LDFLAGS)\"" "LDFLAGS=\"\$(LDFLAGS)\"" \
+      --replace "LDFLAGS = \$(CUDD_XCFLAGS)" "LDFLAGS = -lc -lstdc++" \
+      --replace "@./install.sh silent" ":"
+
+    LPSOLVE_JAR=$(echo ${lp_solve_java}/lib/*.jar) #*/
+    for dir in automata dv hybrid jdd jltl2ba jltl2dstar mtbdd odd param parser pepa/compiler prism pta settings strat userinterface ; do
+      substituteInPlace ./src/$dir/Makefile \
+        --replace "PRISM_CLASSPATH = \"" "PRISM_CLASSPATH = $LPSOLVE_JAR:\""
+    done
+
+    substituteInPlace ./src/bin/prism.linux \
+      --replace "PRISM_DIR=/home/luser/prism" "PRISM_DIR=$out
+PRISM_JAVA=\''${PRISM_JAVA-${jdk}/bin/java}" \
+      --replace "PRISM_CLASSPATH=" "PRISM_CLASSPATH=$LPSOLVE_JAR:" \
+      --replace "PRISM_LIB_PATH=" "PRISM_LIB_PATH=${lp_solve_java}/lib:"
+
+
+    substituteInPlace ./src/bin/xprism.linux \
+      --replace "PRISM_DIR=/home/luser/prism" "PRISM_DIR=$out
+PRISM_JAVA=\''${PRISM_JAVA-${jdk}/bin/java}" \
+      --replace "PRISM_CLASSPATH=" "PRISM_CLASSPATH=$LPSOLVE_JAR:" \
+      --replace "PRISM_LIB_PATH=" "PRISM_LIB_PATH=${lp_solve_java}/lib:"
+    )
+  '';
+
+  configurePhase = "true";
+
+  buildPhase = ''
+    (
+    cd ./prism
+
+    make clean JAVA_DIR="${jdk}"
+    make make_dirs CUDD_DIR="${cuddPrism}" JAVA_DIR="${jdk}" JNI_H_DIR="${jdk}/include/linux" JNI_MD_H_DIR="${jdk}/include/linux"
+    )
+  '';
+
+  installPhase = ''
+    mkdir -p $out/{bin,lib,include,classes,images,share/applications,share/icons/hicolor/{256x256,128x128,64x64,48x48,32x32,24x24,16x16}/apps}
+    cd ./prism
+    make bin_scripts CUDD_DIR="${cuddPrism}" JAVA_DIR="${jdk}" JNI_H_DIR="${jdk}/include/linux" JNI_MD_H_DIR="${jdk}/include/linux"
+
+    cp -r lib include bin classes images $out
+  '' +
+  # ''
+  #   cp etc/scripts/hoa/* $out/bin #*/
+  #   for i in $out/bin/hoa-* ; do
+  #       wrapProgram $i --prefix PATH : ${lib.makeBinPath [ ltl2dstar ltl2ba ]}
+  #   done
+  # '' +
+  ''
+    cp etc/scripts/prism-auto $out/bin
+
+    for i in etc/icons/p*.png ; do
+        SIZE=''${i#*/p}
+        SIZE=''${SIZE%.png}
+        cp $i $out/share/icons/hicolor/''${SIZE}x''${SIZE}/apps/xprism.png
+    done
+
+    ln -s ${makeDesktopItem {
+      name = "xprism";
+      desktopName = "XPrism Model Checker";
+      genericName = "Graphical frontend to Prism Model Checker";
+      exec = "xprism";
+      icon = "xprism";
+      categories = "Application;Science;Development;";
+    }}/share/applications/xprism.desktop $out/share/applications/xprism.desktop
+  '';
+
+  dontStrip = true;
+
+  meta = with lib; {
+    homepage = "http://www.prismmodelchecker.org/";
+    description = "Prism Probabilistic Model Checker";
+    license = licenses.gpl2;
+    maintainers = [ maintainers.spacefrogg ];
+    platforms = with platforms; linux;
+  };
+}