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;
}