ProB Rodin: cannot animate machine m1 - export for ProB classic silently fails

Description

In the following project the latest version of ProB (nightly) for Rodin can animate m0 but animating m1 fails.
The event view remains empty, but there are no error messages.
There is an initial error message concerning the AnimB values which are missing (for both m0 and m1).
Also, exporting m1 generates just a file with "package" inside; no error messages are generated by the exporter.

Environment

None

Attachments

7

Gliffy Diagrams

Activity

Show:

Jenkins Build Server March 12, 2013 at 8:14 AM

Integrated in

ProB_eclipse_develop #765

Result = SUCCESS

Daniel Plagge March 11, 2013 at 10:21 AM

Fixed bug: Incorrect check if new implementations computes the same as the old implementation.

Sebastian Krings March 11, 2013 at 10:05 AM

I still get an Assertion error when animating refreshers_m1_mch. (see proof_obligations.zip)

Daniel Plagge March 11, 2013 at 6:26 AM

The problem was in the new implementation of the translation visitor which will be used to translate Rodin's AST into ProB's AST. Currently both (old and new implementation) translators are used and their results are compared to detect bugs like this one.

The problem that an AssertionError leads to a silent failure is not solved by this fix.

Jens Bendisposto March 10, 2013 at 3:20 PM

Definitely (see also ). Unfortunately it is a bit difficult to produce the right amount (i.e. one) of error messages if a problem occurs.

Fixed

Details

Assignee

Reporter

Priority

Created March 9, 2013 at 4:29 PM
Updated March 12, 2013 at 8:14 AM
Resolved March 11, 2013 at 10:21 AM