From c947fd76bec3ed1dc204fd0070fea8f5112c5826 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Sun, 13 May 2018 10:00:31 +0200
Subject: [PATCH] really add description of SORT function
---
notebooks/manual/ExternalFunctions.ipynb | 458 ++++++++++++++++-------
1 file changed, 328 insertions(+), 130 deletions(-)
diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index 61042fb..f1e110b 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -23,19 +23,19 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-11 13:21:44,730, T+246558] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n",
- "[2018-05-11 13:21:45,901, T+247729] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62905\n",
- "[2018-05-11 13:21:45,901, T+247729] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 40975\n",
- "[2018-05-11 13:21:45,904, T+247732] \"ProB Output Logger for instance 342c2add\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-05-11 13:21:45,926, T+247754] \"ProB Output Logger for instance 342c2add\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
- "[2018-05-11 13:21:46,041, T+247869] \"ProB Output Logger for instance 342c2add\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests])\u001b[0m\n"
+ "[2018-05-13 09:48:02,007, T+3926] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n",
+ "[2018-05-13 09:48:03,239, T+5158] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54031\n",
+ "[2018-05-13 09:48:03,240, T+5159] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62735\n",
+ "[2018-05-13 09:48:03,243, T+5162] \"ProB Output Logger for instance 4f9c1863\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-05-13 09:48:03,263, T+5182] \"ProB Output Logger for instance 4f9c1863\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
+ "[2018-05-13 09:48:03,386, T+5305] \"ProB Output Logger for instance 4f9c1863\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])\u001b[0m\n"
]
},
{
@@ -44,7 +44,7 @@
"Loaded machine: Jupyter : []\n"
]
},
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -142,7 +142,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -151,7 +151,7 @@
"\"abcabc\""
]
},
- "execution_count": 4,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -162,7 +162,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -171,7 +171,7 @@
"\"abc\""
]
},
- "execution_count": 5,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -193,7 +193,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -202,7 +202,7 @@
"3"
]
},
- "execution_count": 6,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -213,7 +213,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -222,7 +222,7 @@
"0"
]
},
- "execution_count": 7,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -245,7 +245,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -254,7 +254,7 @@
"{(1↦\"filename\"),(2↦\"ext\")}"
]
},
- "execution_count": 8,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -265,7 +265,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -274,7 +274,7 @@
"{(1↦\"filename.ext\")}"
]
},
- "execution_count": 9,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -285,7 +285,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
@@ -294,7 +294,7 @@
"[\"usr\",\"local\",\"lib\"]"
]
},
- "execution_count": 10,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -305,7 +305,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -314,7 +314,7 @@
"{(1↦\"\")}"
]
},
- "execution_count": 11,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -332,7 +332,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
@@ -341,7 +341,7 @@
"{(1↦\"usr/local/lib\")}"
]
},
- "execution_count": 12,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -352,7 +352,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -361,7 +361,7 @@
"{(1↦\"usr/lo\"),(2↦\"/lib\")}"
]
},
- "execution_count": 13,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -384,7 +384,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
@@ -393,7 +393,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 14,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -404,7 +404,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
@@ -413,7 +413,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 15,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -424,7 +424,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
@@ -433,7 +433,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 16,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -456,7 +456,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
@@ -465,7 +465,7 @@
"∅"
]
},
- "execution_count": 17,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -476,7 +476,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
@@ -485,7 +485,7 @@
"[\"a\",\"b\",\"c\"]"
]
},
- "execution_count": 18,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -496,7 +496,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -505,7 +505,7 @@
"\"a.b.c\""
]
},
- "execution_count": 19,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -529,7 +529,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -538,7 +538,7 @@
"∅"
]
},
- "execution_count": 20,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -549,7 +549,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
@@ -558,7 +558,7 @@
"[65,90,32,97,122,32,48,57]"
]
},
- "execution_count": 22,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -586,7 +586,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 20,
"metadata": {},
"outputs": [
{
@@ -595,7 +595,7 @@
"TRUE"
]
},
- "execution_count": 24,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -606,7 +606,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 21,
"metadata": {},
"outputs": [
{
@@ -615,7 +615,7 @@
"TRUE"
]
},
- "execution_count": 25,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@@ -626,7 +626,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 22,
"metadata": {},
"outputs": [
{
@@ -635,7 +635,7 @@
"TRUE"
]
},
- "execution_count": 26,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -646,7 +646,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 23,
"metadata": {},
"outputs": [
{
@@ -655,7 +655,7 @@
"FALSE"
]
},
- "execution_count": 27,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
@@ -666,7 +666,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 24,
"metadata": {},
"outputs": [
{
@@ -675,7 +675,7 @@
"FALSE"
]
},
- "execution_count": 28,
+ "execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
@@ -686,7 +686,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 25,
"metadata": {},
"outputs": [
{
@@ -695,7 +695,7 @@
"FALSE"
]
},
- "execution_count": 29,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
@@ -706,7 +706,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 26,
"metadata": {},
"outputs": [
{
@@ -715,7 +715,7 @@
"TRUE"
]
},
- "execution_count": 30,
+ "execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
@@ -726,7 +726,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
@@ -735,7 +735,7 @@
"TRUE"
]
},
- "execution_count": 34,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -746,7 +746,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
@@ -755,7 +755,7 @@
"TRUE"
]
},
- "execution_count": 35,
+ "execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
@@ -779,7 +779,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 29,
"metadata": {},
"outputs": [
{
@@ -788,7 +788,7 @@
"1024"
]
},
- "execution_count": 32,
+ "execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
@@ -799,7 +799,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -808,7 +808,7 @@
"−1"
]
},
- "execution_count": 33,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -830,7 +830,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
@@ -839,7 +839,7 @@
"\"1024\""
]
},
- "execution_count": 36,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -850,7 +850,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -859,7 +859,7 @@
"\"-1024\""
]
},
- "execution_count": 37,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -870,7 +870,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -879,7 +879,7 @@
"\"-1\""
]
},
- "execution_count": 38,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -890,7 +890,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -899,7 +899,7 @@
"TRUE"
]
},
- "execution_count": 39,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -921,7 +921,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 35,
"metadata": {},
"outputs": [
{
@@ -930,7 +930,7 @@
"1024"
]
},
- "execution_count": 40,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -941,7 +941,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
@@ -950,7 +950,7 @@
"102400"
]
},
- "execution_count": 41,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
@@ -961,7 +961,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -970,7 +970,7 @@
"102"
]
},
- "execution_count": 42,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -981,7 +981,7 @@
},
{
"cell_type": "code",
- "execution_count": 44,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -990,7 +990,7 @@
"103"
]
},
- "execution_count": 44,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -1001,7 +1001,7 @@
},
{
"cell_type": "code",
- "execution_count": 46,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -1010,7 +1010,7 @@
"−103"
]
},
- "execution_count": 46,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -1021,7 +1021,7 @@
},
{
"cell_type": "code",
- "execution_count": 47,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -1030,7 +1030,7 @@
"102423"
]
},
- "execution_count": 47,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -1041,7 +1041,7 @@
},
{
"cell_type": "code",
- "execution_count": 48,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -1050,7 +1050,7 @@
"10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
]
},
- "execution_count": 48,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -1061,7 +1061,7 @@
},
{
"cell_type": "code",
- "execution_count": 53,
+ "execution_count": 42,
"metadata": {},
"outputs": [
{
@@ -1070,7 +1070,7 @@
"TRUE"
]
},
- "execution_count": 53,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -1093,7 +1093,7 @@
},
{
"cell_type": "code",
- "execution_count": 54,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -1102,7 +1102,7 @@
"\"12.04\""
]
},
- "execution_count": 54,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -1113,7 +1113,7 @@
},
{
"cell_type": "code",
- "execution_count": 55,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -1122,7 +1122,7 @@
"\"-1.204\""
]
},
- "execution_count": 55,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -1133,7 +1133,7 @@
},
{
"cell_type": "code",
- "execution_count": 56,
+ "execution_count": 45,
"metadata": {},
"outputs": [
{
@@ -1142,7 +1142,7 @@
"\"0.00\""
]
},
- "execution_count": 56,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -1153,7 +1153,7 @@
},
{
"cell_type": "code",
- "execution_count": 57,
+ "execution_count": 46,
"metadata": {},
"outputs": [
{
@@ -1162,7 +1162,7 @@
"\"120400\""
]
},
- "execution_count": 57,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
@@ -1173,7 +1173,7 @@
},
{
"cell_type": "code",
- "execution_count": 58,
+ "execution_count": 47,
"metadata": {},
"outputs": [
{
@@ -1182,7 +1182,7 @@
"\"-0.010\""
]
},
- "execution_count": 58,
+ "execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
@@ -1204,7 +1204,7 @@
},
{
"cell_type": "code",
- "execution_count": 59,
+ "execution_count": 48,
"metadata": {},
"outputs": [
{
@@ -1213,7 +1213,7 @@
"\"1024\""
]
},
- "execution_count": 59,
+ "execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
@@ -1224,7 +1224,7 @@
},
{
"cell_type": "code",
- "execution_count": 60,
+ "execution_count": 49,
"metadata": {},
"outputs": [
{
@@ -1233,7 +1233,7 @@
"\"1024\""
]
},
- "execution_count": 60,
+ "execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@@ -1244,7 +1244,7 @@
},
{
"cell_type": "code",
- "execution_count": 61,
+ "execution_count": 50,
"metadata": {},
"outputs": [
{
@@ -1253,7 +1253,7 @@
"\"{2,3,5}\""
]
},
- "execution_count": 61,
+ "execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
@@ -1264,7 +1264,7 @@
},
{
"cell_type": "code",
- "execution_count": 65,
+ "execution_count": 51,
"metadata": {},
"outputs": [
{
@@ -1273,7 +1273,7 @@
"\"((TRUE|->3)|->{(11|->rec(a:22,b:33))})\""
]
},
- "execution_count": 65,
+ "execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
@@ -1298,7 +1298,7 @@
},
{
"cell_type": "code",
- "execution_count": 68,
+ "execution_count": 52,
"metadata": {},
"outputs": [
{
@@ -1307,7 +1307,7 @@
"\"two to the power ten = 1024\""
]
},
- "execution_count": 68,
+ "execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
@@ -1318,7 +1318,7 @@
},
{
"cell_type": "code",
- "execution_count": 70,
+ "execution_count": 53,
"metadata": {},
"outputs": [
{
@@ -1327,7 +1327,7 @@
"\"My two sets are {1,2} and {}\""
]
},
- "execution_count": 70,
+ "execution_count": 53,
"metadata": {},
"output_type": "execute_result"
}
@@ -1377,19 +1377,19 @@
},
{
"cell_type": "code",
- "execution_count": 72,
+ "execution_count": 54,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-11 14:32:16,550, T+4478378] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n",
- "[2018-05-11 14:32:17,803, T+4479631] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51046\n",
- "[2018-05-11 14:32:17,804, T+4479632] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 42415\n",
- "[2018-05-11 14:32:17,838, T+4479666] \"ProB Output Logger for instance 4ef86d47\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-05-11 14:32:17,839, T+4479667] \"ProB Output Logger for instance 4ef86d47\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
- "[2018-05-11 14:32:17,943, T+4479771] \"ProB Output Logger for instance 4ef86d47\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests])\u001b[0m\n"
+ "[2018-05-13 09:48:06,965, T+8884] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n",
+ "[2018-05-13 09:48:08,087, T+10006] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54038\n",
+ "[2018-05-13 09:48:08,088, T+10007] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62740\n",
+ "[2018-05-13 09:48:08,090, T+10009] \"ProB Output Logger for instance 2f1db1bc\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-05-13 09:48:08,107, T+10026] \"ProB Output Logger for instance 2f1db1bc\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
+ "[2018-05-13 09:48:08,207, T+10126] \"ProB Output Logger for instance 2f1db1bc\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])\u001b[0m\n"
]
},
{
@@ -1398,7 +1398,7 @@
"Loaded machine: Jupyter_CHOOSE : []\n"
]
},
- "execution_count": 72,
+ "execution_count": 54,
"metadata": {},
"output_type": "execute_result"
}
@@ -1414,7 +1414,7 @@
},
{
"cell_type": "code",
- "execution_count": 73,
+ "execution_count": 55,
"metadata": {},
"outputs": [
{
@@ -1423,7 +1423,7 @@
"1"
]
},
- "execution_count": 73,
+ "execution_count": 55,
"metadata": {},
"output_type": "execute_result"
}
@@ -1434,7 +1434,7 @@
},
{
"cell_type": "code",
- "execution_count": 74,
+ "execution_count": 56,
"metadata": {},
"outputs": [
{
@@ -1443,7 +1443,7 @@
"1"
]
},
- "execution_count": 74,
+ "execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
@@ -1454,7 +1454,7 @@
},
{
"cell_type": "code",
- "execution_count": 76,
+ "execution_count": 57,
"metadata": {},
"outputs": [
{
@@ -1463,7 +1463,7 @@
"\"a\""
]
},
- "execution_count": 76,
+ "execution_count": 57,
"metadata": {},
"output_type": "execute_result"
}
@@ -1474,7 +1474,7 @@
},
{
"cell_type": "code",
- "execution_count": 77,
+ "execution_count": 58,
"metadata": {},
"outputs": [
{
@@ -1483,7 +1483,7 @@
"0"
]
},
- "execution_count": 77,
+ "execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
@@ -1494,7 +1494,7 @@
},
{
"cell_type": "code",
- "execution_count": 78,
+ "execution_count": 59,
"metadata": {},
"outputs": [
{
@@ -1503,7 +1503,7 @@
"0"
]
},
- "execution_count": 78,
+ "execution_count": 59,
"metadata": {},
"output_type": "execute_result"
}
@@ -1537,6 +1537,204 @@
"`"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Sorting Sets\n",
+ "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "`DEFINITIONS \"SORT.def\"`\n",
+ "\n",
+ "Alternatively you can use the following if you use ProB prior to version 1.7.1:\n",
+ "`\n",
+ "DEFINITIONS\n",
+ " SORT(X) == [];\n",
+ " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T));\n",
+ "`\n",
+ "\n",
+ "This external function SORT takes a set and translates it into a B sequence.\n",
+ "It uses ProB's internal order for sorting the elements.\n",
+ "It will not work for infinite sets.\n",
+ "Type: $POW(\\tau) \\rightarrow seq(\\tau)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 60,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-13 09:48:08,755, T+10674] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n",
+ "[2018-05-13 09:48:09,935, T+11854] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54042\n",
+ "[2018-05-13 09:48:09,935, T+11854] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62744\n",
+ "[2018-05-13 09:48:09,937, T+11856] \"ProB Output Logger for instance f4b34d8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
+ "[2018-05-13 09:48:09,963, T+11882] \"ProB Output Logger for instance f4b34d8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
+ "[2018-05-13 09:48:10,084, T+12003] \"ProB Output Logger for instance f4b34d8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])\u001b[0m\n"
+ ]
+ },
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_CHOOSE : []\n"
+ ]
+ },
+ "execution_count": 60,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_CHOOSE\n",
+ "DEFINITIONS\n",
+ " SORT(X) == [];\n",
+ " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T))\n",
+ " END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 61,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "[1,2,3]"
+ ]
+ },
+ "execution_count": 61,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT(1..3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 62,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "[6,9,27]"
+ ]
+ },
+ "execution_count": 62,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({3*3,3+3,3**3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 63,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "[\"1\",\"10\",\"11\",\"2\",\"a\",\"aa\",\"ab\",\"b\"]"
+ ]
+ },
+ "execution_count": 63,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({\"ab\",\"aa\",\"a\",\"b\",\"10\",\"1\",\"2\",\"11\"})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 64,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "[(\"a\"↦0),(\"a\"↦1),(\"b\"↦0)]"
+ ]
+ },
+ "execution_count": 64,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({(\"a\"|->1),(\"b\"|->0),(\"a\"|->0)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A related external function is LEQ_SYM_BREAK which allows one to compare values of arbitrary type.\n",
+ "Calls to this external function are automatically\n",
+ "inserted by ProB for symmetry breaking of quantifiers.\n",
+ "It should currently not be used for sets or sequences."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryIO\n",
+ "\n",
+ "This library provides various input/output facilities.\n",
+ "It is probably most useful for debugging, but can also be used to write B machines\n",
+ "which can read and write data.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryIO.def\"`\n",
+ "\n",
+ "The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryXML\n",
+ "\n",
+ "This library provides various functions to read and write XML data from file and strings.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryXML.def\"`\n",
+ "\n",
+ "The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.\n",
+ "\n",
+ "### Internal Data Type\n",
+ "\n",
+ "An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence\n",
+ " of XML elements, whose type is defined by the following (included in the LibraryXML.def file):\n",
+ "\n",
+ "`\n",
+ " XML_ELement_Type == \n",
+ " struct(\n",
+ " recId: NATURAL1,\n",
+ " pId:NATURAL,\n",
+ " element:STRING,\n",
+ " attributes: STRING +-> STRING,\n",
+ " meta: STRING +-> STRING\n",
+ " );\n",
+ "`\n",
+ "\n",
+ "### Files and Strings\n",
+ "\n",
+ "XML documents can either be stored in a file or in a B string."
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,
--
GitLab