Search results
From Event-B
Jump to navigationJump to searchCreate the page "User page" on this wiki! See also the search results found.
- <div id="accueil_title">{{Main Page/title}}</div> <div align="right" class="main_page_frame_link">[[Template:Main Page/title|Edit]]</div>2 KB (194 words) - 09:48, 19 May 2020
- ...just a private place for some tests towards a hopefully fullfeatured Main Page'' [[Rodin Platform|Rodin Platform User Support]]295 bytes (39 words) - 22:09, 4 July 2008
- ...Any modification to this page shall be announced on the [[#Mailing_lists |User]] mailing list!</font> This page groups together all the rewrite rules implemented (or planned for implement739 bytes (98 words) - 13:29, 26 April 2013
- This page gives a brief summary of documents describing Event-B's modeling notation. [[Category:User documentation]]410 bytes (54 words) - 08:45, 27 October 2011
- ...cumentation for users of the plug-in is available in [[Theory Plug-in|this page]]. ...and list the release in [[Template:Dev News]] (it is included in the front page)3 KB (394 words) - 07:15, 15 July 2021
- ...predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions). The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as t4 KB (642 words) - 08:33, 29 June 2012
- ==11th Rodin User and Developer Workshop== The 11th Rodin User and Developer Workshop, 25th June, 2024, Bergamo, Italy3 KB (368 words) - 12:49, 15 April 2024
- ...predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions). The Theory plug-in provides, among other things, a user-friendly mechanism to extend the Event-B mathematical language as well as t4 KB (648 words) - 14:52, 7 October 2013
- This page gives a brief summary of tutorial documents for Rodin and other Plug-ins. [[Category:User documentation]]617 bytes (79 words) - 08:47, 27 October 2011
- The user must give a value for each constants. A constant value is set in the contex * a page for each model4 KB (679 words) - 14:59, 16 September 2009
- ...n is broadcasted on the [[Mailing_lists | Announce]] and [[Mailing_lists | User]] mailing lists. ...g-ins are spread on the [[Mailing_lists | Announce]] and [[Mailing_lists | User]] mailing lists.4 KB (532 words) - 06:51, 4 April 2023
- ...nd parameterized tactics to discharge some specific proof obligations. The user can furthermore share and backup these defined tactics using the provided i ...n the tactic profile editor as well as an import/export feature. Indeed, a user that elaborates a good profile for a certain proof pattern is now able to s4 KB (596 words) - 13:21, 18 July 2012
- Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platf ...Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page). In particular:7 KB (963 words) - 11:30, 27 January 2010
- ...composition_Plug-in_User_Guide Atomicity Decomposition Plug-in User Guide] page for tool support details.1 KB (166 words) - 15:46, 7 August 2012
- This page provides extensive documentation for the rule-based prover plug-in. == User Documentation ==2 KB (338 words) - 17:11, 9 July 2010
- ...predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions). ...ies are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.7 KB (1,095 words) - 14:40, 21 December 2010
- This page gives a brief summary of documents describing Event-B's logic aka mathemati [[Category:User documentation]]1 KB (203 words) - 11:28, 23 January 2014
- This page has been created to give a wish list of tool plug-ins that cannot be resour ...llowing list has been established during the [[Rodin_Workshop_2009 | Rodin User and Developer Workshop 2009]] (July 15-17 2009):983 bytes (138 words) - 12:16, 3 July 2017
- This page is a first tentative to describe the scenario that a merge tool will have t ...all ''L'' the ''local'' database/user/branch, ''O'' the ''other'' database/user/branch and ''A'' the database which reflects the common state from which ''6 KB (1,046 words) - 10:34, 27 October 2011
- This page describes the text syntax for Event-B models in the TextEditor. It shows it See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.4 KB (559 words) - 12:43, 12 August 2009
- ...ularly or watching this page for changes. We will announce updates on this page too.'' To get a first impression also visit the [[TextEditor Screenshots|screenshot page]].6 KB (945 words) - 12:22, 27 January 2015
- ''This page is under development'' ...of the element. This contains details which are otherwise hidden from the user.3 KB (507 words) - 07:02, 1 August 2011
- This page documents the procedure followed for building the binary packages of the Ro # the full platform version used for provisioning, and which is the user-visible version which is displayed in ''About Rodin Platform''. This versio6 KB (928 words) - 15:50, 11 September 2020
- The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to pr DetailsPageProvider : returns the sequent details page when a proof tree node is selected2 KB (254 words) - 12:54, 12 August 2009
- The intention of this page is to collect and discuss possible improvements of the layout in the event- In a user feedback report posted on the Deploy WP9 mailing list, Michael Leuschel rep1 KB (215 words) - 12:08, 12 August 2009
- The complete Event-B XText Front-end User Guide is available as pdf [https://sourceforge.net/projects/rodin-b-sharp/f ...of this editor, see [[Event-B_XText_Front-end|the Event-B XText Front-end page]].<br>2 KB (231 words) - 23:27, 21 July 2017
- This page sum up the developments recently done around or for the [[Rodin Platform]], ...a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants).6 KB (915 words) - 16:57, 27 February 2014
- The purpose of this page is to give a common structure and guidelines to collaboratively build the A ...g second period of the project (Sept 2012-Sept 2013). The contents of each page should not go deeply into technical details, but should rather look like an6 KB (830 words) - 13:21, 7 October 2013
- The CamilleX User Guide is available as pdf '''[https://sourceforge.net/projects/rodin-b-shar ...ore details about the principles on CamilleX, see the [[CamilleX|CamilleX page]].<br>2 KB (281 words) - 12:31, 9 March 2023
- [[User:afuerst]] at '''ETH Zurich''' is in charge of the [[Pattern]] plug-in. As there are usually multiple guards and action in an event, the user has (at the current state of the tool) to declare which guards and actions17 KB (2,670 words) - 15:07, 24 January 2012
- This page describes the requirements for a '''parameterizable lexical analyser''' (i. mathematical language syntax can be extended by the final user.3 KB (440 words) - 09:10, 1 March 2010
- In this page are presented various proof obligations commands that can be run from the E ...discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially).3 KB (457 words) - 10:43, 18 March 2010
- '''Minimize the access to an expert a user of Event-B/Rodin needs to be productive.''' We maintain a separate page [[Documentation Overhaul DoW]] that lists the Description of Work, Work Pac5 KB (720 words) - 11:28, 15 September 2011
- Below we list some guidelines of how to prevent such problems. This page will be continuously updated. [[Category:User documentation]]2 KB (287 words) - 08:56, 27 September 2010
- ==10th Rodin User and Developer Workshop== The 10th Rodin User and Developer Workshop, 30th May, 2023, Nancy, France3 KB (375 words) - 15:36, 26 May 2023
- ...and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities. ...olymorphic theorems. The [http://wiki.event-b.org/images/Theory_Plugin.pdf user manual] provides a guide to developing and using theories.7 KB (958 words) - 14:53, 14 June 2021
- ...of proof trees, one can have a look at the [[Proof_Manager|Proof Manager]] page. But before the user saves its proof, he or she is modifying it, so the proof is unstable and un3 KB (496 words) - 12:58, 12 August 2009
- This short help page provides necessary information on the Rodin Keyboard plug-in and also on ho ...the Unicode characters for the mathematical language. From the Preferences page, you can choose the font, the style and the size for the text area.14 KB (1,930 words) - 12:58, 21 July 2010
- ...iki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page for technical details. ...iki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page). This is done by right-clicking on the machine and launch ''Atomicity Deco6 KB (912 words) - 15:13, 21 August 2012
- This page sum up the known developments that are being done around or for the [[Rodin The efforts in [[Düsseldorf]] ([[User:Fabian|Fabian]]) and [[Newcastle]] ([[User:Alexei|Alexei]]) have been joined to create a single text editor which will12 KB (1,869 words) - 16:35, 18 March 2014
- [[User:Son]] is in charge of the plug-in. ...e Probability, see the [[Qualitative Probability | Qualitative Probability page]].6 KB (749 words) - 17:54, 21 March 2018
- ...://wiki.event-b.org/index.php/Generic_Instantiation Generic Instantiation] page for technical details. ## Click ''Next'', after some time, the ''Install Details'' page appears5 KB (720 words) - 15:20, 4 July 2013
- ...ared, prover behaviours were only determined by a sequent and optionally a user input. Several features of the platform now require extra information: Similarly, when the user profile metatactic knows which project it is applied to, it can call the pr4 KB (600 words) - 14:09, 15 December 2010
- ...uld be read in conjunction with the [[Structured_Types|Structured Types]] page which gives a more theoretical description of the origin of the Records ext ...aining record elements. Hence the translated Event-B is not visible to the user.8 KB (1,347 words) - 13:07, 21 July 2010
- = Rodin User and Developer Workshop, University of Duesseldorf, 20-22 September 2010 = :Extending the pretty print page5 KB (716 words) - 09:28, 22 November 2010
- Animation allows the user to validate if the model corresponds to the user's intentions. ...rnal functions entry in ProB user manual</ref> have been added to the ProB user manual.11 KB (1,711 words) - 09:47, 26 June 2012
- ...t visible as a tab on the top right-hand corner of the main interface, the user can switch to it via "Window -> Open Perspective". ...at is not discharged yet by the prover. Instead, it has been "seen" by the user who decided to postpone the proof. Marking nodes as "reviewed" is very conv27 KB (4,348 words) - 08:56, 26 September 2011
- ...t visible as a tab on the top right-hand corner of the main interface, the user can switch to it via "Window -> Open Perspective". ...at is not discharged yet by the prover. Instead, it has been "seen" by the user who decided to postpone the proof. Marking nodes as "reviewed" is very conv27 KB (4,348 words) - 18:45, 28 September 2011
- Go to the [[Modularisation Plug-in|plug-in description page]]. ...just the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example,8 KB (1,166 words) - 20:58, 10 November 2009
- * set options in the bottom of the page: User Release date : 2011/07/22.3 KB (398 words) - 15:31, 22 July 2011
- ...s'', and unfold the SMT section in order to display the ''Configurations'' page. ...erences, and unfold the SMT section in order to display the Configurations page.17 KB (2,538 words) - 15:41, 2 October 2017
- | [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.2.6 || <span style="color:green"> available</s ...22nd Mar. 2012|| [mailto:ae2@ecs.soton.ac.uk email] ||*See Code Generation page for details of a compatibility issue.12 KB (1,324 words) - 13:37, 3 June 2013
- ...r instance, it causes the welcome page to display a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be instal * set options in the bottom of the page:6 KB (899 words) - 16:25, 9 July 2014
- * set options in the bottom of the page: User Release date : 2011/08/01.4 KB (515 words) - 08:41, 1 August 2011
- ...t the general functionality, please visit the [http://eclipse.org/rmf/ RMF page] at eclipse.org. In particular, the short video there provides a quick ove * <span style="color:red;">Red</span> marked text passages reminds the user that an undeclared identifier is used.6 KB (915 words) - 10:04, 21 June 2013
- A user builds and checks a Mode/FT view in the diagram editor, makes a link to an ...ilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework fo5 KB (816 words) - 17:37, 3 December 2010
- # User selects element to be renamed at the Event-B Explorer # User introduces new element name in the first page of the wizard. Then click in 'Next'. [[Image:new_name_wizard2.png|400x350px11 KB (1,773 words) - 07:41, 12 January 2016
- * [[Teamwork Requirements|Feedback Page/Ideas for requirements]] [[Category:User documentation]]3 KB (445 words) - 07:03, 1 August 2011
- * set options in the bottom of the page: User Release date : 15/03/2011.3 KB (395 words) - 13:15, 1 June 2011
- ''See also the [[Talk:Scenarios for Team-based Development|associated talk page]] for discussion about this topic.'' ...n this scenario it is sufficient if access for editing is granted only one user at a time.4 KB (670 words) - 14:38, 29 January 2009
- The code snippets on this page are derived from the UML-B plugin 'ac.soton.umlb.eventB', package 'generato ...not strictly necessary but it can be used to distinguish projects that the user has created from ones that have been created programmatically).6 KB (784 words) - 15:19, 21 August 2023
- ...//handbook.event-b.org/current/html/preferences.html] at the bottom of the page). ...r instance, it causes the welcome page to display a link instead of a html page); xulrunner-1.9.x must be installed.11 KB (1,401 words) - 09:39, 8 November 2011
- === Event-B User Interface === The Event-B User Interface of the Roding Platform has two major components that are concerne8 KB (1,260 words) - 12:45, 30 July 2015
- ...experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be This section concerns the actual editors that user work with to view and modify models.13 KB (1,991 words) - 20:57, 20 April 2012
- ...tig machine/context the component is created on-the-fly without asking the user. Partly caused by a bug in the EMF persistence for Event-B. ...he special editing mode for the template is left to quickly, i.e., without user interaction.6 KB (800 words) - 08:50, 19 August 2014
- ...over, as soon as a new feature is added to the platform, the corresponding user documentation is created on the Wiki.9 KB (1,423 words) - 16:28, 14 November 2011
- ...ent-b.org/index.php/Event_Model_Decomposition Event-B Model Decomposition] page for technical details on ''shared variables'' (A-style) decomposition. ## Click ''Next'', after some time, the ''Install Details'' page appears17 KB (2,521 words) - 15:25, 4 July 2013
- ...dedicated [[Rodin_Editor| wiki page]] and its [[Rodin_Editor_User_Guide | user guide]]. ...r instance, it causes the welcome page to display a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be instal10 KB (1,328 words) - 16:14, 3 August 2012
- This page describes how to measure the performance of SMT solvers linked to the Rodin ...> packaged with the Rodin platform. This makes the tests closer to the end-user experience, and therefore more meaningful.4 KB (652 words) - 08:48, 6 June 2014
- ...feel that this chapter requires a lot of diligence. Also, we will perform user tests with the tutorial, once created. ...e that the mathematical background exists, introduce the GUI and guide the user through a few modeling sessions.9 KB (1,421 words) - 12:41, 8 December 2011
- :* '''IUserSupport API simplification''': some operations of the user support work only on the proof tree in main memory. Therefore, they cannot ...r instance, it causes the welcome page to display a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be instal11 KB (1,478 words) - 17:32, 2 May 2012
- ...r instance, it causes the welcome page to display a link instead of a html page); xulrunner-1.9.x must be installed. * set options in the bottom of the page:10 KB (1,354 words) - 13:31, 1 July 2011
- :'''Import/export profiles''': from the tactic preference page, profiles can be exported and imported to/from the file system ...r instance, it causes the welcome page to display a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be instal11 KB (1,542 words) - 08:35, 1 March 2012
- ...r instance, it causes the welcome page to display a link instead of a html page and the '''Pretty Printer''' does not work); xulrunner-1.9.x must be instal * set options in the bottom of the page:10 KB (1,301 words) - 07:11, 29 August 2013
- ...Instead, come up with your own proposal, or expand on a proposal from this page. Explore the code a little bit. Make a clear schedule to show the intermedi ...the Rodin platform uses self-made automatic theorem provers to support the user in proving.10 KB (1,629 words) - 12:50, 12 August 2009
- ...teps as possible automatically or at least supports the developer wherever user interaction is required. ...documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.6 KB (1,034 words) - 14:43, 27 January 2010
- A dedicated page [[Element Hierarchy Extension Point & Library]] exist and documents the per 636 Typo in Rodin User's Handbook, range restriction8 KB (1,195 words) - 16:35, 9 July 2014
- This tutorial walks the user through using the Systerel Requirements Plug-In for Rodin. This Plug-In al * On the next page, select "ProB update site" and click Finish7 KB (995 words) - 15:44, 25 February 2009
- ...Any modification to this page shall be announced on the [[#Mailing_lists |User]] mailing list!</font> ...\;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(S)}</math> || the user has to write the set corresponding to <math>T</math> in the editing area of36 KB (5,611 words) - 10:22, 1 February 2024
- ...f [http://en.wikipedia.org/wiki/Wizard_%28software%29 wizard], guiding the user step by step toward ''test suite generation'', starting with the most abstr The first step requires the user to specify the value for the ''maximum sequence length'' constant (<math>l<9 KB (1,434 words) - 06:45, 6 April 2012
- ...arser is available from the [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page]. ...s] (Note that the 2.0 version is not supported because it does not support user-defined attributes).5 KB (797 words) - 10:29, 24 October 2011
- * [[User:Steve| Steve Wright]], [http://www.cs.bris.ac.uk/~eder/ Kerstin Eder] and [ ...ch project, please feel free to add a short description and a link to this page.'''</span>5 KB (718 words) - 11:40, 23 October 2015
- User defined foreground color and comment foreground color are now taken into ac set options in the bottom of the page:9 KB (1,317 words) - 11:09, 6 July 2017
- ...ns in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate There is a dedicated wiki page covering the plug-in functionality:5 KB (796 words) - 11:44, 8 January 2010
- ...been provided in such case, taking the form of warnings or errors that any user can understand and review. ...ductive using Event-B and the Rodin toolset. The contents of the handbook, user oriented, were originated by some contents of the Event-B wiki.35 KB (5,228 words) - 10:12, 23 April 2012
- ...t-tactic|How to use it]] and [[Preferences_for_the_automatic_tactics | the page on the work done about Preferences for the automatic tactics]] Bug 3164796: Goal Page does not react to font changes10 KB (1,277 words) - 13:45, 26 July 2011
- This page contains descriptions of the available proof tactics within the RODIN Platf * '''[[The Proving Perspective (Rodin User Manual)#The Automatic Post-tactic|Post-tactic]]''': ''No'': the tactic cann57 KB (6,150 words) - 17:25, 21 February 2012
- ...ad to be made. In all these instances, meaningful error messages guide the user, and the editor attempts to be as unobtrusive as possible. * [http://wiki.event-b.org/index.php/Text_Editor Text Editor Wiki Page]8 KB (1,257 words) - 15:56, 28 January 2010
- ..." action will then be scheduled as a further task to be performed, and the user will have to wait or cancel the command. Those commands are accessible by r :'''Proof details can now be displayed'''. It is now possible for the user to have a look at what a proof rule really did. A new view, the Rule Detail15 KB (2,008 words) - 15:34, 10 January 2011
- ...Y lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which coul ...rease directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.21 KB (3,334 words) - 21:20, 20 April 2012
- ...space, you will just commit 'content.jar' and 'artifacts.jar' to SVN. This page explains how to generate these two files. ...akes it easier to locate the file from the terminal command line since the user home directory is the default local directory in Terminal)10 KB (1,436 words) - 09:06, 27 May 2015
- Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details. * Theory help (2.0.0) User documentations.8 KB (1,015 words) - 13:50, 1 April 2022
- ## Click ''Next'', after some time, the ''Install Details'' page appears ...e inclusion of more invariants (from the included machines) depends on the user’s choice on ''Includes''. The defined invariants on the composed machine7 KB (1,161 words) - 11:02, 4 July 2013
- :'''Extensible pretty print'''. It is now possible to extend the pretty print page with the same kind of mechanism used to extend the structured editor. :See also: [[Extending the Pretty Print Page]]12 KB (1,642 words) - 13:21, 28 July 2010
- === User Requirements === === User Input ===19 KB (2,883 words) - 18:20, 17 March 2014
- ...put and output parameters. At the top there are two buttons that allow the user to increase/decrease '''Target Temperature'''. The target temperature perio ...rchive file, which includes the complete development, can be found on this page.7 KB (1,119 words) - 10:06, 12 May 2011
- The purpose of this page is to describe how to extend the Event-B project explorer. It covers on the ...on for use when displaying the metadata about the content extension to the user.20 KB (2,461 words) - 16:33, 24 May 2010
- ...ent systems sharing data, for details see the [[Tasking Event-B Overview]] page. ...e following, which should be installed if the features are required by the user for editing:17 KB (2,568 words) - 09:03, 19 October 2015
- This page describes the requirements for a '''generic parser''' for the [[Event-B Mat mathematical language syntax can be extended by the final user.27 KB (3,967 words) - 13:21, 15 February 2010
- ...ilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework fo ...was to make a simple to use environment that can be used by a non-Event-B user (e.g. requirements engineer, fault tolerance specialist), yet provides the19 KB (2,944 words) - 15:28, 27 January 2011
- A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps asso ...ided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ad15 KB (2,298 words) - 15:08, 27 January 2011
- : A crash may occur when closing the Welcome page. After restarting Rodin, everything works fine.<br/> User Release date : 2014-12-17.6 KB (909 words) - 13:48, 17 December 2014
- This page describes the core facilities for loading Rodin Event-B models in EMF and t ...xt string that contains the name identifier of the referenced element. The user may edit this identifier to a new name that may or may not exist. The edit26 KB (3,961 words) - 13:04, 19 May 2020
- ...erview of Tasking Event-B can be found on the [[Tasking_Event-B_Overview]] page. [[Category:User documentation]]12 KB (1,741 words) - 08:25, 14 December 2010
- This page is for listing available example Event-B/Rodin projects. By [[User:Steve|Steve]].9 KB (1,283 words) - 13:58, 5 July 2017
- ...e need to be productive using Event-B and minimize the access to an expert user. It is continuously maintained by the various actors involved in the envir ...video tutorials about the use of the platform.<ref>http://www.youtube.com/user/EventBTv</ref>20 KB (3,030 words) - 13:18, 18 July 2012
- First, this can give the user a deeper insight into how the model behaves and how the refinement levels a ...be discharged. But without an animator it is not always easy to see for an user if this is caused by the complexity of the proof or by an error.16 KB (2,553 words) - 15:12, 27 January 2011
- The mode views (simply '''''views''''' in the rest of the page) development process is a chain of documents much like Event-B models. One Each view generates a number of proof obligations to be discharged by a user. These POs formally ensure that the mode/FT view is actually a view on the21 KB (3,472 words) - 20:32, 26 June 2015
