SiemensComplicatedProp - Revision history

Michael Leuschel at 07:34, 26 October 2010

2010-10-26T07:34:27Z

← Older revision		Revision as of 07:34, 26 October 2010
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.

Michael Leuschel at 07:34, 26 October 2010

2010-10-26T07:34:12Z

← Older revision		Revision as of 07:34, 26 October 2010
Line 19:		Line 19:
	It stems from a Siemens model for the automatic controller for Line 9 of Sao Paulo.		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.		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.


	[[File:GraphicalViewerSiemensSaoPauloL9.png\|700px]]		[[File:GraphicalViewerSiemensSaoPauloL9.png\|700px]]

Michael Leuschel at 13:03, 25 October 2010

2010-10-25T13:03:00Z

← Older revision		Revision as of 13:03, 25 October 2010
Line 6:		Line 6:
	!(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)
	=>		=>

Michael Leuschel at 13:02, 25 October 2010

2010-10-25T13:02:46Z

← Older revision		Revision as of 13:02, 25 October 2010
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>

Michael Leuschel at 13:02, 25 October 2010

2010-10-25T13:02:13Z

← Older revision		Revision as of 13:02, 25 October 2010
Line 6:		Line 6:
	!(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)
	=>		=>

Michael Leuschel at 13:01, 25 October 2010

2010-10-25T13:01:59Z

← Older revision		Revision as of 13:01, 25 October 2010
Line 6:		Line 6:
	!(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)
	=>		=>

Michael Leuschel at 12:59, 25 October 2010

2010-10-25T12:59:46Z

← Older revision		Revision as of 12:59, 25 October 2010
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]]

Michael Leuschel at 12:58, 25 October 2010

2010-10-25T12:58:38Z

← Older revision		Revision as of 12:58, 25 October 2010
Line 1:		Line 1:
	~~This shows~~ the graphical visualisation of a complicated property by ProB's graphical formula viewer.		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\|PDF File]].
	The property is the following one:		The property is the following one:

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.~~pdf~~]]		[[File:GraphicalViewerSiemensSaoPauloL9.png]]

Michael Leuschel: Created page with 'This shows the graphical visualisation of a complicated property by ProB's graphical formula viewer. The property is the following one:

 (!iti_ztr.(iti_ztr: t_iti_ztr_pas =…'

2010-10-25T12:56:35Z

Created page with 'This shows the graphical visualisation of a complicated property by ProB's graphical formula viewer. The property is the following one: <pre> (!iti_ztr.(iti_ztr: t_iti_ztr_pas =…'

New page

This shows the graphical visualisation of a complicated property by ProB's graphical formula viewer.
The property is the following one:

<pre>
(!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))))
</pre>

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.

[[File:GraphicalViewerSiemensSaoPauloL9.pdf]]