# Copyright 2026 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
JAVA_PKG_WANT_BUILD_VM="
openjdk-11 openjdk-bin-11
openjdk-17 openjdk-bin-17
openjdk-21 openjdk-bin-21
openjdk-25 openjdk-bin-25
"
JAVA_PKG_WANT_SOURCE="1.8"
JAVA_PKG_WANT_TARGET="1.8"
JAVA_RM_FILES=( "spins/lib/javacc.jar" )
inherit autotools flag-o-matic java-pkg-2 optfeature shell-completion
SPINS_SHA="bfca30be3ce81fd77b31b9d47043145ae66ddc96"
DESCRIPTION="High-performance language-independent model checking tools"
HOMEPAGE="https://github.com/utwente-fmt/ltsmin"
SRC_URI="
https://github.com/utwente-fmt/ltsmin/releases/download/v${PV}/ltsmin-v${PV}-source.tgz -> ${P}.tgz
buddy? (
https://github.com/utwente-fmt/buddy/archive/refs/tags/v2.4.tar.gz
-> ${PN}-buddy-2.4.tar.gz
)
spins? (
https://github.com/utwente-fmt/spins/archive/${SPINS_SHA}.tar.gz
-> ${PN}-spins-${SPINS_SHA}.tar.gz
)
"
S="${WORKDIR}/${P}"
LICENSE="BSD GPL-2+ buddy? ( buddy ) spins? ( Apache-2.0 )"
SLOT="0"
KEYWORDS="~amd64"
IUSE="+gmp +prob +sylvan boost buddy mpi pnml profiler spins test zip"
BDEPEND="
>=sys-devel/bison-3.0.2
sys-devel/flex
virtual/pkgconfig
spins? (
>=dev-java/ant-1.9.8:0
>=virtual/jdk-11:*
)
"
COMMON_DEPEND="
dev-libs/popt
virtual/zlib
gmp? ( dev-libs/gmp:= )
mpi? ( virtual/mpi )
pnml? ( dev-libs/libxml2:2= )
prob? ( net-libs/czmq:= )
profiler? ( dev-util/google-perftools:=[-minimal] )
sylvan? (
>=sci-mathematics/sylvan-1.1
<sci-mathematics/sylvan-1.2
)
zip? ( dev-libs/libzip:= )
"
DEPEND="
${COMMON_DEPEND}
boost? ( dev-libs/boost )
"
RDEPEND="
${COMMON_DEPEND}
spins? (
sys-devel/gcc
>=virtual/jre-1.8:*
)
"
RESTRICT="!test? ( test )"
PATCHES=(
"${FILESDIR}/${P}-configure-bignum-test.patch"
"${FILESDIR}/${P}-configure-cache-line-test.patch"
"${FILESDIR}/${P}-czmq-zsock.patch"
"${FILESDIR}/${P}-default-listdd64.patch"
"${FILESDIR}/${P}-mpi3.patch"
"${FILESDIR}/${P}-prob-lace-options.patch"
"${FILESDIR}/${P}-ltl2ba-fno-common.patch"
)
DOCS=( AUTHORS CODING-STANDARDS README.md )
pkg_setup() {
use spins && java-pkg-2_pkg_setup
}
src_prepare() {
rm "${S}/spins/spins.jar" || die
rmdir "${S}/spins" || die
if use spins; then
mv "${WORKDIR}/spins-${SPINS_SHA}" "${S}/spins" || die
sed -i -e 's/\r$//' "${S}/spins/src/build.xml" || die
eapply "${FILESDIR}/${P}-spins-build.patch"
fi
if use buddy; then
pushd "${WORKDIR}/buddy-2.4" >/dev/null || die
eapply "${FILESDIR}/${PN}-buddy-2.4-bddproduced-type.patch"
AT_M4DIR=m4 eautoreconf
popd >/dev/null || die
fi
default
use spins && java-pkg-2_src_prepare
# Keep the generated Automake 1.14 files from being regenerated after
# patching their source files and the generated configure script.
touch -r aclocal.m4 configure.ac m4/acx_cache_line.m4 || die
}
src_configure() {
local buddy_prefix=${T}/buddy
# This release and its BuDDy fork contain incompatible declarations
# across translation units. GCC LTO diagnoses these and may miscompile
# the code even where the linker accepts it.
filter-lto
if use buddy; then
# LTSmin needs its own BuDDy fork. The stock implementation has the
# same API but aborts when LTSmin creates an FDD domain, and both
# projects install libbdd.so. Keep the compatible fork private and
# link it statically instead of colliding with sci-libs/buddy.
mkdir "${WORKDIR}/buddy-build" || die
pushd "${WORKDIR}/buddy-build" >/dev/null || die
(
append-flags -fPIC
ECONF_SOURCE="${WORKDIR}/buddy-2.4" econf \
--prefix="${buddy_prefix}" \
--libdir="${buddy_prefix}/lib" \
--disable-shared \
--enable-static
emake
emake install
)
popd >/dev/null || die
fi
# The bundled Lemon generator uses pre-C23 K&R function declarations.
append-cflags -std=gnu17
local myeconfargs=(
--disable-doxygen-doc
--disable-opaal
--disable-scoop
--disable-werror
--with-mcrl=no
--with-mcrl2=no
--with-viennacl="${T}/disabled"
--without-spot
$(use_enable mpi dist)
$(use_enable pnml)
$(use_enable prob)
$(use_with boost)
$(use_with spins)
$(use_with sylvan)
--with-bignum=$(usex gmp gmp no)
)
if use buddy; then
export PKG_CONFIG_PATH="${buddy_prefix}/lib/pkgconfig${PKG_CONFIG_PATH:+:${PKG_CONFIG_PATH}}"
myeconfargs+=( --with-buddy )
else
myeconfargs+=( --without-buddy )
fi
# AC_ARG_WITH(profiler) treats --without-profiler as enabled, so omit
# the switch entirely for the default disabled case.
use profiler && myeconfargs+=( --with-profiler )
# libzip has no configure switch in this release.
use zip || export ac_cv_lib_zip_zip_open=no
econf "${myeconfargs[@]}"
}
src_compile() {
use spins && eant -f spins/src/build.xml jar
# lemon/Makefile replaces rather than augments CFLAGS.
emake CFLAGS="${CFLAGS}"
}
src_test() {
# The top-level DejaGNU suite unconditionally exercises optional external
# compilers such as DiVinE and SpinS. Run the self-contained unit tests
# here, then cover the enabled backends explicitly below.
emake -C src CFLAGS="${CFLAGS}" check
local testdir=${T}/functional
mkdir "${testdir}" || die
cat > "${testdir}/cycle.etf" <<-EOF || die
begin state
x:int
end state
begin edge
end edge
begin init
0
end init
begin trans
0/1
1/0
end trans
EOF
local lace_args=()
use sylvan && lace_args=( --lace-workers=1 )
local output
output=$("${S}/src/pins2lts-seq/etf2lts-seq" "${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"2 states 2 transitions"* ]] || die "sequential ETF test failed"
output=$("${S}/src/pins2lts-sym/etf2lts-sym" "${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"state space has 2 states"* ]] || die "symbolic ETF test failed"
if use sylvan; then
[[ ${output} == *"Creating a multi-core ListDD domain"* ]] ||
die "default symbolic backend is not Sylvan LDDmc"
output=$("${S}/src/pins2lts-sym/etf2lts-sym" "${lace_args[@]}" \
--vset=lddmc "${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"Creating a multi-core ListDD domain"* ]] ||
die "Sylvan LDDmc ETF test failed"
[[ ${output} == *"state space has 2 states"* ]] ||
die "Sylvan LDDmc ETF state count failed"
output=$("${S}/src/pins2lts-sym/etf2lts-sym" "${lace_args[@]}" \
--vset=sylvan "${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"Creating a Sylvan domain"* ]] ||
die "Sylvan BDD ETF test failed"
[[ ${output} == *"state space has 2 states"* ]] ||
die "Sylvan BDD ETF state count failed"
fi
output=$("${S}/src/pins2lts-mc/etf2lts-mc" "${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"2 states 2 transitions"* ]] || die "multicore ETF test failed"
if use buddy; then
output=$("${S}/src/pins2lts-sym/etf2lts-sym" "${lace_args[@]}" --vset=fdd \
"${testdir}/cycle.etf" 2>&1) || die
[[ ${output} == *"Creating a BuDDy fdd domain"* ]] || die "BuDDy ETF test failed"
fi
if use prob; then
output=$(nonfatal "${S}/src/pins2lts-sym/prob2lts-sym" --help 2>&1)
[[ ${output} == *"--lace-workers"* ]] || die "ProB Lace options are unavailable"
fi
if use spins; then
pushd "${testdir}" >/dev/null || die
output=$("${S}/src/scripts/spins" -o "${S}/examples/p117.pml" 2>&1) ||
die "SpinS failed to compile Promela: ${output}"
output=$("${S}/src/pins2lts-seq/prom2lts-seq" p117.pml.spins 2>&1) ||
die "LTSmin failed to explore the SpinS model: ${output}"
[[ ${output} == *"354 states 828 transitions"* ]] || die "SpinS Promela test failed"
popd >/dev/null || die
fi
}
src_install() {
default
if ! use mpi; then
rm -f "${ED}"/usr/bin/*-dist \
"${ED}"/usr/bin/ce-mpi \
"${ED}"/usr/bin/ltsmin-reduce-dist || die
fi
if ! use spins; then
rm -f "${ED}"/usr/bin/spins "${ED}"/usr/share/ltsmin/spins.jar || die
fi
# Upstream only installs generated manual pages when documentation build
# tools are detected. Install the release-matched pages for commands that
# survived USE filtering, plus the shared format documentation.
local command page
for command in "${ED}"/usr/bin/*; do
[[ -e ${command} ]] || continue
page="${S}/doc/${command##*/}.1"
[[ -f ${page} ]] && doman "${page}"
done
doman "${S}"/doc/*.5 "${S}/doc/ltsmin.7"
newbashcomp contrib/bash-completion/ltsmin ltsmin
find "${ED}" -type f -name '*.la' -delete || die
rm -f "${ED}/usr/share/doc/${PF}/COPYING" || die
}
pkg_postinst() {
use prob && optfeature "ProB model checking" sci-mathematics/prob-bin
}