Skip to content
Snippets Groups Projects
Commit 36450cb4 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

update presentations

parent a00765bc
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/presentations/BvsLP.ipynb
+ 102
− 1
View file @ 36450cb4
%% Cell type:markdown id: tags:
# B compared to Logic Programming
Important differences:
* B is based on classical predicate logic with classical negation
* B is based on arithmetic and set theory, LP on (rational) trees aka uninterpreted functions
* B is strongly typed, but allows higher-order data types
* B allows arbitrary nesting of quantifiers and negation
As B is based on classical negation and classical predicate logic (without induction), how can it deal with natural numbers, transitive closure, ...?
* Integer arithmetic is built-in, providing induction through the back door. One can construct bijections between user-defined sets and the integers or natural numbers.
* Transitive closure is built-in, providing another way to introduce induction or recursion.
%% Cell type:markdown id: tags:
## Append in B
The logic program
```
append([],L,L) <-
append([H|X],Y,[H|Z]) <- append(X,Y,Z)
```
can be encoded in various ways in B.
### Built-in Sequence Operator
B has built-in sequences, which are special cases of functions, which are special cases of relations, which are sets of pairs.
The sequence [4,5,6] is represented by the relation {(1,4),(2,5),(3,6)}:
%% Cell type:code id: tags:
``` prob
[4,5,6] = {(1,4),(2,5),(3,6)}
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph [4,5,6]
```
%% Output
<Dot visualization: expr_as_graph [[4,5,6]]>
%% Cell type:markdown id: tags:
The built-in concatenation operator can be used to append sequences:
%% Cell type:code id: tags:
``` prob
[1,2,3] ^ [4,5,6]
```
%% Output
$[1,2,3,4,5,6]$
[1,2,3,4,5,6]
%% Cell type:code id: tags:
``` prob
[1,2,3] ^ x = [1,2,3,4,5,6]
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = [4,5,6]$
TRUE
Solution:
x = [4,5,6]
%% Cell type:code id: tags:
``` prob
:table {x,y | x^y = [1,2,3]}
```
%% Output
|x|y|
|---|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$[1,2,3]$|
|$\{(1\mapsto 1)\}$|$\{(1\mapsto 2),(2\mapsto 3)\}$|
|$\{(1\mapsto 1),(2\mapsto 2)\}$|$\{(1\mapsto 3)\}$|
|$[1,2,3]$|$\emptyset$|
x y
{} [1,2,3]
{(1|->1)} {(1|->2),(2|->3)}
{(1|->1),(2|->2)} {(1|->3)}
[1,2,3] {}
%% Cell type:markdown id: tags:
One can also write the append as a B function. Note that B is strongly typed (and user defined functions cannot yet be polymorphic), hence we have to provide the type for the arguments to the function.
%% Cell type:code id: tags:
``` prob
app = %(x,y).(x:seq(INTEGER) & y:seq(INTEGER) | x \/ {i,e | (i-size(x),e) : y}) & app([1,2],[3,4]) = res
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}}\mathit{TRUE}$
**Solution:**
* $\mathit{app} = \lambda(\mathit{x},\mathit{y})\qdot(\mathit{x} \in \mathit{seq}(\mathit{INTEGER}) \land \mathit{y} \in \mathit{seq}(\mathit{INTEGER})\mid \mathit{x} \bunion \{\mathit{i},\mathit{e}\mid \mathit{i} - \mathit{size}(\mathit{x}) \mapsto \mathit{e} \in \mathit{y}\})$
* $\mathit{res} = [1,2,3,4]$
TRUE
Solution:
app = λ(x,y)·(x ∈ seq(INTEGER) ∧ y ∈ seq(INTEGER)∣x ∪ {i,e∣i − size(x) ↦ e ∈ y})
res = [1,2,3,4]
%% Cell type:markdown id: tags:
## Recursion using transitive closure
Given an operator TP from sets to sets, one can compute the transitive closure
using ```closure(TP)```. Together with the relational image operator ```.[.]``` one can
compute the least fixed point containing a starting set S
(given the well known conditions) using ```closure(TP)[S]```.
To simplify the presentation, we encode a variation of append, working on sets:
```
set_app({},L,L) <-
set_app({H}\/X],Y,{H}\/Z) <- set_app(X,Y,Z)
```
%% Cell type:code id: tags:
``` prob
TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)
&
Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts
&
tp = /*@symbolic*/ {S,TPS|S:HB & #(x,y,z,h).( (x,y,z) = S & h:TYPE & TPS= (x\/{h},y,z\/{h}))} // The TP Operator
&
LHM = closure(tp)[Facts] // the least Herbrand model
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}}\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\mathit{TRUE}$
**Solution:**
* $\mathit{LHM} = \{((\emptyset\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\emptyset\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\}),((\{\mathit{FALSE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\{\mathit{FALSE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{FALSE},\mathit{TRUE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{FALSE},\mathit{TRUE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{TRUE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{TRUE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\})\}$
* $\mathit{HB} = ((\pow(\{\mathit{FALSE},\mathit{TRUE}\}) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) * \pow(\{\mathit{FALSE},\mathit{TRUE}\}))$
* $\mathit{tp} = \{\mathit{S},\mathit{TPS}\mid \mathit{S} \in ((\pow(\{\mathit{FALSE},\mathit{TRUE}\}) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) \land \exists(\mathit{x},\mathit{y},\mathit{z},\mathit{h})\qdot(\mathit{x} \mapsto \mathit{y} \mapsto \mathit{z} = \mathit{S} \land \mathit{h} \in \{\mathit{FALSE},\mathit{TRUE}\} \land \mathit{TPS} = (\mathit{x} \bunion \{\mathit{h}\}) \mapsto \mathit{y} \mapsto (\mathit{z} \bunion \{\mathit{h}\}))\}$
* $\mathit{TYPE} = \{\mathit{FALSE},\mathit{TRUE}\}$
* $\mathit{Facts} = \{((\emptyset\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\emptyset\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\})\}$
TRUE
Solution:
LHM = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE}),(({FALSE}↦{FALSE})↦{FALSE}),(({FALSE}↦{TRUE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{FALSE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{TRUE})↦{FALSE,TRUE}),(({TRUE}↦{FALSE})↦{FALSE,TRUE}),(({TRUE}↦{TRUE})↦{TRUE})}
HB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))
tp = {S,TPS∣S ∈ ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE})) ∧ ∃(x,y,z,h)·(x ↦ y ↦ z = S ∧ h ∈ {FALSE,TRUE} ∧ TPS = (x ∪ {h}) ↦ y ↦ (z ∪ {h}))}
TYPE = {FALSE,TRUE}
Facts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}
%% Cell type:markdown id: tags:
### Axiomatic Encoding using logical implication
%% Cell type:code id: tags:
``` prob
TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)
&
Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts
&
Facts <: Model
&
!(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\/{h},y,z\/{h}):Model))
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\mathit{TRUE}$
**Solution:**
* $\mathit{Model} = \{((\emptyset\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\}),((\emptyset\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\{\mathit{FALSE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{TRUE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\}),((\{\mathit{FALSE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\{\mathit{TRUE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{FALSE},\mathit{TRUE}\}\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\}),((\{\mathit{FALSE},\mathit{TRUE}\}\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE},\mathit{TRUE}\})\}$
* $\mathit{HB} = ((\pow(\{\mathit{FALSE},\mathit{TRUE}\}) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) * \pow(\{\mathit{FALSE},\mathit{TRUE}\}))$
* $\mathit{TYPE} = \{\mathit{FALSE},\mathit{TRUE}\}$
* $\mathit{Facts} = \{((\emptyset\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\emptyset\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\})\}$
TRUE
Solution:
Model = {((∅↦{TRUE})↦{TRUE}),((∅↦{FALSE})↦{FALSE}),(({FALSE}↦{TRUE})↦{FALSE,TRUE}),(({TRUE}↦{TRUE})↦{TRUE}),(({FALSE}↦{FALSE})↦{FALSE}),(({TRUE}↦{FALSE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{TRUE})↦{FALSE,TRUE}),(({FALSE,TRUE}↦{FALSE})↦{FALSE,TRUE})}
HB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))
TYPE = {FALSE,TRUE}
Facts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}
%% Cell type:code id: tags:
``` prob
TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)
&
Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts
&
Facts <: Model
&
!(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\/{h},y,z\/{h}):Model))
&
Model = HB
```
%% Output
$\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\newcommand{\pow}{\mathop{\mathbb P\hbox{}}\nolimits}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\mathit{TRUE}$
**Solution:**
* $\mathit{Model} = ((\pow(\{\mathit{FALSE},\mathit{TRUE}\}) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) * \pow(\{\mathit{FALSE},\mathit{TRUE}\}))$
* $\mathit{HB} = ((\pow(\{\mathit{FALSE},\mathit{TRUE}\}) * \pow(\{\mathit{FALSE},\mathit{TRUE}\})) * \pow(\{\mathit{FALSE},\mathit{TRUE}\}))$
* $\mathit{TYPE} = \{\mathit{FALSE},\mathit{TRUE}\}$
* $\mathit{Facts} = \{((\emptyset\mapsto\{\mathit{FALSE}\})\mapsto\{\mathit{FALSE}\}),((\emptyset\mapsto\{\mathit{TRUE}\})\mapsto\{\mathit{TRUE}\})\}$
TRUE
Solution:
Model = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))
HB = ((ℙ({FALSE,TRUE}) ∗ ℙ({FALSE,TRUE})) ∗ ℙ({FALSE,TRUE}))
TYPE = {FALSE,TRUE}
Facts = {((∅↦{FALSE})↦{FALSE}),((∅↦{TRUE})↦{TRUE})}
%% Cell type:markdown id: tags:
### Additional Material
%% Cell type:code id: tags:
``` prob
TYPE = BOOL & HB = POW(TYPE)*POW(TYPE)*POW(TYPE)
&
Facts = UNION(L).(L:TYPE|{({L}-{L},{L},{L})}) // The set of all Facts
&
AllModels = {Model | Facts <: Model &
!(x,y,z).( (x,y,z):Model => !h.(h:TYPE => (x\/{h},y,z\/{h}):Model))}
```
%% Output
$\mathit{time\_out}$
time_out
%% Cell type:code id: tags:
``` prob
```
......
notebooks/presentations/LPOP18.ipynb
+ 91
− 35
View file @ 36450cb4
%% Cell type:markdown id: tags:
# Solving (Set) Constraints in B and Event-B #
Michael Leuschel,
David Geleßus (Jupyter Interface)
## A quick Introduction to B ##
%% Cell type:markdown id: tags:
### Basic Datavalues in B ###
%% Cell type:markdown id: tags:
B provides the booleans, strings and integers as built-in datatypes. (Strings are not available in Event-B.)
%% Cell type:code id: tags:
``` prob
BOOL
```
%% Output
$\{\mathit{FALSE},\mathit{TRUE}\}$
{FALSE,TRUE}
%% Cell type:code id: tags:
``` prob
"this is a string"
```
%% Output
$\text{"this is a string"}$
"this is a string"
%% Cell type:code id: tags:
``` prob
1024
```
%% Output
$1024$
1024
%% Cell type:markdown id: tags:
Users can define their own datatype in a B machine.
One distinguishes between explicitly specified enumerated sets and deferred sets.
%% Cell type:code id: tags:
``` prob
::load
MACHINE MyBasicSets
SETS Trains = {thomas, gordon}; Points
END
```
%% Output
Loaded machine: MyBasicSets
%% Cell type:markdown id: tags:
For animation and constraint solving purposes, ProB will instantiate deferred sets to some finite set (the size of which can be controlled and is partially inferred).
%% Cell type:code id: tags:
``` prob
Points
```
%% Output
$\{\mathit{Points1},\mathit{Points2}\}$
{Points1,Points2}
%% Cell type:markdown id: tags:
### Pairs ###
B also has pairs of values, which can be written in two ways:
%% Cell type:code id: tags:
``` prob
(thomas,10)
```
%% Output
$(thomas\mapsto10)$
(thomas↦10)
%% Cell type:code id: tags:
``` prob
thomas |-> 10
```
%% Output
$(thomas\mapsto10)$
(thomas↦10)
%% Cell type:markdown id: tags:
Tuples simply correspond to nested pairs:
%% Cell type:code id: tags:
``` prob
(thomas |-> gordon |-> 20)
```
%% Output
$((\mathit{thomas}\mapsto \mathit{gordon})\mapsto 20)$
((thomas↦gordon)↦20)
%% Cell type:markdown id: tags:
Classical B also provides records:
%% Cell type:code id: tags:
``` prob
:prettyprint r=rec(train:thomas,length:20,position:10302)
```
%% Output
$\mathit{r} = \mathit{rec}(length:20,position:10302,train:\mathit{thomas})$
r = rec(length:20,position:10302,train:thomas)
%% Cell type:markdown id: tags:
### Sets ###
Sets in B can be specified in multiple ways.
For example, using explicit enumeration:
%% Cell type:code id: tags:
``` prob
{1,3,2,3}
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:markdown id: tags:
or via a predicate by using a set comprehension:
%% Cell type:code id: tags:
``` prob
{x|x>0 & x<4}
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:markdown id: tags:
For integers there are a variety of other sets, such as intervals:
%% Cell type:code id: tags:
``` prob
1..3
```
%% Output
$\{1,2,3\}$
{1,2,3}
%% Cell type:markdown id: tags:
or the set of implementable integers INT = MININT..MAXINT or the set of implementable natural numbers NAT = 0..MAXINT.
%% Cell type:markdown id: tags:
Sets can be higher-order and contain other sets:
%% Cell type:code id: tags:
``` prob
{ 1..3, {1,2,3,2}, 0..1, {x|x>0 & x<4} }
```
%% Output
$\{\{0,1\},\{1,2,3\}\}$
{{0,1},{1,2,3}}
%% Cell type:markdown id: tags:
Relations are modelled as sets of pairs:
%% Cell type:code id: tags:
``` prob
{ thomas|->gordon, gordon|->gordon, thomas|->thomas}
```
%% Output
$\{(\mathit{thomas}\mapsto \mathit{thomas}),(\mathit{thomas}\mapsto \mathit{gordon}),(\mathit{gordon}\mapsto \mathit{gordon})\}$
{(thomas↦thomas),(thomas↦gordon),(gordon↦gordon)}
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("rel",{ thomas|->gordon, gordon|->gordon, thomas|->thomas})
```
%% Output
<Dot visualization: expr_as_graph [("rel",{(thomas,gordon),(gordon,gordon),(thomas,thomas)})]>
%% Cell type:markdown id: tags:
Note: a pair is an element of a Cartesian product, and a relation is just a subset of a Cartesian product.
The above relation is a subset of ```Trains * Trains```.
%% Cell type:markdown id: tags:
Functions are relations which map every domain element to at most one value:
%% Cell type:code id: tags:
``` prob
{ thomas|->1, gordon|->2}
```
%% Output
$\{(thomas\mapsto1),(gordon\mapsto2)\}$
{(thomas↦1),(gordon↦2)}
%% Cell type:markdown id: tags:
## Expressions vs Predicates vs Substitutions ##
%% Cell type:markdown id: tags:
### Expressions ###
Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as:
%% Cell type:code id: tags:
``` prob
2**1000
```
%% Output
$10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376$
10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376
%% Cell type:markdown id: tags:
B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.
For example set union and set difference:
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
$\{1,7,8,9,10\}$
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
(1..3 ∪ 5..10) \ (2..6)
```
%% Output
$\{1,7,8,9,10\}$
{1,7,8,9,10}
%% Cell type:markdown id: tags:
The range of a relation or function:
%% Cell type:code id: tags:
``` prob
dom({(thomas↦1),(gordon↦2)})
```
%% Output
$\{thomas,gordon\}$
{thomas,gordon}
%% Cell type:markdown id: tags:
Function application:
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Output
$1$
1
%% Cell type:markdown id: tags:
Relational inverse (.~) and relational image .[.] :
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Output
$\{\mathit{gordon}\}$
{gordon}
%% Cell type:markdown id: tags:
## Predicates
ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false).
%% Cell type:code id: tags:
``` prob
2>3
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
$TRUE$
TRUE
%% Cell type:markdown id: tags:
Within predicates you can use **open** variables, which are implicitly existentially quantified.
ProB will display the solution for the open variables, if possible.
%% Cell type:code id: tags:
``` prob
x*x=100
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = -10$
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation.
Note that by this we turn a predicate into an expression.
%% Cell type:code id: tags:
``` prob
{x|x*x=100}
```
%% Output
$\{-10,10\}$
{−10,10}
%% Cell type:markdown id: tags:
### Substitutions ###
B also has a rich syntax for substitutions, aka statements.
For example ```x := x+1``` increments the value of x by 1.
We will not talk about substitutions in the rest of this presentation.
The major differences between classical B and Event-B lie in the area of substitutions, machine composition and refinement.
%% Cell type:markdown id: tags:
## Definition of Constraint Solving ##
Constraint solving is determine whether a predicate with open/existentially quantified variables is satisfiable and providing values for the open variables in case it is.
We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.
The following is an unsatisfiable predicate:
%% Cell type:code id: tags:
``` prob
:prettyprint #x.(x:NATURAL & x*x=1000)
```
%% Output
$\exists \mathit{x}\cdot (\mathit{x} \in \mathbb N \wedge \mathit{x} * \mathit{x} = 1000)$
∃x·(x ∈ ℕ ∧ x * x = 1000)
%% Cell type:markdown id: tags:
The difference to **proof** is that in constraint solving one has to produce a solution (aka a model). The difference to **execution** is that not all variables are known.
%% Cell type:markdown id: tags:
## Constraint Solving Applications ##
Constraint solving has many applications in formal methods in general and B in particular.
%% Cell type:markdown id: tags:
#### Animation ####
It is required to animate implicit specifications.
Take for example an event
```
train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &
train_position(t1) < train_position(t2) &
x:1..(train_position(t2)-train_position(t1)-1) then
train_position(t1) := train_position(t1)+x end
```
To determine whether the event is enabled, and to obtain values for the parameters of the event in a given state of the model, we have to solve the following constraint:
%% Cell type:code id: tags:
``` prob
train_position = {thomas|->100, gordon|->2020} &
t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &
x:1..(train_position(t2)-train_position(t1)-1)
```
%% Output
$TRUE$
**Solution:**
* $x = 1$
* $train_position = \{(thomas\mapsto100),(gordon\mapsto2020)\}$
* $t1 = thomas$
* $t2 = gordon$
TRUE
Solution:
x = 1
train_position = {(thomas↦100),(gordon↦2020)}
t1 = thomas
t2 = gordon
%% Cell type:code id: tags:
``` prob
train_position = {thomas|->2019, gordon|->2020} &
t1:dom(train_position) & t2:dom(train_position) & train_position(t1) < train_position(t2) &
x:1..(train_position(t2)-train_position(t1)-1)
```
%% Output
$FALSE$
FALSE
%% Cell type:markdown id: tags:
Many other applications exist: generating **testcases**, finding counter examples using **bounded model checking** or other algorithms like IC3.
Other applications are analysing **proof obligations**.
Take the proof obligation for an event theorem t1 $/=$ t2:
```
train_position:Trains-->1..10000 & train_position(t1) < train_position(t2) |- t1 /= t2
```
We can find counter examples to it by negating the proof goal:
%% Cell type:code id: tags:
``` prob
train_position:Trains-->1..10000 &
train_position(t1) < train_position(t2) &
not( t1 /= t2 )
```
%% Output
$FALSE$
FALSE
%% Cell type:markdown id: tags:
As no counter example has been found, we can in this case establish the goal to be proven.
%% Cell type:markdown id: tags:
### Modelling and Solving Problems in B ###
Obviously, we can also use constraint solving to solve puzzles or real-life problems.
#### Send More Money Puzzle ####
We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:
%% Cell type:code id: tags:
``` prob
:prettyprint {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y
```
%% Output
$\{\mathit{S},\mathit{E},\mathit{N},\mathit{D},\mathit{M},\mathit{O},\mathit{R},\mathit{Y}\} \subseteq 0 .. 9 \wedge \mathit{S} > 0 \wedge \mathit{M} > 0 \wedge \mathit{card}(\{\mathit{S},\mathit{E},\mathit{N},\mathit{D},\mathit{M},\mathit{O},\mathit{R},\mathit{Y}\}) = 8 \wedge \mathit{S} * 1000 + \mathit{E} * 100 + \mathit{N} * 10 + \mathit{D} + \mathit{M} * 1000 + \mathit{O} * 100 + \mathit{R} * 10 + \mathit{E} = \mathit{M} * 10000 + \mathit{O} * 1000 + \mathit{N} * 100 + \mathit{E} * 10 + \mathit{Y}$
{S,E,N,D,M,O,R,Y} ⊆ 0 ‥ 9 ∧ S > 0 ∧ M > 0 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S * 1000 + E * 100 + N * 10 + D + M * 1000 + O * 100 + R * 10 + E = M * 10000 + O * 1000 + N * 100 + E * 10 + Y
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{R} = 8$
* $\mathit{S} = 9$
* $\mathit{D} = 7$
* $\mathit{E} = 5$
* $\mathit{Y} = 2$
* $\mathit{M} = 1$
* $\mathit{N} = 6$
* $\mathit{O} = 0$
TRUE
Solution:
R = 8
S = 9
D = 7
E = 5
Y = 2
M = 1
N = 6
O = 0
%% Cell type:markdown id: tags:
We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single solution:
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y }
```
%% Output
$\{(((((((9\mapsto 5)\mapsto 6)\mapsto 7)\mapsto 1)\mapsto 0)\mapsto 8)\mapsto 2)\}$
{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}
%% Cell type:code id: tags:
``` prob
:table {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y }
```
%% Output
|S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y
9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags:
#### KISS PASSION Puzzle####
A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem.
%% Cell type:code id: tags:
``` prob
{K,P} <: 1..9 &
{I,S,A,O,N} <: 0..9 &
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S)
= 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &
card({K, I, S, P, A, O, N}) = 7
```
%% Output
$TRUE$
**Solution:**
* $P = 4$
* $A = 1$
* $S = 3$
* $I = 0$
* $K = 2$
* $N = 9$
* $O = 8$
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:markdown id: tags:
Finally, a simple puzzle involving sets is to find a subset of numbers from 1..5 whose sum is 14:
%% Cell type:code id: tags:
``` prob
x <: 1..5 & SIGMA(y).(y:x|y)=14
```
%% Output
$TRUE$
**Solution:**
* $x = \{2,3,4,5\}$
TRUE
Solution:
x = {2,3,4,5}
%% Cell type:markdown id: tags:
## How to solve (set) constraints in B ##
We will now examine how one can perform constraint solving for B.
%% Cell type:markdown id: tags:
### Booleans ###
If we have only booleans, constraint solving is equivalent to SAT solving.
Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.
(We do not translate to CNF also because of well-definedness issues.)
%% Cell type:markdown id: tags:
### Integers ###
Let us take the integer constraint ```x*x=100``` which we saw earlier.
This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.
So, let us first look at some simpler constraints, where the domains of the variables are all bounded.
%% Cell type:markdown id: tags:
Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.
As you can see there are three solutions for this constraint:
%% Cell type:code id: tags:
``` prob
{X,Y|X:0..3 & Y:0..3 & X+Y=2}
```
%% Output
$\{(0\mapsto2),(1\mapsto1),(2\mapsto0)\}$
{(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
We will now study how such constraints can be solved.
%% Cell type:markdown id: tags:
#### Solving constraints by translating to SAT ####
Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.
The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.
We can translate the addition to a propositional logic formula:
Bit1 | Bit0
-----|-----
X1 | X0
+ Y1 | Y0
|
Z1 | Z0
Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:
%% Cell type:code id: tags:
``` prob
card({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) &
((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) &
(CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) &
(CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &
Z0=FALSE & Z1=TRUE})
```
%% Output
$4$
4
%% Cell type:markdown id: tags:
As you can see, we have found four solutions and not three! One solution is 3+3=2.
This is a typical issue when translating arithmetic to binary numbers: we have to prevent overflows, which we do below:
%% Cell type:code id: tags:
``` prob
:table ({X0,X1,Y0,Y1,Z0,Z1,CARRY0 | ((X0=TRUE <=> Y0=TRUE) <=> Z0=FALSE) &
((X0=TRUE & Y0=TRUE) <=> CARRY0=TRUE) &
(CARRY0=FALSE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=FALSE)) &
(CARRY0=TRUE => ((X1=TRUE <=> Y1=TRUE) <=> Z1=TRUE)) &
(CARRY0=TRUE => (X1=FALSE & Y1=FALSE)) & // no overflow
(CARRY0=FALSE => (X1=FALSE or Y1=FALSE)) & // no overflow
Z0=FALSE & Z1=TRUE})
```
%% Output
|Nr|X0|X1|Y0|Y1|Z0|Z1|CARRY0|
|---|---|---|---|---|---|---|---|
|1|FALSE|FALSE|FALSE|TRUE|FALSE|TRUE|FALSE|
|2|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|FALSE|
|3|TRUE|FALSE|TRUE|FALSE|FALSE|TRUE|TRUE|
Nr X0 X1 Y0 Y1 Z0 Z1 CARRY0
1 FALSE FALSE FALSE TRUE FALSE TRUE FALSE
2 FALSE TRUE FALSE FALSE FALSE TRUE FALSE
3 TRUE FALSE TRUE FALSE FALSE TRUE TRUE
%% Cell type:markdown id: tags:
In ProB, we can use **Kodkod** backend to achieve such a translation to SAT.
- Kodkod (https://github.com/emina/kodkod) is the API to the **Alloy** (http://alloytools.org) constraint analyzer and takes relational logic predicates and translates them to SAT.
- The SAT problem can be solved by any SAT solver (Sat4J, minisat, glucose,...).
- ProB translates parts of B to the Kodkod API and translates the results back to B values.
- Prior to the translation, ProB performs an interval analysis to determine possible ranges for the integer decision variables.
The details were presented at FM'2012 (Plagge, L.).
![ProBKodkod](./img/ProB_Kodkod_Architecture.png)
%% Cell type:code id: tags:
``` prob
:solve kodkod x:0..2 & y:0..2 & x+y=2
```
%% Output
$TRUE$
**Solution:**
* $x = 2$
* $y = 0$
TRUE
Solution:
x = 2
y = 0
%% Cell type:markdown id: tags:
We can find all solutions and check that we find exactly the three expected solutions:
%% Cell type:code id: tags:
``` prob
:solve kodkod {x,y|x:0..2 & y:0..2 & x+y=2}=res
```
%% Output
$TRUE$
**Solution:**
* $res = \{(0\mapsto2),(1\mapsto1),(2\mapsto0)\}$
TRUE
Solution:
res = {(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
#### Translation to SMTLib ####
At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.
Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.
![ProBZ3](./img/inputoutputflow.pdf)
%% Cell type:markdown id: tags:
Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:
- mk_var(integer,x) $\rightarrow$ 2
- mk_var(integer,y) $\rightarrow$ 3
- mk_int_const(0) $\rightarrow$ 4
- mk_op(greater_equal,2,4) $\rightarrow$ 5
- mk_int_const(2) $\rightarrow$ 6
- mk_op(greater_equal,6,2) $\rightarrow$ 7
- mk_int_const(0) $\rightarrow$ 8
- mk_op(greater_equal,3,8) $\rightarrow$ 9
- mk_int_const(2) $\rightarrow$ 10
- mk_op(greater_equal,10,3) $\rightarrow$ 11
- mk_op(add,2,3) $\rightarrow$ 12
- mk_int_const(2) $\rightarrow$ 13
- mk_op(equal,12,13) $\rightarrow$ 14
- mk_op_arglist(conjunct,[5,7,9,11,14]) $\rightarrow$ 15
%% Cell type:code id: tags:
``` prob
:solve z3 x:0..2 & y:0..2 & x+y=2
```
%% Output
$TRUE$
**Solution:**
* $x = 0$
* $y = 2$
TRUE
Solution:
x = 0
y = 2
%% Cell type:markdown id: tags:
#### ProB's CLP(FD) Solver ####
ProB's default solver makes use of constraint logic programming.
For arithmetic, it builts on top of CLP(FD), the finite domain library of SICStus Prolog.
In CLP(FD):
- every integer variable is associated with a domain of possible values, typically an interval
- when adding a new constraints, the domains of the involved variables are updated, or more precisely narrowed down.
- at some point we need to chose variables for enumeration; typically ProB chooses the value with the smallest domain.
Let us use a slightly adapted constraint ```x:0..9 & y:0..9 & x+y=2``` to illustrate how constraint processing works:
- x:0..9 $\leadsto$ x:0..9, y:$-\infty$..$\infty$
- y:0..9 $\leadsto$ x:0..9, y:0..9
- x+y=2 $\leadsto$ x:0..2, y:0..2
- Enumerate (label) variable x
- x=0 $\leadsto$ x:0..0, y:2..2
- x=1 $\leadsto$ x:1..1, y:1..1
- x=2 $\leadsto$ x:2..2, y:0..0
%% Cell type:markdown id: tags:
Let us now examine the three approaches for the KISS-PASSION puzzle:
%% Cell type:code id: tags:
``` prob
:time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 &
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) =
1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7
```
%% Output
Execution time: 0.213287097 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{P} = 4$
* $\mathit{A} = 1$
* $\mathit{S} = 3$
* $\mathit{I} = 0$
* $\mathit{K} = 2$
* $\mathit{N} = 9$
* $\mathit{O} = 8$
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:code id: tags:
``` prob
:time :solve z3 {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve kodkod {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7
```
%% Output
Error from ProB: ProB reported Errors
Warning: Kodkod SAT Solver Timeout for Problem Id: 0
%% Cell type:markdown id: tags:
Result for KISS*KISS=PASSION puzzle:
Solver | Runtime
-------|-------
ProB Default | 0.01 sec
Kodkod Backend | 1 sec
Z3 Backend | ? > 100 sec
%% Cell type:markdown id: tags:
### Unbounded integers ###
The SAT translation via Kodkod/Alloy requires to determine the bid width.
It cannot be applied to unbounded integers.
Even for bounded integers it is quite tricky to get the bid widths correct: one needs also to take care of intermediate results. Alloy can detect incorrect models where an overflow occured, but to our understanding not where an overflow prevented a model (e.g., use inside negation or equivalence, see ```#(V.SS->V.SS)=0 iff no V.SS``` in paper at ABZ conference).
SMTLib is more tailored towards proof than towards model finding; as such it has typically no/less issues with unbounded values.
The ProB default solver can also deal with unbounded integers: it tries to narrow down domains to finite ones. If this fails, an unbounded variable is enumerated (partially) and an **enumeration warning** is generated. In case a solution is found, this warning is ignored, otherwise the result of ProB's analysis is **UNKNOWN**.
Some inconsistencies cannot be detected by interval/domain propagation; here it helps to activate ProB's CHR module which performs some additional inferences.
Let us perform some experiments. Both ProB and Z3 can solve the following:
%% Cell type:code id: tags:
``` prob
:solve z3 x*x=100
```
%% Output
$TRUE$
**Solution:**
* $x = -10$
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
Here is an example where ProB generates an enumeration warning, but finds a solution:
%% Cell type:code id: tags:
``` prob
x>100 & x mod 2000 = 1 & x mod 3000 = 1
```
%% Output
$TRUE$
**Solution:**
* $x = 6001$
TRUE
Solution:
x = 6001
%% Cell type:code id: tags:
``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1
```
%% Output
$TRUE$
**Solution:**
* $x = 6001$
TRUE
Solution:
x = 6001
%% Cell type:markdown id: tags:
Here ProB generates an enumeration warning and does not find a solution, hence the result is **UNKNOWN**. Here Z3 finds a solution.
%% Cell type:code id: tags:
``` prob
:solve prob x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
```
%% Output
$TRUE$
**Solution:**
* $x = 6756001$
TRUE
Solution:
x = 6756001
%% Cell type:markdown id: tags:
Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.
ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**.
%% Cell type:code id: tags:
``` prob
:solve z3 x>y & y>x
```
%% Output
$FALSE$
FALSE
%% Cell type:code id: tags:
``` prob
:solve prob x>y &y>x
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
### Summary for Integer Arithmetic ###
Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded)
------|------------|---------------|---
ProB CLP(FD) | yes | very good | limited with CHR
ProB Z3 | yes | reasonable | very good
ProB Kodkod | no | good | -
%% Cell type:markdown id: tags:
## Set Constraints ##
After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables.
### Translation to SAT ###
The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements.
Take for example the following constraint:
%% Cell type:code id: tags:
``` prob
x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1:x & x ⊂ y
```
%% Output
$TRUE$
**Solution:**
* $x = \{1\}$
* $y = \{1,2\}$
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:markdown id: tags:
| Element | x | y | x ∪ y |
| ------------- |-------------| -----| -----|
| 1 | x1 | y1 | x1 or y1
| 2 | x2 | y2 | x2 or y2 |
%% Cell type:code id: tags:
``` prob
:table {x1,x2,y1,y2 | {x1,x2,y1,y2} <: BOOL &
(x1=TRUE or y1=TRUE) & (x2=TRUE or y2=TRUE) & // x ∪ y = 1..2
x1=TRUE & // 1:x
(x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) //x ⊂ y
}
```
%% Output
|x1|x2|y1|y2|
|---|---|---|---|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
x1 x2 y1 y2
TRUE FALSE TRUE TRUE
%% Cell type:markdown id: tags:
This translation to SAT is exactly what the Kodkod backend does:
%% Cell type:code id: tags:
``` prob
:solve kodkod x <: 1..2 & y<: 1..2 & x \/ y = 1..2 & 1:x & x <<: y
```
%% Output
$TRUE$
**Solution:**
* $x = \{1\}$
* $y = \{1,2\}$
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:markdown id: tags:
Limitations of translating set constraints to SAT:
- this cannot deal with **unbounded** sets: we need to know a finite type for each set, so that we can generate a finite bit vector
- this approach cannot usually deal with **higher order** sets (sets of sets), as the size of the bit vector would be prohibitively large
Given that:
%% Cell type:code id: tags:
``` prob
card(POW(1..100))
```
%% Output
$1267650600228229401496703205376$
1267650600228229401496703205376
%% Cell type:markdown id: tags:
translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376.
%% Cell type:code id: tags:
``` prob
x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)
```
%% Output
$TRUE$
**Solution:**
* $x = \{\{100\},\{1\}\}$
TRUE
Solution:
x = {{100},{1}}
%% Cell type:markdown id: tags:
Also, in the following constraint, the set x is unbounded and no translation to SAT is feasible (without a very clever analysis of the universal implications).
%% Cell type:code id: tags:
``` prob
{100}:x & !y.(y:x => (!z.(z:y => y \/ {z / 2}:x)))
```
%% Output
$TRUE$
**Solution:**
* $x = \{\{100\},\{50,100\},\{25,50,100\},\{12,25,50,100\},\{6,12,25,50,100\},\{3,6,12,25,50,100\},\{1,3,6,12,25,50,100\},\{0,1,3,6,12,25,50,100\}\}$
TRUE
Solution:
x = {{100},{50,100},{25,50,100},{12,25,50,100},{6,12,25,50,100},{3,6,12,25,50,100},{1,3,6,12,25,50,100},{0,1,3,6,12,25,50,100}}
%% Cell type:markdown id: tags:
However, when it is applicable the propositional encoding of sets can be very effective for SAT solvers.
The following example, involving various relational operators can currently only be solved by our Kodkod backend:
%% Cell type:code id: tags:
``` prob
:time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=4..5
```
%% Output
Execution time: 0.097977646 seconds
$TRUE$
**Solution:**
* $r = \{(3\mapsto5),(3\mapsto4),(5\mapsto5),(5\mapsto4),(1\mapsto4),(2\mapsto4),(4\mapsto4)\}$
TRUE
Solution:
r = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}
%% Cell type:markdown id: tags:
### Translation to SMTLib ###
This can in principle deal with higher-order sets and unbounded sets, but makes heavy use of quantifiers.
The practical usefulness is currently very limited.
%% Cell type:code id: tags:
``` prob
:solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2
```
%% Output
$TRUE$
**Solution:**
* $x = \emptyset$
* $y = \{1,2\}$
TRUE
Solution:
x = ∅
y = {1,2}
%% Cell type:markdown id: tags:
Internally, the constraint is rewritten to support operators which do not exist in SMTLib:
%% Cell type:code id: tags:
``` prob
∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & // x ⊆ 1..2
∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) & // y ⊆ 1..2
x ∪ y = {1,2}
```
%% Output
$TRUE$
**Solution:**
* $x = \emptyset$
* $y = \{1,2\}$
TRUE
Solution:
x = ∅
y = {1,2}
%% Cell type:markdown id: tags:
This in turn gets translated to SMTLib (calls to the Z3 API):
- mk_var(set(integer),x) $\rightarrow$ 2
- mk_var(set(integer),y) $\rightarrow$ 3
- mk_bounded_var(integer,_smt_tmp28) $\rightarrow$ 4
- mk_op(member,4,2) $\rightarrow$ 5
- mk_int_const(1) $\rightarrow$ 6
- mk_op(greater_equal,4,6) $\rightarrow$ 7
- mk_int_const(2) $\rightarrow$ 8
- mk_op(greater_equal,8,4) $\rightarrow$ 9
- mk_op_arglist(conjunct,[7,9]) $\rightarrow$ 10
- mk_op(implication,5,10) $\rightarrow$ 11
- mk_quantifier(forall,[4],11) $\rightarrow$ 12
- mk_bounded_var(integer,_smt_tmp29) $\rightarrow$ 13
- mk_op(member,13,3) $\rightarrow$ 14
- mk_int_const(1) $\rightarrow$ 15
- mk_op(greater_equal) $\rightarrow$ 13,15,16
- mk_int_const(2) $\rightarrow$ 17
- mk_op(greater_equal,17,13) $\rightarrow$ 18
- mk_op_arglist(conjunct,[16,18]) $\rightarrow$ 19
- mk_op(implication,14,19) $\rightarrow$ 20
- mk_quantifier(forall,[13],20) $\rightarrow$ 21
- mk_op(union,2,3) $\rightarrow$ 22
- mk_int_const(1) $\rightarrow$ 23
- mk_int_const(2) $\rightarrow$ 24
- mk_set([23,24]) $\rightarrow$ 25
- mk_op(equal,22,25) $\rightarrow$ 26
- mk_op_arglist(conjunct,[12,21,26]) $\rightarrow$ 27
%% Cell type:markdown id: tags:
This can be solved by Z3 but not by CVC4. Already the slightly more complicated example from above (or the other examples) cannot be solved:
%% Cell type:code id: tags:
``` prob
:solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
Let us look at another relatively simple example which poses problems:
%% Cell type:code id: tags:
``` prob
:solve z3 f = {1|->3, 2|->6} & r = f~[{6}]
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
To understand why this simple constraint cannot be solved, we have to know how the translation works:
The relational inverse gets translated into two universal quantifications for SMTLib:
```
x = y~
<=>
!(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) &
!(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x))
```
Similarly, r = f[s] is translated as follows:
```
r = f[s]
<=>
!st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) &
!st27.(#st26.(st26 |-> st27 : f & st26 : s) => st27 : r)
```
The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can).
%% Cell type:code id: tags:
``` prob
:prettyprint f = {(1|->3),(2|->6)} &
#st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &
!(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
```
%% Output
$\mathit{f} = \{(1\mapsto 3),(2\mapsto 6)\} \wedge (\exists /* LET */ (\mathit{st13}).( (\mathit{st13})=\mathit{r} \wedge \forall \mathit{st15}\cdot (\mathit{st15} \in \mathit{st13} \mathbin\Rightarrow \exists \mathit{st16}\cdot (6 \mapsto \mathit{st15} \in \mathit{st16} \wedge (\forall (\mathit{st17},\mathit{st18})\cdot (\mathit{st17} \mapsto \mathit{st18} \in \mathit{st16} \mathbin\Rightarrow \mathit{st18} \mapsto \mathit{st17} \in \mathit{f}) \wedge \forall (\mathit{st17},\mathit{st18})\cdot (\mathit{st18} \mapsto \mathit{st17} \in \mathit{f} \mathbin\Rightarrow \mathit{st17} \mapsto \mathit{st18} \in \mathit{st16})))) \wedge \forall \mathit{st15}\cdot (\exists \mathit{st19}\cdot (6 \mapsto \mathit{st15} \in \mathit{st19} \wedge (\forall (\mathit{st20},\mathit{st21})\cdot (\mathit{st20} \mapsto \mathit{st21} \in \mathit{st19} \mathbin\Rightarrow \mathit{st21} \mapsto \mathit{st20} \in \mathit{f}) \wedge \forall (\mathit{st20},\mathit{st21})\cdot (\mathit{st21} \mapsto \mathit{st20} \in \mathit{f} \mathbin\Rightarrow \mathit{st20} \mapsto \mathit{st21} \in \mathit{st19}))) \mathbin\Rightarrow \mathit{st15} \in \mathit{st13})))$
f = {(1↦3),(2↦6)} ∧ (∃ /* LET */ (st13).( (st13)=r ∧ ∀st15·(st15 ∈ st13 ⇒ ∃st16·(6 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16)))) ∧ ∀st15·(∃st19·(6 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ⇒ st15 ∈ st13)))
%% Cell type:code id: tags:
``` prob
:time :solve prob f = {(1|->3),(2|->6)} &
#st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &
!(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
```
%% Output
Execution time: 0.140791514 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{r} = \{2\}$
* $\mathit{f} = \{(1\mapsto 3),(2\mapsto 6)\}$
TRUE
Solution:
r = {2}
f = {(1↦3),(2↦6)}
%% Cell type:code id: tags:
``` prob
:time :solve cvc4 f = {(1|->3),(2|->6)} &
#st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &
!(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
The SMTLib translation is still of limited value for finding models.
However, for finding inconsistencies it is much better and can detect certain inconsistencies which ProB's solver cannot.
While both ProB and Z3 can solve the following:
%% Cell type:code id: tags:
``` prob
:solve prob x:s1 & x:s2 & x /: (s1 /\ s2) & s1 <: INTEGER
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
only the Z3 backend can solve this one:
%% Cell type:code id: tags:
``` prob
:solve z3 x:s1 & x/:s2 & x /: (s1 \/s2) & s1 <: INTEGER
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
### ProB's Set Solver ###
ProB has actually three set representations:
- Prolog lists of elements
- AVL trees for fully known sets
- symbolic closures for large or infinite sets
For finite sets, the AVL tree representation is the most efficient and allows for efficient lookups.
It, however, requires all elements to be fully known.
The symbolic closure can be used for large or infinite sets.
ProB will automatically use it for sets it knows to be infinite, or when an enumeration warning occurs during an attempt at expanding a set.
The list representation is used for sets where some of the members are known or partially known.
#### AVL tree representation ####
The following generates the AVL tree representation:
%% Cell type:code id: tags:
``` prob
{x|x∈0..2**10 & x mod 100 = 0}
```
%% Output
$\{0,100,200,300,400,500,600,700,800,900,1000\}$
{0,100,200,300,400,500,600,700,800,900,1000}
%% Cell type:markdown id: tags:
A lot of operators and predicates have optimised versions for the AVL tree represenation, e.g.,
%% Cell type:code id: tags:
``` prob
s = {x|x∈0..2**10 & x mod 100 = 0} &
mx = max(s) &
mn = min(s)
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{mn} = 0$
* $\mathit{s} = \{0,100,200,300,400,500,600,700,800,900,1000\}$
* $\mathit{mx} = 1000$
TRUE
Solution:
mn = 0
s = {0,100,200,300,400,500,600,700,800,900,1000}
mx = 1000
%% Cell type:markdown id: tags:
#### Symbolic closure representation ####
In the following case, ProB knows that the set is infinite and is kept symbolic:
%% Cell type:code id: tags:
``` prob
{x|x>1000}
```
%% Output
$\{\mathit{x}\mid \mathit{x} > 1000\}$
{x∣x > 1000}
%% Cell type:markdown id: tags:
Symbolic sets can be used in various ways:
%% Cell type:code id: tags:
``` prob
inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{inf} = \{\mathit{x}\mid \mathit{x} > 1000\}$
* $\mathit{res} = (1001 \ldots 1100)$
TRUE
Solution:
inf = {x∣x > 1000}
res = (1001 ‥ 1100)
%% Cell type:markdown id: tags:
For the following set, ProB tries to expand it and then an enumeration warning occurs (also called a **virtual timeout**, ProB realises that no matter what time budget it would be given a timeout would occur).
The set is then kept symbolic and can again be used in various ways.
%% Cell type:code id: tags:
``` prob
inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf
```
%% Output
$\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}}\mathit{TRUE}$
**Solution:**
* $\mathit{inf} = \{\mathit{x}\mid \mathit{x} > 1000 \land \mathit{x} \mathit{mod} 25 = 0\}$
* $\mathit{res} = ((900 \ldots 1100) \binter \{\mathit{x}\mid \mathit{x} > 1000 \land \mathit{x} \mathit{mod} 25 = 0\})$
TRUE
Solution:
inf = {x∣x > 1000 ∧ x mod 25 = 0}
res = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})
%% Cell type:markdown id: tags:
The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:
%% Cell type:code id: tags:
``` prob
inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf
```
%% Output
$\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}}\mathit{TRUE}$
$\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}}\mathit{TRUE}$
**Solution:**
* $\mathit{inf} = \{\mathit{x}\mid \mathit{x} > 1000 \land \mathit{x} \mathit{mod} 25 = 0\}$
* $\mathit{res} = ((900 \ldots 1100) \binter \{\mathit{x}\mid \mathit{x} > 1000 \land \mathit{x} \mathit{mod} 25 = 0\})$
* $\mathit{res} = ((900 \upto 1100) \binter \{\mathit{x}\mid \mathit{x} > 1000 \land \mathit{x} \mathit{mod} 25 = 0\})$
TRUE
Solution:
inf = {x∣x > 1000 ∧ x mod 25 = 0}
res = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})
%% Cell type:markdown id: tags:
Internally, a symbolic representation is a **closure** in functional programming terms: all dependent variables are *compiled* into the closure: the closure can be passed as a value and evaluated without needing access to an environment. In Prolog this is represented as a tuple:
- closure(Parameters,Types,CompiledPredicate)
For example, a set {x|x>v} where v has the value 17 is compiled to:
- closure([x],[integer],```x>17```)
%% Cell type:markdown id: tags:
#### List representation ####
The list representation is used when a finite set is partially known and constraint solving has to determine the set.
%% Cell type:code id: tags:
``` prob
vec: 1..10 --> 0..9999 &
vec(1) : {1,10} &
!x.(x:2..10 => vec(x) = vec(x-1)*2)
```
%% Output
$TRUE$
**Solution:**
* $vec = \{(1\mapsto1),(2\mapsto2),(3\mapsto4),(4\mapsto8),(5\mapsto16),(6\mapsto32),(7\mapsto64),(8\mapsto128),(9\mapsto256),(10\mapsto512)\}$
TRUE
Solution:
vec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128),(9↦256),(10↦512)}
%% Cell type:markdown id: tags:
Note that Kodkod translation and SMT translation not very effective for the above.
The Kodkod translation can deal with a simpler version of the above:
%% Cell type:code id: tags:
``` prob
:time :solve kodkod vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)
```
%% Output
Execution time: 2.542529935 seconds
$TRUE$
**Solution:**
* $vec = \{(3\mapsto4),(5\mapsto16),(6\mapsto32),(7\mapsto64),(1\mapsto1),(2\mapsto2),(4\mapsto8),(8\mapsto128)\}$
TRUE
Solution:
vec = {(3↦4),(5↦16),(6↦32),(7↦64),(1↦1),(2↦2),(4↦8),(8↦128)}
%% Cell type:code id: tags:
``` prob
:time :solve prob vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)
```
%% Output
Execution time: 0.016755497 seconds
$TRUE$
**Solution:**
* $vec = \{(1\mapsto1),(2\mapsto2),(3\mapsto4),(4\mapsto8),(5\mapsto16),(6\mapsto32),(7\mapsto64),(8\mapsto128)\}$
TRUE
Solution:
vec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128)}
%% Cell type:code id: tags:
``` prob
:time :solve z3 vec: 1..8 --> 0..199 & vec(1) : {1,10} & !x.(x:2..8 => vec(x) = vec(x-1)*2)
```
%% Output
:time: :solve: Computation not completed: time out
%% Cell type:markdown id: tags:
### ProB's Solving Algorithm ###
ProB tries to accomplish several conflicting goals:
- being able to deal with concrete data, i.e., sets and relations containing thousands or hundreds of thousands of elementas
- being able to deal with symbolic, infinite sets, relations and functions.
- being able to perform efficient computation over large data as well as constraint solving
For example, efficient computation over large concrete data is the following:
%% Cell type:code id: tags:
``` prob
:time :solve prob s1 = {x|x:1..10**n & x mod n = 0} & s2 = {y|y:1..10**n & y mod (n+1) = 0} & s3 = s1 /\ s2 & n=4
```
%% Output
Execution time: 0.266020568 seconds
Execution time: 0.716030873 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{s3} = \exists 500\in\{20,40,\0xpto,9980,10000\}$
* $\mathit{s3} = \#500\in\{20,40,\ldots,9980,10000\}$
* $\mathit{n} = 4$
* $\mathit{s1} = \exists 2500\in\{4,8,\0xpto,9996,10000\}$
* $\mathit{s2} = \exists 2000\in\{5,10,\0xpto,9995,10000\}$
* $\mathit{s1} = \#2500\in\{4,8,\ldots,9996,10000\}$
* $\mathit{s2} = \#2000\in\{5,10,\ldots,9995,10000\}$
TRUE
Solution:
s3 = ∃500∈{20,40,…,9980,10000}
s3 = #500∈{20,40,…,9980,10000}
n = 4
s1 = ∃2500∈{4,8,…,9996,10000}
s2 = ∃2000∈{5,10,…,9995,10000}
s1 = #2500∈{4,8,…,9996,10000}
s2 = #2000∈{5,10,…,9995,10000}
%% Cell type:markdown id: tags:
Here is a simple verison of the above
%% Cell type:code id: tags:
``` prob
:time :solve prob x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y
```
%% Output
Execution time: 0.014582494 seconds
Execution time: 0.122529996 seconds
$TRUE$
$\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\mathit{TRUE}$
**Solution:**
* $xy = \exists201\in\{1,2,\0xpto,299,300\}$
* $x = (1 \ldots 100)$
* $y = (200 \ldots 300)$
* $n = 100$
* $\mathit{xy} = \exists 201\in\{1,2,\ldots,299,300\}$
* $\mathit{x} = (1 \upto 100)$
* $\mathit{y} = (200 \upto 300)$
* $\mathit{n} = 100$
TRUE
Solution:
xy = ∃201∈{1,2,…,299,300}
x = (1 ‥ 100)
y = (200 ‥ 300)
n = 100
%% Cell type:code id: tags:
``` prob
:solve z3 x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y
```
%% Output
:solve: Computation not completed: time out
%% Cell type:code id: tags:
``` prob
:time :solve kodkod x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y
```
%% Output
Execution time: 0.546787958 seconds
Execution time: 2.035079877 seconds
$TRUE$
$\mathit{TRUE}$
**Solution:**
* $xy = \{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,\0xpto\}$
* $x = \{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64\}$
* $y = \{200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256\}$
* $n = 100$
* $\mathit{xy} = \{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,\ldots\}$
* $\mathit{x} = \{3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64\}$
* $\mathit{y} = \{200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256\}$
* $\mathit{n} = 100$
TRUE
Solution:
xy = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,200,201,202,203,204,205,206,…}
x = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64}
y = {200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256}
n = 100
%% Cell type:markdown id: tags:
In the appendix there are more examples which analyse the performance for such examples.
%% Cell type:markdown id: tags:
ProB employs the *Andorra* principle: deterministic computations are done first.
As there are multiple set representations, there are actually two kinds of deterministic computations:
- deterministic computations that generate an efficient representation, e.g., an AVL set representation
- and other deterministic computations
The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.
- Priority 0 means that an efficient representation can be generated
- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation
- Priority k is a choice point/enumeration which may generate k possible values
At each solving step one waitflag is activated, the one with the lowest priority.
CLP(FD) variables are also registered in the WAITFLAG store and are enumerated before a waitflag of the same priority is activated. For tie breaking one typically uses the **most attached constraints first** (ffc) heuristic.
#### Example ####
Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y``` is solved.
- all constraints are registered
- in phase 0 ```n=100``` is run
- this means that ```1..n``` can be efficiently computed
- this means that ```x = 1..n``` triggers in phase 0
- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```
- this means that ```y = 2*n..3*n``` triggers in phase 0
- again, this means that ```x \/ y``` can be efficiently computed
- finally ```xy = x \/ y``` can be executed in phase 0
No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.
%% Cell type:markdown id: tags:
#### Dealing with unbounded enumeration ####
Note: if an unbounded enumeration is encountered, the solver registers an **enumeration warning** in the current scope (every quantification / comprehension set results in a new inner scope). Depending on the kind of scope (existential/universal) and on whether a solution is found, the warning gets translated into an **UNKNOWN** result.
%% Cell type:markdown id: tags:
### Functional Programming ###
Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqrt) = 100
```
%% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\mathit{TRUE}$
**Solution:**
* $\mathit{r2} = \{1,4,9,16,25,36,49,64,81,100\}$
* $\mathit{r3} = [4,9,25,49,121]$
* $\mathit{r4} = 256$
* $\mathit{sqrt} = 10$
* $\mathit{f} = \lambda \mathit{x}\qdot(\mathit{x} \in \mathit{INTEGER}\mid \mathit{x} * \mathit{x})$
* $\mathit{r1} = 10000000000$
TRUE
Solution:
r2 = {1,4,9,16,25,36,49,64,81,100}
r3 = [4,9,25,49,121]
r4 = 256
sqrt = 10
f = λx·(x ∈ INTEGER∣x ∗ x)
r1 = 10000000000
%% Cell type:code id: tags:
``` prob
f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqr) = 100 &
r5 = closure1(f)[{10000}]
```
%% Output
$\newcommand{\cprod}{\mathbin\times}\newcommand{\cprod}{\mathbin\times}\mathit{TRUE}$
**Solution:**
* $\mathit{r2} = \{1,2,3,4\}$
* $\mathit{r3} = [2,2,3,3,4]$
* $\mathit{r4} = 2$
* $\mathit{r5} = \{2,4,10,100\}$
* $\mathit{sqr} = 9802$
* $\mathit{f} = \{\mathit{x},\mathit{y}\mid \mathit{x} \in \mathit{NATURAL} \land \mathit{y} \cprod 2 \geq \mathit{x} \land (\mathit{y} - 1) \cprod 2 < \mathit{x}\}$
* $\mathit{r1} = 317$
TRUE
Solution:
r2 = {1,2,3,4}
r3 = [2,2,3,3,4]
r4 = 2
r5 = {2,4,10,100}
sqr = 9802
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
r1 = 317
%% Cell type:markdown id: tags:
### Reification ###
Reification is linking the truth value of a constraint with a boolean variable.
ProB's kernel provides support for reifying a considerable number of constraints (but not yet all!).
Reification is important for efficiency, to avoid choice points and is important to link various solvers of ProB (set, arithmetic, boolean,...).
![CBCKernel](./img/ProB_CBC_Kernel.pdf)
%% Cell type:code id: tags:
``` prob
(x>100 <=> (ReifVar=TRUE)) & (x<125 <=> (ReifVar=FALSE)) & x<200
```
%% Output
$TRUE$
**Solution:**
* $x = 125$
* $ReifVar = TRUE$
TRUE
Solution:
x = 125
ReifVar = TRUE
%% Cell type:markdown id: tags:
![Linking](./img/Linking.png)
%% Cell type:markdown id: tags:
## Summary of Set Constraint Solving Approaches ##
- SAT Translation (Kodkod backend):
- needs finite and small base type, no unbounded or higher-order sets
- can be very effective for complex constraints involving image, transitive closure,...
- limited performance for large sets
- SMTLib Translation (Z3/CVC4 backend):
- can deal with unbounded and large sets
- due to heavy use of quantifiers, some finite constraints get translated into infinite ones: limited model finding capabilities
- ProB's default backend:
- can deal with unbounded and large sets
- limited constraint solving for complex constraints involving image, transitive closure,...
- no learning, backjumping
- works well for large sets and semi-deterministic computation
- works well for animation, data validation, disproving
- limitations appear for symbolic model checking (IC3,...)
- Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable)
- CHR: can complement ProB's default backend
- currently only very limited propagations (>, >=, x=y+c, ...)
- very difficult to control and avoid propagation loops
%% Cell type:markdown id: tags:
### Integrations of Approaches ###
ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.
Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.
The main motivation was new symbolic validation techniques such as IC3.
The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.
However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).
A more promising, fine-grained integration has been presented at PADL'18.
%% Cell type:markdown id: tags:
## Appendix ##
%% Cell type:markdown id: tags:
### Explicit Computations ####
What about explicit computations? How well does the SMTLib translation fare here?
%% Cell type:code id: tags:
``` prob
:solve z3 x = 1..1000 /\ (200..300)
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..40 /\ (6..15)
```
%% Output
Execution time: 0.224425596 seconds
$TRUE$
**Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..60 /\ (6..15)
```
%% Output
Execution time: 1.149180308 seconds
$TRUE$
**Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..80 /\ (6..15)
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve prob x = 1..80 /\ (6..15)
```
%% Output
Execution time: 0.005873811 seconds
$TRUE$
**Solution:**
* $x = (6 \ldots 15)$
TRUE
Solution:
x = (6 ‥ 15)
%% Cell type:markdown id: tags:
In the following the inverse operator seems to pose problems to Z3:
%% Cell type:code id: tags:
``` prob
:solve z3 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]
```
%% Output
$TRUE$
**Solution:**
* $r = \{2,3,5,7,11\}$
* $c = (\{2,3,5,7,11\} * \{4,8,16,32\})$
* $s1 = \{2,3,5,7,11\}$
* $s2 = \{4,8,16,32\}$
TRUE
Solution:
r = {2,3,5,7,11}
c = ({2,3,5,7,11} ∗ {4,8,16,32})
s1 = {2,3,5,7,11}
s2 = {4,8,16,32}
%% Cell type:markdown id: tags:
### Benchmark Puzzles ####
#### N-Queens ####
%% Cell type:code id: tags:
``` prob
:time :solve prob n=8 &
queens : 1..n >-> 1..n &
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
```
%% Output
Execution time: 0.060237608 seconds
$TRUE$
**Solution:**
* $queens = \{(1\mapsto4),(2\mapsto2),(3\mapsto7),(4\mapsto3),(5\mapsto6),(6\mapsto8),(7\mapsto5),(8\mapsto1)\}$
* $n = 8$
TRUE
Solution:
queens = {(1↦4),(2↦2),(3↦7),(4↦3),(5↦6),(6↦8),(7↦5),(8↦1)}
n = 8
%% Cell type:code id: tags:
``` prob
:time :solve z3 n=8 &
queens : 1..n >-> 1..n &
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
```
%% Output
Execution time: 0.393750784 seconds
$TRUE$
**Solution:**
* $queens = \{(1\mapsto4),(2\mapsto7),(3\mapsto5),(4\mapsto2),(5\mapsto6),(6\mapsto1),(7\mapsto3),(8\mapsto8)\}$
* $n = 8$
TRUE
Solution:
queens = {(1↦4),(2↦7),(3↦5),(4↦2),(5↦6),(6↦1),(7↦3),(8↦8)}
n = 8
%% Cell type:code id: tags:
``` prob
:time :solve kodkod n=8 &
queens : 1..n >-> 1..n &
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
```
%% Output
Execution time: 0.467670114 seconds
$TRUE$
**Solution:**
* $queens = \{(3\mapsto2),(5\mapsto5),(6\mapsto1),(7\mapsto8),(1\mapsto3),(2\mapsto6),(4\mapsto7),(8\mapsto4)\}$
* $n = 8$
TRUE
Solution:
queens = {(3↦2),(5↦5),(6↦1),(7↦8),(1↦3),(2↦6),(4↦7),(8↦4)}
n = 8
%% Cell type:code id: tags:
``` prob
:time :solve z3 n=3 & bshp <: (1..n)*(1..n) &
!(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &
card(bshp) = 3
```
%% Output
:time: :solve: Computation not completed: time out
%% Cell type:markdown id: tags:
Solving takes about 150 seconds; Kodkod translation currently does not work due to card and preventing overflows.
%% Cell type:code id: tags:
``` prob
:prettyprint n=3 & bshp <: (1..n)*(1..n) &
!(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &
card(bshp) = 3
```
%% Output
$\mathit{n} = 3 \wedge \mathit{bshp} \subseteq (1 .. \mathit{n}) \times (1 .. \mathit{n}) \wedge \forall (\mathit{i},\mathit{j})\cdot (\{\mathit{i},\mathit{j}\} \subseteq 1 .. \mathit{n} \mathbin\Rightarrow (\mathit{i} \mapsto \mathit{j} \in \mathit{bshp} \mathbin\Rightarrow \forall \mathit{k}\cdot (\mathit{k} \in \mathit{i} + 1 .. \mathit{n} \mathbin\Rightarrow (\mathit{k} \mapsto (\mathit{j} + \mathit{k}) - \mathit{i}) \not\in \mathit{bshp} \wedge (\mathit{k} \mapsto (\mathit{j} - \mathit{k}) + \mathit{i}) \not\in \mathit{bshp}))) \wedge \mathit{card}(\mathit{bshp}) = 3$
n = 3 ∧ bshp ⊆ (1 ‥ n) × (1 ‥ n) ∧ ∀(i,j)·({i,j} ⊆ 1 ‥ n ⇒ (i ↦ j ∈ bshp ⇒ ∀k·(k ∈ i + 1 ‥ n ⇒ (k ↦ (j + k) - i) ∉ bshp ∧ (k ↦ (j - k) + i) ∉ bshp))) ∧ card(bshp) = 3
%% Cell type:markdown id: tags:
#### Datavalidation example ####
%% Cell type:code id: tags:
``` prob
::load
MACHINE
signals
SETS
/* Ensemble des signaux */
SIGNAL =
{ PL01
, PL02
, PL03
, PL04
, PL05
, PL06
, PL07
, PL08
, PL09
, PL10
, PL11
, PL12
, PL13
, PL14
, PL15
, PL16
, PL17
, PL18
, PL19
, PL20
}
END
```
%% Output
Loaded machine: signals
%% Cell type:code id: tags:
``` prob
:time :solve prob nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL]
```
%% Output
Execution time: 0.199987519 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{res} = \{\mathit{PL01},\mathit{PL12}\}$
* $\mathit{nxt} = \{(\mathit{PL01}\mapsto \mathit{PL02}),(\mathit{PL02}\mapsto \mathit{PL03}),(\mathit{PL03}\mapsto \mathit{PL04}),(\mathit{PL04}\mapsto \mathit{PL05}),(\mathit{PL05}\mapsto \mathit{PL06}),(\mathit{PL06}\mapsto \mathit{PL07}),(\mathit{PL07}\mapsto \mathit{PL08}),(\mathit{PL08}\mapsto \mathit{PL09}),(\mathit{PL09}\mapsto \mathit{PL10}),(\mathit{PL10}\mapsto \mathit{PL11}),(\mathit{PL11}\mapsto \mathit{PL11}),(\mathit{PL12}\mapsto \mathit{PL13}),(\mathit{PL13}\mapsto \mathit{PL14}),(\mathit{PL14}\mapsto \mathit{PL15}),(\mathit{PL15}\mapsto \mathit{PL16}),(\mathit{PL16}\mapsto \mathit{PL17}),(\mathit{PL17}\mapsto \mathit{PL18}),(\mathit{PL18}\mapsto \mathit{PL19}),(\mathit{PL19}\mapsto \mathit{PL20}),(\mathit{PL20}\mapsto \mathit{PL20})\}$
TRUE
Solution:
res = {PL01,PL12}
nxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}
%% Cell type:code id: tags:
``` prob
:time :solve z3 nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL]
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve kodkod nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL]
```
%% Output
Execution time: 0.789322780 seconds
$\mathit{TRUE}$
**Solution:**
* $\mathit{res} = \{\mathit{PL01},\mathit{PL12}\}$
* $\mathit{nxt} = \{(\mathit{PL01}\mapsto \mathit{PL02}),(\mathit{PL02}\mapsto \mathit{PL03}),(\mathit{PL03}\mapsto \mathit{PL04}),(\mathit{PL04}\mapsto \mathit{PL05}),(\mathit{PL05}\mapsto \mathit{PL06}),(\mathit{PL06}\mapsto \mathit{PL07}),(\mathit{PL07}\mapsto \mathit{PL08}),(\mathit{PL08}\mapsto \mathit{PL09}),(\mathit{PL09}\mapsto \mathit{PL10}),(\mathit{PL10}\mapsto \mathit{PL11}),(\mathit{PL11}\mapsto \mathit{PL11}),(\mathit{PL12}\mapsto \mathit{PL13}),(\mathit{PL13}\mapsto \mathit{PL14}),(\mathit{PL14}\mapsto \mathit{PL15}),(\mathit{PL15}\mapsto \mathit{PL16}),(\mathit{PL16}\mapsto \mathit{PL17}),(\mathit{PL17}\mapsto \mathit{PL18}),(\mathit{PL18}\mapsto \mathit{PL19}),(\mathit{PL19}\mapsto \mathit{PL20}),(\mathit{PL20}\mapsto \mathit{PL20})\}$
TRUE
Solution:
res = {PL01,PL12}
nxt = {(PL01↦PL02),(PL02↦PL03),(PL03↦PL04),(PL04↦PL05),(PL05↦PL06),(PL06↦PL07),(PL07↦PL08),(PL08↦PL09),(PL09↦PL10),(PL10↦PL11),(PL11↦PL11),(PL12↦PL13),(PL13↦PL14),(PL14↦PL15),(PL15↦PL16),(PL16↦PL17),(PL17↦PL18),(PL18↦PL19),(PL19↦PL20),(PL20↦PL20)}
%% Cell type:code id: tags:
``` prob
:prettyprint x=NATURAL & y=NAT
```
%% Output
$\mathit{x} = \mathbb N \wedge \mathit{y} = NAT$
x = ℕ ∧ y = NAT
%% Cell type:code id: tags:
``` prob
x=NATURAL & y=NAT
```
%% Output
$\newcommand{\upto}{\mathbin{.\mkern1mu.}}\mathit{TRUE}$
**Solution:**
* $\mathit{x} = \mathit{NATURAL}$
* $\mathit{y} = (0 \upto 3)$
TRUE
Solution:
x = NATURAL
y = (0 ‥ 3)
%% Cell type:code id: tags:
``` prob
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment