Hello,
I used MRMC on a DTMC model to check a bounded until formula. Depending on the chosen time bounds and error_bound setting, it segfaulted on several occasions.
MRMC Version 1.4.1 built from source OS: Debian/testing on amd64 GCC: gcc version 4.4.3 20100108 (prerelease) (Debian 4.4.2-9)
Nevertheless it works well on 32 Bit OpenBSD -current with gcc 3.3.5
Is this behavior to be expected on 64 bit systems? Or is it maybe a gcc issue? Sorry if I missed something, but I did not find information about this on the webpage.
best regards Matthias