2009: 2010: 2011: 2012: 2013: Jan (10) Feb (57) Mar (16) Apr (15) May (31) Jun (17) Jul (10) Aug (18) Sep (20) Oct (31) Nov (6) Dec (7) Jan (21) Feb (40) Mar (35) Apr (14) May (21) Jun (6) Jul (33) Aug (97) Sep (55) Oct (37) Nov (35) Dec (23) Jan (9) Feb (9) Mar (57) Apr (21) May (4) Jun (6) Jul (12) Aug (13) Sep (18) Oct (9) Nov (11) Dec (3) Jan (45) Feb (18) Mar (18) Apr (14) May (11) Jun (14) Jul (3) Aug (6) Sep (2) Oct (16) Nov (31) Dec (10) Jan (29) Feb (7) Mar (21) Apr (52) May (32) Jun (8) Jul (9) Aug (9) Sep (7) Oct (22) Nov (12) Dec
 [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Konstantin Weitz - 2012-12-06 10:34 Attachments: Message as HTML ```Hi, I followed the Celebrity Tutorial ( http://handbook.event-b.org/current/html/tut_celebrity_problem.html), and was wondering if there is a way to actually use the algorithm to solve a problem that I supplied. E.g. P = {0,1,2,3} c = 2 k = {(0|->2),(0|->3),(1|->2),(3|->2),(3|->0)} I tried ProB, but from my understanding it only suggests a couple of setups, but doesn't allow me to specify my own. Thanks, Konstantin Weitz ```

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Daniel Plagge - 2012-12-06 11:06 Attachments: Message as HTML ```Hello Konstantin, one way to provide example data is to create a new context which extends the original context and defines your problem. Then modify the "sees" clause of the model you want to animate to use your new context instead of the original. After animation, you can undo the changes to the "sees" clause. Concrete for Celebrity_0 this would mean: Create a context "example1" with context example1 extends Celebrity_c0 axioms @ex1 P = {0,1,2,3} @ex2 c = 2 @ex3 k = {(0?2),(0?3),(1?2),(3?2),(3?0)} end You can actually omit axiom @ex2, ProB is able to compute it just by the definition in "Celebrity_c0". In Celebrity_0 change machine Celebrity_0 sees Celebrity_c0 to machine Celebrity_0 sees Celebrity_c0 example1 or machine Celebrity_0 sees example1 In the first version you get a warning but it is easier to undo later. Just make sure to undo the changes to Celebrity_0 before you start proving. Having example data in your hypothesis can really make proving a lot more messy and might lead to non-discharged proof obligations later when you remove your example data. In my list of wishes for ProB is an option to include such an extra context for animation without the need to change the original models. The main problem is how to integrate such an option into the GUI. Implementing it into the logic below the GUI seems quite easy. Best regards Daniel Am 06.12.2012 11:04, schrieb Konstantin Weitz: > Hi, > > I followed the Celebrity Tutorial > (http://handbook.event-b.org/current/html/tut_celebrity_problem.html), > and was wondering if there is a way to actually use the algorithm to > solve a problem that I supplied. E.g. > > P = {0,1,2,3} > c = 2 > k = {(0|->2),(0|->3),(1|->2),(3|->2),(3|->0)} > > I tried ProB, but from my understanding it only suggests a couple of > setups, but doesn't allow me to specify my own. > > Thanks, > Konstantin Weitz > > > ------------------------------------------------------------------------------ > LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial > Remotely access PCs and mobile devices and provide instant support > Improve your efficiency, and focus on delivering more value-add services > Discover what IT Professionals Know. Rescue delivers > http://p.sf.net/sfu/logmein_12329d2d > > > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Leuschel-Family - 2012-12-06 11:08 Attachments: Message as HTML ```Hi Konstantin, In ProB you can simply add a new axiom to the contexts or define a new context which extends the existing one(s). For example, to animate Celebrity_1 I have just added the following context (with Camille): context Celebrity_c1_prob extends Celebrity_c1 axioms @prob_axiom P = {0,1,2,3} ∧ c = 2 ∧ k = {(0↦2),(0↦3),(1↦2),(3↦2),(3↦0)} end Then you can adapt the sees clause in Celebrity_1 to: sees Celebrity_c0_prob and animation should work as expected. In future we would like to provide custom animation settings in a separate ProB settings file, so that you don't have to modify existing models or contexts. Another solution is to export your model to ProB Classic and then load the generated Celebrity_1_mch.eventb file into ProB classic Tcl/Tk. Then choose "Animate -> Execute Operation ..." and then you can type in values for your constants (see screenshot). Best regards, Michael Leuschel On 6 Dec 2012, at 11:04, Konstantin Weitz wrote: > Hi, > > I followed the Celebrity Tutorial (http://handbook.event-b.org/current/html/tut_celebrity_problem.html), and was wondering if there is a way to actually use the algorithm to solve a problem that I supplied. E.g. > > P = {0,1,2,3} > c = 2 > k = {(0|->2),(0|->3),(1|->2),(3|->2),(3|->0)} > > I tried ProB, but from my understanding it only suggests a couple of setups, but doesn't allow me to specify my own. > > Thanks, > Konstantin Weitz > ------------------------------------------------------------------------------ > LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial > Remotely access PCs and mobile devices and provide instant support > Improve your efficiency, and focus on delivering more value-add services > Discover what IT Professionals Know. Rescue delivers > http://p.sf.net/sfu/logmein_12329d2d_______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Laurent Voisin - 2012-12-06 12:13 Attachments: Message as HTML ```Dear Daniel, I think that an alternative would be to create a refinement of the machine at the same time as the new context and to animate the refined machine. By default, when you create a refinement with the GUI, all events and variables are kept the same and you don't need to do any editing. The only thing you would do is change the SEES clause in the refinement and not touch the original model. Then, when you're happy with your animation, just remove the context and the refinement. Don't you think this would solve your issue ? Cheers, Laurent. Le 6 déc. 2012 à 12:06, Daniel Plagge a écrit : > Hello Konstantin, > > one way to provide example data is to create a new context which extends the original context and defines your problem. Then modify the "sees" clause of the model you want to animate to use your new context instead of the original. After animation, you can undo the changes to the "sees" clause. > > Concrete for Celebrity_0 this would mean: Create a context "example1" with > context example1 extends Celebrity_c0 > axioms > @ex1 P = {0,1,2,3} > @ex2 c = 2 > @ex3 k = {(0↦2),(0↦3),(1↦2),(3↦2),(3↦0)} > end > You can actually omit axiom @ex2, ProB is able to compute it just by the definition in "Celebrity_c0". > In Celebrity_0 change > machine Celebrity_0 sees Celebrity_c0 > to > machine Celebrity_0 sees Celebrity_c0 example1 > or > machine Celebrity_0 sees example1 > In the first version you get a warning but it is easier to undo later. > > Just make sure to undo the changes to Celebrity_0 before you start proving. Having example data in your hypothesis can really make proving a lot more messy and might lead to non-discharged proof obligations later when you remove your example data. > > In my list of wishes for ProB is an option to include such an extra context for animation without the need to change the original models. The main problem is how to integrate such an option into the GUI. Implementing it into the logic below the GUI seems quite easy. > > Best regards > Daniel > > > Am 06.12.2012 11:04, schrieb Konstantin Weitz: >> Hi, >> >> I followed the Celebrity Tutorial (http://handbook.event-b.org/current/html/tut_celebrity_problem.html), and was wondering if there is a way to actually use the algorithm to solve a problem that I supplied. E.g. >> >> P = {0,1,2,3} >> c = 2 >> k = {(0|->2),(0|->3),(1|->2),(3|->2),(3|->0)} >> >> I tried ProB, but from my understanding it only suggests a couple of setups, but doesn't allow me to specify my own. >> >> Thanks, >> Konstantin Weitz >> >> >> ------------------------------------------------------------------------------ >> LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial >> Remotely access PCs and mobile devices and provide instant support >> Improve your efficiency, and focus on delivering more value-add services >> Discover what IT Professionals Know. Rescue delivers >> http://p.sf.net/sfu/logmein_12329d2d >> >> >> _______________________________________________ >> Rodin-b-sharp-user mailing list >> Rodin-b-sharp-user@... >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > ------------------------------------------------------------------------------ > LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial > Remotely access PCs and mobile devices and provide instant support > Improve your efficiency, and focus on delivering more value-add services > Discover what IT Professionals Know. Rescue delivers > http://p.sf.net/sfu/logmein_12329d2d_______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Konstantin Weitz - 2012-12-06 11:15 Attachments: Message as HTML      Screen Shot 2012-12-06 at 12.06.29.png

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Daniel Plagge - 2012-12-07 09:38 Attachments: Message as HTML ```Hello Laurent, yes, you're right, that would have the advantage that the original model stays unchanged. On the downside, we may need one extra model for each machine that we want to animate. And if we actively develop a machine (adding or deleting events) we have to incorporate the changes in the animation model. So - still room for improvement of the ProB UI. :-) Best regards Daniel Am 06.12.2012 13:13, schrieb Laurent Voisin: > Dear Daniel, > > I think that an alternative would be to create a refinement of the > machine at the same time as the new context and to animate the refined > machine. By default, when you create a refinement with the GUI, all > events and variables are kept the same and you don't need to do any > editing. The only thing you would do is change the SEES clause in the > refinement and not touch the original model. > > Then, when you're happy with your animation, just remove the context > and the refinement. > > Don't you think this would solve your issue ? > > Cheers, > Laurent. > > Le 6 déc. 2012 à 12:06, Daniel Plagge a écrit : > >> Hello Konstantin, >> >> one way to provide example data is to create a new context which >> extends the original context and defines your problem. Then modify >> the "sees" clause of the model you want to animate to use your new >> context instead of the original. After animation, you can undo the >> changes to the "sees" clause. >> >> Concrete for Celebrity_0 this would mean: Create a context "example1" >> with >> >> context example1 extends Celebrity_c0 >> axioms >> @ex1 P = {0,1,2,3} >> @ex2 c = 2 >> @ex3 k = {(0↦2),(0↦3),(1↦2),(3↦2),(3↦0)} >> end >> >> You can actually omit axiom @ex2, ProB is able to compute it just by >> the definition in "Celebrity_c0". >> In Celebrity_0 change >> >> machine Celebrity_0 sees Celebrity_c0 >> >> to >> >> machine Celebrity_0 sees Celebrity_c0 example1 >> >> or >> >> machine Celebrity_0 sees example1 >> >> In the first version you get a warning but it is easier to undo later. >> >> Just make sure to undo the changes to Celebrity_0 before you start >> proving. Having example data in your hypothesis can really make >> proving a lot more messy and might lead to non-discharged proof >> obligations later when you remove your example data. >> >> In my list of wishes for ProB is an option to include such an extra >> context for animation without the need to change the original models. >> The main problem is how to integrate such an option into the GUI. >> Implementing it into the logic below the GUI seems quite easy. >> >> Best regards >> Daniel >> >> >> Am 06.12.2012 11:04, schrieb Konstantin Weitz: >>> Hi, >>> >>> I followed the Celebrity Tutorial >>> (http://handbook.event-b.org/current/html/tut_celebrity_problem.html), >>> and was wondering if there is a way to actually use the algorithm to >>> solve a problem that I supplied. E.g. >>> >>> P = {0,1,2,3} >>> c = 2 >>> k = {(0|->2),(0|->3),(1|->2),(3|->2),(3|->0)} >>> >>> I tried ProB, but from my understanding it only suggests a couple of >>> setups, but doesn't allow me to specify my own. >>> >>> Thanks, >>> Konstantin Weitz >>> >>> >>> ------------------------------------------------------------------------------ >>> LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial >>> Remotely access PCs and mobile devices and provide instant support >>> Improve your efficiency, and focus on delivering more value-add services >>> Discover what IT Professionals Know. Rescue delivers >>> http://p.sf.net/sfu/logmein_12329d2d >>> >>> >>> _______________________________________________ >>> Rodin-b-sharp-user mailing list >>> Rodin-b-sharp-user@... >>> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user >> >> ------------------------------------------------------------------------------ >> LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial >> Remotely access PCs and mobile devices and provide instant support >> Improve your efficiency, and focus on delivering more value-add services >> Discover what IT Professionals Know. Rescue delivers >> http://p.sf.net/sfu/logmein_12329d2d_______________________________________________ >> Rodin-b-sharp-user mailing list >> Rodin-b-sharp-user@... >> >> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > ```

 Re: [Rodin-b-sharp-user] Animate Machine with Custom Setup From: Michael Leuschel - 2012-12-07 10:23 Attachments: Message as HTML ```Hi, On 7 Dec 2012, at 10:37, Daniel Plagge wrote: > > yes, you're right, that would have the advantage that the original model stays unchanged. > > On the downside, we may need one extra model for each machine that we want to animate. And if we actively develop a machine (adding or deleting events) we have to incorporate the changes in the animation model. So - still room for improvement of the ProB UI. :-) Or what would help here is an "extends" keyword in Event-B/Rodin at at the machine level, i.e., we could write: machine M1_ProB extends M1 sees C1_ProB end then the machine M1_ProB wouldn't have to be updated if events are added or removed from M1. Greetings, Michael ```