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

update presentation

parent 1c366417
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/presentations/LPOP18.ipynb
+ 209
− 44
View file @ 82412e5c
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Solving (Set) Constraints in B and Event-B # # Solving (Set) Constraints in B and Event-B #
Michael Leuschel, Michael Leuschel,
David Geleßus (Jupyter Interface) David Geleßus (Jupyter Interface)
## A quick Introduction to B ## ## A quick Introduction to B ##
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Basic Datavalues in B ### ### Basic Datavalues in B ###
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
B provides the booleans, strings and integers as built-in datatypes. (Strings are not available in Event-B.) B provides the booleans, strings and integers as built-in datatypes. (Strings are not available in Event-B.)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
BOOL BOOL
``` ```
%% Output %% Output
$\{\mathit{FALSE},\mathit{TRUE}\}$ $\{\mathit{FALSE},\mathit{TRUE}\}$
{FALSE,TRUE} {FALSE,TRUE}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
"this is a string" "this is a string"
``` ```
%% Output %% Output
$\text{"this is a string"}$ $\text{"this is a string"}$
"this is a string" "this is a string"
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1024 1024
``` ```
%% Output %% Output
$1024$ $1024$
1024 1024
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Users can define their own datatype in a B machine. Users can define their own datatype in a B machine.
One distinguishes between explicitly specified enumerated sets and deferred sets. One distinguishes between explicitly specified enumerated sets and deferred sets.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE MyBasicSets MACHINE MyBasicSets
SETS Trains = {thomas, gordon}; Points SETS Trains = {thomas, gordon}; Points
END END
``` ```
%% Output %% Output
Loaded machine: MyBasicSets Loaded machine: MyBasicSets
%% Cell type:markdown id: tags: %% 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). 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: %% Cell type:code id: tags:
``` prob ``` prob
Points Points
``` ```
%% Output %% Output
$\{\mathit{Points1},\mathit{Points2}\}$ $\{\mathit{Points1},\mathit{Points2}\}$
{Points1,Points2} {Points1,Points2}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Pairs ### ### Pairs ###
B also has pairs of values, which can be written in two ways: B also has pairs of values, which can be written in two ways:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(thomas,10) (thomas,10)
``` ```
%% Output %% Output
$(thomas\mapsto10)$ $(thomas\mapsto10)$
(thomas↦10) (thomas↦10)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
thomas |-> 10 thomas |-> 10
``` ```
%% Output %% Output
$(thomas\mapsto10)$ $(thomas\mapsto10)$
(thomas↦10) (thomas↦10)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
**Tuples** simply correspond to nested pairs: **Tuples** simply correspond to nested pairs:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(thomas |-> gordon |-> 20) (thomas |-> gordon |-> 20)
``` ```
%% Output %% Output
$((\mathit{thomas}\mapsto \mathit{gordon})\mapsto 20)$ $((\mathit{thomas}\mapsto \mathit{gordon})\mapsto 20)$
((thomas↦gordon)↦20) ((thomas↦gordon)↦20)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Classical B also provides **records**, i.e., tuples with named fields: Classical B also provides **records**, i.e., tuples with named fields:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint r=rec(train:thomas,length:20,position:10302) :prettyprint r=rec(train:thomas,length:20,position:10302)
``` ```
%% Output %% Output
$\mathit{r} = \mathit{rec}(length:20,position:10302,train:\mathit{thomas})$ $\mathit{r} = \mathit{rec}(length:20,position:10302,train:\mathit{thomas})$
r = rec(length:20,position:10302,train:thomas) r = rec(length:20,position:10302,train:thomas)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Sets ### ### Sets ###
Sets in B can be specified in multiple ways. Sets in B can be specified in multiple ways.
For example, using explicit enumeration: For example, using explicit enumeration:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1,3,2,3} {1,3,2,3}
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
or via a predicate by using a **set comprehension**: or via a predicate by using a **set comprehension**:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x|x>0 & x<4} {x|x>0 & x<4}
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
For integers there are a variety of other sets, such as intervals: For integers there are a variety of other sets, such as intervals:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1..3 1..3
``` ```
%% Output %% Output
$\{1,2,3\}$ $\{1,2,3\}$
{1,2,3} {1,2,3}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
or the set of implementable integers INT = MININT..MAXINT or the set of implementable natural numbers NAT = 0..MAXINT. or the set of implementable integers INT = MININT..MAXINT or the set of implementable natural numbers NAT = 0..MAXINT.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Sets can be **higher-order** and contain other sets: Sets can be **higher-order** and contain other sets:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ 1..3, {1,2,3,2}, 0..1, {x|x>0 & x<4} } { 1..3, {1,2,3,2}, 0..1, {x|x>0 & x<4} }
``` ```
%% Output %% Output
$\{\{0,1\},\{1,2,3\}\}$ $\{\{0,1\},\{1,2,3\}\}$
{{0,1},{1,2,3}} {{0,1},{1,2,3}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
**Relations** are modelled as sets of pairs: **Relations** are modelled as sets of pairs:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ thomas|->gordon, gordon|->gordon, thomas|->thomas} { thomas↦gordon, gordon↦gordon, thomas↦thomas}
``` ```
%% Output %% Output
$\{(\mathit{thomas}\mapsto \mathit{thomas}),(\mathit{thomas}\mapsto \mathit{gordon}),(\mathit{gordon}\mapsto \mathit{gordon})\}$ :eval: Computation not completed: Unknown identifier "thomas",Unknown identifier "gordon",Unknown identifier "gordon",Unknown identifier "gordon",Unknown identifier "thomas",Unknown identifier "thomas"
{(thomas↦thomas),(thomas↦gordon),(gordon↦gordon)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("rel",{ thomas|->gordon, gordon|->gordon, thomas|->thomas}) :dot expr_as_graph ("rel",{ thomas|->gordon, gordon|->gordon, thomas|->thomas})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("rel",{(thomas,gordon),(gordon,gordon),(thomas,thomas)})]> <Dot visualization: expr_as_graph [("rel",{(thomas,gordon),(gordon,gordon),(thomas,thomas)})]>
%% Cell type:markdown id: tags: %% 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. 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```. The above relation is a subset of ```Trains * Trains```.
%% Cell type:code id: tags:
``` prob
:pref DOT_ENGINE=circo
```
%% Output
Preference changed: DOT_ENGINE = circo
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("k5",{x,y|x:1..5 & y:1..5 & x>y})
```
%% Output
<Dot visualization: expr_as_graph [("k5",{x,y|x:1..5 & y:1..5 & x>y})]>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
**Functions** are relations which map every domain element to at most one value: **Functions** are relations which map every domain element to at most one value:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ thomas|->1, gordon|->2} { thomas↦1, gordon↦2}
``` ```
%% Output %% Output
$\{(thomas\mapsto1),(gordon\mapsto2)\}$ $\{(thomas\mapsto1),(gordon\mapsto2)\}$
{(thomas↦1),(gordon↦2)} {(thomas↦1),(gordon↦2)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
**Sequences** are just functions whose domain is 1..n for some n: **Sequences** are just functions whose domain is 1..n for some n:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[4,5,6] = {1|->4, 2|->5, 3|->6} [4,5,6] = {1↦4, 2↦5, 3↦6}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Expressions vs Predicates vs Substitutions ## ## Expressions vs Predicates vs Substitutions ##
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Expressions ### ### Expressions ###
Expressions in B have a value. With ProB and with ProB's Jupyter backend, you can evaluate expresssions such as: 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: %% Cell type:code id: tags:
``` prob ``` prob
2**1000 2**1000
``` ```
%% Output %% Output
$10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376$ $10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376$
10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376
%% Cell type:markdown id: tags: %% 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. 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: For example set union and set difference:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..3 \/ 5..10) \ (2..6) (1..3 \/ 5..10) \ (2..6)
``` ```
%% Output %% Output
$\{1,7,8,9,10\}$ $\{1,7,8,9,10\}$
{1,7,8,9,10} {1,7,8,9,10}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..3 ∪ 5..10) \ (2..6) (1..3 ∪ 5..10) \ (2..6)
``` ```
%% Output %% Output
$\{1,7,8,9,10\}$ $\{1,7,8,9,10\}$
{1,7,8,9,10} {1,7,8,9,10}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The range of a relation or function: The range of a relation or function:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom({(thomas↦1),(gordon↦2)}) dom({(thomas↦1),(gordon↦2)})
``` ```
%% Output %% Output
$\{thomas,gordon\}$ $\{thomas,gordon\}$
{thomas,gordon} {thomas,gordon}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Function application: Function application:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{(thomas↦1),(gordon↦2)} (thomas) {(thomas↦1),(gordon↦2)} (thomas)
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Relational inverse (.~) and relational image .[.] : Relational inverse (.~) and relational image .[.] :
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{(thomas↦1),(gordon↦2)}~[2..3] {(thomas↦1),(gordon↦2)}~[2..3]
``` ```
%% Output %% Output
$\{\mathit{gordon}\}$ $\{\mathit{gordon}\}$
{gordon} {gordon}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Predicates ## 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). 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: %% Cell type:code id: tags:
``` prob ``` prob
2>3 2>3
``` ```
%% Output %% Output
$FALSE$ $FALSE$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
3>2 3>2
``` ```
%% Output %% Output
$TRUE$ $TRUE$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Within predicates you can use **open** variables, which are implicitly existentially quantified. Within predicates you can use **open** variables, which are implicitly existentially quantified.
ProB will display the solution for the open variables, if possible. ProB will display the solution for the open variables, if possible.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x*x=100 x*x=100
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = -10$ * $\mathit{x} = -10$
TRUE TRUE
Solution: Solution:
x = −10 x = −10
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation. 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. Note that by this we turn a predicate into an expression.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x|x*x=100} {x|x*x=100}
``` ```
%% Output %% Output
$\{-10,10\}$ $\{-10,10\}$
{−10,10} {−10,10}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Substitutions (Statements) ### ### Substitutions (Statements) ###
B also has a rich syntax for **substitutions**, aka statements. B also has a rich syntax for **substitutions**, aka statements.
For example ```x := x+1``` increments the value of x by 1. For example ```x := x+1``` increments the value of x by 1.
Other constructs are WHILE loops and CASE statements. Other constructs are WHILE loops and CASE statements.
We will not talk about substitutions in the rest of this presentation. We will not talk about substitutions in the rest of this presentation.
But B can provide a nice mixture of **functional programming**, **constraint programming** and **imperative programming**, with precise proof rules rooted in logic. But B can provide a nice mixture of **functional programming**, **constraint programming** and **imperative programming**, with precise proof rules rooted in logic.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Definition of Constraint Solving ## ## 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. 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```. We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.
The following is an unsatisfiable predicate: The following is an unsatisfiable predicate:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint #x.(x:NATURAL & x*x=1000) :prettyprint #x.(x:NATURAL & x*x=1000)
``` ```
%% Output %% Output
$\exists \mathit{x}\cdot (\mathit{x} \in \mathbb N \wedge \mathit{x} * \mathit{x} = 1000)$ $\exists \mathit{x}\cdot (\mathit{x} \in \mathbb N \wedge \mathit{x} * \mathit{x} = 1000)$
∃x·(x ∈ ℕ ∧ x * x = 1000) ∃x·(x ∈ ℕ ∧ x * x = 1000)
%% Cell type:markdown id: tags: %% 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. 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: %% Cell type:markdown id: tags:
## Constraint Solving Applications ## ## Constraint Solving Applications ##
Constraint solving has many applications in formal methods in general and B in particular: Constraint solving has many applications in formal methods in general and B in particular:
* Animation, in particular dealing with implict specifications to determine parameters * Animation, in particular dealing with implict specifications to determine parameters
* Test-case generation * Test-case generation
* Bounded Model Checking * Bounded Model Checking
* Disprover and prover * Disprover and prover
* Enabling analysis (determining implicit control flow) * Enabling analysis (determining implicit control flow)
and many more and many more
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
As no counter example has been found, we can in this case establish the goal to be proven. As no counter example has been found, we can in this case establish the goal to be proven.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Modelling and Solving Problems in B ### ### Modelling and Solving Problems in B ###
Obviously, we can also use constraint solving in B to solve puzzles or real-life problems. Obviously, we can also use constraint solving in B to solve puzzles or real-life problems.
In other words, we use B as way to express constraint problems in almost pure mathematics. In other words, we use B as way to express constraint problems in almost pure mathematics.
#### Send More Money Puzzle #### #### Send More Money Puzzle ####
We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits: We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` 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 & :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 S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y
``` ```
%% Output %% 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}$ $\{\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 {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: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 & {S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 & card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y M*10000 + O*1000 + N*100 + E*10 + Y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{R} = 8$ * $\mathit{R} = 8$
* $\mathit{S} = 9$ * $\mathit{S} = 9$
* $\mathit{D} = 7$ * $\mathit{D} = 7$
* $\mathit{E} = 5$ * $\mathit{E} = 5$
* $\mathit{Y} = 2$ * $\mathit{Y} = 2$
* $\mathit{M} = 1$ * $\mathit{M} = 1$
* $\mathit{N} = 6$ * $\mathit{N} = 6$
* $\mathit{O} = 0$ * $\mathit{O} = 0$
TRUE TRUE
Solution: Solution:
R = 8 R = 8
S = 9 S = 9
D = 7 D = 7
E = 5 E = 5
Y = 2 Y = 2
M = 1 M = 1
N = 6 N = 6
O = 0 O = 0
%% Cell type:markdown id: tags: %% 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: 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: %% Cell type:code id: tags:
``` prob ``` prob
{S,E,N,D, M,O,R, Y | {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & {S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 & card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y } M*10000 + O*1000 + N*100 + E*10 + Y }
``` ```
%% Output %% Output
$\{(((((((9\mapsto 5)\mapsto 6)\mapsto 7)\mapsto 1)\mapsto 0)\mapsto 8)\mapsto 2)\}$ $\{(((((((9\mapsto 5)\mapsto 6)\mapsto 7)\mapsto 1)\mapsto 0)\mapsto 8)\mapsto 2)\}$
{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)} {(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table {S,E,N,D, M,O,R, Y | :table {S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & {S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 & card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D + S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E = M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y } M*10000 + O*1000 + N*100 + E*10 + Y }
``` ```
%% Output %% Output
|S|E|N|D|M|O|R|Y| |S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---| |---|---|---|---|---|---|---|---|
|$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$| |$9$|$5$|$6$|$7$|$1$|$0$|$8$|$2$|
S E N D M O R Y S E N D M O R Y
9 5 6 7 1 0 8 2 9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### KISS PASSION Puzzle#### #### KISS PASSION Puzzle####
A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem. A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{K,P} <: 1..9 & {K,P} ⊆ 1..9 &
{I,S,A,O,N} <: 0..9 & {I,S,A,O,N} ⊆ 0..9 &
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) (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 & = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &
card({K, I, S, P, A, O, N}) = 7 card({K, I, S, P, A, O, N}) = 7
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $P = 4$ * $P = 4$
* $A = 1$ * $A = 1$
* $S = 3$ * $S = 3$
* $I = 0$ * $I = 0$
* $K = 2$ * $K = 2$
* $N = 9$ * $N = 9$
* $O = 8$ * $O = 8$
TRUE TRUE
Solution: Solution:
P = 4 P = 4
A = 1 A = 1
S = 3 S = 3
I = 0 I = 0
K = 2 K = 2
N = 9 N = 9
O = 8 O = 8
%% Cell type:code id: tags:
``` prob
:table {K,I,S,P,A,O,N | {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
|K|I|S|P|A|O|N|
|---|---|---|---|---|---|---|
|$2$|$0$|$3$|$4$|$1$|$8$|$9$|
K I S P A O N
2 0 3 4 1 8 9
%% Cell type:markdown id: tags: %% 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: 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: %% Cell type:code id: tags:
``` prob ``` prob
x <: 1..5 & SIGMA(y).(y:x|y)=14 x <: 1..5 & SIGMA(y).(y:x|y)=14
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = \{2,3,4,5\}$ * $x = \{2,3,4,5\}$
TRUE TRUE
Solution: Solution:
x = {2,3,4,5} x = {2,3,4,5}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The well known n Queens problem can be solved as follows: The well known n Queens problem can be solved as follows:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve prob n=8 & :time :solve prob n=8 &
queens : perm(1..n) & queens ∈ perm(1..n) &
∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2)) ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))
``` ```
%% Output %% Output
Execution time: 0.020736936 seconds Execution time: 0.113811662 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{queens} = \{(1\mapsto 1),(2\mapsto 5),(3\mapsto 8),(4\mapsto 6),(5\mapsto 3),(6\mapsto 7),(7\mapsto 2),(8\mapsto 4)\}$ * $\mathit{queens} = \{(1\mapsto 1),(2\mapsto 5),(3\mapsto 8),(4\mapsto 6),(5\mapsto 3),(6\mapsto 7),(7\mapsto 2),(8\mapsto 4)\}$
* $\mathit{n} = 8$ * $\mathit{n} = 8$
TRUE TRUE
Solution: Solution:
queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)} queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)}
n = 8 n = 8
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Mixing Functional Programming with Constraint Programming ### ### Mixing Functional Programming with Constraint Programming ###
In B we can also define (higher-order) functions and mix those with logical predicates. In B we can also define (higher-order) functions and mix those with logical predicates.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
f = %x.(x:INTEGER|x*x) & // this is an infinite function f = %x.(x:INTEGER|x*x) & // this is an infinite function
r1 = f(100000) & r1 = f(100000) &
r2 = f[1..10] & r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) & // relational composition ; corresponds to map r3 = ([2,3,5,7,11] ; f) & // relational composition ; corresponds to map
r4 = iterate(f,3)(2) & // we can apply the iteration or transitive closure operators r4 = iterate(f,3)(2) & // we can apply the iteration or transitive closure operators
f(sqrt) = 100 // compute the square root of 100 f(sqrt) = 100 // compute the square root of 100
``` ```
%% Output %% Output
$\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\mathit{TRUE}$ $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{r2} = \{1,4,9,16,25,36,49,64,81,100\}$ * $\mathit{r2} = \{1,4,9,16,25,36,49,64,81,100\}$
* $\mathit{r3} = [4,9,25,49,121]$ * $\mathit{r3} = [4,9,25,49,121]$
* $\mathit{r4} = 256$ * $\mathit{r4} = 256$
* $\mathit{sqrt} = 10$ * $\mathit{sqrt} = 10$
* $\mathit{f} = \lambda \mathit{x}\qdot(\mathit{x} \in \mathit{INTEGER}\mid \mathit{x} * \mathit{x})$ * $\mathit{f} = \lambda \mathit{x}\qdot(\mathit{x} \in \mathit{INTEGER}\mid \mathit{x} * \mathit{x})$
* $\mathit{r1} = 10000000000$ * $\mathit{r1} = 10000000000$
TRUE TRUE
Solution: Solution:
r2 = {1,4,9,16,25,36,49,64,81,100} r2 = {1,4,9,16,25,36,49,64,81,100}
r3 = [4,9,25,49,121] r3 = [4,9,25,49,121]
r4 = 256 r4 = 256
sqrt = 10 sqrt = 10
f = λx·(x ∈ INTEGER∣x ∗ x) f = λx·(x ∈ INTEGER∣x ∗ x)
r1 = 10000000000 r1 = 10000000000
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r1 = f(100000) & r1 = f(100000) &
r2 = f[1..10] & r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) & r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) & r4 = iterate(f,3)(2) &
f(sqr) = 100 & f(sqr) = 100 &
r5 = closure1(f)[{10000}] r5 = closure1(f)[{10000}]
``` ```
%% Output %% Output
$\newcommand{\cprod}{\mathbin\times}\newcommand{\cprod}{\mathbin\times}\mathit{TRUE}$ $\newcommand{\cprod}{\mathbin\times}\newcommand{\cprod}{\mathbin\times}\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{r2} = \{1,2,3,4\}$ * $\mathit{r2} = \{1,2,3,4\}$
* $\mathit{r3} = [2,2,3,3,4]$ * $\mathit{r3} = [2,2,3,3,4]$
* $\mathit{r4} = 2$ * $\mathit{r4} = 2$
* $\mathit{r5} = \{2,4,10,100\}$ * $\mathit{r5} = \{2,4,10,100\}$
* $\mathit{sqr} = 9802$ * $\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{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$ * $\mathit{r1} = 317$
TRUE TRUE
Solution: Solution:
r2 = {1,2,3,4} r2 = {1,2,3,4}
r3 = [2,2,3,3,4] r3 = [2,2,3,3,4]
r4 = 2 r4 = 2
r5 = {2,4,10,100} r5 = {2,4,10,100}
sqr = 9802 sqr = 9802
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x} f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
r1 = 317 r1 = 317
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## How to solve (set) constraints in B ## ## How to solve (set) constraints in B ##
We will now examine how one can perform constraint solving for B. We will now examine how one can perform constraint solving for B.
ProB has three main solving backends ProB has three main solving backends
* the default solver using CLP(FD) and Prolog co-routines * the default solver using CLP(FD) and Prolog co-routines
* a SAT-based solver, using the Kodkod API of Alloy * a SAT-based solver, using the Kodkod API of Alloy
* an SMT-based solver, using Z3 or CVC4 * an SMT-based solver, using Z3 or CVC4
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve prob n=20 & :time :solve prob n=20 &
queens : perm(1..n) & queens : perm(1..n) &
∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2)) ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))
``` ```
%% Output %% Output
Execution time: 0.036815957 seconds Execution time: 0.036815957 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{queens} = \{(1\mapsto 1),(2\mapsto 3),(3\mapsto 5),(4\mapsto 14),(5\mapsto 17),(6\mapsto 4),(7\mapsto 16),(8\mapsto 7),(9\mapsto 12),(10\mapsto 18),(11\mapsto 15),(12\mapsto 19),(13\mapsto 6),(14\mapsto 10),(15\mapsto 20),(16\mapsto 11),(17\mapsto 8),(18\mapsto 2),(19\mapsto 13),(20\mapsto 9)\}$ * $\mathit{queens} = \{(1\mapsto 1),(2\mapsto 3),(3\mapsto 5),(4\mapsto 14),(5\mapsto 17),(6\mapsto 4),(7\mapsto 16),(8\mapsto 7),(9\mapsto 12),(10\mapsto 18),(11\mapsto 15),(12\mapsto 19),(13\mapsto 6),(14\mapsto 10),(15\mapsto 20),(16\mapsto 11),(17\mapsto 8),(18\mapsto 2),(19\mapsto 13),(20\mapsto 9)\}$
* $\mathit{n} = 20$ * $\mathit{n} = 20$
TRUE TRUE
Solution: Solution:
queens = {(1↦1),(2↦3),(3↦5),(4↦14),(5↦17),(6↦4),(7↦16),(8↦7),(9↦12),(10↦18),(11↦15),(12↦19),(13↦6),(14↦10),(15↦20),(16↦11),(17↦8),(18↦2),(19↦13),(20↦9)} queens = {(1↦1),(2↦3),(3↦5),(4↦14),(5↦17),(6↦4),(7↦16),(8↦7),(9↦12),(10↦18),(11↦15),(12↦19),(13↦6),(14↦10),(15↦20),(16↦11),(17↦8),(18↦2),(19↦13),(20↦9)}
n = 20 n = 20
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve kodkod n=13 & :time :solve kodkod n=13 &
queens : 1..n >-> 1..n & 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)) ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))
``` ```
%% Output %% Output
Execution time: 1.417787341 seconds Execution time: 1.417787341 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{queens} = \{(3\mapsto 4),(5\mapsto 10),(6\mapsto 3),(7\mapsto 5),(9\mapsto 1),(10\mapsto 6),(11\mapsto 2),(12\mapsto 12),(13\mapsto 8),(1\mapsto 7),(2\mapsto 9),(4\mapsto 13),(8\mapsto 11)\}$ * $\mathit{queens} = \{(3\mapsto 4),(5\mapsto 10),(6\mapsto 3),(7\mapsto 5),(9\mapsto 1),(10\mapsto 6),(11\mapsto 2),(12\mapsto 12),(13\mapsto 8),(1\mapsto 7),(2\mapsto 9),(4\mapsto 13),(8\mapsto 11)\}$
* $\mathit{n} = 13$ * $\mathit{n} = 13$
TRUE TRUE
Solution: Solution:
queens = {(3↦4),(5↦10),(6↦3),(7↦5),(9↦1),(10↦6),(11↦2),(12↦12),(13↦8),(1↦7),(2↦9),(4↦13),(8↦11)} queens = {(3↦4),(5↦10),(6↦3),(7↦5),(9↦1),(10↦6),(11↦2),(12↦12),(13↦8),(1↦7),(2↦9),(4↦13),(8↦11)}
n = 13 n = 13
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve z3 n=8 & :time :solve z3 n=8 &
queens : perm(1..n) & queens : perm(1..n) &
∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 => queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2)) ∀(q1,q2).(q1∈1..n & q2∈2..n & q2>q1 ⇒ queens(q1)+(q2-q1) ≠ queens(q2) & queens(q1)+(q1-q2) ≠ queens(q2))
``` ```
%% Output %% Output
:time: :solve: Computation not completed: no solution found (but one might exist) :time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Result for KISS*KISS=PASSION puzzle: Result for KISS*KISS=PASSION puzzle:
Solver | Runtime Solver | Runtime
-------|------- -------|-------
ProB Default | 0.01 sec ProB Default | 0.01 sec
Kodkod Backend | 1 sec Kodkod Backend | 1 sec
Z3 Backend | ? > 100 sec Z3 Backend | ? > 100 sec
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Unbounded integers ### ### Unbounded integers ###
The SAT translation via Kodkod/Alloy requires to determine the bid width. The SAT translation via Kodkod/Alloy requires to determine the bid width.
It cannot be applied to unbounded integers. 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). 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. 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**. 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. 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: Let us perform some experiments. Both ProB and Z3 can solve the following:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x*x=100 :solve z3 x*x=100
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = -10$ * $x = -10$
TRUE TRUE
Solution: Solution:
x = −10 x = −10
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Here is an example where ProB generates an enumeration warning, but finds a solution: Here is an example where ProB generates an enumeration warning, but finds a solution:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x>100 & x mod 2000 = 1 & x mod 3000 = 1 x>100 & x mod 2000 = 1 & x mod 3000 = 1
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = 6001$ * $x = 6001$
TRUE TRUE
Solution: Solution:
x = 6001 x = 6001
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 :solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = 6001$ * $x = 6001$
TRUE TRUE
Solution: Solution:
x = 6001 x = 6001
%% Cell type:markdown id: tags: %% 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. 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: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0 :solve prob x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
``` ```
%% Output %% Output
:solve: Computation not completed: no solution found (but one might exist) :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0 :solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = 6756001$ * $x = 6756001$
TRUE TRUE
Solution: Solution:
x = 6756001 x = 6756001
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation. 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**. ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x>y & y>x :solve z3 x>y & y>x
``` ```
%% Output %% Output
$FALSE$ $FALSE$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob x>y &y>x :solve prob x>y &y>x
``` ```
%% Output %% Output
:solve: Computation not completed: no solution found (but one might exist) :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Summary for Integer Arithmetic ### ### Summary for Integer Arithmetic ###
Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded) Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded)
------|------------|---------------|--- ------|------------|---------------|---
ProB CLP(FD) | yes | very good | limited with CHR ProB CLP(FD) | yes | very good | limited with CHR
ProB Z3 | yes | reasonable | very good ProB Z3 | yes | reasonable | very good
ProB Kodkod | no | good | - ProB Kodkod | no | good | -
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Set Constraints ## ## Set Constraints ##
After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables. After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables.
### Translation to SAT ### ### Translation to SAT ###
The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements. 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, the sets x and y are translated to bit vectors of size 2 and set union is simple bitwise or: Take for example the following constraint, the sets x and y are translated to bit vectors of size 2 and set union is simple bitwise or:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve kodkod x <: 1..2 & y<: 1..2 & x \/ y = 1..2 & 1:x & x <<: y :solve kodkod x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y
``` ```
%% Output %% Output
$TRUE$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $x = \{1\}$ * $\mathit{x} = \{1\}$
* $y = \{1,2\}$ * $\mathit{y} = \{1,2\}$
TRUE TRUE
Solution: Solution:
x = {1} x = {1}
y = {1,2} y = {1,2}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Limitations of translating set constraints to SAT: 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 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 - 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: Given that:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(POW(1..100)) card(POW(1..100))
``` ```
%% Output %% Output
$1267650600228229401496703205376$ $1267650600228229401496703205376$
1267650600228229401496703205376 1267650600228229401496703205376
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376. translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x) x ⊆ POW(1..100) & {100}∈x & ∀y.(y∈x ⇒ {card(y)}:x)
``` ```
%% Output %% Output
$TRUE$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $x = \{\{100\},\{1\}\}$ * $\mathit{x} = \{\{100\},\{1\}\}$
TRUE TRUE
Solution: Solution:
x = {{100},{1}} x = {{100},{1}}
%% Cell type:markdown id: tags: %% 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). 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: %% Cell type:code id: tags:
``` prob ``` prob
{100}:x & !y.(y:x => (!z.(z:y => y \/ {z / 2}:x))) {100}∈x & ∀y.(y∈x ⇒ (∀z.(z∈y ⇒ y ∪ {z / 2}∈x)))
``` ```
%% Output %% Output
$TRUE$ $\mathit{TRUE}$
**Solution:** **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\}\}$ * $\mathit{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 TRUE
Solution: 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}} 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: %% Cell type:markdown id: tags:
However, when it is applicable the propositional encoding of sets can be very effective for SAT solvers. 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: The following example, involving various relational operators can currently only be solved by our Kodkod backend:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=4..5 :time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=4..5
``` ```
%% Output %% Output
Execution time: 0.097977646 seconds Execution time: 0.097977646 seconds
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $r = \{(3\mapsto5),(3\mapsto4),(5\mapsto5),(5\mapsto4),(1\mapsto4),(2\mapsto4),(4\mapsto4)\}$ * $r = \{(3\mapsto5),(3\mapsto4),(5\mapsto5),(5\mapsto4),(1\mapsto4),(2\mapsto4),(4\mapsto4)\}$
TRUE TRUE
Solution: Solution:
r = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)} r = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Translation to SMTLib ### ### Translation to SMTLib ###
This can in principle deal with higher-order sets and unbounded sets, but makes heavy use of quantifiers. 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. The practical usefulness is currently very limited.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 :solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = \emptyset$ * $x = \emptyset$
* $y = \{1,2\}$ * $y = \{1,2\}$
TRUE TRUE
Solution: Solution:
x = ∅ x = ∅
y = {1,2} y = {1,2}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Internally, the constraint is rewritten to support operators which do not exist in SMTLib: Internally, the constraint is rewritten to support operators which do not exist in SMTLib:
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Let us look at another relatively simple example which poses problems: Let us look at another relatively simple example which poses problems:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 f = {1|->3, 2|->6} & r = f~[{6}] :solve z3 f = {1|->3, 2|->6} & r = f~[{6}]
``` ```
%% Output %% Output
:solve: Computation not completed: no solution found (but one might exist) :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
To understand why this simple constraint cannot be solved, we have to know how the translation works: 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: The relational inverse gets translated into two universal quantifications for SMTLib:
``` ```
x = y~ x = y~
<=> <=>
!(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) & !(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) &
!(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x)) !(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x))
``` ```
Similarly, r = f[s] is translated as follows: Similarly, r = f[s] is translated as follows:
``` ```
r = f[s] r = f[s]
<=> <=>
!st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) & !st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) &
!st27.(#st26.(st26 |-> st27 : f & st26 : s) => st27 : r) !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). The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can).
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:prettyprint f = {(1|->3),(2|->6)} & :prettyprint f = {(1|->3),(2|->6)} &
#st13.(r = st13 & ( #st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) & !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))) !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
``` ```
%% Output %% 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})))$ $\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))) 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: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve prob f = {(1|->3),(2|->6)} & :time :solve prob f = {(1|->3),(2|->6)} &
#st13.(r = st13 & ( #st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) & !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))) !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
``` ```
%% Output %% Output
Execution time: 0.140791514 seconds Execution time: 0.140791514 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{r} = \{2\}$ * $\mathit{r} = \{2\}$
* $\mathit{f} = \{(1\mapsto 3),(2\mapsto 6)\}$ * $\mathit{f} = \{(1\mapsto 3),(2\mapsto 6)\}$
TRUE TRUE
Solution: Solution:
r = {2} r = {2}
f = {(1↦3),(2↦6)} f = {(1↦3),(2↦6)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve cvc4 f = {(1|->3),(2|->6)} & :time :solve cvc4 f = {(1|->3),(2|->6)} &
#st13.(r = st13 & ( #st13.(r = st13 & (
!st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 &
(!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) &
!(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) &
!st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) & !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))) !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))
``` ```
%% Output %% Output
:time: :solve: Computation not completed: no solution found (but one might exist) :time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
The SMTLib translation is still of limited value for finding models. 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. 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: While both ProB and Z3 can solve the following:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob x:s1 & x:s2 & x /: (s1 /\ s2) & s1 <: INTEGER :solve prob x:s1 & x:s2 & x /: (s1 /\ s2) & s1 <: INTEGER
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
only the Z3 backend can solve this one: only the Z3 backend can solve this one:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x:s1 & x/:s2 & x /: (s1 \/s2) & s1 <: INTEGER :solve z3 x:s1 & x/:s2 & x /: (s1 \/s2) & s1 <: INTEGER
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### ProB's Set Solver ### ### ProB's Set Solver ###
ProB has actually three set representations: ProB has actually three set representations:
- Prolog lists of elements - Prolog lists of elements
- AVL trees for fully known sets - AVL trees for fully known sets
- symbolic closures for large or infinite sets - symbolic closures for large or infinite sets
For finite sets, the AVL tree representation is the most efficient and allows for efficient lookups. 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. It, however, requires all elements to be fully known.
The symbolic closure can be used for large or infinite sets. 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. 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. The list representation is used for sets where some of the members are known or partially known.
#### AVL tree representation #### #### AVL tree representation ####
The following generates the AVL tree representation: The following generates the AVL tree representation:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x|x∈0..2**10 & x mod 100 = 0} {x|x∈0..2**10 & x mod 100 = 0}
``` ```
%% Output %% Output
$\{0,100,200,300,400,500,600,700,800,900,1000\}$ $\{0,100,200,300,400,500,600,700,800,900,1000\}$
{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: %% Cell type:markdown id: tags:
#### Symbolic closure representation #### #### Symbolic closure representation ####
In the following case, ProB knows that the set is infinite and is kept symbolic: In the following case, ProB knows that the set is infinite and is kept symbolic:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x|x>1000} {x|x>1000}
``` ```
%% Output %% Output
$\{\mathit{x}\mid \mathit{x} > 1000\}$ $\{\mathit{x}\mid \mathit{x} > 1000\}$
{x∣x > 1000} {x∣x > 1000}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Symbolic sets can be used in various ways: Symbolic sets can be used in various ways:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf inf = {x|x>1000} & 1024 : inf & not(1000:inf) & res = (900..1100) ∩ inf
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{inf} = \{\mathit{x}\mid \mathit{x} > 1000\}$ * $\mathit{inf} = \{\mathit{x}\mid \mathit{x} > 1000\}$
* $\mathit{res} = (1001 \ldots 1100)$ * $\mathit{res} = (1001 \ldots 1100)$
TRUE TRUE
Solution: Solution:
inf = {x∣x > 1000} inf = {x∣x > 1000}
res = (1001 ‥ 1100) res = (1001 ‥ 1100)
%% Cell type:markdown id: tags: %% 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: 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) - closure(Parameters,Types,CompiledPredicate)
For example, a set {x|x>v} where v has the value 17 is compiled to: For example, a set {x|x>v} where v has the value 17 is compiled to:
- closure([x],[integer],```x>17```) - closure([x],[integer],```x>17```)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### List representation #### #### List representation ####
The list representation is used when a finite set is partially known and constraint solving has to determine the set. 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: %% Cell type:code id: tags:
``` prob ``` prob
vec: 1..10 --> 0..9999 & vec: 1..10 --> 0..9999 &
vec(1) : {1,10} & vec(1) : {1,10} &
!x.(x:2..10 => vec(x) = vec(x-1)*2) !x.(x:2..10 => vec(x) = vec(x-1)*2)
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $vec = \{(1\mapsto1),(2\mapsto2),(3\mapsto4),(4\mapsto8),(5\mapsto16),(6\mapsto32),(7\mapsto64),(8\mapsto128),(9\mapsto256),(10\mapsto512)\}$ * $vec = \{(1\mapsto1),(2\mapsto2),(3\mapsto4),(4\mapsto8),(5\mapsto16),(6\mapsto32),(7\mapsto64),(8\mapsto128),(9\mapsto256),(10\mapsto512)\}$
TRUE TRUE
Solution: Solution:
vec = {(1↦1),(2↦2),(3↦4),(4↦8),(5↦16),(6↦32),(7↦64),(8↦128),(9↦256),(10↦512)} 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: %% Cell type:markdown id: tags:
Note that Kodkod translation and SMT translation not very effective for the above. Note that Kodkod translation and SMT translation not very effective for the above.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### ProB's Solving Algorithm ### ### ProB's Solving Algorithm ###
ProB tries to accomplish several conflicting goals: 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 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 deal with symbolic, infinite sets, relations and functions.
- being able to perform efficient computation over large data as well as constraint solving - 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: For example, efficient computation over large concrete data is the following:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` 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 :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 %% Output
Execution time: 0.716030873 seconds Execution time: 0.716030873 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{s3} = \#500\in\{20,40,\ldots,9980,10000\}$ * $\mathit{s3} = \#500\in\{20,40,\ldots,9980,10000\}$
* $\mathit{n} = 4$ * $\mathit{n} = 4$
* $\mathit{s1} = \#2500\in\{4,8,\ldots,9996,10000\}$ * $\mathit{s1} = \#2500\in\{4,8,\ldots,9996,10000\}$
* $\mathit{s2} = \#2000\in\{5,10,\ldots,9995,10000\}$ * $\mathit{s2} = \#2000\in\{5,10,\ldots,9995,10000\}$
TRUE TRUE
Solution: Solution:
s3 = #500∈{20,40,…,9980,10000} s3 = #500∈{20,40,…,9980,10000}
n = 4 n = 4
s1 = #2500∈{4,8,…,9996,10000} s1 = #2500∈{4,8,…,9996,10000}
s2 = #2000∈{5,10,…,9995,10000} s2 = #2000∈{5,10,…,9995,10000}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Here is a simple verison of the above Here is a simple verison of the above
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In the appendix there are more examples which analyse the performance for such examples. In the appendix there are more examples which analyse the performance for such examples.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
ProB employs the *Andorra* principle: deterministic computations are done first. ProB employs the *Andorra* principle: deterministic computations are done first.
As there are multiple set representations, there are actually two kinds of deterministic computations: 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 - deterministic computations that generate an efficient representation, e.g., an AVL set representation
- and other deterministic computations - and other deterministic computations
The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority. 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 0 means that an efficient representation can be generated
- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation - 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 - 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. 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. 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 #### #### Example ####
Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y``` is solved. Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y``` is solved.
- all constraints are registered - all constraints are registered
- in phase 0 ```n=100``` is run - in phase 0 ```n=100``` is run
- this means that ```1..n``` can be efficiently computed - this means that ```1..n``` can be efficiently computed
- this means that ```x = 1..n``` triggers in phase 0 - 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``` - 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 - this means that ```y = 2*n..3*n``` triggers in phase 0
- again, this means that ```x \/ y``` can be efficiently computed - again, this means that ```x \/ y``` can be efficiently computed
- finally ```xy = x \/ y``` can be executed in phase 0 - 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. No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### Dealing with unbounded enumeration #### #### 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. 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: %% Cell type:markdown id: tags:
## Summary of Set Constraint Solving Approaches ## ## Summary of Set Constraint Solving Approaches ##
- SAT Translation (Kodkod backend): - SAT Translation (Kodkod backend):
- needs finite and small base type, no unbounded or higher-order sets - needs finite and small base type, no unbounded or higher-order sets
- can be very effective for complex constraints involving image, transitive closure,... - can be very effective for complex constraints involving image, transitive closure,...
- limited performance for large sets - limited performance for large sets
- SMTLib Translation (Z3/CVC4 backend): - SMTLib Translation (Z3/CVC4 backend):
- can deal with unbounded and large sets - 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 - due to heavy use of quantifiers, some finite constraints get translated into infinite ones: limited model finding capabilities
- ProB's default backend: - ProB's default backend:
- can deal with unbounded and large sets - can deal with unbounded and large sets
- limited constraint solving for complex constraints involving image, transitive closure,... - limited constraint solving for complex constraints involving image, transitive closure,...
- no learning, backjumping - no learning, backjumping
- works well for large sets and semi-deterministic computation - works well for large sets and semi-deterministic computation
- works well for animation, data validation, disproving - works well for animation, data validation, disproving
- limitations appear for symbolic model checking (IC3,...) - 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) - 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 - CHR: can complement ProB's default backend
- currently only very limited propagations (>, >=, x=y+c, ...) - currently only very limited propagations (>, >=, x=y+c, ...)
- very difficult to control and avoid propagation loops - very difficult to control and avoid propagation loops
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Integrations of Approaches ### ### Integrations of Approaches ###
ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```. 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. 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 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. 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). 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. A more promising, fine-grained integration has been presented at PADL'18.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Appendix ## ## Appendix ##
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
### Explicit Computations #### ### Explicit Computations ####
What about explicit computations? How well does the SMTLib translation fare here? What about explicit computations? How well does the SMTLib translation fare here?
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 x = 1..1000 /\ (200..300) :solve z3 x = 1..1000 /\ (200..300)
``` ```
%% Output %% Output
:solve: Computation not completed: no solution found (but one might exist) :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve z3 x = 1..40 /\ (6..15) :time :solve z3 x = 1..40 /\ (6..15)
``` ```
%% Output %% Output
Execution time: 0.224425596 seconds Execution time: 0.224425596 seconds
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$ * $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE TRUE
Solution: Solution:
x = {6,7,8,9,10,11,12,13,14,15} x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve z3 x = 1..60 /\ (6..15) :time :solve z3 x = 1..60 /\ (6..15)
``` ```
%% Output %% Output
Execution time: 1.149180308 seconds Execution time: 1.149180308 seconds
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = \{6,7,8,9,10,11,12,13,14,15\}$ * $x = \{6,7,8,9,10,11,12,13,14,15\}$
TRUE TRUE
Solution: Solution:
x = {6,7,8,9,10,11,12,13,14,15} x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve z3 x = 1..80 /\ (6..15) :time :solve z3 x = 1..80 /\ (6..15)
``` ```
%% Output %% Output
:time: :solve: Computation not completed: no solution found (but one might exist) :time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve prob x = 1..80 /\ (6..15) :time :solve prob x = 1..80 /\ (6..15)
``` ```
%% Output %% Output
Execution time: 0.005873811 seconds Execution time: 0.005873811 seconds
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $x = (6 \ldots 15)$ * $x = (6 \ldots 15)$
TRUE TRUE
Solution: Solution:
x = (6 ‥ 15) x = (6 ‥ 15)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In the following the inverse operator seems to pose problems to Z3: In the following the inverse operator seems to pose problems to Z3:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve z3 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}] :solve z3 s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]
``` ```
%% Output %% Output
:solve: Computation not completed: no solution found (but one might exist) :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}] :solve prob s1 = {2,3,5,7,11} & s2 = {4,8,16,32} & c = s1*s2 & r=c~[{8}]
``` ```
%% Output %% Output
$TRUE$ $TRUE$
**Solution:** **Solution:**
* $r = \{2,3,5,7,11\}$ * $r = \{2,3,5,7,11\}$
* $c = (\{2,3,5,7,11\} * \{4,8,16,32\})$ * $c = (\{2,3,5,7,11\} * \{4,8,16,32\})$
* $s1 = \{2,3,5,7,11\}$ * $s1 = \{2,3,5,7,11\}$
* $s2 = \{4,8,16,32\}$ * $s2 = \{4,8,16,32\}$
TRUE TRUE
Solution: Solution:
r = {2,3,5,7,11} r = {2,3,5,7,11}
c = ({2,3,5,7,11} ∗ {4,8,16,32}) c = ({2,3,5,7,11} ∗ {4,8,16,32})
s1 = {2,3,5,7,11} s1 = {2,3,5,7,11}
s2 = {4,8,16,32} s2 = {4,8,16,32}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
#### Datavalidation example #### #### Datavalidation example ####
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE MACHINE
signals signals
SETS SETS
/* Ensemble des signaux */ /* Ensemble des signaux */
SIGNAL = SIGNAL =
{ PL01 { PL01
, PL02 , PL02
, PL03 , PL03
, PL04 , PL04
, PL05 , PL05
, PL06 , PL06
, PL07 , PL07
, PL08 , PL08
, PL09 , PL09
, PL10 , PL10
, PL11 , PL11
, PL12 , PL12
, PL13 , PL13
, PL14 , PL14
, PL15 , PL15
, PL16 , PL16
, PL17 , PL17
, PL18 , PL18
, PL19 , PL19
, PL20 , PL20
} }
END END
``` ```
%% Output %% Output
Loaded machine: signals Loaded machine: signals
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve prob nxt = :time :solve prob nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05, {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09, PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13, PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17, PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} & PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL] res = SIGNAL \ nxt[SIGNAL]
``` ```
%% Output %% Output
Execution time: 0.199987519 seconds Execution time: 0.199987519 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{res} = \{\mathit{PL01},\mathit{PL12}\}$ * $\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})\}$ * $\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 TRUE
Solution: Solution:
res = {PL01,PL12} 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)} 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: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve z3 nxt = :time :solve z3 nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05, {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09, PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13, PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17, PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} & PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL] res = SIGNAL \ nxt[SIGNAL]
``` ```
%% Output %% Output
:time: :solve: Computation not completed: no solution found (but one might exist) :time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:time :solve kodkod nxt = :time :solve kodkod nxt =
{PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05, {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,
PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09, PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,
PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13, PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL11, PL12 |-> PL13,
PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17, PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,
PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} & PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20} &
res = SIGNAL \ nxt[SIGNAL] res = SIGNAL \ nxt[SIGNAL]
``` ```
%% Output %% Output
Execution time: 0.789322780 seconds Execution time: 0.789322780 seconds
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{res} = \{\mathit{PL01},\mathit{PL12}\}$ * $\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})\}$ * $\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 TRUE
Solution: Solution:
res = {PL01,PL12} 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)} 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: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment