From 2d3bfa583207161baf0d2b8a7ade867411619e61 Mon Sep 17 00:00:00 2001 From: Michael Raitza Date: Mon, 7 Dec 2020 23:10:02 +0100 Subject: [PATCH] Add prism model checker --- default.nix | 2 + lp_solve_java.nix | 44 +++++++++++++++ prism.nix | 136 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 182 insertions(+) create mode 100644 lp_solve_java.nix create mode 100644 prism.nix diff --git a/default.nix b/default.nix index dfa268e..2b9dc75 100644 --- 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 { }; diff --git a/lp_solve_java.nix b/lp_solve_java.nix new file mode 100644 index 0000000..4dccaa1 --- /dev/null +++ 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; + }; +} diff --git a/prism.nix b/prism.nix new file mode 100644 index 0000000..7140bca --- /dev/null +++ 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; + }; +}