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" <htson@...>
>> Subject: Re: [Rodin-b-sharp-user] [Rodin-b-sharp-devel] Proof
>> Obligation(PO) missing ? or PO simplified?
>> To: Devel Rodin B-sharp <rodin-b-sharp-devel@...>
>> Cc: "rodin-b-sharp-user@... User"
>> <rodin-b-sharp-user@...>
>> Message-ID: <E2BCE425-50DF-48ED-B3EA-50F5C899962A@...>
>> 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 <zcheng@...>>
>> 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
>> Rodin-b-sharp-user@...
>> 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
> Rodin-b-sharp-user@...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
|