"becomes such as" operation causes unhandled loop exception
Description
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 AMEdited
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.
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