moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
126 stars 73 forks source link

STORM installation fails at Jani installation #524

Closed ranai-srivastav closed 1 month ago

ranai-srivastav commented 2 months ago

I am trying to write a Dockerfile for my software repository. I cannot use the Dockerfile that is in the repository because I need the base image to be CUDA compatible and have access to the GPU.

While installing, I clone the repository successfully but it stops with really weird errors like note: 'uint64_t' is defined in header '<cstdint>'; did you forget to '#include <cstdint>' or cannot convert const::boost in int, as can be seen in the error I've attached below.

My environment can be found in this Dockerfile

Error:

216.1 In file included from /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.cpp:1:
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:31:88: error: 'uint64_t' has not been declared
216.1    31 |     void makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const;
216.1       |                                                                                        ^~~~~~~~
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:42:21: error: 'uint64_t' was not declared in this scope
216.1    42 |     std::pair<bool, uint64_t> canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model,
216.1       |                     ^~~~~~~~
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:4:1: note: 'uint64_t' is defined in header '<cstdint>'; did you forget to '#include <cstdint>'?
216.1     3 | #include <boost/optional.hpp>
216.1   +++ |+#include <cstdint>
216.1     4 | #include <vector>
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:42:29: error: template argument 2 is invalid
216.1    42 |     std::pair<bool, uint64_t> canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model,
216.1       |                             ^
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:43:114: error: 'uint64_t' was not declared in this scope
216.1    43 |                                                    std::vector<Property> const& properties = {}, boost::optional<uint64_t> automatonIndex = boost::none) const;
216.1       |                                                                                                                  ^~~~~~~~
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:43:114: note: 'uint64_t' is defined in header '<cstdint>'; did you forget to '#include <cstdint>'?
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:43:122: error: template argument 1 is invalid
216.1    43 |                                                    std::vector<Property> const& properties = {}, boost::optional<uint64_t> automatonIndex = boost::none) const;
216.1       |                                                                                                                          ^
216.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:43:148: error: could not convert 'boost::none' from 'const boost::none_t' to 'int'
216.1    43 |                                                    std::vector<Property> const& properties = {}, boost::optional<uint64_t> automatonIndex = boost::none) const;
216.1       |                                                                                                                                             ~~~~~~~^~~~
216.1       |                                                                                                                                                    |
216.1       |                                                                                                                                                    const boost::none_t
216.2 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/ModelFeatures.cpp.o
216.4 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/ModelType.cpp.o
216.6 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/OrderedAssignments.cpp.o
217.0 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/ParallelComposition.cpp.o
217.0 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/Property.cpp.o
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.cpp:81:6: error: no declaration matches 'void storm::jani::JaniScopeChanger::makeVariableLocal(const storm::expressions::Variable&, storm::jani::Model&, uint64_t) const'
217.1    81 | void JaniScopeChanger::makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const {
217.1       |      ^~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:31:10: note: candidate is: 'void storm::jani::JaniScopeChanger::makeVariableLocal(const storm::expressions::Variable&, storm::jani::Model&, int) const'
217.1    31 |     void makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const;
217.1       |          ^~~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:17:7: note: 'class storm::jani::JaniScopeChanger' defined here
217.1    17 | class JaniScopeChanger {
217.1       |       ^~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.cpp:108:27: error: no declaration matches 'std::pair<bool, long unsigned int> storm::jani::JaniScopeChanger::canMakeVariableLocal(const storm::expressions::Variable&, const storm::jani::Model&, const std::vector<storm::jani::Property>&, boost::optional<long unsigned int>) const'
217.1   108 | std::pair<bool, uint64_t> JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model,
217.1       |                           ^~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:42:31: note: candidate is: 'int storm::jani::JaniScopeChanger::canMakeVariableLocal(const storm::expressions::Variable&, const storm::jani::Model&, const std::vector<storm::jani::Property>&, int) const'
217.1    42 |     std::pair<bool, uint64_t> canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model,
217.1       |                               ^~~~~~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:17:7: note: 'class storm::jani::JaniScopeChanger' defined here
217.1    17 | class JaniScopeChanger {
217.1       |       ^~~~~~~~~~~~~~~~
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.cpp: In member function 'void storm::jani::JaniScopeChanger::makeVariablesLocal(storm::jani::Model&, const std::vector<storm::jani::Property>&) const':
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.cpp:180:46: error: cannot convert 'const boost::none_t' to 'int'
217.1   180 |         auto makeLocal = canMakeVariableLocal(v.getExpressionVariable(), model, properties);
217.1       |                          ~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
217.1       |                                              |
217.1       |                                              const boost::none_t
217.1 /root/software/storm-1.8.0/src/storm/storage/jani/JaniScopeChanger.h:43:124: note:   initializing argument 4 of 'int storm::jani::JaniScopeChanger::canMakeVariableLocal(const storm::expressions::Variable&, const storm::jani::Model&, const std::vector<storm::jani::Property>&, int) const'
217.1    43 |                                                    std::vector<Property> const& properties = {}, boost::optional<uint64_t> automatonIndex = boost::none) const;
217.1       |                                                                                                  ~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~
217.2 [ 90%] Building CXX object src/storm/CMakeFiles/storm.dir/storage/jani/TemplateEdge.cpp.o
217.4 make[3]: *** [src/storm/CMakeFiles/storm.dir/build.make:6368: src/storm/CMakeFiles/storm.dir/storage/jani/JaniScopeChanger.cpp.o] Error 1
217.4 make[3]: *** Waiting for unfinished jobs....
220.7 make[2]: *** [CMakeFiles/Makefile2:1925: src/storm/CMakeFiles/storm.dir/all] Error 2
220.7 make[1]: *** [CMakeFiles/Makefile2:1899: src/storm/CMakeFiles/storm-main.dir/rule] Error 2
220.7 make: *** [Makefile:743: storm-main] Error 2
------
Dockerfile:127
--------------------
 125 |     RUN cd build && cmake .. 
 126 |     WORKDIR /root/software/storm-1.8.0/build
 127 | >>> RUN make storm-main -j8
 128 |     
 129 |     # WORKDIR /root/software
volkm commented 2 months ago

Can you try using the latest release 1.8.1 of Storm and see whether this makes a difference?

ranai-srivastav commented 2 months ago

@volkm The error does not change at all. I've updated my Dockerfile with the new version at the same link as above (https://github.com/IowaState-AutonomousSystemsLab/TRELPy/blob/main/.devcontainer/Dockerfile)

tquatmann commented 2 months ago

It looks like there is simply an include missing. PR #525 adds this missing include.

There might be more includes missing for your setup. Can you check if using the corresponding branch from my repository in your dockerfile works?

sjunges commented 2 months ago

In addition, can you post the compiler version you have. It should be part of the output when running cmake on a fresh build folder.

ranai-srivastav commented 2 months ago

That was great! Any idea on when this will get merged to the stable branch?

sjunges commented 1 month ago

I guess this will be another 4 weeks....

ranai-srivastav commented 1 month ago

Hey Sorry for the delayed response @sjunges . If there's any other info that can be helpful lmk!

gcc-13, CXX compiler 13.1.0

The PR being merged fixed the issue for me.