eventb-soton / coda_componentdiagrams Goto Github PK

Connectors should be decomposed as one machine per type with a single read operation and a single write operation. These operations should not have guards specifying the value to be read/written. The connector name should be used as the instance name for prefixing. The connector operations should be event synchronised with all component operations that read/write to that connector.

James 10/12/15: The hover over text doesn’t resize/relocate with respect to the diagram (i.e. zoom in, zoom out doesn’t change hover over text size or position); note I am using GTK2, not GTK3 so this may not be an issue in GTK3 (I am working on getting the relevant C library installed to use GTK3).

Colin - At the moment it is just positionsed at a fixed offset from the target element. It should be possible to find the co-ordinates relative to the boundary of the canvas and deduce the best position from this. However, using the 'tool-tip' hover over text for this feature is not ideal anyway. Another problem is that the text often gets in the way. Consider re-implementing this in a better way. (E.g. using a separate view which refocusses depending on hover)

The Symbols view is not available for use whilst using the Properties view for Components. Is there a way to enable this for use as I can't always remember the ASCII equivalents.

James 10/12/15: The hover over does not display in the Component View (perspective) for any operations (transitions, port wakes, etc.)

This is not implemented for CODA

James: The Refactoring in the latest packaging is not rebuilding/generating the Component view and leads to errors. The fix is to simply go into each component refactored and build again, but it caught us off guard to begin with. Information is being unlinked during the refactoring process even though it has not been refactored in previous refinements i.e. variables not defined although present in the event-b code. Perhaps this relates to a refresh issue?

The parameter guard is generated after any other specified guards from iUML-B StateMachines. (James email, 10/12/15)

Son 14/12/15: Yes, this is something that Colin and I have been discussing for awhile. The order of the generated elements need to be more specific, e.g., user-defined. At the moment, I sometime have to add the generated guard as the parameter guard (hence it will be duplicated in the resulting Event-B model) to get some POs (specifically WD ones) proved.

Colin 14/12/15: In general, yes,.. but in this case I think James means the type of the transition’s parameter should come before the same transition's guards (which may refer to the parameter). We can easily fix this using the priorities scheme. Is there any circumstance when this (fixed) order would not be better?

Hovering over transitions, it went a bit loopy, no pun intended. Attached is the error log.

eclipse.buildId=unknown
java.version=1.8.0_45
java.vendor=Oracle Corporation
BootLoader constants: OS=linux, ARCH=x86_64, WS=gtk, NL=en_GB
Command-line arguments:  -os linux -ws gtk -arch x86_64

org.eclipse.ui
Error
Tue Dec 08 08:31:45 GMT 2015
Unhandled event loop exception

java.lang.NullPointerException
	at ac.soton.eventb.statemachines.diagram.edit.parts.TransitionEditPart.getMethodText(TransitionEditPart.java:238)
	at ac.soton.eventb.statemachines.diagram.edit.parts.TransitionEditPart.showTargetFeedback(TransitionEditPart.java:216)
	at org.eclipse.gef.tools.TargetingTool.showTargetFeedback(TargetingTool.java:378)
	at org.eclipse.gef.tools.TargetingTool.handleEnteredEditPart(TargetingTool.java:196)
	at org.eclipse.gef.tools.TargetingTool.setTargetEditPart(TargetingTool.java:357)
	at org.eclipse.gef.tools.TargetingTool.updateTargetUnderMouse(TargetingTool.java:431)
	at org.eclipse.gef.tools.SelectionTool.handleMove(SelectionTool.java:365)
	at org.eclipse.gef.tools.AbstractTool.mouseMove(AbstractTool.java:1182)
	at org.eclipse.gef.tools.SelectionTool.mouseMove(SelectionTool.java:563)
	at org.eclipse.gef.EditDomain.mouseMove(EditDomain.java:287)
	at org.eclipse.gef.ui.parts.DomainEventDispatcher.dispatchMouseMoved(DomainEventDispatcher.java:365)
	at org.eclipse.draw2d.LightweightSystem$EventHandler.mouseMove(LightweightSystem.java:543)
	at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:212)
	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)

An instance property should be available for naming Components. This would be used as the prefix for decomposition. (Default if left empty)

(see separate task on connectors)

James: I have tried using the VHDL generator, it seems to work for some components but not all, is there an error log for it somewhere?

This is a request by James (via email on 8/1/2016)

The translation adds a prefix (component name) to the definition of wake kind.
But this prefix is missing in the generated invariants, and actions that use the wake kind

James: It appears that newly added Axioms to a refinement are propagated through subsequent refinements. I don't think this is quite right, an axiom is normally associated with a single refinement level isn't it?

The CODA model in a xmc composition machine should support modelling of the inclusion and event synch clauses.