No edit summary |
Jan Gruteser (talk | contribs) |
||

(10 intermediate revisions by 2 users not shown) | |||

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 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>. | ||

* <tt>CHOOSE.def</tt>: providing the [http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html Hilbert choice operator] for choosing a designated element from each set. Again, this function is polymorphic and thus cannot be defined as a B function. This function is useful for defining [[Recursively_Defined_Functions|recursive functions]] over sets (see also [[TLA]]). Note that it in ProB it is undefined for the empty set. | * <tt>CHOOSE.def</tt>: providing the [http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html Hilbert choice operator] for choosing a designated element from each set. Again, this function is polymorphic and thus cannot be defined as a B function. This function is useful for defining [[Recursively_Defined_Functions|recursive functions]] over sets (see also [[TLA]]). Note that it in ProB it is undefined for the empty set. | ||

* <tt>LibraryMeta.def</tt>: providing access to meta-information about the loaded model (<tt>PROJECT_INFO</tt>), about the state space (<tt>HISTORY</tt>, < | * <tt>LibraryMeta.def</tt>: providing access to meta-information about the loaded model (<tt>PROJECT_INFO</tt>), about the state space (<tt>HISTORY</tt>, <tt>STATE_TRANS</tt>, ...) and about ProB itself (<tt>GET_PREF</tt>, <tt>PROB_INFO_STR</tt>, <tt>PROB_INFO_INT</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>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>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>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. | |||

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). | ||

Line 25: | 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> |

As of version 1.3.5-beta7 ProB can make use of externally defined functions.
These functions must currently be written in Prolog (in principle C, Java, Tcl or even other languages can be used via the SICStus Prolog external function interfaces).
These functions can be used to write *expression*, *predicates*, or *substitutions*.
The general mechanism that is used is to mark certain DEFINITIONS as external, in which case ProB will make use of external Prolog code rather than using the right-hand-side of the DEFINITION whenever it is used. However, these DEFINITIONS can often (unless they are polymorphic) be wrapped into B (constant) functions. If you just want to use the standard external functions already defined by ProB, then you don't have to understand this mechanism in detail (or at all).

We have a PDF describing the external functions generated from a ProB-Jupyter notebook: File:ExternalFunctions.pdf The Notebook is available and can now be launched via binder.

In a first instance we have predefined a series of external functions and grouped them in various library machines and definition files:

`LibraryMath.mch`: defining sin, cos, tan, sinx, cosx, tanx, logx, gcd, msb, random as well as access to all other Prolog built-in arithmetic functions.`LibraryStrings.mch`: functions manipulating B STRING objects by providing`length`,`append`,`split`and conversion functions`chars`,`codes`.`LibraryStrings.def`used by`LibraryStrings.mch`: providing direct access to various operators on strings (`STRING_LENGTH`,`STRING_APPEND`,`STRING_SPLIT``INT_TO_STRING`,...)`LibraryFiles.mch`: various functions to obtain information about files and directories in the underlying file system`LibraryIO.def`: 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`LibraryIO.def`.`CHOOSE.def`: providing the Hilbert choice operator for choosing a designated element from each set. Again, this function is polymorphic and thus cannot be defined as a B function. This function is useful for defining recursive functions over sets (see also TLA). Note that it in ProB it is undefined for the empty set.`LibraryMeta.def`: providing access to meta-information about the loaded model (`PROJECT_INFO`), about the state space (`HISTORY`,`STATE_TRANS`, ...) and about ProB itself (`GET_PREF`,`PROB_INFO_STR`,`PROB_INFO_INT`,..).`LibraryReals.def`: providing access to operators on Reals and Floats (`RSIN`,`RCOS`,`RTAN`,`REXP`,`ROUND`,`RLOG`,`RSQRT`,...).`LibraryRegex.def`: providing access to regular expression operators on strings (`REGEX_MATCH`,`REGEX_REPLACE`,`REGEX_SEARCH`,...)`LibraryCSV.def`: contains a`READ_CSV`external function to read in CSV files or strings and convert them to a B data structure`LibrarySVG.def`: providing utility functions for VisB (`svg_points`,`svg_axis`,...)`LibraryXML.def`: contains a`READ_XML`external function to read in XML files or strings and convert them to a B data structure with strings and records. Also contains`READ_JSON`to read JSON files and converting them to the same B format.`LibraryBits.def`: contains bit-manipulation functions on integers (`BNOT`,`BAND`,`BXOR`,...).`SORT.def`: providing sorting related functions (`SORT`,`SQUASH`,`REPLACE`).`SCCS.def`: providing access to`SCCS`to compute the strongly connected components of a relation and`CLOSURE1`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).

To use a library machine you can use the `SEES` mechanism:

SEES LibraryMath

Note that for rules machines (.rmch) you have to use `REFERENCES` instead.

In general you can do the following with an external function, such as `sin`, wrapped into a constant:

- apply the function:
`sin(x)` - compute the image of the function:
`sin[1..100]` - compose the function with a finite relation on the left:
`([1..100] ; sin)` - compute the domain of the function:
`dom(sin)`

To use a library definition file, you need to include the file in the DEFINITIONS clause:

DEFINITIONS "LibraryIO.def"

Currently, external functions are linked to classical B machines using B DEFINITIONS as follows:

- one definition, which defines the function as it is seen by tools other than ProB (e.g., Atelier-B). Suppose we want to declare an external cosinus function named
`COS`, then this definition could be`COS(x) == cos(x)`. - one definition declaring the type of the function. For
`COS`this would be`EXTERNAL_FUNCTION_COS == INTEGER --> INTEGER`. - Prolog code which gets called by ProB in place of the right-hand-side of the first definition

Usually, it is also a good idea to encapsulate the external function inside a CONSTANT which is defined as a lambda abstraction with as body simply the call to the first DEFINITION. For `COS` this would be `cos = %x.(x:NATURAL|COS(x))`. Observe that for Atelier-B this is a tautology.
For ProB, the use of such a constant allows one to have a real B function representing the external function, for which we can compute the domain, range, etc.

For the typing of an external function `NAME` with type `TYPE` there are three possibilities, depending on whether the function is a function, a predicate or a substitution:

`EXTERNAL_FUNCTION_NAME == TYPE``EXTERNAL_PREDICATE_NAME == TYPE``EXTERNAL_SUBSTITUTION_NAME == TYPE`

In case the external function is polymorphic, the `DEFINITION` can take extra arguments: each argument is treated like a type variable.
For example, the following is used in `CHOOSE.def` to declare the Hilbert choice operator:

`EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)`