Search results

From Event-B
Jump to navigationJump to search

Page title matches

  • This page is here to describe the work that I started, but which is yet to be finished. ...ath> and <math>\upred</math> are proceeded. But, more re-writing should be done. Unfortunately, I did not take too much time to analyze all the possibiliti
    10 KB (1,685 words) - 11:50, 26 February 2013

Page text matches

  • [[Category:Work in progress]]
    140 bytes (19 words) - 09:40, 4 March 2009
  • ...cument intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during t The document is divided according to the work package tasks: general platform maintenance, improvement of automated proof
    2 KB (325 words) - 17:32, 29 November 2013
  • ...r November 7th and 8th, 2013 the industrial partners which are involved in work packages 1 and 2 expressed their tooling needs to support the case studies. == Common needs across both work packages ==
    4 KB (677 words) - 16:41, 2 December 2013
  • ...cument intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during t ...ss the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).
    2 KB (371 words) - 16:27, 13 July 2012
  • ...over. The rules are added using as various plug-ins with most of the work done in a declarative fashion. Moreover the new features are also tested using t The work is related to the following rewriting rule:
    4 KB (738 words) - 12:53, 12 August 2009
  • ...rview of the work done within the WP9 ''Tooling research and development'' work package, during the fourth and last period of the DEPLOY project (Feb 2011- ...zed, and periodically updated to both fit with the original Description of Work (DoW) and give answers to DEPLOY partner issues.
    3 KB (500 words) - 09:18, 23 April 2012
  • ...the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), a ...ber of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the generation of well-de
    3 KB (415 words) - 17:03, 24 November 2010
  • ...stall other items but if you install the Java HL client adapter it may not work for models and you may need to change the preferences to SVNKit) Currently the EMF compare editor does not work with the team-synchronise with repository view.
    3 KB (445 words) - 07:03, 1 August 2011
  • A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenc 2. copy/paste one of the following scripts (both should work; if one does not, just try the other one) :
    2 KB (321 words) - 13:25, 3 February 2010
  • The work on the development of a flash-based file system in Event-B is reported in a ...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
    4 KB (656 words) - 13:06, 18 November 2010
  • This work is planned for project year 2. This chapter introduces the main requirement [[Category:Work in progress]]
    2 KB (308 words) - 16:35, 17 December 2008
  • 3. '''Work around''': we show a solution (rather a work-around) for the current RODIN Platform. In order to finish the proof, a correct "proof by cases" is done to consider <math>a = 1</math> or <math>a \neq 1</math>.
    4 KB (545 words) - 22:17, 5 March 2010
  • == Description of Work and Progress == ...te page [[Documentation Overhaul DoW]] that lists the Description of Work, Work Packages and their progress.
    5 KB (720 words) - 11:28, 15 September 2011
  • ...cking on the transition name inside the statemachine figure. (This dosen't work for nested statemachines because they do not appear on the class diagram).
    778 bytes (122 words) - 12:15, 4 March 2009
  • # doing this does not work because the text compare editor opens in preference (I think this is becaus ...ent type extensions (rodin core, eventb core etc) but this did not seem to work
    4 KB (623 words) - 19:48, 24 September 2009
  • ...[http://decert.gforge.inria.fr/deliverable/D1-RequirementAnalysis-2009.pdf Work Package 1] of the project. Using the [http://www.smtlib.org/ SMT-LIB] stand ...eoretic constructs from each other and simplifies predicates. Once this is done, the Event-B Abstract Syntax Tree to be translated in SMT-LIB is restricted
    5 KB (797 words) - 10:29, 24 October 2011
  • ...:green"> available </span> || ?.x.x || || || Checked and appears to still work in Rodin 3.4 - cfsnook 12/12/09 ...aurent.voisin@systerel.fr Laurent Voisin] || Checked and appears to still work in Rodin 3.4 - cfsnook 12/12/09
    6 KB (855 words) - 16:00, 12 December 2019
  • The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext
    785 bytes (113 words) - 23:20, 21 July 2017
  • [[Category:Work in progress]]
    1 KB (160 words) - 20:27, 10 March 2009
  • ...9-Jan 2010), in the course of the WP9 ''Tooling research and development'' work package, and brings new perspectives for the coming year.
    3 KB (399 words) - 11:20, 27 January 2010
  • an overview of the work done and of some of the results. == Description of Work ==
    6 KB (967 words) - 12:57, 28 October 2008
  • ...mplementation-oriented view. That is, it would be nicer if extenders could work at a more model-oriented level and not have to understand (and get right) d ...ng new attributes and collections to this subclass. However, this does not work retrospectively for previously created models. Also, extensions are effecti
    7 KB (1,094 words) - 10:50, 22 January 2010
  • Rodin will work on the following operating systems ...on 11 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
    4 KB (640 words) - 14:09, 25 May 2021
  • The work of the project will be driven by the tasks of achieving and evaluating indu
    1 KB (174 words) - 11:11, 18 September 2008
  • [[Category:Work in progress]]
    1 KB (176 words) - 07:06, 1 August 2011
  • It would be great if two people work independtly on different proofs that the discharged proof obligations could
    1,010 bytes (157 words) - 10:00, 22 October 2009
  • * There is work in progress towards support of the upcoming 2.0 version of the Theory plug- The work on physical unit support has been completed and is available as an optional
    6 KB (1,016 words) - 10:41, 23 September 2013
  • ...le will give to the project reviewers some insight on what happened in the work package 3, concerning its 3 main objectives: ...created (see [[#Contents | Contents]]) to give a brief description of the work that was carried on during second period of the project (Sept 2012-Sept 201
    6 KB (830 words) - 13:21, 7 October 2013
  • Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
    1 KB (162 words) - 19:48, 17 October 2010
  • ...e development platform. There is currently two plug-ins that are known to work quite well: [http://subclipse.tigris.org/ Subclipse] and [http://www.eclips Note that the filtering on <tt>CVSROOT</tt> didn't seem to work as expected: this directory still occurred in the SVN trunk and had to be r
    4 KB (710 words) - 09:37, 1 April 2009
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. ...isplay a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be installed.
    6 KB (899 words) - 16:25, 9 July 2014
  • * [[:Category:Work in progress]]
    2 KB (179 words) - 09:17, 20 November 2013
  • ...on in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports acc The need for constraint-based deadlock checking arose in the automotive work package, more precisely during the elaboration of the cruise control system
    7 KB (1,025 words) - 21:35, 20 April 2012
  • ...tigate a version of MBT using Event-B models as test models. This research work provides a new feature in the Rodin platform, complementing the existing th ...were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of va
    8 KB (1,215 words) - 15:14, 27 January 2011
  • [[Category:Work in progress]]
    1,001 bytes (119 words) - 14:53, 21 January 2010
  • Rodin will work on the following operating systems ...on 11 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
    5 KB (703 words) - 14:37, 29 April 2022
  • ...pton, Hitachi Ltd. and ETH Zurich are discussing on how to consolidate the work and merge the two plug-ins.
    2 KB (232 words) - 15:23, 4 July 2013
  • For source plugins to work properly in a [[Using Rodin as Target Platform|target platform]] configurat ...hat the workspace is in the release revision (no further commits have been done). If this is not the case, switch the workspace into the release revision.
    2 KB (237 words) - 14:58, 10 March 2011
  • In the last year of DEPLOY, the work done on MBT proceeded according to the plan (summarized in the previous delivera ...fits well with the notion of Event-B refinement. It can also be adapted to work with decomposed Event-B models.
    7 KB (1,044 words) - 21:39, 20 April 2012
  • [[category:Work in progress]]
    1 KB (215 words) - 12:08, 12 August 2009
  • ...e improved. We like working on this project because this project makes our work more effective, and we hope you'll like it, too. Showing your motivation he == Getting things done ==
    10 KB (1,629 words) - 12:50, 12 August 2009
  • ...invite all the academic and industrial partners to submit papers about the work they carried out inside the DEPLOY project. ...purposes inside the DEPLOY community. Copyright is not an issue since the work will not be formally published and the presentation will remain internal to
    7 KB (1,003 words) - 20:08, 12 October 2009
  • ...uite old previous version that was shipped and the good work that has been done since on the prover.
    2 KB (281 words) - 15:57, 11 September 2017
  • ...]]. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become avai [[Category:Work in progress]]
    5 KB (738 words) - 09:13, 4 March 2009
  • ; (S-2) Multiple users work concurrently on an Event-B Project: In this scenario, it is expected that s ...file. This still leaves open the issue of how to enable multiple users to work on proofs a the same time. If every proof is represented by a single file,
    4 KB (670 words) - 14:38, 29 January 2009
  • ...ss variables and less events and less proof obligations. This partition is done in a way that the sub-models (also referred as sub-components) are independ ...ning and revision control, provided by the SVN system. It was difficult to work on models in parallel and manage changes made by different parties, especia
    5 KB (780 words) - 11:22, 21 December 2010
  • This page sum up the developments recently done around or for the [[Rodin Platform]], which are integrated or compatibles w [[User:Maria|Maria Husmann]] was in charge of this exploratory work during her internship at [http://www.systerel.fr Systerel].
    6 KB (915 words) - 16:57, 27 February 2014
  • Rodin will work on the following operating systems ...ion 8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
    8 KB (1,249 words) - 13:09, 11 September 2020
  • Rodin will work on the following operating systems ...on 11 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
    5 KB (775 words) - 12:00, 4 April 2023
  • ...ay for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them. ...nstance), mainly because of time constraints (in the DEPLOY description of work, the decomposition support is planned for end of 2009).
    6 KB (825 words) - 13:27, 27 January 2010
  • Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
    1 KB (216 words) - 15:46, 28 January 2011
  • * Click on the '''Work with''' dropdown list and select the Atelier B provers update site.
    2 KB (322 words) - 16:45, 20 April 2010
  • ...ting file dependencies is delegated to indexers (however, if it is already done by indexers that run before yours, there is no need to do it twice, simply ...ndexer depends on others (see below), you can also get the result of their work.
    6 KB (969 words) - 13:17, 29 May 2009
  • Bug #3086746: Functional Image Rewrites does not work properly
    2 KB (248 words) - 15:58, 16 November 2010
  • This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations abo ===== Work already performed =====
    12 KB (1,869 words) - 16:35, 18 March 2014
  • ...(resp. corrective maintenance) has its origin in the DEPLOY description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, dev ...ks are processed in the same way as the task planned in the description of work.
    9 KB (1,423 words) - 16:28, 14 November 2011
  • ==Initial Work == Initial work towards implementation of this framework is described in [http://stups.hhu.
    11 KB (1,773 words) - 07:41, 12 January 2016
  • ...conflicts with the more general definition of bridges the prover will not work properly. (It would be better if the type axiom for bridges was minimal and
    2 KB (386 words) - 22:23, 11 December 2008
  • ...RE (8 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE. : Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents t
    5 KB (758 words) - 16:28, 7 March 2018
  • ...all Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site availabl === Ongoing Work ===
    17 KB (2,568 words) - 09:03, 19 October 2015
  • ...of work for DEPLOY that was not identified in the original Description of Work for the project. During the first year of the project, as the Deployment P The code generation work is being lead by Southampton with initial input from Newcastle.
    11 KB (1,725 words) - 18:07, 7 December 2009
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. : Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents t
    6 KB (909 words) - 13:48, 17 December 2014
  • [[Category:Work in progress]]
    2 KB (320 words) - 07:06, 1 August 2011
  • * There is work in progress towards full support of Theory plug-in: support for external an The latter is particularly important in light of the Theory plug-in work.
    11 KB (1,711 words) - 09:47, 26 June 2012
  • ...ect Explorer. In order to work with the Requirements Plug-In, you need to work with the Navigator View. You can open it via Window > Show View > Other... ...te 1:''' While Identifier and Document can be edited here, it shouldn't be done (changes will be lost upon next synchronization).
    7 KB (995 words) - 15:44, 25 February 2009
  • The recommended practice is to work with a target platform, as described in how to adapt plug-ins that work with Rodin 2.7 to the new 3.0 API.
    8 KB (1,260 words) - 12:45, 30 July 2015
  • ...umber of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Dec ...mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will
    15 KB (2,298 words) - 15:08, 27 January 2011
  • obligation <tt>FIS</tt> is supposed to work as a filter and prevent models from [[Category:Work done]]
    8 KB (1,284 words) - 18:33, 30 January 2012
  • Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
    2 KB (353 words) - 12:45, 12 August 2009
  • ...h or a path relative to the search path or a path relative to your current work directory. * Support for Windows is limited. Export of proof obligations does work. Invoking Isabelle from Rodin does not. The problem is to launch Isabelle t
    9 KB (1,317 words) - 10:07, 29 April 2013
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. ...isplay a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be installed.
    10 KB (1,328 words) - 16:14, 3 August 2012
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. ...isplay a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be installed.
    11 KB (1,542 words) - 08:35, 1 March 2012
  • :* '''IUserSupport API simplification''': some operations of the user support work only on the proof tree in main memory. Therefore, they cannot raise any Rod ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE.
    11 KB (1,478 words) - 17:32, 2 May 2012
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. ...isplay a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be installed.
    10 KB (1,301 words) - 07:11, 29 August 2013
  • ...y, the Camille editor is very strict on dependencies, so although it would work fine with a minor update, it has to be removed before you can install the n
    3 KB (469 words) - 14:17, 21 October 2009
  • ...nts (plug-in contributers) will be allowed to select the mode they want to work with. This verification will be done as follows: Check each occurrence of the <tt>typeCheck()</tt>, <tt>isTypeC
    3 KB (431 words) - 15:14, 18 February 2010
  • ...unterexamples for proof obligations. Searching for a counterexample can be done effortlessly and without user interaction. If successful, the futility of a ...enumerations, ProB is able to tell if the search for a counterexample was done exhaustively. If this is the case, the proof obligation in question is disc
    7 KB (1,145 words) - 10:05, 8 October 2013
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. * Linux: the internal browser does not work with xulrunner-2.0 (for instance, it causes the welcome page to display a l
    11 KB (1,401 words) - 09:39, 8 November 2011
  • [[Category:Work in progress]]
    3 KB (496 words) - 12:58, 12 August 2009
  • '''This did not work. It is not possible to dynamically add to statically generated EMF classes.
    6 KB (506 words) - 12:00, 25 November 2009
  • ...is due to limitations in Eclipse p2 (about conflict resolutions) and would work only if no plug-ins are installed... which makes it close to useless ! ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE.
    8 KB (1,195 words) - 16:35, 9 July 2014
  • ...va JRE (8 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. : Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents t
    7 KB (1,079 words) - 13:54, 12 July 2017
  • This page describes work done for optimising well-definedness lemmas generated by the Core Rodin platform
    4 KB (617 words) - 09:43, 19 June 2012
  • The following paragraphs will give an overview of the the work that has been performed concerning maintenance on the existing platform com Work on release 3.0 will start concurrently with development of Rodin 2.7 and wi
    20 KB (3,030 words) - 13:18, 18 July 2012
  • ...only wish to update some fields and leave others changed, this needs to be done by specifying explicitly that some fields This can be done by including the new field ''g'' as projection function on ''R'' in a cont
    18 KB (2,643 words) - 12:41, 12 August 2009
  • ...evelopment of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B model ...tten. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation techno
    12 KB (1,818 words) - 08:31, 20 April 2012
  • Furthermore, the work was driven by requirements of Siemens and SAP; some tool development was al This required a considerable amount of work on improving the scalability of the ProB kernel, to be able to deal with la
    17 KB (2,580 words) - 15:55, 28 January 2010
  • ...platform in the order given above, otherwise links to source files do not work correctly in Eclipse.
    4 KB (678 words) - 05:58, 24 October 2014
  • have been found to work well.
    4 KB (569 words) - 07:04, 1 August 2011
  • ...eral platform performance.''' One of the main task of the scheduled future work, concerning the maintenance and evolution of Rodin, is to increase the plat ...se it]] and [[Preferences_for_the_automatic_tactics | the page on the work done about Preferences for the automatic tactics]]
    10 KB (1,277 words) - 13:45, 26 July 2011
  • Select the main Rodin Update site from the "work with:" field in the Help > Install New Software menu in Rodin. ...hoice. The latex documents are generated in the 'latex' folder like it was done in other previous releases.
    4 KB (718 words) - 17:22, 8 July 2016
  • * The plug-in cannot work alongside any other plug-in contributing SC and POG modules. It will try to
    4 KB (601 words) - 23:58, 13 October 2009
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. * Linux: the internal browser does not work with xulrunner-2.0 (for instance, it causes the welcome page to display a l
    10 KB (1,354 words) - 13:31, 1 July 2011
  • We expect that during this work, the rest of the documentation will start to fill up with placeholders (e.g ...roduce a guideline for Plugin developers for including references to their work in the handbook.
    9 KB (1,421 words) - 12:41, 8 December 2011
  • This page is here to describe the work that I started, but which is yet to be finished. ...ath> and <math>\upred</math> are proceeded. But, more re-writing should be done. Unfortunately, I did not take too much time to analyze all the possibiliti
    10 KB (1,685 words) - 11:50, 26 February 2013
  • ## In the ''Work with'' dropdown list, choose the location URL: Rodin
    5 KB (720 words) - 15:20, 4 July 2013
  • ...er Science at the University of Southampton (especially the organisational work of Maggie Bond), the DEPLOY project and additional government funding.
    5 KB (766 words) - 09:59, 21 September 2011
  • *: Also, internship positions are open to work in industry applying Formal Methods. Please contact Dinho (agrj@aes.com.br)
    5 KB (718 words) - 11:40, 23 October 2015
  • [[Category:Work in progress]]
    4 KB (671 words) - 12:45, 12 August 2009
  • ...JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. : Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents t
    9 KB (1,317 words) - 11:09, 6 July 2017
  • * 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
  • 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
  • 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
  • ...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
  • ...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
  • ...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
  • 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
  • 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
  • ...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
  • 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
  • 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
  • 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
  • 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
  • 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
  • ...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
  • ## 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
  • 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
  • ''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
  • ## 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
  • 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
  • 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
  • ...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
  • ...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
  • [[Category:Work in progress]] [[Category:Design]]
    8 KB (1,347 words) - 13:07, 21 July 2010
  • 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
  • ...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
  • 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
  • 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
  • * 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
  • ...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
  • ...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
  • ...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
  • ...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
  • ...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
  • 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
  • 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
  • [[Category:Work in progress]]
    17 KB (2,378 words) - 09:48, 17 June 2010
  • ...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
  • ...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
  • 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
  • ...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
  • :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