From b758e41e11661f4e79f977af0a331a0717e5a4f2 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Sat, 2 Jun 2018 10:48:33 +0200
Subject: [PATCH] add prettyprints to presentation
---
notebooks/presentations/SETS_RODIN18.ipynb | 210 +++++++++++++++++----
1 file changed, 176 insertions(+), 34 deletions(-)
diff --git a/notebooks/presentations/SETS_RODIN18.ipynb b/notebooks/presentations/SETS_RODIN18.ipynb
index f7ffa47..d78fffd 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-05-30 15:21:17,073, T+12885] \"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-05-30 15:21:18,280, T+14092] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53783\n",
- "[2018-05-30 15:21:18,281, T+14093] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63388\n",
- "[2018-05-30 15:21:18,283, T+14095] \"ProB Output Logger for instance 762b9e9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-05-30 15:21:18,299, T+14111] \"ProB Output Logger for instance 762b9e9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-02 10:17:46,918, T+41014880] \"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-02 10:17:48,006, T+41015968] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 59775\n",
+ "[2018-06-02 10:17:48,007, T+41015969] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 20947\n",
+ "[2018-06-02 10:17:48,015, T+41015977] \"ProB Output Logger for instance 222389d1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-02 10:17:48,028, T+41015990] \"ProB Output Logger for instance 222389d1\" 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"
}
@@ -638,7 +638,27 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{1,7,8,9,10}"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(1..3 \\/ 5..10) \\ (2..6)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
"metadata": {
"slideshow": {
"slide_type": "fragment"
@@ -651,13 +671,13 @@
"{1,7,8,9,10}"
]
},
- "execution_count": 16,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "(1..3 \\/ 5..10) \\ (2..6)"
+ "(1..3 ∪ 5..10) \\ (2..6)"
]
},
{
@@ -1093,6 +1113,30 @@
"We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\{\\mathit{S},\\mathit{E},\\mathit{N},\\mathit{D},\\mathit{M},\\mathit{O},\\mathit{R},\\mathit{Y}\\} \\subseteq 0 .. 9 \\wedge \\mathit{S} > 0 \\wedge \\mathit{M} > 0 \\wedge \\mathit{card}(\\{\\mathit{S},\\mathit{E},\\mathit{N},\\mathit{D},\\mathit{M},\\mathit{O},\\mathit{R},\\mathit{Y}\\}) = 8 \\wedge \\mathit{S} * 1000 + \\mathit{E} * 100 + \\mathit{N} * 10 + \\mathit{D} + \\mathit{M} * 1000 + \\mathit{O} * 100 + \\mathit{R} * 10 + \\mathit{E} = \\mathit{M} * 10000 + \\mathit{O} * 1000 + \\mathit{N} * 100 + \\mathit{E} * 10 + \\mathit{Y}$"
+ ],
+ "text/plain": [
+ "{S,E,N,D,M,O,R,Y} ⊆ 0 ‥ 9 ∧ S > 0 ∧ M > 0 ∧ card({S,E,N,D,M,O,R,Y}) = 8 ∧ S * 1000 + E * 100 + N * 10 + D + M * 1000 + O * 100 + R * 10 + E = M * 10000 + O * 1000 + N * 100 + E * 10 + Y"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & card({S,E,N,D, M,O,R, Y}) = 8 & \n",
+ " S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 29,
@@ -2265,7 +2309,7 @@
},
{
"cell_type": "code",
- "execution_count": 59,
+ "execution_count": 22,
"metadata": {},
"outputs": [
{
@@ -2278,13 +2322,13 @@
"\ty = {1,2}"
]
},
- "execution_count": 59,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- ":solve z3 x <: 1..2 & y<: 1..2 & x \\/ y = 1..2"
+ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2"
]
},
{
@@ -2296,7 +2340,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -2309,15 +2353,15 @@
"\ty = {1,2}"
]
},
- "execution_count": 60,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "!smt_tmp28.(smt_tmp28 : x => smt_tmp28 >= 1 & 2 >= smt_tmp28) & \n",
- "!smt_tmp29.(smt_tmp29 : y => smt_tmp29 >= 1 & 2 >= smt_tmp29) &\n",
- "x \\/ y = {1,2}"
+ "∀ smt_tmp28.(smt_tmp28 ∈ x ⇒ smt_tmp28 ≥ 1 & 2 ≥ smt_tmp28) & \n",
+ "∀ smt_tmp29.(smt_tmp29 ∈ y ⇒ smt_tmp29 ≥ 1 & 2 ≥ smt_tmp29) &\n",
+ "x ∪ y = {1,2}"
]
},
{
@@ -2366,16 +2410,9 @@
},
{
"cell_type": "code",
- "execution_count": 61,
+ "execution_count": 23,
"metadata": {},
"outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[2018-05-30 15:21:33,243, T+29055] \"ProB Output Logger for instance 762b9e9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] z3exception in query: canceled\u001b[0m\n"
- ]
- },
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: time out",
@@ -2386,7 +2423,7 @@
}
],
"source": [
- ":solve z3 x <: 1..2 & y<: 1..2 & x \\/ y = 1..2 & 1:x & x <<: y"
+ ":solve z3 x ⊆ 1..2 & y ⊆ 1..2 & x ∪ y = 1..2 & 1∈x & x ⊂ y"
]
},
{
@@ -2444,6 +2481,35 @@
"The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can)."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge (\\exists /* LET */ (\\mathit{st13}).( (\\mathit{st13})=\\mathit{r} \\wedge \\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\Rightarrow \\exists \\mathit{st16}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st16} \\wedge (\\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16} \\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\Rightarrow \\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16})))) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st19}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st19} \\wedge (\\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19} \\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$"
+ ],
+ "text/plain": [
+ "f = {(1↦3),(2↦6)} ∧ (∃ /* LET */ (st13).( (st13)=r ∧ ∀st15·(st15 ∈ st13 ⇒ ∃st16·(6 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16)))) ∧ ∀st15·(∃st19·(6 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ⇒ st15 ∈ st13)))"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 82,
@@ -2481,6 +2547,30 @@
" !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))\n"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":time :solve cvc4 f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -3968,18 +4058,18 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-06-01 10:33:14,681, T+1705365] \"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-01 10:33:15,765, T+1706449] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53813\n",
- "[2018-06-01 10:33:15,766, T+1706450] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2267\n",
- "[2018-06-01 10:33:15,767, T+1706451] \"ProB Output Logger for instance 1cb4e9b8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-06-01 10:33:15,784, T+1706468] \"ProB Output Logger for instance 1cb4e9b8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
+ "[2018-06-01 22:55:14,469, T+62431] \"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-01 22:55:15,676, T+63638] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62712\n",
+ "[2018-06-01 22:55:15,677, T+63639] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 15345\n",
+ "[2018-06-01 22:55:15,681, T+63643] \"ProB Output Logger for instance 1fa8bcc7\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-06-01 22:55:15,695, T+63657] \"ProB Output Logger for instance 1fa8bcc7\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n"
]
},
{
@@ -3988,7 +4078,7 @@
"Loaded machine: GraphTheorem : []\n"
]
},
- "execution_count": 30,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -4001,6 +4091,33 @@
"END"
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{edges} \\in \\mathit{NODES5} \\rel \\mathit{NODES5} \\wedge \\mathit{edges}^{-1} = \\mathit{edges} \\wedge \\neg (\\exists (\\mathit{n1},\\mathit{n2}).(\\mathit{n1} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\in \\mathit{NODES5} \\wedge \\mathit{n2} \\neq \\mathit{n1} \\wedge \\mathit{card}(\\mathit{edges}[\\{\\mathit{n1}\\}]) = \\mathit{card}(\\mathit{edges}[\\{\\mathit{n2}\\}]))) \\wedge \\mathit{dom}(\\mathit{edges}) = \\mathit{NODES5} \\wedge id(\\mathit{NODES5}) \\cap \\mathit{edges} = \\emptyset $"
+ ],
+ "text/plain": [
+ "edges ∈ NODES5 ↔ NODES5 ∧ edges⁻¹ = edges ∧ ¬(∃(n1,n2).(n1 ∈ NODES5 ∧ n2 ∈ NODES5 ∧ n2 ≠ n1 ∧ card(edges[{n1}]) = card(edges[{n2}]))) ∧ dom(edges) = NODES5 ∧ id(NODES5) ∩ edges = ∅"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint edges : NODES5 <-> NODES5 & \n",
+ " edges~=edges &\n",
+ " not(#(n1,n2).(n1:NODES5 & n2:NODES5 & n2/=n1 & \n",
+ " card(edges[{n1}]) = card(edges[{n2}]))) &\n",
+ " dom(edges)=NODES5 & id(NODES5) /\\ edges = {}"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 32,
@@ -4339,6 +4456,31 @@
"Solving takes about 150 seconds; Kodkod translation currently does not work due to card and preventing overflows."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{n} = 3 \\wedge \\mathit{bshp} \\subseteq (1 .. \\mathit{n}) \\times (1 .. \\mathit{n}) \\wedge \\forall (\\mathit{i},\\mathit{j})\\cdot (\\{\\mathit{i},\\mathit{j}\\} \\subseteq 1 .. \\mathit{n} \\Rightarrow (\\mathit{i} \\mapsto \\mathit{j} \\in \\mathit{bshp} \\Rightarrow \\forall \\mathit{k}\\cdot (\\mathit{k} \\in \\mathit{i} + 1 .. \\mathit{n} \\Rightarrow (\\mathit{k} \\mapsto (\\mathit{j} + \\mathit{k}) - \\mathit{i}) \\not\\in \\mathit{bshp} \\wedge (\\mathit{k} \\mapsto (\\mathit{j} - \\mathit{k}) + \\mathit{i}) \\not\\in \\mathit{bshp}))) \\wedge \\mathit{card}(\\mathit{bshp}) = 3$"
+ ],
+ "text/plain": [
+ "n = 3 ∧ bshp ⊆ (1 ‥ n) × (1 ‥ n) ∧ ∀(i,j)·({i,j} ⊆ 1 ‥ n ⇒ (i ↦ j ∈ bshp ⇒ ∀k·(k ∈ i + 1 ‥ n ⇒ (k ↦ (j + k) - i) ∉ bshp ∧ (k ↦ (j - k) + i) ∉ bshp))) ∧ card(bshp) = 3"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint n=3 & bshp <: (1..n)*(1..n) & \n",
+ " !(i,j).({i,j}<:1..n => ( (i,j): bshp => (!k.(k:(i+1)..n => (k,j+k-i) /: bshp & (k,j-k+i) /: bshp )) )) &\n",
+ " card(bshp) = 3"
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,
--
GitLab