Activity for Son Hoang
-
Son Hoang committed [r16741]
Resotore removeFeature.xml
-
Remove EMF Inclusions and CamilleX (now available from Soton update site)
-
Removed eXtended Event-B editors (now CamilleX)
-
Move scripts for setting up composite update site to a folder
-
We will need another release of Rodin when Eclipse 2020-12 is released.
-
Refreshing issue on Mac OS X Big Sur 11.0.0
-
I now remember that it is about proof reuse. In order to reuse the proofs, the number of sub-goals has to be identical. This decision has been made since the early development of Rodin, i.e., the constraints is that every reasoner with the same input will produce the same number of sub-goal. For example, if you change your operator so that the WD is not longer trivial, the shape of your proof tree changed, hence you potentially lose all the sub-proofs. So this is a feature, not a bug.
-
I cannot remember the exact reason, but it must have something to do with Well-definedness.
-
Dear Leona, I tried the decomposition plug-in with the latest Rodin 3.5.0 and the tool did produce the decomposed model (There are some other issues which you can ignore, but the sub-model seems to work). Did you choose "B-Style" decomposition in the wizard and edit the partition to ensure that the variables are distributed accordingly? Apology for the late reply. Best regards, Son
-
Dear Yang, Which version of Rodin that you tried? Is this Rodin 3.4? If it is then it does not work with Java 14. Rodin 3.4 only works with Java 8. We are working on Rodin 3.5 at the moment. The release candidate (which you can find from the "Files" tab above, under Core_Rodin_Platform will work with Java 14. Best regards, Son
-
Rodin 3.5.0 will be based on Eclipse 2020-06 (4.16) and will work with Java 13.
-
@lvoisin Should this be closed for Rodin 3.5.0 (now that we use Eclipse 4.16)?
-
Dear Leona, I will try to have a look at this some time next week. Best regards, Son
-
Dear Paul, The log file indicates that Java 13.0.1 was used. As far as I can tell, Rodin 3.4 only works with Java 8. For Java 9 and 10, some modifications required to rodin.ini for it to launch. I am quite certain that it does not work for later version of Java (due to the fact that it was built on top of Eclipse Oxygen 4.7.2). Best regards, Son
-
Dear Keith, I did have a problem with the latest Java (Java 11) installed on Mac (together with other Java versions). When launching Eclipse/Rodin, it always pick the Java 11 which does not work for Eclispe 4.7.2 and Rodin 3.40. To enforce the correct Java version, I added -vm arguments to rodin.ini. The following two lines must be put just before the -vmargs argument. -vm /path/to/JVM More information on the -vm option is at https://wiki.eclipse.org/Eclipse.ini#Specifying_the_JVM For example, on...
-
CODA VHDL v0.0.5
-
CamilleX v1.0.0
-
EMF Inclusion 1.0.0
-
Event-B Translator Support 0.0.1
-
EMF Translator 3.0.0
-
EMF Event-B Extension 6.0.0
-
EMF Event-B 6.0.0
-
Just want to mention that we would like to keep the name of the projects and the machines/contexts to be proper identifiers, so that it can be identified with other mechanism, e.g., machine inclusion.
-
Hi Laurent, Having multiple variants is definitely what we want to have. However, the above proof obligation will lead to many repetitive, in particular for the events that decreases v1, i.e., (v1' < v1), it is redundant to prove the second part. (The proof of the second will bascially to prove v1' /= v1 by proving that v1' < v1). I think if we label the variant and anotate the event with each invariant, we could generate the proof obligations for each event much better. Let we have the following...
-
Hi Laurent, Having multiple variants is definitely what we want to have. However, the above proof obligation will lead to many repetitive, in particular for the events that decreases v1, i.e., (v1' < v1), it is redundant to prove the second part. (The proof of the second will bascially to prove v1' /= v1 by proving that v1' < v1). I think if we label the variant and anotate the event with each invariant, we could generate the proof obligations for each event much better. Let we have the following...
-
Utilities feature: Update description with Release History
-
Utilities Tests feature 0.2.4: Initial version
-
Utilities SDK feature: Update feature description with Release History
-
Feature and plug-in version number to release.
-
Update README file.
-
Event-B Utilities 0.2.4
-
Utils SDK feature: Set version number to 0.2.4.qualifier
-
Event-B SCUtils: add method to get invariants from statically checked machine.
-
Event-B Utils: Fixed EOL encoding
-
Event-B Utils: Set the feature number to 0.2.4.qualifier
-
Event-B Utils: Set the plug-in version to 0.2.4.qualifier
-
Seems OK for me on MacOS. (I assme what you mean by the profile editor is the dialog for editing the tactics)
-
XEvent-B 0.0.7
-
Release of EMF Inclusion 0.2.0
-
Qualitative Probability 0.2.4
-
XEvent-B 0.0.6
-
EMF Inclusion framework 0.1.0
-
EMF Utilities version 2.1.1
-
Theory Plugin 4.0.0 RC1
-
Hi Laurent, I did not notice that the hypothesis not(x = 0) is only deselected, but...
-
Generalized Modus Ponens turns goal into "false"
-
Fix appear in [176e85] and will be available in Rodin 3.3.0. Related Commit: [17...
-
Symbols for total and partial surjection
-
Generalized Modus Ponens leads to unprovable sub-goal
-
Stepping through the code (org.eventb.internal.core.seqprover.eventbExtensions.genmp.GenMPC),...
-
Generalized Modus Ponens leads to unprovable sub-goal
-
Dear Laurent, Thank you very much. The changes look reasonable to me. We have checked...
-
Some more information related to the problem: In Linux, the Symbols view seems to...
-
Hi Laurent, The Brave Sans Mono font is loaded by the Event-B UI plug-in. If the...
-
Some symbols do not display properly in the symbols panel
-
The easiest solution is to have the Rodin Keyboard support both style of combinations...
-
Symbols for total and partial surjection
-
Set Rodin Linence feature version to 1.0.0.release
-
Event-B XText Front-end 0.0.5
-
Event-B XText Front-end 0.0.4
-
Event-B XText Front-end 0.0.3
-
Event-B XText Front-end 0.0.2
-
Just to added that I was desparated for the third option (rename automatically) not...
-
Insteads of storing all formula factories outside the proofs, we can store the "datatype...
-
The same goes for the display names of the underlying reasoner. Cheers, Son
-
We have made some experiments along this line and I will speak something about this...
-
I have the feeling that we might need some tactic defined by each theory (or even...
-
Hi Luis Diaz, I assume that you would like to have several operator definitions for...
-
Predicates separation in Theories
-
Datatype Translation for Atelier-B throws IllegalArgumentException
-
RbP0.getPossibleApplications(): Trying to register an existing name with a different type
-
- Bug fixing
-
- Reimplement ContrHypsTests using the new meth...
-
- Make AbstractReasonerTests extends TestCase
-
The matching facilities has been reimplemented using ISpecialization which is the...
-
The matching facilities are now reimplemented using ISpecialization which is the...
-
Changing proof rules do not invalidate proofs
-
Change theory path have no effects on existing proofs
-
Too restrictive: Not all inductive cases are covered
-
XD reasoner: Reasoner fails unexpectedly
-
RbP0.getPossibleApplications(): Trying to register an existing name with a different type
-
Missing NULL state
-
Published iUML-B State Machines 3.4.1 SDK
-
Published iUML-B State Machines 3.4.1
-
Revert to r16646 to fix Statemachines 3.4.0
-
Published iUML-B State Machines 3.4.0
-
Published iUML-B Class Diagrams 1.2.0
-
Published EMF Event-B support for Diagrams 6.0.0
-
- Increase feature number to 5.2.0 (minor upgrade)
-
- Added SDK feature version 5.2.0
-
Increase plugin number to 4.2.0 (minor upgrade)
-
Published EMF Event-B support for Extensions 5.2.0
-
Published EMF Event-B 5.4.0
-
Fix the release notes
-
Increase feature number to 5.4.0 (minor upgrade)
-
Increase version number to 5.4.0
-
Increase the plugin number to 5.4.0 (minor upgr...
-
Export the ac.soton.eventb.emf.core.extension.n...
-
Increase feature version for org.eventb.emf.fea...
-
Added org.eventb.emf.sdk (version 5.3.2)
1 >