SiemensComplicatedProp: Difference between revisions

No edit summary
No edit summary
 
Line 20: Line 20:
The property defied validation using Atelier B or alternate methods.
The property defied validation using Atelier B or alternate methods.


Indeed, the property  is related to routes from one zone controller to another one:
Indeed, the property  is related to routes from one zone controller to another one: each route is decomposed into virtual blocks, each virtual block is linked with another virtual block by a function, and each couple of blocks has a direction.
each route is decomposed into virtual blocks, each virtual block is linked with another virtual block by a function, and each couple of blocks has a direction.
This property checks the coherence of all these items.
This property checks the coherence of all these items.
This property involves several large functions, with images of images of functions, and has a double universal quantifier. All this lead to a proof tree and a goal size that is beyond the capabilities of Atelier B.
This property involves several large functions, with images of images of functions, and has a double universal quantifier. All this lead to a proof tree and a goal size that is beyond the capabilities of Atelier B.

Latest revision as of 07:34, 26 October 2010

Below we show the graphical visualisation of a complicated property by ProB's graphical formula viewer. The graphics are also available as File:GraphicalViewerSiemensSaoPauloL9.pdf. The property is the following one:

!iti_ztr.(iti_ztr: t_iti_ztr_pas =>
  !(cv_ztr1,cv_ztr2).(cv_ztr1: t_cv_ztr & cv_ztr2: t_cv_ztr &
    cv_ztr1: {aa,bb | aa: t_iti_ztr_pas & bb: t_cv_ztr &
      bb: inv_iti_ztr_cv_liste_i[inv_iti_ztr_cv_deb(aa)..inv_iti_ztr_cv_fin(aa)]}[{iti_ztr}] &
    cv_ztr2: {aa,bb | aa: t_iti_ztr_pas & bb: t_cv_ztr &
      bb: inv_iti_ztr_cv_liste_i[inv_iti_ztr_cv_deb(aa)..inv_iti_ztr_cv_fin(aa)]}[{iti_ztr}] &
    not(cv_ztr1 = cv_ztr2)
   =>
    inv_ztr_cv_pas_i(inv_iti_ztr_pas_i(iti_ztr)|->cv_ztr1)
                      |->inv_ztr_cv_pas_i(inv_iti_ztr_pas_i(iti_ztr)|->cv_ztr2)
      :
    dom(inv_cv_sens_orientation)))

It stems from a Siemens model for the automatic controller for Line 9 of Sao Paulo. The property defied validation using Atelier B or alternate methods.

Indeed, the property is related to routes from one zone controller to another one: each route is decomposed into virtual blocks, each virtual block is linked with another virtual block by a function, and each couple of blocks has a direction. This property checks the coherence of all these items. This property involves several large functions, with images of images of functions, and has a double universal quantifier. All this lead to a proof tree and a goal size that is beyond the capabilities of Atelier B.


GraphicalViewerSiemensSaoPauloL9.png