"We will not talk about substitutions in the rest of this presentation."
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"## Constraint Solving ##\n",
"\n",
"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.\n",
"We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.\n",
"The following is an unsatisfiable predicate:"
]
},
{
"cell_type": "code",
"execution_count": 31,
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
"outputs": [
{
"data": {
"text/plain": [
"FALSE"
]
},
"execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"x*x=1000"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"# Constraint solving has many applications in formal methods in general and B in particular.\n",
"It is required to animate implicit specifications.\n",
"Take for example an event\n",
"```\n",
"train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &\n",
"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:"
"Suppose that we have the invariant, ```train_position:TRAINS-->1..10000``` we can check whether the event is feasible in at least one valid state by solving:"
"Finally, a simple puzzle involving sets is to find a subset of numbers from 1..5 whose sum is 14:"
]
},
{
"cell_type": "code",
"execution_count": 48,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tx = {2,3,4,5}"
]
},
"execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"x <: 1..5 & SIGMA(y).(y:x|y)=14"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"## How to solve (set) constraints in B ##"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Booleans ###\n",
"\n",
"If we have only booleans, constraint solving is equivalent to SAT solving.\n",
"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.\n",
"\n",
"#### Knights and Knave Puzzle####\n",
"Here is a puzzle from Smullyan involving an island with only knights and knaves.\n",
"We know that:\n",
" - Knights: always tell the truth\n",
" - Knaves: always lie\n",
"\n",
"We are given the following information about three persons A,B,C on the island:\n",
" 1. A says: “B is a knave or C is a knave”\n",
" 2. B says “A is a knight”\n",
"\n",
"What are A, B and C?\n",
"Note: we model A,B,C as boolean variables which are equal to TRUE if they are a knight and FALSE if they are a knave."
]
},
{
"cell_type": "code",
"execution_count": 49,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tA = TRUE\n",
"\tB = TRUE\n",
"\tC = FALSE"
]
},
"execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
" (A=TRUE <=> (B=FALSE or C=FALSE)) & // Sentence 1\n",
" (B=TRUE <=> A=TRUE) // Sentence 2"
]
},
{
"cell_type": "code",
"execution_count": null,
...
...
%% Cell type:markdown id: tags:
## Introduction to B ##
%% Cell type:markdown id: tags:
### Basic Datavalues ###
%% Cell type:markdown id: tags:
B provides the booleans, strings and integers as built-in datatypes.
%% Cell type:code id: tags:
``` prob
BOOL
```
%% Output
{FALSE,TRUE}
%% Cell type:code id: tags:
``` prob
"this is a string"
```
%% Output
"this is a string"
%% Cell type:code id: tags:
``` prob
1024
```
%% Output
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.
[2018-05-25 13:12:43,407, T+1178229] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54757
[2018-05-25 13:12:43,408, T+1178230] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 94534
B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
ran({(thomas↦1),(gordon↦2)})
```
%% Output
{1,2}
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Output
1
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Output
{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
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
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
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}
%% 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.
%% Cell type:markdown id: tags:
## 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
x*x=1000
```
%% Output
FALSE
%% Cell type:markdown id: tags:
# Constraint solving has many applications in formal methods in general and B in particular.
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:
Suppose that we have the invariant, ```train_position:TRAINS-->1..10000``` we can check whether the event is feasible in at least one valid state by solving:
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}
%% Cell type:markdown id: tags:
## How to solve (set) constraints in 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.
#### Knights and Knave Puzzle####
Here is a puzzle from Smullyan involving an island with only knights and knaves.
We know that:
- Knights: always tell the truth
- Knaves: always lie
We are given the following information about three persons A,B,C on the island:
1. A says: “B is a knave or C is a knave”
2. B says “A is a knight”
What are A, B and C?
Note: we model A,B,C as boolean variables which are equal to TRUE if they are a knight and FALSE if they are a knave.
