Option to complete / Soundness possibly wrong result

[timKraeuter]

I was comparing the Soundness result of fbpmn with the one obtained from BProVe and got different results for the following model:

According to fbpmn this model is sound, while BProVe claims it is not since it does not fulfill the Option to Complete property.

Do you interpret Soundness/Option to complete differently, or why do both tools give a different result?

Thanks in advance!

The bpmn-file for the model can be found here (just remove .txt):
ects.bpmn.txt.

[pascalpoizat]

Hello @timKraeuter

Sorry I have not been notified of your issue (I may have missed something in the repo parameters). I will check it next week.

Pascal

[pascalpoizat]

Hello @timKraeuter,
I think it is a matter of fairness. At this level of abstraction (we do not have data to check whether the exclusive gateway will always loop or not, hence we have potentially an infinite set of traces) we make an assumption that, since the branch to attending the course is infinitely often reachable, it will not never be reached. Hence there is an option to complete. See details in Section 2.2.6 and 5.3, and Fig. 25 left, of our Information Systems paper. In BProve I think that they acknowledge that the path with an infinite series of <Checking ECTS - test - no> is possible, hence there is a possibility that the process does not terminate (even if there is one that it does). The difference is the interpretation of option to complete as a temporal logic formula. But I'll make more experiments in the next week to make it more clear (I have not used BProve for some time now). Sorry again for my late reply due to not receiving issue notifications (still not have found where to re-activate this).
Pascal

[timKraeuter]

Indeed, I think it is a matter of interpretation. I think both interpretations make sense, and was just confused about the disagreement.
In the original textbook about BPMN (Fundamentals of Business Process Management, Second Edition), they give two counterexamples for option to complete. One is a deadlock, the other a livelock which would both be detected by your tool and BProve.

Let me know if you find out anything new during testing otherwise, feel free to close this issue.