In default model
Editor.generateApproximation().click -> Editor.model.diff("THRES: y: 0,4,8, 15","THRES: y: 0,4,5,8, 15") -> Editor.generateApproximation().click ->Editor.properties.diff("low = y < 4","low = y < 5") -> Editor.runParameterSynthesis().click
results in error:
Missing threshold
Status Bar:
Started processing formula y < 5.0
java.lang.IllegalArgumentException: You have to use an exact threshold in propositions! Proposition: y < 5.0, Thresholds: Variable(name=y, range=(0.0, 15.0), thresholds=[0.0, 2.010804, 2.917167, 3.685474, 4.0, 5.564226, 6.290516, 7.082833, 8.0, 8.04922, 9.345738, 11.320528, 15.0], varPoints=null, equation=[1.0*Param(-1)Approx(0)[0.0, 2.010804, 2.917167, 3.685474, 5.564226, 6.290516, 7.082833, 8.04922, 9.345738, 11.320528, 15.0]{1.0, 0.98959, 0.936679, 0.821302, 0.369445, 0.24085, 0.149163, 0.084657, 0.041991, 0.01653, 0.004098}, -1.0Param(1)Var(1)])
at com.github.sybila.ode.generator.AbstractOdeFragment.validNodes(AbstractOdeFragment.kt:49)
at com.github.sybila.checker.ModelChecker.validNodes(ModelChecker.kt)
at com.github.sybila.checker.ModelChecker.verify(ModelChecker.kt:49)
at com.github.sybila.checker.ModelChecker.checkExistUntil(ModelChecker.kt:96)
at com.github.sybila.checker.ModelChecker.verify(ModelChecker.kt:56)
at com.github.sybila.biodivine.exe.MainKt.main(Main.kt:91)
You have to use an exact threshold in propositions! Proposition: y < 5.0, Thresholds: Variable(name=y, range=(0.0, 15.0), thresholds=[0.0, 2.010804, 2.917167, 3.685474, 4.0, 5.564226, 6.290516, 7.082833, 8.0, 8.04922, 9.345738, 11.320528, 15.0], varPoints=null, equation=[1.0Param(-1)Approx(0)[0.0, 2.010804, 2.917167, 3.685474, 5.564226, 6.290516, 7.082833, 8.04922, 9.345738, 11.320528, 15.0]{1.0, 0.98959, 0.936679, 0.821302, 0.369445, 0.24085, 0.149163, 0.084657, 0.041991, 0.01653, 0.004098}, -1.0Param(1)*Var(1)]) (java.lang.IllegalArgumentException)
but
Editor.model.diff("THRES: y: 0,4,8, 15","THRES: y: 0,4,5,8, 15") -> Editor.generateApproximation().click ->Editor.properties.diff("low = y < 4","low = y < 5") -> Editor.runParameterSynthesis().click
works fine