ProB for Rodin should support theorems in guards

Description

theorems in guards are currently ignored.
They should be at least shown in the State view under the "guards" section.
We should also examine whether they should be used for multi-level refinement and or cbc-refinement checking.

Below is a minimal example (Camille syntax).

machine ThmInGuard

variables x

invariants
@inv1 x ∈ ℤ

events
event INITIALISATION
then
@act1 x ≔ 0
end

event inc
where
@grd1 x∈ℕ
theorem @grd2 x≥0
then
@act1 x ≔ x + 1
end
end

Environment

None

Gliffy Diagrams

Activity

Show:

Jenkins Build Server July 16, 2013 at 8:11 AM

SUCCESS: Integrated in

ProB_Tests_Linux64 #6808
support theorem in guards in evaluation view + when loading proof info () (leuschel: rev 7ca66b70f53098ae5790099ead6a1abadbf7728e)

  • src/bvisual2.pl

  • src/bmachine.pl

Jenkins Build Server April 18, 2013 at 8:00 PM

Integrated in

ProB_Tests_Linux32 #133
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)

Result = SUCCESS
leuschel :
Files :

  • src/bvisual2.pl

  • src/bmachine.pl

Jenkins Build Server April 18, 2013 at 7:49 PM

Integrated in

ProB_Tests_Leopard64 #125
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)

Result = SUCCESS
leuschel :
Files :

  • src/bmachine.pl

  • src/bvisual2.pl

Jenkins Build Server April 18, 2013 at 6:41 PM

Integrated in

ProB_Tests_Windows #331
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)

Result = SUCCESS
leuschel :
Files :

  • src/bmachine.pl

  • src/bvisual2.pl

Michael Leuschel April 18, 2013 at 10:07 AM

theorems (in guards) now appears in the ProB for Rodin state view and the ProB Tcl/Tk Evaluation view

Fixed

Details

Assignee

Reporter

Priority

Created April 18, 2013 at 8:14 AM
Updated January 22, 2014 at 7:53 AM
Resolved January 22, 2014 at 7:53 AM