imported>Mathieu |
imported>Jastram |
| Line 1: |
Line 1: |
| − | The purpose of the '''Relevance Filter Plugin''' is to try to automatically
| + | == Description == |
| − | select relevant hypotheses for a proof as opposed to the user doing this
| |
| − | manually.
| |
| | | | |
| − | === Instructions ===
| + | The Requirements Plugin... |
| | | | |
| − | The relevance filter can be invoked either by clicking the RF button in
| + | * Manages Text-Based Requirements |
| − | the proof control, or automatically as part of the auto tactic.
| |
| | | | |
| − | It also comes with a preference dialog (under Event-B > Sequent Prover > Meta Prover) that allows you to configure the
| + | * Requirements are managed and edited in an external Tool (currently Latex, Plain Text and OpenOffice) |
| − | filter(s). The plugin implements several filtering methods that will be
| |
| − | tried sequentially. The default setting is a selection of filters that
| |
| − | have been found to work well.
| |
| | | | |
| − | If you want to add the relevance filter to the auto tactic you should
| + | * Multiple Requirement Specifications can be managed in a Requirements Project. |
| − | add the Meta Prover item. It replaces NewPP after lasoo, NewPP
| |
| − | unrestricted, Atelier B P1 and Atelier B PP since this functionality is
| |
| − | already included in the Meta prover. You still have to add ML at the
| |
| − | appropriate place in the tactic as well as NewPP restricted and Atelier
| |
| − | B P0.
| |
| | | | |
| − | You can install the feature composition plug-in from the Rodin Update Site.
| + | == Status == |
| | | | |
| − | === Filters ===
| + | The Requirements-Plug-In is currently available through CVS only and not yet useable. |
| − | The relevance filter plugin includes the following filtering methods: | |
| − | * Meng & Paulson's relevance filter
| |
| − | This filter uses a set of relevant symbols which is initialized with the symbols contained in the goal. Hypotheses are then selected if they contain the symbols contained in this set of relevant symbols. When selected their symbols are also added to the set of relevance filters. The passmark parameter determines how many symbols a hypothesis may contain that are not in the relevant set, in order to be selected. When the pass mark parameter is 0.8 a hypothesis is still considered relevant if 20% of its symbols are not in the relevant set. I.e. higher numbers select less hypotheses. When running the algorithm the pass mark is increased incrementaly to avoid selecting too many hypotheses. The c paramter determines how fast this happens. The parameter must be greater or equal to 1, where 1 is the fastest increase.
| |
| − | * SInE
| |
| − | SInE is based on the idea that each symbol has a defining hypothesis. It selects all hypotheses that define a symbol contained in the goal and recursively all hypotheses that define a symbol contained in the previously selected hypotheses.
| |
| − | * DCR
| |
| − | This filter builds a weighted graph between all hypotheses and the goal. The edges are weighted based on the symbol overlap between the connected formulas. The threshold parameter defines the maximal distance a hypothesis may have from the goal in order to be considered relevant. If "use contextual relevance" is selected the overall frequency of a symbol is taken into account when computing the distance between two formulas.
| |
| − | * Sub-Expression filter
| |
| − | Selects hypotheses that have a common expression with the goal. The initial selection size parameter determines how many hypotheses similar to the goal are selected in the initialization step at most. The threshold parameter defines how similar the formulas selected in the initialization step must be to the goal. Higher means more similar. The value must be between 0 and 1.
| |
| − | * Lasso
| |
| − | Selects all hypotheses that have a symbol in common with the goal or any of the selected hypotheses
| |
| − | * Unrestricted
| |
| − | Selects all hypotheses.
| |
| | | | |
| − | More information can be found in [http://e-collection.ethbib.ethz.ch/view/eth:2278 "Relevance Filters for Event-B"]
| + | == User Documentation == |
| | | | |
| − | == Releases ==
| + | Currently, a new Requirements Project is created by manually creating a file, ending in .req, containing the following: |
| | | | |
| − | ===== Version 1.0.0 ===== | + | <?xml version="1.0" encoding="UTF-8" standalone="no"?> |
| | + | <root> |
| | + | </root> |
| | | | |
| − | ''27th Sep 2010''
| + | == Developer Documentation == |
| | | | |
| − | Version compatible with Rodin 2.0
| + | The Requirements Plug-in actually consists of two: |
| | | | |
| − | == References ==
| + | * DocGenerator |
| − | * Röder, Jann [http://e-collection.ethbib.ethz.ch/view/eth:2278 "Relevance Filters for Event-B"], ''ETH Zürich'', April 5, 2010 | + | * ReqsMgr |
| | | | |
| − | [[Category:User documentation]]
| + | === DocGenerator === |
| | | | |
| − | [[Category:Plugin]]
| + | === ReqsMgr === |
Description
The Requirements Plugin...
- Manages Text-Based Requirements
- Requirements are managed and edited in an external Tool (currently Latex, Plain Text and OpenOffice)
- Multiple Requirement Specifications can be managed in a Requirements Project.
Status
The Requirements-Plug-In is currently available through CVS only and not yet useable.
User Documentation
Currently, a new Requirements Project is created by manually creating a file, ending in .req, containing the following:
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<root>
</root>
Developer Documentation
The Requirements Plug-in actually consists of two:
DocGenerator
ReqsMgr
