Difference between pages "TextEditor EBNF" and "User:Nicolas/Collections/ADVANCE D3.4 Model Checking"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Fabian
m
 
imported>Ladenberger
 
Line 1: Line 1:
−
{| align="right"
+
== Overview ==
−
| __TOC__
+
{{TODO}}
−
|}
 
−
This page describes the text syntax for Event-B models in the TextEditor. It shows its EBNF, [[Explanation|explains]] some details and design decisions and gives some [[#Examples|examples]].
 
  
−
See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.
+
== Motivations / Decisions ==
 +
'''B to TLA+'''
  
−
Screenshots which give an impression of the syntax in the text editor are shown on the [[TextEditor_Screenshots| screenshot page]].
+
'''LTL Fairness'''
  
−
===EBNF for the TextEditor's syntax ===
+
'''Theory Support'''
  
−
parse_unit =
+
'''Physical Units'''
−
    'machine' identifier_literal comment*
 
−
    ('refines' identifier_literal (',' identifier_literal)*)?
 
−
    ('sees' identifier_literal (',' identifier_literal)*)?
 
−
    ('variables' identifier_list)?
 
−
    ('invariants' labeled_predicate_with_theorem+)?
 
−
    ('variant' variant)?
 
−
    ('events' event+)?
 
−
    end |
 
−
   
 
−
    'context' identifier_literal comment*
 
−
    ('extends' identifier_literal (',' identifier_literal)*)?
 
−
    ('sets' identifier_list)?
 
−
    ('constants' identifier_list)?
 
−
    ('axioms' labeled_predicate_with_theorem+)?
 
−
    end ;
 
−
 
−
variant = expression comment*;
 
−
 
−
event =
 
−
    convergence? 'event' identifier_literal comment*
 
−
    event_refinement?
 
−
    ('any' identifier_list)?
 
−
    ('where' labeled_predicate+)?
 
−
    ('with' labeled_predicate+)?
 
−
    ('then' labeled_action+)? ;
 
−
 
−
convergence = 'ordinary' | 'convergent' | 'anticipated' ;
 
−
 
−
event_refinement =
 
−
    'refines' identifier_literal (',' identifier_literal)* |
 
−
    'extends' identifier_literal ;
 
−
 
−
labeled_action = '@' identifier_literal action comment*;
 
−
 
−
labeled_predicate = '@' identifier_literal predicate comment*;
 
−
 
−
labeled_predicate_with_theorem =
 
−
    '@' identifier_literal predicate comment*|
 
−
    'theorem' '@' identifier_literal predicate comment*;
 
−
 
−
identifier = identifier_literal comment*;
 
−
 
−
identifier_list = identifier identifier* ;
 
−
 
−
comment =
 
−
    '//' string-to-next-linebreak |
 
−
    '/*' string '*/' ;
 
  
 +
The physical units analysis has been further stabilised, several reported bugs have been fixed.
 +
Support for physical units has been extended to theories along with the general theory-related improvements of ProB mentioned in the previous paragraph.
 +
The plug-in was ported to Rodin 3, all bugfixes and changes could be back ported to Rodin 2 successfully.
  
−
===Explanation ===
+
Further extension to the unit analysis include:
−
====Formulas ====
+
* Support for the analysis of units throughout refinement relations.
−
As you might notice the grammar only describes the structure of machines and contexts. For the terminals ''predicate'', ''expression'' and ''action'' you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts.
+
* Support for abstract units like "length" that can later be concretised to standard SI units.
  
−
====Comments ====
+
{{TODO}}
−
Also note that the rather strict position for comments is necessary. In the RodinDB most elements can be commented. That means if you comment an element this comment is attached to the element. To reflect this in a text syntax we need to exactly specify to which textual element a comment belongs. Therefore we decided to always associate a comment to the previous element.
 
−
Additionally database only allows one comment per element. The grammar allows multiple comments, but to reflect the database restriction to one internally multiple comments are concatenated to one with linebreaks between the separate comments.
 
  
 +
== Available Documentation ==
  
−
===Examples ===
+
'''ProB'''<br>
−
''Feel free to add own examples!''
+
The ProB Website<ref>http://www.stups.uni-duesseldorf.de/ProB</ref> is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.
  
 +
In addition we run a bug tracking system<ref>http://jira.cobra.cs.uni-duesseldorf.de/</ref> to document known bugs, workarounds and feature requests.
  
−
=====Machine 'm0' from example 'maximum' =====
+
{{TODO}}
  
−
See the [[TextEditor_Screenshots#Machine_.27m0.27_from_example_.27maximum.27|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].
+
== Conclusion ==
 +
{{TODO}}
  
−
machine m0 sees array
+
== References ==
−
+
<references/>
−
variables i
 
−
 
−
invariants
 
−
  @inv1 i ∈ ℕ
 
−
 
−
events
 
−
  event INITIALISATION
 
−
    then
 
−
      @act1 i :∈ ℕ
 
−
  end
 
−
 
−
  event find_max
 
−
    any j
 
−
    where
 
−
      @grd1 j ∈ 1‥n
 
−
      @grd2 ∀k·k∈1‥n ⇒ a(k) ≤ a(j)
 
−
    then
 
−
      @act1 i ≔ j
 
−
  end
 
−
end
 
−
 
 
−
=====Context 'array' from example 'maximum' =====
 
−
 
 
−
See the [[TextEditor_Screenshots#Context_.27array.27_from_example_.27maximum.27|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].
 
−
 
 
−
context array
 
−
 
−
constants n a
 
−
 
−
axioms
 
−
  @axm1 n ∈ ℕ1
 
−
  @axm2 a ∈ 1‥n → ℤ
 
−
end
 

Revision as of 13:03, 15 October 2014

Overview

TODO

Motivations / Decisions

B to TLA+

LTL Fairness

Theory Support

Physical Units

The physical units analysis has been further stabilised, several reported bugs have been fixed. Support for physical units has been extended to theories along with the general theory-related improvements of ProB mentioned in the previous paragraph. The plug-in was ported to Rodin 3, all bugfixes and changes could be back ported to Rodin 2 successfully.

Further extension to the unit analysis include:

  • Support for the analysis of units throughout refinement relations.
  • Support for abstract units like "length" that can later be concretised to standard SI units.

TODO

Available Documentation

ProB
The ProB Website[1] is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.

In addition we run a bug tracking system[2] to document known bugs, workarounds and feature requests.

TODO

Conclusion

TODO

References

  1. ↑ http://www.stups.uni-duesseldorf.de/ProB
  2. ↑ http://jira.cobra.cs.uni-duesseldorf.de/
Retrieved from ‘https://wiki.event-b.org/index.php?title=TextEditor_EBNF&oldid=10924’