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}

_{Nov}

_{Dec}

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 
From: Thái Sơn Hoàng <tshoang@us...>  20150905 07:37:46

Hi YuanFang, Yes, when the goal to prove is "false" then we should look for some contradiction in the antecedents. Of course, it could also be an indication that there are some problem with the model. Best regards, Son 20150905 2:09 GMT+01:00 YuanFang Li <liyuanfang@...>: > 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 >> > > > 
From: YuanFang Li <liyuanfang@gm...>  20150905 01:09:59

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 > > > 
From: Thái Sơn Hoàng <tshoang@us...>  20150904 14:43:57

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 >> 
From: Michael Leuschel <leuschel@cs...>  20150904 12:51:45

Hi, The PO seems provable: ProB does not find an invariant violation using model checking nor using constraintbased invariant checking. Like you I was unable to discharge it with ML, PP or SMT; but I haven’t had time to dig deeper. Kind regards, Michael PS: The ProB Disprover discharges the PO automatically; so it is a nice example for my presentation next week at SEFM ;) 
From: YuanFang Li <liyuanfang@gm...>  20150904 12:11:48

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 > > 
From: YuanFang Li <liyuanfang@gm...>  20150904 11:56:58

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 
From: JeanRaymond Abrial <jrabrial@ne...>  20150904 09:38:30

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@...> 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_______________________________________________ <http://pubads.g.doubleclick.net/gampad/clk?id=241902991&iu=/4140_______________________________________________>; > Rodinbsharpuser mailing list > Rodinbsharpuser@... <mailto:Rodinbsharpuser@...> > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser <https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser>; 
From: Jens Bendisposto <bendisposto@cs...>  20150904 09:24:10

Hi, usually I do something like this: CONTEXT ctx › SETS ⚬ A › ⚬ B › CONSTANTS ⚬ f not symbolic Physical Unit: Inferred Physical Unit: › AXIOMS ⚬ axm1: finite(A) not theorem › ⚬ axm2: finite(B) not theorem › ⚬ axm3: f∈ A↔B not theorem › ⚬ axm3a: f ⊆ A×B theorem › ⚬ axm3b: finite(A×B) theorem › ⚬ axm4: finite(f) theorem › END axm3a and axm3b will help the auto provers to prove that f is finite. Cheers, Jens On 04.09.2015, at 11:15, Sam Pinkus <sgpinkus@...> wrote: > 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: Sam Pinkus <sgpinkus@gm...>  20150904 09:16:01

<html> <head> <meta httpequiv="contenttype" content="text/html; charset=utf8"> </head> <body text="#000000" bgcolor="#FFFFFF"> Hi,<br> <br> 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> <br> 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> <br> CONTEXT<br> ctx ›<br> SETS<br> ⚬ FOO <br> ⚬ BAH <br> AXIOMS<br> ⚬ axm2: finite(FOO) not theorem<br> ⚬ axm3: finite(BAH) not theorem<br> END<br> <br> MACHINE<br> mchn ›<br> SEES<br> ⚬ ctx <br> VARIABLES<br> ⚬ f <br> ⚬ g <br> ⚬ x <br> INVARIANTS<br> ⚬ inv1: f ⊆ FOO not theorem<br> ⚬ inv2: finite(f) theorem<br> ⚬ inv3: g ⊆ BAH not theorem<br> ⚬ inv4: finite(g) theorem<br> ⚬ inv5: x ∈ f ⇸ g not theorem<br> ⚬ inv6: finite(x) theorem<br> EVENTS<br> ⚬ INITIALISATION: not extended ordinary<br> THEN<br> ⚬ act1: f ≔ ∅<br> ⚬ act2: g ≔ ∅<br> ⚬ act3: x ≔ ∅<br> END<br> END<br> <br> Thanks,<br> <br> Sam.<br> <br> <div class="mozsignature"> <br> <p style="color:#CCC; fontsize:small"><strong>PGP</strong>: 0xA53455C1</p> </div> </body> </html> 
From: ACKERMANN J G <32247060@my...>  20150902 21:40:05

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 
From: Sam Pinkus <sgpinkus@gm...>  20150902 02:17:25

<html> <head> <meta content="text/html; charset=utf8" httpequiv="ContentType"> </head> <body text="#000000" bgcolor="#FFFFFF"> <div class="mozciteprefix">Thanks Son, that has solved this issue. <br> <br> So, Rodin provers will simply not use any other valid invariants to prove an invariant, even though it could. Rodin will only use guards and axioms, unless you explicitly tell it you want to use invariants by declaring something a "theorem".<br> <br> Thanks,<br> <br> Sam.<br> <br> On 09/01/2015 01:54 AM, Thái Sơn Hoàng wrote:<br> </div> <blockquote cite="mid:CAMfA3i+BGUK+J+vwjRuHJOp4L+BcUDngT=ObY=D10==52gf_Sg@..." type="cite"> <pre wrap=""> Dear Sam, Rodin should be able to prove "card(var1) ≤ card(THINGS)" as a theorem from the fact that "var1 ⊆ THINGS" automatically. Just change the inv2 into a theorem and it will solve your problem. Best regards, Son 20150831 13:05 GMT+01:00 Sam Pinkus <a class="moztxtlinkrfc2396E" href="mailto:sgpinkus@..."><sgpinkus@...></a>: </pre> <blockquote type="cite"> <pre wrap="">Hi, I'm new to Rodin and I'm having an issue making Rodin discharge a proof involving card(). I have constructed a simple machine to expose the issue: CONTEXT ctx SETS ⚬ THINGS AXIOMS ⚬ axm1: finite(THINGS) END MACHINE mch SEES ⚬ ctx VARIABLES ⚬ var1 INVARIANTS ⚬ inv1: var1 ⊆ THINGS ⚬ inv2: card(var1) ≤ card(THINGS) EVENTS ⚬ INITIALISATION: not extended ordinary THEN ⚬ act1: var1 ≔ ∅ END ⚬ add_thing: not extended ordinary ANY ⚬ thing WHERE ⚬ grd1: thing ∈ THINGS ∖ var1 THEN ⚬ act1: var1 ≔ var1 ∪ {thing} END END Rodin can't prove `inv2: card(var1) ≤ card(THINGS)` is maintained by `add_thing()`. Specifically it ends up failing to prove this: card(var1)+1 − card(var1∩{thing})≤card(THINGS) I found a few questions in the archives relating to card(), proofs not working properly but could not map the solution to my problem  newb. Any help appreciated. Thanks, Sam.  PGP: 0xA53455C1  _______________________________________________ Rodinbsharpuser mailing list <a class="moztxtlinkabbreviated" href="mailto:Rodinbsharpuser@...">Rodinbsharpuser@...</a> <a class="moztxtlinkfreetext" href="https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser">https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser</a>; </pre> </blockquote> </blockquote> <br> <br> <div class="mozsignature"> <br> <p style="color:#CCC; fontsize:small"><strong>PGP</strong>: 0xA53455C1</p> </div> </body> </html> 
From: Thái Sơn Hoàng <tshoang@us...>  20150831 15:54:53

Dear Sam, Rodin should be able to prove "card(var1) ≤ card(THINGS)" as a theorem from the fact that "var1 ⊆ THINGS" automatically. Just change the inv2 into a theorem and it will solve your problem. Best regards, Son 20150831 13:05 GMT+01:00 Sam Pinkus <sgpinkus@...>: > Hi, > > I'm new to Rodin and I'm having an issue making Rodin discharge a proof > involving card(). I have constructed a simple machine to expose the issue: > > CONTEXT > ctx > SETS > ⚬ THINGS > AXIOMS > ⚬ axm1: finite(THINGS) > END > > > MACHINE > mch > SEES > ⚬ ctx > VARIABLES > ⚬ var1 > INVARIANTS > ⚬ inv1: var1 ⊆ THINGS > ⚬ inv2: card(var1) ≤ card(THINGS) > EVENTS > ⚬ INITIALISATION: not extended ordinary > THEN > ⚬ act1: var1 ≔ ∅ > END > > ⚬ add_thing: not extended ordinary > ANY > ⚬ thing > WHERE > ⚬ grd1: thing ∈ THINGS ∖ var1 > THEN > ⚬ act1: var1 ≔ var1 ∪ {thing} > END > END > > Rodin can't prove `inv2: card(var1) ≤ card(THINGS)` is maintained by > `add_thing()`. Specifically it ends up failing to prove this: > > card(var1)+1 − card(var1∩{thing})≤card(THINGS) > > I found a few questions in the archives relating to card(), proofs not > working properly but could not map the solution to my problem  newb. Any > help appreciated. > > Thanks, > > Sam. > >  > > PGP: 0xA53455C1 > > >  > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Sam Pinkus <sgpinkus@gm...>  20150831 12:05:33

<html> <head> <meta httpequiv="contenttype" content="text/html; charset=utf8"> </head> <body text="#000000" bgcolor="#FFFFFF"> Hi,<br> <br> I'm new to Rodin and I'm having an issue making Rodin discharge a proof involving card(). I have constructed a simple machine to expose the issue:<br> <br> CONTEXT<br> ctx <br> SETS<br> ⚬ THINGS <br> AXIOMS<br> ⚬ axm1: finite(THINGS)<br> END<br> <br> <br> MACHINE<br> mch <br> SEES<br> ⚬ ctx <br> VARIABLES<br> ⚬ var1 <br> INVARIANTS<br> ⚬ inv1: var1 ⊆ THINGS<br> ⚬ inv2: card(var1) ≤ card(THINGS)<br> EVENTS<br> ⚬ INITIALISATION: not extended ordinary<br> THEN<br> ⚬ act1: var1 ≔ ∅<br> END<br> <br> ⚬ add_thing: not extended ordinary<br> ANY<br> ⚬ thing <br> WHERE<br> ⚬ grd1: thing ∈ THINGS ∖ var1<br> THEN<br> ⚬ act1: var1 ≔ var1 ∪ {thing}<br> END<br> END<br> <br> Rodin can't prove `inv2: card(var1) ≤ card(THINGS)` is maintained by `add_thing()`. Specifically it ends up failing to prove this:<br> <br> card(var1)+1 − card(var1∩{thing})≤card(THINGS)<br> <br> I found a few questions in the archives relating to card(), proofs not working properly but could not map the solution to my problem  newb. Any help appreciated.<br> <br> Thanks,<br> <br> Sam.<br> <br> <div class="mozsignature"> <br> <p style="color:#CCC; fontsize:small"><strong>PGP</strong>: 0xA53455C1</p> </div> </body> </html> 