Build Error without z3 #667
Comments
|
This issue has probably been fixed already in this PR #520 (which is probably not in the stable branch yet). |
|
I have switch to master branch git checkout master and delete the build folder and create again follow these steps cd build Get a new error CMake Error at /work/cs-grad/tuanle/xSRL/storm/build/sylvan/src/sylvan-stamp/sylvan-configure-RELEASE.cmake:49 (message): '/work/cs-grad/tuanle/miniconda3/envs/xsrl/bin/cmake' '-DPROJECT_NAME=storm' '-DCMAKE_C_COMPILER=/usr/bin/cc' '-DCMAKE_CXX_COMPILER=/usr/bin/c++' '-DSYLVAN_BUILD_DOCS=OFF' '-DSYLVAN_BUILD_EXAMPLES=OFF' '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_POSITION_INDEPENDENT_CODE=ON' '-DSYLVAN_GMP=ON' '-DUSE_CARL=ON' '-Dcarl_DIR=/work/cs-grad/tuanle/xSRL/carl-storm/build' '-DBUILD_SHARED_LIBS=OFF' '-GUnix Makefiles' '-S' '/work/cs-grad/tuanle/xSRL/storm/resources/3rdparty/sylvan' '-B' '/work/cs-grad/tuanle/xSRL/storm/build/resources/3rdparty/sylvan' See also The log file is �[31mCMake Error at /work/cs-grad/tuanle/miniconda3/envs/xsrl/share/cmake-3.29/Modules/FindPackageHandleStandardArgs.cmake:230 (message): �[0m -- The C compiler identification is GNU 11.4.1 |
|
Please help me with this issue. I appreciate your help a lot. Thank you so much for your help. |
|
Appearantly, sylvan does not find the GMP library. Did you install the GMP library? In particular, here are the dependencies we require: https://www.stormchecker.org/documentation/obtain-storm/dependencies.html Furthermore, could you add all CMAKE output? Sebastian |
|
i have successfully go to the step 'make test' and i have this Failed test. May I ask you if you can help me with this [ FAILED ] BeliefExplorationTest/1.simple_Rmax, where TypeParam = (anonymous namespace)::SelfloopReductionDefaultDoubleVIEnvironment 280 FAILED TESTS 35/36 Test #35: run-test-pomdp-tracking ................***Failed 0.03 sec [----------] Global test environment tear-down 1 FAILED TEST 36/36 Test #36: run-test-pomdp-api .....................***Failed 0.05 sec [----------] Global test environment tear-down 14 FAILED TESTS 36% tests passed, 23 tests failed out of 36 Total Test time (real) = 184.00 sec The following tests FAILED: |
|
Hey, thanks for the report. the error says that the optional dependency z3 was not available during compilation. We recommend installing z3, but depending on what you want to do, you will not need it. However, the absence of z3 does not explain why the other tests fail. Could you post here why run-test-model fails? @AlexBork can you look into the error messages that are given for the POMDPs? I guess we need some skipping. -- Sebastian |
|
this is all the error message ERROR (Z3SmtSolver.cpp:120): Storm is compiled without Z3 support. [----------] 8 tests from ExplicitJaniModelBuilderTest [----------] 4 tests from DdPrismModelBuilderTest_Sylvan [----------] 4 tests from DdPrismModelBuilderTest_Cudd [----------] 1 test from UnboundedTest_Sylvan [----------] 1 test from UnboundedTest_Cudd [----------] 6 tests from DdJaniModelBuilderTest_Sylvan [----------] 6 tests from DdJaniModelBuilderTest_Cudd [----------] Global test environment tear-down 14 FAILED TESTS 4/36 Test #4: run-test-logic ......................... Passed 0.02 sec [----------] 1 test from MarkovAutomatonTest [----------] Global test environment tear-down 1 FAILED TEST 6/36 Test #6: run-test-parser ........................ Passed 0.58 sec [----------] Global test environment tear-down 1 FAILED TEST 8/36 Test #8: run-test-solver ........................ Passed 0.13 sec [----------] 10 tests from SymbolicModelBisimulationDecomposition [----------] 26 tests from SylvanDd [----------] 3 tests from StronglyConnectedComponentDecomposition [----------] 6 tests from SparseMatrixBuilder [----------] 22 tests from SparseMatrix [----------] 2 tests from SchedulerTest [----------] 3 tests from PrismProgramTest [----------] 1 test from NondeterministicModelBisimulationDecomposition [----------] 5 tests from MaximalEndComponentDecomposition [----------] 19 tests from JaniLocalEliminator [----------] 9 tests from Expression [----------] 3 tests from ExpressionEvaluation [----------] 2 tests from DeterministicModelBisimulationDecomposition [----------] 19 tests from CuddDd [----------] Global test environment tear-down 19 FAILED TESTS 10/36 Test #10: run-test-transformer ...................***Failed 0.04 sec [----------] 3 tests from NonMarkovianChainTransformerTest [----------] 1 test from NeutralECRemover [----------] 1 test from DAProductBuilderTest_aUb [----------] 1 test from DAProductBuilderTest_aWb [----------] 2 tests from AddUncertaintyTransformerTest [----------] Global test environment tear-down 9 FAILED TESTS 11/36 Test #11: run-test-utility .......................***Failed 3.44 sec [----------] 6 tests from GraphTest [----------] 2 tests from FileTest [----------] Global test environment tear-down 9 FAILED TESTS 12/36 Test #12: run-test-modelchecker-csl ..............***Failed 4.80 sec [----------] 1 test from SteadyStateCtmcCslModelCheckerTest/1, where TypeParam = (anonymous namespace)::SparseSoundEvtEnvironment [----------] 1 test from SteadyStateCtmcCslModelCheckerTest/2, where TypeParam = (anonymous namespace)::SparseClassicEnvironment [----------] 1 test from SteadyStateCtmcCslModelCheckerTest/3, where TypeParam = (anonymous namespace)::SparseEigenRationalLuEnvironment [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/0, where TypeParam = (anonymous namespace)::SparseDoubleValueIterationEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/0.LtlSimple (0 ms) [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/1, where TypeParam = (anonymous namespace)::JaniSparseDoubleValueIterationEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/1.LtlSimple (0 ms) [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/2, where TypeParam = (anonymous namespace)::JaniHybridDoubleValueIterationEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/2.LtlSimple (0 ms) [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/3, where TypeParam = (anonymous namespace)::SparseDoubleIntervalIterationEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/3.LtlSimple (0 ms) [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/4, where TypeParam = (anonymous namespace)::SparseRationalPolicyIterationEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/4.LtlSimple (0 ms) [----------] 5 tests from MarkovAutomatonCslModelCheckerTest/5, where TypeParam = (anonymous namespace)::SparseRationalRationalSearchEnvironment [ SKIPPED ] MarkovAutomatonCslModelCheckerTest/5.LtlSimple (0 ms) [----------] 6 tests from LraCtmcCslModelCheckerTest/0, where TypeParam = (anonymous namespace)::GBSparseGmmxxGmresIluEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/1, where TypeParam = (anonymous namespace)::GBJaniSparseGmmxxGmresIluEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/2, where TypeParam = (anonymous namespace)::GBJaniHybridCuddGmmxxGmresEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/4, where TypeParam = (anonymous namespace)::GBSparseEigenDGmresEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/5, where TypeParam = (anonymous namespace)::GBSparseEigenDoubleLUEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/6, where TypeParam = (anonymous namespace)::GBSparseNativeSorEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/7, where TypeParam = (anonymous namespace)::DistrSparseGmmxxGmresIluEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/8, where TypeParam = (anonymous namespace)::DistrSparseEigenDoubleLUEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/9, where TypeParam = (anonymous namespace)::ValueIterationSparseEnvironment [----------] 6 tests from LraCtmcCslModelCheckerTest/10, where TypeParam = (anonymous namespace)::SoundEnvironment [----------] 1 test from ExpectedVisitingTimesCtmcCslModelCheckerTest/0, where TypeParam = (anonymous namespace)::SparseGmmxxGmresIluEnvironment [----------] 1 test from ExpectedVisitingTimesCtmcCslModelCheckerTest/1, where TypeParam = (anonymous namespace)::SparseSoundEnvironment [----------] 1 test from ExpectedVisitingTimesCtmcCslModelCheckerTest/2, where TypeParam = (anonymous namespace)::SparseEigenRationalLuEnvironment [----------] 7 tests from CtmcCslModelCheckerTest/0, where TypeParam = (anonymous namespace)::SparseGmmxxGmresIluEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/0.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/0.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/1, where TypeParam = (anonymous namespace)::JaniSparseGmmxxGmresIluEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/1.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/1.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/2, where TypeParam = (anonymous namespace)::SparseEigenDGmresEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/2.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/2.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/3, where TypeParam = (anonymous namespace)::SparseEigenDoubleLUEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/3.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/3.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/4, where TypeParam = (anonymous namespace)::SparseNativeSorEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/4.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/4.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/5, where TypeParam = (anonymous namespace)::HybridCuddGmmxxGmresEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/5.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/5.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/6, where TypeParam = (anonymous namespace)::JaniHybridCuddGmmxxGmresEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/6.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/6.LtlProbabilitiesPolling (0 ms) [----------] 7 tests from CtmcCslModelCheckerTest/7, where TypeParam = (anonymous namespace)::HybridSylvanGmmxxGmresEnvironment [ SKIPPED ] CtmcCslModelCheckerTest/7.LtlProbabilitiesEmbedded (0 ms) [ SKIPPED ] CtmcCslModelCheckerTest/7.LtlProbabilitiesPolling (0 ms) [----------] 1 test from CtmcCslModelCheckerTest [----------] Global test environment tear-down 102 FAILED TESTS 13/36 Test #13: run-test-modelchecker-exploration ......***Failed 0.04 sec [----------] Global test environment tear-down 3 FAILED TESTS 14/36 Test #14: run-test-modelchecker-lexicographic .... Passed 0.03 sec [----------] 2 tests from SparseMdpCbMultiObjectiveModelCheckerTest [----------] 1 test from SparseMaCbMultiObjectiveModelCheckerTest [----------] 3 tests from SparseDtmcMultiDimensionalRewardUnfoldingTest [----------] Global test environment tear-down 12 FAILED TESTS 16/36 Test #16: run-test-modelchecker-reachability ..... Passed 0.12 sec [----------] 2 tests from LraDtmcPrctlModelCheckerTest/1, where TypeParam = (anonymous namespace)::GBEigenDoubleDGmresEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/2, where TypeParam = (anonymous namespace)::GBEigenRationalLUEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/3, where TypeParam = (anonymous namespace)::GBNativeSorEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/4, where TypeParam = (anonymous namespace)::GBNativeWalkerChaeEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/5, where TypeParam = (anonymous namespace)::DistrGmmxxDoubleGmresEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/6, where TypeParam = (anonymous namespace)::DistrEigenRationalLUEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/7, where TypeParam = (anonymous namespace)::DistrNativeWalkerChaeEnvironment [----------] 2 tests from LraDtmcPrctlModelCheckerTest/8, where TypeParam = (anonymous namespace)::ValueIterationEnvironment [----------] 3 tests from ExplicitDtmcPrctlModelCheckerTest [----------] 6 tests from DtmcPrctlModelCheckerTest/0, where TypeParam = (anonymous namespace)::SparseGmmxxGmresIluEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/0.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/0.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/1, where TypeParam = (anonymous namespace)::JaniSparseGmmxxGmresIluEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/1.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/1.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/2, where TypeParam = (anonymous namespace)::SparseGmmxxGmresDiagEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/2.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/2.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/3, where TypeParam = (anonymous namespace)::SparseGmmxxBicgstabIluEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/3.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/3.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/4, where TypeParam = (anonymous namespace)::SparseEigenDGmresEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/4.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/4.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/5, where TypeParam = (anonymous namespace)::SparseEigenDoubleLUEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/5.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/5.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/6, where TypeParam = (anonymous namespace)::SparseEigenRationalLUEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/6.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/6.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/7, where TypeParam = (anonymous namespace)::SparseRationalEliminationEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/7.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/7.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/8, where TypeParam = (anonymous namespace)::SparseNativeJacobiEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/8.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/8.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/9, where TypeParam = (anonymous namespace)::SparseNativeWalkerChaeEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/9.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/9.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/10, where TypeParam = (anonymous namespace)::SparseNativeSorEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/10.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/10.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/11, where TypeParam = (anonymous namespace)::SparseNativePowerEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/11.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/11.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/12, where TypeParam = (anonymous namespace)::SparseNativeSoundValueIterationEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/12.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/12.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/13, where TypeParam = (anonymous namespace)::SparseNativeOptimisticValueIterationEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/13.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/13.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/14, where TypeParam = (anonymous namespace)::SparseNativeIntervalIterationEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/14.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/14.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/15, where TypeParam = (anonymous namespace)::SparseNativeRationalSearchEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/15.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/15.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/16, where TypeParam = (anonymous namespace)::SparseTopologicalEigenLUEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/16.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/16.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/17, where TypeParam = (anonymous namespace)::HybridSylvanGmmxxGmresEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/17.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/17.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/18, where TypeParam = (anonymous namespace)::HybridCuddNativeJacobiEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/18.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/18.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/19, where TypeParam = (anonymous namespace)::HybridCuddNativeSoundValueIterationEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/19.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/19.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/20, where TypeParam = (anonymous namespace)::HybridSylvanNativeRationalSearchEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/20.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/20.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/21, where TypeParam = (anonymous namespace)::DdSylvanNativePowerEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/21.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/21.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/22, where TypeParam = (anonymous namespace)::JaniDdSylvanNativePowerEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/22.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/22.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/23, where TypeParam = (anonymous namespace)::DdCuddNativeJacobiEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/23.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/23.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 6 tests from DtmcPrctlModelCheckerTest/24, where TypeParam = (anonymous namespace)::DdSylvanRationalSearchEnvironment [ SKIPPED ] DtmcPrctlModelCheckerTest/24.LtlProbabilitiesDie (0 ms) [ SKIPPED ] DtmcPrctlModelCheckerTest/24.LtlProbabilitiesSynchronousLeader (0 ms) [----------] 1 test from DtmcPrctlModelCheckerTest [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/0, where TypeParam = (anonymous namespace)::GmmxxDoubleGmresEnvironment [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/1, where TypeParam = (anonymous namespace)::EigenDoubleDGmresEnvironment [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/2, where TypeParam = (anonymous namespace)::EigenRationalLUEnvironment [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/3, where TypeParam = (anonymous namespace)::NativeSorEnvironment [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/4, where TypeParam = (anonymous namespace)::NativePowerEnvironment [----------] 1 test from ConditionalDtmcPrctlModelCheckerTest/5, where TypeParam = (anonymous namespace)::NativeWalkerChaeEnvironment [----------] Global test environment tear-down 75 FAILED TESTS 18/36 Test #18: run-test-modelchecker-prctl-mdp ........***Failed 79.32 sec [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/0.ltl (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/0.ltlNondetChoice (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/0.ltlUnsat (0 ms) [----------] 6 tests from SchedulerGenerationMdpPrctlModelCheckerTest/1, where TypeParam = (anonymous namespace)::DoubleSoundViEnvironment [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/1.ltl (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/1.ltlNondetChoice (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/1.ltlUnsat (0 ms) [----------] 6 tests from SchedulerGenerationMdpPrctlModelCheckerTest/2, where TypeParam = (anonymous namespace)::DoublePIEnvironment [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/2.ltl (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/2.ltlNondetChoice (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/2.ltlUnsat (0 ms) [----------] 6 tests from SchedulerGenerationMdpPrctlModelCheckerTest/3, where TypeParam = (anonymous namespace)::RationalPIEnvironment [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/3.ltl (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/3.ltlNondetChoice (0 ms) [ SKIPPED ] SchedulerGenerationMdpPrctlModelCheckerTest/3.ltlUnsat (0 ms) [----------] 7 tests from RobustMDPModelCheckingTest [----------] 4 tests from QuantileQueryTest/0, where TypeParam = (anonymous namespace)::UnsoundEnvironment [----------] 4 tests from QuantileQueryTest/1, where TypeParam = (anonymous namespace)::SoundEnvironment [----------] 4 tests from QuantileQueryTest/2, where TypeParam = (anonymous namespace)::ExactEnvironment [----------] 9 tests from MdpPrctlModelCheckerTest/0, where TypeParam = (anonymous namespace)::SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/0.LtlProbabilitiesCoin (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/0.LtlDice (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/0.LtlCoinFlips (0 ms) [----------] 9 tests from MdpPrctlModelCheckerTest/1, where TypeParam = (anonymous namespace)::SparseDoubleValueIterationGmmxxRegularMultEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/1.LtlProbabilitiesCoin (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/1.LtlDice (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/1.LtlCoinFlips (0 ms) [----------] 9 tests from MdpPrctlModelCheckerTest/2, where TypeParam = (anonymous namespace)::SparseDoubleValueIterationNativeGaussSeidelMultEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/2.LtlProbabilitiesCoin (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/2.LtlDice (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/2.LtlCoinFlips (0 ms) [----------] 9 tests from MdpPrctlModelCheckerTest/3, where TypeParam = (anonymous namespace)::SparseDoubleValueIterationNativeRegularMultEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/3.LtlProbabilitiesCoin (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/3.LtlDice (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/3.LtlCoinFlips (0 ms) [----------] 9 tests from MdpPrctlModelCheckerTest/4, where TypeParam = (anonymous namespace)::JaniSparseDoubleValueIterationEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/4.LtlProbabilitiesCoin (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/4.LtlDice (0 ms) [ SKIPPED ] MdpPrctlModelCheckerTest/4.LtlCoinFlips (0 ms) [----------] 9 tests from MdpPrctlModelCheckerTest/5, where TypeParam = (anonymous namespace)::SparseDoubleIntervalIterationEnvironment [ SKIPPED ] MdpPrctlModelCheckerTest/5.LtlProbabilitiesCoin (0 ms) [----------] 2 tests from ExplicitMdpPrctlModelCheckerTest [----------] Global test environment tear-down |
|
Ok, so the problem is somehow that we execute tests that are not supported by your compilation. I really think that you should install z3. |
|
For better debugging the error you encountered, can you tell us what commit you are on? |
I am installing storm package in order to install stormpy, and I have some errors. I am following this instruction to install storm. Thank you so much for your help.
git clone -b stable https://github.com/moves-rwth/storm.git
export STORM_DIR=
cd $STORM_DIR
mkdir build
cd build
cmake ..
make
I have errors when execute
makeas below[ 1%] Built target l3pp_ext
[ 1%] Built target eigen_src
[ 1%] Performing configure step for 'glpk_ext'
CMake Error at /work/cs-grad/tuanle/xSRL/storm/build/resources/3rdparty/glpk-5.0/src/glpk_ext-stamp/glpk_ext-configure-RELEASE.cmake:49 (message):
Command failed: 1
'/work/cs-grad/tuanle/xSRL/storm/resources/3rdparty/glpk-5.0/configure' '--prefix=/work/cs-grad/tuanle/xSRL/storm/build/resources/3rdparty/glpk-5.0' '--libdir=/work/cs-grad/tuanle/xSRL/storm/build/resources/3rdparty/glpk-5.0/lib' 'CC=/usr/bin/cc' 'CXX=/usr/bin/c++'
See also
make[2]: *** [CMakeFiles/glpk_ext.dir/build.make:92: resources/3rdparty/glpk-5.0/src/glpk_ext-stamp/glpk_ext-configure] Error 1
make[1]: *** [CMakeFiles/Makefile2:767: CMakeFiles/glpk_ext.dir/all] Error 2
The output logs file of
storm/build/resources/3rdparty/glpk-5.0/src/glpk_ext-stamp/glpk_ext-configure-err.log
is
config.status: error: cannot find input file: `examples/Makefile.in'
the output of storm/build/resources/3rdparty/glpk-5.0/src/glpk_ext-stamp/glpk_ext-configure-out.log
is
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a thread-safe mkdir -p... /usr/bin/mkdir -p
checking for gawk... gawk
checking whether make sets $(MAKE)... yes
checking for gcc... /usr/bin/cc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether /usr/bin/cc accepts -g... yes
checking for /usr/bin/cc option to accept ISO C89... none needed
checking for style of include used by make... GNU
checking dependency style of /usr/bin/cc... gcc3
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking how to print strings... printf
checking for a sed that does not truncate output... /usr/bin/sed
checking for grep that handles long lines and -e... /usr/bin/grep
checking for egrep... /usr/bin/grep -E
checking for fgrep... /usr/bin/grep -F
checking for ld used by /usr/bin/cc... /usr/bin/ld
checking if the linker (/usr/bin/ld) is GNU ld... yes
checking for BSD- or MS-compatible name lister (nm)... /usr/bin/nm -B
checking the name lister (/usr/bin/nm -B) interface... BSD nm
checking whether ln -s works... yes
checking the maximum length of command line arguments... 1572864
checking whether the shell understands some XSI constructs... yes
checking whether the shell understands "+="... yes
checking how to convert x86_64-unknown-linux-gnu file names to x86_64-unknown-linux-gnu format... func_convert_file_noop
checking how to convert x86_64-unknown-linux-gnu file names to toolchain format... func_convert_file_noop
checking for /usr/bin/ld option to reload object files... -r
checking for objdump... objdump
checking how to recognize dependent libraries... pass_all
checking for dlltool... no
checking how to associate runtime and link libraries... printf %s\n
checking for ar... ar
checking for archiver @file support... @
checking for strip... strip
checking for ranlib... ranlib
checking command to parse /usr/bin/nm -B output from /usr/bin/cc object... ok
checking for sysroot... no
checking for mt... no
checking if : is a manifest tool... no
checking how to run the C preprocessor... /usr/bin/cc -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking for dlfcn.h... yes
checking for objdir... .libs
checking if /usr/bin/cc supports -fno-rtti -fno-exceptions... no
checking for /usr/bin/cc option to produce PIC... -fPIC -DPIC
checking if /usr/bin/cc PIC flag -fPIC -DPIC works... yes
checking if /usr/bin/cc static flag -static works... yes
checking if /usr/bin/cc supports -c -o file.o... yes
checking if /usr/bin/cc supports -c -o file.o... (cached) yes
checking whether the /usr/bin/cc linker (/usr/bin/ld -m elf_x86_64) supports shared libraries... yes
checking whether -lc should be explicitly linked in... no
checking dynamic linker characteristics... GNU/Linux ld.so
checking how to hardcode library paths into programs... immediate
checking whether stripping libraries is possible... yes
checking if libtool supports shared libraries... yes
checking whether to build shared libraries... yes
checking whether to build static libraries... yes
checking for exp in -lm... yes
checking sys/time.h usability... yes
checking sys/time.h presence... yes
checking for sys/time.h... yes
checking for gettimeofday... yes
checking whether to use GNU MP bignum library... no
checking whether to enable shared library support... no
checking whether to enable MathProg ODBC support... no
checking whether to enable MathProg MySQL support... no
checking whether to enable reentrancy support... yes
checking for thread local storage (TLS) class specifier... _Thread_local
checking if libtool needs -no-undefined flag to build shared libraries... no
checking that generated files are newer than configure... done
configure: creating ./config.status
config.status: creating src/Makefile
The text was updated successfully, but these errors were encountered: