Menu
▾
▴
Re: [Rodin-b-sharp-user] Proof Obligation(PO) missing? or PO simplified?
|
From: Laurent V. <lau...@sy...> - 2013-01-23 11:39:36
|
Dear Zheng, I have reproduced this issue on a simpler model and created a bug entry on SourceForge for this. Please have a look at [https://sourceforge.net/p/rodin-b-sharp/bugs/646/] for details. Normally, this should be fixed in Rodin 3.0. Anyhow, thank you very much for reporting this behavior. Cheers, Laurent. Le 23 janv. 2013 à 11:41, Laurent Voisin a écrit : > Dear Zheng, > > as Son wrote, there is tension between how far the POG goes in simplifying proof obligations and the confidence we can have in it. From a user point of view, the less trivial proof obligations, the better. But when we simplify / normalize too much proof obligations, it becomes increasingly difficult to decipher them and relate them to the model (this was a plague with Atelier B for instance, which required expect knowledge of the tools to understand some tricky proof obligations). > > From memory, there is one simplification case that Son has forgotten: a proof obligation is filtered out when the goal is a membership of a type (e.g., x ∈ Type). > > However, I agree with you that the example that you have pointed out look strange. For instance, in the INITIALISATION, we have a bunch of similar actions (simple assignments) but only one SIM proof obligation generated. One would expect to have either a SIM proof obligation for each action, or none at all. > > Cheers, > Laurent. > > Le 21 janv. 2013 à 14:44, ZHENG CHENG a écrit : > >> Dear Son, >> >> Thank you for your explanation. That makes perfect sense. >> >> Another minor issue is I find Rodin takes the goal (might be also the predicates in the hypothesis list) in the rewritten form. Therefore, I suspect it is likely the original goal in the hypothesis list, but the rewritten goal is not. As a result, some of the trivial case might not be filter out. >> >> For example, >> _______________________________ >> >> 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 >> Machine of interest: mode_m4 >> PO of interest: >> INITIALISATION/act5/SIM >> VOBC_transit_acceptance_passive/act4/SIM >> VOBC_special_transit_availability/act3/SIM >> VOBC_special_transit_one_cab_active/act3/SIM >> VOBC_special_do_nothing_availability/act3/SIM >> VOBC_special_states/act3/SIM >> The common characteristic of these PO is that the original goal contains in the hypothesis list (as the before-after predicate). but the rewritten goal is not. I guess my question is that would it be safe if I filter them out? Also, if the goal takes the form of "a=a", should it be considered as the goal is true, and be filtered out? >> _______________________________ >> >> Thank you very much. >> >> Regards, >> Zheng >> >> >> Message: 5 >> Date: Sun, 13 Jan 2013 22:09:54 +0000 >> From: "Hoang, Thai Son" <ht...@in...> >> Subject: Re: [Rodin-b-sharp-user] [Rodin-b-sharp-devel] Proof >> Obligation(PO) missing ? or PO simplified? >> To: Devel Rodin B-sharp <rod...@li...> >> Cc: "rod...@li... User" >> <rod...@li...> >> Message-ID: <E2B...@in...> >> Content-Type: text/plain; charset="Windows-1252" >> >> 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, 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. SALE $99.99 this month only -- learn more at: >> http://p.sf.net/sfu/learnmore_122412_______________________________________________ >> Rodin-b-sharp-user mailing list >> Rod...@li... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > ------------------------------------------------------------------------------ > Master Visual Studio, SharePoint, SQL, 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/learnnow-d2d_______________________________________________ > Rodin-b-sharp-user mailing list > Rod...@li... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user |