"becomes such as" operation causes unhandled loop exception

Description

Hello All,

please try "test" project that I have attached to this post. I am experiencing strange :| (becomes such that) behaviour, especially if I use unions in it.

After the first execution of "leave_B" event, animator fails to reset the animation and becomes strangely unresponsive. I can see unhandled loop exception thrown with the assertion message:

java.lang.AssertionError: Expected:
Bresponded Bresponded' Bresponded b
but was:
Bresponded b' Bresponded b
at de.prob.eventb.translator.internal.TranslationVisitor.translateAssignment(TranslationVisitor.java:799)

So in general, Rodin doesn't throw any errors and animator assertion fails.

Correct me if I am wrong, but :| should be able to handle any set theory operation? Including implication statement.

Thank you!

Gintautas

Environment

OSX 10.9
Rodin 2.8

Attachments

4

Gliffy Diagrams

Activity

Show:

GintautasS November 19, 2013 at 1:34 AM

You are right, Jens, they are actually valid projects. Something went terribly wrong with several Rodin installations on OSX 10.9

False alarm. Sorry

Jens Bendisposto November 11, 2013 at 8:46 PM

Both projects work for me. Have you tried cleaning them?

GintautasS November 7, 2013 at 2:30 AM
Edited

I have another example, with fully discharged POs that is expected to work nicely in ProB Animator.

Please find example project attached.

Problematic bit:
@act1 and act2 lines in leave_B event.
Substituting lines with commented out ones fixes ProB Animator issue.

Fixed

Details

Assignee

Reporter

Components

Fix versions

Affects versions

Priority

More fields

Created October 30, 2013 at 3:13 PM
Updated January 22, 2014 at 7:49 AM
Resolved January 22, 2014 at 7:49 AM