Search results

Create the page "Work done" on this wiki! See also the search results found.

• Developer FAQ
  * In the "Work with" text entry, enter the full path to the downloaded Rodin developer arc For source plugins to work properly in a [[Using Rodin as Target Platform|target platform]] configurat
  15 KB (2,372 words) - 16:29, 19 May 2015
• D32 Model Animation
  More details about this work can be found in the following works: <ref>M. Leuschel, J. Falampin, F. Frit ...strial applications. In order to reach this level the contribution of this work consists of three parts:
  16 KB (2,553 words) - 15:12, 27 January 2011
• Scenarios for Merging Proofs
  Rodin is able, actually with a bit of work, to provide a ''reuse'' mechanism. This mechanism would allow to check, wit The only interaction envisioned is done after the merge, and is related to digging into [[proof history]]
  6 KB (1,046 words) - 10:34, 27 October 2011
• EMF framework for Event-B
  ...l, this makes it possible to write code that is more generic, since it can work on features without knowing which concrete meta-class the instance it is wo ...wish to support this established kind of behaviour for tools that need to work at a multi-component level.
  26 KB (3,961 words) - 13:04, 19 May 2020
• D45 General Platform Maintenance
  ...DEPLOY partners. The following paragraphs will give an overview of the the work that has been performed concerning maintenance on the existing platform com ...eady planned tasks coming from both DEPLOY partners and the Description of Work.
  35 KB (5,228 words) - 10:12, 23 April 2012
• D32 Modes and Fault Tolerance
  ...g activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tr
  5 KB (816 words) - 17:37, 3 December 2010
• Rodin Platform 1.1 Release Notes
  Bug 2105507: too difficult to work with explicit set expressions Bug 2656831: saving proofs does not always work
  9 KB (1,298 words) - 10:06, 28 July 2010
• File Root Separation
  The link between files and internal elements is done through a root element. A where file types and root elements coexist allows to work on the modification
  6 KB (897 words) - 11:47, 29 January 2009
• Rodin Index Design
  ...ses to define the granularity at which these indexers will be declared and work. Having an indexer declared and working on a whole project would be too co ...we rather queue them for later processing by the indexing thread. This is done through a blocking queue.
  14 KB (2,204 words) - 12:58, 12 October 2009
• D32 Provers
  The relevance filter heuristics we have considered do not work out of the box - their parameters need to be carefully adjusted. avoid expanding the trusted base of the sequent prover) but rather to work on
  11 KB (1,699 words) - 15:25, 27 January 2011
• Rodin Platform 1.3 Release Notes
  Bug 2656831: saving proofs does not always work Bug 2952959: Disabling auto-provers doesn't work
  12 KB (1,642 words) - 13:21, 28 July 2010
• D45 Scalability
  This section concerns the actual editors that user work with to view and modify models. ...REL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the earl
  13 KB (1,991 words) - 20:57, 20 April 2012
• D45 Prover Enhancement
  An interesting side-effect of our work is that the ProB toolset now provides a double-chain (relying on technology ...actic and reports the result back to Rodin. Most of the work that has been done concerned the study of Event-B theory and its translation to HOL. Unlike tr
  21 KB (3,334 words) - 21:20, 20 April 2012
• D23 General Platform Maintenance
  The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to
  7 KB (963 words) - 11:30, 27 January 2010
• ProR
  ...the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>
  6 KB (915 words) - 10:04, 21 June 2013
• Decomposition Plug-in User Guide
  ## In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-shar ...error exists in the decomposition file, the decomposition button will not work and the decomposition will not be run.
  17 KB (2,521 words) - 15:25, 4 July 2013
• Rodin Platform 1.2 Release Notes
  Bug 2105507: too difficult to work with explicit set expressions Bug 2656831: saving proofs does not always work
  11 KB (1,488 words) - 10:06, 28 July 2010
• Camille Editor
  ''This is how it should work. Unfortunately the update doesn't always notify the user properly. So we re
  6 KB (945 words) - 12:22, 27 January 2015
• Parallel Composition using Event-B
  ## In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-shar
  7 KB (1,161 words) - 11:02, 4 July 2013
• D32 Mathematical Extensions
  The Theory plug-in v2.1 is released. Work will continue on general maintenance, bug fixes as well adding new features
  7 KB (1,095 words) - 14:40, 21 December 2010
• Proof Manager
  2. '''Replayable''' A reasoner must work ''deterministically'', i.e. given the same input, a reasoner must generate
  9 KB (1,478 words) - 10:33, 27 October 2011
• Rodin Platform 3.2.0 External Plug-ins
  ...tyle="color:green"> available </span> || ?.x.x || || || (appears to still work - cfsnook 23/06/15)
  13 KB (1,514 words) - 14:38, 6 July 2017
• Rodin Platform 3.3.0 External Plug-ins
  ...e="color:#8B4513"> not checked</span> || ?.x.x || || || (appears to still work - cfsnook 23/06/15)
  13 KB (1,514 words) - 07:16, 2 September 2017
• Records Extension
  [[Category:Work in progress]] [[Category:Design]]
  8 KB (1,347 words) - 13:07, 21 July 2010
• Extending the Rodin Event-B Explorer (How to extend Rodin Tutorial)
  We continue our work on the UI integration of our plug-in and extend the Event-B Explorer view. ...nt)</tt> shall then return the <tt>Bound</tt> elements themselves. This is done via the method <tt>getChildren(Object parent)</tt>.<br>
  10 KB (1,424 words) - 07:15, 7 September 2010
• ADVANCE D3.3 General Platform Maintenance
  ...variants of UML-B. Classic UML-B is self contained (i.e. all modelling is done on the diagram) and a read-only Event-B project is automatically generated ...aspects to an extant Event-B machine (i.e. some of the modelling is still done in an Event-B machine). iUML-B currently provides a project diagram, and st
  16 KB (2,554 words) - 14:05, 8 October 2013
• Modularisation Plug-in
  The modules comprising a model are weaved together so that they work on the same global ...stage, the focus is always on a particular module. Thus, several teams may work on different modules simultaneously.
  18 KB (2,784 words) - 10:57, 6 September 2010
• D23 TEXT
  Rodin has done away with a textual representation of the formal models. ...ing/emf/ Eclipse Modelling Framework Project]) data model. It allows us to work with Event-B models independently of the persistence strategy. In addition
  8 KB (1,257 words) - 15:56, 28 January 2010
• Modus Ponens generalized
  * Its time execution is enormous because of the work that tactic performed (intrinsic), and because of the test realized to ensu
  10 KB (1,784 words) - 16:04, 18 March 2014
• D32 UML-B
  ...owever, the Records plug-in took longer than expected and this has delayed work on iUML-B. Some progress on iUML-B has recently been made with the release
  9 KB (1,382 words) - 11:05, 27 January 2011
• Rodin Keyboard User Guide
  ...s extensible) when there is a modification of the text. The translation is done for the whole text spanned over multiple lines. [[Category:Work in progress]]
  14 KB (1,930 words) - 12:58, 21 July 2010
• D32 Scalability
  ...g activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tr In this work one obvious source of inspiration is the Classical B method <ref name="bboo
  19 KB (2,944 words) - 15:28, 27 January 2011
• Code Generation Tutorial
  ...since it can give rise to exceptions. The PrettyPrinter would need further work to make it robust, however it is intended only as a short-term solution.
  12 KB (1,741 words) - 08:25, 14 December 2010
• Event-B Examples
  ...affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligati
  9 KB (1,283 words) - 13:58, 5 July 2017
• Rodin Proving Perspective
  To work on an un-discharged PO it is necessary to load the proof into the Proving P ...equent (the node and its subtree). Pasting the node and subtree back in is done in a similar manner, with a right mouse click on a proof node. This allows
  27 KB (4,348 words) - 08:56, 26 September 2011
• The Proving Perspective (Rodin User Manual)
  To work on an un-discharged PO it is necessary to load the proof into the Proving P ...equent (the node and its subtree). Pasting the node and subtree back in is done in a similar manner, with a right mouse click on a proof node. This allows
  27 KB (4,348 words) - 18:45, 28 September 2011
• Sequent Prover Developer Guide
  [[Category:Work in progress]]
  17 KB (2,378 words) - 09:48, 17 June 2010
• Pattern
  ...ctical checking is easier than doing proofs, especially if they have to be done manually. Once all checks are done, the refinement of the problem is generated by merging the pattern refineme
  17 KB (2,670 words) - 15:07, 24 January 2012
• Event-B Statemachines
  ...envisioned as ancilliary to a regular Event-B model, all modelling can be done from the diagram if so desired. [Note that only guards may be added to tran ...ors because the link to the abstract implicit context is not maintained. A work-around is to translate the statemachine of the middle refinement even thoug
  13 KB (2,134 words) - 08:04, 6 October 2015
• Extending the Static Checker
  monitor.done(); ...essary to define the checks that are required for each element and this is done by providing an extension to <tt>org.eventb.core.configurations</tt>.
  24 KB (3,013 words) - 16:24, 5 July 2011
• Migration to Eclipse 3.6
  ...handler. This does not affect <tt>ActionSets</tt>, which will continue to work with key bindings when active within a perspective. ...nteger value as the valid range for a Spinner is valid, so this can now be done.
  12 KB (1,814 words) - 08:44, 30 June 2010
• Rodin Platform 2.0 Release Notes
  :Update the compiler settings to be compliant with level 1.6. This can be done in '''Window > Preferences > Java > Compiler'''. Bug 2105507: too difficult to work with explicit set expressions
  15 KB (2,008 words) - 15:34, 10 January 2011

View (previous 100 | next 100) (20 | 50 | 100 | 250 | 500)