Comments (6)
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.
Related Issues (20)
- man pages are behind
- --filter=action_labels
- Building LTSmin before installing Sylvan blocks ./configure from finding Sylvan afterwards
- Update LTSmin for newest version of Sylvan
- Tests fail when BuDDy is installed
- Bug in TGBA mode for LTL
- Build issue on NetBSD HOT 3
- Add examples to assets
- missing instructions for LTSmin installation for end-users HOT 1
- Installation instructions step by step
- Can ltsmin read the SMV format file? HOT 1
- Issues with LTL traces in MT context HOT 5
- make & make install error: multiple definitions for "rank" and "scc_stack" HOT 9
- how to install ltsmin? HOT 3
- Extracting Buchi Automata from PINS HOT 3
- question about example sokoban
- a question about PTS HOT 6
- Segmentation Fault in pnml2lts-mc HOT 4
- Question about LTL POR Provisos HOT 5
- (Possibly?) Unsound Partial Order Reduction
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from ltsmin.