search

fluentverification / stamina-storm

STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.
https://staminachecker.org
GNU General Public License v3.0
5 stars 2 forks source link

Exception in `StaminaModelBuilder::build()` #4

Closed ifndefJOSH closed 2 years ago

ifndefJOSH commented 3 years ago

Backtrace:

#0  __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1  0x00007ffff4fe1859 in __GI_abort () at abort.c:79
#2  0x00007ffff5267911 in ?? () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#3  0x00007ffff527338c in ?? () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#4  0x00007ffff52733f7 in std::terminate() () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#5  0x00007ffff52736a9 in __cxa_throw () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#6  0x00007ffff61a9bbc in storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >::assertValidityOfComponents(storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> > const&) const [clone .cold] () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#7  0x00007ffff6efd521 in storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >::Model(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#8  0x00007ffff6efd65d in storm::models::sparse::DeterministicModel<double, storm::models::sparse::StandardRewardModel<double> >::DeterministicModel(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#9  0x00007ffff70187bf in storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >::Ctmc(storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) ()
   from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#10 0x00007ffff702b385 in std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> > > storm::utility::builder::buildModelFromComponents<double, storm::models::sparse::StandardRewardModel<double> >(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) ()
   from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#11 0x00005555555aaea0 in stamina::StaminaModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::build (this=0x5555558cf110)
    at /path/to/stamina/stamina-cplusplus/src/StaminaModelBuilder.cpp:111
#12 0x00005555555da091 in stamina::StaminaModelChecker::modelCheckProperty (this=0x55555582c220, prop=..., modulesFile=...) at /path/to/stamina/stamina-cplusplus/src/StaminaModelChecker.cpp:157
#13 0x0000555555590c0a in stamina::Stamina::run (this=0x7fffffffd560) at /path/to/stamina/stamina-cplusplus/src/Stamina.cpp:53
#14 0x0000555555577301 in main (argc=3, argv=0x7fffffffdaa8) at /path/to/stamina/stamina-cplusplus/src/main.cpp:37
ifndefJOSH commented 3 years ago

My bad, was not a segfault...was just a std::exception. Was too fast writing this

ifndefJOSH commented 3 years ago

This exception is caused by the unfinished implementation of StaminaModelBuilder::buildMatrices(). This issue will be closed after that method is finished being implemented.

ifndefJOSH commented 2 years ago

There is another exception in this method, but this one is fixed.