External Functions - Revision history

Jan Gruteser: /* Standard Libraries provided by ProB */

2025-04-02T05:36:28Z

Standard Libraries provided by ProB

← Older revision		Revision as of 05:36, 2 April 2025
Line 24:		Line 24:
	* <tt>LibraryCSV.def</tt>: contains a <tt>READ_CSV</tt> external function to read in CSV files or strings and convert them to a B data structure		* <tt>LibraryCSV.def</tt>: contains a <tt>READ_CSV</tt> external function to read in CSV files or strings and convert them to a B data structure
	* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)		* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)
	* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains <tt>~~READ_JSON~~</tt> to read JSON files and converting them to the same B format.		* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains <tt>READ_JSON_AS_XML</tt>/<tt>READ_JSON_FROM_STRING_AS_XML</tt> to read JSON files and converting them to the same B format.
	* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).		* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).
	* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).		* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).

Michael Leuschel: /* Standard Libraries provided by ProB */

2025-03-28T07:15:17Z

Standard Libraries provided by ProB

← Older revision		Revision as of 07:15, 28 March 2025
Line 29:		Line 29:
	* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.		* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.
	* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.		* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.
	* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON ~~communication library either over regular sockets or ZMQ sockets.mch</tt>: providing access to a JSON communication~~ library either over regular sockets or ZMQ sockets. More information is available on [[JSON and Sockets]].		* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON RPC (Remote Procedure Call) library either over regular sockets or ZMQ sockets. More information is available on [[JSON and Sockets]].

	Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).		Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).

Michael Leuschel: /* Standard Libraries provided by ProB */

2025-03-28T07:08:12Z

Standard Libraries provided by ProB

← Older revision		Revision as of 07:08, 28 March 2025
Line 29:		Line 29:
	* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.		* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.
	* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.		* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.
	* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.		* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets. More information is available on [[JSON and Sockets]].

	Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).		Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).

Michael Leuschel: /* Standard Libraries provided by ProB */

2025-03-28T07:00:41Z

Standard Libraries provided by ProB

← Older revision		Revision as of 07:00, 28 March 2025
Line 28:		Line 28:
	* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).		* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).
	* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.		* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.
	* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.		* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.
			* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.

	Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).		Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).

Michael Leuschel: /* Standard Libraries provided by ProB */

2025-03-28T06:57:41Z

Standard Libraries provided by ProB

← Older revision		Revision as of 06:57, 28 March 2025
Line 28:		Line 28:
	* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).		* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).
	* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.		* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.
			* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets.

	Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).		Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).

Jan Gruteser: /* Standard Libraries provided by ProB */

2024-05-11T06:37:42Z

Standard Libraries provided by ProB

← Older revision		Revision as of 06:37, 11 May 2024
Line 33:		Line 33:
	To use a library machine you can use the <tt>SEES</tt> mechanism:		To use a library machine you can use the <tt>SEES</tt> mechanism:
	SEES LibraryMath		SEES LibraryMath
			Note that for rules machines (.rmch) you have to use <tt>REFERENCES</tt> instead.

	In general you can do the following with an external function, such as <tt>sin</tt>, wrapped into a constant:		In general you can do the following with an external function, such as <tt>sin</tt>, wrapped into a constant:
	* apply the function: <tt>sin(x)</tt>		* apply the function: <tt>sin(x)</tt>

Jan Gruteser: /* Standard Libraries provided by ProB */

2024-05-10T14:14:43Z

Standard Libraries provided by ProB

← Older revision		Revision as of 14:14, 10 May 2024
Line 15:		Line 15:
	* <tt>LibraryMath.mch</tt>: defining sin, cos, tan, sinx, cosx, tanx, logx, gcd, msb, random as well as access to all other Prolog built-in arithmetic functions.		* <tt>LibraryMath.mch</tt>: defining sin, cos, tan, sinx, cosx, tanx, logx, gcd, msb, random as well as access to all other Prolog built-in arithmetic functions.
	* <tt>LibraryStrings.mch</tt>: functions manipulating B STRING objects by providing <tt>length</tt>, <tt>append</tt>, <tt>split</tt> and conversion functions <tt>chars</tt>, <tt>codes</tt>.		* <tt>LibraryStrings.mch</tt>: functions manipulating B STRING objects by providing <tt>length</tt>, <tt>append</tt>, <tt>split</tt> and conversion functions <tt>chars</tt>, <tt>codes</tt>.
	* <tt>LibraryStrings.def</tt> used by <tt>LibraryStrings.mch</tt>: providing ~~directa~~ access to various operators on strings (<tt>STRING_LENGTH</tt>, <tt>STRING_APPEND</tt>, <tt>STRING_SPLIT</tt> <tt>INT_TO_STRING</tt>,...)		* <tt>LibraryStrings.def</tt> used by <tt>LibraryStrings.mch</tt>: providing direct access to various operators on strings (<tt>STRING_LENGTH</tt>, <tt>STRING_APPEND</tt>, <tt>STRING_SPLIT</tt> <tt>INT_TO_STRING</tt>,...)
	* <tt>LibraryFiles.mch</tt>: various functions to obtain information about files and directories in the underlying file system		* <tt>LibraryFiles.mch</tt>: various functions to obtain information about files and directories in the underlying file system
	* <tt>LibraryIO.def</tt>: providing functions to write information to screen or file. Note: these external functions are polymorphic and as such cannot be defined as B constants: you have to use the DEFINITIONS provided in <tt>LibraryIO.def</tt>.		* <tt>LibraryIO.def</tt>: providing functions to write information to screen or file. Note: these external functions are polymorphic and as such cannot be defined as B constants: you have to use the DEFINITIONS provided in <tt>LibraryIO.def</tt>.

Jan Gruteser: /* Standard Libraries provided by ProB */

2024-05-10T11:42:08Z

Standard Libraries provided by ProB

← Older revision		Revision as of 11:42, 10 May 2024
Line 22:		Line 22:
	* <tt>LibraryReals.def</tt>: providing access to operators on [[Reals and Floats]] (<tt>RSIN</tt>, <tt>RCOS</tt>, <tt>RTAN</tt>, <tt>REXP</tt>, <tt>ROUND</tt>, <tt>RLOG</tt>,<tt>RSQRT</tt>,...).		* <tt>LibraryReals.def</tt>: providing access to operators on [[Reals and Floats]] (<tt>RSIN</tt>, <tt>RCOS</tt>, <tt>RTAN</tt>, <tt>REXP</tt>, <tt>ROUND</tt>, <tt>RLOG</tt>,<tt>RSQRT</tt>,...).
	* <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)		* <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)
			* <tt>LibraryCSV.def</tt>: contains a <tt>READ_CSV</tt> external function to read in CSV files or strings and convert them to a B data structure
	* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)		* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)
	* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains <tt>READ_JSON</tt> to read JSON files and converting them to the same B format.		* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains <tt>READ_JSON</tt> to read JSON files and converting them to the same B format.

Michael Leuschel: /* Standard Libraries provided by ProB */

2024-02-23T10:07:02Z

Standard Libraries provided by ProB

← Older revision		Revision as of 10:07, 23 February 2024
Line 23:		Line 23:
	* <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)		* <tt>LibraryRegex.def</tt>: providing access to regular expression operators on strings (<tt>REGEX_MATCH</tt>, <tt>REGEX_REPLACE</tt>, <tt>REGEX_SEARCH</tt>,...)
	* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)		* <tt>LibrarySVG.def</tt>: providing utility functions for VisB (<tt>svg_points</tt>, <tt>svg_axis</tt>,...)
	* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records.		* <tt>LibraryXML.def</tt>: contains a <tt>READ_XML</tt> external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains <tt>READ_JSON</tt> to read JSON files and converting them to the same B format.
	* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).		* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).
	* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).		* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).

Jan Gruteser: /* Standard Libraries provided by ProB */

2023-12-29T17:30:20Z

Standard Libraries provided by ProB

← Older revision		Revision as of 17:30, 29 December 2023
Line 26:		Line 26:
	* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).		* <tt>LibraryBits.def</tt>: contains bit-manipulation functions on integers (<tt>BNOT</tt>, <tt>BAND</tt>, <tt>BXOR</tt>,...).
	* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).		* <tt>SORT.def</tt>: providing sorting related functions (<tt>SORT</tt>, <tt>SQUASH</tt>, <tt>REPLACE</tt>).
	* <tt>SCCS.ef</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.		* <tt>SCCS.def</tt>: providing access to <tt>SCCS</tt> to compute the strongly connected components of a relation and <tt>CLOSURE1</tt> an alternative algorithm for compting the transitive closure of a relation.

	Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).		Since version 1.5 the standard library is shipped with ProB and references to machines and DEFINITION-files in the standard library are resolved automatically when referenced (see [[PROBPATH]] for information about how to customize the lookup path).