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. | ||
[[File:GraphicalViewerSiemensSaoPauloL9.png]] | [[File:GraphicalViewerSiemensSaoPauloL9.png|700px]] | ||
Revision as of 12:59, 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.
