SiemensComplicatedProp: Difference between revisions

No edit summary
No edit summary
Line 3: Line 3:


<pre>
<pre>
(!iti_ztr.(iti_ztr: t_iti_ztr_pas =>
!iti_ztr.(iti_ztr: t_iti_ztr_pas =>
   !(cv_ztr1,cv_ztr2).(cv_ztr1: t_cv_ztr & cv_ztr2: t_cv_ztr &
   !(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 &
    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}] &
        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 &
    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}] &
        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)
    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_ztr1)
                       |->inv_ztr_cv_pas_i(inv_iti_ztr_pas_i(iti_ztr)|->cv_ztr2)
                       |->inv_ztr_cv_pas_i(inv_iti_ztr_pas_i(iti_ztr)|->cv_ztr2)
       :
       :
    dom(inv_cv_sens_orientation))))
    dom(inv_cv_sens_orientation)))
</pre>
</pre>



Revision as of 13:02, 25 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.

GraphicalViewerSiemensSaoPauloL9.png