Re: [Rodin-b-sharp-user] [Rodin-b-sharp-devel] Proof Obligation(PO) missing ? or PO simplified?

[Hoang, T. S. <ht...@in...>]

 Dear Zheng,
 (I also Cc the user mailing list since this might be relevant for Rodin Users).
 Regarding the Rodin Proof Obligation Generator (POG), first of all, all POs are generated more or less according to the Event-B book. Afterward, the POs are passed through some filters to filter out those that are "trivial".
 From the top of my head, the following are consider to be trivial (there might be more):
- The goal is "true"
- A hypothesis is "false"
- The goal is one of the hypothesis.

 For the example that you mentioned, below is my guessed explanation on why SIM PO is filtered out.
 The abstract event is as follows
  VOBC_special =
  WHEN … THEN
     …
     current_mode :: M
  END

  The concrete event  VOBC_special_stationary does not have any action that update variable current_mode, i.e. current_mode' = current_mode
  As a result the SIM proof obligation will be have the following goal "current_mode : M" (the POG does some clever rewriting already if the action is deterministic) which is the same as one of the invariant (inv2) in the hypotheses.
  Since the goal is in the hypotheses, the PO is filtered out. That's why the mentioned PO is not there.
 Best,
Son
On 13 Jan 2013, at 19:24, ZHENG CHENG <zc...@cs...<mailto:zc...@cs...>>
 wrote:

Dear All

My question is regarding the Proof Obligation(PO) simplification strategy in Rodin v2.7. More specifically, I developed a  plugin to generate a list of refinement PO of eventb program(let's call it Set A). The POs are generated according to the Rodin User’s Handbook v.2.7<http://handbook.event-b.org/current/html/generated_proof_obligations.html>. Then, I compare them with the refinement PO list generated from Rodin(Set B). I found Set B is a subset of Set A.

I agree some of the refinement POs in my list are indeed redundant. For example, if a guard of abstract event is contained by the guards of corresponding concrete event, then no GRD PO is needed. However, in one case study, I found a SIM PO that should be presented according to the handbook but somehow is absent from Rodin v2.7. Let me illustrate this scenario.

------------------
How to reproduce:
Event program: Vehicle On-Board Controller for Trains<http://deploy-eprints.ecs.soton.ac.uk/316/> , developed by Wen Su, Jean-Raymond Abrial, Runlei Huang and Huibiao Zhu
Abstract Machine: mode_m0
Abstract Event: VOBC_special
Abstract Action of interest: act3
Abstract Variable of interest: current_mode


Concrete Machine: mode_m1
Concrete Event: VOBC_special_stationary
Abstract Variable of interest is presented in the context: true

My understanding is that: since the abstract variable "current_mode" is also declared in the concrete machine, a SIM PO for the concrete event should be generated from "act3" of "VOBC_special" in "mode_m0". And such PO should fail to proof, because the concrete event did not ensure the behaviour of the abstract one, i.e., "current_mode" is not given a value in "M", and there is no clue(no guards or witnesses or invariant) in the context to guarantee/infer this. Therefore, I conclude that the refinement from mode_m0 to mode_m1 is inconsistent in their behaviour.


-------------------

So, I wonder is there are documentation for underlying PO simplification strategy for Rodin. and Could anybody confirm is this kind of PO being simplified or missing? Thank you very much.

Regards,
Zheng



------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET<http://ASP.NET>, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnmore_123012_______________________________________________
Rodin-b-sharp-devel mailing list
Rod...@li...
https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-devel