Non-exact calculation compiled without CADP

[kris7t]

I'm trying to run the latest DFTCalc (529c7fb1410fb2c68d79b61d4e131adece6c2e77) with the latest DFTRES (https://github.com/utwente-fmt/DFTRES/commit/bc69223915bf8a965519a50cb5dd2f1cb91a001b) and Storm 1.6.4 (https://github.com/moves-rwth/storm/commit/6f39d431a371a7739c98f2550e000cae55e5edb5).

When I run dftcald without the --exact flag, I get

commandline:warning:CADP mode not compiled in, enabling --exact

and Storm returns and exact solution. Thus, I can't get a floating-point result, even if I specify an error bound with -E.

Due to the large size of the models I want to analyse, I'd like run Storm with floating-point arithmetic.

It seems the warning is emitted in

https://github.com/utwente-fmt/dftcalc/blob/abaa25cade1a49c414d507c3b2831fb15a89a58a/dftcalc/dftcalc.cpp#L1139-L1144

and runExact is forced in

https://github.com/utwente-fmt/dftcalc/blob/abaa25cade1a49c414d507c3b2831fb15a89a58a/dftcalc/dftcalc.cpp#L870-L871

which subsequently passes --exact to Storm.

I removed latter lines above, and DFTCalc with Storm seems to produce correct floating-point solutions. Are there any pitfalls with this calculation approach? It would be nice if DFTCalc supported non-exact calculation without CADP out of the box.

[ennoruijters]

Thanks for the feedback,

Your suggested change should be safe. We're planning to drop CADP support entirely soon, at which point the --exact flag will lose its double meaning of non-CADP and Storm-exact.

The branch "feature/mixed-exactness" should also do what you are looking for (non-exact computation without CADP) as long as CADP is not compiled in. I'll merge that into master once I find the time to test it properly :)

[ennoruijters]

Fix merged into master: dftcalc now defaults to non-exact calls to Storm also for the non-CADP version.