CSP-M - Revision history

David Geleßus: Update paper link

2021-02-04T15:33:19Z

Update paper link

← Older revision		Revision as of 15:33, 4 February 2021
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/~~~leuschel~~/~~publication_detail~~.~~php?id=1~~]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".		ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [https://www3.hhu.de/stups/downloads/pdf/LeBu05_1.pdf]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

	You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:		You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:

Daniel Plagge: /* Command Line option for guided CSP||B */

2012-03-20T06:13:27Z

Command Line option for guided CSP||B

← Older revision		Revision as of 06:13, 20 March 2012
Line 39:		Line 39:
	For the syntax definition see [[CSP-M Syntax]]		For the syntax definition see [[CSP-M Syntax]]

	=== Command Line option for guided CSP\|\|B ===		====== Command Line option for guided CSP\|\|B ======
	From the command line, you can specify a CSP File that should be used to guide the B machine with		From the command line, you can specify a CSP File that should be used to guide the B machine with
	-csp-guide <Filename>		-csp-guide <Filename>
			(This feature is included since version 1.3.5-beta7.)

	== References ==		== References ==
	<references />		<references />

Daniel Plagge: /* Guiding B Machines with CSP */

2012-03-20T06:09:58Z

Guiding B Machines with CSP

← Older revision		Revision as of 06:09, 20 March 2012
Line 38:		Line 38:

	For the syntax definition see [[CSP-M Syntax]]		For the syntax definition see [[CSP-M Syntax]]

			=== Command Line option for guided CSP\|\|B ===
			From the command line, you can specify a CSP File that should be used to guide the B machine with
			-csp-guide <Filename>

	== References ==		== References ==
	<references />		<references />

Michael Leuschel: /* Limitations of CSP-M Support */

2012-01-23T11:31:08Z

Limitations of CSP-M Support

← Older revision		Revision as of 11:31, 23 January 2012
Line 12:		Line 12:
	* currying and lambda expressions have only been partially tested		* currying and lambda expressions have only been partially tested
	* extensions and productions are not yet supported (but {\| \|} is)		* extensions and productions are not yet supported (but {\| \|} is)
	* the priority of rename compared to external choice is unfortunately different than in FDR; please use ~~parenthesis~~		* the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
	* mixing of closure with other set operations (especially diff) is not yet fully supported		* mixing of closure with other set operations (especially diff) is not yet fully supported
	* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.		* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.

Michael Leuschel: /* Limitations of CSP-M Support */

2012-01-23T11:29:38Z

Limitations of CSP-M Support

← Older revision		Revision as of 11:29, 23 January 2012
Line 12:		Line 12:
	* currying and lambda expressions have only been partially tested		* currying and lambda expressions have only been partially tested
	* extensions and productions are not yet supported (but {\| \|} is)		* extensions and productions are not yet supported (but {\| \|} is)
			* the priority of rename compared to external choice is unfortunately different than in FDR; please use parenthesis
	* mixing of closure with other set operations (especially diff) is not yet fully supported		* mixing of closure with other set operations (especially diff) is not yet fully supported
	* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.		* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.

Michael Leuschel: /* Limitations of CSP-M Support */

2012-01-23T11:26:24Z

Limitations of CSP-M Support

← Older revision		Revision as of 11:26, 23 January 2012
Line 10:		Line 10:

	ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues		ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
	* assert declarations are ignored
	* currying and lambda expressions have only been partially tested		* currying and lambda expressions have only been partially tested
	* extensions and productions are not yet supported (but {\| \|} is)		* extensions and productions are not yet supported (but {\| \|} is)

Joy Clark: "", s to z

2011-04-18T11:54:17Z

"", s to z

← Older revision		Revision as of 11:54, 18 April 2011
Line 3:		Line 3:
	ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".		ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

	You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" ~~submenu~~ of the File menu:		You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:
	* use CSP file: uses the CSP file to control the current B machine (see below)		* use CSP file: uses the CSP file to control the current B machine (see below)
	* use default CSP file: trys to use a CSP with the same name as the current B machine to control it		* use default CSP file: trys to use a CSP with the same name as the current B machine to control it
Line 17:		Line 17:
	* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.		* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

	Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP ~~synchronisation~~ constructs).		Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronization constructs).

	== Guiding B Machines with CSP ==		== Guiding B Machines with CSP ==

Joy Clark: grammatical edits, punctuation edits

2011-04-14T13:34:52Z

grammatical edits, punctuation edits

Joy Clark: /* Limitations of CSP-M Support */ changed comma to semi-colon

2011-04-12T14:51:31Z

Limitations of CSP-M Support: changed comma to semi-colon

← Older revision		Revision as of 14:51, 12 April 2011
Line 17:		Line 17:
	* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.		* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

	Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved; especially with deeply nested CSP synchronisation constructs).		Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronisation constructs).

	== Guiding B Machines with CSP ==		== Guiding B Machines with CSP ==

Joy Clark: /* Limitations of CSP-M Support */ added a but

2011-04-12T14:50:57Z

Limitations of CSP-M Support: added a but

← Older revision		Revision as of 14:50, 12 April 2011
Line 15:		Line 15:
	* mixing of closure with other set operations (especially diff) not yet fully supported		* mixing of closure with other set operations (especially diff) not yet fully supported
	* input patterns can only contain variables,tuples,integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.		* input patterns can only contain variables,tuples,integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
	* channel declarations can either use associative dot tuples or non-associative tuples, not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.		* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

	Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved; especially with deeply nested CSP synchronisation constructs).		Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved; especially with deeply nested CSP synchronisation constructs).

← Older revision		Revision as of 13:34, 14 April 2011
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref>, as supported by FDR and ProBE. CSP files can be animated and model checked on their own, simply by opening a file ending with ".csp".		ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref> as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

	You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" submenu of the File menu:		You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" submenu of the File menu:
Line 13:		Line 13:
	* currying and lambda expressions have only been partially tested		* currying and lambda expressions have only been partially tested
	* extensions and productions are not yet supported (but {\| \|} is)		* extensions and productions are not yet supported (but {\| \|} is)
	* mixing of closure with other set operations (especially diff) not yet fully supported		* mixing of closure with other set operations (especially diff) is not yet fully supported
	* input patterns can only contain variables,tuples,integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.		* input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
	* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.		* channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

Line 26:		Line 26:
	The CSP file should define a process called "MAIN".		The CSP file should define a process called "MAIN".
	This process will be executed in parallel with the B machine.		This process will be executed in parallel with the B machine.
	The ~~synchronisation~~ between the B machine and the CSP specification is as follows:		The synchronization between the B machine and the CSP specification is as follows:
	* CSP events that have the same name as B Operations will ~~synchronise~~ with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:<pre> CSP [\| {op1,...,opn} \|] B</pre> where op1,...,opn are the visible operations defined in the B machine.		* CSP events that have the same name as B Operations will synchronize with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:<pre> CSP [\| {op1,...,opn} \|] B</pre> where op1,...,opn are the visible operations defined in the B machine.
	* CSP events do not need to provide all arguments of B operations:		* CSP events do not need to provide all arguments of B operations:
	add!1 -> will match add(1,1) or add(1,2) or ...		add!1 -> will match add(1,1) or add(1,2) or ...
Line 33:		Line 33:
	add -> will match add(1,2), add(2,1), ...		add -> will match add(1,2), add(2,1), ...
	add!1!2 -> will only match add(1,2)</pre>		add!1!2 -> will only match add(1,2)</pre>
	* B Output arguments are specified at the end<pre>lookup!X!2 will match lookup(X) --> 2</pre>Note, however, for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont.		* B Output arguments are specified at the end<pre>lookup!X!2 will match lookup(X) --> 2</pre>Note however, that for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont.
	* If you have a variable called vv then you can use vv?VAL to get the value of vv. You can also use, ~~e.g.~~, vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. ~~E.g.~~, vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).		* If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. For example, use vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
	* see the file "bookstore_guide.csp" in the provided Machines directory for an example.		* see the file "bookstore_guide.csp" in the provided Machines directory for an example.