search

motib / erigone

Erigone Model Checker
8 stars 1 forks source link

Guided simulation StringIndexOutOfBoundsException #2

Open subchannel13 opened 5 years ago

subchannel13 commented 5 years ago

When running a guided simulation inside EUI on test.txt (renamed to .txt since GitHub doesn't allow uploading .pml) I get no steps in right hand window and there is an exception in command prompt:

Exception in thread "Thread-3" java.lang.StringIndexOutOfBoundsException: begin 104, end 92, length 117 at java.base/java.lang.String.checkBoundsBeginEnd(String.java:3410) at java.base/java.lang.String.substring(String.java:1883) at eui.Filter.extractBraces(Filter.java:394) at eui.Filter.storeVariables(Filter.java:457) at eui.Filter.filterSimulation(Filter.java:300) at eui.RunSpin$RunThread.run(RunSpin.java:138)

Unfortunately I don't have smaller example but I hope it's not too big.

motib commented 5 years ago

I was able to run a guided simulation, although I don't know if the output is OK, at least it didn't crash. Are you running a verification before a guided simulation? If you want to pursue this, please send screenshots of all the steps.

subchannel13 commented 5 years ago

Sorry for a delay on this, here are screenshots: eui-sc1-compile eui-sc2-safety eui-sc3-guided

Steps are: open file, compile button, safety button, guided button. There is no crash per se (probably worker thread crashes but the main thread survives) but there is no simulation result that demonstrates the counterexample. There is exception printout in command prompt. I don't know exactly where I've downloaded EUI from, probably from jSpin download section on Google Code. The program is started from run.bat.

motib commented 5 years ago

Hi Ivan, The verification run writes a "trail file", which is then read by the guided simulation to replay the scenario. There is some inconsistency between what is written and the expected input: some string is too long. It may be caused by something unexpected in the source program or possibly by a bug in Erigone/EUI. I suggest that you check exactly which line in the trail file is causing the crash and take it from there. Moti