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}
(18) 
_{May}
(8) 
_{Jun}
(19) 
_{Jul}
(15) 
_{Aug}
(22) 
_{Sep}
(11) 
_{Oct}
(8) 
_{Nov}
(4) 
_{Dec}
(14) 
2015 
_{Jan}
(2) 
_{Feb}
(4) 
_{Mar}
(10) 
_{Apr}
(7) 
_{May}
(11) 
_{Jun}
(17) 
_{Jul}
(5) 
_{Aug}
(7) 
_{Sep}
(23) 
_{Oct}
(4) 
_{Nov}
(9) 
_{Dec}

From: Laurent Voisin <laurent.voisin@sy...>  20151112 13:07:43

Dear Alex, except that plugins are installed within Eclipse and are not directly executable. Although possible, I find it very unlikely that anybody tampers with the plugins to install malware. There are much easier ways to install malware from SourceForge downloads. Cheers, Laurent. > Le 11 nov. 2015 à 01:49, Alex C <immibis@...> a écrit : > > Downloaded plugins have the same ability to install malware as any other executable files. > > On Tue, Nov 10, 2015 at 10:57 PM, Laurent Voisin <laurent.voisin@... <mailto:laurent.voisin@...>> wrote: > Indeed, there is no way to check them. However, there is very little chance that this is an issue as the downloaded files are mere plugins encapsulated in a jar file. > >> Le 5 nov. 2015 à 23:42, Alex C <immibis@... <mailto:immibis@...>> a écrit : >> >> I don't see a way to verify the checksums when installing additional plugins from Help>Install New Software menu. >> >> On Thu, Nov 5, 2015 at 10:44 PM, Laurent Voisin <laurent.voisin@... <mailto:laurent.voisin@...>> wrote: >> Dear Alex, >> >> > Le 18 oct. 2015 à 05:49, Alex C <immibis@... <mailto:immibis@...>> a écrit : >> > >> > I was wondering if there were any plans to move Rodin off SourceForge. SourceForge have been known to insert malicious code into software downloads, and even if they don't seem to be currently targeting Rodin, it would be nice if I could install/update Rodin without worrying about that. >> >> We do not have any plans for moving out of SourceForge. In 10+ years, we have had a very good relationship with them. >> >> If you are afraid of the downloaded files to be tampered with (which is very unlikely in my opinion), you can double check the downloaded file with its MD5 sum on the Rodin wiki (which is not hosted by SourceForge). >> >> These sums are available from http://wiki.eventb.org/index.php/Rodin_Platform_3.2_Release_Notes#About <http://wiki.eventb.org/index.php/Rodin_Platform_3.2_Release_Notes#About>; >> >> Best Regards, >> Laurent. >> >> > > 
From: Thái Sơn Hoàng <t.hoang@so...>  20151110 15:36:48

(Apologies if you receive multiple copies of this announcement) The 6th Rodin User and Developer Workshop, 2324 May, 2016, Linz, Austria http://wiki.eventb.org/index.php/Rodin_Workshop_2016 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. The 6th Rodin workshop will be collocated with the ABZ 2016 Conference: http://www.cdcc.faw.jku.at/ABZ2016/ 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. 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@...(mailto:rodin@...) 18 April 2016. 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 Thai Son Hoang, University of Southampton Michael Leuschel, University of Düsseldorf Laurent Voisin, Systerel — Thai Son Hoang ECS, Faculty of Physical Sciences and Engineering University of Southampton Southampton, United Kingdom. SO17 1BJ Sent with Mail Pilot 
From: david streader <davidistreader@gm...>  20151105 17:51:54

Thanks very silly mistake n could indeed have been 0. On 5 November 2015 at 22:05, Laurent Voisin <laurent.voisin@...> wrote: > Dear David, > > if you have the hypothesis that "1 < n” as suggested by Michael, did you > install the Atelier B plugin? > > Without that latter plugin the automated prover of Rodin is rather weak. > > Cheers, > Laurent. > > Le 5 nov. 2015 à 00:57, david streader <davidistreader@...> a écrit > : > > Hi > I have installed the Theory plugin (in 3.2) and stated working through > the paper  tutorial on the Theory plugin. All working so far but in > discharging one of the proof obligations the tool can not prove that 1 is > an element of the set {1,2,3...n} OR "1:1..n" > > Not sure what to do at this point? > > And is there a library of available theories any where? > > regards david > > > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > >  David Streader Victoria University of Wellington 
From: Colin Snook cfs <cfs@ec...>  20151105 12:08:47

H David, Have you installed the AtelierB provers? Colin On 4 Nov 2015, at 23:57, david streader <davidistreader@...> wrote: > Hi > I have installed the Theory plugin (in 3.2) and stated working through the paper  tutorial on the Theory plugin. All working so far but in discharging one of the proof obligations the tool can not prove that 1 is an element of the set {1,2,3...n} OR "1:1..n" > > Not sure what to do at this point? > > And is there a library of available theories any where? > > regards david > > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20151105 09:59:53

Dear Yongwang, we still have a problem in the refresh of the statistics view / EventB Explorer. This is due to mismanaged concurrency in the core platform code. However, this is only a display issue and your proofs are not at risk. Cheers, Laurent. > Le 12 oct. 2015 à 14:26, 赵永望 <zhaoyongwang@...> a écrit : > > Dear All, > > When I use Rodin 3.2, I am always confused by the list of proof > obligations under a machine in the view of "EventB Explorer" and the > statistics view. I have finished 5 machines with more than 1000 proof > obligations. The numbers of total, auto, undischarged column in view > "Statistics" always change at times when I open Rodin. I try to Refresh > the project in the view of "EventB Explorer", the numbers also changes. > The proof obligations list under a machine sometimes has same problem. I > worry very much that the discharged proof obligations will disappear. > > How can I resolve this problem? > > Thanks. > > Yongwang > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20151105 09:44:51

Dear Alex, > Le 18 oct. 2015 à 05:49, Alex C <immibis@...> a écrit : > > I was wondering if there were any plans to move Rodin off SourceForge. SourceForge have been known to insert malicious code into software downloads, and even if they don't seem to be currently targeting Rodin, it would be nice if I could install/update Rodin without worrying about that. We do not have any plans for moving out of SourceForge. In 10+ years, we have had a very good relationship with them. If you are afraid of the downloaded files to be tampered with (which is very unlikely in my opinion), you can double check the downloaded file with its MD5 sum on the Rodin wiki (which is not hosted by SourceForge). These sums are available from http://wiki.eventb.org/index.php/Rodin_Platform_3.2_Release_Notes#About Best Regards, Laurent. 
From: Laurent Voisin <laurent.voisin@sy...>  20151105 09:25:07

Dear David, if you have the hypothesis that "1 < n” as suggested by Michael, did you install the Atelier B plugin? Without that latter plugin the automated prover of Rodin is rather weak. Cheers, Laurent. > Le 5 nov. 2015 à 00:57, david streader <davidistreader@...> a écrit : > > Hi > I have installed the Theory plugin (in 3.2) and stated working through the paper  tutorial on the Theory plugin. All working so far but in discharging one of the proof obligations the tool can not prove that 1 is an element of the set {1,2,3...n} OR "1:1..n" > > Not sure what to do at this point? > > And is there a library of available theories any where? > > regards david > > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Michael Leuschel <leuschel@cs...>  20151105 08:31:16

Hi David, Are you sure you have the predicate n>0 in your selected hypotheses ? > On 5 Nov 2015, at 00:57, david streader <davidistreader@...> wrote: > > > Not sure what to do at this point? Greetings, Michael 
From: david streader <davidistreader@gm...>  20151104 23:57:06

Hi I have installed the Theory plugin (in 3.2) and stated working through the paper  tutorial on the Theory plugin. All working so far but in discharging one of the proof obligations the tool can not prove that 1 is an element of the set {1,2,3...n} OR "1:1..n" Not sure what to do at this point? And is there a library of available theories any where? regards david 
From: Michael Leuschel <leuschel@cs...>  20151030 07:26:29

Hi Matt, ProB provides testcase generation features (http://www3.hhu.de/stups/prob/index.php/Test_Case_Generation <http://www3.hhu.de/stups/prob/index.php/Test_Case_Generation>;) for classical B and EventB. You can use modelchecking based and constraintbased generation. The features are unfortunately not available within Rodin, you have to export your model for ProB “classic” (http://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_Exporting <http://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_Exporting>;) and then either use the commandline version probcli or the Tcl/Tk version of ProB. A recent paper that uses this for EventB is for example: http://link.springer.com/chapter/10.1007%2F9783319229690_10 You may also want to have a look at the MBT Plugin http://wiki.eventb.org/index.php/MBT_plugin <http://wiki.eventb.org/index.php/MBT_plugin>; which uses ProB but adds additional algorithms and works in Rodin. Greetings, Michael > On 30 Oct 2015, at 03:15, Matt Stevens <Matt@...> wrote: > > What modelbased testing tools are available for use with EventB > models? Preferably free or available under an academic licence. > > Regards > Matt > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matt Stevens <M<att@st...>  20151030 02:44:54

What modelbased testing tools are available for use with EventB models? Preferably free or available under an academic licence. Regards Matt 
From: Alex C <immibis@gm...>  20151018 03:49:15

Hi all, I was wondering if there were any plans to move Rodin off SourceForge. SourceForge have been known to insert malicious code into software downloads, and even if they don't seem to be currently targeting Rodin, it would be nice if I could install/update Rodin without worrying about that. 
From: 赵永望 <zhaoyongwang@gm...>  20151012 12:21:35

Dear All, When I use Rodin 3.2, I am always confused by the list of proof obligations under a machine in the view of "EventB Explorer" and the statistics view. I have finished 5 machines with more than 1000 proof obligations. The numbers of total, auto, undischarged column in view "Statistics" always change at times when I open Rodin. I try to Refresh the project in the view of "EventB Explorer", the numbers also changes. The proof obligations list under a machine sometimes has same problem. I worry very much that the discharged proof obligations will disappear. How can I resolve this problem? Thanks. Yongwang 
From: ACKERMANN J G <32247060@my...>  20150928 19:52:06

Good evening, Prof. Abrial, Apologies for the very late reply. Thank you for the advice, it has served me well. I am, however, still curious to know if there is a pattern to using constants instead of 'direct definitions'. Kindest regards Jaco Ackermann ________________________________ From: JeanRaymond Abrial <jrabrial@...> Sent: 04 September 2015 11:38 To: ACKERMANN J G Cc: rodinbsharpuser@... Subject: Re: [Rodinbsharpuser] SMT CVC3 prover  interesting result Hi Jaco, You can prove it (almost) automatically as follows:  Have a tactic profile with the two elementary tactics: "remove all Membership/Inclusion in goal", "remove all Membership/Inclusion in hypotheses".  launch the proof  Instantiate the existentially quantified variable s in the goal with A**s The proof terminates. Best JeanRaymond On 02 Sep 2015, at 23:06, ACKERMANN J G <32247060@...<mailto:32247060@...>> wrote: Hi everyone, I have stumbled upon a very interesting result when attempting to prove the following theorem (for constants A oftype POW(INT) and B oftype POW(POW(INT)), i.e. A <: INT and B <: POW(INT)): A ** union(B) <: union({ x . x : B  A ** x }) I wasn't able to discover a proof, even though there may be a proof that relies on quantifier instantiation or some other interactive steps. What was interesting was that the introduction of the function PROD given by PROD : POW(INT) ** POW(INT) > POW(INT ** INT) !X, Y . X <: INT & Y <: INT => (PROD(X >Y) = X ** Y) and the restatement of the theorem: PROD(A > union(B)) <: union({ x . x : B  PROD(A > x) }) enables the SMT CVC3 prover to find a proof rapidly. I may of course have made some mistake. But if this is not the case, can anyone shed some light on why the CVC3 inference mechanism 'likes' this additional function so much? [The idea was taken from Van der Poll's doctoral work on OTTER, "Automated support for settheoretic specifications", 2000]. Thank you! Jaco Ackermann, South Africa  Monitor Your Dynamic Infrastructure at Any Scale With Datadog! Get realtime metrics from all of your servers, apps and tools in one place. SourceForge users  Click here to start your Free Trial of Datadog now! http://pubads.g.doubleclick.net/gampad/clk?id=241902991&iu=/4140_______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@...<mailto:Rodinbsharpuser@...> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Jason Keltz <jas@cs...>  20150922 15:36:48

Hi. Last year around this time, I was preparing a virtual machine for our Software Engineering students which included Rodin 3.1. I had a few problems because I didn't include the necessary 32 bit support in the VM. This time around, I've upgraded the OS in the VM to the latest CentOS 7.1, and Rodin to 3.2. On our standard CentOS 6.X systems, everything works fine with Rodin 3.2, but in the VM, I'm again having trouble. I don't see any unresolved 32 bit dependencies. For example, if I start Rodin 3.2 in the VM, create a new EventB project, then add an EventB component to the project, then if I click to the left of the green arrow, I do see "Add Variable". However, when I select the option, nothing happens. I did find the following in .metadata/.log: !SESSION 20150922 11:09:04.409  eclipse.buildId=unknown java.version=1.8.0_51 java.vendor=Oracle Corporation BootLoader constants: OS=linux, ARCH=x86_64, WS=gtk, NL=en_US Commandline arguments: os linux ws gtk arch x86_64 debug !ENTRY org.eclipse.ui 4 4 20150922 11:10:01.529 !MESSAGE Failed to execute item null !STACK 0 org.eclipse.core.commands.NotHandledException: There is no handler to execute for command fr.systerel.editor.addChild at org.eclipse.core.commands.Command.executeWithChecks(Command.java:512) at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:508) at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210) at org.eclipse.ui.internal.handlers.LegacyHandlerService.executeCommand(LegacyHandlerService.java:343) at org.eclipse.ui.menus.CommandContributionItem.handleWidgetSelection(CommandContributionItem.java:829) at org.eclipse.ui.menus.CommandContributionItem.access$21(CommandContributionItem.java:815) at org.eclipse.ui.menus.CommandContributionItem$5.handleEvent(CommandContributionItem.java:805) at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84) at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4454) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1388) at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3799) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3409) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1151) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1032) at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:148) at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:636) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:579) at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150) at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:135) at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:497) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:648) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:603) at org.eclipse.equinox.launcher.Main.run(Main.java:1465) at org.eclipse.equinox.launcher.Main.main(Main.java:1438) . . . Any help to get this working would be very much appreciated. Jason. 
From: Sam Pinkus <sgpinkus@gm...>  20150909 05:52:31

<html> <head> <meta content="text/html; charset=utf8" httpequiv="ContentType"> </head> <body text="#000000" bgcolor="#FFFFFF"> <div class="mozciteprefix">I see. Thank you. Yes I found Jens approach worked in my simple example. In terms of finiteness proofs, it seems the auto provers need you to specify some obvious things sometimes. For example in a more complicated model I had to specify `∀z·((x ▷ {z}) ⊆ x)` where `finite(x)` was proven to get `finite(x ▷ {z})`.<br> <br> Thanks again,<br> <br> Sam.<br> <br> On 09/07/2015 10:48 PM, Laurent Voisin wrote:<br> </div> <blockquote cite="mid:FC286BBB40AF49B6B6E17BC94BA1B404@..." type="cite"> <meta httpequiv="ContentType" content="text/html; charset=utf8"> Dear Sam, <div class=""><br class=""> </div> <div class="">in general, you have two ways to prove a finiteness result with the Rodin platform : either you give an upper bound of your set which you know to be finite (or for which finiteness is easier to prove) or you unfold the definition of finiteness (which will lead to a difficult manual proof). For the first case, the idea is to click on the finite keyword in the goal. You then obtain a list of applicable rules. Then enter the appropriate upper bound in the input area of the Proof Control, then select the appropriate rule.</div> <div class=""><br class=""> </div> <div class="">The difficulty for the automated prover is to find the appropriate upper bound, so that if you make it explicit in your model with some theorems (as Jens has explained), you have better chance that the automated prover notices it and use it directly.</div> <div class=""><br class=""> </div> <div class="">Cheers,</div> <div class="">Laurent.</div> <div class=""><br class=""> <div> <blockquote type="cite" class=""> <div class="">Le 4 sept. 2015 à 11:15, Sam Pinkus <<a mozdonotsend="true" href="mailto:sgpinkus@..." class="">sgpinkus@...</a>> a écrit :</div> <br class="Appleinterchangenewline"> <div class=""> <meta httpequiv="contenttype" content="text/html; charset=utf8" class=""> <div text="#000000" bgcolor="#FFFFFF" class=""> Hi,<br class=""> <br class=""> It seems given `x <: y & finite(y)` Rodin provers cant automatically prove `finite(x)`, let alone where we have is a some sort of relation, function, restriction/substraction related to x where the finiteness of said is obviously implied by finiteness of x. Is this right? Is there any general advice available on whats going on, why, and how to proceed manually? I know there are some threads about related finite() things not discharging when they should but I can't read these and understand why, and how to fix in general.<br class=""> <br class=""> As an example, the following machine is a cut down version of the situation I have in a more complicated machine I'm trying to write, where I noticed the issue. inv6 wont discharge. Note if I change the "theorems" to "not theorems" everythin discharges, but that is not fixing the issue.<br class=""> <br class=""> CONTEXT<br class=""> ctx ›<br class=""> SETS<br class=""> ⚬ FOO <br class=""> ⚬ BAH <br class=""> AXIOMS<br class=""> ⚬ axm2: finite(FOO) not theorem<br class=""> ⚬ axm3: finite(BAH) not theorem<br class=""> END<br class=""> <br class=""> MACHINE<br class=""> mchn ›<br class=""> SEES<br class=""> ⚬ ctx <br class=""> VARIABLES<br class=""> ⚬ f <br class=""> ⚬ g <br class=""> ⚬ x <br class=""> INVARIANTS<br class=""> ⚬ inv1: f ⊆ FOO not theorem<br class=""> ⚬ inv2: finite(f) theorem<br class=""> ⚬ inv3: g ⊆ BAH not theorem<br class=""> ⚬ inv4: finite(g) theorem<br class=""> ⚬ inv5: x ∈ f ⇸ g not theorem<br class=""> ⚬ inv6: finite(x) theorem<br class=""> EVENTS<br class=""> ⚬ INITIALISATION: not extended ordinary<br class=""> THEN<br class=""> ⚬ act1: f ≔ ∅<br class=""> ⚬ act2: g ≔ ∅<br class=""> ⚬ act3: x ≔ ∅<br class=""> END<br class=""> END<br class=""> <br class=""> Thanks,<br class=""> <br class=""> Sam.<br class=""> <br class=""> <div class="mozsignature"> <br class=""> <p style="color:#CCC; fontsize:small" class=""><strong class="">PGP</strong>: 0xA53455C1</p> </div> </div> <br class=""> _______________________________________________<br class=""> Rodinbsharpuser mailing list<br class=""> <a mozdonotsend="true" href="mailto:Rodinbsharpuser@..." class="">Rodinbsharpuser@...</a><br class=""> <a class="moztxtlinkfreetext" href="https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser">https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser</a><br class=""> </div> </blockquote> </div> <br class=""> </div> </blockquote> <br> <br> <div class="mozsignature"> <br> <p style="color:#CCC; fontsize:small"><strong>PGP</strong>: 0xA53455C1</p> </div> </body> </html> 
From: Laurent Voisin <laurent.voisin@sy...>  20150907 12:48:52

Dear Sam, in general, you have two ways to prove a finiteness result with the Rodin platform : either you give an upper bound of your set which you know to be finite (or for which finiteness is easier to prove) or you unfold the definition of finiteness (which will lead to a difficult manual proof). For the first case, the idea is to click on the finite keyword in the goal. You then obtain a list of applicable rules. Then enter the appropriate upper bound in the input area of the Proof Control, then select the appropriate rule. The difficulty for the automated prover is to find the appropriate upper bound, so that if you make it explicit in your model with some theorems (as Jens has explained), you have better chance that the automated prover notices it and use it directly. Cheers, Laurent. > Le 4 sept. 2015 à 11:15, Sam Pinkus <sgpinkus@...> a écrit : > > Hi, > > It seems given `x <: y & finite(y)` Rodin provers cant automatically prove `finite(x)`, let alone where we have is a some sort of relation, function, restriction/substraction related to x where the finiteness of said is obviously implied by finiteness of x. Is this right? Is there any general advice available on whats going on, why, and how to proceed manually? I know there are some threads about related finite() things not discharging when they should but I can't read these and understand why, and how to fix in general. > > As an example, the following machine is a cut down version of the situation I have in a more complicated machine I'm trying to write, where I noticed the issue. inv6 wont discharge. Note if I change the "theorems" to "not theorems" everythin discharges, but that is not fixing the issue. > > CONTEXT > ctx › > SETS > ⚬ FOO > ⚬ BAH > AXIOMS > ⚬ axm2: finite(FOO) not theorem > ⚬ axm3: finite(BAH) not theorem > END > > MACHINE > mchn › > SEES > ⚬ ctx > VARIABLES > ⚬ f > ⚬ g > ⚬ x > INVARIANTS > ⚬ inv1: f ⊆ FOO not theorem > ⚬ inv2: finite(f) theorem > ⚬ inv3: g ⊆ BAH not theorem > ⚬ inv4: finite(g) theorem > ⚬ inv5: x ∈ f ⇸ g not theorem > ⚬ inv6: finite(x) theorem > EVENTS > ⚬ INITIALISATION: not extended ordinary > THEN > ⚬ act1: f ≔ ∅ > ⚬ act2: g ≔ ∅ > ⚬ act3: x ≔ ∅ > END > END > > Thanks, > > Sam. > >  > PGP: 0xA53455C1 > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20150907 12:34:08

Dear Alex, > Le 7 sept. 2015 à 03:36, Alex C <immibis@...> a écrit : > > Hi. This is my first time posting to a Rodin mailing list, and I'm not sure if user or devel fits better. This is typically a problem with usage of the Rodin platform, hence the user mailing list applies. The devel mailing list is devoted to plain development (both core platform and plugins). > It seems that if the Generalized MP reasoner finds the goal in one of the hypotheses, it will replace it with ⊥. Yes, this is the case. > That is, if I have the goal "carOnCrossing=FALSE", and a hypothesis "carOnCrossing=FALSE ∨ pedestrianOnCrossing=FALSE", it will get replaced with "⊥ ∨ pedestrianOnCrossing=FALSE", then simplified to "pedestrianOnCrossing=FALSE". This doesn't seem to be logically sound. What's the rationale for this, or is it a bug? Although counterintuitive, this is logically sound in classical logic (but not in an intuitionistic logic). For your example, you could consider starting a proof by cases on your disjunction. You would then have to prove on the one hand “carOnCrossing=FALSE  carOnCrossing=FALSE” (which trivially holds) and on the other hand “pedestrianOnCrossing=FALSE  carOnCrossing=FALSE” which is what you are left after generalized MP and normalization. A similar argument can be used in the general case. If you have goal G, just add the hypothesis “G ∨ ¬G” with a cut, then start a proof by case on it. You will end up with “¬G” in hypothesis. > I'm using a version of Rodin built from source, due to concerns about SourceForge's adware injection program, but the problem couldn't have been caused by e.g. mismatched plugin versions, since the faulty logic is contained within one source file. > > Codewise, in the org.eventb.core.seqprover plugin, class org.eventb.internal.core.seqprover.eventbExtensions.genmp.GenMPC, the method extractSubstitutes calls addSubstitute for the goal (or each of its disjuncts), passing fromGoal=true. This calls either makeSubstitutes or makeSubstitutesL2, where the predicate is treated as being negated if fromGoal is true (isPos = !fromGoal). > ——————————————————————————————————————— If you look closely at the code, you will see in class AbstractGenMP some Java tags named @ProverRule. These refers to the specification of the prover rules available from http://wiki.eventb.org/index.php/Inference_Rules and that are implemented in the corresponding reasoner. These rules have been formally proved and reviewed for correctness. But as the process is human, it is possible that there is a mistake there (it has sometimes happened in the past). If you find such an issue, please report it on this mailing list. And in doubt, report it anyway: we prefer to address nonissues, rather than having some unknown hidden issues. Anyhow, thank you very much for having taken the time to write this very nice and documented report. Cheers, Laurent. 
From: Alex C <immibis@gm...>  20150907 01:36:52

Hi. This is my first time posting to a Rodin mailing list, and I'm not sure if user or devel fits better. It seems that if the Generalized MP reasoner finds the goal in one of the hypotheses, it will replace it with ⊥. That is, if I have the goal "carOnCrossing=FALSE", and a hypothesis "carOnCrossing=FALSE ∨ pedestrianOnCrossing=FALSE", it will get replaced with "⊥ ∨ pedestrianOnCrossing=FALSE", then simplified to "pedestrianOnCrossing=FALSE". This doesn't seem to be logically sound. What's the rationale for this, or is it a bug? I'm using a version of Rodin built from source, due to concerns about SourceForge's adware injection program, but the problem couldn't have been caused by e.g. mismatched plugin versions, since the faulty logic is contained within one source file. Codewise, in the org.eventb.core.seqprover plugin, class org.eventb.internal.core.seqprover.eventbExtensions.genmp.GenMPC, the method extractSubstitutes calls addSubstitute for the goal (or each of its disjuncts), passing fromGoal=true. This calls either makeSubstitutes or makeSubstitutesL2, where the predicate is treated as being negated if fromGoal is true (isPos = !fromGoal). 
From: Thái Sơn Hoàng <tshoang@us...>  20150906 17:29:46

Dear YuanFang, As an alternative to what Michael suggested, I see that the machine is "generic" in terms of the actual directions and the conflict relationship. As the result, one can prove it at a more abstract level (with some generic properties about CONFLICT). The abstract context is as follows: CONTEXT c0traffic_light › SETS LIGHTS › DIRECTION › CONSTANTS Red Green Amber CONFLICT AXIOMS axm1: partition(LIGHTS,{Red},{Green},{Amber}) not theorem › axm5: CONFLICT∈DIRECTION↔DIRECTION not theorem › axm6: CONFLICT = CONFLICT∼ not theorem › axm7: CONFLICT ∩ id = ∅ not theorem › END The machine is almost identical to what you have, I just put in some copy of the theorems in guards of ToGreen and ToAmber to help with the proofs. MACHINE m0traffic_light › SEES c0traffic_light VARIABLES light_dir Physical Unit: Inferred Physical Unit: › INVARIANTS inv1: light_dir∈DIRECTION→LIGHTS not theorem › inv11: ∀d·d∈DIRECTION ∧light_dir(d)∈{Green,Amber} ⇒ light_dir[CONFLICT[{d}]] = {Red} not theorem › EVENTS INITIALISATION: not extended ordinary › THEN act1: light_dir≔DIRECTION × {Red} › END ToRed: not extended ordinary › ANY dir › WHERE grd1: dir∈DIRECTION not theorem › grd2: light_dir(dir)= Amber not theorem › THEN act1: light_dir(dir)≔Red › END ToGreen: not extended ordinary › ANY dir › WHERE grd1: dir∈DIRECTION not theorem › grd2: light_dir(dir) = Red not theorem › grd7: light_dir[CONFLICT[{dir}]] = {Red} not theorem › thm1: CONFLICT ∩ id = ∅ theorem › thm2: CONFLICT = CONFLICT∼ theorem › THEN act1: light_dir(dir)≔Green › END ToAmber: not extended ordinary › ANY dir › WHERE grd1: dir∈DIRECTION not theorem › grd2: light_dir[{dir}] = {Green} not theorem › thm1: CONFLICT ∩ id = ∅ theorem › THEN act1: light_dir (dir)≔ Amber › END END There should be only one proof obligations remain (you might have to increase the timeout for AtelierB P0). The remaining PO (for ToGreen) with one proof branch undischarged can be finished with a case distinction as in the attachment. The advantage of this approach is that the machine is generic, i.e., your proof will guarantee that it works with any instantiation of traffic lights, e.g., 2way, 5way, etc. What left (very important) is to ensure that the instantiation of DIRECTIONS and CONFLICT is correct. In this way, ProB will help you to check that in a flash. For example, the instantiation for 5way traffic can be done using context extension. CONTEXT c1five_way › EXTENDS c0traffic_light CONSTANTS North South SouthRight EastWest NorthRight AXIOMS axm3: partition(DIRECTION,{North},{SouthRight},{NorthRight},{EastWest},{South}) not theorem › axm6: CONFLICT[{EastWest}] = {North,South,SouthRight,NorthRight} not theorem › axm7: CONFLICT[{North}] = {EastWest,SouthRight} not theorem › axm8: CONFLICT[{South}]= {EastWest, NorthRight} not theorem › axm9: CONFLICT[{SouthRight}] = {EastWest,North} not theorem › axm10: CONFLICT[{NorthRight}] = {EastWest,South} not theorem › END And a simple machine refinement can use the new context for a 5way traffic light. This machine does not have any proof obligations. MACHINE m1five_way › REFINES m0traffic_light SEES c1five_way .... Best regards, Son 20150906 9:14 GMT+01:00 Michael Leuschel <leuschel@...>: > Hi, > > On 5 Sep 2015, at 15:52, YuanFang Li <liyuanfang@...> wrote: > > > However, again I'm having trouble discharging the same PO about the safety > invariant for the event ToGreen. This time I'm again able to arrive at > "false" as a goal after a long sequence of proof. However I can't seem to > find obvious contradictions. I tried the ProB Disprover and the SMT solvers > without success. The new specification can be found at > https://www.dropbox.com/s/anolxja7ucilzdm/5way_traffic.zip?dl=0. Your help > is greatly appreciated! > > > If you add the following theorem (or axiom will also do) to your context, > then ProB can discharge the PO: > > theorem @prob CONFLICT = > {(North↦SouthRight),(North↦EastWest), > (SouthRight↦North),(SouthRight↦EastWest), > (NorthRight↦EastWest),(NorthRight↦South), > (EastWest↦North),(EastWest↦SouthRight), > (EastWest↦NorthRight),(EastWest↦South), > (South↦NorthRight),(South↦EastWest)} > > (It is on our todolist to improve ProB’s solving capabiilites concerning > relational image.) > I haven’t tried doing the proof interactively. > > BTW: I had to import your .bum and .buc files manually; Eclipse was > complaining that there is no project to import. > > Best regards, > Michael Leuschel > > >  > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Michael Leuschel <leuschel@cs...>  20150906 13:07:18

Hi, > On 6 Sep 2015, at 12:55, YuanFang Li <liyuanfang@...> wrote: > > Many thanks Michael for the help. However I can't seem to find how to use ProB within Rodin to discharge the PO automatically. In my proof control window there is only "(Dis)Prove with ProB". Yes, that is the button. The command will try to find counterexamples to the PO, and in some cases it may find a proof along the way (for this the proof obligation must not make use of deferred sets (nonenumerated carrier sets) and ProB must be able to constrain its enumeration to a finite number of cases; see http://stups.hhu.de/w/Special:Publication/disprover_eval). Note: The use of the Disprover as a prover is still a relatively new feature and has been less extensively tested than ML, PP; please keep us informed about any issues. Kind regards, Michael 
From: YuanFang Li <liyuanfang@gm...>  20150906 10:56:14

Many thanks Michael for the help. However I can't seem to find how to use ProB within Rodin to discharge the PO automatically. In my proof control window there is only "(Dis)Prove with ProB". Did you mean that I right click on the machine and select "Start Animation / Model Checking", and then use "Invariant Preservation" under "checks/Constraint based checking"? Thanks again. Best regards YuanFang On 6 September 2015 at 18:14, Michael Leuschel < leuschel@...> wrote: > Hi, > > On 5 Sep 2015, at 15:52, YuanFang Li <liyuanfang@...> wrote: > > > However, again I'm having trouble discharging the same PO about the safety > invariant for the event ToGreen. This time I'm again able to arrive at > "false" as a goal after a long sequence of proof. However I can't seem to > find obvious contradictions. I tried the ProB Disprover and the SMT solvers > without success. The new specification can be found at > https://www.dropbox.com/s/anolxja7ucilzdm/5way_traffic.zip?dl=0. Your > help is greatly appreciated! > > > If you add the following theorem (or axiom will also do) to your context, > then ProB can discharge the PO: > > theorem @prob CONFLICT = > {(North↦SouthRight),(North↦EastWest), > (SouthRight↦North),(SouthRight↦EastWest), > (NorthRight↦EastWest),(NorthRight↦South), > (EastWest↦North),(EastWest↦SouthRight), > (EastWest↦NorthRight),(EastWest↦South), > (South↦NorthRight),(South↦EastWest)} > > (It is on our todolist to improve ProB’s solving capabiilites concerning > relational image.) > I haven’t tried doing the proof interactively. > > BTW: I had to import your .bum and .buc files manually; Eclipse was > complaining that there is no project to import. > > Best regards, > Michael Leuschel > > 
From: Michael Leuschel <leuschel@cs...>  20150906 08:14:21

Hi, > On 5 Sep 2015, at 15:52, YuanFang Li <liyuanfang@...> wrote: > > > However, again I'm having trouble discharging the same PO about the safety invariant for the event ToGreen. This time I'm again able to arrive at "false" as a goal after a long sequence of proof. However I can't seem to find obvious contradictions. I tried the ProB Disprover and the SMT solvers without success. The new specification can be found at https://www.dropbox.com/s/anolxja7ucilzdm/5way_traffic.zip?dl=0 <https://www.dropbox.com/s/anolxja7ucilzdm/5way_traffic.zip?dl=0>;. Your help is greatly appreciated! If you add the following theorem (or axiom will also do) to your context, then ProB can discharge the PO: theorem @prob CONFLICT = {(North↦SouthRight),(North↦EastWest), (SouthRight↦North),(SouthRight↦EastWest), (NorthRight↦EastWest),(NorthRight↦South), (EastWest↦North),(EastWest↦SouthRight), (EastWest↦NorthRight),(EastWest↦South), (South↦NorthRight),(South↦EastWest)} (It is on our todolist to improve ProB’s solving capabiilites concerning relational image.) I haven’t tried doing the proof interactively. BTW: I had to import your .bum and .buc files manually; Eclipse was complaining that there is no project to import. Best regards, Michael Leuschel 
From: YuanFang Li <liyuanfang@gm...>  20150905 13:53:07

Hi Jens: actually I forgot to tick the box "Contact all update sites". After I tick that box everything works. Hi Thái Sơn: thanks for the clarification. I extended the 2way traffic specification into a 5way system, where right turn on northsouth is supported (driving on the left). The new specification extends the previous one in a very similar way, with the only major change being CONFLICT is now a relation, but not a function (as a direction may be in conflict with multiple other directions). However, again I'm having trouble discharging the same PO about the safety invariant for the event ToGreen. This time I'm again able to arrive at "false" as a goal after a long sequence of proof. However I can't seem to find obvious contradictions. I tried the ProB Disprover and the SMT solvers without success. The new specification can be found at https://www.dropbox.com/s/anolxja7ucilzdm/5way_traffic.zip?dl=0. Your help is greatly appreciated! Best regards YuanFang On 5 September 2015 at 17:52, Jens Bendisposto < bendisposto@...> wrote: > Hi, > > I just tried the installation with both update sites using Rodin 3.2 and > it worked for me, so we will need more information in order to fix the > problem you had. I assume Eclipse told you that it cannot install ProB? If > I remember correctly, Eclipse shows some information about the reason why > it cannot install a selected component, could you provide that information? > Also, what version of Rodin and what system do you use? > > Regards, > Jens > > On 05.09.2015, at 03:09, YuanFang Li <liyuanfang@...> wrote: > > Thanks Thái Sơn. It worked! > > Just to clarify, when the goal/consequent to prove is "false", does it > mean there is a logical contradiction in the antecedents? > > Michael: thanks for the tip about ProB and ProB DisProver. I tried to > download it using both the ProB update site in Rodin and the ProB nightly > update site (http://nightly.cobra.cs.uniduesseldorf.de/rodin/updatesite/), > but none worked. It complained about "Cannot perform operation". Any idea > how I can install it? > > Best regards > YuanFang > > On 5 September 2015 at 00:40, Thái Sơn Hoàng <tshoang@...> wrote: > >> Hi YuanFang, >> The remaining proof branch needs a little bit more work. >>  Add a hypothesis : CONFLICT(CONFLICT(d)) = d (that should be easily >> discharged). >>  Select the following hypotheses: >> >> light_dir(d)∈{Green,Amber} >> >> ¬light_dir(CONFLICT(d))=Green >> >> ¬light_dir(CONFLICT(d))=Amber >> >> light_dir(d)=light_dir(CONFLICT(d)) >> >> It should be enough to discharge the goal. >> Best regards, >> Son >> >> 20150904 13:11 GMT+01:00 YuanFang Li <liyuanfang@...>: >> > Hi, >> > >> > The specification in a zip file that can be imported into Rodin can be >> > downloaded at the following link: >> > https://www.dropbox.com/s/iedfrm13g5ddjrh/2way_traffic.zip?dl=0. >> > >> > Thanks! >> > >> > Best regards >> > YuanFang >> > >> > On 4 September 2015 at 21:56, YuanFang Li <liyuanfang@...> >> wrote: >> >> >> >> Hi, >> >> >> >> I have a very simple 2direction traffic junction specification >> containing >> >> a context and a machine. The context, among others, contains a function >> >> CONFLICT, that records that traffic in the 2 directions are in >> conflict with >> >> each other. >> >> >> >> The machine has a variable, light_dir, which is a function that gives >> the >> >> traffic light's colour of a direction. There is an invariant, inv2, >> that >> >> states that for any direction, if its light is either green or amber, >> the >> >> conflict direction's light must be red. Besides initialisation, the >> machine >> >> has 3 events that change the light of a direction to red, green, and >> amber >> >> respectively. >> >> >> >> A seemingly simple PO for the above invariant, inv2, and the event >> ToGreen >> >> (ToGreen/inv2/INV), cannot be discharged. The auto prover leaves >> "false" >> >> (\bot) to be discharged eventually, and I'm not sure how to proceed. >> >> >> >> The logic in the machine is pretty simple, and the PO itself seems to >> be >> >> simple too. >> >> >> >> The context and machine is shown below. Any assistance will be greatly >> >> appreciated! >> >> >> >> >> >> CONTEXT >> >> Traffic_Context1 › >> >> SETS >> >> ⚬ LIGHT › >> >> ⚬ DIRECTION › >> >> CONSTANTS >> >> ⚬ NorthSouth › >> >> ⚬ EastWest › >> >> ⚬ Red › >> >> ⚬ Green › >> >> ⚬ Amber › >> >> ⚬ CONFLICT › >> >> AXIOMS >> >> ⚬ axm1: partition(DIRECTION, {NorthSouth},{EastWest}) not >> >> theorem › >> >> ⚬ axm3: partition(LIGHT,{Red},{Green},{Amber}) not theorem › >> >> ⚬ axm6: CONFLICT∈DIRECTION→DIRECTION not theorem › >> >> ⚬ axm7: CONFLICT(NorthSouth) = EastWest not theorem › >> >> ⚬ axm8: CONFLICT(EastWest)= NorthSouth not theorem › >> >> ⚬ axm9: ∀d·d∈DIRECTION⇒CONFLICT(d)≠d not theorem › >> >> ⚬ axm10: ∀d·d∈DIRECTION⇒CONFLICT(CONFLICT(d))=d not theorem › >> >> END >> >> >> >> >> >> MACHINE >> >> TwoWay › >> >> SEES >> >> ⚬ Traffic_Context1 >> >> VARIABLES >> >> ⚬ light_dir › >> >> INVARIANTS >> >> ⚬ inv1: light_dir∈DIRECTION→LIGHT not theorem › >> >> ⚬ inv2: ∀d· (d∈DIRECTION ∧ light_dir(d)∈{Green,Amber}) ⇒ >> >> light_dir(CONFLICT(d)) ∈ {Red} not theorem › >> >> EVENTS >> >> ⚬ INITIALISATION: not extended ordinary › >> >> THEN >> >> ⚬ act1: light_dir≔{NorthSouth↦Red, EastWest↦Red} › >> >> END >> >> >> >> ⚬ ToRed: not extended ordinary › >> >> ANY >> >> ⚬ dir › >> >> WHERE >> >> ⚬ grd1: dir∈DIRECTION not theorem › >> >> ⚬ grd2: light_dir(dir)=Amber not theorem › >> >> THEN >> >> ⚬ act1: light_dir(dir)≔Red › >> >> END >> >> >> >> ⚬ ToGreen: not extended ordinary › >> >> ANY >> >> ⚬ dir › >> >> WHERE >> >> ⚬ grd1: dir∈DIRECTION not theorem › >> >> ⚬ grd2: light_dir(dir)=Red not theorem › >> >> ⚬ grd3: light_dir(CONFLICT(dir))=Red not theorem › >> >> THEN >> >> ⚬ act1: light_dir(dir)≔Green › >> >> END >> >> >> >> ⚬ ToAmber: not extended ordinary › >> >> ANY >> >> ⚬ dir › >> >> WHERE >> >> ⚬ grd1: dir∈DIRECTION not theorem › >> >> ⚬ grd2: light_dir(dir)=Green not theorem › >> >> THEN >> >> ⚬ act1: light_dir(dir)≔Amber › >> >> END >> >> >> >> END >> >> >> >> Best regards >> >> YuanFang >> >> >> > >> > >> > >>  >> > >> > _______________________________________________ >> > Rodinbsharpuser mailing list >> > Rodinbsharpuser@... >> > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >> > >> > > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > 
From: Jens Bendisposto <bendisposto@cs...>  20150905 07:52:38

Hi, I just tried the installation with both update sites using Rodin 3.2 and it worked for me, so we will need more information in order to fix the problem you had. I assume Eclipse told you that it cannot install ProB? If I remember correctly, Eclipse shows some information about the reason why it cannot install a selected component, could you provide that information? Also, what version of Rodin and what system do you use? Regards, Jens On 05.09.2015, at 03:09, YuanFang Li <liyuanfang@...> wrote: > Thanks Thái Sơn. It worked! > > Just to clarify, when the goal/consequent to prove is "false", does it mean there is a logical contradiction in the antecedents? > > Michael: thanks for the tip about ProB and ProB DisProver. I tried to download it using both the ProB update site in Rodin and the ProB nightly update site (http://nightly.cobra.cs.uniduesseldorf.de/rodin/updatesite/), but none worked. It complained about "Cannot perform operation". Any idea how I can install it? > > Best regards > YuanFang > > On 5 September 2015 at 00:40, Thái Sơn Hoàng <tshoang@...> wrote: > Hi YuanFang, > The remaining proof branch needs a little bit more work. >  Add a hypothesis : CONFLICT(CONFLICT(d)) = d (that should be easily > discharged). >  Select the following hypotheses: > > light_dir(d)∈{Green,Amber} > > ¬light_dir(CONFLICT(d))=Green > > ¬light_dir(CONFLICT(d))=Amber > > light_dir(d)=light_dir(CONFLICT(d)) > > It should be enough to discharge the goal. > Best regards, > Son > > 20150904 13:11 GMT+01:00 YuanFang Li <liyuanfang@...>: > > Hi, > > > > The specification in a zip file that can be imported into Rodin can be > > downloaded at the following link: > > https://www.dropbox.com/s/iedfrm13g5ddjrh/2way_traffic.zip?dl=0. > > > > Thanks! > > > > Best regards > > YuanFang > > > > On 4 September 2015 at 21:56, YuanFang Li <liyuanfang@...> wrote: > >> > >> Hi, > >> > >> I have a very simple 2direction traffic junction specification containing > >> a context and a machine. The context, among others, contains a function > >> CONFLICT, that records that traffic in the 2 directions are in conflict with > >> each other. > >> > >> The machine has a variable, light_dir, which is a function that gives the > >> traffic light's colour of a direction. There is an invariant, inv2, that > >> states that for any direction, if its light is either green or amber, the > >> conflict direction's light must be red. Besides initialisation, the machine > >> has 3 events that change the light of a direction to red, green, and amber > >> respectively. > >> > >> A seemingly simple PO for the above invariant, inv2, and the event ToGreen > >> (ToGreen/inv2/INV), cannot be discharged. The auto prover leaves "false" > >> (\bot) to be discharged eventually, and I'm not sure how to proceed. > >> > >> The logic in the machine is pretty simple, and the PO itself seems to be > >> simple too. > >> > >> The context and machine is shown below. Any assistance will be greatly > >> appreciated! > >> > >> > >> CONTEXT > >> Traffic_Context1 › > >> SETS > >> ⚬ LIGHT › > >> ⚬ DIRECTION › > >> CONSTANTS > >> ⚬ NorthSouth › > >> ⚬ EastWest › > >> ⚬ Red › > >> ⚬ Green › > >> ⚬ Amber › > >> ⚬ CONFLICT › > >> AXIOMS > >> ⚬ axm1: partition(DIRECTION, {NorthSouth},{EastWest}) not > >> theorem › > >> ⚬ axm3: partition(LIGHT,{Red},{Green},{Amber}) not theorem › > >> ⚬ axm6: CONFLICT∈DIRECTION→DIRECTION not theorem › > >> ⚬ axm7: CONFLICT(NorthSouth) = EastWest not theorem › > >> ⚬ axm8: CONFLICT(EastWest)= NorthSouth not theorem › > >> ⚬ axm9: ∀d·d∈DIRECTION⇒CONFLICT(d)≠d not theorem › > >> ⚬ axm10: ∀d·d∈DIRECTION⇒CONFLICT(CONFLICT(d))=d not theorem › > >> END > >> > >> > >> MACHINE > >> TwoWay › > >> SEES > >> ⚬ Traffic_Context1 > >> VARIABLES > >> ⚬ light_dir › > >> INVARIANTS > >> ⚬ inv1: light_dir∈DIRECTION→LIGHT not theorem › > >> ⚬ inv2: ∀d· (d∈DIRECTION ∧ light_dir(d)∈{Green,Amber}) ⇒ > >> light_dir(CONFLICT(d)) ∈ {Red} not theorem › > >> EVENTS > >> ⚬ INITIALISATION: not extended ordinary › > >> THEN > >> ⚬ act1: light_dir≔{NorthSouth↦Red, EastWest↦Red} › > >> END > >> > >> ⚬ ToRed: not extended ordinary › > >> ANY > >> ⚬ dir › > >> WHERE > >> ⚬ grd1: dir∈DIRECTION not theorem › > >> ⚬ grd2: light_dir(dir)=Amber not theorem › > >> THEN > >> ⚬ act1: light_dir(dir)≔Red › > >> END > >> > >> ⚬ ToGreen: not extended ordinary › > >> ANY > >> ⚬ dir › > >> WHERE > >> ⚬ grd1: dir∈DIRECTION not theorem › > >> ⚬ grd2: light_dir(dir)=Red not theorem › > >> ⚬ grd3: light_dir(CONFLICT(dir))=Red not theorem › > >> THEN > >> ⚬ act1: light_dir(dir)≔Green › > >> END > >> > >> ⚬ ToAmber: not extended ordinary › > >> ANY > >> ⚬ dir › > >> WHERE > >> ⚬ grd1: dir∈DIRECTION not theorem › > >> ⚬ grd2: light_dir(dir)=Green not theorem › > >> THEN > >> ⚬ act1: light_dir(dir)≔Amber › > >> END > >> > >> END > >> > >> Best regards > >> YuanFang > >> > > > > > >  > > > > _______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > >  > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 