lddmc_relprod_union broken

utwente-fmt / sylvan

Multi-core Decision Diagram (BDD/LDD) implementation

Apache License 2.0

41 stars 8 forks source link

lddmc_relprod_union broken #6

Closed Meijuh closed 8 years ago

Meijuh commented 8 years ago

Running this commandline with LTSmin pnml2lts-sym model.pnml --vset=lddmc --next-union -rbs,ru --lace-workers=1 on instance #3 in http://mcc.lip6.fr/archives/GlobalResAllocation-pnml.tar.gz triggers the assertion sylvan_ldd.c:270: lddmc_makenode: Assertionvalue < mddnode_getvalue(((mddnode_t)llmsset_index_to_ptr(nodes, ifneq)))' failed`.

trolando commented 8 years ago

Kindly remind me what is the status of this issue.

Meijuh commented 8 years ago

It could be that this bug is fixed with this commit: https://github.com/utwente-fmt/sylvan/commit/32d0a29fcaab4c3d25677c73f06420119e3b8782.

Somebody should double check this.

trolando commented 8 years ago

Yeah, that commit fixed it as far as I know. Why it is not yet in ltsmin is a mystery, but I sent a mail about that. You could pull from my ltsmin "master"