I encountered a problem when trying to use ProB co...
Description
I encountered a problem when trying to use ProB command line to generate test cases for an Event-B machine animation exported to standalone ProB. I tried using the model-checker mode and the constraint-based test generation and encountered different error reports for both. I've used ProB to create test cases for other anime exported from the same model without encountering this issue.
I have attached the error reports we see for both test generation tools. The issues relate to the same anime.
I am not sure whether this is a limitation of the tools with respect to something my colleague or I have included in the Event-B model, or a bug. If it is a known limitation, or something we need to differently in the Event-B model, it would be very helpful to understand what this is. The machine in question animates and model-checks in Rodin.
Michael Leuschel
blah111b
I encountered a problem when trying to use ProB command line to generate test cases for an Event-B machine animation exported to standalone ProB. I tried using the model-checker mode and the constraint-based test generation and encountered different error reports for both. I've used ProB to create test cases for other anime exported from the same model without encountering this issue.
I have attached the error reports we see for both test generation tools. The issues relate to the same anime.
I am not sure whether this is a limitation of the tools with respect to something my colleague or I have included in the Event-B model, or a bug. If it is a known limitation, or something we need to differently in the Event-B model, it would be very helpful to understand what this is. The machine in question animates and model-checks in Rodin.
Reporter: Kate Habgood
E-mail: kate.habgood@altran.com