Libarchive and DRN Improvements #862

tquatmann · 2026-02-09T13:50:27Z

Storm can now be linked with libarchive as an optional dependency

New features:

Developer: Conveniently read and write binary and textual files from and to an archive (without writing the intermediate file to disk first)
DRN: Control the precision of floats in DRN export using --io:digits option
DRN: Reading from and writing to compressed DRN files (use .drn.gz / drn.xz file extensions and/or the new --compression option) (requires libarchive)
DRN: add @value_type section in DRN files to determine the type of the parsed values.
DRN: support for parsing of DRN interval models from CLI (if they have a corresponding @value_type section)

Once this is merged, we need to adapt this page and add libarchive to the optional dependencies on the website.
~~Side note: I noted that the DRN page does not mention the @nr_choices section.~~

- Storm can now be linked with libarchive as an optional dependency - Auxiliary functions to conveniently read and write binary and textual files from and to an archive - allow to control the precision of floats in DRN export using --io:digits option - allow reading from and writing to compressed DRN files (use .drn.gz / drn.xz file extensions and/or the new --compression option) (requires libarchive)

…arsed values. - support for parsing of DRN interval models from CLI (if they have a @value_type section)

tquatmann · 2026-02-09T13:51:28Z

~~I marked this as a draft since I haven't tested the DRN @value_type logic yet.~~

sjunges · 2026-02-09T14:15:14Z

resources/3rdparty/CMakeLists.txt

+        # following https://stackoverflow.com/a/76916842
+        # Homebrew ships libarchive keg only, include dirs have to be set manually
+        execute_process(
+                COMMAND brew --prefix libarchive


This assumes that it has been installed with brew? Can/Should we maybe first check whether it is somehow already present in the system otherwise via find_package?

Ah, I now see that it is always searched fore and that we are only setting a prefix variable, which is implicitly used by the findpackage below? I am not sure using PREFIX is better than passing this as a hint to the find package?

Seconded. There are people on mac not using homebrew ;).

Yes, the execute_process is used to get a hint to catch the common case where brew is used. It fails quietly if brew is not installed.
I added some comments to clarify this.

Any advice on how to avoid this brew hack? And/or adding a hint to the find_package?
Setting LibArchive_INCLUDE_DIR seems to work most of the time, but I'd rather set the hint.

Relevant:

> brew info libarchive [...] libarchive is keg-only, which means it was not symlinked into /opt/homebrew, because macOS already provides this software and installing another version in parallel can cause all kinds of trouble. If you need to have libarchive first in your PATH, run: echo 'export PATH="/opt/homebrew/opt/libarchive/bin:$PATH"' >> ~/.zshrc For compilers to find libarchive you may need to set: export LDFLAGS="-L/opt/homebrew/opt/libarchive/lib" export CPPFLAGS="-I/opt/homebrew/opt/libarchive/include" For pkgconf to find libarchive you may need to set: export PKG_CONFIG_PATH="/opt/homebrew/opt/libarchive/lib/pkgconfig" [...]

The version shipped with macOS apparently does not have any include files.

Could you use the HINTS for find_package instead of setting the include directory? Alternatively, you could try setting LibArchive_ROOT.
Last idea could be to write a FindLibArchive.cmake which contains the homebrew workaround. This might then also work if we install Storm.

sjunges · 2026-02-09T14:15:33Z

resources/3rdparty/CMakeLists.txt

+                set(LibArchive_INCLUDE_DIR "${LIBARCHIVE_PREFIX}/include")
+            else()
+                message(STATUS "Storm - LibArchive  not found in ${LIBARCHIVE_PREFIX}/include.")
+            endif()


Should we have an else case here that also reports that libarchive is not found?

That output was just to see if the brew hint was successful. I removed it because it is confusing.
There is always some kind of output after find_package

sjunges · 2026-02-09T14:17:53Z

resources/3rdparty/CMakeLists.txt

+	endif()
+else()
+    SET(STORM_HAVE_LIBARCHIVE OFF)
+    message (WARNING "Storm - Not linking with LibArchive. Loading and exporting compressed files such will not be supported.")


Should this be a status or a warning?

STATUS seems to be more in line with other dependencies.

volkm · 2026-02-09T14:18:27Z

Side note: I noted that the DRN page does not mention the @no_choices section.

I think it should be @nr_choices which is mentioned.

sjunges · 2026-02-09T14:18:36Z

resources/3rdparty/CMakeLists.txt

+else()
+    SET(STORM_HAVE_LIBARCHIVE OFF)
+    message (WARNING "Storm - Not linking with LibArchive. Loading and exporting compressed files such will not be supported.")
+endif()


Warning message above may explicitly mention UMB (even uncompressed, as it is packed!)

sjunges · 2026-02-09T14:19:34Z

resources/cmake/stormConfig.cmake.install.in

    )
 endif()

+if(@STORM_HAVE_LIBARCHIVE@) # STORM_HAVE_LIBARCHIVE


Why does this code not need the brew workaround?

Ohh, it might actually need it.

sjunges · 2026-02-09T14:26:03Z

src/storm/io/ArchiveReader.h

+         */
+        Iterator& operator++();
+
+        ArchiveReadEntry operator*() const;


Return a reference to?

ArchiveReadEntry essentially wraps around two (non-owning) pointers.
Returning a reference here has no real benefit and we would need to have an entity that "owns" ArchiveReadEntries.

tquatmann · 2026-02-09T21:11:01Z

Side note: I noted that the DRN page does not mention the @no_choices section.

I think it should be @nr_choices which is mentioned.

Ahh, true. I did not read that paragraph carefully enough. Sorry :)

…lue type from @value_type section

tquatmann · 2026-02-10T10:21:21Z

For future reference, I used the following script to test DRN import/export from CLI a little

mkdir -p tmp
rm tmp/*

set -e
STORM=./build/bin/storm
EXAMPLES=./resources/examples/testfiles

# brp (DTMC)

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn
grep double tmp/brp-double.drn
$STORM -drn tmp/brp-double.drn
$STORM -drn tmp/brp-double.drn --exact
$STORM -drn tmp/brp-double.drn --parametric

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn.xz
$STORM -drn tmp/brp-double.drn.xz

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-double.drn.gz
$STORM -drn tmp/brp-double.drn.gz

$STORM --prism $EXAMPLES/dtmc/brp-16-2.pm --exportbuild tmp/brp-exact.drn --exact
grep rational tmp/brp-exact.drn
$STORM -drn tmp/brp-exact.drn
$STORM -drn tmp/brp-exact.drn --exact
$STORM -drn tmp/brp-exact.drn --parametric

# polling (MA)

$STORM --prism $EXAMPLES/ma/polling.ma -const N=3,Q=3 --exportbuild tmp/pol-double.drn --buildchoicelab
grep double tmp/pol-double.drn
$STORM -drn tmp/pol-double.drn
$STORM -drn tmp/pol-double.drn --buildchoicelab
$STORM -drn tmp/pol-double.drn --exact
$STORM -drn tmp/pol-double.drn --parametric

# robot (IMDP)
$STORM --prism $EXAMPLES/imdp/robot.prism -const delta=0.5 --exportbuild tmp/robot-double.drn
grep "double-interval" tmp/robot-double.drn
$STORM -drn tmp/robot-double.drn

# nand (PDTMC)
$STORM --prism $EXAMPLES/pdtmc/nand-5-2.pm --exportbuild tmp/nand-par.drn --parametric
grep "parametric" tmp/nand-par.drn
$STORM -drn tmp/nand-par.drn --parametric

volkm

Looks good in general. Thanks for all the work.

I have mostly minor comments which should hopefully be fast to modify.

volkm · 2026-02-10T13:44:31Z

src/storm/io/CompressionMode.h

+enum class CompressionMode { Default, None, Gzip, Xz };
+
+/*!
+ * @return The expression mode whose string representation matches the given input


Suggested change

* @return The expression mode whose string representation matches the given input

* @return The compression mode whose string representation matches the given input

volkm · 2026-02-10T13:49:36Z

src/storm/storage/BitVector.h

+     * Sets the bits in the given bucket to the given value.
+     * @param bucketIndex The bucket. Bucket index i refers to the 64 bits with index i*64 to i*64+63.
+     * @param value The values to set. E.g., 1ull sets bit i*64 to 1 and all other bits in the bucket to 0
+     * @note: bucketIndex must be below bucketCount(). Values for bitindices > size() are ignored


Suggested change

* @note: bucketIndex must be below bucketCount(). Values for bitindices > size() are ignored

* @note: bucketIndex must be below bucketCount(). Values for bitindices > bucketCount() are ignored

volkm · 2026-02-10T13:50:11Z

src/storm/storage/BitVector.h

+    void setBucket(uint64_t bucketIndex, uint64_t value);
+
+    /*!
+     * Gets the bits in the given bucket to the given value.


Suggested change

* Gets the bits in the given bucket to the given value.

* Gets the bits in the given bucket.

volkm · 2026-02-10T13:50:23Z

src/storm/storage/BitVector.h

+     * Gets the bits in the given bucket to the given value.
+     * @param bucketIndex The bucket. Bucket index i refers to the 64 bits with index i*64 to i*64+63.
+     * @return The values of the bits in the given bucket.
+     * @note: bucketIndex must be below bucketCount(). Values for bitindices > size() are always 0


Suggested change

* @note: bucketIndex must be below bucketCount(). Values for bitindices > size() are always 0

* @note: bucketIndex must be below bucketCount(). Values for bitindices > bucketCount() are always 0

volkm · 2026-02-10T13:51:40Z

src/storm/storage/BitVector.h

+     *
+     * @return The number of buckets of the underlying storage.
+     */
+    size_t bucketCount() const;


If you are moving the function, maybe move it after size()?
But not important.

volkm · 2026-02-10T15:41:36Z

src/storm/io/ArchiveWriter.cpp

+#include "storm/storage/BitVector.h"
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/NotSupportedException.h"


Suggested change

#include "storm/storage/BitVector.h"

#include "storm/utility/macros.h"

#include "storm/exceptions/NotSupportedException.h"

#include "storm/exceptions/NotSupportedException.h"

#include "storm/storage/BitVector.h"

#include "storm/utility/macros.h"

volkm · 2026-02-10T15:41:52Z

src/storm/io/ArchiveWriter.cpp

+}
+#else
+ArchiveWriter::ArchiveWriter(std::filesystem::path const&, CompressionMode const) {
+    throw storm::exceptions::NotSupportedException() << "Writing archives is not supported. Storm is compiled without LibArchive.";


Suggested change

throw storm::exceptions::NotSupportedException() << "Writing archives is not supported. Storm is compiled without LibArchive.";

throw storm::exceptions::MissingLibraryException() << "Writing archives is not supported. Storm is compiled without LibArchive.";

volkm · 2026-02-10T15:43:00Z

src/storm/io/ArchiveWriter.cpp

+    // Free the entry metadata after we finish writing
+    archive_entry_free(entry);
+#else
+    throw storm::exceptions::NotSupportedException() << "Writing archives is not supported. Storm is compiled without LibArchive.";


Suggested change

throw storm::exceptions::NotSupportedException() << "Writing archives is not supported. Storm is compiled without LibArchive.";

throw storm::exceptions::MissingLibraryException() << "Writing archives is not supported. Storm is compiled without LibArchive.";

volkm · 2026-02-10T15:53:18Z

resources/3rdparty/CMakeLists.txt

+        unset(LibArchive_BREW_HINT)
+    endif()
+    find_package(LibArchive QUIET)
+    if(TARGET LibArchive::LibArchive)


Why not use LibArchive_FOUND?

volkm · 2026-02-10T16:13:37Z

resources/3rdparty/CMakeLists.txt

+        # following https://stackoverflow.com/a/76916842
+        # Homebrew ships libarchive keg only, include dirs have to be set manually
+        execute_process(
+                COMMAND brew --prefix libarchive


Could you use the HINTS for find_package instead of setting the include directory? Alternatively, you could try setting LibArchive_ROOT.
Last idea could be to write a FindLibArchive.cmake which contains the homebrew workaround. This might then also work if we install Storm.

tquatmann added 2 commits February 9, 2026 10:59

- add @value_type section in DRN files to determine the type of the p…

159a86c

…arsed values. - support for parsing of DRN interval models from CLI (if they have a @value_type section)

sjunges reviewed Feb 9, 2026

View reviewed changes

tquatmann added 9 commits February 9, 2026 23:46

clarification of libarchive hack

504d13e

add inline

0a1d101

fix compilation

1aba229

fix drn-test

b4b26bf

fix drn parsing

957805f

revert accidentally commited change

9ecd13c

Drn: fixes and simplifications for parser

13a97a8

Update drn testfiles to new format.

5502409

DRN: more tests, including parsing of compressed files and reading va…

f4a5e2e

…lue type from @value_type section

tquatmann added 4 commits February 10, 2026 11:29

Fix compilation

38b7d1b

Fix compilation

f796ced

Missing include

55cb70c

Compilation fixes

7a3eeba

tquatmann marked this pull request as ready for review February 10, 2026 13:00

volkm requested changes Feb 10, 2026

View reviewed changes

	* @return The expression mode whose string representation matches the given input
	* @return The compression mode whose string representation matches the given input

	* @note: bucketIndex must be below bucketCount(). Values for bitindices > size() are ignored
	* @note: bucketIndex must be below bucketCount(). Values for bitindices > bucketCount() are ignored

	* Gets the bits in the given bucket to the given value.
	* Gets the bits in the given bucket.

	throw storm::exceptions::NotSupportedException() << "Writing archives is not supported. Storm is compiled without LibArchive.";
	throw storm::exceptions::MissingLibraryException() << "Writing archives is not supported. Storm is compiled without LibArchive.";

Libarchive and DRN Improvements #862

Are you sure you want to change the base?

Libarchive and DRN Improvements #862

Uh oh!

Conversation

tquatmann commented Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tquatmann commented Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tquatmann Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

volkm commented Feb 9, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tquatmann commented Feb 9, 2026

Uh oh!

tquatmann commented Feb 10, 2026

Uh oh!

volkm left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tquatmann commented Feb 9, 2026 •

edited

Loading

tquatmann commented Feb 9, 2026 •

edited

Loading

tquatmann Feb 9, 2026 •

edited

Loading