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.

Reporter: Kate Habgood
E-mail: kate.habgood@altran.com

Environment

None

Attachments

2

Activity

Show:

Details

Assignee

Reporter

Created December 22, 2020 at 3:59 PM
Updated December 25, 2020 at 11:55 PM