team
contact
software
publications
teaching
jobs
[ news | issues | download | license | notes | old ]
Mucke
News
The new source release version 0.4.6 is a port to gcc 4.1.3.
Switched to BSD license.
Issues
The current release forces the former flag '-ret' to be asserted all the time and fixes a bug in the rangify code. Now it is possible to specify bit access for enumeration access symbols inside of classes:
enum E { reg, green, blue };
class C { E a, b; };
bool f(C c) c.a = c.b;
bool g(C c) c.a[0] = c.b[0] & c.a[1] = c.b[1];
forall C c. f(c) <-> g(c);
This should actually produce the same BDD for both f and g. Finally we introduced a new flag '-df' which allows to divert the dump of a predicate to a file. The name of the file is the name of the predicate with a '.dump' suffix.
Download
Since Mucke is written in C++ and the language C++ compilers accept has been quite a moving target in the past, you are on your own when trying to compile Mucke with a recent C++ compiler.
License
We use a variant of a BSD style license, which allows the use of Mucke in any way you want, provided you acknowledge the work of the original author in an approriate way as detailed in the COPYRIGHT notice which comes with the sources.
Notes
As in former releases, Mucke is configured with the BDD library ABCD as default. During initialization ABCD tries to grab half of all the available memory. This may slow down the start up of Mucke quite a bit. To restrict the initial memory usage, you can generate a '.abcdbmanrc' file that contains a line saying 'MB 10' that tells 'abcdbman' to use only the given amount of memory, e.g. 10 MB in this case, initially.
You can also just give '-bman simplebman.so' or '-bman longbman.so' as commmand line options to Mucke. These options tell Mucke to use the BDD library BDDSimple respectively the BDD library of David Long instead of ABCD.