Search results

Create the page "' + t + '" on this wiki! See also the search results found.

• Proof Obligation Names (Rodin User Manual)
  |Well-definedness of an event Guard||<math>t</math> / <math>d</math> / WD |<math>t</math> is the event name
  4 KB (575 words) - 15:09, 15 September 2011
• Datatype Rules
  list(T) ::= | cons( head : T, tail : list(T) )
  8 KB (1,199 words) - 13:37, 7 September 2010
• AnimB roadmap
  |Today the predicate evaluator doesn't use type information to infer a set that allow iteration of variable. |Today, the predicate evaluator doesn't allow the variable quantification with function sets (injection, bijection,
  1 KB (160 words) - 20:27, 10 March 2009
• Relation Rewrite Rules
  ...DOMRES_ID}}||<math> S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id </math>|| || A ...MSUB_ID}}||<math> S \domres (T \domsub \id) \;\;\defi\;\; (S \setminus T) \domres \id </math>|| || A
  33 KB (4,853 words) - 16:17, 8 March 2024
• Set Rewrite Rules
  ...||<math> S \binter \ldots \binter \emptyset \binter \ldots \binter T \;\;\defi\;\; \emptyset </math>|| || A ...Ty} \binter \ldots \binter T \;\;\defi\;\; S \binter \ldots \binter T </math>|| where <math>\mathit{Ty}</math> is a type expression || A
  29 KB (4,188 words) - 14:33, 13 April 2023
• EMF Compare Editor Investigation
  Colin's Notes ...s to get the EMF compare one (good!) but the EMF compare editor still didn't open.
  4 KB (623 words) - 19:48, 24 September 2009
• Arithmetic Rewrite Rules
  ...\bunion \ldots \bunion U) \\ \defi & \min (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} </math>|| || A ...\bunion \ldots \bunion U) \\ \defi & \max (S \bunion \ldots \bunion T \bunion \ldots \bunion U) \\ \end{array} </math>|| || A
  14 KB (2,054 words) - 16:50, 19 February 2024
• Rewriting rules for event model decomposition
  ...ed with the <math>\rightsquigarrow</math> symbol. <math>s</math> and <math>t</math> are assumed to be variables shared between <math>M_i</math> and <mat <br>Let's first establish a transformation rule for generic Event-B assignments. It
  10 KB (1,604 words) - 09:19, 27 October 2011
• Inference Rules
  ...{Q} \land \ldots \land \textbf{R} \limp \textbf{S} \;\;\vdash \;\; \textbf{T} }</math> || || A {{RRRow}}| ||{{Rulename|SUBSET_INTER}}|| <math>\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\;
  36 KB (5,611 words) - 10:22, 1 February 2024
• Exporting and importing archives containing theories
  ...the problem, let's say we have developed an Event-B project P and a theory T and want to make an archive in order to share them. The workspace looks lik - T.tuf
  3 KB (539 words) - 14:57, 14 June 2021
• Improved WD Lemma Generation
  <math>f\in S\pfun T\land x\in\dom(f)\land f\in S\pfun T\land y\in\dom(f)</math> ...sub-optimal as it contains twice the same sub-predicate (<math>f\in S\pfun T</math>). Consequently, when the prover is fed with the generated lemma, it
  4 KB (617 words) - 09:43, 19 June 2012
• EMF Compare Editor installation
  ...l the EMF Compare feature (it should have installed automatically but didn't for me - maybe I forgot to add a dependency) ...l the EMF Compare feature (it should have installed automatically but didn't for me - maybe I forgot to add a dependency)
  3 KB (469 words) - 14:17, 21 October 2009
• UML-B notes for 0.4.4
  ...licking on the transition name inside the statemachine figure. (This dosen't work for nested statemachines because they do not appear on the class diagr
  778 bytes (122 words) - 12:15, 4 March 2009
• Empty Set Rewrite Rules
  ...L_EMPTY}}||<math> S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>|| || A ...PE}}||<math> S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression
  10 KB (1,400 words) - 16:39, 12 May 2014
• New Proof Rules
  ==Automatically Apply De Morgan's Laws== The work is related to the following rewriting rules (De Morgan's Laws):
  4 KB (738 words) - 12:53, 12 August 2009
• UML-B release notes for 2.1.0
  * report to user if translation didn't proceed due to model validator
  1 KB (164 words) - 19:23, 19 November 2010
• UML-B notes for 2.0.1
  Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
  1 KB (162 words) - 19:48, 17 October 2010
• Structured Types
  Ev1 ~=\begin{array}[t]{l} Ev2 ~=\begin{array}[t]{l}
  18 KB (2,643 words) - 12:41, 12 August 2009
• AnimB start
  ...guardclosed.png|guardclosed.png]] the guard of the event is closed and can't be executed. * [[Image:unexecutable.png|unexecutable.png]] the guard can't be checked (constant value needed, well defined error, ...).
  4 KB (679 words) - 14:59, 16 September 2009
• Requirements Tutorial
  * That's it! Now you can now start using the Plug-In ...rements Specification]] that we are going to use to demonstrate the Plug-In's features.
  7 KB (995 words) - 15:44, 25 February 2009
• Camille Release History
  ** Cursor position moved after symbol replacement when the replacement didn't change the length of the formula. ** Semantic highlighting didn't update within events after reconcile
  6 KB (800 words) - 08:50, 19 August 2014
• Google Summer of Code 2009
  ...t Open Source software projects in the summer while getting paid for it. It's called '''Google Summer of Code&trade;''', and it provides free software p We would like to participate in 2009's Summer of Code.
  10 KB (1,629 words) - 12:50, 12 August 2009
• EMF framework for Event-B/Extensibility Issues
  * Design an EMF meta model (ecore) of your extension's abstract syntax. The model should include one or more root elements that E ==Ideas that didn't work==
  7 KB (1,094 words) - 10:50, 22 January 2010
• UML-B notes for 2.1.0
  Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
  1 KB (216 words) - 15:46, 28 January 2011
• Tracking Memory Leaks
  ...by sending a QUIT signal (number 3) to the JVM while it is running (I don't know how to do that on Windows platforms).
  2 KB (337 words) - 11:03, 10 November 2008
• Statemachine Animation Tutorial
  Prior to working with the ATM UML-B project let's create a new clean environment i.e. a new Rodin workspace First let's open the abstract UML-B class diagram <tt>ATM.ATM_A.classDiag</tt> which c
  13 KB (2,247 words) - 18:16, 13 January 2010
• UML-B FAQ
  ...d corresponding classes and set their variability to fixed (because we don't want to model creation of land and bridges). To force them to have the same
  2 KB (386 words) - 22:23, 11 December 2008
• ReqsManagement
  ...spect of system development. Even a proven B-Model is useless if it doesn't realize the desired requirements. The objective of the requirements plug-i
  2 KB (335 words) - 14:16, 3 December 2010
• Railway Interlocking Feedback
  the railway's people, we chose to allocate a great chunk of time to the B model that couldn't be discharged), in contrast to the
  6 KB (967 words) - 12:57, 28 October 2008
• Camille Editor
  ## If you didn't install the ''Event-B EMF Framework'' yet it will be automatically added. C ''This is how it should work. Unfortunately the update doesn't always notify the user properly. So we recommend checking for updates regul
  6 KB (945 words) - 12:22, 27 January 2015
• UML-B notes for 0.5.8
  Inverse function ~ doesn't work with dot notation. Use normal event-B notation instead.
  2 KB (353 words) - 12:45, 12 August 2009
• Membership in Goal
  <math>H,\quad x\in S,\quad S\subset T,\quad T\subseteq U \quad\vdash\quad x\in U</math> ...if the expression of the <math>x</math> or the intermediate sets <math>S, T, \dots</math> is too complicated, they may get lost into details and not di
  19 KB (3,362 words) - 13:50, 5 June 2014
• Rodin Platform 2.2.2 Release Notes
  == What's New in Rodin 2.2.2 ? == ...cker/?func=detail&aid=3374051&group_id=108850&atid=651669 Bug 3374051: Can't type < in quantifier box]
  4 KB (515 words) - 08:41, 1 August 2011
• Rodin Platform 2.4 Release Notes
  == What's New in Rodin 2.4? == Bug 2974867: Camille text editor - doesn't allow non alphanumeric chars
  11 KB (1,542 words) - 08:35, 1 March 2012
• Mathematical Language Evolution Design
  Let's look at the following formula: ..., this entails rewriting <math>\id_{T}(x)</math> into <math>x \domres \id_{T}</math>.
  14 KB (2,104 words) - 09:40, 11 May 2009
• Rodin Platform 2.5 Release Notes
  == What's New in Rodin 2.5? == Bug 3472979: B2Latex doesn't handle more than one paragraph in a Comment
  11 KB (1,478 words) - 17:32, 2 May 2012
• Rodin Platform 2.7 Release Notes
  == What's New in Rodin 2.7 == Bug 3565590: Can't open a proof
  10 KB (1,301 words) - 07:11, 29 August 2013
• Documentation Overhaul DoW
  ...a good understanding of the content we intend to cover. Otherwise we won't be able to allocate our resources wisely. The FAQ will grow naturally and won't need a detailed plan beforehand.
  9 KB (1,421 words) - 12:41, 8 December 2011
• Rodin Platform 2.3 Release Notes
  == What's New in Rodin 2.3? == Bug 3374051: Can't type < in quantifier box
  11 KB (1,401 words) - 09:39, 8 November 2011
• Rodin Editor User Guide
  Once you've installed Rodin 2.4 or upper, you are ready to use the Rodin Editor plug- Let's create a Rodin project, and add a context component called ''Celebrity_C0'
  8 KB (1,328 words) - 16:43, 3 June 2013
• Rodin Platform 2.1 Release Notes
  == What's New in Rodin 2.1? == ...cerning the maintenance and evolution of Rodin, is to increase the platform's performances. Investigation has started and some early enhancements are al
  10 KB (1,277 words) - 13:45, 26 July 2011
• DynamicContainer
  * Design an EMF meta model (ecore) of your extension's abstract syntax. The model should NOT deal with ownership of the extension // Mark meta-data to indicate it can't be changed
  6 KB (506 words) - 12:00, 25 November 2009
• Developer FAQ
  If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[T r2. The solution of 1 didn't work and I still have some errors in the plugin.xml file. (You will have to
  15 KB (2,372 words) - 16:29, 19 May 2015
• Rodin Platform 2.6 Release Notes
  == What's New in Rodin 2.6? == Bug 2974867: Camille text editor - doesn't allow non alphanumeric chars
  10 KB (1,328 words) - 16:14, 3 August 2012
• Modus Ponens generalized
  * Each hypothesis must be scanned only once to avoid accumulating predicate's running time. From that point of view, two decisions can be inferred : :<math>P \lor R \lor Q \lor S \lor T</math>
  10 KB (1,784 words) - 16:04, 18 March 2014
• Adding Reasoners(How to extend Rodin Tutorial)
  Let's call this rule DBL_INEQ. By reading this rule, we see it is goal agnostic. ...te any activator for our plugin, so no such constant prefix exists. So, let's create here something like :
  13 KB (2,012 words) - 15:43, 21 September 2021
• Switch from CVS to Subversion
  Note that the filtering on <tt>CVSROOT</tt> didn't seem to work as expected: this directory still occurred in the SVN trunk an
  4 KB (710 words) - 09:37, 1 April 2009
• The Use of Theories in Code Generation
  The array operator notation is defined in the expression array(s: P(T)); and the semantics is defined in the direct definition. arrayN constrains ...d side of the rule. The ''Type Rules'' section describes the implementation's description of the ''arrayN'' type.
  4 KB (599 words) - 15:00, 14 June 2021
• TextEditor EBNF
  ===EBNF for the TextEditor's syntax === The syntax doesn't allow whitespaces within labels. It assumes that all characters following a
  4 KB (559 words) - 12:43, 12 August 2009
• SMT Solvers Plug-in Developer Support
  If you don't have an Eclipse development platform for Java and Eclipse plug-ins installe To run a Rodin platform, from the sources in the developpment workspace, you'll need to create an Eclipse launch configuration:
  4 KB (691 words) - 14:34, 19 May 2014
• Isabelle for Rodin
  ...'''Rodin's software installation facilities''' and is available on '''Rodin's main update site''' (<nowiki>http://rodin-b-sharp.sourceforge.net/updates< ** Isabelle's generic parser is used to parse the theories generated by Rodin.
  9 KB (1,317 words) - 10:07, 29 April 2013
• Indexing System
  ...en indexing their project, using type ''IRodinFile'' for generic parameter T. ...to be understood as a node in the dependence graph. It has a label of type T and lists of predecessors and successors.
  10 KB (1,541 words) - 17:41, 9 March 2009
• B2Latex
  Since B2Latex 0.6.1, this file won't be overwritten if already exists, so no user modifications are accidentally
  4 KB (718 words) - 17:22, 8 July 2016
• Rodin Platform 1.3 Release Notes
  == What's New in Rodin 1.3? == Bug 2952959: Disabling auto-provers doesn't work
  12 KB (1,642 words) - 13:21, 28 July 2010
• Mathematical Extensions
  The following definitions hold at a given instant <math>t</math> and for the whole platform.<br /> ...}_t</math> denote the affectation of tags to an extension at instant <math>t</math> (<math>\mathit{tag}_t \in \mathit{EXTENSION}_t \pfun \intg</math>);<
  19 KB (2,883 words) - 18:20, 17 March 2014
• Scenarios for Team-based Development
  ...nt-B Project is maintained and accessible: In this scenario, the users don't care much about the team aspect, but require access to a change history.
  4 KB (670 words) - 14:38, 29 January 2009
• How to create Rodin projects programmatically
  // add the rodin nature if it isn't already there
  6 KB (784 words) - 15:19, 21 August 2023
• Generic Event-B EMF extensions
  The class should be extended by a client plug-in and the client's class should be registered as a Refinement Participant using the relevant For example, a basic type invariant that doesn't depend on other variables might be placed at position 1 whereas a theorem o
  13 KB (1,988 words) - 11:01, 30 May 2020
• Extending the Static Checker (How to extend Rodin Tutorial)
  # We encounter a problem which doesn't affect the PO generation: it leads to a '''warning''' (fixed by a default a ...ule configuration lifecycle. He has to be aware, at any time, of his module's hierarchy, and has to call sub-modules explicitly when meaningful. Further
  18 KB (2,534 words) - 13:53, 5 September 2013
• User Documentation Overhaul
  * The tutorial doesn't make clear what knowledge is expected when starting the tutorial.
  5 KB (720 words) - 11:28, 15 September 2011
• Single View Design
  ...g Sets''': Allows you to see the working sets as top level elements. If you're not familiar with working sets, consult [http://help.eclipse.org/help32/i ...is mean if you select both machines and projects at the same time, you won't get any statistics.
  5 KB (842 words) - 18:35, 26 March 2010
• Refinement of Statemachines
  ...e moment the refinement is valid because it is an exact copy, but it doesn't make any progress. We will make the refinement more interesting by modifyin c) Open the new state machine's diagram by right-clicking on it and selecting 'open diagram'.
  6 KB (895 words) - 06:12, 8 September 2011
• Scenarios for Merging Proofs
  ...r). We also consider ''L'' and ''O'' as being symmetrical (and thus we won't describe symmetrical scenarios).
  6 KB (1,046 words) - 10:34, 27 October 2011
• Event-B Statemachines
  ...w shows its available properties (if you cannot find it, please go to Rodin's menu ''Window > Show View > Properties''). This view allows you to modify ...guard. I.e. the transition may fire from either of the incoming transition's source states. Junctions can be cascaded if required in order to build a b
  13 KB (2,134 words) - 08:04, 6 October 2015
• Rodin Index Design
  However, the element handle doesn't carry directly the user-defined name for the element. This name is stored ...tructed expensively by running all indexers on all files). However, we don't want to save all index tables, but only essential information (the rest bei
  14 KB (2,204 words) - 12:58, 12 October 2009
• D32 Provers
  Concerning Rodin's provers the following contributions have been made: ...tics. The tactic then inputs the reduced sequent to one or several of Rodin's external provers (PP, newPP, ML). Jann Röder carried out experiments usin
  11 KB (1,699 words) - 15:25, 27 January 2011
• Constrained Dynamic Parser
  ...cking -- see [[#Some Difficulties|here before]]). As a side effect, it won't be possible to define new ''lambda like'', ''union like'' and ''sets like'' t = token # t is the processed symbol
  27 KB (3,967 words) - 13:21, 15 February 2010
• Rodin Platform 2.2 Release Notes
  == What's New in Rodin 2.2? == Bug 2974867: Camille text editor - doesn't allow non alphanumeric chars
  10 KB (1,354 words) - 13:31, 1 July 2011
• Rodin Platform 1.2 Release Notes
  == What's New in Rodin 1.2? == Bug 2893379: Can't edit Refinement if var and event have the same name
  11 KB (1,488 words) - 10:06, 28 July 2010
• Migration to Eclipse 3.6
  ::It's now possible to export the contents of your current target platform into a ::In the list of export wizards (File -> Export...), you'll find the wizard available under Plug-in Development -> Target definition.
  12 KB (1,814 words) - 08:44, 30 June 2010
• ADVANCE Deliverable D3.3
  To ease the reviewer's reading of the present deliverable, the structure of the document will fol * User's guides.
  6 KB (830 words) - 13:21, 7 October 2013
• Rodin Platform 2.0 Release Notes
  == What's New in Rodin 2.0? == :'''Better platform's behaviour'''. Some cumbersome behaviours were improved:
  15 KB (2,008 words) - 15:34, 10 January 2011
• D32 Mathematical Extensions
  * polymorphism (<math>l \in List(S \cprod T)</math>) ...g/index.php/Constrained_Dynamic_Parser#Design_Alternatives ''Generic Parser's Design Alternatives'' ]
  7 KB (1,095 words) - 14:40, 21 December 2010
• Details for Maintaining Main Rodin Update Site
  ...e existing categories and create a new one only if your plug-in really don't fit in existing ones.
  39 KB (4,626 words) - 08:33, 6 April 2012
• ADVANCE D3.3 Improvement of automated proof
  ...tness. We will also prepare a set of automatic tests to ensure that we don't regress.
  7 KB (1,145 words) - 10:05, 8 October 2013
• D32 UML-B
  :#* Report to user if translation didn't proceed due to model validator - previously, it was not clear when the mode
  9 KB (1,382 words) - 11:05, 27 January 2011
• UML-B Tutorial
  c. Create an initial state (it doesn't need a name).
  11 KB (1,713 words) - 20:07, 18 April 2010
• Event Model Decomposition
  ...r. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already i ...es is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where <math>e</math> is a
  43 KB (6,950 words) - 09:48, 27 October 2011
• Mode/FT Views
  ...g. For example, the doors now can be opened for the passengers (which wasn't allowed while moving) and maintenance carried by the staff. Likewise, when ...t modal elements’ references to their abstract counterparts. There shouldn’t be any confusion: a mode only refines another mode, and Event-B model can o
  21 KB (3,472 words) - 20:32, 26 June 2015
• Code Generation Tutorial
  ...ne is refined, but choose a different machine to refine (any one, it doesn't matter).
  12 KB (1,741 words) - 08:25, 14 December 2010
• EMF framework for Event-B
  ...collection of ''Annotations''. ''Annotations'' (which are similar to Ecore's ''EAnnotations'' ) give a flexible and efficient way to store information ...class should be configured to use the 'ExtensionSynchroniser' from the core's persistence plug-in. (No Rodin element identifier should be given). The ch
  26 KB (3,961 words) - 13:04, 19 May 2020
• Rodin Platform 3.0 Release Notes
  == What's New in Rodin 3.0? == 704 Can't display information about VAR and NAT PO
  8 KB (1,195 words) - 16:35, 9 July 2014
• D45 Prover Enhancement
  ...impler" for Rodin's theorem provers, or (3) implement an extension of Rodin's theorem provers in Java. None of these options is fully satisfactory for m ..., and it requires considerable experience and a deep understanding of Rodin's theorem provers.
  21 KB (3,334 words) - 21:20, 20 April 2012
• Rodin Platform 3.2 Release Notes
  == What's New in Rodin 3.2? == Technically speaking, it's because of hidden package dependencies in Eclipse 4 that are not automatic
  9 KB (1,317 words) - 11:09, 6 July 2017
• Refactoring Framework
  ...all its occurrences. Moreover, they require that renaming an element doesn't modify their existing proof state (no loss of proof). ...//stups.hhu.de/mediawiki/images/9/94/Holl2007_Bachelorarbeit.pdf Sonja Holl's Bachelor thesis]
  11 KB (1,773 words) - 07:41, 12 January 2016
• Rodin Proof Tactics
  ...: Simplifies predicates containing type expressions such as E ∈ T to ⊤ and T = ∅ to ⊥.
  57 KB (6,150 words) - 17:25, 21 February 2012
• Variations in HYP, CNTR and GenMP
  ...urns a list of predicates stronger (e.g which infer) than the input. But it's also performed by the function StongerNegative. So this function applies t ...substitute previously computed and we ensure that the given predicate won't be rewrite by himself. We store the substitute and the position in the pred
  11 KB (1,594 words) - 07:08, 8 July 2014
• Rodin 3.0 Plug-in Migration Guide
  Let's consider that you dispose of a new type environment of type {{class|ITypeE There isn't any change from Event-B UI Plug-in which impacts its downstream plug-ins.
  17 KB (2,614 words) - 16:25, 14 February 2014