Search results
From Event-B
Jump to navigationJump to searchCreate the page "Example page/Some sub-page" on this wiki! See also the search results found.
- This page describes work done for optimising well-definedness lemmas generated by the ...metimes generates lemmas that are unnecessarily complicated. We first give some motivating examples showing cases where this happens, then we describe what4 KB (617 words) - 09:43, 19 June 2012
- ...le event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The Flows plug-in ad ...tions can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kin4 KB (699 words) - 17:36, 3 December 2010
- ...sources is available at <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt>. :'''Example'''17 KB (2,670 words) - 15:07, 24 January 2012
- ...Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page). In particular: * A wiki page is dedicated to each release.7 KB (963 words) - 11:30, 27 January 2010
- ...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
- The Pretty Print Page of the [http://handbook.event-b.org/current/html/eventb_editor.html Event-B [[Image:PrettyPrintPage.png|480px|center|An example of pretty print page]]17 KB (2,385 words) - 09:53, 27 October 2011
- This page describes the design of a tactic requested here : [https://sourceforge.net/5 KB (824 words) - 16:05, 18 March 2014
- This page describes the design of a tactic for putting a sequent in Negation Normal F ...t is not clear how to decide which sub-predicate should get the negation. Some cases seem obvious. For instance, if one of the child is itself a negation3 KB (596 words) - 16:48, 13 April 2011
- ...s the part related to the machine ''v2'' (''e2''<nowiki>''</nowiki>). Also some other events are separated (''e1'' and ''v1'' only exist on machine ''S1'' ## Click ''Next'', after some time, the ''Install Details'' page appears7 KB (1,161 words) - 11:02, 4 July 2013
- The purpose of this page is to list and justify the transformation rules applied in the event model It is first necessary to introduce some equivalence and simplification rules on Event-B assignments and predicates.10 KB (1,604 words) - 09:19, 27 October 2011
- ...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 First define Records in the Record Declarations section. Some of these can subtype others but you need at least one that is not a subset,8 KB (1,347 words) - 13:07, 21 July 2010
- This page describes the design of a tactic replacing a predicate <math> P </math> in ...ssible conjunctions in the left-hand side of the implication, it checks if some appear in selected hypothesis. In that case, every predicate which is also10 KB (1,784 words) - 16:04, 18 March 2014
- This page sum up the developments recently done around or for the [[Rodin Platform]], The following tasks were planned at some stage of the [[Deploy]] project.6 KB (915 words) - 16:57, 27 February 2014
- ...tions can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kin ...roperty is mostly appropriate: ''termination with probability one''. As an example for this type of systems is to consider tossing a coin until it comes up ta19 KB (2,944 words) - 15:28, 27 January 2011
- ...odel which "''could'' have some sense"). This means that we have to verify some additional properties on the newly added elements. <br> 1. To extend the static checker in order to verify some conditions, one has to '''define a static checker module''' using the exten18 KB (2,534 words) - 13:53, 5 September 2013
- This page contains descriptions of the available proof tactics within the RODIN Platf * '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Pe57 KB (6,150 words) - 17:25, 21 February 2012
- * the [[Main Page]] of this very site. ...core), unpack these two files in the same place (the second will overwrite some files).15 KB (2,372 words) - 16:29, 19 May 2015
- ...and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities. In this section, you find a set of standard theories and some models using some of these theories.7 KB (958 words) - 14:53, 14 June 2021
- ...erview of Tasking Event-B can be found on the [[Tasking_Event-B_Overview]] page. The example/tutorial projects are,12 KB (1,741 words) - 08:25, 14 December 2010
- ...r itself also will be monitored through the '''Heater Sensor'''. If due to some faults the heater is not working properly, the controller will activate eit ...rchive file, which includes the complete development, can be found on this page.7 KB (1,119 words) - 10:06, 12 May 2011
- ...ekly teleconferences. The updates allowed to capture and integrate rapidly some minor changes to enhance the usability of the platform which were required Some other which were later added and prioritized are worth to mention:35 KB (5,228 words) - 10:12, 23 April 2012
- ...ieved by <tt>IInternalElement.getAttributeValue(PROB_ATTRIBUTE)</tt>). For example, it should return "probabilistic" if the attribute has value <tt>true</tt>, ...ur probabilistic attribute to events. Return to the MANIFEST.MF extensions page.<br>10 KB (1,503 words) - 13:34, 5 September 2013
- This page describes the requirements for a '''generic parser''' for the [[Event-B Mat :* on [http://en.wikipedia.org/wiki/Parser_combinator wikipedia]. Some implementations are referenced [http://pdos.csail.mit.edu/~baford/packrat/27 KB (3,967 words) - 13:21, 15 February 2010
- :'''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
- This page describes the introduction of variations in the HYP, HYP_OR, CNTR and GENMP The variations in the [[Inference Rules]] page have been generated such that the following facts hold:11 KB (1,594 words) - 07:08, 8 July 2014
- HEAD revision is always working, but some glitches can appear * [[Extending the Pretty Print Page]]8 KB (1,260 words) - 12:45, 30 July 2015
- ...even with the dedicated proof rules and with maximum memory allocated. In some of the bigger and more recent models, just substituting values for variable ...nd showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be comb16 KB (2,553 words) - 15:12, 27 January 2011
- This page describes the core facilities for loading Rodin Event-B models in EMF and t ...available. This can be configured to generate Event-B EMF and is used for some more recent Event-B generators. It will eventually replace the generator th26 KB (3,961 words) - 13:04, 19 May 2020
- The [[Modularisation Plug-in Tutorial]] page is currently in preparation. There is a dedicated page for [[Modularisation Integration Issues]].18 KB (2,784 words) - 10:57, 6 September 2010
- * Verification of preconditions (see for example <tt>AssociativeExpression.checkPreconditions</tt>) According to the [[Constrained_Dynamic_Parser| Parser]] page, the following informations are required by the parser in order to be able19 KB (2,883 words) - 18:20, 17 March 2014
- The purpose of this page is to describe how to extend the static checker. It covers on the one hand, ...ked elements that are similar to the unchecked elements. We will use as an example the ''decompositionFile'' that is defined as follows:24 KB (3,013 words) - 16:24, 5 July 2011
