From 7f54a9798cf071eecc5e64d1e97f7ea4ee302eb4 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Mon, 4 Jun 2018 23:17:03 +0200
Subject: [PATCH] update presentation
---
notebooks/presentations/SETS_RODIN18.ipynb | 612 ++++++++++++++----
.../presentations/img/inputoutputflow.pdf | Bin 0 -> 14906 bytes
2 files changed, 485 insertions(+), 127 deletions(-)
create mode 100644 notebooks/presentations/img/inputoutputflow.pdf
diff --git a/notebooks/presentations/SETS_RODIN18.ipynb b/notebooks/presentations/SETS_RODIN18.ipynb
index 7004a21..dba64d2 100644
--- a/notebooks/presentations/SETS_RODIN18.ipynb
+++ b/notebooks/presentations/SETS_RODIN18.ipynb
@@ -121,7 +121,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 14,
"metadata": {
"slideshow": {
"slide_type": "-"
@@ -132,11 +132,11 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 13:54:14,028, T+23877] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 13:54:15,603, T+25452] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62613\n",
- "[2018-06-04 13:54:15,605, T+25454] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47762\n",
- "[2018-06-04 13:54:15,609, T+25458] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 13:54:15,624, T+25473] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-04 17:10:21,614, T+7877565] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
+ "[2018-06-04 17:10:22,773, T+7878724] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57165\n",
+ "[2018-06-04 17:10:22,774, T+7878725] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52908\n",
+ "[2018-06-04 17:10:22,782, T+7878733] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-04 17:10:22,792, T+7878743] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
]
},
{
@@ -145,7 +145,7 @@
"Loaded machine: MyBasicSets : []\n"
]
},
- "execution_count": 4,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -741,7 +741,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Function application:"
]
@@ -761,7 +765,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
"source": [
"Relational inverse (.~) and relational image .[.] :"
]
@@ -985,7 +993,17 @@
"source": [
"## Constraint Solving Applications ##\n",
"Constraint solving has many applications in formal methods in general and B in particular.\n",
- "\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
"#### Animation ####\n",
"It is required to animate implicit specifications.\n",
"Take for example an event\n",
@@ -1150,7 +1168,11 @@
{
"cell_type": "code",
"execution_count": 32,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "skip"
+ }
+ },
"outputs": [
{
"data": {
@@ -1173,7 +1195,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
@@ -1192,13 +1214,13 @@
"\tO = 0"
]
},
- "execution_count": 33,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ "{S,E,N,D, M,O,R, Y} ⊆ 0..9 & S >0 & M >0 & \n",
" card({S,E,N,D, M,O,R, Y}) = 8 & \n",
" S*1000 + E*100 + N*10 + D +\n",
" M*1000 + O*100 + R*10 + E =\n",
@@ -1207,7 +1229,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single soltuion:"
]
@@ -1237,6 +1263,37 @@
" M*10000 + O*1000 + N*100 + E*10 + Y }"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|S|E|N|D|M|O|R|Y|\n",
+ "|---|---|---|---|---|---|---|---|---|\n",
+ "|1|9|5|6|7|1|0|8|2|\n"
+ ],
+ "text/plain": [
+ "Nr\tS\tE\tN\tD\tM\tO\tR\tY\n",
+ "1\t9\t5\t6\t7\t1\t0\t8\t2\n"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {S,E,N,D, M,O,R, Y |\n",
+ " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " card({S,E,N,D, M,O,R, Y}) = 8 & \n",
+ " S*1000 + E*100 + N*10 + D +\n",
+ " M*1000 + O*100 + R*10 + E =\n",
+ " M*10000 + O*1000 + N*100 + E*10 + Y }"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -1331,13 +1388,27 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"### Booleans ###\n",
"\n",
"If we have only booleans, constraint solving is equivalent to SAT solving.\n",
"Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.\n",
- "(We do not translate to CNF also because of well-definedness issues.)\n",
+ "(We do not translate to CNF also because of well-definedness issues.)\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
"\n",
"#### Knights and Knave Puzzle####\n",
"Here is a puzzle from Smullyan involving an island with only knights and knaves.\n",
@@ -1356,7 +1427,11 @@
{
"cell_type": "code",
"execution_count": 37,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
"outputs": [
{
"data": {
@@ -1391,45 +1466,7 @@
"\n",
"Let us take the integer constraint ```x*x=100``` which we saw earlier.\n",
"This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.\n",
- "So, let us first look at some simpler constraints, where the domains of the variables are all bounded.\n",
- "Let us consider a small arithmetic puzzle \n",
- "```\n",
- " X Y\n",
- "+ X Y\n",
- "-----\n",
- " Y 0\n",
- "```"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 38,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tX = 2\n",
- "\tY = 5"
- ]
- },
- "execution_count": 38,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "X:1..9 & Y:0..9 & X*10 + Y + X*10 + Y = Y*10"
- ]
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "Given that we know the domain of X and Y one can represent the integers by binary numbers and convert the constraint to a SAT problem."
+ "So, let us first look at some simpler constraints, where the domains of the variables are all bounded."
]
},
{
@@ -1440,7 +1477,8 @@
}
},
"source": [
- "Let us look at an even simpler constraint X:0..3 & Y:0..3 & X+Y=2. As you can see there are three solutions for this constraint:\n"
+ "Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.\n",
+ "As you can see there are three solutions for this constraint:\n"
]
},
{
@@ -1472,11 +1510,15 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"#### Solving constraints by translating to SAT ####\n",
- "Given that we know the domain of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2``` one can represent the integers by binary numbers and convert the constraint to a SAT problem.\n",
- "The number 2 is 10 in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n",
+ "Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.\n",
+ "The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n",
"We can translate the addition to a propositional logic formula:\n",
"\n",
"Bit1 | Bit0\n",
@@ -1486,7 +1528,7 @@
" |\n",
" Z1 | Z0\n",
" \n",
- "Let us find one solution to this constraint, by encoding addition using an additional carry bit:"
+ "Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:"
]
},
{
@@ -1525,7 +1567,11 @@
{
"cell_type": "code",
"execution_count": 41,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"data": {
@@ -1557,7 +1603,11 @@
{
"cell_type": "code",
"execution_count": 42,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
"outputs": [
{
"data": {
@@ -1602,7 +1652,11 @@
{
"cell_type": "code",
"execution_count": 43,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"name": "stdout",
@@ -1676,12 +1730,28 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"#### Translation to SMTLib ####\n",
- "At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the Z3 or CVC4 SMT solver.\n",
- "Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports integer predicates and operators in the language.\n",
- "Here is ProB's SMTLib/Z3 API calls for the constraint:\n",
+ "At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.\n",
+ "Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.\n",
+ "\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:\n",
"- mk_var(integer,x) $\\rightarrow$ 2\n",
"- mk_var(integer,y) $\\rightarrow$ 3\n",
"- mk_int_const(0) $\\rightarrow$ 4\n",
@@ -1726,7 +1796,7 @@
"cell_type": "markdown",
"metadata": {
"slideshow": {
- "slide_type": "subslide"
+ "slide_type": "slide"
}
},
"source": [
@@ -1749,11 +1819,34 @@
" - x=2 $\\leadsto$ x:2..2, y:0..0"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Let us now examine the three approaches for the KISS-PASSION puzzle:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": 17,
"metadata": {},
"outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.050491290 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.050491290 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
{
"data": {
"text/plain": [
@@ -1769,46 +1862,63 @@
"\tO = 8"
]
},
- "execution_count": 46,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
+ ":time :solve prob {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
]
},
{
"cell_type": "code",
- "execution_count": 47,
- "metadata": {},
+ "execution_count": 18,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
]
}
],
"source": [
- ":solve z3 {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
+ ":time :solve z3 {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
]
},
{
"cell_type": "code",
- "execution_count": 48,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:01:42,085, T+471934] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
- "[2018-06-04 14:01:42,086, T+471935] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [373]\u001b[0m\n"
+ "[2018-06-04 21:43:31,067, T+24267018] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
+ "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
+ "[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [636]\u001b[0m\n"
]
},
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 2.287290784 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 2.287290784 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
{
"data": {
"text/plain": [
@@ -1824,18 +1934,22 @@
"\tO = 8"
]
},
- "execution_count": 48,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":solve kodkod {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
+ ":time :solve kodkod {K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
]
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Result for KISS*KISS=PASSION puzzle:\n",
"\n",
@@ -1848,7 +1962,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"### Unbounded integers ###\n",
"The SAT translation via Kodkod/Alloy requires to determine the bid width.\n",
@@ -2020,7 +2138,8 @@
}
},
"source": [
- "Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation. ProB can detect it with CHR enabled, but without the module the result is **UNKNOWN**."
+ "Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.\n",
+ "ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**."
]
},
{
@@ -2072,7 +2191,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"### Summary for Integer Arithmetic ###\n",
"\n",
@@ -2195,7 +2318,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"This translation to SAT is exactly what the Kodkod backend does:"
]
@@ -2299,7 +2426,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Also, in the following constraint, the set x is unbounded and no translation to SAT is feasible (without a very clever analysis of the universal implications)."
]
@@ -2327,6 +2458,61 @@
"{100}:x & !y.(y:x => (!z.(z:y => y \\/ {z / 2}:x)))"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "However, when it is applicable the propositional encoding of sets can be very effective for SAT solvers.\n",
+ "The following example, involving various relational operators can currently only be solved by our Kodkod backend:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-06-04 21:54:17,800, T+24913751] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: r : 1 .. 5 <-> 1 .. 5 & (r ; r) = r & r /= {} & do... ints: irange(0,5), intatoms: irange(0,5)\u001b[0m\n",
+ "[2018-06-04 21:54:17,801, T+24913752] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,2,1,1,3,2,1,2,1,1,5,1,1,2,1,2,1,2,1,1,1,1]\u001b[0m\n"
+ ]
+ },
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.153314218 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.153314218 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = {(3↦5),(3↦4),(5↦5),(5↦4),(1↦4),(2↦4),(4↦4)}"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve kodkod r: 1..5 <-> 1..5 & (r;r) = r & r /= {} & dom(r)=1..5 & r[2..3]=4..5"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -2375,7 +2561,11 @@
{
"cell_type": "code",
"execution_count": 64,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "fragment"
+ }
+ },
"outputs": [
{
"data": {
@@ -2437,7 +2627,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"This can be solved by Z3 but not by CVC4. Already the slightly more complicated example from above (or the other examples) cannot be solved:"
]
@@ -2525,7 +2719,11 @@
{
"cell_type": "code",
"execution_count": 67,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"data": {
@@ -2554,7 +2752,11 @@
{
"cell_type": "code",
"execution_count": 68,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"name": "stdout",
@@ -2681,7 +2883,6 @@
},
"source": [
"### ProB's Set Solver ###\n",
- "\n",
"ProB has actually three set representations:\n",
"- Prolog lists of elements\n",
"- AVL trees for fully known sets\n",
@@ -2696,7 +2897,6 @@
"The list representation is used for sets where some of the members are known or partially known.\n",
"\n",
"#### AVL tree representation ####\n",
- "\n",
"The following generates the AVL tree representation:"
]
},
@@ -2871,7 +3071,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:"
]
@@ -2916,7 +3120,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"#### List representation ####\n",
"The list representation is used when a finite set is partially known and constraint solving has to determine the set.\n"
@@ -2927,7 +3135,7 @@
"execution_count": 78,
"metadata": {
"slideshow": {
- "slide_type": "subslide"
+ "slide_type": "fragment"
}
},
"outputs": [
@@ -3148,7 +3356,11 @@
{
"cell_type": "code",
"execution_count": 91,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"ename": "CommandExecutionException",
@@ -3389,7 +3601,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"### Relation to SETLOG ###\n",
"\n",
@@ -3435,7 +3651,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Another example from that paper is\n",
"```\n",
@@ -3611,7 +3831,11 @@
{
"cell_type": "code",
"execution_count": 102,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"name": "stdout",
@@ -3658,13 +3882,34 @@
"- ProB's default backend:\n",
" - can deal with unbounded and large sets\n",
" - limited constraint solving for complex constraints involving image, transitive closure,...\n",
+ " - no learning, backjumping\n",
" - works well for large sets and semi-deterministic computation\n",
" - works well for animation, data validation, disproving\n",
- " - limitations trigger for symbolic model checking (IC3,...)\n",
- " - Future work: improve combination with Z3, improve list representation (maybe use a bit-vector like representation) \n",
+ " - limitations appear for symbolic model checking (IC3,...)\n",
+ " - Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable) \n",
" "
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "### Integrations of Approaches ###\n",
+ "\n",
+ "ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.\n",
+ "Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.\n",
+ "The main motivation was new symbolic validation techniques such as IC3.\n",
+ "\n",
+ "The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.\n",
+ "However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).\n",
+ "\n",
+ "A more promising, fine-grained integration has been presented at PADL'18."
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -3829,7 +4074,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"In the following the inverse operator seems to pose problems to Z3:"
]
@@ -3880,7 +4129,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"### Comparison ###\n",
"Some further examples for comparison of the backends"
@@ -4100,7 +4353,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"#### Graph theorem ####\n",
"\n",
@@ -4109,18 +4366,18 @@
},
{
"cell_type": "code",
- "execution_count": 117,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:09:20,430, T+930279] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 14:09:21,622, T+931471] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63550\n",
- "[2018-06-04 14:09:21,622, T+931471] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47978\n",
- "[2018-06-04 14:09:21,624, T+931473] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 14:09:21,638, T+931487] \"ProB Output Logger for instance 2d81a536\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-04 16:46:59,166, T+6475117] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
+ "[2018-06-04 16:47:00,347, T+6476298] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55595\n",
+ "[2018-06-04 16:47:00,348, T+6476299] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52301\n",
+ "[2018-06-04 16:47:00,350, T+6476301] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-04 16:47:00,364, T+6476315] \"ProB Output Logger for instance ecdd0f\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
]
},
{
@@ -4129,7 +4386,7 @@
"Loaded machine: GraphTheorem : []\n"
]
},
- "execution_count": 117,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -4194,7 +4451,11 @@
{
"cell_type": "code",
"execution_count": 120,
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"name": "stdout",
@@ -4249,7 +4510,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"So with Kodkod we proved the theorem for 5 nodes in about a second.\n",
"What if we remove the self-loops restriction:"
@@ -4325,7 +4590,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
"source": [
"### Benchmark Puzzles ####\n",
"\n",
@@ -4435,7 +4704,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"#### N-Bishops ####\n"
]
@@ -4678,7 +4951,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"#### Datavalidation example ####\n"
]
@@ -4845,18 +5122,18 @@
},
{
"cell_type": "code",
- "execution_count": 139,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-04 14:09:38,543, T+948392] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
- "[2018-06-04 14:09:39,778, T+949627] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63572\n",
- "[2018-06-04 14:09:39,779, T+949628] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47990\n",
- "[2018-06-04 14:09:39,781, T+949630] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-04 14:09:39,798, T+949647] \"ProB Output Logger for instance 1361b11\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-04 15:03:05,856, T+241807] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n",
+ "[2018-06-04 15:03:07,015, T+242966] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51091\n",
+ "[2018-06-04 15:03:07,018, T+242969] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 50312\n",
+ "[2018-06-04 15:03:07,021, T+242972] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-04 15:03:07,034, T+242985] \"ProB Output Logger for instance 5f836b9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
]
},
{
@@ -4865,7 +5142,7 @@
"Loaded machine: signals : []\n"
]
},
- "execution_count": 139,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -5010,8 +5287,89 @@
},
{
"cell_type": "code",
- "execution_count": 142,
+ "execution_count": 5,
"metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|Nr|prj1|prj2|\n",
+ "|---|---|---|\n",
+ "|1|PL01|PL02|\n",
+ "|2|PL02|PL03|\n",
+ "|3|PL03|PL04|\n",
+ "|4|PL04|PL05|\n",
+ "|5|PL05|PL06|\n",
+ "|6|PL06|PL07|\n",
+ "|7|PL07|PL08|\n",
+ "|8|PL08|PL09|\n",
+ "|9|PL09|PL10|\n",
+ "|10|PL10|PL11|\n",
+ "|11|PL11|PL12|\n",
+ "|12|PL12|PL13|\n",
+ "|13|PL13|PL14|\n",
+ "|14|PL14|PL15|\n",
+ "|15|PL15|PL16|\n",
+ "|16|PL16|PL17|\n",
+ "|17|PL17|PL18|\n",
+ "|18|PL18|PL19|\n",
+ "|19|PL19|PL20|\n",
+ "|20|PL20|PL20|\n",
+ "|21|PL30|PL31|\n",
+ "|22|PL31|PL32|\n",
+ "|23|PL33|PL34|\n",
+ "|24|PL34|PL35|\n"
+ ],
+ "text/plain": [
+ "Nr\tprj1\tprj2\n",
+ "1\tPL01\tPL02\n",
+ "2\tPL02\tPL03\n",
+ "3\tPL03\tPL04\n",
+ "4\tPL04\tPL05\n",
+ "5\tPL05\tPL06\n",
+ "6\tPL06\tPL07\n",
+ "7\tPL07\tPL08\n",
+ "8\tPL08\tPL09\n",
+ "9\tPL09\tPL10\n",
+ "10\tPL10\tPL11\n",
+ "11\tPL11\tPL12\n",
+ "12\tPL12\tPL13\n",
+ "13\tPL13\tPL14\n",
+ "14\tPL14\tPL15\n",
+ "15\tPL15\tPL16\n",
+ "16\tPL16\tPL17\n",
+ "17\tPL17\tPL18\n",
+ "18\tPL18\tPL19\n",
+ "19\tPL19\tPL20\n",
+ "20\tPL20\tPL20\n",
+ "21\tPL30\tPL31\n",
+ "22\tPL31\tPL32\n",
+ "23\tPL33\tPL34\n",
+ "24\tPL34\tPL35\n"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {PL01 |-> PL02, PL02 |-> PL03, PL03 |-> PL04, PL04 |-> PL05,\n",
+ " PL05 |-> PL06, PL06 |-> PL07, PL07 |-> PL08, PL08 |-> PL09,\n",
+ " PL09 |-> PL10, PL10 |-> PL11, PL11 |-> PL12, PL12 |-> PL13,\n",
+ " PL13 |-> PL14, PL14 |-> PL15, PL15 |-> PL16, PL16 |-> PL17,\n",
+ " PL17 |-> PL18, PL18 |-> PL19, PL19 |-> PL20, PL20 |-> PL20,\n",
+ " PL30 |-> PL31, PL31 |-> PL32, PL33 |-> PL34, PL34 |-> PL35}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 142,
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"outputs": [
{
"name": "stdout",
diff --git a/notebooks/presentations/img/inputoutputflow.pdf b/notebooks/presentations/img/inputoutputflow.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..6d46a5603ef25a94a12cc7ece12b6de556c5a66b
GIT binary patch
literal 14906
zcmY!laB<T$)HCK%J@WL^)7Q&CFSu~z7?+8HfkJ*#7MG2Ug1%2`UV2G}f~kUmLXd*K
zTV_s4YLSAzTTWt0s!M8eeoCr>ogG(kNl|KIE>{KP+K7{VBJKivpNBswv?#H>9@S^?
z>EH>E2bm`)_44mH%dt39;Pn5~?_Hl<v$Z{Y)agq|O6r=QN=A$J-7x>wUHW6XS^D2i
zx7NRZ`~KVHzc0Vd-rk;n?RI|q=kMQZq`$1aF1tJD&#s%wM^a8NXRo|f*}pt?+piCe
z{kz`ZJ9k^;n#iQD#m6p79oV}pv)FRYvE{k5o~v#XeeFCesp#~9=hren-p=ATbAQv9
zxHWptoo#vt+e*6%<C-$H?Gno4(q3EN*IThqZ}0jLZms#5WpcAhEFLQ)cHeE<_UXp{
z=DqG);-d2HvRLxpt86)U@9ra!Jp$J8%_SDMRHsU`ay+)}aqrodRD9<_QbTucs^8@~
z<}C|99^A9Ribc{eD!a#srQ%IjU~<a#O-X-(l1x6Zx|k>~@~wzn@r!Zxp{r|bW~f!O
z?q;qIju)TRJNNWG#y-)?z7x`mCNXT?;d4&4`NW<Z%;u^I#!6;OufBUU<<cfb!QYGj
zX6{!v`~Lmgv!lkl|7X<S<GvO>W&Nqo3`!Fwoma8lf4e-gf6@WvzLqT$7pGt8H>+S$
z(RO%}bF0fi<axTbd_aWX&xRRBj7cU;9`jb7_h4|i^=;}2mJ=1G9~5WV=(n!$(ARGB
zR1*7f>iV0OeOj?W6JD$k%iub7O8I}si-#RvWsfVGls^d7e3s5RGSNV!MbhbE^0kn4
z+8(;gU*7vUO_C`<Btgn2Nkc%LpV7l?K4)#qqV+0j9&QgMeh4IRx=!X(KjpRcfcU;V
zb?1ebddoR)hp)&KyD~K|{p<Sz(LHj<)D#kD|Cj#|H&y(QNaXW#7k|I{Z2w+f?(ubB
z?`?k!gWlB6P!D-|^YL`{oo25X-8)30Wl~PRZa8!N+MX9ls)wiWW-Zyr!xw!*Gn%nc
zW}6Aerz^o*P8jn!=nA|#_@hDg$;V9%S{`#l0~B4kExH{yFj#4ao>|@0VD?Jpugwj9
z^)DYaV}5HqyTrm|b?CA~6W=;jt|iRp6r%Imo)(0AvWYbcCZ)w3R6C-Scy@DUkk~{g
z)-bt;vsZ{Qtuu7t>ALXGg(L10iwk43=ClCQn|^1qf{wHwH1BjTzA97S@iu7Y+sCJR
zgd-V_or!<G$5Qib{jJ&8<L4{xe{(iH<mLW1|DG<ky4!uqYVj}Y_T4O{3^PlPaJHWm
z7kW4KwR4p4H<O}P0j;;M4y>%)KEciGkyfIQhqU~}*G|lw=`!C1z6kxdk6TwN_aNI%
zruWvAuvs1-vy|QmD|T)!+<oIrw^xz=8Jqc&s@0ZVS-~!SaRSdy@xXKKcUG(X<lh#c
z`n{zoR`vTX1<w_WmOhEw=umu~ZOOL@)sCfNj>{&fe&?E+$yiXE6(_!=HTi>Zgt2<v
zb-kA>E7~KAn(f^?xi0mxIJJ29C|;V=lVRB=qqF4M0wGoQsVgjREb+*DC}8HHX}MyR
zH(%F9UH0aTY^NzYmKrUcvzmV`o6gqO1P-BR4;<z_Szwvpx9IU!t-BXnWmv9FmznpX
z|IAtL-J8qTf7}1>clmyqeP7DH?8>>bq+v&#*)sFk6FFPFqBoew->?1k?Zdm@=}#)p
zzrSU@b+`LR`R!%56?O~nx-g4(hI*Ju<==OnFRIx8ga>_$*EqUgGvsK!xQd2;6xY9Q
zR@VQ5mk&4m_n7Ofw33tc|0kisfIs1@?%2jocu@ak@^hOD2fhf~h8CTvXyi<8&RMtP
z_#3kacDXvzya}x#ceDcw*1I(4OkK1ioR#(as$CD_dUAL4FIvkPxamP$M^|<2Wl#!O
zc+mV<vcmeuc1PcGy<6H}E%dGaNO!@0J)z)?xQpF9d#66^`S|VGHM{!1r*EgnrXBqe
zS$cfS>elY%DlY5ax@D}r$H4Vq-t(X{#kw&}OrJL0J1NT$@W|p)fwP0_UfUJCw(Vju
zLTk=$T{T&6>MpLpNqLicxq4QtQ{6lB>XMGLs~qIE78vrj?CD4^I~aAx=Gf%86H{MJ
zmD#QupWXVcg{v|AgvQA{uGXI+$%|B%#7z6@b-+ToY00eD#)}VCJ8S+3*D_4w$h&Iw
z)==5=>dF+}o(w^53CV@4Dnlno^`G|L(xJR}Mfm>py?fT|u`<mFbbqcDdzP=hd`65>
zS5@wsb81)b->aABdf)mn{I=FS=cMla=Po9dBu#Ge7Uc~qJ78g*!7`_C?~Q2J8s-}Y
zAyGSCn4O7RaZ7Nmf5(Oims9;V%WzrEO#K)zQEmRmrEE-rU(fAa`fY05X&&={e8!t=
zI-JZt&z{`xc7`cXV{_W6oL3du-A?_Ub-sm$i#{-!|DDut<iAatJK@-e4@Z7{bySb+
zJl}Qjc4|%4g&!;-8C(69)otus+#A(2eG5x9bCpw652vvH)ufnj;ydauR0ZwOh_Sel
z^~Z8*htnMa(`$3~skr=E7ksXT>--ME|6+VKi+5EpNkn8F?sa&uCi-=B62qGXkEX`8
zL@V8XeJzi>_xs+veCaaRYu&C}me0M~axG81yJ~msw!J^o?d=*3YWy$$Z0c+{`2WoQ
z9jAU=_|yF(!1$N?m(Kd<GWH+z^A7t2`)2$T?cP<Ne!Kp~{NwD)r@c_QP*mA|dq={I
zcrk|8rLzq)5~HH#xRxub6rDJ~a$>>(lj2=}cjZrL^Sk))k4mr2K5L#^fm!ZCn|{A*
zI%EEy@i)iBLtLqODbN}_H7^BJ(SvGt5N&8_Y6+4Bv5k-#0U?zIsS5f5iRoanC^fG{
z!5GpY2udx^FD*(=Emkmt2sr2Gm89mC6f1xl5kU(2zNsmhiB9<y3eg4%1_~yY1`3Ae
z7O`CVLHQ+#C8-JqpymVA6(AEpHiMcS0Y&-A!Koz*(F*zjE^Z3?A*mH53b6|M&iOg{
zMZpD$$*Bq;WzNNh3g%FYi;Wa4z)U+k1%0>tyb=W)8!r8j5JLq^n6RB4%y)($*T5`;
zws8y%!Rqw=6bu#g9YGD9JdhLhT~f<3lT+P`5-SNefR=`{M@+shW%u9Xkk^f1w;Lyn
z7QB(1$(X|L7?LF9A)(0D)UZS2DAzSzJ{eKnuAnVZf*N{P9xccVc)cUQn{}z!>Kz-Z
z&T}rf@NMUJyYpxN%l!LZlV0=M_I^EsL+pvE9-9go9QrKcrG!rV&6_#r(2~2%Tn^$Z
znA{hfdivD!#>I<*1zZBpyI5b?e*C_PJHeyqFymX(!Z-WBY1BB%@t?C|jTW@;pU%wi
zjF(|;zxu>y%nLFYpFZRMq{`9mv}UTPyfj0h76X^o;_QVIGg>%~Fs<x3&NH#7dxqkj
zIWl^eZ(f`!se9H}JoSI`)r^b(Kc7B1O>y_d^DJgl_pI4b@T08d+w_k+8##76*UUK1
z+a-OppWCH#qQGzFhS{E<mLGSLVf$zk8O9`?RNe9V^3sEx0>7PVqBXc(E2J1&{5Bfc
zaV8~q96s_{X|ck$mWUIlxjh<husxDm*wFlmCD|=T<Z1CE#kOA^%P-xDFu5<raA~$a
z2anXm$uA>!K0Lu@tnpuOy#n9Kr)J{Z%oFAYh~J!glDE6<2G=9;rZ)m6^6#7tCp>Xq
zY@0Y=NaI|eOVwY+bwW>0{%x)G3g2fS_w<Y;!>Y)ACUR?Aw*@}F?0Qh9qghc;#LIc2
z%r9?S#go%M^BimW<)_u{y3biY^B_|pQ<vhSqe1ITG+2@(w4<~=j_hz?C^~5KV><hh
z1?&cnasrJ^mZunECNN72M<wt_bIeg~^W{o^(x{_xzG27r#}=;^i)Qq)^gU@Ru`rfi
zCq3DSQGT6#Wc#-ht-N0^?5q7$Te<j`%))&PkJmTy^l=|#kP&w>VJ<nX+InH1%nkmA
zAW50i4HbLD(oZO-3+QeyJ;G+vx8+NJ*2z}wA4RdsuP01b-p1-M`{)9RKE>Nl=1tzE
z(mjW3wz#C@uL(Lk%{1o(vdBCs%HNse^IHA<#QeYVThFy`>-%0;v*%b+jnpx1`FC@8
zZAJQzsq;sD=DRi5bl0z7lc!SGB~Ik1Oj;FcILC5pQTN36XM$eF2);k{>frwgTm5fJ
zU4Cbvm>>AKQZb$DfBv3^T^iRl!!`Le%o&CE)h{dw`lYbTdnfyRYx%dGa>v<4s*lJB
z{?Tr->oZJfiL}|t@>EIMPD8(b`{&?uZr^^M=95so-feMu+WRJnY0T26);P?&F0f)g
z_veZ1i*=iAT<;V#^hnO%EvWn0&!O6LwOm5kTANZvgV$GQoj<+x#NxZ2W=rn{Wa@j0
zuQ#0F@$AYp9&VNSZh>+vr<LQ~nu4mYDPCj9=3hPU>zuC-F7sT|y_Ubm@0y;)r<MqR
z8Pz`Fvo72h8E0&`?lebj*3%X9GFs1Xm%r|t^5cZ%tP=%C%<pL|p4k6$@f@l1e+%VK
zJvJ57HL2GLp1D}P)aH9Y&2eM4)Hn5;Giuz_!&)Z3IpHsRc+SHk3k-84^?1yflV=<{
zKJy{}M9afHf(I|OE?&r!?WT}?>3BuYoWc}#tM?s=$)yj2MZMb=C;K@3<5c8d@@dvl
z*{|Q%+Zm}>bZX7Y__OlRiw`M%8B!}bldX<F(n>$kGI=V4Y3Bi^jCPS@qI1g(*QlQ1
zEDlh03*|5pnyq^Nq5T||OEXH8EH@arGOC?ai}m;)*t2S?c}>7tsg?KmmdML|Rb}=p
z4>^9UnxS02Q+!p%|D3-+CMzze3R=6;F(muvy`uLk8m|Oo86*VFoiN9$Rf=sR`>d(@
z8ZG7g3`|9;u0erq2J=t0ZI@x3to+RKmhs$3zYnk5-uYzkF`Q3+Qm*K;yjgv+SkDQM
zFN+vdE9PHf`t@OT7T^ABd>6FMAF%G9>G*+9fc251(G2Fl0*8FO5>vbn7zOZY9hBN2
zn8Rv)P%eO7>Of)v&z7dk57-MhV_4@t(EBs*OOtwnz#f*v5^Wa^td@1YOjetrn$~Wa
z{BDN6Sc_}I#t5TnZK(-KK5bJI<|j_QVU?r3jeGUseMe_)ynKW8jZ_)?>w~{G+Hcry
z(YX3S)DFSCR{w){3(e&Ejz8Y~k*CHku4nqg)gR7Q@W%C<KU)6LyF&e5ul>Px4hIck
zs}{|N4m*SyT|_22EfEe%G7NMK5j1sSUc>nI2=AiV5(@Vwgal1anZ#$%y)cF8r1JC0
z-6y9$2`iGn=`l|=e}e53g`e}BmP-V^(U>Q~m#U`Pys06`Z{?yZL485z4szY~uJl|Q
zRGLtCC*j_tl{2rjUYUC3?Um*$!B?`cv|mw_>Rsl)dGXH+i!x%O?AFfN)*9w-?YZ0U
z_0qjz0bvG#1z{Xv9)SYdQ?x=f--KH%EQozL@z91vvlcB~v^;5wQv61b!mW?wj*1=C
z?%LaR*z1+oH7`4_k6tsqPERq@Hr1FLyleTFn8?VRJ~y2$-6EIl38~!tN%86DQ?{q_
zLrg+)LYYE>LQ}L>hkRQ#Cury5Pjmd1M_>H=Qu9mAFRd!szdU~#|C%~aet6=6!H*u*
zo-8-z$5xM5u3EHesaAApU)IK~sjmdDYOi9>>dFesV$6!!dNk{5*4eD>SK6+aUY&bo
z@s;8$;j7+<?_Y3lx#Q&xmpCpx$exn<=9<Ogj{%b}m|W+%@FcTt*-rP*bJEs}g`SS;
zUOaVW=*q9X*HYIy=JLMHyw!QD_14u}$G7e-<&f2u?ep7qE^F>#t5~c2(%zDryO{2Z
z?&95by)^!%@1@Vzg<piekiGKyO7-gVSNJcTzZAc^-sk^5#>|9lf#eMb650=1HaB`k
zP2QvSQ7zQR%I2lI^PLOV46YR{e3*Bb@35kB@?rty&WmD;jop}!SsnX#Z00fP9)F4N
zvomJ>nAPE9He-%S<(VsKn`YiTbN0;UGmgQ|mji-lzSO&XdfDN$YiXQmOVilTzMHK*
zbNB4!v-1t|jper(Y@Cr8m{fS+k-E35ce(e%r)sCmPKSqG3-b&+y|yp%Yvk+5;x*lC
z`6KRcUU>V*%`@9qZro`()9Pkz(X}UUC$GQtXq(<Pr`uV#waa$QT|M_i-tN1m)m?kr
z_ukld?BBHJF6P?{4?Jve?qA%O+>*TVvElLM!8*&9_(WPStvyvejayr~?(RFQOp8{_
zsa9Jp{yxlkeWrL_**?pucBU1tCav@hp6|PPw%Uws$+vRFeWy$6osPW~^RJ||c<L^*
z9p83G?pV4rw|Mu{bx-Bq?z{AN5Bt&NUB`v`!}`tVt(*6AUb}7m_o5G{KHYkM^?B}F
z-4FL3|GjYhO#AE2r<dQJ{&M!S-&6Cq&tEBjef_cb>Gj3+`|8*JSN@h#rnY<D-x90r
zT_wLRzFf~_!z{)+hf9UYnMs>TpFNXBl_i(AN+3sUj$n;Kg~1Wkl*AJ&1H3XSUfjA6
zEu+lWAADSrr<glhq|7Wv)kd!-`^R~~ZGx9Nrb+(j*&z8k{Z99m9uarBZl=IFE4~JP
zU%YnlbN70A=ibh~m3===uW4>m*=Fl!oR@d!-;U`YFFy`He&2V4=LFR)s;ktNsa;du
z=f&j{HT{Zh@u@Se#`>z#D&3Q22W4n>YHrnZ-rSUyJLl@`SCgXV-7>vhRrc@=cQMbi
zl=GH$;iY=z?<SgfMFrjZx261!Mjmf@hFto+ZI#V?81AXv6W(WE&%8hWfpUa;#guoG
z_v!7`Kdhcy>$d-be}t-x0Bgs#u6e0#Y46U|OckBF)%>+{S<ttGGOcsA%t_nWX5n39
zcHLsT!S`85{DSme&U<fJ|M-t%=8i39{HJHny*_0<>;HpqCfqz>H~p)~53vyOJ#iCu
zJn&dpwQ$FV#V599xL#cR=)t4);*+>5xo>;<cu$-9MJGxB)>esVoBYDtLZ4Mry{o3T
z>D=A!lNot!le~B2($`+`HPgOCde02Jd1+Jo{Pvo<1#<%RboXz)ll}9Y{t11T_?S4u
z(xcNv-)sL671xfO8anlT*r%|#KbKyfJ{w;bF?HXoPg&QmT3-ve-f_KT?bqnt`E!5m
zdQ{4P{d~mz9gRB|CLQkXEjEu^F)M6q@#ITtH<!ITD>!@hwuqd_%}?)!J-l}A)yu2w
z+a>d&H@>}E_V3$k>p$ftZ%l4Q?)>~Ve9`*6_gpuxMkI#@Z=Jnscf$Ae)k5F5)W7{#
z8oSmpH}&oO>Z8@WzaM>P9sN8keEa=^|F4*TFy3tZ_v^~9)%RKIE?;?YVZ-YM=MJ87
zelX$9g~$1q_r0}}soU|k<M+h2_d5G;mxX-Ja8<q*amAv-r((@+&7Ci!iX)1nyTeak
zd@sBI{_U(=QMEC@f4ma*Qa|NaV-Z<X^kT}BD+gZoT;{+1Y};L1<IiW#ZZ=HUpU-Vy
z{;&Ok{JAZgZ~M>tZh61z;Af}LuHU<l>+OuodQ<Sy;@9HS{qFj^<MQ@ADqH$;)$yy-
zvhQ8@i}}90?w8wxUirMDytr3AZ}wc9dZF}p*sHbgZvVMmTfXVN&F_^DmOtF>{ZMt^
zqkXsju3~TF&-!QjGoF2S?C$>WEZ<80$bA2Nw|!5$f8EL7Ph<0MuKyChT5hJzs@KKu
zvfuK*+yATL+T(lblhhA0Ki$9b|F*X)&t86C_x=Cg<br1j?~Pw>=C5B<v+jS*`|eEr
zTWyQl<@TJZwEVN`(bj*jYxD2i-?HDg>UT!PLF-$)&({0>+x)cl$M0(SBD<O&=DM*T
zWI&xT)D9@P>jmnL85^6KgQP)hP{$5LM=R)iIy*Zh7N@2tfctGh3b8OXhREGiSU(Qh
zH}z96#?p@qa(5!!jhj2IJS6z0So`_C=6f#)DJiIak*eZUxMb}i$`aV=*$}|g)}mJC
z!s;d>s2P?La)8mjT`AdBguA&Z={n~pfq-KN16^F7-tEcee81N8^SxPrk4N6W`F#8J
zo9XXsukT_A_|wF4s3d~1!DL~C$h+4EV}yiHANkHCA;8EN!Fb?dS{jS{4;Q8@fA-qW
zoVmi|*yeBV^cqrj-`3e5pjLeCfBi%yb7vJc1}@jDW;S(d;!l~T1aCenY4o4v)R(E6
zMs0>hVhcGJtx<Y>WPQ%J<<GQtpPVsW?a4x^$a9i=Oy>3M4!Ac<_2J?kmW44hR3D@-
zu3=Bz8{#>O;pumc%a?!5@nJ9!nHhiPx!S^<P9s+l$#<Qfm>4*w9I@O}#Mk}PGGiV?
z#j^A#T`ZlRNy`MU&&YiG;zZi7kDG&kCK+l^Iqdteqr&I>mn}Sf2I39t^QXBosz&C{
z%$WFgt<2lEk=LGO{M>)@zFb}KU)vK^ze7K&y*WS6v1eZ7{hT*z^!JJ}d{c><ExUQ&
z)KG>kxoi$kAFlC#ufXt$m0`=hIiKa)a^fZ(dBmg6-TmfGPBG*BY(4E4=D+7R<)7N$
zX8C>Q>36@wte1(~H!6FI8mGEGUABCgx67F`Jbcs7r~Lgc@c;1v%gnPU59`dCe?a_W
z>x<C97gIP}Ix}{++B8N?&`aTJslWQLUcyYBU9xU&wn#>4JVR}(Wxx(k_7nNG49?2T
zDtY!*Otr701q``P?Aw#EcH;Wtexs^?&wt5t$8_aA^l?-Qe)f&0Kcz@@k&fiz`z<*K
znS>^=mn`5iY1A`d(n;WzX)rEezNf&@(%>P$JdIh;gDKO2Ws{@b4F)bp!yAlc%~=Hu
zR~oA>u=q8Z6|lvygdgB7;O1#?ci?I}=xxAwuQ8LO>4SjiBF9w|#Fp^Sbh;)W9mP@U
z>=<An!hF=ZbArGmho2YJR!C?yuUhCFVEaY6L~0jDZ1b-L>=zVF*#0uswg}E(x}3;+
zgJE04%?;Kv9PWosKX9oKox?7E;PykW9b$HT+YgC9l>We=(;9zhGKa$n4(5w)5ggJV
zU7RLFs4xmDW=~XF!nD$L)&#yK(mQ)SCKf(nW@}%VI7340nB?R3$exEuVTsq0ybP|+
zNS+bqBmT@RO~APEXVcQ8s~eX^sIRdv<1`bT-K%>fETKOkdc*XM%r_F>Sj+GoKOp%?
zrl4+zM2u0M={lC}{MUPSH@rT~`%vv;#U8DDBJZ2{4;Ft&s!`m>RWDO7cfVi$*nag1
zoKY;<P5g?}6jX9lLIk8Zo^$+d5j<oP*to*KM5#@n@<>dQ=ElAoj(a?1)chukc($pC
z2dQYz+|n50nWYq~W~;VWaq>y46!#*DNQXH8bt>}};#K)4*#}I~P!sX@l5usq>1XM+
z)1lI#(s^kR?~1%D5vykGnj7W6*QM60R^NTH@$}ErAD>)1dG*BXsjsJ3tNKs5KD~T;
zyxx5Ec*T0Jf6M;tU<y3wa4@)W@rJO4ZV$H{vTgNrowaCcQb*FPq|T(~N2W&uRrgG4
zoU~oYf2G6A4VP4xDoQzBURrr+#}?l$R<}}b8OXYuFZq3W^2?)N<X`Ol!kMa?8vRt`
zsmxQUr<+d&u^lo<_+cC*xwL0;&+eZ7&nC}yo_~D)w%Pj3xc_@Jr~cH+)2f-OG&OB1
z<JA6DKB4(nMXt_WmAlISib0lIR$|u8tlwAlR`;G?e!hI(`ML2X|DXJ6f3;y(XVs2h
zSziyovVApKYL?VKDM_hNsp%%iOeJUK%{n>j>8$4_$G2oeac^abdK&e7Yn;K<neWbo
zq^WN1wp_S&-P`557wwkZU2VHIdBx_4^u>Og&k4s)(u+2C+#a(%xZKI#TR%cSetqEk
zg?54S*Un$E-+g~{{iy>N6mBJSJI+41Vqw?9{fYAu7e7o^UNv#`MXkkAi>;4YByTJ1
z`e^q!T5Ut;T+d0Ky(fKxZ(O+-lCbOimh(K>&ob0ZR-5iVzG%ap$jCKr*A`eFwmDI=
zxN`PSZEoA{i0-*!cg5m$-s%MFzSfbC)Qn_}$lda4!>_})j?BuAO|CuOmi0J!^SNbr
zpKV>cQult@{<pQ(vtl>g72EB%`}{Y)Z%V(_ejBpewpX<8<@<i4q)cOXOYK#`*DoIK
zIQOyVF}r%T`o_zi%kR&PJg0e%_uOJ`9`O(2S9B$cE*3uAAyYI_FGa5>zM^2^mC)N$
zA4k3Zb;kF4@AI-Fxkv8au)X<r$8T+ZZ~lqy-N&aapZr|vJa=5j^!4Er!`E-0^gZc)
z*8AmlR(73sy>`O;%J!|U)&G(Bm+5cWue+bGe|Y}u`fq<03zjvUFSwSlxUqz>+i@Fl
z3bB^596rc+aCeiu{-t=8m@8sTPJf)sT5UK@d16I>6-(&pn5<EIQ@JCwqOPKxMK{US
z#reo?kNy*vPPljXig}BbyPb4D>U!1P*R|Spx~uo}2%X5yPuzN<dK8w~ipfihR;!d1
zt^9uJu6O(6H;=d;ztc00nYQ`Ot)i_@SDrq<ZbJOQ$U-eSX?fZE0{=UO53PLav+hg$
z&hn=$*C+38|2^sXG41EQA7g){{+Y-!y=7C&MVIMEVmp&P*LjM1K4$WF-1?w&Q~amK
zCo88+n6g;Yc;&^FXER&2{Md5YNj0%+gLbU3t@>X5!zPOjoOhkdy!tLwc#*@!i9Q;|
zk!ibU^!@Ys>d~VzTeUfodvn&Nd+F|}^G^ky5q$RL$*d=Nr)5umKKZ-OG|jZUG<{#$
zzqUUIP2Xknt!=%wF6Q=5zw+3FyB>bs_qsn<A=l&PhtqDSdsC(F=XKq?61X66!@h)!
z&F`NbbK2<?_;9c8xoEzeqdB5EZ||mUUYm7$x>DT5uSusLbv^P|y))_c{m9zzpLfrE
zYk9kO>9?i7%O8|+l;64ga@XgGnMsjxH!rMv5WDv2nNN#8ZQmXKW?xuhbYTL2W`9cm
z7NZrL_Ij<)a=*I#)sk0@QvI`@?R{0f{q5Xa$8TTXe?PbWGGj0EQFc2y5t%*pC%y+{
zuXW5lnt12on#1Q`FM73We|mj<y~|sVj}y<kx4JJqeyG3ns`ZuY<}1vnm>ue!bZq0}
z!sGdWAAEJL7GC`_z<BY_A1oG%mLDG-{~`Z=9*@n<%C6c~FV+9f|F-QyR9Do(Yj>`7
zZd+oOS?yDO|7FAFxw7YEb?s;WuldsRZRV`ar_#O8Pdq0&XSU`1^14q>$67yjcZ#=L
zg_qdv+VbSm+;tn)-8<bleSO@=okc5e@BRHJbo%P_b(XQ#wR3CtzHR&4drfZlylL@o
z>M~z$eV@DcWx?jZ(;lzw+s9h_{8#L6{d?bb)jsX}KUbQ$o9)*-y?xdH<L=nLtiAX5
zBKu1IIQuhI7JoDTCck;SNS(`HYu+mRwSTYvxSqCh@0T|Vt|y$|+>zejw!>Nf|J0xB
z{SULAUwK~JZHwD0_qFcldw%xZt=jnI=!eri(=R`6-LLs?+xMv#SI@62|GhUo>Ew|Q
z*%x2WwD-EVVxQ%&Yu|F8r@VM_xjggzvgKX(R`0X_*7$ef@8mDXC%$~+|HFUk{9gO=
z8qPnTD%5h*p56c6^7%KYL5kL<1vNuK?N=i+LnDwhhz**d0MRIIT2LDnsZ9&h2b$nO
z%)At%&!w0d8Y!4t8i6N8O7luUlNR2YDa8uW3Q+TqrdA9=voRoh5oS6kmL%rnr$eT7
zilOs4hzSzVoC&H1@RW*vaA{Hrcs3}cs5BMgI#A0TA{iRy6c8S&?U9;OmRgdToamQY
znhKeVaY-#sF3Kz@$uHtE1kE-DDd@ZACFiGP=A|p>`z9s_<>w~mAw=9Vi;7E}GZKpw
zjExlZeG;J@LqjtK{qW3`k_@mn%`Lb<(>MrhWNN7Z!VnQ-3y>!uYy$;TQ_%bpjE7E}
znOJa{S(qxA8-W53CJQqQq}Re6G(BXXU}ge}Ly%e!%hVhcvM}{#;C_q&+*PK=<_e~k
zp!fulARa`e5!4n44Kf{Oj<K<^f~kRlg0Z2gLM(Cwf&vXQJ`lkQ31+{<+*Ad99MO=I
zm|hGHPf%nzIptSyMeACc8Y<|TSQsi8T3VPZ7#f(H$13Q1mL%q6COhV(=YS^Y^c{<n
zK{I}qrbY_-APYepT_Zzd1%2nl0*}<p^o$ZNb3-Eq{os<++%N?L(4wJ4aLgK6DCkE(
zR4AAk8GvHC0vvq`Mn*=a5GT83=A;@a7=j`v2-(9R0hotj9Xn8uFbHHkXibu#g1HIE
zOgBPnk|KF?qOX_k`#!0EiO1gwkL)#rROYWx4>Hm0s{13TI&+h1^roE1NxIP`O1uAc
zKRvUq_lEc5oYOtIACnlRo5W5&OOb9XdofE?Q)G=tYHCC?tLJnb=AMO_Vdo>Rv)$db
zCWG0;{zd<i+UI-KUCTBrNI3ocFt7UOy}i$CzR!6-?|aS5#``u$rEZF*C2bXc-WQv2
z>$p+(GkHIo3e9ETe}-RRd$+sb*PM&>6Ag>6zuY|i{pH_bG4FfN&bKNHdcQe-q3*e4
zhxeb?W>`NvA6w<|-rL@(`r(_O!pGiUGyC%UoNV=pi1~Nj?7!Vie(v}3`u1As-0Q8M
z#q}j?XFb2i%|FLz-Sd?9aevK^S(uw--M%q-P2*W(W8qsFQydM;561V|$DFz0ooxU6
z(8X#0zVA5gQnvAVc}<(tw_}&>-~PIKBWw3p)y-Xb&4$fo{h66-XK%eZ@9_KZHTs#x
zncpSibG^@8K0CdzJz-zoKVKd56JBd(Z#6d8%Y2=7|A_wX_cBp!6Vt@r#U<I8eX>qx
zI_!O>kMCX58R!4UZYHi+x7F^MfKax`dPDKLb3OVS+fLqmZt?%|FQNGAlFS*dc?Y5{
zUsR4Z2vrl4wlv;z!oIohM1q2Bd)lcZWqPwFSuan2T9u=?&7iDEahtJO{hKF?ELU#*
z@$ib1t$1|G@AUHzejmuG*%-#3zhe2TuXbmWmsJ*U>&34~Zu{LUc_GVrr)Z2y>apbR
zW#>-bTzT`T_Th&|Zxz_e^dEN<i=Q(mwx-ZRX8rZTsi}v9B7EMxHj7T&tlE1&_m|FZ
zL-u7W^mQ)GdC__9$D?j;?uV=ui+WFdR6W<jSmAYj#w2C$J!Y2P_E(=&%wT)6L#AE!
zYvP%^6D053TQhk-O6mN2T_N@GY=zPsiLPwv#CgumTV4h?ZTUIb;nt^4h0?r;D)uFM
zH{PgtMB7UR{Y+-K>#*aSAV>T~!F`_uId;EyxbgWTN45EzwuyETudfPxtM}qyx8po?
z(7&Z1<M1VG0lve}1QhRVYb?;+bHc1ij3a)hcFN8Fl867tpHQBy@cjKIrtgird~}Zc
zX3KwYk6eFZLq|o<Tk%JcW{Uq>OCN8~?D3u9x7qWf#IcM&hSNlveL95Cs5h-~_Sq;q
zf$!4I{hI}a?gSq;m95d2K4A5B57#%vX;&(DOpLs7{bK*dnemT38I!Kqr!8LUc5BJ~
zwNW#s-ZbOA<kfR?rgOIR$Gb;nMRs4iynoK@k`3zFuJ?UgR@LsgWj-OXPVB-L1@4U-
zmKmCL?LU9`c=?a=7S}y#TC<n=^3V8p?oQ&rT_#$!VZVY;i?6M{R=@RX&iC8@4t%RR
ze6wx&o91uF3%4h*%DAlWu5W1%E9*MP91y`*!@JS)V5Yg^PU#&NzUaBlH9zooiRqm*
zg_jc}3$pcmn!g>~WvFnm;m8@2gk!uBtmYmU3eN4hJ^6WI_?@?1yMKJWTK}x|(5uXk
zS565(`sL+X!+qlUwN-mO|446`xp?xigFYKhypiEbu0L~z{bh@YqO~Hs;&(^6mY7x>
z&Ywn4Do<!nShiEKb1&o5b^$~7*=uJN+g8>qp1!*F=%hPm_Rd>TQJZny;s1*ZN9^KP
zy?@$mU-4x7zsHT2-`ni?yO8~y@xE^dqo&qIZ+<Cp^U9XI$w%@Qel~MCbMOG0hNA~p
zP-Bnds|m&vPEW|5@OnbJg1N$ar&-UY&FJ2cWAJ8^7+Yd^m`0IETclLhEKk|3bD96@
z&;O^Xv#VlX&BwLwa{uf$yh^oy`1_~Aw{r)lH5#`k+E#8iU-#{kh5Vd3M?6yA+V0be
zOKXmaOY>t9d-$?MPq`vzmRuRrqUaZUcn$w-ILI%JkLXVg;nfo>+Zr}4l1X`q?nalq
znW+Zvu2e}{?0jnGCK&lDH#b)F^{UseS4D&$-KBLcbmO|N($F=llR%<yp;ZsXkL7H=
z?XZCJqvJc%gSM<MCaiOK&+N41`$H$;misLSHk9>z&uqJ>&uq@QJ87Z0)}DE3it1LP
zH-$u7?>R2adm9o`8~?;*^9HePd`WlQr<Z<inX^Nb<G5FBW5TXGcH7*~eE9JoXXEyL
zu{X`8=pFz4E%oZkB$qQ5k6T>|uS`GF9<6%v%zO#coll%>!Y15pck^OjeX*d>Yprai
z*t@&7KQFGazgWNELYyDF_S9`YEFp^5>KfM{5A?rSr!Humc0kin>H)X&ze)W(|G2#D
ze_Wl+|GDY*5$>fs_8*Aft7G^5>ecQ2zMtM4nR)g9Gp_r)e{KKct$oz|{*gI6oBb00
zX<vA&bIwSnRnh!YfAXaT8yy1r#kIek-L)@2?Co_CHmwPU9<oJjMUq9lMY5lGp0GU$
z<v8lil^f7(KlO5wVyk8F>*8ew>0ZBAKd9yjYM;{>(-zYl({97Old)3NY3G%yYDvcj
z32Sfdk-0tVK-%_2XM<W)K8QGKs6LqBd|Ld9>jlZl<`+IYrb|`jh4Qm?pNai=Hu1vB
z6yHsmkFTfy-?w)P-<w%cwcXdRt_-?;?rm#OTv^`DRlokf+I_L8Jmb3AKlS`b=9%Zb
zTE)Y<ic+_4`g<?!;mvr>ci(Qk6^h^at5JE*)Zgt}b>78QyZ_<+p?30|?&cL6*#qY?
zFD}sM;_GQ*Ui{#IhJ^t(W&-1me21TkEHWO^FR$$3JyhKNaOY9ZG`$15N6ZD27Ea$G
zcvojpe0P~)&6RDXk5Vdsm8To6e0l#~{agK6{j(Omida{czjf`}D*xO+GXEo=2E=cv
zy1%uv^SEEwyg!G}%nPbMe`ROmr#~U*<#w<gS^n|w9I?ayQd?vW@!d`=x|Eq@u;6xR
zfv>#i`n4ikHyp7Qna*V;lpTMqFLsyvqG}1H`#EnGOUgZn34FYc^WWX8t4$6rshDwX
z&JnG;JNM7<<;G2Ra(M2*)u?vk(SdE!(_U0Am2cro7VYXvz0=g?czG62?={^WTzP*M
zPL-|swBg6SE8mYiy#M>)cT@Xi;rrA);-Y_c%{XdxBH+_Yi=0glr|fULB<NjGCDW8H
zvNf(l*hllFj;5mVlCNhbY-kjE6zjCj^8^p)OhrXwm6W!YGZQ9A3K=;&rFop-@jT5l
z>uRC!y_*|Dn8g+^mD+OSdT~?ckIXG;ffklew3~iBNuR#_*zx6I|6jjYyZQO~`A?_s
zNOfOpcIM~7sY>r3i2Kd6+5e8eFqntGsh)4zaU~DsTtP|g?%5K~(vEd)26BuI3h8&P
zS?_7SzNh)Yud$qKPw<1eOz%Z1mLC9#A_?`_W*=KL+t{*^L0Mn(w(|wyh$}a=C+xA$
zauQ5%(t3U8p62Y7C0mZY5_YdwS?=7M=E<@8@4sncvjx=J<1^(~#qC-Dd#e2V7yS7z
zm(P7#xqc3JYu8Rc_w2lELy=d3w{#YL{c&O8<kk0o{45AO>HfxmGedpiW%UV{MZdXE
zxolCD5FygGG~mg^c}!M;9nQy(F#FiNo>9@z>ArhYQyFHyiMi4JV`1d#BQ+tMmyN2<
zO*i?wZqD`>$K{0Lu5mP++q>rIiMoIG?XFqZCkEB!=`7~)J@3P>xpA%Y#&x!$KMV3+
zng9B%uEu?=qQX1A<a^-1&#!zeMReY1KWh(iEYDV%9a5#-JMYVdX$u!K2i7O9TJ-Kr
zo9(&)ExqTrq})s9eE8?gqtLg;=jNQ%xA=skUoM}+nir|4X0=%}<m!&^a~Io3Rz}+F
zDGIgeIn{39zE?-hAe_0WMX5Py-m?ij?_X|NV%gyn@GfbcP}Xvb<0*ynHP(my;MRWs
zdAXXpx@**Ip~~AEzs=jgE&e+3_RqZ``uh)@;#jLD)-bKDjY-zvx8Xt;;pc5J5gU1;
zPbIuHirCF_O|N<DX)yCl&XEiKPL)hb8;Vm!P8(jiX|CZHVDtOpd&4cN(~j?{oRBJ&
z&69uSp{LgF$!E3&wsT7zh+fjmD9w8#qah+>!;)#uo@eg19g<OtX)c;;RcvsJO_kwg
z(-g(U6CzL8JW=f6EmKQ$v|i+s(5G|u;h}#ijE-U*=^yWDoGx?ZbM$kzW4~Clm+Pr#
zhlA*a<cLjYK1rJeYEIj-fGK$P&tIG&QYL}1I_f%Ml^2%Cp3&=He<3<(mg?UFPJ6g^
z`*&)8iV3_ojo1D2?MI)s%`?lld8*krE6v6I|GgfYAioIPzG<w_uX)9rJ>n{_xb%1K
z+C`c({nY1nPMV~7dac;%t(p=U-dm!Arp|l2GOW6~^7O0U7tLNq_wr>ot4n@%i^{FD
zbmh-9sA5k_;(nyl5cEAVL~6l8hPnkM+zg73?6S^gtV}uWl+TuB^6c;o{^YY4nya3%
zPyBiC>luD0UZu~?3VjMj_8n*Vl|DD0_@iK^)4|IPVH(-5NVPkwlbmMRzGtDaQI?FZ
zi$z|J=FDf;e#Ys#G%lO=+G>a1y3qZvpVx)FnIU*~WzM<Swc*Mav-a+<xS?Hf^=9DN
z6t<~h;pz3|Sq_E5vVA{pN9VrW_;~51j~{z3ot0h9Ja_R^mpwaHZ%$6v6x0ry^xE<Y
z&z?I6UbFsP^Fhh+gof4k7jqV@(sg7#nEUo*f1sXn{fB*Gn}mx5oZgqpBej177Qaed
zQMExO>1uoA+Zk8;B0c#X_$8{Os-z4`7dw2(igXN5d9h_l^G?=_KF78)?Cm%xC%7Q|
z64&Cd$6MD-h}q=5Z*z-Qg?wSzm-2kJF8g&4XMW8&R{T|OPG0Bru>0S)@6Np|HEXx=
z+`HB%1$*m#9>`l?*pV*jvwpsc+zdB;&TEEW4%AhhQEbX~xjloKd7DH!!%smb?Tbeh
zU&vgZ;HT=uez#!uyh~qIK0juh8MHw}Kj_m!izNk`pZ3Sq2LG_STHzD=hn>&Dt?T8%
zbz$e~<14(s_pJE3knf^h#rX$sRQH*#D*O4@>tlB7y=`|Kl+5j;UrO1=t(_<Hc2=vs
zh@iis*o(i+3!X_tnY$hkIVEXy+NoMGQ~ZTrQCD1OU%<joSI+cU*xB1}|Kz==;FyT~
zxu1om&rbA&&Azyp|J}-mua6(Ndfv@!zV&GhsjuY%Qx<;t@S@dKM8xh+n$wyLbzw%I
znM<cnc1zpYv)m<Oh2Zqiux#UZ=ej28pWkumaBKG}flH_KE8AnvvYfJA9sh*=lJeeM
z_W-5Wzh#<i^N!rJ*WIY+lErn2mD^^+0p`D#PxG$*#-Mz&lx<UU<D1t!DeTK{9CRo%
zm>|oO!p?jX3v+o@Pm=D6T$Q7<a-Q_~RF{RH(~zGg6;)v?bSC8S$1JrS_vHGn_VMtX
zyPCA|)}03jCPwvi--*cAxMDr+bnjE=g?}Q}71iiWm9maoIY+{K`EkFD-<A!3?`Yq-
zVYjyL!s*ys`_&d)ciH2S&mh$!n{BXTLQk-D;h`1G#`Df(Bt9wFz0Ljq&E4B?ltp~W
zKU}X{c&)Eo>;A!eUpB6<iwHZ?<I{8Sq0N^W$CNAoo;2fkDctiizw=Xr8o$eD2NN8G
z)N<<$_EXMgZi(w)uCfm;b5)+)9bw^Fs%JElFKyLC3B4=)nH#45QM|bL#nsnVQx3}8
zeVKWk`+#>zm|uzZ?`@hB?>Ok(x_|jyr)FNh)<a?AWiF}ZYKB3Rs*k51uVy~kqdp~^
zDgM>XiCMWXWzMKpKbDi3|E}Y_aLz`Pibn_UY)k3(*3;hmv~0S$ApaI?-Lm~mG9SaH
zxF3mEdVV0KJl$?@<&wXf7OARzI4pY0I*FNoBjeln?vFP9foW!o&h&6g=uNp$m7k^a
zaOz%Gai+DWLf6i5*!$zpnKwDbD&q1%HV4yQZkaHzuBzs%wCqfW!#hsiyLG7jn4sGU
z=eL``rB}@U5-9&m-myyha))}B{0&piuyY$^x@IxO`H2QH@@`1{a8YlHfAtMJv)1SL
zCFjJpZ#ijk@6)45A$e|z8E0kg*i~jMtNwE3CcA&ERq>-6M>PMeSN|RF{AX=1Xsi=$
zC=@hs0~*XRF+oi48-m8sK!O^Xc?G2<`K2WVr6p-O`Q@4*13(gnpz%8pL&G;QS;0S8
zAwt2>K+n)v&qN`xG_k0pN+H0-4ZPsIq6DtV2sFe7))btYlvrGnnV6^GU6h%ZUL0d!
zXylujoROHCqu`TTTAZAbnuE{=8r=hH^Uux8bT3LwOUp@BFxNBJGeoEXjSYg;xL6q(
z7+M&Z8JHManiv|IM;REX8yKj=Rl*Dd54UEP<fJNqeH)~p?^s%rkzb?$c4d%)en3%v
zN@;RxkpkGSK??fLMX8A;AO#>JVEoMdJeS0hR4(waA!t#3ehP@M0Ocb_Z7YgW)3^*2
zjEuPq;6TC5)YRBiAx!}yW@ut)W}yI<Rmg*i85kLuo1%+Zm|B{niy0VztORLB)@zEP
z*T~Sq5?!yUIi{F}shJ_VItz1S19UMXBTToLnq&II)WQhEEf%IG80J}+Szw4+8X94^
z+0xh?U7ew^r4f3#7#drGMukzr#n9N&!U)YDh9(Ba=<YK#F|fq2!^F_Y457EAC^0i9
zwFtZ)GdQy<Rl&$uK|d%zzeE8%t{<eJ@0pjDuK-Oko-PW}3N{9YY37N>=0+Ath6YB4
xDM=PdNohvLre<a)NvY;$CP{W&gq1)>po>cqi%P%=%h1Hg!h%ax)z#mP3jn#0=w<)_
literal 0
HcmV?d00001
--
GitLab