eventb-soton / xeventb Goto Github PK

I have intentionally created an error in a machine, using a variable that does not exist (Ss in the last line of the context shown below).
Saving the file in CamilleX did not create an error marker nor error message, despite Build and Prove automatically being enabled.
I often have a similar issue with Camille at the moment; the Event-B context editor does not have this issue.

Comments for XMachine (multiline comments) are not translated to Rodin machine (See m0 in the following attached project).
P.zip
Note that the it works for XContext (see c0 in the same project).

In the following context c0, a record A is declared

context c0
sets S
records
	record A
	    x : many S
end

In the following machine m0, a record B extends A, which causes an error due to A cannot be found

machine m0
sees c0
records
	record B extends A
end

This problem occurs on Rodin 3.4.0 with CamilleX prototype installed. This does not occur when running from code.

Quite often the generated Rodin files (contexts and machines) are disappeared. This stops the XText builder to complete the build. Often, ones need to go through each CamilleX constructs to regenerate the files one by one.

It is desirable to have comment for a part of an expression/predicate. For example,
@Label:
"<" // Comment on 1st part
"<<second part" // Comment on 2nd part
"<>" // Comment on 3rd part
This feature is requested by Tomas Fischer via private communication.

The Rodin Symbol Table does not work with CamilleX editors. Error messages state "Cannot insert symbol: select a text line in an editor".

The formatter for XMachine does not indent the end keyword for events when there is a present of witness (with clause) as showed in the following example.

	convergent event CloseCourse
	refines CloseCourses
	any
		c
	where
		@grd2_1: c ∈ dom(atnds)
	then
		@act1_2: atnds ≔ {c} ⩤ atnds
	with
		@cs: cs = {c} 
end

The formatter seems to work fine without the with clause as in the following example

	convergent event Register
	refines Register
	any
		p
		c
	where
		@grd2_1: p ∈ PRTCPT
		@grd2_2: p ≠ instrs(c)
		@grd2_3: c ∈ dom(atnds)
		@grd2_4: p ∉ atnds(c)
		theorem @thm2_3: atnds(c) = prtcpts[{c}]
	then
		@act2_1: atnds(c) ≔ atnds(c) ∪ {p}
	end

At the moment, identifiers (e.g., variables, machine names, constants, carrier sets, etc.) must be ASCII identifiers. It is desirable to have support for proper Unicode identifiers (which is already supported by Rodin itself).

Undo does not work using keyboard shortcuts.
(undo works from the edit menu and ctrl-C and ctrl-V shortcuts work ok).

Currently, comments are restricted to before the modelling elements (Multi-line) or after the modelling elements (single-line). This is quite restrictive and due to the translation of the comments into the Rodin elements. We should allow comments everywhere by ignoring them, however it means that the comments will no longer be kept in the underlying Rodin elements (but that is OK).

Currently the comment must be put before the commented element. However, the single line comment fits better after the commented element, e.g. in the sets, constants, variables or parameters sections, but also for short axioms, invariants, guards and actions.
(This feature is requested by Tomas Fischer via private communication)

Currently, converting some Rodin contexts/machines result in empty XContext/XMachine.
(This bug is reported by Tomas Fischer via private communication)

It would be easier to have the events always ended with keyword "end" and removed the character ";". This feature is requested by Tomas Fischer via private communication.

It would be nice to show inherited event elements in the outline and in the tooltip.
This feature is requested by Tomas Fischer via private communication.

Variant is not translated in machine inclusion.

Add the moment, convert from Rodin constructs to CamilleX ignore features of generated elements (e.g., elements generated from UML-B). This is done by transient value services for XContext (ac.soton.xeventb.common.XContextTransientValueService) and XMachine (ac.soton.xeventb.common.XMachineTransientValueService).

This cause the generator to fail with exceptions thrown when the feature is a required feature, e.g., the name and predicate of axioms. As a result, the generator should NOT ignore the feature of the generated elements.

Contextual links lead to generated bum/buc files instead of bumx/bucx sources.
This feature is requested by Tomas Fischer via private communication.

Currently, a marker (error/warning/info) attached to the XMachine or XContext will highlight the whole content of the XMachine or XContext. It is therefore better to attach the marker to the name of the machine or the context.

The models/projects should have version numbers (using semantic versioning). This can be done with some Manifest file.

Hello XEventB team,

The Xtext team would like to update the Xtext community website listing all the cool projects people are building around Xtext/Xtend.

See also the corresponding GitHub issue and Bugzilla ticket.

If you are interested that the XEventB project is listed there, please provide the following information as a comment to this issue:

<tr>
	<td><a href="project_link">project_name</a></td>
	<td>project_description_max_2_sentences</td>
	<td>license</td>
	<td>category</td>
	<td>author(s)</td>
</tr>

We will then update the Xtext community website and get it online as soon as possible.

Thanks!
Tamás

I have tried to copy and paste a machine from Camille (non-X version).
I had to reformat slightly.
For some reason the begin was not accepted for the INITIALISATION (contrary what seems to be used in the Camille guide PDF).
I had to rename when to where.
After some tweaks I got the contents to pass through CamilleX.
HOwever, the generated .bum files contains several errors.

Here are the contents:
machine XTransfer0
variables b c
invariants
@INV1: b∈ℕ // the bank account
@Inv2: c∈ℕ // the client account, no overdrafts
@inv3: b+c = 10 // total sum of credits: 10
events
event INITIALISATION
then
@Ini1: b := 5
@Ini2: c ≔ 5
end
event b2c where @g1 b>0 then
@A1: b ≔ b−1
@a2: c ≔ c+1
end
event c2b where @g1 c>0 then
@A1: b ≔ b+1
@a2: c ≔ c−1
end
end

The Rodin errors are:
Description Resource Path Location Type
Lexical error. Character : has been ignored XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker
Syntax error: Operator: ≔ should appear at the beginning of a sub-formula XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker
Syntax error: Operator: ≔ should appear at the beginning of a sub-formula XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker
Syntax error: Operator: ≔ should appear at the beginning of a sub-formula XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker
Syntax error: Operator: ≔ should appear at the beginning of a sub-formula XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker
Syntax error: Unknown operator: (expected to find an assignment operator) XTransfer0.bum /CamilleXTests Unknown Rodin Problem Marker

After adding a : after the two labels @g1 some of the errors disappeared, but there is still a lexical error for ini1; somehow the := is not converted to its Unicode equivalent.

When importing a project with CamilleX source, the XText builder cannot automatically generate the corresponding Rodin files. As a result, users often need to go through each CamilleX files (in the right order) to generate them manually (i.e., making changes to the source file, e.g., adding a blank space, and saving it again to enable the generator.
It would be nice to have a way to do this automatically.

This is requested by Jonathan Hammond via private email (December 2020).

When converting plain text to Rodin keyboard symbols using the contextual helper, it puts "invariant" keyword at the end of the preceding line

It would be desirable to include machines from a different project than the one containing the including machine.

I had old Camille open on the generated file; I saved a change in CamilleX and then reloaded the contents in Camille and got the following error message, which I guess is coming from new CamilleX?

At the moment using BOOL as type of field will cause an error

context c0
sets S
records
	record A
	    x : BOOL
end

(This is reported by @cfsnook)

It would be useful to have a menu option to re-generate selected (or all) machines and contexts in a project.

There are a few use cases where this is needed - e.g. if a project is shared in a repo, we may not track the bum and buc files because they have a lot of spurious changes.

At the moment i have to open each CamilleX file and make a change and save it and then revert the change and save it again.

Currently, users have to look at the Rodin components (Contexts and Machines) for problems at the "inner syntax" of the components. It would be desirable to display the information in the CamilleX components (XContexts and XMachines).

CodeQL currently uses Maven to compile the code. Since Rodin 3.8 was released, Rodin 3.7 was moved to "old" which causes the issue. As a result, we should not use version specific update site, but rather the composite update site for Rodin core, i.e., http://rodin-b-sharp.sourceforge.net/core-updates/

In CamilleX 3.0.0, the events group in the machine only support 1 event at the moment. That is the following

events
    event e
    end
end

is OK, but

events
    event e
    end

    event f
    end
end

is NOT OK.

This is a bug that needs to be fixed.

converting from event-b to xtext with extended property is now fixed for next release 0.08

Currently, the formulae are translated into Event-B mathematical language automatically. However, untranslated formulae inconsistency in displaying errors/warnings from the Rodin components, e.g., in the positions of the problems. Therefore it is important to warn the user about that.

I seem to get error messages and exceptions from CamilleX when I have closed projects.
For example,

An exception occurred invoking extension: ac.soton.xeventb.xcontext.ui.navigatorContent.XContext for object org.eclipse.jface.viewers.TreePath@276a6e1

org.eclipse.core.internal.resources.ResourceException: Project 'Soda' is not open.
at org.eclipse.core.internal.resources.Project.checkAccessible(Project.java:144)
at org.eclipse.core.internal.resources.Container.members(Container.java:239)
at org.eclipse.core.internal.resources.Container.members(Container.java:226)
at ac.soton.xeventb.ui.AbstractXEventBContentProvider.getChildren(AbstractXEventBContentProvider.java:74)
at ac.soton.xeventb.ui.AbstractXEventBContentProvider.hasChildren(AbstractXEventBContentProvider.java:129)
at org.eclipse.ui.internal.navigator.extensions.SafeDelegateTreeContentProvider.hasChildren(SafeDelegateTreeContentProvider.java:112)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.callNormalHasChildren(NavigatorContentServiceContentProvider.java:442)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.access$4(NavigatorContentServiceContentProvider.java:437)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider$3.run(NavigatorContentServiceContentProvider.java:405)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.hasChildren(NavigatorContentServiceContentProvider.java:390)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceContentProvider.hasChildren(NavigatorContentServiceContentProvider.java:434)
at org.eclipse.jface.viewers.AbstractTreeViewer.isExpandable(AbstractTreeViewer.java:2099)
at org.eclipse.jface.viewers.TreeViewer.isExpandable(TreeViewer.java:537)
at org.eclipse.jface.viewers.AbstractTreeViewer.isExpandable(AbstractTreeViewer.java:2137)
at org.eclipse.jface.viewers.AbstractTreeViewer.optionallyPruneChildren(AbstractTreeViewer.java:2770)
at org.eclipse.jface.viewers.AbstractTreeViewer.updateChildren(AbstractTreeViewer.java:2569)
at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefreshStruct(AbstractTreeViewer.java:1894)
at org.eclipse.jface.viewers.TreeViewer.internalRefreshStruct(TreeViewer.java:668)
at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefreshStruct(AbstractTreeViewer.java:1900)
at org.eclipse.jface.viewers.TreeViewer.internalRefreshStruct(TreeViewer.java:668)
at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefresh(AbstractTreeViewer.java:1870)
at org.eclipse.jface.viewers.AbstractTreeViewer.internalRefresh(AbstractTreeViewer.java:1827)
at org.eclipse.ui.navigator.CommonViewer.internalRefresh(CommonViewer.java:529)
at org.eclipse.jface.viewers.StructuredViewer.lambda$3(StructuredViewer.java:1531)
at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1447)
at org.eclipse.jface.viewers.TreeViewer.preservingSelection(TreeViewer.java:354)
at org.eclipse.jface.viewers.StructuredViewer.preservingSelection(StructuredViewer.java:1408)
at org.eclipse.jface.viewers.StructuredViewer.refresh(StructuredViewer.java:1531)
at org.eclipse.jface.viewers.ColumnViewer.refresh(ColumnViewer.java:535)
at org.eclipse.ui.navigator.CommonViewer.refresh(CommonViewer.java:349)
at fr.systerel.internal.explorer.navigator.EventBNavigator$1.refresh(EventBNavigator.java:29)
at org.eclipse.ui.navigator.CommonViewer.refresh(CommonViewer.java:492)
at org.eclipse.jface.viewers.StructuredViewer.refresh(StructuredViewer.java:1467)
at fr.systerel.internal.explorer.navigator.NavigatorController$ViewerRefresher.refreshViewer(NavigatorController.java:96)
at fr.systerel.internal.explorer.navigator.NavigatorController$ViewerRefresher$1.run(NavigatorController.java:79)
at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:37)
at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:182)
at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4034)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3701)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$5.run(PartRenderingEngine.java:1150)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:336)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1039)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:153)
at org.eclipse.ui.internal.Workbench.lambda$3(Workbench.java:680)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:336)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:594)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:148)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:151)
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:388)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:243)
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:498)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:653)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:590)
at org.eclipse.equinox.launcher.Main.run(Main.java:1499)

It would be beneficial to show the bucx / bumx files in the explorer and to put the generated bum / buc files as their child nodes (like Complex Context Structure and Complex Machine Structure do).
(This feature is requested by Tomas Fischer via private communication)