Skip to content

CIF data-based synthesis crashes when using an initial node table size of 1

When running data-based synthesis with --bdd-table=1, the application crashes with a JavaBDD exception:

java.lang.IllegalArgumentException: bound must be positive
	at java.base/java.util.Random.nextInt(Random.java:557)
	at com.github.javabdd.JFactory.Random(JFactory.java:9791)
	at com.github.javabdd.JFactory.isMillerRabinPrime(JFactory.java:9858)
	at com.github.javabdd.JFactory.isPrime(JFactory.java:9881)
	at com.github.javabdd.JFactory.bdd_prime_gte(JFactory.java:9893)
	at com.github.javabdd.JFactory.bdd_init(JFactory.java:6794)
	at com.github.javabdd.JFactory.initialize(JFactory.java:398)
	at com.github.javabdd.JFactory.init(JFactory.java:67)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.createFactory(CifToBddConverter.java:318)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesis.computeControlledSystem(CifDataSynthesis.java:173)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesis.doSynthesisOnSpec(CifDataSynthesis.java:107)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.doSynthesis(CifDataSynthesisApp.java:207)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.runInternal(CifDataSynthesisApp.java:172)
	at org.eclipse.escet.common.app.framework.Application.runApplication(Application.java:316)
	at org.eclipse.escet.common.app.framework.Application.run(Application.java:181)
	at org.eclipse.escet.common.eclipse.ui.BaseFileCommandHandler.run(BaseFileCommandHandler.java:261)
	at org.eclipse.escet.common.eclipse.ui.BaseFileCommandHandler$1.run(BaseFileCommandHandler.java:102)
	at java.base/java.lang.Thread.run(Thread.java:1583)

It seems that, during initialization of JavaBDD (i.e., bdd_init), actual node table size is determined by searching for the next prime number that's greater than or equal to the user-specified initial table size. Which in this case is 1. The search procedure starts by calling, isPrime(1) which in turn calls isMillerRabinPrime(1), to determine whether 1 is a prime number. However, that method calls Random(1 - 1), i.e., Random(0), which fails since 0 is not positive.

I think the issue can easily be fixed by adding the following condition to JFactory#isPrime(int src) (I haven't tested this):

if (src == 1) {
	return false;
}