SiemensComplicatedProp

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.