stormchecker/storm: v1.14.0

Zenodo (CERN European Organization for Nuclear Research)

Abstract

Moved from settings to environments or options in several places: LP solvers Model building Bisimulation Parsing Symbolic models Revised state and observation valuations. Added support for HiGHS MILP solver. Renamed --additional-checks to --check-zeno. Removed deprecated --lex argument. Lexicographic model checking can be invoked using the multilex(..) syntax. Reintroduced sample-derivative for storm-pars. Bug fixes: Parsing of Prism files such as observables and reserved keywords. Parsing of constant strings and negative number in commandline options. Parsing of DRN files with rational intervals. Multi-objective model checking for negative rewards. WeightVectorChecker for negative weights. In Valuations. Setting relative precision in LRA. Scheduler extraction for topological solver. State elimination for absorbing states. Synchronization vector for non-synchronizing JANI choices. MDP model checking of globally properties via hybrid engine. Memory products and initial states. Requires CMake >= 3.25. Updated gmm version to 5.5. Moved from parallel-hashmap to gtl. Developer: Sped up compilation of storm-parsers and storm-pars. Developer: Sped up tests by skipping a few costly tests. Developer: Fixed a number of compiler warnings. Developer: Cleaned up parts of code base such as state elimination and cli-utilities. Developer: Added support for clang-tidy. Developer: Improved code quality via reports from clang-tidy. Developer: Consistent handling of includes, asserts and throwing of exceptions. Developer: Introduced STORM_LOG_STATS. Developer: Added CMake option STORM_COMPILE_WITH_PCH. Developer: Added Copilot instructions.

Authors 28

1. Christian Hensel
2. Tim Quatmann Aachen @moves-rwth

   RWTH Aachen University

   Affiliation as printed

   @moves-rwth

3. Matthias Volk

   Eindhoven University of Technology

   Affiliation as printed

   Eindhoven University of Technology

4. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University

5. J. Berger Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

6. jipspel
7. Gereon Kremer
8. Alex Bork Aachen @moves-rwth

   RWTH Aachen University

   Affiliation as printed

   @moves-rwth

9. Daniel Basgöze
10. David
11. Hannah
12. Joachim Klein

    Technische Universität Dresden

    Affiliation as printed

    Ex TU Dresden, Germany

13. Timo P. Gros

    German Research Centre for Artificial Intelligence

    Affiliation as printed

    German Research Center for Artificial Intelligence (DFKI)

14. SPranger
15. Tom Janson
16. Johannes Lehmann

    Technische Universität Dresden

    Affiliation as printed

    TU Dresden

17. Jan Karuc
18. looomis
19. Linus
20. Sascha Vincent Kurowski
    Affiliation as printed

    Amazon Europe (@amzn)

21. SvStein
22. luko van der maas
23. Florent Delgrange

    Vrije Universiteit Brussel

    Affiliation as printed

    AI Lab, Vrije Universiteit Brussel

24. Josh Jeppson
    Affiliation as printed

    Lucid Software

25. Marckvdv
26. Arash Partow
    Affiliation as printed

    ἑ

27. spacefrogg
28. Peter Lindner Aachen

    RWTH Aachen University

    Affiliation as printed

    RWTH Aachen University