Difference between pages "Constrained Dynamic Parser" and "D32 Model Animation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Daniel
 
Line 1: Line 1:
−
{{TOCright}}
+
= Model Animation =
−
This page describes the requirements for a '''generic parser''' for the [[Event-B Mathematical Language]].
 
  
−
A first design proposal is also drafted.
+
== Overview ==
 +
=== Siemens Application===
 +
The most important additions of the last 12 months are:
 +
* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper
 +
<ref name="fm2009">Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009</ref>
 +
only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
 +
* In this article we describe the previous method adopted by Siemens in much more detail,  as well as explaining the performance issues with Atelier B.
 +
* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
 +
* We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
  
−
== Requirements ==
+
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
−
In order to be usable [[mathematical extensions]] require that the event-b mathematical language syntax can be extended by the final user.  
+
 +
Also, since  <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
  
−
The lexical analyser and the syntaxic parser thus have to be extensible in a simple enough way (from a user point of vue).
+
More details:
 +
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
−
=== Requirements Exported by the Current Language Design ===
+
=== Multi-level Animation ===
−
==== Operator Priority ====
 
−
* operator are defined by group,
 
−
* group of operator have a defined precedences,
 
−
* there may be precedences defined inside groups.
 
  
−
==== Operator Compatibility ====
+
Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored.
−
* a compatibility table defines allowed associativities inside a group,
+
In
−
* a compatibility table defines allowed associativities between groups (it allows to forbid a syntaxic construction like <math>f(x)^{-1}\;</math>
+
<ref name="abz2010">Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Refinement-Animation for Event-B - Towards a Method of Validation, ASM'2010, LNCS 5977, Springer-Verlag, 2010</ref>
−
: nota: this requirement was added afterwards with consistency in mind.
+
and
 +
<ref name="ml-journal">Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Validation of Formal Models by Refinement Animation, to appear in Science of Computer Programming, Elsevier</ref>
 +
we extended ProB in a way that all refinement levels of a model can be animated simultaneously.
  
−
=== Expected Extension Schemes ===
+
First, this can give the user a deeper insight into how the model behaves and how the refinement levels are related to each other.
−
We do want to at least define operators of the following form :
 
−
* infix : <math>a + b\;</math> or <math>a \vdash b : c\;</math>
 
−
* prefix : <math>\neg a\;</math>
 
−
* postfix : <math> R^*\;</math>
 
−
* closed : <math>\|a\|\;</math>
 
−
* parentheses sugar : <math>(a +b) * c\;</math>
 
−
* functional postfix : <math> a \langle b \rangle\;</math>
 
−
* functional prefix : <math>  \langle b \rangle f\;</math>
 
−
* lambda like : <math> \lambda x\mapsto y . P | E\;</math>
 
−
* Union like : <math> \Union\{ e \mid P\}</math> or <math> \Union\{ x,y . P \mid e\}</math>
 
−
* sets : <math>\{a, b, c + e\}\;</math> or <math>\{ e \mid P\}\;</math> or <math>\{x,y . P \mid e\}\;</math>
 
  
−
We also like to define precisely precedences and associativity between existing and new operators.
+
Second, we can now find errors in context of refinement. This include violation of the gluing invariant or not satisfiable witnesses for abstract variables. If such errors are present in a model, the corresponding proof obligation cannot 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.
  
−
=== Requirements exported by the dynamic feature ===
+
In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.
−
* the precedence should not be enumerated but defined by a relation, like: '+' < '*' and '*' < '**', ...
 
  
−
== Limitations ==
+
=== Evaluation of the ProB Constraint Solver ===
 +
Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be  conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC  for TLA+, AnimB for Event-B,  and Alloy.
 +
 
 +
The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes (TLC was only able to solve the n-queens problem up until n=9, or n=14 when reformulating the problem as a model checking problem rather than a constraint-solving problem). In another small experiment, we checked whether two graphs with 9 nodes of out-degree exactly one are isomorphic by checking for the existence of a permutation which preserved the graph structure. TLC finds a permutation after 2 hours 6 minutes and 28 seconds; ProB 1.3.3 takes 0.01 seconds to find the same solution, while Alloy takes 0.11 seconds with SAT4J and 0.05 seconds with minisat.
 +
For some other examples (in particular time-tabling) involving operators such as the relational image, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint  programming language.
  
−
== Design Alternatives ==
+
=== Constraint-Based Deadlock Checking ===
 +
Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
 +
chosen.
  
−
=== Make Existing Parser Extensible ===
+
The basic idea is to generate deadlocks by solving a constraint consisting of the axioms Ax, the invariants Inv together with a constraint D specifying a deadlock. More formally, D is the negation of the disjunction of all the guards.  
−
The existing parser is a LL recursive descent parser generated by the [http://www.ssw.uni-linz.ac.at/Coco/ Coco/R Compiler Generator], which makes extensive use of pre-computed lookahead, which makes it very difficult to be transformed in a sufficiently enough generic parser.
 
  
−
=== Parser Combinator ===
+
The following tool developments were required to meet the challenges raised by the industrial application:
−
:* on [http://en.wikipedia.org/wiki/Parser_combinator wikipedia]. Some implementations are referenced [http://pdos.csail.mit.edu/~baford/packrat/ here].
+
* generation of the deadlock freedom proof obligation by ProB (to avoid dependence on other plug-ins and being able to control whether theorems are to be used or not; currently they are not used)
−
:* with functionnal language [http://wiki.portal.chalmers.se/agda/Agda Agda] : ''[http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf Parsing Mixfix Operators]
+
* implementation of a constraint-based deadlock checking algorithm:
−
:: This paper is interesting in its proposal of using an acyclic graph to define operator precedence.
+
** with the possibility to specify an additional goal predicate  to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10
−
:* with functional language [http://user.cs.tu-berlin.de/~opal/opal-language.html OPAL] : ''[http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=8A8A8B39FFBF1AEF17C782C4822C5AF6?doi=10.1.1.58.655&rep=rep1&type=url&i=0 How To Obtain Powerful Parsers That Are Elegant and Practical]''
+
** with semantic relevance filtering (to be able to filter out guards which are always false given the goal predicate).
 +
** with partitioning of the constraint predicate into components and optionally reordering according to usage (basic predicates which occur in most guards are listed first)
 +
* Improvements to ProB's constraint solving engine: (reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel).
  
−
=== Pratt Parser ===
+
ProB has been applied successfully to two models of the adaptive cruise control by Bosch. The more complicated model is CrCtrl_Comb2Final. To give an idea, here are some statistics of the deadlock freedom proof obligation for CrCtrl_Comb2Final:
−
:* [http://portal.acm.org/citation.cfm?id=512931 original paper from Vaughan Pratt]
+
* when printed in 9-point Courier ASCII the formula takes 32 A4 pages (the disjunction of the guards starts at page 6)
−
:* [http://effbot.org/zone/tdop-index.htm SImple ''Pratt'' parsing in python]
+
* the model contains 59 events with 837 guards (19 of them disjunctions, some of which themselves nested)
−
:* [http://javascript.crockford.com/tdop/tdop.html ''Pratt'' parsing in javascript]
+
* Bosch are interested in deadlocks that are possible according to a flow specified using the flow plugin; these can be found with ProB by specifying a goal predicate (such as "Counter=10")
−
Note that a ''pratt'' parser is essentially a parser for expressions (where expression parts are themselves expressions)... But it may be tweaked to limit the accepted sub-expressions or to enforce some non-expression parts inside an expression. More on that hereafter.
+
* the proof obligation (as generated by the flow plugin) initially could not be loaded in Rodin due to "Java Heap Space Error".
 +
* Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 seconds).
  
−
=== Some Existing Extensible Languages ===
+
=== BMotionStudio for Industrial Models ===
−
* [http://www.chrisseaton.com/katahdin/ Katahdin], and the associated paper [http://www.chrisseaton.com/katahdin/katahdin-thesis.pdf A Programming Language Where the Syntax and Semantics Are Mutable at Runtime] which describes the language and its implementation (in C#).
 
−
* [http://itcentre.tvu.ac.uk/~clark/xmf.html XMF] whose implementation seems not be describes in details.
 
−
* [http://xlr.sourceforge.net/index.html XLR: Extensible Language and Runtime], which looks like a ''pratt'' parser according to the [http://xlr.svn.sourceforge.net/viewvc/xlr/trunk/xl2/xlr/parser.cpp?revision=805&view=markup sources].
 
−
* [http://www.pi-programming.org/What.html <math>\pi</math>] whose implementation seems not be describes in details (but sources availables).
 
  
−
== Design Proposal ==
+
Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.
−
=== Main Concepts ===
 
−
;symbol: a symbol is a lexem known by the parser.
 
−
;group: each symbol belongs to one and only one group.
 
−
;symbol compatibility: a relation telling if inside a group two symbol are compatibles.
 
−
:Two symbol are compatibles is they can be parsed without parentheses (see [[Event-B Mathematical Language]] for more on compatibility).
 
−
;group compatibility: a relation telling if two groups are compatibles.
 
−
:Two symbol of different groups are said compatibles if their group are compatibles.
 
−
;symbol associativity: a relation which gives the associative precedence of symbols inside a given group.
 
−
;group associativity: a relation which gives the associative precedence of groups.
 
−
:Two symbol of different groups have a relative precedence given by the associative precedence of their groups.
 
−
;generic parser: the parser which is defined.
 
−
: This parser may be called recursively (an infix expression being build upon a left and right sub-expression) and is often the default parser used when building the AST associated with a ''symbol''.
 
−
;specific parser: some specific parser, predefined as helper functions to build specific AST.
 
−
:Some example of specific parser are the one used to parse and build list of identifiers (for quantified predicates), mapplets lists (for lambda), and so one...
 
  
−
=== Proposed User Interface ===
+
In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:
−
''The hereafter proposition does not preclude the final UI to take other (more user friendly forms). But the concepts should probably stay the same''
 
  
−
We propose that the user will be able to create several predefined type of symbols (new types may certainly be further added by mean of eclipse extension points). When defining a symbol, the user can choose the parser used to parse the sub-expressions (default to generic parser, but a specific parser may be used) and can enforce the form of the resulting parsed sub-expression in terms of their AST root type.
+
* We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
 +
* Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
 +
* We introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.
  
−
==== Predefined Symbol Builders ====
+
=== Various other improvements ===
−
The proposed predefined symbol builders are:
 
−
;infix: For example predicate conjunction which expects two predicates for left and right parts may be defined by <code>infix("∧", gid="(logic pred)", expected_nonterm=["predicate", "predicate"])</code>
 
−
:As another example, substitution ≔ of group '(infix subst)' which expect two ''ident list'' for left and right expressions may be defined by <code>infix(symbol="≔", gid="(infix subst)", parsers=["ident_list", "ident_list"], expected_nonterm=["ident_list", "ident_list"])</code>
 
  
−
;prefix: <code>prefix("¬", "(not pred)", expected_nonterm=["predicate"])</code>
+
mainly inspired by Siemens and Bosch Applications
  
−
;atomic: <code>atomic("⊤", "(atomic pred)")</code>
+
* Improved AVL algorithms, more operators
  
−
;prefix closed: used to build prefix symbol which must be followed by enclosing symbol(brackets, parentheses,..). For example <tt>finite</tt> may be defined by: <code>prefix_closed("finite", "(", ")","(atomic pred)", expected_nonterm=["expression"])</code>
+
* record support: automatic detection of records described by a bijection between a cartesian product and a carrier set (these axioms can either be entered manually, such as in the Bosch models, or generated by the Records plug-in).  
  
−
:postfix: <code>postfix("∼", gid="(unary relation)",  expected_nonterm=["expression"])</code>
+
* treatment of infinite sets, in particular complement sets such as INTEGER \ {x}. Such sets are being used in some of the Siemens models.
  
−
;quantified: <code>quantified("∀", "·", expected_nonterm=["predicate"]</code>
+
* Partitioning of predicates into connected sub-components (was useful for Siemens application, to be able to pinpoint location of an inconsistency in the axioms; it turned out useful for constraint-based deadlock checking as well)
  
−
;lambda like: <code>lambda_like("λ", "·", u"∣", gid="(quantification)", expected_nonterm=["ident list", "predicate", "expression"])</code>
+
* Improved constraint solving, better use of Prolog's CLP(FD) constraint solver
  
−
;quantified union like: <code>Union_like("⋃", "·", "∣", gid="(quantification)")</code>
+
* reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel
  
−
;closed sugar: use for parentheses added to enforce associativity: <code>closed_sugar("(", ")")</code>
+
== Motivations ==
  
−
;functional postfix: <code>functional_postfix("(", ")", gid="(functional)", expected_nonterm=["expression", "expression"])</code>
+
The above works were motivated mainly to support the following three industrial deployments:
 +
* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
 +
* Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
 +
* SAP: provide a way to generate test cases using constraint-based animation
  
−
Some right associative versions of those symbol builders may also be supplied (infix_right, or a specific parameter ''right associative'' parameter may also be provided to the ''infix'' symbol builder).
+
== Available Documentation ==
  
−
==== Predefined Specific Parser ====
+
=== References ===
−
* expression lists
+
<references/>
−
* ident lists
 
−
* maplet tree (for lambda)
 
  
 +
== Planning ==
  
−
==== Defining Compatibility and Precedences ====
+
* Finish Validation Report
−
Inside a group, ''compatibility'' may be defined like:
+
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
−
<code>
+
* Support mathematical extensions in ProB
−
    g = group["(binop)"]
+
* Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.
−
    g.add_many_compatibility(
 
−
            [  ("∪", "∪"),
 
−
                ("∩", "∩"),
 
−
                ("∩", "∖"),
 
−
                ("∩", "▷"),
 
−
                ("∩", "⩥"),
 
−
                ("∘", "∘"),
 
−
                (";", ";"),
 
−
                (";", "▷"),
 
−
                (";", "⩥"),
 
−
                ("", ""),
 
−
                ("◁", "∩"),
 
−
                ("◁", "∖"),
 
−
                ("◁", ";"),
 
−
                ("◁", "⊗"),
 
−
                ("◁", "▷"),
 
−
                ("◁", "⩥"),
 
−
                ("⩥", "∩"),
 
−
                ("⩥", "∖"),
 
−
                ("⩥", ";"),
 
−
                ("⩥", "⊗"),
 
−
                ("⩥", "▷"),
 
−
                ("⩥", "⩥"),
 
−
                ("×", "×"), ]
 
−
</code>
 
−
which defines the compatibility table for expression binary operator as defined in [[Event-B Mathematical Language]].
 
−
 
 
−
 
 
−
Inside a group, ''precedence'' may be defined like:
 
−
<code>
 
−
g = group["(arithmetic)"]
 
−
g.add_many_precedence(
 
−
            [  ("^", "÷"),
 
−
                ("^", "∗"),
 
−
                ("^", "+"),
 
−
                ("^", "−"),
 
−
                ("^", "mod"),
 
−
                ("+", "∗"),
 
−
                ("−", "∗"),
 
−
                ("+", "÷"),
 
−
                ("−", "÷"),
 
−
                ("+", "mod"),
 
−
                ("−", "mod"), ] )
 
−
</code>
 
−
which defines ^ as having the least precedence amongst the operators of the expression arithmetic group.
 
−
 
 
−
Similarly, precedences and compatibilities between groups may be defined :
 
−
<code>
 
−
    group_precedence.add(("(binop)", "(interval)"))
 
−
    group_precedence.add(("(interval)", "(arithmetic)"))
 
−
    group_precedence.add(("(arithmetic)", "(unary relation)"))
 
−
    group_precedence.add(("(unary relation)", "(bound unary)"))
 
−
    group_precedence.add(( "(bound unary)", "(bool)"))
 
−
 
 
−
    group_compatibility.add_all( [ "(binop)", "(interval)", (arithmetic)", "(unary relation)", "(unary relation)", "(bound unary)",....])
 
−
</code>
 
−
 
 
−
==== Some Difficulties ====
 
−
Some difficulties appear when trying to implement an Event-B parser with the preceding scheme:
 
−
* A symbol may be declared by several different builders (think of unary and infix minus for example).
 
−
: ''Pratt'' parsers are able to cope with a symbol appearing either at the beginning of an expression or inside an expression (see ''led'' and ''nud'' hereafter). For example, unary minus and infix minus can be both defined by the proposed scheme. However, in their default form, ''pratt'' parser failed in parsing symbol like '{' which appears at the beginning of extension sets, comprehension sets and quantified sets.
 
−
: SOLUTION #1: The existing Event-B parser uses an infinite lookahead to determine which one of those three sets is actually being parsed.
 
−
: This solution hinders the extensibility of the parser, because the addition of a symbol requires to modify the lookahead.
 
−
: However, such an issue may be bypassed, at least in a first version, in enforcing some usage rules. Thus, a new symbol contributed by an extension but used in the lookahead may be rejected as in invalid symbol.
 
−
: SOLUTION #2: Implementing a backtracking parser.
 
−
: More precisely, it means that the three sets are attempted to be parsed. The parsing is successful if and only if one of these attempts lead to a result (''i.e''., it is a failure if several attempts or none lead to a result).
 
−
: It is a good solution provided that we use memorisation to alleviate the cost of parsing formulas that require heavy backtracking.
 
−
 
 
−
* Defining a grammar or a grammar extension is not an easy job, even with those simple mechanisms.
 
−
: It would certainly be a good idea to implement a user interface to test the grammar, so that an extension designer has a way to ensure that he agrees with the parser on the semantic of his extension (or at least on the AST obtained by using it). For example, the representation of the syntax tree returned by <tt>Formula.getSyntaxTree</tt> could be compared to an expected entered string.
 
−
 
 
−
=== Core Algorithm ===
 
−
==== Main Objects ====
 
−
;{{class|KnownSymbols}}: a table associating a {{class|SymbolParser}} for each known symbol.
 
−
 
 
−
;{{class|SymbolParser}}: a Parser for a specific symbol. It should at least have the following attributes:
 
−
:* {{class|Array<Parser>}} {{ident|led}} for parsing the expression associated to the symbol {{ident|id}} when it appears in the middle of an expression (''left denotation'')
 
−
:* {{class|Array<Parser>}} {{ident|nud}} for parsing the expression associated to the symbol {{ident|id}} when it appears at the beginning of an expression (''null denotation'')
 
−
:* {{class|String}} {{ident|id}}
 
−
:* {{class|String}} {{ident|gid}} designing the group to which the {{ident|id}} symbol belongs to.
 
−
:Note that parsers in ''led'' (respectively ''nud'') will be tried one after another until one match (with backtracking to the original state in between).
 
−
 
 
−
;{{class|Parser}}: A parser, which should have the following attributes
 
−
:*{{class|Parser Array}} {{ident|subparsers}} an array of subparsers used by the {{ident|parse}} method. They defaults to {{ident|MainParser}}, but may be set to specific parsers.
 
−
:and the following methods:
 
−
:*{{ident|parse}}: this method should consume tokens and returns an AST. It may use several {{ident|subparsers}}.
 
−
 
 
−
;{{class|ParserBuilder}}: the class that inherited from this class provide the interface used to create new symbols. It has the following method:
 
−
:*{{ident|build}}: which build a SymbolParser and store it in the {{class|KnownSymbols}} container as being associated to the symbol for which the parser is being built.
 
−
 
 
−
 
 
−
;{{class|MainParser}}
 
−
:This class inherits from {{class|Parser }} and its {{ident|parse}} function implements the core of the ''pratt'' algorithm.
 
−
 
 
−
:Without taking into account backtracking, the algorithm reads:
 
−
<blockquote><code><pre>
 
−
def parse(reckognized_token, has_right_associativity=False):
 
−
    global token
 
−
    t = token                    # t is the processed symbol
 
−
    token = tokenizer.next()        # token is the next symbol
 
−
    left = t.nud()              # a new expression is being parsed (null denotation : nothing on the left)
 
−
    while has_less_priority(reckognized_token, token, has_right_associativity):
 
−
        t = token
 
−
        token = next_token()    # if precedence allows it, we parse next expression
 
−
        left = t.led(left)      # has being left expression of current symbol (left denotation)
 
−
    return left
 
−
</pre></code></blockquote>
 
−
 
 
−
:The parsing of a new expression is initiated by:
 
−
<blockquote><code><pre>
 
−
    token = tokenizer.next()
 
−
    ast = MainParser.parse(KnownSymbols["(eof)"])
 
−
</pre></code></blockquote>
 
−
 
 
−
:where the {{ident|tokenizer}} returns the {{class|SymbolParser}} associated to the next lexem.
 
−
 
 
−
;{{class|identListParser}}: inherits from {{class|Parser}}. Its {{ident|parse}} function implements the parsing of an ident list (like <math>a,b,c\;</math>).
 
−
;{{class|identMapletListParser}}:  inherits from {{class|Parser }}. Its {{ident|parse}} function implements the parsing of a maplet list as used in lambda expression (like <math>a \mapsto (b \mapsto c)\;</math>).
 
−
;{{class|expressionListParser}}:  inherits from {{class|Parser }}. Its {{ident|parse}} function implements a list of expression as used in the extension set expression.
 
−
 
 
−
{{TODO|section being worked on}}
 
−
;{{class|infixParser}}: inherits from {{class|Parser}}. Its {{ident|parse}} function is a ''led'' parser and implements something like (pseudocode):
 
−
<blockquote><code><pre>
 
−
parse(AST left)
 
−
  ast = new AST()
 
−
  ast.first = left
 
−
  verify_expected_group(ast.first, this.expected_non_terminals[0])
 
−
  ast.second = this.parsers[0].parse(ast, is_right_associative=False)
 
−
  verify_expected_group(ast.second, this.expected_non_terminals[1])
 
−
  return ast
 
−
</pre></code></blockquote>
 
−
 
 
−
 
 
−
;{{class|infixBuilder}}: inherits from {{class|ParserBuilder}} and has the following methods:
 
−
:*<code>build(Lexem lexem, GroupID gid, Array<Parser> parsers, Array<NonTermGroups> expected_non_terminals)</code> which implements something like:
 
−
<blockquote><code><pre>
 
−
if lexem in KnownSymbols:
 
−
else:
 
−
</pre></code></blockquote>
 
−
{{TODO}}
 
−
 
 
−
=== Open Questions ===
 
−
How does the user specify the expected AST ?
 
−
: Some examples in the existing parser:
 
−
:* some binary infix predicates are in fact parsed as n-ary operators (with more than 2 childrens if possible). Shall we generalize this feature ? How will this fit within the proposed extension scheme ?
 
−
:* bound identifiers are converted to ''de Bruijn'' indexes while constructing the AST. Is this desirable ? How does the user specify that identifier are bound or not ?
 
−
 
 
−
=== Sample Implementation ===
 
−
A prototype as been developed in Python to quickly try different solutions.
 
−
 
 
−
The development tree of the python prototype is available at http://bitbucket.org/matclab/eventb_pratt_parser/
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
[[Category:Design Proposal]]
 

Revision as of 08:01, 30 November 2010

Model Animation

Overview

Siemens Application

The most important additions of the last 12 months are:

  • Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper

[1] only contained the initial San Juan case study, which was used to evaluate the potential of our approach.

  • In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
  • Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
  • We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.

Also, since [1], ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

More details:

Multi-level Animation

Prior versions of ProB only supported the animation of a single refinement level. Abstract variables and predicates referring to them were ignored. In [4] and [5] we extended ProB in a way that all refinement levels of a model can be animated simultaneously.

First, this can give the user a deeper insight into how the model behaves and how the refinement levels are related to each other.

Second, we can now find errors in context of refinement. This include violation of the gluing invariant or not satisfiable witnesses for abstract variables. If such errors are present in a model, the corresponding proof obligation cannot 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.

In the articles we summarized Event-B's current refinement methodology and showed for each proof obligation how the algorithm would find a counter-example. We presented empirical results and discussed how the algorithm can be combined with symmetry reduction.

Evaluation of the ProB Constraint Solver

Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC for TLA+, AnimB for Event-B, and Alloy.

The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes (TLC was only able to solve the n-queens problem up until n=9, or n=14 when reformulating the problem as a model checking problem rather than a constraint-solving problem). In another small experiment, we checked whether two graphs with 9 nodes of out-degree exactly one are isomorphic by checking for the existence of a permutation which preserved the graph structure. TLC finds a permutation after 2 hours 6 minutes and 28 seconds; ProB 1.3.3 takes 0.01 seconds to find the same solution, while Alloy takes 0.11 seconds with SAT4J and 0.05 seconds with minisat. For some other examples (in particular time-tabling) involving operators such as the relational image, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint programming language.

Constraint-Based Deadlock Checking

Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants chosen.

The basic idea is to generate deadlocks by solving a constraint consisting of the axioms Ax, the invariants Inv together with a constraint D specifying a deadlock. More formally, D is the negation of the disjunction of all the guards.

The following tool developments were required to meet the challenges raised by the industrial application:

  • generation of the deadlock freedom proof obligation by ProB (to avoid dependence on other plug-ins and being able to control whether theorems are to be used or not; currently they are not used)
  • implementation of a constraint-based deadlock checking algorithm:
    • with the possibility to specify an additional goal predicate to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10
    • with semantic relevance filtering (to be able to filter out guards which are always false given the goal predicate).
    • with partitioning of the constraint predicate into components and optionally reordering according to usage (basic predicates which occur in most guards are listed first)
  • Improvements to ProB's constraint solving engine: (reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel).

ProB has been applied successfully to two models of the adaptive cruise control by Bosch. The more complicated model is CrCtrl_Comb2Final. To give an idea, here are some statistics of the deadlock freedom proof obligation for CrCtrl_Comb2Final:

  • when printed in 9-point Courier ASCII the formula takes 32 A4 pages (the disjunction of the guards starts at page 6)
  • the model contains 59 events with 837 guards (19 of them disjunctions, some of which themselves nested)
  • Bosch are interested in deadlocks that are possible according to a flow specified using the flow plugin; these can be found with ProB by specifying a goal predicate (such as "Counter=10")
  • the proof obligation (as generated by the flow plugin) initially could not be loaded in Rodin due to "Java Heap Space Error".
  • Counter examples are found by ProB for various versions of the model in 9-24 seconds (including loading, typechecking and deadlock PO generation; the constraint solving time is 1.03 to 12.86 seconds).

BMotionStudio for Industrial Models

Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.

In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:

  • We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
  • Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
  • We introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.

Various other improvements

mainly inspired by Siemens and Bosch Applications

  • Improved AVL algorithms, more operators
  • record support: automatic detection of records described by a bijection between a cartesian product and a carrier set (these axioms can either be entered manually, such as in the Bosch models, or generated by the Records plug-in).
  • treatment of infinite sets, in particular complement sets such as INTEGER \ {x}. Such sets are being used in some of the Siemens models.
  • Partitioning of predicates into connected sub-components (was useful for Siemens application, to be able to pinpoint location of an inconsistency in the axioms; it turned out useful for constraint-based deadlock checking as well)
  • Improved constraint solving, better use of Prolog's CLP(FD) constraint solver
  • reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel

Motivations

The above works were motivated mainly to support the following three industrial deployments:

  • Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
  • Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
  • SAP: provide a way to generate test cases using constraint-based animation

Available Documentation

References

  1. ↑ 1.0 1.1 Michael Leuschel, Jérôme Falampin, Fabian Fritz and Daniel Plagge, Automated Property Verification for Large Scale B Models, FM'2009, LNCS 5850, Springer-Verlag, 2009
  2. ↑ Leuschel et al. FAC, special issue of FM'2009
  3. ↑ Leuschel et al. Draft of Validation Report
  4. ↑ Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Refinement-Animation for Event-B - Towards a Method of Validation, ASM'2010, LNCS 5977, Springer-Verlag, 2010
  5. ↑ Stefan Hallerstede, Michael Leuschel and Daniel Plagge, Validation of Formal Models by Refinement Animation, to appear in Science of Computer Programming, Elsevier

Planning

  • Finish Validation Report
  • Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
  • Support mathematical extensions in ProB
  • Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Constrained_Dynamic_Parser&oldid=2527’