Skip to content
Snippets Groups Projects
Commit 85a4d60d authored by dgelessus's avatar dgelessus
Browse files

Remove modelling examples in favor of https://prob.hhu.de/w/ 

These examples can be found in nearly identical form on the wiki.
parent dccded69
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 3522 deletions
config.yaml
+ 0
− 9
View file @ 85a4d60d
......@@ -7,12 +7,3 @@ authors:
- Michael Leuschel
content:
- user
---
file: modelling_examples.adoc
title: Modelling Examples
authors:
- Jens Bendisposto
- Joy Clark
- Michael Leuschel
content:
- model_examples
src/docs/chapter/model_examples/00_section_header.adoc deleted 100644 → 0
+ 0
− 3
View file @ dccded69
[[modelling-examples]]
= Modelling Examples
:leveloffset: +1
src/docs/chapter/model_examples/Apples_and_Oranges_(Apple_Interview_Question).adoc deleted 100644 → 0
+ 0
− 85
View file @ dccded69
[[apples-and-oranges]]
= Apples and Oranges
This puzzle is
https://bgr.com/2015/11/20/apple-interview-questions/[apparently an
Interview question at Apple]. Quoting from
https://bgr.com/2015/11/20/apple-interview-questions/[1] we have the
following information:
* (1) There are three boxes, one contains only apples, one contains only
oranges, and one contains both apples and oranges.
* (2) The boxes have been incorrectly labeled such that no label
identifies the actual contents of the box it labels.
* (3) Opening just one box, and without looking in the box, you take out
one piece of fruit.
* (4) By looking at the fruit, how can you immediately label all of the
boxes correctly?
Here is one encoding of this puzzle in B:
....
MACHINE ApplesOranges
SETS
Fruit={apple,orange}; // possible content for the boxes
Label={A,O,Both} // labels for the boxes
CONSTANTS a,o,b, // a,o,b are the three boxes
Take, // which box should we open (the label of that box)
DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
PROPERTIES
a = {apple} & o={orange} & b={apple,orange} // (1)
&
Take : Label //3
&
DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
!label. ( // the decision function has to work for all allowed labelings
( label : {a,o,b} >->> Label &
label(a) /= A & label(o) /= O & label(b) /= Both // (2)
)
=>
!f.(f: label~(Take)
=> DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
)
)
END
....
We have abstracted the box of apples `a` by the set containing `apple`.
Ditto for `o` and `b`, which are abstracted by `{orange}` and
`{apple,orange}` respectively.
NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the
above model with its one-line comments. If you have an older version of
ProB, simply use the normal comments `/* ... */`.
Loading this model with ProB gives you just one solution (after less
than 10 ms):
image::ProB_ApplesOranges_Sol.png[]
As we can see, the only solution is to open the box labelled with
"Both". We can inspect the decision function by using the B REPL
(e.g., double click on the State Properties pane to open it):
....
>>>> DecisionFunction(apple)
{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
>>>> DecisionFunction(orange)
{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}
....
In other words, when we pick an apple out of the box labelled with
"Both", then it contains only apples and the box labelled "O"ranges
contains both apples and oranges. The box labelled "A"pples contains
just oranges. Similarly, if we pick up an orange out of the box labelled
with "Both", then it contains only oranges and the box labelled with
"A"pples contains contains both apples and oranges. The box labelled
"O"ranges contains just apples.
NOTE: You can inspect values or expressions in a tabular form, using the
command "Expression as Table..." in the Visualize->Formulas menu. If
you enter "DecisionFunction" as expression you will see the following
tabular representation:
image::ProB_ApplesOranges_Table.png[]
src/docs/chapter/model_examples/Argumentation_Theory.adoc deleted 100644 → 0
+ 0
− 210
View file @ dccded69
[[argumentation-theory]]
= Argumentation Theory
Below we try to model some concepts of argumentation theory in B. The
examples try to show that classical (monotonic) logic with set theory
can be used to model some aspects of argumentation theory quite
naturally, and that ProB can solve and visualise some problems in
argumentation theory. Alternative solutions are encoding arguments as
normal logic programs (with non-monotonic negation) and using answer set
solvers for problem solving.
The following model was inspired by a talk given by Claudia Schulz.
The model below represents the labelling of the arguments as a total
function from arguments to its status, which can either be in (the
argument is accepted), out (the argument is rejected), or undec (the
argument is undecided). The relation between the arguments is given in
the binary attacks relation.
In case you are new to B, you probably need to know the following
operators to understand the specification below (we als have a
<<summary-of-b-syntax,summary page about the B syntax>>):
* `x : S` specifies that x is an element of S
* `a|->b` represents the pair (a,b); note that a relation and function
in B is a set of pairs.
* `x|->y : R` hence specifies that x is mapped to y in relation R
* `!x.(P => Q)` denotes universal quantification over variable x
* `#x.(P & Q)` denotes existential quantification over variable x
* `A <--> B` denotes the set of relations from A to B
* `A --> B` denotes the set of total functions from A to B
* block comments are of the form `/* ... */` and line comments start
with `//` (be sure to use version 1.5.1 of ProB, e.g., from the
<<download,Nightly download site>> as line comments
were added recently to B)
....
MACHINE ArgumentationTotFun
SETS
ARGUMENTS={A,B,C,D,E};
STATUS = {in,out,undec}
CONSTANTS attacks, label
PROPERTIES
attacks : ARGUMENTS <-> ARGUMENTS /* which argument attacks which other argument */
&
label: ARGUMENTS --> {in,out,undec} & /* the labeling function */
// if an argument y is in any attacker must be out:
!(x,y).(x|->y:attacks => (label(y)=in => label(x)=out)) &
// if an argument x is in anything it attacks must be out:
!(x,y).(x|->y:attacks => (label(x)=in => label(y)=out)) &
//if an argument y is out it must be attacked by a valid argument:
!(y).(y:ARGUMENTS => (label(y)=out => #x.(x|->y:attacks & label(x)=in))) &
// if an argument y is undecided it must be attacked by an undecided argument:
!(y).(y:ARGUMENTS => (label(y)=undec => #x.(x|->y:attacks & label(x)=undec)))
&
// here we model one particular argumentation graph
// A = the sun will shine to day, B = we are in the UK, C = it is summer, D = there are only 10 days of sunshine per year, E = the BBC has forecast sun
attacks = {B|->A, C|->B, D|->C, E |-> B, E|->D}
END
....
Here is a screenshot of ProB Tcl/Tk after loading the model.
image::ProB_Argumentation_Screenshot1.png[]
You can see that there is only a single solution (solving time 10 ms),
as only a single SETUP_CONSTANTS line is available in the "Enabled
Operations" pane. Double-click on SETUP_CONSTANTS and then
INITIALISATION will give you the following result, where you can see the
solution in the "State Properties" pane:
image::ProB_Argumentation_Screenshot2.png[]
If you want to inspect the solution visually, you can select the
"Current State as Graph" command in the "States" submenu of the
"Visualize" menu:
image::ProB_Argumentation_VisCurStateAsGraph.png[]
This results in the following picture being displayed:
image::ProB_Argumentation_Dot.png[]
You can try and experiment with various attack graphs by editing the
file. E.g., with
`attacks = {B|->A, C|->B, D|->C, E |-> B, E|->D, D|->E}`
you now get three possible labelling, the last one assigns undec to all
arguments.
image::ProB_Argumentation_Dot1.png[]
image::ProB_Argumentation_Dot2.png[]
image::ProB_Argumentation_Dot3.png[]
[[a-more-elegant-encoding]]
== A more elegant encoding
The following is a slightly more elegant encoding, where we represent
the labelling as a partition of the arguments. This enables to use the
relational image operator to express some constraints more compactly.
This model is particularly well suited if you wish to use our
<<using-prob-with-kodkod,Kodkod backend>> which translates the
constraints to SAT. However, even the standard ProB solver can solve
this instance in 10 ms (Kodkod requires 70 ms), so this would only be
worthwhile for larger problem instances.
In case you are new to B, you probably need to know the following
additional operators to understand the specification below (we als have
a <<summary-of-b-syntax,summary page about the B syntax>>):
* `r~` is the inverse of a function or relation r
* `r[S]` is the relational image of a relation r for a set of domain
values S
....
MACHINE ArgumentationAsSets
SETS
ARGUMENTS={A,B,C,D,E}
CONSTANTS attacks, in,out,undec
PROPERTIES
attacks : ARGUMENTS <-> ARGUMENTS /* which argument attacks which other argument */
&
// we partition the arguments into three sets
ARGUMENTS = in \/ out \/ undec &
in /\ out = {} & in /\ undec = {} & out /\ undec = {} &
// if an argument is in, any attacker must be out:
attacks~[in] <: out &
// if an argument is in, anything it attacks must be out:
attacks[in] <: out &
//if an argument y is out, it must be attacked by a valid argument:
!y.(y:out => #x.(x|->y:attacks & x:in)) &
// if an argument y is undecided, it must be attacked by an undecided argument:
!y.(y:undec => #x.(x|->y:attacks & x:undec))
&
// here we model one particular argumentation graph
// A = the sun will shine to day, B = we are in the UK, C = it is summer, D = there are only 10 days of sunshine per year, E = the BBC has forecast sun
attacks = {B|->A, C|->B, D|->C, E |-> B, E|->D}
END
....
[[influencing-the-graphical-rendering]]
== Influencing the Graphical Rendering
One can influence the graphical representation of the current state in
various ways. The user can directly define nodes and edges of the graph
to be rendered. One way to do this is by adding the following lines
after the MACHINE section:
....
DEFINITIONS
CUSTOM_GRAPH_NODES == (in * {"green"}) \/ (out * {"red"}) \/ (undec * {"orange"});
CUSTOM_GRAPH_EDGES == attacks
....
These lines do not influence the meaning of the model; they are just
used by ProB. Indeed, one can then use the "Current State as Custom
Graph" command in the "States" submenu of the "Visualise" menu to
obtain the following rendering of the very first example above:
image::ProB_Argumentation_CustomDot.png[]
[[an-event-b-version-of-the-model]]
== An Event-B Version of the Model
Instead of using ProB Tcl/Tk you can also encode this model in Rodin,
the Eclipse-based platform for Event-B.
Here we have split the model into two contexts. The first one encodes
the general rules for labelling (we use Camille syntax):
....
context ArgumentsAsSets
sets ARGUMENTS
constants attacks in out undec
axioms
@axm1 attacks ∈ ARGUMENTS ↔ ARGUMENTS // which argument attacks which other argument
@axm2 partition(ARGUMENTS,in,out,undec) // we partition the arguments into three sets
@axm3 attacks∼[in] ⊆ out // if an argument is in, any attacker must be out
@axm4 attacks[in] ⊆ out // if an argument is in, anything it attacks must be out
@axm5 ∀y·(y∈out ⇒ ∃x·(x↦y∈attacks ∧ x∈in)) //if an argument y is out, it must be attacked by a valid argument
@axm6 ∀y·(y∈undec ⇒ ∃x·(x↦y∈attacks ∧ x∈undec)) // if an argument y is undecided, it must be attacked by an undecided argument
end
....
A second context then extends the above one, and encodes our particular
problem instance:
....
context Arguments_Example extends ArgumentsAsSets
constants A B C D E
axioms
@part partition(ARGUMENTS,{A},{B},{C},{D},{E})
@example attacks = {B↦A, C↦B, D↦C, E ↦ B, E↦D}
/* A = the sun will shine to day, B = we are in the UK
C = it is summer, D = there are only 10 days of sunshine per year, E = the BBC has forecast sun */
end
....
If you load this model with <<tutorial-rodin-first-step,ProB for
Rodin>>, you can see the solution in the State view:
image::ProBRodinArgumentationState.png[]
src/docs/chapter/model_examples/Blocks_World_(Directed_Model_Checking).adoc deleted 100644 → 0
+ 0
− 206
View file @ dccded69
[[blocks-world-directed-model-checking]]
= Blocks World (Directed Model Checking)
In this example we want to highlight the new
<<tutorial-directed-model-checking,directed model checking>> features
of ProB (available as of version 1.5.1), which allow one to direct the
model checker towards a desired goal. Technically speaking, the model
checker now maintains a weighted priority queue of unprocessed states,
choosing states with minimal weights for processing. The user can
influence how the weights for the unprocessed states are to be computed.
The techniques are also explained and evaluated in a scientific paper
footnote:[M. Leuschel and J. Bendisposto: Directed Model Checking for B:
An Evaluation and New Techniques. In Proceedings SBMF'2010, LNCS 6527.
Springer-Verlag, 2010
https://www3.hhu.de/stups/downloads/pdf/LeBe2010.pdf].
To illustrate the directed model checking feature, we use the following
model of Blocks-World, where we manipulate a given set of blocks
(a,b,c,d,e,f). A robot arm can pick of blocks (provided no other block
is on top of it) and either move it onto a table or onto another block
(provided this block has no other block on top of it). The goal is,
given a starting position, to find a plan for the robot to achieve a
certain goal (here: block a is on top of b, which is on top of c, ...).
We want to use the model checker to find such a plan, i.e., a
counter-example found by the model checker is actually a solution to our
planning problem.
In B we can model this task as follows. We have two operations, on to
move a block onto the table and one to move a block onto another one.
The initial configuration is specified in the INITIALISATION; the target
is specified by the GOAL definition (which the ProB model checker
recognises).
....
MACHINE BlocksWorldGeneric6
SETS
Objects={a,b,c,d,e,f}
DEFINITIONS
GOAL == (on = ongoal);
ongoal == {a|->b, b|->c, c|->d, d|->e, e|->f}
VARIABLES on
INVARIANT
on: Objects +-> Objects
INITIALISATION
on := {a|->b, c|->a}
OPERATIONS
move_on_table(obj) = PRE obj /: ran(on) & obj : dom(on) THEN
on := {obj} <<| on
END;
move_on_object(obj,onobj) = PRE obj/:ran(on) & onobj /:ran(on) & obj /= onobj THEN
on(obj) := onobj
END
END
....
Adding a graphical visualization
Adding a <<graphical-visualization,graphical visualization>> is
independent of the model checking, but helps visualising the traces
found by the model checker. For this we can add `ANIMATION_FUNCTION` and
`ANIMATION_FUNCTION_DEFAULT` definition, as specified in the complete
model at the end of this page.
The initial state of our model then looks as follows, when loaded using
ProB Tcl/Tk:
image::ProB_BlockInit_Screenshot.png[]
Finding the GOAL
To use the default mixed depth-first/breadth-first search you can type:
`$ probcli BlocksWorldGeneric6.mch -model_check`
As it has a random component, runtimes vary (typically 0.5 to 3.5
seconds on a Mac Book Air 1.7 GHz). It finds reasonably short counter
examples.
You can use depth-first search using the -df flag:
`$ probcli BlocksWorldGeneric6.mch -model_check -df`
This finds a counter-example of length 48 relatively quickly (120 ms
model checking time). You can use the `-bf` flag to force breadth-first
search, thus obtaining shortest counter-examples (of length 7; model
checking time about 3.3 seconds).
As of version 1.5.1 you can use the
<<using-the-command-line-version-of-prob,`-mc_mode`>>
flag to provide other options to control the model checking (see also
<<tutorial-directed-model-checking,the tutorial page on directed
model checking options>>).
One option is `random`, which gives every node (aka unprocesses state) a
random weight. The difference over the mixed depth-first/breadth-first
mode is that it completely disregards when nodes where generated. The
mixed depth-first/breadth-first mode will try to do a mixture of
depth-first and breadth-first traversal; the random mode here is
"just" random:
`probcli BlocksWorldGeneric6.mch -model_check -mc_mode random`
A variation of the above is the `hash` mode, which simply uses the
state's Prolog hash as the random weight. The difference is that the
result here is predictable, i.e., you will always get the same result
when you run the model checker:
`probcli BlocksWorldGeneric6.mch -model_check -mc_mode hash`
Possibly a more interesting mode is `heuristic`. It looks for a
user-provided DEFINITION for `HEURISTIC_FUNCTION` and uses this a s
priority for states to process next. For example, we can provide the
following definition to measure the distance to our target goal:
....
DIFF(A,TARGET) == (card(A-TARGET) - card(TARGET /\ A));
HEURISTIC_FUNCTION == DIFF(on,ongoal);
....
Now we get very good model checking time and short counter-examples (aka
solution traces):
....
$ probcli BlocksWorldGeneric6.mch -model_check -mc_mode heuristic
ALL OPERATIONS COVERED
found_error(goal_found,62)
finding_trace_from_to(root)
.
Model Checking Time: 80 ms (80 ms walltime)
States analysed: 12
Transitions fired: 99
*** COUNTER EXAMPLE FOUND ***
goal_found
*** TRACE:
1: INITIALISATION({(a|->b),(c|->a)}):
2: move_on_object(c,d):
3: move_on_object(e,f):
4: move_on_table(c):
5: move_on_object(d,e):
6: move_on_object(c,d):
7: move_on_table(a):
8: move_on_object(b,c):
9: move_on_object(a,b):
! *** error occurred ***
! goal_found
....
In ProB Tcl/Tk you simply use the standard model checking dialog (in the
Verify menu) and choose the "Heuristic Function / Random" option in
the "Search Strategy" pop-up menu:
image:ProB_MC_Heuristic.png[200px|center]
After that you can find the solution quickly by simply pressing the
"Model Check" button:
image:ProB_BlockGoal_Screenshot.png[600px|center]
When writing your own heuristic functions, keep in mind that internally
the weights are stored as 64-bit integers on 64-bit systems, and 32-bit
integers on 32-bit systems; currently no overflow checking is performed
and larger values for the `HEURISTIC_FUNCTION` expression are silently
converted to the respective integer size.
The complete model for reference
....
MACHINE BlocksWorldGeneric6
SETS
Objects={a,b,c,d,e,f}
DEFINITIONS
ANIMATION_FUNCTION_DEFAULT == {r,c,img|r:1..card(Objects) & img=0 & c:1..card(Objects)};
ANIMATION_FUNCTION == ( {r,c,i| r=card(Objects) & i:Objects & c:Objects & c=i & i/:dom(on)} \/
{r,c,i| r:1..(card(Objects)-1) & i:Objects & c:Objects &
i|->c:iterate(on,card(Objects)-r) & c/:dom(on)}
);
ANIMATION_IMG0 == "images/empty_box_white.gif";
ANIMATION_IMG1 == "images/A.gif";
ANIMATION_IMG2 == "images/B.gif";
ANIMATION_IMG3 == "images/C.gif";
ANIMATION_IMG4 == "images/D.gif";
ANIMATION_IMG5 == "images/E.gif";
ANIMATION_IMG6 == "images/F.gif";
GOAL == (on = ongoal);
ongoal == {a|->b, b|->c, c|->d, d|->e, e|->f};
DIFF(A,TARGET) == (card(A-TARGET) - card(TARGET /\ A));
HEURISTIC_FUNCTION == DIFF(on,ongoal);
VARIABLES on
INVARIANT
on: Objects +-> Objects
INITIALISATION
on := {a|->b, c|->a}
OPERATIONS
move_on_table(obj) = PRE obj /: ran(on) & obj : dom(on) THEN
on := {obj} <<| on
END;
move_on_object(obj,onobj) = PRE obj/:ran(on) & onobj /:ran(on) & obj /= onobj THEN
on(obj) := onobj
END
END
....
src/docs/chapter/model_examples/Bridges_Puzzle_(Hashiwokakero).adoc deleted 100644 → 0
+ 0
− 174
View file @ dccded69
[[bridges-puzzle-hashiwokakero]]
= Bridges Puzzle (Hashiwokakero)
The https://en.wikipedia.org/wiki/Hashiwokakero[Hashiwokakero] Puzzle is
a logical puzzle where one has to build bridges between islands. The
puzzle is also known under the name Ai-Ki-Ai. The puzzles can also be
http://www.puzzle-bridges.com[played online].
The requirements for this puzzle are as follows:
* the goal is to build bridges between islands so as to generate a
connected graph
* every island has a number on it, indicating exactly how many bridges
should be linked with the island
* there is an upper bound (MAXBRIDGES) on the number of bridges that can
be built-between two islands
* bridges cannot cross each other
A B model for this puzzle can be found below. The constants and sets of
the model are as follows:
* N are the nodes (islands); we have added a constant ignore where one
can stipulate which islands should be ignored in this puzzle
* nl (number of links) stipulates for each island how many bridges it
should be linked with
* xc, yc are the x- and y-coordinates for every island
A simple puzzle with four islands would be defined as follows, assuming
the basic set N is defined as `N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}`:
....
xc(a)=0 & xc(b)=1 & xc(c)=0 & xc(d) = 1 &
yc(a)=0 & yc(b)=0 & yc(c)=1 & yc(d) = 1 &
nl = {a|->2, b|->2, c|->2, d|->2} &
ignore = {e,f,g,h,i,j,k,l,m,n}
....
Below we will use a more complicated puzzle to illustrate the B model.
The model then contains the following derived constants:
* plx,ply: the possible links between islands on the x- and y-axis
respectively
* pl: the possible links both on the x- and y-axis combined
* cs: the conflict set of links which overlap, i.e., one cannot build
bridges on both links (a,b) when the pair (a,b) is in cs
* connected: the set of links on which at least one bridge was built
The model also sets up the goal constant `sol` which maps every link in
`pl` to a number indicating how many bridges are built on it. The model
also stipulates that the graph set up by connected generates a fully
connected graph.
Here is the full model:
....
MACHINE Bridges
DEFINITIONS
MAXBRIDGES==2;
LINKS == 1..(MAXBRIDGES*4);
COORD == 0..10;
p1 == prj1(nodes,nodes);
p2 == prj2(nodes,nodes);
p1i == prj1(nodes,INTEGER)
SETS
N = {a,b,c,d,e,f,g,h,i,j,k,l,m,n}
CONSTANTS nodes, ignore, nl, xc,yc, plx,ply,pl, cs, sol, connected
PROPERTIES
nodes = N \ ignore &
// target number of links per node:
nl : nodes --> LINKS & /* number of links */
// coordinates of nodes
xc: nodes --> COORD & yc: nodes --> COORD &
// possible links:
pl : nodes <-> nodes &
plx : nodes <-> nodes &
ply : nodes <-> nodes &
plx = {n1,n2 | xc(n1)=xc(n2) & n1 /= n2 & yc(n2)>yc(n1) &
!n3.(xc(n3)=xc(n1) => yc(n3) /: yc(n1)+1..yc(n2)-1) } &
ply = {n1,n2 | yc(n1)=yc(n2) & n1 /= n2 & xc(n2)>xc(n1) &
!n3.(yc(n3)=yc(n1) => xc(n3) /: xc(n1)+1..xc(n2)-1)} &
pl = plx \/ ply
&
// compute conflict set (assumes xc,yc coordinates ordered in plx,ply)
cs = {pl1,pl2 | pl1:plx & pl2:ply &
xc(p1(pl1)): xc(p1(pl2))+1..xc(p2(pl2))-1 &
yc(p1(pl2)): yc(p1(pl1))+1..yc(p2(pl1))-1}
&
sol : pl --> 0..MAXBRIDGES &
!nn.(nn:nodes => SIGMA(l).(l:pl &
(p1(l)=nn or p2(l)=nn)|sol(l))=nl(nn)) &
!(pl1,pl2).( (pl1,pl2):cs => sol(pl1)=0 or sol(pl2)=0) // no conflicts
&
// check graph connected
connected = {pl|sol(pl)>0} &
closure1(connected \/ connected~)[{a}] = {nn|nn:nodes & nl(nn)>0}
// encoding of puzzle
&
// A puzzle from bridges.png
xc(a)=1 & yc(a)=1 & nl(a)=4 &
xc(b)=1 & yc(b)=4 & nl(b)=6 &
xc(c)=1 & yc(c)=6 & nl(c)=3 &
xc(d)=2 & yc(d)=2 & nl(d)=1 &
xc(e)=2 & yc(e)=5 & nl(e)=2 &
xc(f)=3 & yc(f)=2 & nl(f)=4 &
xc(g)=3 & yc(g)=4 & nl(g)=6 &
xc(h)=3 & yc(h)=5 & nl(h)=4 &
xc(i)=4 & yc(i)=3 & nl(i)=3 &
xc(j)=4 & yc(j)=6 & nl(j)=3 &
xc(k)=5 & yc(k)=2 & nl(k)=1 &
xc(l)=6 & yc(l)=1 & nl(l)=4 &
xc(m)=6 & yc(m)=3 & nl(m)=5 &
xc(n)=6 & yc(n)=5 & nl(n)=2 &
ignore = {}
END
....
The puzzle encode above can be visualized as follows:
image::ProB_BridgesPuzzle.png[]
A solution for this puzzle is found by ProB in 0.08 seconds (on a
MacBook Air 2.2GHz i7). The conflict set is
`{((d|->e),(b|->g)), ((i|->j),(h|->n))}` and the value for sol is
....
{((a|->b)|->2),((a|->l)|->2),((b|->c)|->2),((b|->g)|->2),((c|->j)|->1),
((d|->e)|->0),((d|->f)|->1),((e|->h)|->2),((f|->g)|->2),((f|->k)|->1),
((g|->h)|->2),((h|->n)|->0),((i|->j)|->2),((i|->m)|->1),((l|->m)|->2),((m|->n)|->2)}
....
[[adding-graphical-visualization-graphical-puzzle]]
== Adding graphical visualization
To show the solution graphically, we can add the following to the
`DEFINITIONS` clause in the model:
....
CUSTOM_GRAPH_NODES == {n,w,w2|(n|->w):nl & w=w2}; // %n1.(n1:nodes|nl(n1));
CUSTOM_GRAPH_EDGES == {n1,w,n2|n1:nl & n2:nl & (p1i(n1),p1i(n2),w):sol}
....
One can then load the model, perform the initialisation (double clicking
on `INITIALISATION` in the operations pane) and the execute the command
"Current State as Custom Graph" in the States sub-menu of the
Visualize menu. This leads to the following picture:
image::ProB_BridgesSol.png[]
One can load the Dot file generated by ProB into another tool (e.g.,
OmniGraffle) and then re-arrange the nodes to obtain the rectangular
layout respecting the x- and y-coordinates:
image::ProB_BridgesSolOmni.png[]
src/docs/chapter/model_examples/Cheryl's_Birthday.adoc deleted 100644 → 0
+ 0
− 104
View file @ dccded69
[[cheryls-birthday]]
= Cheryl's Birthday
This Puzzle is a variation of another Puzzle (Sum and Product) and has
been described
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html[in
a New York Times article].
Here is a first solution in B, where the text of the puzzle has been
integrated as comments. There are almost certainly more elegant
encodings of the problem in B. You can load this model using, e.g., ProB
Tcl/Tk (see below). The model is also available as an example in our
<<prob-logic-calculator,online ProB Logic Calculator>>.
In case you are new to B, you probably need to know the following
operators to understand the specification below (we als have a
<<summary-of-b-syntax,summary page about the B syntax>>):
* `x : S` specifies that x is an element of S
* `dom(r)` is the domain of a function or relation r
* `r~` is the inverse of a function or relation r
* `r[S]` is the relational image of a relation r for a set of domain
values S
* `card(S)` is the cardinality of a set S
* `a|->b` represents the pair (a,b); note that a relation and function
in B is a set of pairs.
* `!x.(P => Q)` denotes universal quantification over variable x
....
MACHINE CherylsBirthday
/* A simplified version of the SumProduct Puzzle taken from
http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html
*/
DEFINITIONS
DontKnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) > 1;
KnowFromDay(PossDates,KDay) == card(PossDates~[{KDay}]) = 1
CONSTANTS Month, Day, PD, PD2
PROPERTIES
/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
Month:STRING & Day:1..31 &
/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */
PD = {("aug"|->14),("aug"|->15),("aug"|->17),
("july"|->14),("july"|->16),("june"|->17),("june"|->18),
("may"|->15),("may"|->16),("may"|->19)}
&
/*
Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday.
To Bernard, she whispered the day, and only the day.
*/
Month : dom(PD) &
Day : ran(PD) &
Month|->Day : PD &
/* Albert: I don’t know when your birthday is, */
card(PD[{Month}]) > 1 &
/* but I know Bernard doesn’t know, either. */
!x.(x:PD[{Month}] => DontKnowFromDay(PD,x) ) &
/* Bernard: I didn’t know originally, */
DontKnowFromDay(PD,Day) &
/* but now I do. */
PD2 = {m,d| (m|->d):PD & !x.(x:PD[{m}] => DontKnowFromDay(PD,x) ) } &
KnowFromDay(PD2,Day) &
/* Albert: Well, now I know, too! */
card({d|Month|->d : PD2 & KnowFromDay(PD2,d)})=1
ASSERTIONS /* single solution found by ProB in 20-30 ms */
Month = "july";
Day = 16
END
....
When loading this B machine in ProB, you will see that there is only a
single solution (solving time 20-30 ms) : `Month = "july" and
`Day = 16`.
Here is a screenshot of ProB Tcl/Tk after loading the model.
image::ProB_Cheryl_Screenshot.png[]
Using an enumerated set
It is possible to use an enumerated set for the Months. One simply has
to add
....
SETS MONTHS = {may, june, july, aug, sep}
....
and then change the definition of the possible dates:
....
PD = {(aug|->14), (aug|->15), (aug|->17),
(july|->14),(july|->16),(june|->17),
(june|->18),
(may|->15),(may|->16),(may|->19)}
....
and also "`july`" in the ASSERTIONS clause into `july`. This makes
constraint solving via ProB marginally faster.
src/docs/chapter/model_examples/Die_Hard_Jugs_Puzzle.adoc deleted 100644 → 0
+ 0
− 277
View file @ dccded69
[[die-hard-jugs-puzzle]]
= Die Hard Jugs Puzzle
This is the B model of a puzzle from the movie "Die Hard with a
Vengeance". This https://www.youtube.com/watch?v=BVtQNK_ZUJg[clip shows
Bruce Willis and Samuel Jackson having a go at the puzzle]. A
http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm[more
detailed explanation can be found here]. At start we have one 3 gallon
and one 5 gallon jug, and we need to measure precisely 4 gallons by
filling, emptying or transferring water from the jugs.
....
MACHINE Jars
DEFINITIONS
GOAL == (4 : ran(level));
SETS Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
....
After opening the file in ProB, choose the Model Check command in the
Verify menu and then check the "Find Define GOAL" check box. This
instructs ProB to search for states satisfying the GOAL predicate
`(4:ran(level))` defined above.
image::ProB_ModelCheckGoalBox.png[]
Now press the model check button and you should now obtain the following
message:
image::ProB_Goal_Found.png[]
The main window of ProB now contains the following information:
image::Jars_Panes.png[]
You can see that the second jug contains exactly 4 gallons. The steps
required to reach this state can be found in the history pane on the
right (in reverse order).
[[graphical-animation]]
== Graphical Animation
This machine above is actually included in the ProB distribution (inside
the examples/B/GraphicalAnimation/ directory). It also contains the
following lines in the DEFINITIONS section, which defines a
quick-and-dirty <<graphical-visualization,graphical visualisation>>
of the state. The images can be found in the subfolder images along the
file Jars.mch.
....
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)}
....
Here is a screenshot of ProB Tcl/Tk after loading the model and having
found the goal:
image::ProB_DieHard_Screenshot.png[]
[[using-probcli-command-line-version]]
== Using probcli (command-line version)
To find the solution using probcli you just need to type:
`probcli -model_check Jars.mch`
The output will be as follows:
....
$ probcli -model_check Jars.mch
% found_enumeration_of_constants(30,40)
% backtrack(found_enumeration_of_constants(30,40))
ALL OPERATIONS COVERED
found_error(goal_found,10)
finding_trace_from_to(root)
.
Model Checking Time: 60 ms (60 ms walltime)
States analysed: 10
Transitions fired: 36
*** COUNTER EXAMPLE FOUND ***
goal_found
*** TRACE:
1: SETUP_CONSTANTS({(j3|->3),(j5|->5)}):
2: INITIALISATION({(j3|->0),(j5|->0)}):
3: FillJar(j5):
4: Transfer(j5,3,j3):
5: EmptyJar(j3):
6: Transfer(j5,2,j3):
7: FillJar(j5):
8: Transfer(j5,1,j3):
! *** error occurred ***
! goal_found
....
[[tla-version]]
== TLA+ Version
A TLA+ version of the puzzle is also included with ProB (inside the
examples/TLA+/ directory). The specification was developed by Leslie
Lamport. It is possible to load TLA+ specifications with ProB as shown
on the <<tla,TLA>> wiki page.
....
------------------------------ MODULE DieHard -------------------------------
(***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
(* goal: to get TLC to solve the problem for us. *)
(* *)
(* First, we write a spec that describes all allowable behaviors of our *)
(* heros. *)
(***************************************************************************)
EXTENDS Naturals
(*************************************************************************)
(* This statement imports the definitions of the ordinary operators on *)
(* natural numbers, such as +. *)
(*************************************************************************)
(***************************************************************************)
(* We next declare the specification's variables. *)
(***************************************************************************)
VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
small \* The number of gallons of water in the 3 gallon jug.
(***************************************************************************)
(* We now define TypeOK to be the type invariant, asserting that the value *)
(* of each variable is an element of the appropriate set. A type *)
(* invariant like this is not part of the specification, but it's *)
(* generally a good idea to include it because it helps the reader *)
(* understand the spec. Moreover, having TLC check that it is an *)
(* invariant of the spec catches errors that, in a typed language, are *)
(* caught by type checking. *)
(* *)
(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
(* or \/ denotes the conjunction or disjunction of those formulas. *)
(* Indentation of subitems is significant, allowing one to eliminate lots *)
(* of parentheses. This makes a large formula much easier to read. *)
(* However, it does mean that you have to be careful with your indentation.*)
(***************************************************************************)
TypeOK == /\ small \in 0..3
/\ big \in 0..5
(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. I like to name this predicate Init, but the *)
(* name doesn't matter. *)
(***************************************************************************)
Init == /\ big = 0
/\ small = 0
(***************************************************************************)
(* Now we define the actions that our hero can perform. There are three *)
(* things they can do: *)
(* *)
(* - Pour water from the faucet into a jug. *)
(* *)
(* - Pour water from a jug onto the ground. *)
(* *)
(* - Pour water from one jug into another *)
(* *)
(* We now consider the first two. Since the jugs are not calibrated, *)
(* partially filling or partially emptying a jug accomplishes nothing. *)
(* So, the first two possibilities yield the following four possible *)
(* actions. *)
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big
FillBigJug == /\ big' = 5
/\ small' = small
EmptySmallJug == /\ small' = 0
/\ big' = big
EmptyBigJug == /\ big' = 0
/\ small' = small
(***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *)
(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
(* makes sense only to either fill B or empty A. And there's no point in *)
(* emptying A if this will cause B to overflow, since that could be *)
(* accomplished by the two actions of first filling B and then emptying A. *)
(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
(* contained in both jugs and (ii) the volume of B. To express this *)
(* mathematically, we first define Min(m,n) to equal the minimum of the *)
(* numbers m and n. *)
(***************************************************************************)
Min(m,n) == IF m < n THEN m ELSE n
(***************************************************************************)
(* Now we define the last two pouring actions. From the observation *)
(* above, these definitions should be clear. *)
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)
BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small)
(***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *)
(* step is a step of one of the six actions defined above. Hence, Next is *)
(* the disjunction of those actions. *)
(***************************************************************************)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall
-----------------------------------------------------------------------------
(***************************************************************************)
(* Remember that our heros must measure out 4 gallons of water. *)
(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
(* solved their problem when they reach a state with big = 4. So, we *)
(* define NotSolved to be the predicate asserting that big # 4. *)
(***************************************************************************)
NotSolved == big # 4
(***************************************************************************)
(* We find a solution by having TLC check if NotSolved is an invariant, *)
(* which will cause it to print out an "error trace" consisting of a *)
(* behavior ending in a states where NotSolved is false. Such a *)
(* behavior is the desired solution. (Because TLC uses a breadth-first *)
(* search, it will find the shortest solution.) *)
(***************************************************************************)
=============================================================================
....
[[z-version]]
== Z Version
A Z version of the puzzle is also included with ProB (inside the
examples/Z/GraphicalAnimation/ directory) and shown on the
<<proz,ProZ>> wiki page.
Here is how the animation of the Z specification should look like:
image::ProZ_jars.png[]
src/docs/chapter/model_examples/Fibonacci_Numbers_with_Automatic_Dynamic_Programming.adoc deleted 100644 → 0
+ 0
− 46
View file @ dccded69
[[fibonacci-numbers-with-automatic-dynamic-programming]]
= Fibonacci Numbers with Automatic Dynamic Programming
In this example we show how one can encode the Fibonacci problem in such
a way that you get dynamic programming automatically when using ProB to
solve the encoding:
....
MACHINE Fibonacci_Dynamic_Programming
/* an encoding of Fibonacci where we get dynamic programming for free from ProB */
DEFINITIONS
DOM == INTEGER; /* INTEGER : For ProB no restriction necessary; for Kodkod yes */
CONSTANTS n, fib, sol
PROPERTIES
fib : 0..n --> DOM &
fib(0) = 1 & fib(1) = 1 &
!x.(x:2..n => fib(x) = fib(x-1) + fib(x-2))
& n = 200 & sol = fib(n)
END
....
Runtimes on a 1.7 GHz i7 Mac Book Air with ProB 1.4.0-rc2, where we have
also used our Kodkod backend with minSAT for comparison. For Kodkod to
be applicable, we had to constrain the domain DOM of possible Fibonacci
numbers as indicated below:
....
n DOM ProB Kodkod -> Result Fib(n)
10 1..100 0.01 1.93 sec
11 1..200 0.01 5.15 sec
10 INTEGER 0.01 impossible
20 INTEGER 0.01 impossible -> 10946
40 INTEGER 0.01 impossible -> 165580141
100 INTEGER 0.02 impossible -> 573147844013817084101
200 INTEGER 0.06 impossible -> 453973694165307953197296969697410619233826
....
[[how-does-it-work]]
== How does it work
[TODO: insert explanation]
src/docs/chapter/model_examples/Game_of_Life.adoc deleted 100644 → 0
+ 0
− 86
View file @ dccded69
[[game-of-life]]
= Game of Life
This is a simple model of Conway's Game of Life. It was written for
animation with ProB. One interesting aspect is that the simulation is
unbounded, i.e., not restricted to some pre-determined area of the grid.
....
MACHINE gol
/* A simple B model of the Game of Life */
/* by Jens Bendisposto and Michael Leuschel */
ABSTRACT_CONSTANTS nc
PROPERTIES
/* neighbour count function: */
nc = %(a,b,alive).(a:INTEGER&b:INTEGER & alive <: INTEGER*INTEGER
| card({(xn,yn)| (xn,yn) : alive & neighbour(xn,yn,a,b)}))
VARIABLES alive
DEFINITIONS
neighbour(x,y,a,b) == (max({x-a,a-x}) : {0,1} & max({y-b,b-y}) : {0,1} & (x,y)/=(a,b));
INVARIANT
alive <: INTEGER * INTEGER & alive /= {}
INITIALISATION
alive := {(2,1),(2,2),(2,3)} /* blinker */
OPERATIONS
step = alive := {(u1,v1) | (u1,v1):alive & nc(u1,v1,alive) : {2,3} } \/
{(u2,v2) | #(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) & /* restrict enumeration to neighbours of alive */
(u2,v2)/:alive & nc(u2,v2,alive)=3 }
END
....
We believe this to be quite compact. In the future we hope to be able to
remove the need to add the predicate
`#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2))` by improving ProB's
constraint solver for cardinality constraints on set comprehensions. You
may want to compare this to an
https://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/[ASM
specification found here] and described on pages 39-40 in Egon Börger
and Robert Stärk, Abstract State Machines, A Method for High-Level
System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).
If you want to visualize the simulation using ProB's Tk graphical viewer
one needs to add a definition for the animation function. This leads to
the following B model (where we have also added an alternate definition
of the neighbourhood relationship):
....
MACHINE gol
/* A simple B model of the Game of Life */
/* by Jens Bendisposto and Michael Leuschel */
ABSTRACT_CONSTANTS nc
PROPERTIES
/* neighbour count function: */
nc = %(a,b,alive).(a:INTEGER&b:INTEGER & alive <: INTEGER*INTEGER
| card({(xn,yn)| (xn,yn) : alive & neighbour(xn,yn,a,b)}))
VARIABLES alive
DEFINITIONS
/* two alternate definitions of neighbour relationship; both work */
neighbour1(x,y,a,b) == (max({x-a,a-x}) : {0,1} & max({y-b,b-y}) : {0,1} & (x,y)/=(a,b));
neighbour(x,y,a,b) == ((x-a)**2 <= 1 & (y-b)**2 <=1 & (x,y)/=(a,b));
/* some simple patterns : */
blinker == {(2,1),(2,2),(2,3)} ; glider == {(1,2),(2,3),(3,1),(3,2),(3,3)} ;
SET_PREF_CLPFD == TRUE;
/* describing the animation function for the graphical visualization : */
wmin == min(dom(alive)\/{1}); wmax == max(dom(alive)\/{1});
hmin == min(ran(alive)\/{1}); hmax == max(ran(alive)\/{1});
ANIMATION_FUNCTION_DEFAULT == ( (wmin..wmax)*(hmin..hmax)*{0} );
ANIMATION_FUNCTION == ( alive * {1} );
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif"
INVARIANT
alive <: INTEGER * INTEGER & alive /= {}
INITIALISATION
alive := glider
OPERATIONS
step = alive := {(u1,v1) | (u1,v1):alive & nc(u1,v1,alive) : {2,3} } \/
{(u2,v2) | #(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) & /* restrict enumeration to neighbours of alive */
(u2,v2)/:alive & nc(u2,v2,alive)=3 }
END
....
The following is a screenshot of ProB Tcl/Tk animating the above model:
image:ProB_GameOfLife_Screenshot.png[600px|center]
src/docs/chapter/model_examples/Gilbreath_Card_Trick.adoc deleted 100644 → 0
+ 0
− 244
View file @ dccded69
[[gilbreath-card-trick]]
= Gilbreath Card Trick
My belief is that B is a very expressive language, which can be very
convenient for modelling many problems. Hence, when in the Dagstuhl
library I stumbled upon a nice short
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10[article
by Tony Hoare and Natarajan Shankar] in memory of Amir Pnueli, I decided
to model the problem and time how long it would take me to solve the
problem using ProB. The article unravels a card trick by Gilbreath. The
card trick has several phases:
* first you arrange 16 cards into a sequence of quartets with one card
from each suit (Spade, Club, Heart, Diamond) in the same order. The
example in the
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10[article]
is as follows: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩, ⟨K♠⟩,⟨2♡⟩,⟨7♣⟩,⟨4♢⟩,
⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩
* you split the cards into two sequences. The example in the
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10[article]
is: ⟨5♠⟩,⟨3♡⟩,⟨Q♣⟩,⟨8♢⟩,⟨K♠⟩ and ⟨2♡⟩,⟨7♣⟩,⟨4♢⟩,⟨8♠⟩,⟨J♡⟩,⟨9♣⟩,⟨A♢⟩ .
* you reverse one of the sequences
* you perform a (not necessarily perfect) riffle shuffle of the two
sequences
* the resulting final sequence is guaranteed to consist of a sequence of
four quartets with one card from each suite.
I attempted to model this problem in B and wanted to use model checking
to validate the property on the final sequence. As I wanted to measure
the time spent modeling I used a stopwatch. It took 13 minutes (starting
from an empty B specification) to produce a first model that could be
model checked by ProB. Full validation was finished after 19 minutes
from the start. The model checking itself generated 150,183 states and
179,158 transitions and took 2 minutes and 17 seconds on a Mac Book Air
(1.8 GHz i7). (Further below on this page I also describe ways to reduce
the model checking time.) I am very interested in seeing how much
combined modelling and verification time is required to solve this task
in other formalisms and with other model checking tools (e.g., Promela
with Spin, CSP with FDR, TLA+ with TLC).
Here is the specification
....
MACHINE CardTrick
/* Translation by Michael Leuschel of Example in
"Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar
in LNCS 6200, pp. 195-201, 2010.
DOI: 10.1007/978-3-642-13754-9_10
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
*/
SETS
SUIT={spade,club,heart,diamond}
DEFINITIONS
all == [spade,club,heart,diamond]; /* an arbitrary permutation of the suits */
/* check that in dst we can partition the deck into quartets where every suit occurs once: */
ok(dst) == #(a,b,c,d).(dst = a^b^c^d & size(a)=4 & size(b)=4 & size(c)=4 & size(d)=4 &
a : perm(SUIT) & b:perm(SUIT) & c:perm(SUIT) & d:perm(SUIT))
CONSTANTS
initial
PROPERTIES
initial = all^all^all^all /* we fix the sequence; i.e., we perform symmetry reduction by hand; it should be possible to achieve this by ProB's symmetry reduction itself using a deferred set */
VARIABLES x,y,dest,reversed
INVARIANT
x:seq(SUIT) & y:seq(SUIT) & dest:seq(SUIT) & reversed:BOOL &
((x=<> & y=<>) => ok(dest)) /* the property we are interested in: after the riffle shuffle the sequence consists of four quartets, each containing every suit */
INITIALISATION
x,y : (x^y = initial) /* split the initial sequence into two: x and y */
|| dest := <> || reversed := FALSE
OPERATIONS
/* reverse one of the two decks */
Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;
/* perform the riffle shuffle: transfer one card from either x or y to dest */
Shuffle1 = PRE x/=<> & reversed=TRUE THEN dest := dest<-last(x) || x:= front(x) END;
Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END
END
....
Some observations:
* in the above model I perform symmetry reduction by hand, by forcing a
particular order of the cards initially
* a version of the model which does not do this can be found below; it
requires symmetry reduction to be enabled for efficient model checking
* I have tried to translate this example to TLA+ and use
http://lamport.azurewebsites.net/tla/tlc.html[TLC]
(using our new B-TLC translator), but TLC cannot deal with the
initialisation `x,y : (x^y = initial)`. Later Domink Hansen produced an
adapted (more low-level) version of my B machine which can be run by
TLC; see below.
* A (longer) Why3 encoding can be found
http://proval.lri.fr/gallery/unraveling_a_card_trick.en.html[here].
* Arguably model checking gives less insight into why the trick works
than proof. However, by adding a graphical visualization, a different
kind of insight can be gained. This is shown below.
[[adding-graphical-visualization-gilbreath-card-trick]]
== Adding graphical visualization
To add a simple graphical visualization one needs to generate four
pictures (in GIF format). I took pictures from Wikimedia Commons. In the
DEFINITIONS section of the B machine above, you then simply have to add
the following:
....
ANIMATION_FUNCTION_DEFAULT == {(1,0,"x"),(2,0,"y"),(3,0,"dest")};
ANIMATION_FUNCTION == ( {r,c,i| r=1 & c|->i:x} \/ {r,c,i| r=2 & c|->i:y} \/ {r,c,i| r=3 & c|->i:dest} );
ANIMATION_IMG1 == "images/French_suits_Spade.gif";
ANIMATION_IMG2 == "images/French_suits_Club.gif";
ANIMATION_IMG3 == "images/French_suits_Heart.gif";
ANIMATION_IMG4 == "images/French_suits_Diamond.gif";
....
Details about the use of this feature can be found in the
<<graphical-visualization,Graphical_Visualization>> page of the
manual. With the above, ProB will display the variables x, y and dist in
a graphical way, and by animation one can gain insights into why it is
impossible not to generate four quartets.
image:ProB_Card_Screenshot.png[600px|center]
[[a-version-requiring-symmetry-reduction]]
== A version requiring symmetry reduction
....
MACHINE CardTrickSym /* a version to be used with ProB's symmetry reduction */
/* see comments in machine CardTrick for more details about the modeling effort */
/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
DOI: 10.1007/978-3-642-13754-9_10
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
*/
/* Model checking with hash symmetry taking 161.9 seconds to traverse
150,183 states and 179,181 transitions (on a MacBook Air 1.8Ghz i7) */
SETS
SUIT /* ={spade,club,heart,diamond} */
DEFINITIONS
/* check that in dst we can partition the deck into quartets where every suit occurs once */
ok(dst) == #(a,b,c,d).(dst = a^b^c^d & size(a)=4 & size(b)=4 & size(c)=4 & size(d)=4 &
a : perm(SUIT) & b:perm(SUIT) & c:perm(SUIT) & d:perm(SUIT))
CONSTANTS
all
PROPERTIES
card(SUIT)=4 &
all : perm(SUIT) /* a sequence of all suits in any order */
VARIABLES x,y,dest,reversed
INVARIANT
x:seq(SUIT) & y:seq(SUIT) & dest:seq(SUIT) & reversed:BOOL &
((x=<> & y=<>) => ok(dest))
INITIALISATION x,y : (x^y = all^all^all^all ) || dest := <> || reversed := FALSE
OPERATIONS
Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;
Shuffle1 = PRE x/=<> & reversed=TRUE THEN dest := dest<-last(x) || x:= front(x) END;
Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END
END
....
[[a-more-low-level-version-for-use-with-tlc]]
== A more low-level version for use with TLC
We later adapted the above model (without symmetry) to make it somewhat
more low-level and to enable the translation to TLA+ for use with
http://lamport.azurewebsites.net/tla/tlc.html[TLC]
(this is a new feature inside ProB Tcl/Tk). The machine is shown below.
The model checking time with ProB is now reduced to 75 seconds. With the
command "Verify -> External Tools -> Model Check with TLC..." you can
use
http://lamport.azurewebsites.net/tla/tlc.html[TLC]
as a backend. The model checking time is then approximately 15 seconds
(including the translation time from B to TLA+).
....
MACHINE CardTrick_TLC
/* A version of the machine (adapted by Domink Hansen) which is a bit more low-level;
this improves model checking performance and now allows translation to TLC */
/* Translation by Michael Leuschel of Example in "Unraveling a Card Trick" by Tony Hoare and Natarajan Shankar in LNCS 6200, pp. 195-201, 2010.
DOI: 10.1007/978-3-642-13754-9_10
https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10
*/
SETS
SUIT={spade,club,heart,diamond}
DEFINITIONS
all == [spade,club,heart,diamond];
/* check that in dst we can partition the deck into quartets where every suit occurs once */
subseq(s,m,n) == (s/|\n)\|/m-1;
ok(dst) == subseq(dst,1,4) : perm(SUIT)
& subseq(dst,5,8) : perm(SUIT)
& subseq(dst,9,12) : perm(SUIT)
& subseq(dst,13,16) : perm(SUIT);
/*#(a,b,c,d).(dst = a^b^c^d & size(a)=4 & size(b)=4 & size(c)=4 & size(d)=4 &
a : perm(SUIT) & b:perm(SUIT) & c:perm(SUIT) & d:perm(SUIT));*/
initial == all^all^all^all
/* we fix the sequence; i.e., we perform symmetry reduction by hand; it should be possible to achieve this by ProB's symmetry reduction itself using a deferred set */
VARIABLES x,y,dest,reversed
INVARIANT
x:seq(SUIT) & y:seq(SUIT) & dest:seq(SUIT) & reversed:BOOL &
((x=<> & y=<>) => ok(dest))
INITIALISATION x,y :(#n.(n : 0..size(initial) & x = initial /|\ n & y = initial \|/ n & x^y = initial)) || dest := <> || reversed := FALSE
OPERATIONS
Reverse = PRE reversed=FALSE THEN CHOICE x := rev(x) OR y := rev(y) END || reversed := TRUE END;
Shuffle1 = PRE x/=<> & reversed=TRUE THEN dest := dest<-last(x) || x:= front(x) END;
Shuffle2 = PRE y/=<> & reversed=TRUE THEN dest := dest<-last(y) || y:= front(y) END
END
....
The TLA+ translation generated by B-TLC is as follows:
....
---- MODULE CardTrick_TLC ----
EXTENDS Naturals, Sequences, SequencesExtended
CONSTANTS spade, club, heart, diamond
VARIABLES x, y, dest, reversed
SUIT == {spade, club, heart, diamond}
all == <<spade, club, heart, diamond>>
subseq(s, m, n) == DropFirstElements(TakeFirstElements(s, n), m - 1)
ok(dst) == subseq(dst, 1, 4) \in Perm(SUIT) /\ subseq(dst, 5, 8) \in Perm(SUIT) /\ subseq(dst, 9, 12) \in Perm(SUIT) /\ subseq(dst, 13, 16) \in Perm(SUIT)
initial == all \o all \o all \o all
Invariant == x \in Seq(SUIT) /\ y \in Seq(SUIT) /\ dest \in Seq(SUIT) /\ reversed \in BOOLEAN /\ (x = <<>> /\ y = <<>> => ok(dest))
Init == \E n \in (0 .. Len(initial)) : n \in (0 .. Len(initial)) /\ x = TakeFirstElements(initial, n) /\ y = DropFirstElements(initial, n) /\ x \o y = initial
/\ dest = <<>>
/\ reversed = FALSE
Reverse == reversed = FALSE
/\ ((x' = Rev(x) /\ UNCHANGED <<y>>) \/ (y' = Rev(y) /\ UNCHANGED <<x>>))
/\ reversed' = TRUE /\ UNCHANGED <<dest>>
Shuffle1 == (x # <<>> /\ reversed = TRUE)
/\ dest' = Append(dest, Last(x))
/\ x' = Front(x) /\ UNCHANGED <<y, reversed>>
Shuffle2 == (y # <<>> /\ reversed = TRUE)
/\ dest' = Append(dest, Last(y))
/\ y' = Front(y) /\ UNCHANGED <<x, reversed>>
Next == \/ Reverse
\/ Shuffle1
\/ Shuffle2
====
....
src/docs/chapter/model_examples/Mutual_Exclusion_(Fairness).adoc deleted 100644 → 0
+ 0
− 83
View file @ dccded69
[[mutual-exclusion-fairness]]
= Mutual Exclusion (Fairness)
Consider an Event-B model formalizing an algorithm for mutual exclusion
with semaphores for two concurrent processes latexmath:[$P_1$] and
latexmath:[$P_2$]. Each process has been simplified to perform three
types of events: _request_ (for entering in the critical section),
_enter_ (entering the critical section), and _release_ (exiting the
critical section). (For more information on the algorithm and the design
of the model see footnote:[C.Baier and J.-P. Katoen. “Principles of
Model Checking”, The MIT Press, 2008, pages 43-45.]).
Each of the actions of a process are represented by a respective event:
image::LTLViewMUTEXEvents.png[]
Each process latexmath:[$P_i$] has three possible states that are
denoted by the constants latexmath:[$noncrit_{i}$] (the state in which
latexmath:[$P_i$] performs noncritical actions), latexmath:[$wait_{i}$]
(the state in which latexmath:[$P_{i}$] waits to enter the critical
section), and latexmath:[$crit_{i}$] (representing the state in which
latexmath:[$P_{i}$] is in the critical section). Both processes share
the binary semaphore y where y=1 indicates that the semaphore is free
and y=0 that the semaphore is currently processed by one of the
processes.
There are several requirements that the mutual exclusion algorithm
should satisfy. The most important one is the mutual exclusion property
that says _always at most one process is in its critical section_. This
can be simply expressed, for example, as an invariant of the respective
Event-B model: not(p1 = crit1 & p2 = crit2). However, there are other
properties that can be easily expressed by means of LTL formulas and
automatically checked on the model. For example, the requirement _each
process will enter infinitely often its critical section_ can be
specified by the LTL formula `GF \{p1 = crit1} & GF \{p2 = crit2}` or
the starvation freedom property that states _each waiting process will
eventually enter its critical section_:
`G ({p1 = wait1} => F {p1 = crit1}) & G ({p2 = wait2} => F {p2=crit2})`
Running the LTL model checker of ProB will provide for the last two
properties above a counterexample since the model permits that a process
may perform infinitely often consecutively the events _request_, _enter_
and _release_, and in this way to ignore the other process infinitely.
An example trace that describes this behavior could be
latexmath:[$\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle$].
On the other hand, such behaviors can be considered as unrealistic
computations for the eventual implementation of the algorithm. Therefore
fairness constraints can be set in order to discard such behaviors. For
example, checking the property _process latexmath:[$P_1$] will enter its
critical section infinitely often_ (as LTL property: `GF \{p1 = crit1}`)
can be checked by restricting that the event `Req1` will not be
continuously ignored and that the event `Enter1` will not be ignored
infinitely often. Both conditions for the property can be given by means
of an LTL^[e]^ formula on the left side of the following implication:
`(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}`
For checking the formula the LTL model checker generates 13312
atomsfootnote:[The number of atoms generated for the search graph
corresponds to the number of valuations of the respective LTL^[e]^
formula times the number of states of the model.] and 7515 transitions
and needs overall 509 ms to prove the property (the model has 8 states
and 15 transitions in total). On the other hand, using the extension of
the LTL model checker for checking fairness (by entering the formula
`WF(Req1) & SF(Enter1) => GF \{p1=crit1}`), the model checker generates
32 atoms and 39 transitions (the atoms and transitions generated just
for `GF \{p1 = crit1}`) and an overall time of 50 ms.
For checking the requirement _each process will enter infinitely often
its critical section_ the LTL formula ` GF \{p1 = crit1} & GF \{p2 =
crit2}` should be checked with the following fairness constraints:
`(WF(Req1) & WF(Req2)) & (SF(Enter1) & SF(Enter2))`
Encoding these fairness conditions as an LTL^[e]^ formula will blow up
exponentially the number of atoms and the transitions in regard to the
number of temporal operators (in this case `G` (globally) and
`F`(finally)) and thus make practically impossible to check the above
property in a reasonable time.
src/docs/chapter/model_examples/N-Bishops_Puzzle.adoc deleted 100644 → 0
+ 0
− 71
View file @ dccded69
[[n-bishops-puzzle]]
= N-Bishops Puzzle
This puzzle is a variation of the <<n-queens,N-Queens>> puzzle: we
try to place as many bishops as possible on a n by n chess board. In
contrast to the N-Queens puzzle, one can place more than one bishop per
row. As such, we can now longer represent the positions of the bishops
as an total function `1..n >-> 1..n`. There are two encodings we show
below. The first represents the bishops as a subset of the Cartesian
product `(1..n)*(1..n)`, i.e., a set of positions (aka a binary relation
on `1..n`).
....
MACHINE NBishopsSets
CONSTANTS n, nbishops, hasbishop
PROPERTIES
n=8 &
hasbishop <: (1..n)*(1..n) &
!(i,j).(i:1..n & j:1..n
=>
( (i,j): hasbishop
=>
(!k.(k:(i+1)..n =>
(k,j+k-i) /: hasbishop &
(k,j-k+i) /: hasbishop
))
))
& nbishops = card(hasbishop)
& nbishops >13
END
....
One can try and find the maximum number of bishops by gradually
increasing the lower limit for nbishops in the last line of the model
before the final END. The maximum number of bishops that can be placed
is 2*n - 2; see http://mathworld.wolfram.com/BishopsProblem.html[here].
ProB 1.5.1 can solve this puzzle with `nbishops >13` in about half a
second.
One can use <<graphical-visualization,graphical visualisation>>
features to display the solution, by declaring the ANIMATION FUNCTION
inside the DEFINITIONS section as follows:
....
DEFINITIONS
BWOFFSET(x,y) == (x+y) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == {r,c,i|(r,c):hasbishop & i= 2+BWOFFSET(r,c)} ;
ANIMATION_IMG0 == "ChessPieces/Chess_emptyl45.gif";
ANIMATION_IMG1 == "ChessPieces/Chess_emptyd45.gif";
ANIMATION_IMG2 == "ChessPieces/Chess_bll45.gif";
ANIMATION_IMG3 == "ChessPieces/Chess_bld45.gif";
SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == 1;
END
....
This will lead to ProB to show the solution graphically, as follows:
image:ProB_Bishops_8_14_Screenshot.png[300px|center]
For the chess pieces we have used the images available at
https://commons.wikimedia.org/wiki/Category:SVG_chess_pieces[this site].
These images are available under the
https://en.wikipedia.org/wiki/Creative_Commons[Creative Commons]
https://creativecommons.org/licenses/by-sa/3.0/deed.en[Attribution-Share
Alike 3.0 Unported license]. The same applies to the screenshots shown
here.
src/docs/chapter/model_examples/N-Queens.adoc deleted 100644 → 0
+ 0
− 70
View file @ dccded69
[[n-queens]]
= N-Queens
The N-Queens is a famous constraint solving benchmark puzzle. It is a
generalisation of the original
https://en.wikipedia.org/wiki/Eight_queens_puzzle[eight queens puzzle],
where the goal is to place eight queens on a 8*8 chessboard so that no
two queens attach each other.
Here is one way to encode the N-Queens puzzle in B.
....
MACHINE NQueens
CONSTANTS n,queens
PROPERTIES
n = 40 &
queens : 1..n >-> 1..n /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+q2-q1 /= queens(q2) & queens(q1)-q2+q1 /= queens(q2))
END
....
ProB 1.3.7 can solve this puzzle in about 0.150 seconds (for n=40, on a
1.7 GHz Mac Book Air).
One can use <<graphical-visualization,graphical visualisation>>
features to display the solution, by declaring the ANIMATION FUNCTION as
follows:
....
MACHINE NQueens40
CONSTANTS n,queens
PROPERTIES
n = 40 &
queens : 1..n >-> 1..n /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+q2-q1 /= queens(q2) & queens(q1)-q2+q1 /= queens(q2))
DEFINITIONS
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( {r,c,i|c:1..n & r=queens(c) & i=2+((r+c) mod 2) } );
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif";
ANIMATION_IMG2 == "images/sm_queen_white.gif";
ANIMATION_IMG3 == "images/sm_queen_black.gif";
SET_PREF_CLPFD == TRUE;
END
....
This will lead to ProB to show the solution graphically, as follows (the
screenshot is unfortunately cropped and does not show all rows):
image:ProB_Queens_40_Screenshot.png[600px|center]
Instead of using ProB's standard constraint-solving backend, you can
also use our <<using-prob-with-kodkod,Kodkod backend>> to solve this
puzzle. To do this, either "Enable Kodkod for Properties" in the ProB
Tcl/Tk "Preferences" menu or add the following to the DEFINITIONS in
the machine file above:
....
SET_PREF_KODKOD == TRUE
....
However, using the MiniSat backend solving the N-queens puzzle for n=40
takes 57.1 seconds (on the same hardware as above).
src/docs/chapter/model_examples/Nine_Prisoners.adoc deleted 100644 → 0
+ 0
− 118
View file @ dccded69
[[nine-prisoners]]
= Nine Prisoners
An https://www.quantamagazine.org/150-year-old-math-design-problem-solved-20150609[article
in Quanta magazine] mentions the following puzzle by Dudeney and
popularized by Martin Gardner:
"So in the spirit of Kirkman, we will leave the gentle reader with
another brainteaser, a slight variation on the schoolgirl puzzle devised
in 1917 by the British puzzle aficionado Henry Ernest Dudeney and later
popularized by Martin Gardner: Nine prisoners are taken outdoors for
exercise in rows of three, with each adjacent pair of prisoners linked
by handcuffs, on each of the six weekdays (back in Dudeney’s less
enlightened times, Saturday was still a weekday). Can the prisoners be
arranged over the course of the six days so that each pair of prisoners
shares handcuffs exactly once?"
An encoding of this puzzle in B is relatively straightforward, thanks to
the use of sets, sequences and permutations and universal
quantification. To improve the performance, symmetry reductions were
added by hand in the model below. The constant `arrange` contains the
solution to our puzzle: the arrangement of the prisoners for every
working day from 1 to `Days`.
....
MACHINE NinePrisoners
DEFINITIONS
Prisoners == 1..9;
Days == 6;
Cuffs == {1,2, 4,5, 7,8 };
share(day,cuff) == {arrange(day)(cuff),arrange(day)(cuff+1)}
CONSTANTS arrange
PROPERTIES
/* typing + permutation requirement */
arrange : (1..Days) --> perm(Prisoners) &
/* symmetry breaking */
arrange(1) = %i.(i:Prisoners|i) &
!d.(d:1..Days =>
!c.(c:Prisoners & c mod 3 = 1 => arrange(d)(c) < arrange(d)(c+2))) &
!d.(d:1..Days =>
!c.(c:{1,3} => arrange(d)(c) < arrange(d)(c+3)))
&
/* the constraint proper */
!(c,d).(c:Cuffs & d:2..Days =>
!(c1,d1).(d1<d & d1>0 & c1:Cuffs =>
share(d,c) /= share(d1,c1))
)
END
....
The solving time using ProB on a MacBook Air is as follows: for Days ==
4: 0.08 seconds, for Days==5: 0.20 seconds, for Days == 6: 80 seconds
(i.e., the complete puzzle).
[[simple-graphical-visualization]]
== Simple Graphical Visualization
To generate a simple graphical visualization of the solutions found by
ProB, one needs to add a definition for the animation function, e.g., as
follows:
....
ANIMATION_FUNCTION ==
{r,c,i| r:1..Days & c:1..3 & i = arrange(r)(c) } \/
{r,c,i| r:1..Days & c:5..7 & i = arrange(r)(c-1) } \/
{r,c,i| r:1..Days & c:9..11 & i = arrange(r)(c-2) };
ANIMATION_FUNCTION_DEFAULT == {r,c,i| r:1..Days & c:1..11 & i = " " }
....
This gives rise to the following visualisation:
image::ProB_NinePrisoners_Simple.png[]
As can be seen in the screenshot, we have also added an operation to
inspect the solution computed by ProB:
....
OPERATIONS
r <-- Neighbours(i) = PRE i:Prisoners THEN /* compute for every day the neighbours of i */
r := %d.(d:1..Days |
UNION(x,c).( x:Prisoners & c:Cuffs & i: share(d,c)| share(d,c) \ {i})
) END
....
[[adding-graphical-visualization-nine-prisoners]]
== Adding graphical visualization
To add a better graphical visualization one needs to generate 10
pictures (in GIF format). I generate these using OmniGraffle. In the
DEFINITIONS section of the B machine above, you then simply have to add
the following (and remove the definition of `ANIMATION_FUNCTION_DEFAULT`
from above):
....
ANIMATION_FUNCTION_DEFAULT == {r,c,i| r:1..Days & c:1..11 & i = 0 };
ANIMATION_IMG0 == "images/Prisoner_0.gif";
ANIMATION_IMG1 == "images/Prisoner_1.gif";
ANIMATION_IMG2 == "images/Prisoner_2.gif";
ANIMATION_IMG3 == "images/Prisoner_3.gif";
ANIMATION_IMG4 == "images/Prisoner_4.gif";
ANIMATION_IMG5 == "images/Prisoner_5.gif";
ANIMATION_IMG6 == "images/Prisoner_6.gif";
ANIMATION_IMG7 == "images/Prisoner_7.gif";
ANIMATION_IMG8 == "images/Prisoner_8.gif";
ANIMATION_IMG9 == "images/Prisoner_9.gif"
....
This gives rise to the following graphical visualization of the first
solution found by ProB:
image:ProB_NinePrisoners_Fancy.png[600px|center]
Details about the use of this visualization feature can be found in the
<<graphical-visualization,Graphical_Visualization>> page of the
manual.
src/docs/chapter/model_examples/Peaceable_Armies_of_Queens.adoc deleted 100644 → 0
+ 0
− 223
View file @ dccded69
[[peaceable-armies-of-queens]]
= Peaceable Armies of Queens
I found this challenging constraint programming problem in the following
paper:
* B. M. Smith, K. E. Petrie, and I. P. Gent. Models and symmetry
breaking for peaceable armies of queens. In Integration of AI and OR
Techniques in Constraint Programming for Combinatorial Optimization
Problems, pages 271–286. Springer Berlin Heidelberg, 2004.
A variation of the problem can be found on page 329 of the
https://www.elsevier.com/books/handbook-of-constraint-programming/rossi/978-0-444-52726-4[Handbook
on Constraint Programming].
The challenge is to place two equal-sized armies of white and black
queens onto a chessboard. We can distinguish between two problems:
* checking whether two armies of n queens can be placed on a dim*dim
chessboard,
* for a given board of size dim*dim find the maximal size n of armies
that can be placed onto the board, i.e., solving an optimisation
problem.
[[checking]]
== Checking
Here is a B model for the checking problem. The problem is quite
straightforward to encode in B. Many lines below (in the DEFINITIONS)
just define the <<graphical-visualization,animation function to
graphically represent solutions>>.
....
MACHINE JustQueens
DEFINITIONS
SET_PREF_TIME_OUT == 1000000;
SET_PREF_MAX_INITIALISATIONS == 1;
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif";
ANIMATION_IMG2 == "images/sm_queen_white.gif";
ANIMATION_IMG3 == "images/sm_queen_black.gif";
ANIMATION_IMG4 == "images/sm_knight_white.gif";
ANIMATION_IMG5 == "images/sm_knight_black.gif";
ANIMATION_IMG6 == "images/sm_white_queen_white.gif";
ANIMATION_IMG7 == "images/sm_white_queen_black.gif";
BWOFFSET(xx,yy) == (xx+yy) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..dim & c:1..dim & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( UNION(k).(k:1..n| {(blackc(k),blackr(k),2+BWOFFSET(blackc(k),blackr(k)))}) \/
UNION(k).(k:1..n| {(whitec(k),whiter(k),6+BWOFFSET(whitec(k),whiter(k)))}) );
ORDERED(c,r) == (!i.(i:1..(n-1) => c(i) <= c(i+1)) &
!i.(i:1..(n-1) => (c(i)=c(i+1) => r(i) < r(i+1))))
CONSTANTS n, dim, blackc, blackr, whitec, whiter
PROPERTIES
n = 8 & dim = 8 &
blackc : 1..n --> 1..dim &
whitec : 1..n --> 1..dim &
blackr : 1..n --> 1..dim &
whiter : 1..n --> 1..dim &
ORDERED(blackc,blackr) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec,whiter) &
!(i,j).(i:1..n & j:1..n => blackc(i) /= whitec(j)) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j)) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j) + (blackc(i)-whitec(j))) &
!(i,j).(i:1..n & j:1..n => blackr(i) /= whiter(j) - (blackc(i)-whitec(j))) &
whitec(1) < blackc(1) /* symmetry breaking */
END
....
Here are some running times on my MacBook Air 1.7 GHz i7, also comparing
to using <<using-prob-with-kodkod,Kodkod as ProB's backend>> and
using an http://alloy.mit.edu/alloy/[Alloy] model (see below).
....
dim=7, n=7 : solved in 0.3 secs
dim=7, n=8 : unsat in 20 secs
dim=8, n=6 : solved in 0.02 secs (1.12 secs with Kodkod)
dim=8, n=7 : solved in 0.06 secs (2.66 secs with Kodkod)
dim=8, n=8 : solved in 0.53 secs (8.44 secs with Kodkod; 7.03 secs second run; +/- 8.5 with Alloy & miniSat; 9.3 seconds if we avoid overflows)
dim=8, n=9 : solved in 12.96 secs (128.07 secs with Kodkod ; +/- 84 secs with Alloy & miniSat)
dim=8, n=10 : unsat in 728 secs (Alloy & miniSat still running after over four hours)
....
The first solution found for dim=8 and n=9 is as follows:
image::ProB_PeaceableQueens_8_9_Screenshot.png[]
[[the-alloy-model-for-comparison]]
=== The Alloy model for comparison
Here is the http://alloy.mit.edu/alloy/[Alloy] model we have used.
Initially, the model gave us wrong solutions as we were using `+`
instead of `sum`; this was correct for previous versions of Alloy but
not for Alloy 4.2 which we were using.
....
abstract sig Queens {
row : one Int,
col: one Int,
} {
row >= 0 and row < 8
and col >= 0 and col < 8
}
sig BQueens extends Queens {} {}
sig WQueens extends Queens {} {}
pred nothreat(q1,q2 : Queens) {
q1.row != q2.row
and q1.col != q2.col
and plus[ int[q1.row] , int[q1.col]] != plus[ int[q2.col] , int[q2.row]]
and plus [int[q1.row] , int[q2.col]] != plus[ int[q1.col] , int[q2.row]]
}
pred nothreats { all q1:BQueens, q2:WQueens |
nothreat[q1, q2]
}
pred alldiffB { all q1:BQueens, q2:BQueens |
q1=q2 or q1.row != q2.row or q1.col != q2.col
}
pred alldiffW { all q1:WQueens, q2:WQueens |
q1=q2 or q1.row != q2.row or q1.col != q2.col
}
pred equalnum {
#(WQueens) = #(BQueens)
}
pred valid {
nothreats and equalnum and alldiffB and alldiffW
}
fact {
#Queens = 16
}
run valid for 16 Queens, 7 int
....
[[optimization]]
== Optimization
One can obviously use the above models to try and manually find a
maximal value of n for a given board size dim. Below, we have encoded
this process as B constraints, by setting up the problem twice: once for
the army size n and a second time for army size n+1. The second encoding
is wrapped into a negated existential quantification. (This model can no
longer be translated into Kodkod because of this.)
ProB solves this optimisation problem in about 780 seconds for a board
size of 8. This is very competitive with the timings reported in the
above mentioned constraint solving paper using new symmetry breaking
techniques and much more low-level encoding on state of the art
constraint solving libraries such as ILOG.
....
MACHINE JustQueens_FindOptimal_CBC
DEFINITIONS
SET_PREF_TIME_OUT == 1000000;
SET_PREF_MAX_INITIALISATIONS == 1;
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif";
ANIMATION_IMG2 == "images/sm_queen_white.gif";
ANIMATION_IMG3 == "images/sm_queen_black.gif";
ANIMATION_IMG4 == "images/sm_knight_white.gif";
ANIMATION_IMG5 == "images/sm_knight_black.gif";
ANIMATION_IMG6 == "images/sm_white_queen_white.gif";
ANIMATION_IMG7 == "images/sm_white_queen_black.gif";
BWOFFSET(xx,yy) == (xx+yy) mod 2;
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..dim & c:1..dim & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( UNION(k).(k:1..n| {(blackc(k),blackr(k),2+BWOFFSET(blackc(k),blackr(k)))}) \/
UNION(k).(k:1..n| {(whitec(k),whiter(k),6+BWOFFSET(whitec(k),whiter(k)))}) );
ORDERED(c,r,nn) == (!i.(i:1..(nn-1) => c(i) <= c(i+1)) &
!i.(i:1..(nn-1) => (c(i)=c(i+1) => r(i) < r(i+1))));
CHECK_TYPE(bc,br,wc,wr,nn) == (
bc : 1..nn --> 1..dim &
wc : 1..nn --> 1..dim &
br : 1..nn --> 1..dim &
wr : 1..nn --> 1..dim );
CHECK_DIAGONALS(bc,br,wc,wr,nn) == (
!(i,j).(i:1..nn & j:1..nn => bc(i) /= wc(j)) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j)) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j) + (bc(i)-wc(j))) &
!(i,j).(i:1..nn & j:1..nn => br(i) /= wr(j) - (bc(i)-wc(j)))
)
CONSTANTS n, dim, blackc, blackr, whitec, whiter
PROPERTIES
n : 1..16 & dim = 8 &
CHECK_TYPE(blackc, blackr, whitec, whiter, n) &
ORDERED(blackc,blackr,n) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec,whiter,n) &
CHECK_DIAGONALS(blackc, blackr, whitec, whiter, n) &
whitec(1) < blackc(1) /* symmetry breaking */ &
/* Repeat constraints for n+1 and assert that it cannot be solved */
not( #(n1,blackc1, blackr1, whitec1, whiter1).
(n1=n+1 & /* n1:2..17 & */
CHECK_TYPE(blackc1, blackr1, whitec1, whiter1, n1) &
ORDERED(blackc1,blackr1,n1) & /* ensures proper ordering + that we do not place two queens on same square */
ORDERED(whitec1,whiter1,n1) &
CHECK_DIAGONALS(blackc1, blackr1, whitec1, whiter1, n1) &
whitec1(1) < blackc1(1) /* symmetry breaking */
)
)
END
....
Here are the solving times for various board sizes on my MacBook Air:
....
dim=5 --> optimum n=4 found in 0.18 secs
dim=6 --> optimum n=5 found in 1.16 secs
dim=7 --> optimum n=7 found in 21.174 secs
dim=8 --> optimum n=9 found in 780.130 secs
....
The first solution found for dim=8 is as follows:
image::ProB_PeaceableQueens_8_9_Opt_Screenshot.png[]
src/docs/chapter/model_examples/Proving_Theorems_in_the_ProB_REPL.adoc deleted 100644 → 0
+ 0
− 197
View file @ dccded69
[[proving-theorems-in-prob-repl]]
= Proving Theorems in ProB REPL
For this example we try and use the REPL (Read-Eval-Print-Loop) of ProB
to prove theorems. The REPL can either be started using probcli's
command `-repl` or by starting the <<eval-console,Eval Console in
ProB Tcl/Tk>>.
See the beginning of <<sudoku-solved-in-the-prob-repl,Sudoku Solved
in the ProB REPL>> for more details about how to start the REPL.
The general principle for proving a sequent `Hyp |- Goal` is to state
the hypotheses `Hyp` and negate the goal. If ProB finds a solution, a
counter example to the sequent exists and it cannot be proven. If ProB
finds no solution, then under certain circumstances the sequent is
proven, as no counter example exists. (This mechanism is used by the
<<tutorial-disprover,ProB Disprover in Rodin>>.)
Let us prove that from `x:1..100` it follows that the equation
`x*x+2*x+2 = 1` has no solution:
....
>>> x:1..100 & not(x*x+2*x+2/=1)
Existentially Quantified Predicate over x is FALSE
....
In this case, ProB has not generated an "enumeration warning", i.e.,
all cases where considered: we have a proof. In general when all
variables are restricted to a finite set of values in the hypotheses,
ProB can be used as a prover.
Let us now lift the finiteness restriction on `x` and prove the theorem
for all integer values:
....
>>> x:INTEGER & not(x*x+2*x+2/=1)
### Warning: enumerating x : INTEGER : inf: -1 ---> -1: -1
Existentially Quantified Predicate over x is TRUE
Solution:
x = -1
....
Here ProB has found a counter example and the sequent is not valid. As
you can see, an enumeration warning occurred; meaning that not all of
the infinitely many values for `x` will be tried. But this warning is
not relevant here as a solution was found.
Let us try and restrict `x` to positive values; the number of values are
infinite (`NATURAL` is the set of mathematical natural numbers, not
restricted by `MAXINT`):
....
>>> x:NATURAL & not(x*x+2*x+2/=1)
Existentially Quantified Predicate over x is FALSE
....
Here ProB has found no solution and generated no enumeration warning:
the sequent is proven.
Now let us try and prove that `x>=y` follows from `x>y`:
....
>>> x>y & not(x>=y)
% Timeout when posting constraint:
% kernel_objects:(_15735#>0)
### Warning: enumerating x : INTEGER : inf:sup ---> -1:3
% Timeout when posting constraint:
% kernel_objects:(_15735#<0)
Existentially Quantified Predicate over x,y is UNKNOWN [FALSE with ** ENUMERATION WARNING **]
....
As you can see, here the solver was not able to detect the inconsistency
and prove the sequent over the unbounded integers x and y. There are two
things one can try. First, one can enable some additional constraint
propagation rules (implemented using the Constraint Handling Rules
library of Prolog) in the standard ProB kernel by setting the CHR
preference to TRUE:
....
>>> -p CHR TRUE
Executing probcli command: [set_pref(CHR,TRUE)]
>>> x>y & not(x>=y)
Existentially Quantified Predicate over x,y is FALSE
....
This has enabled us to prove the sequent. (The ProB
<<tutorial-disprover,Disprover>> automatically sets this preference
for you.) Another solution is again to use the Z3 backend:
....
>>> :z3 x>y & not(x>=y)
PREDICATE is FALSE
....
[[user-defined-sets]]
=== User-Defined Sets
Suppose we want to prove a property not over a specific set such as the
integers but over an arbitrary set. If you want to use additional basic
types in the ProB REPL you need to define them in a B machine, they
cannot (yet) be added in the REPL. For example, let us create a file
`DefSets.mch`:
....
MACHINE DefSets
SETS D;E = {e1,e2,e3,e4,e5} // we just define two sets to be used in the REPL, D is deferred, E is enumerated
END
....
Then you can load the file and start the REPL:
`rlwrap probcli DefSets.mch -repl`
Let us try and prove that `A={a,b} & B={c,d}` implies `A /\ B = {}`. We
can state this as follows. Note that in B we need to type A and B. Here
we first use the enumerated set E for that purpose.
....
>>> A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} )
Existentially Quantified Predicate over A,B,a,b,c,d is TRUE
Solution:
A = {e1} &
B = {e1} &
a = e1 &
b = e1 &
c = e1 &
d = e1
....
As you can see, the goal `A /\ B = {}` cannot be proven, a
counter-example is provided. If we add hypotheses that a,b,c,d are all
pair-wise distinct we can prove the assertion:
....
>>> A <: E & B<: E & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d & not( A /\ B = {} )
Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
....
This has used ProB’s Prolog-CLPFD solver. You can use ProB's translation
to Z3 (see <<using-prob-with-z3,Using ProB with Z3>>) by prefixing
the formula with `z3:`
....
>>> :z3 A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
PREDICATE is FALSE
....
You can also translate the query to SAT via the Kodkod library (see
<<using-prob-with-kodkod,Using ProB with KODKOD>>) using:
....
>>> :kodkod A <: E & B<: E & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
kodkod ok: A = {a,b} & B = {c,d} & not(A /\ B = {}) & a /= b ... ints: none, intatoms: none
Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).
Times for computing solutions: []
Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
....
Note that ProB’s Prolog-CLPFD solver and Kodkod cannot provide proofs
when you use deferred sets whose cardinality is not specified and
finite. For example, let us use the deferred set D instead of E to type
A and B:
....
>>> A <: D & B<: D & A={a,b} & B={c,d} & not( A /\ B = {} ) & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
>>> D
Expression Value =
{D1,D2}
....
As you can see, ProB has set the size of the set D to two (see
<<deferrred-sets,Deferrred_Sets>>). You can see this also by asking
ProB to find four different Values:
....
>>> A <: D & B<: D & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
Existentially Quantified Predicate over A,B,a,b,c,d is FALSE
....
So, in the presence of deferred sets, ProB's default solver and the
Kodkod-based solver cannot be used to prove theorems; they can only be
used to find counter-examples. The Z3 backend however does not fix the
size of D:
....
>>> :z3 A <: D & B<: D & A={a,b} & B={c,d} & a/=b & a/=c & a/=d & b/=c & b/=d & c/=d
PREDICATE is TRUE
Solution:
A = {D1,D2}
B = {}
a = D1
b = D2
c = D3
d = D4
....
src/docs/chapter/model_examples/Rush_Hour_Puzzle.adoc deleted 100644 → 0
+ 0
− 728
View file @ dccded69
This diff is collapsed.
src/docs/chapter/model_examples/Rush_Hour_XTL.adoc deleted 100644 → 0
+ 0
− 347
View file @ dccded69
[[rush-hour-xtl]]
= Rush Hour XTL
This case studies tackles encoding the
https://en.wikipedia.org/wiki/Rush_Hour_(puzzle)[rush hour board
game] in which cars are packed on a 6-by-6 grid and can either move
horizontally or vertically. The goal is to move the red car to the exit.
In this particular instance we try to solve the
http://www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40[hardest
puzzle of the original game Nr. 40].
This is a <<other-languages,Prolog XTL encoding>> of the
<<rush-hour-puzzle,B solution which is also available>>. On the
Prolog XTL encoding presented here ProB finds the example in one second
(on a Mac Book Air, 1.7 GHz i7), on the B version it takes ProB about 10
seconds (but the TLC backend is faster). Part of the B models are shown
in comments for reference below. This file needs to be saved with a `.P`
extension so that it can be loaded by <<installation,ProB Tcl/Tk>> or
<<using-the-command-line-version-of-prob,probcli>>.
Observe how we use sort and ord_add_element to avoid multiple versions
of the same state. The important predicates that ProB uses are
`start/1`, `trans/3` and `prop/2`.
....
/* a Prolog XTL translation of the more elegant encoding of the Rush Hour puzzle */
/* Michael Leuschel, July 2014 */
/* ProB finds solution in about 0.5 - 1 second *using mixed DF/BF search */
/* Using BF search it takes 1.3 seconds */
/* This shows the potential of compiling the ProB B interpreter down to Prolog */
/* The Prolog could still be optimized further (e.g. run through a partial evaluator ) */
%:- use_module(library(lists)). % not needed when run from ProB
%:- use_module(library(ordsets)). % not needed when run from ProB
sze([2,2,2,2,2, 2,2,2,2, 3,3,3, 2]). /* the sizes of the cars */
dir([v,v,v,v,v, h,h,h,h, v,v,h, h]). /* indicating whether the cars move vertically or horizontally */
red(Len) :- sze(S), length(S,Len). /* the last car is the red one */
dim(5). /* the grid goes from 0..dim */
free_initial([(0,3),(1,3), (0,5), (3,4),(4,0),(4,1),(5,5)]).
col_initial([(1),(2),(2),(3),(4), /* vertical 2-size cars */
(0),(1),(3),(4), /* horiz. 2-size cars */
(0),(5), /* vertical 3-size cars */
(0), /* horiz. 3-size cars */
(3)] /* red car */
).
row_initial([(1),(1),(4),(3),(0),
(5),(0),(5),(4),
(0),(1),
(3),
(2)]).
init(S) :- start(S).
start(rcf(Rows,Cols,SFree)) :- free_initial(Free),
sort(Free,SFree),
row_initial(Rows),
col_initial(Cols).
prop(rcf(_,_,Free),free(I,J)) :- member((I,J),Free).
prop(rcf(Rows,Cols,_),car(Car,Row,Col)) :- nth1(Car,Rows,Row),nth1(Car,Cols,Col).
/*
prop(rcf(_,_,Free),unsafe) :- member((N,M),Free), (N>5 ; N<0 ; M>5 ; M<0).
prop(rcf(Rows,_,_),unsafe) :- member(N,Rows), (N>5 ; N<0).
prop(rcf(_,Cols,_),unsafe) :- member(N,Cols), (N>5 ; N<0).
*/
prop(rcf(_Rows,Cols,_Free),unsafe) :- last(Cols,4). /* The target : move red car to the right */
% utility for updating lists of columns/rows:
replace([_|T],1,New,Res) :- !, Res=[New|T].
replace([H|T],N,New,[H|TR]) :- N1 is N-1, replace(T,N1,New,TR).
trans(mv_down(Car,F),rcf(Rows,Cols,Free),rcf(Rows1,Cols,SFree1)) :-
dir(Dir),
nth1(Car,Dir,v),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
sze(Sze),
nth1(Car,Sze,SC),
FR is RC+SC, F = (FR,CC),
select(F,Free,Free0),
ord_add_element(Free0,(RC,CC),SFree1),
RC1 is RC+1,
replace(Rows,Car,RC1,Rows1).
/*
mv_down(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)+sze(c)|->col(c) &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)} ||
row(c) := row(c)+1
END;
*/
trans(mv_up(Car,F),rcf(Rows,Cols,Free),rcf(Rows1,Cols,SFree1)) :-
dir(Dir),
nth1(Car,Dir,v),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
FR is RC-1, F = (FR,CC),
select(F,Free,Free0),
sze(Sze),
nth1(Car,Sze,SC),
RSC1 is RC+SC-1,
ord_add_element(Free0,(RSC1,CC),SFree1),
replace(Rows,Car,FR,Rows1).
/*
mv_up(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)-1|->col(c) &
F : free THEN
free := free - {F} \/ {row(c)+sze(c)-1|->col(c)} ||
row(c) := row(c)-1
END; */
trans(mv_right(Car,F),rcf(Rows,Cols,Free),rcf(Rows,Cols1,SFree1)) :-
dir(Dir),
nth1(Car,Dir,h),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
sze(Sze),
nth1(Car,Sze,SC),
CCS is CC+SC, F = (RC,CCS),
select(F,Free,Free0),
ord_add_element(Free0,(RC,CC),SFree1),
CC1 is CC+1,
replace(Cols,Car,CC1,Cols1).
/*
mv_right(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)+sze(c) &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)} ||
col(c) := col(c)+1
END; */
trans(mv_left(Car,F,RC,CC,SC,CCS),rcf(Rows,Cols,Free),rcf(Rows,Cols1,SFree1)) :-
dir(Dir),
nth1(Car,Dir,h),
nth1(Car,Rows,RC),
nth1(Car,Cols,CC),
CC1 is CC-1, F = (RC,CC1),
select(F,Free,Free0),
sze(Sze),
nth1(Car,Sze,SC),
CCS is CC1+SC,
ord_add_element(Free0,(RC,CCS),SFree1),
replace(Cols,Car,CC1,Cols1).
/*
mv_left(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)-1 &
F : free THEN
free := free - {F} \/ {row(c)|->col(c)+sze(c)-1} ||
col(c) := col(c)-1
END
END
*/
....
We can also add a simple <<graphical-visualization,graphical
visualisation>> by including the following in the XTL file (using the
`animation_function_result` predicate recognised by ProB as of version
1.4.0-rc3):
....
% Graphical Visualization Animation Function:
is_index(I,I).
is_index(I,Res) :- dim(N), I<N, I1 is I+1, is_index(I1,Res).
animation_function_result(State,Matrix) :-
findall(((RowNr,ColNr),Cell), (is_index(0,RowNr),is_index(0,ColNr),
cell_content(State,RowNr,ColNr,Cell)),Matrix).
cell_content(rcf(Rows,Cols,Free),Row,Col,'--') :- member((Row,Col),Free).
cell_content(rcf(Rows,Cols,Free),Row,Col,Car) :- nth1(Car,Rows,Row), nth1(Car,Cols,Col).
cell_content(rcf(Rows,Cols,Free),Row1,Col,Car) :- dir(Dir),
sze(Sze),
nth1(Car,Dir,v),
nth1(Car,Sze,SC),
nth1(Car,Rows,Row), nth1(Car,Cols,Col),
(Row1 is Row+1 ; SC>2, Row1 is Row+2).
cell_content(rcf(Rows,Cols,Free),Row,Col1,Car) :- dir(Dir),
sze(Sze),
nth1(Car,Dir,h),
nth1(Car,Sze,SC),
nth1(Car,Rows,Row), nth1(Car,Cols,Col),
(Col1 is Col+1 ; SC>2, Col1 is Col+2).
....
Here is a screenshot of ProB after finding the shortest solution using
model checking. You can see the (simple)
<<graphical-visualization,graphical visualisation>> of the state of
the model.
image:ProB_RushHour_XTL_Screenshot.png[600px|center]
[[running-using-probcli]]
== Running using probcli
Here is how you can find the solution using
<<using-the-command-line-version-of-prob,probcli>> (run on a Mac Book
Air, 1.7 GHz i7):
----
$ probcli -mc 100000 RushHour_Prolog.P -bf
tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
found_error(xtl_error,3026)
finding_trace_from_to(root)
....................
Model Checking Time: 1310 ms
States analysed: 3026
Transitions fired: 19821
*** COUNTER EXAMPLE FOUND ***
xtl_error
*** TRACE:
1: start_xtl_system:
2: mv_right(8,(5,5)):
3: mv_down(4,(5,3)):
4: mv_up(11,(0,5)):
5: mv_right(12,(3,3)):
6: mv_down(10,(3,0)):
7: mv_left(7,(0,0),0,1,2,2):
8: mv_right(12,(3,4)):
9: mv_up(2,(0,2)):
10: mv_down(1,(3,1)):
11: mv_down(10,(4,0)):
12: mv_right(12,(3,5)):
13: mv_left(13,(2,2),2,3,2,4):
14: mv_down(1,(4,1)):
15: mv_up(3,(3,2)):
16: mv_right(6,(5,2)):
17: mv_left(13,(2,1),2,2,2,3):
18: mv_down(10,(5,0)):
19: mv_left(13,(2,0),2,1,2,2):
20: mv_down(2,(2,2)):
21: mv_right(7,(0,2)):
22: mv_down(5,(2,4)):
23: mv_right(7,(0,3)):
24: mv_right(7,(0,4)):
25: mv_up(2,(0,2)):
26: mv_right(13,(2,2)):
27: mv_up(10,(2,0)):
28: mv_left(6,(5,0),5,1,2,2):
29: mv_down(3,(5,2)):
30: mv_left(12,(3,2),3,3,3,5):
31: mv_right(13,(2,3)):
32: mv_up(1,(2,1)):
33: mv_up(1,(1,1)):
34: mv_left(12,(3,1),3,2,3,4):
35: mv_up(10,(1,0)):
36: mv_up(10,(0,0)):
37: mv_up(1,(0,1)):
38: mv_left(12,(3,0),3,1,3,3):
39: mv_up(4,(3,3)):
40: mv_left(13,(2,1),2,2,2,3):
41: mv_up(4,(2,3)):
42: mv_up(4,(1,3)):
43: mv_right(12,(3,3)):
44: mv_down(10,(3,0)):
45: mv_down(11,(3,5)):
46: mv_right(7,(0,5)):
47: mv_up(4,(0,3)):
48: mv_right(13,(2,3)):
49: mv_right(12,(3,4)):
50: mv_down(1,(2,1)):
51: mv_down(1,(3,1)):
52: mv_down(1,(4,1)):
53: mv_left(13,(2,1),2,2,2,3):
54: mv_down(4,(2,3)):
55: mv_left(7,(0,3),0,4,2,5):
56: mv_up(11,(0,5)):
57: mv_right(12,(3,5)):
58: mv_up(3,(3,2)):
59: mv_right(6,(5,2)):
60: mv_down(10,(4,0)):
61: mv_down(10,(5,0)):
62: mv_left(13,(2,0),2,1,2,2):
63: mv_down(2,(2,2)):
64: mv_left(7,(0,2),0,3,2,4):
65: mv_left(7,(0,1),0,2,2,3):
66: mv_left(7,(0,0),0,1,2,2):
67: mv_up(2,(0,2)):
68: mv_right(13,(2,2)):
69: mv_left(9,(4,3),4,4,2,5):
70: mv_up(10,(2,0)):
71: mv_left(6,(5,0),5,1,2,2):
72: mv_up(4,(0,3)):
73: mv_right(13,(2,3)):
74: mv_left(8,(5,3),5,4,2,5):
75: mv_down(3,(5,2)):
76: mv_left(12,(3,2),3,3,3,5):
77: mv_down(11,(3,5)):
78: mv_down(11,(4,5)):
79: mv_up(5,(0,4)):
80: mv_right(13,(2,4)):
81: mv_down(11,(5,5)):
82: mv_right(13,(2,5)):
! *** error occurred ***
! xtl_error
----
The full states has 4781 states (including the root node) and 29889
transitions. This is the output of ProB's coverage statistics:
----
STATES
deadlocked:0
open:0
live:4781
total:4781
TOTAL_OPERATIONS
29889
COVERED_OPERATIONS
mv_down:8461
mv_left:6483
mv_right:6483
mv_up:8461
start_xtl_system:1
UNCOVERED_OPERATIONS
----
Complete model checking, without looking for goal states, takes 1.6
seconds (on a Mac Book Air, 1.7 GHz i7):
----
$ probcli -mc 100000 RushHour_Prolog.P -noinv --coverage
tcltk_open_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
new_xtl_file(/Users/leuschel/git_root/prob_examples/public_examples/B/Puzzles/RushHour/RushHour_Prolog.P)
% All open nodes visited
Model Checking Time: 1610 ms
States analysed: 4780
Transitions fired: 29889
No Counter Example found. ALL nodes visited.
Coverage:
[STATES,deadlocked:0,open:0,live:4781,total:4781,TOTAL_OPERATIONS,29889,COVERED_OPERATIONS,mv_down:8461,mv_left:6483,mv_right:6483,mv_up:8461,start_xtl_system:1,UNCOVERED_OPERATIONS]
----
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment