Symbolic back-end can not cope with ~> 10^380 states about ltsmin HOT 6 CLOSED

I like this issue :)

from ltsmin.

isn't this already solved with the bignum libraries?

from ltsmin.

There is "some" support for the bignum libraries. If I remember correctly, @Meijuh created some custom code for this. In Sylvan there is no native support for e.g. gmp, although very very recently I have implemented support for gmp rational numbers in MTBDDs, so perhaps I could use an MTBDD leaf and the Sylvan garbage collection framework thing for this too.

from ltsmin.

@trolando I don't think we need to use custom terminals for this.
The problem with this issue was that LTSmin would crash when a floating point representing infinity was converted to a bignum; bignums don't support infinity. So, in essence LTSmin could cope with more than 10^380 states, but LTSmin would just represent this as infinity. The way I fixed it is 3-fold:

• I changed the vset interface to put the number of states directly in a double, instead of bignum: Meijuh@cc2dfdd
• The above commit also adds an extra vset function to count precisely with bignums (vset_count_precise)
• I added a vset_ccount function with can count using long doubles. Of which implementations of the vset interface use two cache entries to store the 128 bit result. The commit is here: Meijuh@78b9a6f. Long doubles can store ~10^4000 states.

This issue can be closed when these changes are merged in this repo.

from ltsmin.

Note that storing large integers in long double leads to loss of precision, particularly if adding widely different scales together, you can get some severe drift in number of states reported with long double.
Basically getting the first 12 digits right (MCC asks for that precision) was not always possible in my experiments with long double, because the result is computed as sums and multiplications of these.

GMP is the way to go imho, it's a pretty small dependency (available basically everywhere) + it has a simple C or c++ API.

from ltsmin.

This issue is resolved by now.
The symbolic backend automatically switches to long doubles if necessary.
If you want to precisely count the number of states use the --precise flag. This uses the GMP library.

from ltsmin.