Skip to content
Snippets Groups Projects
Commit 539f0cdc authored by dgelessus's avatar dgelessus
Browse files

Remove AdvancedFeatures section whose content can be found on the wiki

parent 7c0989c2
Branches master
No related tags found
No related merge requests found
Pipeline #54231 failed
Stage: build
Stage: deploy
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 785 deletions
src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc deleted 100644 → 0
+ 0
− 7
View file @ 7c0989c2
[[advanced-features]]
= Advanced Features
:leveloffset: +1
Over the years, the ProB Team developed a few features for advanced users.
You can find further descriptions and tutorials on how to use them in the following sections.
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 7c0989c2
[[feature-description]]
= Feature Description
:leveloffset: +1
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc deleted 100644 → 0
+ 0
− 35
View file @ 7c0989c2
[[bash-completion]]
= Bash Completion
For the http://en.wikipedia.org/wiki/Bash_(Unix_shell)[Bash] Unix Shell
we provide command completion support.
Example
....
$ probcli -re
-refchk -repl
....
[[installation-bash-completion]]
== Installation
A generated version of the command completion for Bash is available
http://nightly.cobra.cs.uni-duesseldorf.de/bash/prob_completion.sh[here].
To install download the linked file and store it locally on your
machine. To enable the completion you need to *source* the file.
....
$ source
....
To enable the completion automatically add the line above to your Bash
settings, e.g. in the *.bashrc* or *.profile* files in your home
directory.
[[contributing]]
== Contributing
Bugs and improvements can be submitted on the project's
https://github.com/bivab/prob_bash_completion[GitHub Page]
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc deleted 100644 → 0
+ 0
− 112
View file @ 7c0989c2
[[common-subexpression-elimination]]
= Common Subexpression Elimination
As of version 1.5.1 ProB supports
https://en.wikipedia.org/wiki/Common_subexpression_elimination[common
subexpression elimination (CSE)].
[[basics-of-cse]]
== Basics of CSE
To enable CSE you need to set the advanced preference `CSE` to true
(this can be done using the switch `-p CSE TRUE` when using the
<<using-the-command-line-version-of-prob,command-line version
probcli>> or using the Advanced Preferences command in ProB Tcl/Tk). With
CSE enabled, ProB will translate the predicate
`x:dom(f(a)) & r=f(a)(x)`
into
`(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))`
before evaluating it. As you can see, the common sub-expression `f(a)`
has been lifted into a LET statement. This has the advantage that the
expression `f(a)` will only get evaluated once (rather than twice, in
case `x:dom(f(a))`). Identifiers introduced by the CSE always start with
the @-sign. As another example, the predicate
`x*x+2*x > y*y*y & y*y*y > x*x+2*x`
gets translated into
`LET @2==(x*x+2*x) IN (LET @4==((y*y)*y) IN @2 > @4 & @4 > @2))`
You may observe that the B-language does not have a let-construct for
expression nor predicates (only for substitutions). There are various
ways one can overcome this (e.g., using an existential quantifier for a
predicate), but ProB adds its own LET-construct to the language in the
interpreter. Moreover, to avoid issues with well-definedness and
ensuring that ProB only evaluates the LET expressions when really
needed, this LET has a different behaviour than the "standard"
constructs. Indeed, ProB's LET is lazy, i.e., it will only evaluate the
expression when required by the computation of the body of the LET. For
example, in
`LET @1==f(a) IN 2>3 & @1+@1>10`
the expression `f(a)` will never be evaluated. This is important for
well-definedness (e.g., suppose a is not in the domain of f) and for
performance.
[[substitutions]]
== Substitutions
To enable CSE also inside substitutions (aka B statements) you need to
set the preference `CSE_SUBST` to true. By default, the CSE will only be
applied to top-level predicates, such as the invariant, the assertions,
the properties or individual predicates inside operations (but not the
operation as a whole).
[[sharing-predicates]]
== Sharing Predicates
By default ProB's CSE will also share predicates. You can turn off CSE
for predicates, i.e., only expressions get shared, by setting the
preference `CSE_PRED` to `FALSE`. For example, by default ProB's CSE
will translate
`x+1 > 10 & (x+1 > 10 => y=22)`
into
`LET @1==(x + 1 > 10) IN @1 & (@1 => y = 22)`
After setting `CSE_PRED` to `FALSE`, this will be translated into:
`LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)`
[[other-preferences]]
== Other Preferences
ProB will also share expressions which are potentially not well-defined,
and takes extra care with those expressions (in particular in the
context of set comprehensions and quantifications). However, you can
completely turn off sharing of potentially not-well defined expressions
by setting the preference `CSE_WD_ONLY` to `TRUE`. For example, by
default the following predicate
`x>1 & 100/x > 20 & 100/x <26`
will get translate into
`LET @0==(100 / x) IN (x > 1 & @0 > 20) & @0 < 26)`
and ProB will find the solution `x=4`. With `CSE_WD_ONLY` to `TRUE`, the
predicate will be left unchanged (and ProB will find the same solution).
[[tips]]
== Tips
To inspect the effect of CSE, you do one of the following:
* In ProB Tcl/Tk you can use the command "Show Internal
Representation" in the Debug menu to inspect the effect of CSE on your
machine
* For probcli, you can use the command `-pp FILE` to write the
pretty-printed internal representation of your machine after CSE to a
file
* For the REPL of probcli (command -repl), you can use the option
`-p REPL_UNICODE TRUE` to force ProB to print your
expressions/predicates after CSE processing (using Unicode characters)
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc deleted 100644 → 0
+ 0
− 32
View file @ 7c0989c2
[[probpath]]
= PROBPATH
Starting with version 1.5 of ProB, it is possible to customize where the
parser will ProB will search for referenced files.
By default ProB will try to find files referenced from a machine (using
SEES, INCLUDES, DEFINITON-files, etc) resolving paths as relative to the
current machine or within the ProB standard library.
Commonly used files can be placed in a shared location, e.g. in the
standard library (the stdlib directory in the ProB distribution) or any
custom location.
The search path can be customized by defining a PROBPATH environment
variable that contains a list of directories to be searched. On windows
the directors are separated by a ";" and on unix systems by a ":"
character, e.g.:
On unix:
`PROBPATH=\~/myproject/common:~/myotherproject/common probcli model.mch`
And on windows:
`PROBPATH=\~/myproject/common;~/myotherproject/common probcli model.mch`
will resolved referenced files relative to model.mch, then in
*~/myproject/common* then in *~/myotherproject/common* and finally in
the standard library of ProB, stopping as soon as a file with the name
being looked up is found.
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc deleted 100644 → 0
+ 0
− 144
View file @ 7c0989c2
[[tlc]]
= TLC
As of version 1.4.0, ProB can make use of
http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html[TLC]
as an alternative model checker to validate B specifications. TLC is an
efficient model checker for TLA+ specifications, which can check LTL
properties with fairness. It is particularly good for lower level
specifications, where it can be substantially faster than ProB's own
model checker. TLC has been released as an open source project, under
the
http://research.microsoft.com/en-us/um/people/lamport/tla/license.html[MIT
License].
[[how-to-use-tlc]]
== How to use TLC
[[using-tlc-in-prob-tcltk]]
=== Using TLC in ProB Tcl/Tk
First you have to open a B specification in the ProB GUI. Then you can
select the menu command "Model Check with TLC" in the
"Verify->External Tools" menu.
image::Model_Checking_With_TLC.png[]
You can use TLC to find the following kinds of errors in the B
specification:
* Deadlocks
* Invariant violations
* Assertion errors
* Goal found (a desired state is reached)
* Properties violations (i.e, axioms over the B constants are false)
* Well-definedness violations
* Temporal formulas violations
In some cases, TLC reports a trace leading to the state where the error
(e.g. deadlock or invariant violation) occur. Such traces are
automatically replayed in the ProB animator (displayed in the history
pane) to give an optimal feedback.
image::Model_Checking_With_TLC_Trace.png[]
[[requirements]]
==== Requirements
On Linux the tlc-thread package is required to run TLC from the tcl/tk
ui:
`sudo apt-get install tcl-thread`
[[using-tlc-in-probcli]]
=== Using TLC in probcli
You can use the following switch to use TLC rather than ProB's model
checker:
`-mc_with_tlc`
Some of the standard probcli options also work for TLC:
* -noinv (no invariant checking)
* -nodead (no deadlock checking)
* -noass (no assertion checking)
* -nogoal (no checking for the optional goal predicate)
In addition you can provide
* -noltl (no checking of LTL assertions)
The preference `TLC_WORKERS` influences the number of workers that will
be used by TLC. So, a call might look like this:
`probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl`
[[when-to-use-tlc]]
== When to use TLC
TLC is extremely valuable when it comes to explicit state model checking
for large state spaces. Otherwise, TLC has no constraint solving
abilities.
[[translation-from-b-to-tla]]
Translation from B to TLA+
--------------------------
TLC is a very efficient model checker for specifications written in
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+].
To validate B specification with TLC we developed the translator TLC4B
which automatically translates a B specification to TLA+, invokes the
model checker TLC, and translates the results back to B. Counter
examples produced by TLC are double checked by ProB and replayed in the
ProB animator. The translation to TLA+ and back to B is completely
hidden to the user. Hence, the user needs no knowledge of TLA+ to use
TLC.
There is a
http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport[technical
report] that describes our translation from B to TLA+.
[[limitations-tlc]]
== Limitations
The following constructs are currently not supported by the TLC4B
translator:
* Refinement specifications
* Machine inclusion (SEES, INCLUDES, ..)
* Sequential composition statement (G;H)
[[visited-states]]
== Visited States
Sometimes TLC will show a different number of visited states compared to
the ProB model checker. The following example should illustrate this
issue:
....
MACHINE NumberOfStates
CONSTANTS k
PROPERTIES
k : 1..10
VARIABLES x
INVARIANT
x : NATURAL
INITIALISATION x := k
END
....
ProB will report 21 distinct states (1 root state, 10 constant setup
states, 10 initialization states):
image::NumberOfStates.jpeg[]
TLC will only report 10 distinct states (10 initialization states).
[[more-information]]
== More Information
More information can be found in our
https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_ABZ14.pdf[ABZ'14
article].
src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 7c0989c2
:leveloffset: -1
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 7c0989c2
[[using-prob]]
= Using ProB
:leveloffset: +1
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc deleted 100644 → 0
+ 0
− 107
View file @ 7c0989c2
[[generating-documents-with-prob-and-latex]]
= Generating Documents with ProB and Latex
ProB can (as of version 1.6.1) be used to process Latex files, i.e., the
command-line tool probcli scans a given Latex file and replaces certain
commands by processed results.
[[usage-generating-documents]]
== Usage
A typical usage would be as follows:
....
probcli FILE -init -latex Raw.tex Final.tex
....
Note: the FILE and -init commands are optional; they are required in
case you want to process the commands in the context of a certain model.
Currently the probcli Latex commands mainly support B and Event-B
models, TLA+ and Z models can also be processed but all commands below
expect B syntax. You can add more commands if you wish, e.g., set
preferences using `-p PREF VAL` or run model checking `--model-check`.
The Latex processing will take place after most other commands, such as
model checking.
You will probably want to put the probcli call into a Makefile, in
particular when you want to generate dot graphics using ProB.
The distribution folder of ProB contains an example with a Makefile,
producing the following file, which at the same time documents the core
features:
https://www3.hhu.de/stups/prob/images/7/7f/Prob_latex_doc.pdf[ProB Latex Documentation]
[[commands]]
== Commands
The commands are described in the PDF document above. Here is a short
summary of some of the commands:
* `\probexpr{EXRP}` command takes a B expression `EXPR`as argument and
evaluates it. By default it shows the B expression and the value of the
expression. Example: `\probexpr` will be replaced by `{1,1024}`
** `ascii` to print the result as ASCII rather than using Latex math
symbols
** `time` to display the time taken for the command
** `string` the result value is a string, and do not print the quotes
around the string
** `value` to just print the value, not the expression
* `\probrepl{CMD}` command takes a probcli REPL command `CMD` as
argument and executes it. By default it shows only the output of the
execution, e.g., in case it is a predicate TRUE or FALSE. Example:
`\probrepl{let DOM = 1..3}`. A variation of the latter is the new
command `\problet{DOM}{1..3}` which shows the let construct itself
within the generated Latex. Optional arguments for `\probrepl` are :
** `solution` to display the solution bindings (for existential
variables) found by ProB
** `store` to store the solution bindings as local variables (similar to
let)
** `ascii` to print the result as ASCII rather than using Latex math
symbols
** `time` to display the time taken for the command
** `print` to print the expression/predicate being evaluated
(automatically set by `\problet`
** `silent` to not print the result of the evaluation
* `\probtable{EXRP}` command takes a B expression `EXPR`as argument,
evaluates it and shows it as a Latex table. Optional arguments are
`no-tabular`, `no-hline`, `no-headings`, `no-row-numbers`,
`max-table-size=NR`.
* `\probdot{DOT}{File1}` command takes a B expression `EXPR`as argument,
evaluates it as a graph and writes a dot file `File1`. You can provide a
second File as argument, in which case `dot` is called to generate a PDF
document. You can also set `sfdp` as third argument, in which case the
`sfdp` tool will be used instead of `dot`.
* `\probprint{EXRP}` command takes a B expression or predicate `EXPR`as
argument and pretty prints it. Optional arguments are:
** `pred` only try to parse first argument as predicate
** `expr` only try to parse first argument as expression
** `ascii` to print the result as ASCII rather than using Latex math
symbols
* `\probif{EXPR}{Then}{Else}` command takes an expression or predicate
`EXPR` and two Latex texts. If the expression evaluates to TRUE the
first branch `Then` is processed, otherwise the other one `Else` is
processed.
* `\probfor{ID}{Set}{Body}` command takes an identifier `ID`, a set
expression `Set` and a Latex text `Body`, and processes the Latex text
for every element of the set expression, setting the identifier to a
value of the set.
[[some-examples]]
== Some Examples
* Presentation held in Grenoble in September 2016 about "Constraint
Programming Puzzles in B"
https://www3.hhu.de/stups/prob/images/2/2d/Puzzle_latex_presentation.pdf[Puzzle Latex Presentation]
* SBMF'2016 keynote article:
https://www3.hhu.de/stups/prob/images/1/17/Sbmf_2016_latex.pdf[Formal Model-Based Constraint Solving and Document Generation]
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc deleted 100644 → 0
+ 0
− 95
View file @ 7c0989c2
[[using-prob-with-atelier-b]]
= Using ProB with Atelier B
As of version 1.3,
ProB contains a much improved parser which tries be compliant with
Atelier B as much as possible.
[[atelier-b-plugin]]
== Atelier B Plugin
There is also a
http://tools.clearsy.com/tools/atelier-b-4-0-gui/external-tools-integration/prob-etool-generation/[plugin
for Atelier B] for use withthe standalone Tcl/Tk Version on
http://www.atelierb.eu/[Atelier B] projects.
[[differences-with-atelier-b]]
== Differences with Atelier B
[[extra-features-of-prob]]
=== Extra Features of ProB
* Identifiers: ProB also allows identifiers consisting of a single
letter. ProB also accepts enumerated set elements to be used as
identifiers.
* Lexing: The Atelier-B parser (`bcomp`) reports a lexical error
(`illegal token |-`) if the vertical bar (|) of a lambda abstraction is
followed directly by the minus sign.
* Typing:
** ProB makes use of a unification-based type inference algorithm. As
such, typing information can not only flow from left-to-right inside a
formula, but also from right-to-left. For example, it is sufficient to
type `xx<:yy & yy<:NAT` instead of typing both `xx` and `yy` in ProB.
** Similar to Rodin, ProB extracts typing information from all
predicates. As such, it is sufficient to write `xx/:{1,2}` to assign a
type to `xx`.
** the fields of records are normalized (sorted); hence the predicate
`rec(a:0,b:1) = rec(b:y,a:x)` is correctly typed for ProB.
* DEFINITIONS: the definitions and its arguments are checked by ProB. We
believe this to be an important feature for a formal method language.
However, as such, every DEFINITION must be either a predicate, an
expression or a substitution. You *cannot* use, for example, lists of
identifiers as a definition. Also, for the moment, the arguments to
DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS
the associativity is not changed. E.g., with `PLUS(x,y) == x+y`, the
expression `PLUS(2,3)*10` will evaluate to 50 (and not to 32 as with
Atelier-B).
* for a LET substitution, Atelier-B does not allow introduced
identifiers to be used in the right-hand side of equations; ProB allows
`LET x,y BE x=2 & y=x*x IN ... END`
* ProB allows WHILE loops and sequential composition in abstract
machines
* ProB now allows the IF-THEN-ELSE for expressions with parentheses
around it: `(IF x<0 THEN -x ELSE x END)`
[[limitations-with-atelierb]]
=== Limitations
* Parsing: ProB will require parentheses around the comma, the
relational composition, and parallel product operators. For example, you
cannot write `r2=rel;rel`. You need to write `r2=(rel;rel)`. This allows
ProB to distinguish the relational composition from the sequential
composition (or other uses of the semicolon).
* <<well-definedness-checking,Well-definedness>>: ProB will try to
check if your predicates are well-defined during animation or model
checking. For this ProB assumes (similar to Rodin) a stricter
left-to-right definition of well-definedness than Atelier B.
* Closure: The transitive and reflexive closure operator of classical B
is not supported as defined in the B-Book by Abrial. AtelierB also does
not support the operator as defined in the B-Book (as this version
cannot be applied in practice). For the reflexive component of closure,
ProB will compute the elements in the domain and range of the relation.
Note however, that the transitive closure operator `closure1` is fully
supported, and hence one can translate an expression `closure(e)`, where
e is a binary relation over some domain d, into the expression
`closure1(e) \/ id(d`).
* Unsupported Operators:
** Trees and binary trees: most but not all tree operators (mirror,
infix) are supported yet (the `STRING` type is now supported);
** `VALUES`: This clause of the `IMPLEMENTATION` machines is not yet
supported;
* There are also some general limitations wrt refinements. See
<<current-limitations,Current
Limitations section>> for more details.
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc deleted 100644 → 0
+ 0
− 121
View file @ 7c0989c2
[[using-prob-with-kodkod]]
= Using ProB with KODKOD
As of version 1.3.5 ProB can make use of
http://alloy.mit.edu/kodkod/[Kodkod] as an alternate way of solving
constraints. Kodkod provides a relational interface to SAT solvers and
is the heart of the http://alloy.mit.edu/alloy/[Alloy] tool.
[[how-to-enable-kodkod]]
== How to enable Kodkod
For the command-line version you need to call prob as follows:
`probcli -p KODKOD TRUE`
Note: to experiment with Kodkod you may want to try out the command:
`probcli -p KODKOD TRUE -repl`
If in addition you want see a graphical representation of the solutions
found you can use the following command and open the `out.dot` file
using dotty or GraphViz:
`probcli -p KODKOD TRUE -repl -evaldot ~/out.dot`
For the ProB Tcl/Tk Version you should select the menu command "Enable
Kodkod for Properties" in the _Preferences_ menu.
[[what-can-be-translated-kodkod]]
== What can be translated
* Types:
** Basic Types: Deferred Sets, enumerated sets, integers, booleans
** Sets of basic types
** Relations between basic types
** Higher-order types (sets of sets) are not supported
* Operators:
** Predicates: &, or, \=>, \<\=>, not, !, #, =, /=
** Booleans: TRUE, FALSE, BOOL, bool(...)
** Sets: \{..,...} \{x|P}, POW, card, Cartesian product, \/, /\, -, :,
/:, /<:, <<: /<<:
** Numbers: n..m, >, <, >=, <=, +, -, *, SIGMA(x).(P|x)
** Relations: \<\->, |\->, dom, ran, id, <|, <<|, |>, |>>, ~, [...], <+,
prj1, prj2, closure1
** x : S+\->T, x:S-\->T, ..., lambda
** currently no operations on sequences are supported
* Some limitations:
** If integers are used, a predicate can only be translated if a static
analysis can estimate the interval of its possible values.
** Generally only complete predicates are translated or nothing at all,
unless you set the `KODKOD_ONLY_FULL` preference to FALSE.
[[when-is-the-kokod-translation-used]]
== When is the Kokod translation used
Once enabled, the Kodkod translation will be used in the following
circumstances:
* for solving PROPERTIES
* constraint-based assertion checking (`-cbc_assertions` command for
`probcli` or the "Check Assertions on Constants" command in the menu
_Verify_ -> Constraint-Based Checking)
* constraint-based deadlock checking
* in the <<eval-console,Eval Console>> in the ProB Tcl/Tk version
* for the REPL in probcli (`probcli -p KODKOD TRUE -repl`)
[[sat-solver]]
== SAT solver
By default Kodkod in ProB uses the bundled SAT4J solver. You can switch
to using minisat by putting a current version of `libminisat.jnilib`
into ProB's `lib` directory.
Similarly, as of ProB 1.6.1-beta5 you can also use the Solver
http://fmv.jku.at/lingeling/[lingeling] or
http://www.labri.fr/perso/lsimon/glucose/[glucose] by dropping
`liblingeling.dylib` or `libglucose.dylib` into ProB's lib folder (for
Mac OS X; for Linux the extension will be different). You can control
the solver being used using the `KODKOD_SAT_SOLVER` preference (which
has four possible values: sat4j, minisat, lingeling, glucose).
These files can be downloaded from the
http://alloy.mit.edu/kodkod/download.html[Kodkod download site].
[[more-preferences]]
== More Preferences
If you set `KODKOD_ONLY_FULL` to `FALSE`, then the Kodkod translation
can be applied to part of a predicate. In other words, the predicate
(such as the PROPERTIES) are partitioned into two parts: one that can be
understood by Kodkod and the rest which will be dealt with by ProB's
solver.
You can also enable symmetry by using the preference `KODKOD_SYMMETRY`.
By default, ProB will set this value to 0, i.e., symmetry is off. This
means that Kodkod can also be used within set comprehensions. By setting
the preference to a value higher than 0 you will enable symmetry within
Kodkod, which may mean that not all solutions will be returned. Setting
the value too high may be counter productive; Kodkod's recommended
default is 20.
Finally, you can control the number of solutions that Kodkod computes in
one go using the preference `KODKOD_MAX_NR_SOLS`. E.g., if you are
interested in only one solution and `KODKOD_ONLY_FULL` is `TRUE`, then
you should set this value to 1.
[[more-details-on-kodkod]]
== More details
* https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[Plagge,
Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. In Proceedings
FM'2012, Dimitra Giannakopoulou and Dominique Méry, LNCS 7436, Springer,
372--386, 2012. (pdf)]
You can also have a look at these Wiki pages:
* <<proving-theorems-in-the-prob-repl,Proving_Theorems_in_the_ProB_REPL>>
* <<argumentation-theory,Argumentation Theory Example>>
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc deleted 100644 → 0
+ 0
− 118
View file @ 7c0989c2
[[using-prob-with-z3]]
= Using ProB with Z3
The current nightly versions of ProB can make use of
https://github.com/Z3Prover/z3[Z3] as an alternate way of solving
constraints.
[[how-to-use-z3-within-prob]]
== How to use Z3 within ProB
One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the
`-repl` command line option. Any predicate preceded with `:z3` will be
solved by Z3. The full integration of Z3 and ProB’s kernel can be
enabled by setting the corresponding preference by passing
`-p SMT SUPPORTED INTERPRETER TRUE`
on the command line.
[[how-to-install-z3-for-prob]]
== How to install Z3 for ProB
First of all, download a nightly build of ProB from the
<<download,Downloads>> page. To connect Z3 to ProB you also need the
proper extension. For Linux and Mac OS, the extension is build by on our
infrastructure and ships with the regular ProB download. For Windows,
you can download it from the following URLs:
* https://www3.hhu.de/stups/downloads/z3interface/windows32/z3interface.dll[32bit]
* https://www3.hhu.de/stups/downloads/z3interface/windows64/z3interface.dll[64bit]
and place it in the "lib" folder of the ProB nightly build.
In addition to ProB, you need to install Z3 by downloading it from
https://github.com/Z3Prover[Z3's GitHub page]. Currently, ProB is linked
against the stable release 4.4.1 of Z3. Inside the zip file you will
find a folder called "bin" with the z3 binary and the belonging
libraries inside.
These libraries have to be made available to ProB. On Linux or Mac, this
can either be done by placing them in an appropriate folder (like
/usr/lib or /usr/local/lib) or by setting an environmental variable
(like LD_LIBRARY_PATH on Linux or DYLD_LIBRARY_PATH on Mac). On Windows,
you can place z3.dll in the main folder of the ProB distribution, i. e.,
on the same level as the lib directory, not inside it. If the libraries
can not be loaded, ProB will answer with "solver_not_available" when
Z3 is queried.
[[what-can-be-translated-z3]]
== What can be translated
Currently, the Z3 translation is unable to cope with the following
constructs:
* Strings
* Generalised union, generalised intersection
* Generalised concatenation
* Permutation
* Iteration and Closure
* Projection
When using Z3 alone, the solver will report
"unsupported_type_or_expression" if it can not handle parts of a
constraint.
When used together with ProB, everything Z3 can not be coped with will
be handled by ProB alone automatically.
[[examples-z3]]
== Examples
Using the repl, one can try out different examples.
First an example which can be solved by Z3 and not by ProB:
....
>>> X0)
### Warning: enumerating X : INTEGER : inf:sup ---> -1:3
Existentially Quantified Predicate over X,Y is UNKNOWN
[FALSE with ** ENUMERATION WARNING **]
....
Using the Z3 translation it can be solved:
....
>>> :z3 X>> (2|->4):{y|#x.(y=(x|->x+2))}
PREDICATE is TRUE
....
This one cannot be solved by Z3:
....
>>> :z3 (2|->4):{y|#x.(y=(x|->x+2))}
PREDICATE is UNKNOWN: solver_answered_unknown
....
Here an example that shows that Z3 can be used to solve constraints and
obtain solutions for the open variables:
....
>>> :z3 {x} /\ {y} /= {} & x:1000000..20000000 & y>=0 & y<2000000
PREDICATE is TRUE
Solution:
x = 1000000
y = 1000000
....
[[more-details-z3]]
=== More details
A paper describing the integration of ProB and Z3 has been submitted to
iFM 2016. You can download the
* https://www3.hhu.de/stups/downloads/z3interface/rawdata[raw data] from
our benchmarks including the R scripts to generate the
* https://www3.hhu.de/stups/downloads/z3interface/output[resulting
graphs].
src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 7c0989c2
:leveloffset: -1
src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 7c0989c2
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment