You can subscribe to this list here.
2009 
_{Jan}
(10) 
_{Feb}
(57) 
_{Mar}
(16) 
_{Apr}
(15) 
_{May}
(31) 
_{Jun}
(17) 
_{Jul}
(10) 
_{Aug}
(18) 
_{Sep}
(20) 
_{Oct}
(31) 
_{Nov}
(6) 
_{Dec}
(7) 

2010 
_{Jan}
(21) 
_{Feb}
(40) 
_{Mar}
(35) 
_{Apr}
(14) 
_{May}
(21) 
_{Jun}
(6) 
_{Jul}
(33) 
_{Aug}
(97) 
_{Sep}
(55) 
_{Oct}
(37) 
_{Nov}
(35) 
_{Dec}
(23) 
2011 
_{Jan}
(9) 
_{Feb}
(9) 
_{Mar}
(57) 
_{Apr}
(21) 
_{May}
(4) 
_{Jun}
(6) 
_{Jul}
(12) 
_{Aug}
(13) 
_{Sep}
(18) 
_{Oct}
(9) 
_{Nov}
(11) 
_{Dec}
(3) 
2012 
_{Jan}
(45) 
_{Feb}
(18) 
_{Mar}
(18) 
_{Apr}
(14) 
_{May}
(11) 
_{Jun}
(14) 
_{Jul}
(3) 
_{Aug}
(6) 
_{Sep}
(2) 
_{Oct}
(16) 
_{Nov}
(31) 
_{Dec}
(10) 
2013 
_{Jan}
(29) 
_{Feb}
(7) 
_{Mar}
(21) 
_{Apr}
(52) 
_{May}
(32) 
_{Jun}
(8) 
_{Jul}
(9) 
_{Aug}
(9) 
_{Sep}
(7) 
_{Oct}
(22) 
_{Nov}
(12) 
_{Dec}

2014 
_{Jan}
(36) 
_{Feb}
(11) 
_{Mar}
(11) 
_{Apr}
(11) 
_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 



1

2

3

4

5

6

7

8
(1) 
9

10

11

12
(3) 
13
(4) 
14
(2) 
15

16

17

18
(1) 
19
(4) 
20
(1) 
21
(5) 
22
(2) 
23
(3) 
24
(2) 
25

26

27
(1) 
28

29

30

31



From: Stefan Hallerstede <stefan.hallerstede@wa...>  20130127 12:10:43

4th Rodin User and Developer Workshop, June 1011, 2013, Turku, Finland http://wiki.eventb.org/index.php/Rodin_Workshop_2013 EventB is a formal method for systemlevel modelling and analysis. The Rodin Platform is an Eclipsebased toolset for EventB that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plugins. A range of plugins have already been developed including ones that support animation, model checking and UMLB. Preceding Rodin User and Developer Workshops were held at the University of Southampton, the University of Dusseldorf and the University of ParisEst Creteil. The fourth workshop will be collocated with the conference iFM 2013: http://www.it.abo.fi/iFM2013/ While much of the development and use of Rodin takes place within EU FP7 Projects (RODIN, DEPLOY, ADVANCE), there is a growing group of users and plugin developers outside these projects. The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of ongoing tool developments. For plugin developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort. The format will be presentations together with plenty of time for discussion. On day 1 in the morning a Demonstrator and Developer Tutorial will be held while the remaining 1 1/2 days will be devoted to tool usage and tool developments. If you are interested in giving a presentation at the Rodin workshop or have a plugin to demonstrate, send a short abstract (1 or 2 pages PDF) to rodin@... by 11 April 2013. Indicate whether it is a tool usage or tool development presentation. Plugin presentations may be about existing developments or planned future developments. We will endeavour to accommodate all submissions that are clearly relevant to Rodin and EventB. Organisers Michael Butler, University of Southampton Stefan Hallerstede, Aarhus University Thierry Lecomte, ClearSy Michael Leuschel, University of Düsseldorf Alexander Romanovsky, University of Newcastle Laurent Voisin, Systerel Marina Walden, Aabo Akademi 
From: Daniel Plagge <plagge@cs...>  20130124 21:24:47

Hello Aymerick, the theory plugin has support for the transitive closure. But ProB does not handle theories yet. It is planned that ProB will support them in the near future. Until then you have to stick with classical B or to do without ProB. :( Best regards Daniel Am 24.01.2013 21:36, schrieb Aymerick Savary: > Hello, > > In B models I use the closure function with ProB but i can't with Rosin. Is there an easy way to make it work? > > Aymerick Savary >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > http://p.sf.net/sfu/learnnowd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Aymerick Savary <aymerick.savary@gm...>  20130124 20:37:12

Hello, In B models I use the closure function with ProB but i can't with Rosin. Is there an easy way to make it work? Aymerick Savary 
From: Luiz Lemos Junior <lclemos@in...>  20130123 12:32:35

Dear Sirs, My name is Luiz Lemos Junior, I am a Master's student in Computer Science at Federal University of Pelotas, working with Rodin platform for EventB. I have been looking for some material about the implemented tatics and rules in Rodin's external provers (PP, newPP, ML, AtelierB). I have found the (Atelier B) interactive prover reference/user manuals and the paper Click’n Prove Interactive Proofs Within Set Theory (among others), but I would like to find anything about the proof procedure that was implemented (tatics and rules that are applied). Please, could you indicate me some references or material about that? Thanks for information. Regards, Luiz Lemos Jr. 
From: Laurent Voisin <laurent.voisin@sy...>  20130123 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/rodinbsharp/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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 beforeafter 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: [Rodinbsharpuser] [Rodinbsharpdevel] Proof >> Obligation(PO) missing ? or PO simplified? >> To: Devel Rodin Bsharp <rodinbsharpdevel@...> >> Cc: "rodinbsharpuser@... User" >> <rodinbsharpuser@...> >> MessageID: <E2BCE42550DF48EDB3EA50F5C899962A@...> >> ContentType: text/plain; charset="Windows1252" >> >> 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 EventB 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@...<mailto: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.eventb.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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 stepbystep video tutorials by Microsoft >> MVPs and experts. SALE $99.99 this month only  learn more at: >> http://p.sf.net/sfu/learnmore_122412_______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > http://p.sf.net/sfu/learnnowd2d_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20130123 10:42:17

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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 beforeafter 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: [Rodinbsharpuser] [Rodinbsharpdevel] Proof > Obligation(PO) missing ? or PO simplified? > To: Devel Rodin Bsharp <rodinbsharpdevel@...> > Cc: "rodinbsharpuser@... User" > <rodinbsharpuser@...> > MessageID: <E2BCE42550DF48EDB3EA50F5C899962A@...> > ContentType: text/plain; charset="Windows1252" > > 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 EventB 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@...<mailto: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.eventb.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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 stepbystep video tutorials by Microsoft > MVPs and experts. SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122412_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Alexei Iliasov <alexei.iliasov@nc...>  20130122 19:39:30

22.01.2013 17:16, Thiago Carvalho de Sousa пишет: > Dear all, > > I´m modelling a directed graph as a relation of a set to itself. > "aa"," bb", "cc" and "dd" are nodes. So, I have: > > INVARIANTS > nodes : pow(VERTEX_SET) > graph : nodes<> nodes > > INITIALISATION > graph := {aa \mapsto bb, aa \mapsto cc, bb \mapsto dd, cc \mapsto dd, > dd \mapsto aa, dd \mapsto bb} > > I´d like to detect cycles in this graph. Is there any simple way to > check this? Maybe using ProB? Any suggestion? add theorem (or axiom if you rely on prob): not # z . z <: dom(graph) & {} <<: z & c <: graph[z] should be easy to check with prob or smt plugin > Thanks in advance, > > Thiago > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > http://p.sf.net/sfu/learnnowd2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Thiago Carvalho de Sousa <thiagocsousa@gm...>  20130122 17:16:31

Dear all, I´m modelling a directed graph as a relation of a set to itself. "aa"," bb", "cc" and "dd" are nodes. So, I have: INVARIANTS nodes : pow(VERTEX_SET) graph : nodes <> nodes INITIALISATION graph := {aa \mapsto bb, aa \mapsto cc, bb \mapsto dd, cc \mapsto dd, dd \mapsto aa, dd \mapsto bb} I´d like to detect cycles in this graph. Is there any simple way to check this? Maybe using ProB? Any suggestion? Thanks in advance, Thiago 
From: Hoang, Thai Son <htson@in...>  20130121 14:17:55

Dear Zheng, On 21 Jan 2013, at 14:44, ZHENG CHENG <zcheng@...<mailto:zcheng@...>> wrote: 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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 beforeafter 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. I think you are right that these POs can be filtered out. The filtering in the POG is done after simplification hence these POs still remain. As you notice, the goal of these PO become "a = a". The POG does NOT filter out these POs. The idea (from what I understand) is that it filter out POs purely at the syntactic level, i.e., according the shape of the PO sequent. It does not look inside the goal or the hypotheses. Otherwise, the behaviour of the POG might become unpredictable and quite difficult to trace if a PO is missing. Cheers, Son 
From: ZHENG CHENG <zcheng@cs...>  20130121 13:45:06

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 OnBoard Controller for Trains< http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 beforeafter 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: [Rodinbsharpuser] [Rodinbsharpdevel] Proof Obligation(PO) missing ? or PO simplified? To: Devel Rodin Bsharp <rodinbsharpdevel@...> Cc: "rodinbsharpuser@... User" <rodinbsharpuser@...> MessageID: <E2BCE42550DF48EDB3EA50F5C899962A@...> ContentType: text/plain; charset="Windows1252" 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 EventB 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@...<mailto: 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.eventb.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 OnBoard Controller for Trains< http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 
From: Dipak Chaudhari <dipakc@gm...>  20130121 10:38:08

You may also find the following papers useful. Hallerstede, S., and M. Leuschel. “Experiments in Program Verification Using EventB.” Formal Aspects of Computing 24, no. 1 (2012): 97–125. Hallerstede, Stefan. “Structured EventB Models and Proofs.” In Abstract State Machines, Alloy, B and Z, edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, and Steve Reeves, 5977:273–286. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2010. http://dx.doi.org/10.1007/9783642118111_21. Boström, P. “Creating Sequential Programs from EventB Models.” In Integrated Formal Methods, 74–88, 2010. http://www.springerlink.com/index/W087U6N4VM4135U0.pdf. Regards, Dipak On Mon, Jan 21, 2013 at 3:29 PM, Hoang, Thai Son <htson@...> wrote: > DO 
From: Hoang, Thai Son <htson@in...>  20130121 09:59:31

Dear Konstantin, On 19 Jan 2013, at 00:52, Konstantin Weitz <weitzkon@...> wrote: > In B, it is possible to write sequential code such as (The BBook p. 400) > > WHILE x > 0 DO > x := x  1 > END > > Is this syntax possible in EventB, if not, are there alternatives? EventB is more general purpose (and simpler) modelling method than B. Hence it is not only to model sequential programs, but also other type of systems, e.g., distributed one. There is no sequential code like WHILE loop in EventB. Instead, it can usually be modelled using two events: body WHEN x > 0 THEN x := x  1 END finish WHEN not(x > 0) THEN // do something after the loop END You can find more information about using EventB to model sequential programs from chapter 15 of JeanRaymond's EventB book. The slides for that chapter are available online. http://wiki.eventb.org/index.php/EventB_Language Cheers, Son 
From: Hoang, Thai Son <htson@in...>  20130121 09:53:01

Dear George, Attached is a development where I mimic the proof of induction. If you have any problem with the proving interface of Rodin, the following page from the Rodin Handbook will be quite useful. http://handbook.eventb.org/current/html/proving_perspective.html Cheers, Son On 19 Jan 2013, at 17:42, George Zaff <ggzaff@...<mailto:ggzaff@...>> wrote: Thanks that is very helpful. I have another question relating to induction: Out of interest, I was wondering whether it is possible to prove the axiom of induction on natural numbers using Rodin? Ive looked at the proof on the Wikipedia article: https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction However, I have been unable to carry out the proof in Rodin. 
From: <kimmo.varpaaniemi@ko...>  20130120 09:39:07

Hello, See the theorem "thm_Wiki_trick" in the EventB context "Results" in the EventB project "PowersOfTwo" that is available in the archive http://sourceforge.net/p/rodinbsharp/bugs/_discuss/thread/8454803b/9bdc/attachment/PowersOfTwo.zip where all proof obligations have got discharged as indicated by the EventB Explorer view in Rodin Platform. All items in the "Axioms" section are theorems indeed, so the proofs are at least as convincing as Rodin Platform. As indicated by the name of the project, the same section contains some theorems about powers of two. I created the project almost two years ago as a reaction to discussions where provability of such properties in Rodin Platform had been questioned. With best regards, Kimmo Varpaaniemi George Zaff [ggzaff@...] kirjoitti: > Thanks that is very helpful. > > I have another question relating to induction: Out of interest, I was > wondering whether it is possible to prove the axiom of induction on natural > numbers using Rodin? Ive looked at the proof on the Wikipedia article: > > https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction > > However, I have been unable to carry out the proof in Rodin. > > > Thanks, > George > > > On Sat, Jan 19, 2013 at 12:38 AM, Hoang, Thai Son <htson@...> wrote: > > > Dear George, > > Here is the wiki page for an example of performing a proof by induction > > http://wiki.eventb.org/index.php/Induction_proof > > In your case, for proving axm18, you can instantiate s in axm11 with {a  > > a'fromNat(toNat(a))=a}. > > Cheers, > > Son > > On 18 Jan 2013, at 20:11, George Zaff <ggzaff@...<mailto: > > ggzaff@...>> > > wrote: > > > > Hi all, > > > > Im new to Rodin/eventb and have been exploring the interactive proof > > system. I found myself stuck while trying to apply induction. > > > > In the following, I define a set of natural numbers, mappings to/from this > > set into the builtin set of natural numbers and show that it defines the > > same set. However, when attempting to show that the mappings are > > isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their > > proofs require the induction hypothesis. > > > > CONTEXT > > Nat : > > SETS > > Nat : > > CONSTANTS > > zero : > > suc : > > toNat : > > fromNat : > > S : > > AXIOMS > > axm1: zero Nat not theorem : > > axm2: suc Nat Nat not theorem : > > axm3: toNat Nat not theorem : > > axm4: toNat(0) = zero not theorem : > > axm5: n · n Ò toNat(n + 1) = suc(toNat(n)) not theorem : > > axm6: toNat(1) = suc(zero) theorem : > > axm7: fromNat Nat not theorem : > > axm8: fromNat(zero) = 0 not theorem : > > axm9: n · n Nat Ò fromNat(suc(n)) = fromNat(n) + 1 not > > theorem : > > axm10: fromNat(suc(zero)) = 1 theorem : > > axm11: s · s ' 0 s ' ( n · n s Ò n + 1 s) Ò s > > not theorem : > > axm12: n · n Ò n = 0 ( ( m · m ' n = m + 1) theorem : > > axm13: S = { n # n ' ( x · x Nat ' n = fromNat(x)) } not > > theorem : > > axm14: S theorem : > > axm15: 0 S theorem : > > axm16: s · s S Ò s + 1 S theorem : > > axm17: S theorem : > > axm18: n · n Ò fromNat(toNat(n)) = n theorem : > > axm19: x · x Nat Ò x = zero ( ( y · y Nat ' x = suc(y)) > > not theorem : > > axm20: x · x Nat Ò toNat(fromNat(x)) = x theorem : > > END > > > > > > A second small query I have is whether there is support for a type of all > > sets? E.g. it is possible to write something of the form: > > A , B , f , a , a' · A SET ' B SET ' f A B ' a A ' a' A ' a > > = a' Ò f(a) = f(a') > > > > Thanks, > > George > > > >  > > Master HTML5, CSS3, ASP.NET<http://ASP.NET>;, MVC, AJAX, Knockout.js, Web > > API and > > much more. Get web development skills now with LearnDevNow  > > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > > SALE $99.99 this month only  learn more at: > > > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > > > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122912 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Colin Snook cfs <cfs@ec...>  20130119 17:39:28

Dear All, We are pleased to announce a new release of the EventB Statemachines plugin (and updates to the supporting frameworks) Improvements include: 1) Support for 'disjunctive source states (2 transitions that elaborate the same event in the same statemchine). 2) Support for Final states in root level state machines 3) A new experimental translation involving data refinement of an enumeration (Suggested by Abdolbaghi Rezazadeh) 4) Simulataneous Animation of multiple state machine diagrams is now supported 5) Improved deletion command (now deletes associated diagram files and generated elements) 6) Layout refiner  preserves diagram layouts when making a refinement Thanks to Panos Tanelian and D Wang for contributing to these improvements If you already have the Statemachines plugin installed, please make sure you select all the available updates simultaneously (see screenshot) otherwise the installer will not be able to resolve the new dependencies with your existing versions. Colin 
From: George Zaff <ggzaff@gm...>  20130119 16:42:30

Thanks that is very helpful. I have another question relating to induction: Out of interest, I was wondering whether it is possible to prove the axiom of induction on natural numbers using Rodin? Ive looked at the proof on the Wikipedia article: https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction However, I have been unable to carry out the proof in Rodin. Thanks, George On Sat, Jan 19, 2013 at 12:38 AM, Hoang, Thai Son <htson@...> wrote: > Dear George, > Here is the wiki page for an example of performing a proof by induction > http://wiki.eventb.org/index.php/Induction_proof > In your case, for proving axm18, you can instantiate s in axm11 with {a  > a∈ℕ∧fromNat(toNat(a))=a}. > Cheers, > Son > On 18 Jan 2013, at 20:11, George Zaff <ggzaff@...<mailto: > ggzaff@...>> > wrote: > > Hi all, > > Im new to Rodin/eventb and have been exploring the interactive proof > system. I found myself stuck while trying to apply induction. > > In the following, I define a set of natural numbers, mappings to/from this > set into the builtin set of natural numbers and show that it defines the > same set. However, when attempting to show that the mappings are > isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their > proofs require the induction hypothesis. > > CONTEXT > Nat › > SETS > Nat › > CONSTANTS > zero › > suc › > toNat › > fromNat › > S › > AXIOMS > axm1: zero ∈ Nat not theorem › > axm2: suc ∈ Nat → Nat not theorem › > axm3: toNat ∈ ℕ → Nat not theorem › > axm4: toNat(0) = zero not theorem › > axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › > axm6: toNat(1) = suc(zero) theorem › > axm7: fromNat ∈ Nat → ℕ not theorem › > axm8: fromNat(zero) = 0 not theorem › > axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not > theorem › > axm10: fromNat(suc(zero)) = 1 theorem › > axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s > not theorem › > axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › > axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not > theorem › > axm14: S ⊆ ℕ theorem › > axm15: 0 ∈ S theorem › > axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › > axm17: ℕ ⊆ S theorem › > axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › > axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) > not theorem › > axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › > END > > > A second small query I have is whether there is support for a type of all > sets? E.g. it is possible to write something of the form: > ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a > = a' ⇒ f(a) = f(a') > > Thanks, > George > >  > Master HTML5, CSS3, ASP.NET<http://ASP.NET>;, MVC, AJAX, Knockout.js, Web > API and > much more. Get web development skills now with LearnDevNow  > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > SALE $99.99 this month only  learn more at: > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > 
From: Hoang, Thai Son <htson@in...>  20130119 00:38:18

Dear George, Here is the wiki page for an example of performing a proof by induction http://wiki.eventb.org/index.php/Induction_proof In your case, for proving axm18, you can instantiate s in axm11 with {a  a∈ℕ∧fromNat(toNat(a))=a}. Cheers, Son On 18 Jan 2013, at 20:11, George Zaff <ggzaff@...<mailto:ggzaff@...>> wrote: Hi all, Im new to Rodin/eventb and have been exploring the interactive proof system. I found myself stuck while trying to apply induction. In the following, I define a set of natural numbers, mappings to/from this set into the builtin set of natural numbers and show that it defines the same set. However, when attempting to show that the mappings are isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their proofs require the induction hypothesis. CONTEXT Nat › SETS Nat › CONSTANTS zero › suc › toNat › fromNat › S › AXIOMS axm1: zero ∈ Nat not theorem › axm2: suc ∈ Nat → Nat not theorem › axm3: toNat ∈ ℕ → Nat not theorem › axm4: toNat(0) = zero not theorem › axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › axm6: toNat(1) = suc(zero) theorem › axm7: fromNat ∈ Nat → ℕ not theorem › axm8: fromNat(zero) = 0 not theorem › axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not theorem › axm10: fromNat(suc(zero)) = 1 theorem › axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s not theorem › axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not theorem › axm14: S ⊆ ℕ theorem › axm15: 0 ∈ S theorem › axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › axm17: ℕ ⊆ S theorem › axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) not theorem › axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › END A second small query I have is whether there is support for a type of all sets? E.g. it is possible to write something of the form: ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a = a' ⇒ f(a) = f(a') Thanks, George  Master HTML5, CSS3, ASP.NET<http://ASP.NET>;, MVC, AJAX, Knockout.js, Web API and much more. Get web development skills now with LearnDevNow  350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only  learn more at: http://p.sf.net/sfu/learnmore_122812_______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Konstantin Weitz <weitzkon@cs...>  20130119 00:20:40

In B, it is possible to write sequential code such as (The BBook p. 400) WHILE x > 0 DO x := x  1 END Is this syntax possible in EventB, if not, are there alternatives? Regards, Konstantin Weitz 
From: George Zaff <ggzaff@gm...>  20130118 19:11:30

Hi all, Im new to Rodin/eventb and have been exploring the interactive proof system. I found myself stuck while trying to apply induction. In the following, I define a set of natural numbers, mappings to/from this set into the builtin set of natural numbers and show that it defines the same set. However, when attempting to show that the mappings are isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their proofs require the induction hypothesis. CONTEXT Nat › SETS Nat › CONSTANTS zero › suc › toNat › fromNat › S › AXIOMS axm1: zero ∈ Nat not theorem › axm2: suc ∈ Nat → Nat not theorem › axm3: toNat ∈ ℕ → Nat not theorem › axm4: toNat(0) = zero not theorem › axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › axm6: toNat(1) = suc(zero) theorem › axm7: fromNat ∈ Nat → ℕ not theorem › axm8: fromNat(zero) = 0 not theorem › axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not theorem › axm10: fromNat(suc(zero)) = 1 theorem › axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s not theorem › axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not theorem › axm14: S ⊆ ℕ theorem › axm15: 0 ∈ S theorem › axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › axm17: ℕ ⊆ S theorem › axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) not theorem › axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › END A second small query I have is whether there is support for a type of all sets? E.g. it is possible to write something of the form: ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a = a' ⇒ f(a) = f(a') Thanks, George 
From: Rodolfo Campos <camposer@gm...>  20130114 10:22:43

Ken, thank you very much. I already had that "cheatsheet" :) About the book, thank you for your offering, please send it to me. Best regards, Rodolfo. On Mon, Jan 14, 2013 at 1:35 AM, Ken Robinson <kenr@...> wrote: > Hi Rodolfo, > > I'm attaching a copy of a Concise Summary of EventB, which you might find > useful. This gives a summary of all the EventB notation in only 4 pages. > You will also find a copy of this on the EventB and Rodin Documentation > Wiki. > > I am also working on a book on EventB and am happy to send you a copy of > the most current version if you would like it. Just tell me. > > Cheers, > > Ken > > > > > On 13/01/2013, at 08:43 AM, Rodolfo Campos wrote: > > > Hi, > > > > I'm new to Rodin trying to make an exercise about a very simple bank > which allows clients to open accounts, deposit, withdraw and transfer. > Right now I'm stuck with a very annoying problem, the thing is I need to > make 2 assignments over the same set on an event, and the tool gives me the > following error: "Left hand sides of assignments must be disjoint sets of > variables". > > > > ... > > THEN > > accountBalances(accountWithdraw) ≔ accountBalances(accountWithdraw)  > amount > > accountBalances(accountDeposit) ≔ accountBalances(accountDeposit) + > amount > > > > Do you have any idea of how to solve this? You can find attached my > exercise so far (error on transfer event). Thanks in advance for your help. > > > > Regards, > > > > Rodolfo. > > > > > <BankBCC_1.zip> > > 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 stepbystep video tutorials by Microsoft > > MVPs and experts. SALE $99.99 this month only  learn more at: > > > http://p.sf.net/sfu/learnmore_122912_______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > > Ken Robinson > > School of Computer Science & Engineering > UNSW NSW 2052 > > CRICOS Provider No: 00098G > > This message is intended for the addressee named and may contain > confidential information. If you are not the intended recipient, > please delete it and notify the sender. Views expressed in this > message are those of the individual sender and are not necessarily > the views of UNSW. > > > 
From: Rodolfo Campos <camposer@gm...>  20130114 10:20:27

Thank you very much Son, finally we solved the problem just isolating the variable, making something like: a < 3/2 b <=> 2a < 3b As easy as that, again, thank you very much for your help. Regards, Rodolfo. On Sun, Jan 13, 2013 at 11:42 PM, Hoang, Thai Son <htson@...> wrote: > Hi Rodolfo, > I know that there are some push for having real numbers using the Theory > plugin in Rodin, but I do not know how far that work goes. > The best right now is to use context to define rational numbers, > operations and axioms about these operations. Below can be a starting point > CONTEXT Rational > SETS RATIONAL > CONSTANTS > Frac /* Constructing a rational number from 2 integers */ > Rmultiply /* Multiplication for rational numbers */ > AXIOMS > Frac : INT ** (INT \ {0}) > RATIONAL > Rmultiply : RATIONAL ** RATIONAL > RATIONAL > END > > It is not pretty, especially you will need to formulate a number of > axioms about rational before you can do some interesting proofs. > Cheers, > Son > > > On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...<mailto: > camposer@...>> > wrote: > > Hello again guys, > > Now I'm having troubles using fractional values, don't know how to resolve > things like 3/2 * K, because we're only able to use INT and NAT values, > what I resolved so far, is to replace the above formula by K + K/2, but as > you may notice this is rounding the numbers and loosing some precision, is > it possible to use real values or something similar? > > Thanks in advance, best regards, > > Rodolfo. > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > > http://p.sf.net/sfu/learnmore_123012_______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. ON SALE this month only  learn more at: > http://p.sf.net/sfu/learnmore_123012 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Hoang, Thai Son <htson@in...>  20130113 22:43:10

Hi Rodolfo, I know that there are some push for having real numbers using the Theory plugin in Rodin, but I do not know how far that work goes. The best right now is to use context to define rational numbers, operations and axioms about these operations. Below can be a starting point CONTEXT Rational SETS RATIONAL CONSTANTS Frac /* Constructing a rational number from 2 integers */ Rmultiply /* Multiplication for rational numbers */ AXIOMS Frac : INT ** (INT \ {0}) > RATIONAL Rmultiply : RATIONAL ** RATIONAL > RATIONAL END It is not pretty, especially you will need to formulate a number of axioms about rational before you can do some interesting proofs. Cheers, Son On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...<mailto:camposer@...>> wrote: Hello again guys, Now I'm having troubles using fractional values, don't know how to resolve things like 3/2 * K, because we're only able to use INT and NAT values, what I resolved so far, is to replace the above formula by K + K/2, but as you may notice this is rounding the numbers and loosing some precision, is it possible to use real values or something similar? Thanks in advance, best regards, Rodolfo.  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 stepbystep video tutorials by Microsoft MVPs and experts. ON SALE this month only  learn more at: http://p.sf.net/sfu/learnmore_123012_______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Hoang, Thai Son <htson@in...>  20130113 22:10:10

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 EventB 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@...<mailto: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.eventb.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 OnBoard Controller for Trains<http://deployeprints.ecs.soton.ac.uk/316/>; , developed by Wen Su, JeanRaymond 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 stepbystep video tutorials by Microsoft MVPs and experts. ON SALE this month only  learn more at: http://p.sf.net/sfu/learnmore_123012_______________________________________________ Rodinbsharpdevel mailing list Rodinbsharpdevel@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpdevel 
From: Rodolfo Campos <camposer@gm...>  20130113 17:12:09

Hello again guys, Now I'm having troubles using fractional values, don't know how to resolve things like 3/2 * K, because we're only able to use INT and NAT values, what I resolved so far, is to replace the above formula by K + K/2, but as you may notice this is rounding the numbers and loosing some precision, is it possible to use real values or something similar? Thanks in advance, best regards, Rodolfo. 
From: Rodolfo Campos <camposer@gm...>  20130113 15:07:52

Thank you very much Pagu and Son, what Pagu said did the trick for us. Really appreciate your help. Best regards, Rodolfo. On Sun, Jan 13, 2013 at 12:30 AM, Gechio Pagu <pagugechio@...> wrote: > Hi, > > I think your two assignments can be merged into the following action. > > accountBalances ≔ ({accountWithdraw, > accountDeposit}⩤accountBalances)∪{accountWithdraw↦accountBalances(accountWithdraw) > − amount}∪{accountDeposit↦accountBalances(accountDeposit) + amount} > > Regards, > Pagu. > > *From:* Rodolfo Campos <camposer@...> > *Sent:* Sunday, January 13, 2013 6:43 AM > *To:* rodinbsharpuser@... > *Subject:* [Rodinbsharpuser] Problem with 2 assignments over the same > set on an event  Left hand sides of assignments must be disjoint sets of > variables > > Hi, > > I'm new to Rodin trying to make an exercise about a very simple bank which > allows clients to open accounts, deposit, withdraw and transfer. Right now > I'm stuck with a very annoying problem, the thing is I need to make 2 > assignments over the same set on an event, and the tool gives me the > following error: "Left hand sides of assignments must be disjoint sets of > variables". > > ... > THEN > accountBalances(accountWithdraw) ≔ accountBalances(accountWithdraw)  > amount > accountBalances(accountDeposit) ≔ accountBalances(accountDeposit) + > amount > > Do you have any idea of how to solve this? You can find attached my > exercise so far (error on transfer event). Thanks in advance for your help. > > Regards, > > Rodolfo. > > >  > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122912 > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > 