Skip to content

Data-based synthesis crashes for variable with upper range 2147483647

Example:

plant X:
  disc int[2147483647 .. 2147483647] i;

  location l1:
    initial; marked;
end

Error:

com.github.javabdd.BDDException
	at com.github.javabdd.BDDDomain.<init>(BDDDomain.java:60)
	at com.github.javabdd.BDDFactory$1.<init>(BDDFactory.java:1630)
	at com.github.javabdd.BDDFactory.createDomain(BDDFactory.java:1630)
	at com.github.javabdd.BDDFactory.extDomain(BDDFactory.java:1706)
	at com.github.javabdd.BDDFactory.extDomain(BDDFactory.java:1673)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.createVarDomains(CifToBddConverter.java:1055)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.convertSpec(CifToBddConverter.java:514)
	at org.eclipse.escet.cif.bdd.conversion.CifToBddConverter.convert(CifToBddConverter.java:312)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.doSynthesis(CifDataSynthesisApp.java:261)
	at org.eclipse.escet.cif.datasynth.CifDataSynthesisApp.runInternal(CifDataSynthesisApp.java:174)
	at org.eclipse.escet.common.app.framework.Application.runApplication(Application.java:315)
	at org.eclipse.escet.common.app.framework.Application.run(Application.java:180)
	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:840)