diff --git a/notebooks/experiments/DeliveryExercise.ipynb b/notebooks/experiments/DeliveryExercise.ipynb
index 460b813b45941740e1c4a54da2b0cca2431da295..902fbab70f0258799b007e1ff5de14f1764da32e 100644
--- a/notebooks/experiments/DeliveryExercise.ipynb
+++ b/notebooks/experiments/DeliveryExercise.ipynb
@@ -26,7 +26,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 1,
"metadata": {
"deletable": false,
"editable": false,
@@ -46,7 +46,7 @@
"Loaded machine: exercise1"
]
},
- "execution_count": 25,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -68,7 +68,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 2,
"metadata": {
"nbgrader": {
"grade": false,
@@ -86,7 +86,7 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
- "execution_count": 26,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -130,7 +130,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 3,
"metadata": {
"nbgrader": {
"grade": false,
@@ -151,7 +151,7 @@
"{c1,c2}"
]
},
- "execution_count": 16,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -162,7 +162,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 4,
"metadata": {
"nbgrader": {
"grade": true,
@@ -176,12 +176,17 @@
},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol1",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol1\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -207,7 +212,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 5,
"metadata": {
"nbgrader": {
"grade": false,
@@ -228,7 +233,7 @@
"{a1,a2,a3,a4,a5}"
]
},
- "execution_count": 22,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -239,7 +244,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 6,
"metadata": {
"nbgrader": {
"grade": true,
@@ -261,7 +266,7 @@
"\"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\""
]
},
- "execution_count": 23,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -272,7 +277,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 7,
"metadata": {
"nbgrader": {
"grade": true,
@@ -286,12 +291,17 @@
},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol2",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol2\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -316,13 +326,6 @@
"}\n",
"```"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb
index ffac438b38be2227723c689333acf9a495b68208..a953d6737997549009d5f79095361813e65f3ee6 100644
--- a/notebooks/experiments/SMT_Translation_Experiments.ipynb
+++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb
@@ -16,10 +16,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"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:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
@@ -34,10 +34,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available",
"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:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
@@ -75,10 +75,10 @@
{
"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} \\mathbin\\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} \\mathbin\\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\mathbin\\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} \\mathbin\\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\mathbin\\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$"
+ "$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge \\exists \\mathit{st13}\\cdot (\\mathit{r} = \\mathit{st13} \\wedge (\\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\mathbin\\Rightarrow \\exists \\mathit{st14}\\cdot (\\exists \\mathit{st16}\\cdot (\\mathit{st14} \\mapsto \\mathit{st15} \\in \\mathit{st16} \\wedge (\\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16} \\mathbin\\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16}))) \\wedge \\mathit{st14} \\in \\{6\\})) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st14}\\cdot (\\exists \\mathit{st19}\\cdot (\\mathit{st14} \\mapsto \\mathit{st15} \\in \\mathit{st19} \\wedge (\\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19} \\mathbin\\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\wedge \\mathit{st14} \\in \\{6\\}) \\mathbin\\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)))"
+ "f = {(1↦3),(2↦6)} ∧ ∃st13·(r = st13 ∧ (∀st15·(st15 ∈ st13 ⇒ ∃st14·(∃st16·(st14 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16))) ∧ st14 ∈ {6})) ∧ ∀st15·(∃st14·(∃st19·(st14 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ∧ st14 ∈ {6}) ⇒ st15 ∈ st13)))"
]
},
"execution_count": 3,
@@ -104,10 +104,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 0.347330269 seconds"
+ "Execution time: 0.394252508 seconds"
],
"text/plain": [
- "Execution time: 0.347330269 seconds"
+ "Execution time: 0.394252508 seconds"
]
},
"metadata": {},
@@ -211,10 +211,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp50'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[nodeid(pos(16,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp55'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp56'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp56'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp57'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp58'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp58'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp54'])]),b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp59'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp60'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp60'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp61'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp62'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp62'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp51'])]),b(member(b(identifier('_smt_tmp50'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(20,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(19,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(15,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])]),b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp63'])]),b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp48'])])),pred,[])),pred,[])))",
"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:solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp49'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp50'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp51'),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[nodeid(pos(16,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp55'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp56'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp56'),integer,[]),b(identifier('_smt_tmp55'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp55'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp57'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp58'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp58'),integer,[]),b(identifier('_smt_tmp57'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp57'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp54'])]),b(forall([b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp52'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp54'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp59'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp53'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[nodeid(pos(17,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp60'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp60'),integer,[]),b(identifier('_smt_tmp59'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp59'])])),pred,[used_ids(['_smt_tmp53'])]),b(exists([b(identifier('_smt_tmp61'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp52'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[nodeid(pos(18,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp62'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp62'),integer,[]),b(identifier('_smt_tmp61'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp61'])])),pred,[used_ids(['_smt_tmp52'])])),pred,[])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp54'])])),pred,[used_ids(['_smt_tmp51'])]),b(member(b(identifier('_smt_tmp50'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(20,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(19,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(15,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp48'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])]),b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp63'])]),b(forall([b(identifier('_smt_tmp64'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp63'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp65'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp64'),couple(integer,integer),[]),b(identifier('_smt_tmp65'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(21,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp64'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp63'])])),pred,[used_ids(['_smt_tmp48'])])),pred,[])),pred,[])))\u001b[0m"
]
}
],
@@ -239,10 +239,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp108'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[nodeid(pos(17,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp113'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp114'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp114'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp115'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp116'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp116'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp112'])]),b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp117'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp118'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp118'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp119'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp120'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp120'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp109'])]),b(member(b(identifier('_smt_tmp108'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(21,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(20,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(16,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])]),b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp121'])]),b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp106'])])),pred,[])),pred,[])))",
"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:solve: Computation not completed: no solution found (but one might exist), reason: unsupported_type_or_expression(comprehension_set([b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])],b(conjunct(b(member(b(couple(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp107'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(comprehension_set([b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp108'),boolean,[])],b(conjunct(b(exists([b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp109'),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[nodeid(pos(17,-1,2,7,2,22))])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(conjunct(b(exists([b(identifier('_smt_tmp113'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp114'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp114'),integer,[]),b(identifier('_smt_tmp113'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp113'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp115'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp116'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp116'),integer,[]),b(identifier('_smt_tmp115'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp115'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[]),b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp112'])]),b(forall([b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])],b(member(b(couple(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp110'),integer,[])),couple(integer,integer),[]),b(identifier('_smt_tmp112'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(exists([b(identifier('_smt_tmp117'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp111'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[nodeid(pos(18,-1,2,7,2,14))])),pred,[]),b(forall([b(identifier('_smt_tmp118'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp118'),integer,[]),b(identifier('_smt_tmp117'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp117'])])),pred,[used_ids(['_smt_tmp111'])]),b(exists([b(identifier('_smt_tmp119'),set(integer),[])],b(conjunct(b(member(b(identifier('_smt_tmp110'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[nodeid(pos(19,-1,2,15,2,22))])),pred,[]),b(forall([b(identifier('_smt_tmp120'),integer,[])],b(truth,pred,[]),b(member(b(identifier('_smt_tmp120'),integer,[]),b(identifier('_smt_tmp119'),set(integer),[])),pred,[])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp119'])])),pred,[used_ids(['_smt_tmp110'])])),pred,[])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp112'])])),pred,[used_ids(['_smt_tmp109'])]),b(member(b(identifier('_smt_tmp108'),boolean,[]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(21,-1,2,25,2,30))])]),set(boolean),[nodeid(pos(20,-1,2,24,2,31))])),pred,[])),pred,[])),set(couple(couple(integer,integer),boolean)),[nodeid(pos(16,-1,2,7,2,31))])),pred,[]),b(negation(b(exists([b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])],b(conjunct(b(member(b(identifier('_smt_tmp106'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(conjunct(b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])]),b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[])),pred,[used_ids(['_smt_tmp121'])]),b(forall([b(identifier('_smt_tmp122'),couple(integer,integer),[])],b(member(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp121'),set(couple(integer,integer)),[])),pred,[]),b(exists([b(identifier('_smt_tmp123'),boolean,[])],b(member(b(couple(b(identifier('_smt_tmp122'),couple(integer,integer),[]),b(identifier('_smt_tmp123'),boolean,[])),couple(couple(integer,integer),boolean),[]),b(value(avl_set(node(','(','(int(1),int(3)),pred_true),true,1,empty,node(','(','(int(2),int(6)),pred_true),true,0,empty,empty)))),set(couple(couple(integer,integer),boolean)),[nodeid(pos(22,-1,2,36,2,59))])),pred,[])),pred,[used_ids(['_smt_tmp122'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp121'])])),pred,[used_ids(['_smt_tmp106'])])),pred,[])),pred,[])))\u001b[0m"
]
}
],
diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index dabc22c1c0c03e4c6b82d875e0a15caf6181910a..86e0e88aa70ec9f9af1e261b1bec8c0b32c13e83 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -57,7 +57,7 @@
},
{
"cell_type": "code",
- "execution_count": 198,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -69,7 +69,7 @@
"\"abcabc\""
]
},
- "execution_count": 198,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -80,7 +80,7 @@
},
{
"cell_type": "code",
- "execution_count": 199,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -92,7 +92,7 @@
"\"abc\""
]
},
- "execution_count": 199,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -114,7 +114,7 @@
},
{
"cell_type": "code",
- "execution_count": 200,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -126,7 +126,7 @@
"3"
]
},
- "execution_count": 200,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -137,7 +137,7 @@
},
{
"cell_type": "code",
- "execution_count": 201,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -149,7 +149,7 @@
"0"
]
},
- "execution_count": 201,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -172,7 +172,7 @@
},
{
"cell_type": "code",
- "execution_count": 202,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -184,7 +184,7 @@
"{(1↦\"filename\"),(2↦\"ext\")}"
]
},
- "execution_count": 202,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -195,7 +195,7 @@
},
{
"cell_type": "code",
- "execution_count": 203,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -207,7 +207,7 @@
"{(1↦\"filename.ext\")}"
]
},
- "execution_count": 203,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -218,19 +218,19 @@
},
{
"cell_type": "code",
- "execution_count": 204,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"usr\"},\\text{\"local\"},\\text{\"lib\"}]$"
+ "$\\{(1\\mapsto\\text{\"usr\"}),(2\\mapsto\\text{\"local\"}),(3\\mapsto\\text{\"lib\"})\\}$"
],
"text/plain": [
- "[\"usr\",\"local\",\"lib\"]"
+ "{(1↦\"usr\"),(2↦\"local\"),(3↦\"lib\")}"
]
},
- "execution_count": 204,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -241,7 +241,7 @@
},
{
"cell_type": "code",
- "execution_count": 205,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -253,7 +253,7 @@
"{(1↦\"\")}"
]
},
- "execution_count": 205,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -271,7 +271,7 @@
},
{
"cell_type": "code",
- "execution_count": 206,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
@@ -283,7 +283,7 @@
"{(1↦\"usr/local/lib\")}"
]
},
- "execution_count": 206,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -294,7 +294,7 @@
},
{
"cell_type": "code",
- "execution_count": 207,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -306,7 +306,7 @@
"{(1↦\"usr/lo\"),(2↦\"/lib\")}"
]
},
- "execution_count": 207,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -329,7 +329,7 @@
},
{
"cell_type": "code",
- "execution_count": 208,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
@@ -341,7 +341,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 208,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -352,7 +352,7 @@
},
{
"cell_type": "code",
- "execution_count": 209,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
@@ -364,7 +364,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 209,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -375,7 +375,7 @@
},
{
"cell_type": "code",
- "execution_count": 210,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
@@ -387,7 +387,7 @@
"\"usr/local/lib\""
]
},
- "execution_count": 210,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -410,7 +410,7 @@
},
{
"cell_type": "code",
- "execution_count": 211,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
@@ -422,7 +422,7 @@
"∅"
]
},
- "execution_count": 211,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -433,19 +433,19 @@
},
{
"cell_type": "code",
- "execution_count": 212,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"a\"},\\text{\"b\"},\\text{\"c\"}]$"
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"})\\}$"
],
"text/plain": [
- "[\"a\",\"b\",\"c\"]"
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\")}"
]
},
- "execution_count": 212,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -456,7 +456,7 @@
},
{
"cell_type": "code",
- "execution_count": 213,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -468,7 +468,7 @@
"\"a.b.c\""
]
},
- "execution_count": 213,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -492,7 +492,7 @@
},
{
"cell_type": "code",
- "execution_count": 214,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -504,7 +504,7 @@
"∅"
]
},
- "execution_count": 214,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -515,19 +515,19 @@
},
{
"cell_type": "code",
- "execution_count": 215,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[65,90,32,97,122,32,48,57]$"
+ "$\\{(1\\mapsto 65),(2\\mapsto 90),(3\\mapsto 32),(4\\mapsto 97),(5\\mapsto 122),(6\\mapsto 32),(7\\mapsto 48),(8\\mapsto 57)\\}$"
],
"text/plain": [
- "[65,90,32,97,122,32,48,57]"
+ "{(1↦65),(2↦90),(3↦32),(4↦97),(5↦122),(6↦32),(7↦48),(8↦57)}"
]
},
- "execution_count": 215,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -549,7 +549,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 20,
"metadata": {},
"outputs": [
{
@@ -561,7 +561,7 @@
"\"ABC\""
]
},
- "execution_count": 2,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -583,7 +583,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 21,
"metadata": {},
"outputs": [
{
@@ -595,7 +595,7 @@
"\"ABC_ABC\""
]
},
- "execution_count": 3,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
@@ -606,7 +606,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 22,
"metadata": {},
"outputs": [
{
@@ -618,7 +618,7 @@
"\"AZ-AZ-09-AAOU-AO\""
]
},
- "execution_count": 7,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -629,7 +629,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 23,
"metadata": {},
"outputs": [
{
@@ -641,7 +641,7 @@
"\"\""
]
},
- "execution_count": 5,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
@@ -663,7 +663,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 24,
"metadata": {},
"outputs": [
{
@@ -675,7 +675,7 @@
"\"az-az-09-aaou-ao\""
]
},
- "execution_count": 2,
+ "execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
@@ -698,7 +698,7 @@
},
{
"cell_type": "code",
- "execution_count": 216,
+ "execution_count": 25,
"metadata": {},
"outputs": [
{
@@ -710,7 +710,7 @@
"\"abc\""
]
},
- "execution_count": 216,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
@@ -721,7 +721,7 @@
},
{
"cell_type": "code",
- "execution_count": 217,
+ "execution_count": 26,
"metadata": {},
"outputs": [
{
@@ -733,7 +733,7 @@
"\"abcdefg\""
]
},
- "execution_count": 217,
+ "execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
@@ -744,7 +744,7 @@
},
{
"cell_type": "code",
- "execution_count": 218,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
@@ -756,7 +756,7 @@
"\"de\""
]
},
- "execution_count": 218,
+ "execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
@@ -767,7 +767,7 @@
},
{
"cell_type": "code",
- "execution_count": 219,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
@@ -779,7 +779,7 @@
"\"\""
]
},
- "execution_count": 219,
+ "execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
@@ -790,7 +790,7 @@
},
{
"cell_type": "code",
- "execution_count": 220,
+ "execution_count": 29,
"metadata": {},
"outputs": [
{
@@ -802,7 +802,7 @@
"\"\""
]
},
- "execution_count": 220,
+ "execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
@@ -830,7 +830,7 @@
},
{
"cell_type": "code",
- "execution_count": 221,
+ "execution_count": 30,
"metadata": {},
"outputs": [
{
@@ -842,7 +842,7 @@
"TRUE"
]
},
- "execution_count": 221,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
@@ -853,7 +853,7 @@
},
{
"cell_type": "code",
- "execution_count": 222,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
@@ -865,7 +865,7 @@
"TRUE"
]
},
- "execution_count": 222,
+ "execution_count": 31,
"metadata": {},
"output_type": "execute_result"
}
@@ -876,7 +876,7 @@
},
{
"cell_type": "code",
- "execution_count": 223,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -888,7 +888,7 @@
"TRUE"
]
},
- "execution_count": 223,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -899,7 +899,7 @@
},
{
"cell_type": "code",
- "execution_count": 224,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -911,7 +911,7 @@
"FALSE"
]
},
- "execution_count": 224,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -922,7 +922,7 @@
},
{
"cell_type": "code",
- "execution_count": 225,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -934,7 +934,7 @@
"FALSE"
]
},
- "execution_count": 225,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -945,7 +945,7 @@
},
{
"cell_type": "code",
- "execution_count": 226,
+ "execution_count": 35,
"metadata": {},
"outputs": [
{
@@ -957,7 +957,7 @@
"FALSE"
]
},
- "execution_count": 226,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -968,7 +968,7 @@
},
{
"cell_type": "code",
- "execution_count": 227,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
@@ -980,7 +980,7 @@
"TRUE"
]
},
- "execution_count": 227,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
@@ -991,7 +991,7 @@
},
{
"cell_type": "code",
- "execution_count": 228,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -1003,7 +1003,7 @@
"TRUE"
]
},
- "execution_count": 228,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -1014,7 +1014,7 @@
},
{
"cell_type": "code",
- "execution_count": 229,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -1026,7 +1026,7 @@
"TRUE"
]
},
- "execution_count": 229,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -1050,7 +1050,7 @@
},
{
"cell_type": "code",
- "execution_count": 230,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -1062,7 +1062,7 @@
"1024"
]
},
- "execution_count": 230,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -1073,7 +1073,7 @@
},
{
"cell_type": "code",
- "execution_count": 231,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -1085,7 +1085,7 @@
"−1"
]
},
- "execution_count": 231,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -1107,7 +1107,7 @@
},
{
"cell_type": "code",
- "execution_count": 232,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -1119,7 +1119,7 @@
"\"1024\""
]
},
- "execution_count": 232,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -1130,7 +1130,7 @@
},
{
"cell_type": "code",
- "execution_count": 233,
+ "execution_count": 42,
"metadata": {},
"outputs": [
{
@@ -1142,7 +1142,7 @@
"\"-1024\""
]
},
- "execution_count": 233,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -1153,7 +1153,7 @@
},
{
"cell_type": "code",
- "execution_count": 234,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -1165,7 +1165,7 @@
"\"-1\""
]
},
- "execution_count": 234,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -1176,7 +1176,7 @@
},
{
"cell_type": "code",
- "execution_count": 235,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -1188,7 +1188,7 @@
"TRUE"
]
},
- "execution_count": 235,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -1210,7 +1210,7 @@
},
{
"cell_type": "code",
- "execution_count": 236,
+ "execution_count": 45,
"metadata": {},
"outputs": [
{
@@ -1222,7 +1222,7 @@
"1024"
]
},
- "execution_count": 236,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -1233,7 +1233,7 @@
},
{
"cell_type": "code",
- "execution_count": 237,
+ "execution_count": 46,
"metadata": {},
"outputs": [
{
@@ -1245,7 +1245,7 @@
"102400"
]
},
- "execution_count": 237,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
@@ -1256,7 +1256,7 @@
},
{
"cell_type": "code",
- "execution_count": 238,
+ "execution_count": 47,
"metadata": {},
"outputs": [
{
@@ -1268,7 +1268,7 @@
"102"
]
},
- "execution_count": 238,
+ "execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
@@ -1279,7 +1279,7 @@
},
{
"cell_type": "code",
- "execution_count": 239,
+ "execution_count": 48,
"metadata": {},
"outputs": [
{
@@ -1291,7 +1291,7 @@
"103"
]
},
- "execution_count": 239,
+ "execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
@@ -1302,7 +1302,7 @@
},
{
"cell_type": "code",
- "execution_count": 240,
+ "execution_count": 49,
"metadata": {},
"outputs": [
{
@@ -1314,7 +1314,7 @@
"−103"
]
},
- "execution_count": 240,
+ "execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@@ -1325,7 +1325,7 @@
},
{
"cell_type": "code",
- "execution_count": 241,
+ "execution_count": 50,
"metadata": {},
"outputs": [
{
@@ -1337,7 +1337,7 @@
"102423"
]
},
- "execution_count": 241,
+ "execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
@@ -1348,7 +1348,7 @@
},
{
"cell_type": "code",
- "execution_count": 242,
+ "execution_count": 51,
"metadata": {},
"outputs": [
{
@@ -1360,7 +1360,7 @@
"10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
]
},
- "execution_count": 242,
+ "execution_count": 51,
"metadata": {},
"output_type": "execute_result"
}
@@ -1371,7 +1371,7 @@
},
{
"cell_type": "code",
- "execution_count": 243,
+ "execution_count": 52,
"metadata": {},
"outputs": [
{
@@ -1383,7 +1383,7 @@
"TRUE"
]
},
- "execution_count": 243,
+ "execution_count": 52,
"metadata": {},
"output_type": "execute_result"
}
@@ -1406,7 +1406,7 @@
},
{
"cell_type": "code",
- "execution_count": 244,
+ "execution_count": 53,
"metadata": {},
"outputs": [
{
@@ -1418,7 +1418,7 @@
"\"12.04\""
]
},
- "execution_count": 244,
+ "execution_count": 53,
"metadata": {},
"output_type": "execute_result"
}
@@ -1429,7 +1429,7 @@
},
{
"cell_type": "code",
- "execution_count": 245,
+ "execution_count": 54,
"metadata": {},
"outputs": [
{
@@ -1441,7 +1441,7 @@
"\"-1.204\""
]
},
- "execution_count": 245,
+ "execution_count": 54,
"metadata": {},
"output_type": "execute_result"
}
@@ -1452,7 +1452,7 @@
},
{
"cell_type": "code",
- "execution_count": 246,
+ "execution_count": 55,
"metadata": {},
"outputs": [
{
@@ -1464,7 +1464,7 @@
"\"0.00\""
]
},
- "execution_count": 246,
+ "execution_count": 55,
"metadata": {},
"output_type": "execute_result"
}
@@ -1475,7 +1475,7 @@
},
{
"cell_type": "code",
- "execution_count": 247,
+ "execution_count": 56,
"metadata": {},
"outputs": [
{
@@ -1487,7 +1487,7 @@
"\"120400\""
]
},
- "execution_count": 247,
+ "execution_count": 56,
"metadata": {},
"output_type": "execute_result"
}
@@ -1498,7 +1498,7 @@
},
{
"cell_type": "code",
- "execution_count": 248,
+ "execution_count": 57,
"metadata": {},
"outputs": [
{
@@ -1510,7 +1510,7 @@
"\"-0.010\""
]
},
- "execution_count": 248,
+ "execution_count": 57,
"metadata": {},
"output_type": "execute_result"
}
@@ -1532,7 +1532,7 @@
},
{
"cell_type": "code",
- "execution_count": 249,
+ "execution_count": 58,
"metadata": {},
"outputs": [
{
@@ -1544,7 +1544,7 @@
"\"fe\""
]
},
- "execution_count": 249,
+ "execution_count": 58,
"metadata": {},
"output_type": "execute_result"
}
@@ -1555,7 +1555,7 @@
},
{
"cell_type": "code",
- "execution_count": 250,
+ "execution_count": 59,
"metadata": {},
"outputs": [
{
@@ -1567,7 +1567,7 @@
"\"0\""
]
},
- "execution_count": 250,
+ "execution_count": 59,
"metadata": {},
"output_type": "execute_result"
}
@@ -1578,7 +1578,7 @@
},
{
"cell_type": "code",
- "execution_count": 251,
+ "execution_count": 60,
"metadata": {},
"outputs": [
{
@@ -1590,7 +1590,7 @@
"\"-fe\""
]
},
- "execution_count": 251,
+ "execution_count": 60,
"metadata": {},
"output_type": "execute_result"
}
@@ -1601,7 +1601,7 @@
},
{
"cell_type": "code",
- "execution_count": 252,
+ "execution_count": 61,
"metadata": {},
"outputs": [
{
@@ -1613,7 +1613,7 @@
"\"fffffffffffffffffffffffff\""
]
},
- "execution_count": 252,
+ "execution_count": 61,
"metadata": {},
"output_type": "execute_result"
}
@@ -1635,7 +1635,7 @@
},
{
"cell_type": "code",
- "execution_count": 253,
+ "execution_count": 62,
"metadata": {},
"outputs": [
{
@@ -1647,7 +1647,7 @@
"\"1024\""
]
},
- "execution_count": 253,
+ "execution_count": 62,
"metadata": {},
"output_type": "execute_result"
}
@@ -1658,7 +1658,7 @@
},
{
"cell_type": "code",
- "execution_count": 254,
+ "execution_count": 63,
"metadata": {},
"outputs": [
{
@@ -1670,7 +1670,7 @@
"\"1024\""
]
},
- "execution_count": 254,
+ "execution_count": 63,
"metadata": {},
"output_type": "execute_result"
}
@@ -1681,7 +1681,7 @@
},
{
"cell_type": "code",
- "execution_count": 255,
+ "execution_count": 64,
"metadata": {},
"outputs": [
{
@@ -1693,7 +1693,7 @@
"\"{2,3,5}\""
]
},
- "execution_count": 255,
+ "execution_count": 64,
"metadata": {},
"output_type": "execute_result"
}
@@ -1704,7 +1704,7 @@
},
{
"cell_type": "code",
- "execution_count": 256,
+ "execution_count": 65,
"metadata": {},
"outputs": [
{
@@ -1716,7 +1716,7 @@
"\"(TRUE|->3|->{(11|->rec(a:22,b:33))})\""
]
},
- "execution_count": 256,
+ "execution_count": 65,
"metadata": {},
"output_type": "execute_result"
}
@@ -1741,7 +1741,7 @@
},
{
"cell_type": "code",
- "execution_count": 257,
+ "execution_count": 66,
"metadata": {},
"outputs": [
{
@@ -1753,7 +1753,7 @@
"\"two to the power ten = 1024\""
]
},
- "execution_count": 257,
+ "execution_count": 66,
"metadata": {},
"output_type": "execute_result"
}
@@ -1764,7 +1764,7 @@
},
{
"cell_type": "code",
- "execution_count": 258,
+ "execution_count": 67,
"metadata": {},
"outputs": [
{
@@ -1776,7 +1776,7 @@
"\"My two sets are {1,2} and {}\""
]
},
- "execution_count": 258,
+ "execution_count": 67,
"metadata": {},
"output_type": "execute_result"
}
@@ -1818,7 +1818,7 @@
},
{
"cell_type": "code",
- "execution_count": 259,
+ "execution_count": 68,
"metadata": {},
"outputs": [
{
@@ -1830,7 +1830,7 @@
"\"dom({1 |-> 2})\""
]
},
- "execution_count": 259,
+ "execution_count": 68,
"metadata": {},
"output_type": "execute_result"
}
@@ -1848,7 +1848,7 @@
},
{
"cell_type": "code",
- "execution_count": 260,
+ "execution_count": 69,
"metadata": {},
"outputs": [
{
@@ -1860,7 +1860,7 @@
"\"{1}\""
]
},
- "execution_count": 260,
+ "execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
@@ -1871,7 +1871,7 @@
},
{
"cell_type": "code",
- "execution_count": 261,
+ "execution_count": 70,
"metadata": {},
"outputs": [
{
@@ -1886,7 +1886,7 @@
"\"\\\"abc\\\"\"\t\"abc\"\n"
]
},
- "execution_count": 261,
+ "execution_count": 70,
"metadata": {},
"output_type": "execute_result"
}
@@ -1918,7 +1918,7 @@
},
{
"cell_type": "code",
- "execution_count": 262,
+ "execution_count": 71,
"metadata": {},
"outputs": [
{
@@ -1927,7 +1927,7 @@
"Loaded machine: Jupyter_CHOOSE"
]
},
- "execution_count": 262,
+ "execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
@@ -1941,7 +1941,7 @@
},
{
"cell_type": "code",
- "execution_count": 263,
+ "execution_count": 72,
"metadata": {},
"outputs": [
{
@@ -1953,7 +1953,7 @@
"1"
]
},
- "execution_count": 263,
+ "execution_count": 72,
"metadata": {},
"output_type": "execute_result"
}
@@ -1964,7 +1964,7 @@
},
{
"cell_type": "code",
- "execution_count": 264,
+ "execution_count": 73,
"metadata": {},
"outputs": [
{
@@ -1976,7 +1976,7 @@
"1"
]
},
- "execution_count": 264,
+ "execution_count": 73,
"metadata": {},
"output_type": "execute_result"
}
@@ -1987,7 +1987,7 @@
},
{
"cell_type": "code",
- "execution_count": 265,
+ "execution_count": 74,
"metadata": {},
"outputs": [
{
@@ -1999,7 +1999,7 @@
"\"a\""
]
},
- "execution_count": 265,
+ "execution_count": 74,
"metadata": {},
"output_type": "execute_result"
}
@@ -2010,7 +2010,7 @@
},
{
"cell_type": "code",
- "execution_count": 266,
+ "execution_count": 75,
"metadata": {},
"outputs": [
{
@@ -2022,7 +2022,7 @@
"0"
]
},
- "execution_count": 266,
+ "execution_count": 75,
"metadata": {},
"output_type": "execute_result"
}
@@ -2033,7 +2033,7 @@
},
{
"cell_type": "code",
- "execution_count": 267,
+ "execution_count": 76,
"metadata": {},
"outputs": [
{
@@ -2045,7 +2045,7 @@
"0"
]
},
- "execution_count": 267,
+ "execution_count": 76,
"metadata": {},
"output_type": "execute_result"
}
@@ -2095,7 +2095,7 @@
},
{
"cell_type": "code",
- "execution_count": 268,
+ "execution_count": 77,
"metadata": {},
"outputs": [
{
@@ -2107,7 +2107,7 @@
"2"
]
},
- "execution_count": 268,
+ "execution_count": 77,
"metadata": {},
"output_type": "execute_result"
}
@@ -2118,7 +2118,7 @@
},
{
"cell_type": "code",
- "execution_count": 269,
+ "execution_count": 78,
"metadata": {},
"outputs": [
{
@@ -2130,7 +2130,7 @@
"3"
]
},
- "execution_count": 269,
+ "execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
@@ -2162,7 +2162,7 @@
},
{
"cell_type": "code",
- "execution_count": 270,
+ "execution_count": 79,
"metadata": {},
"outputs": [
{
@@ -2171,7 +2171,7 @@
"Loaded machine: Jupyter_SORT"
]
},
- "execution_count": 270,
+ "execution_count": 79,
"metadata": {},
"output_type": "execute_result"
}
@@ -2185,19 +2185,19 @@
},
{
"cell_type": "code",
- "execution_count": 271,
+ "execution_count": 80,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[1,2,3]$"
+ "$\\{(1\\mapsto 1),(2\\mapsto 2),(3\\mapsto 3)\\}$"
],
"text/plain": [
- "[1,2,3]"
+ "{(1↦1),(2↦2),(3↦3)}"
]
},
- "execution_count": 271,
+ "execution_count": 80,
"metadata": {},
"output_type": "execute_result"
}
@@ -2208,19 +2208,19 @@
},
{
"cell_type": "code",
- "execution_count": 272,
+ "execution_count": 81,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[6,9,27]$"
+ "$\\{(1\\mapsto 6),(2\\mapsto 9),(3\\mapsto 27)\\}$"
],
"text/plain": [
- "[6,9,27]"
+ "{(1↦6),(2↦9),(3↦27)}"
]
},
- "execution_count": 272,
+ "execution_count": 81,
"metadata": {},
"output_type": "execute_result"
}
@@ -2231,19 +2231,19 @@
},
{
"cell_type": "code",
- "execution_count": 273,
+ "execution_count": 82,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"1\"},\\text{\"10\"},\\text{\"11\"},\\text{\"2\"},\\text{\"a\"},\\text{\"aa\"},\\text{\"ab\"},\\text{\"b\"}]$"
+ "$\\{(1\\mapsto\\text{\"1\"}),(2\\mapsto\\text{\"10\"}),(3\\mapsto\\text{\"11\"}),(4\\mapsto\\text{\"2\"}),(5\\mapsto\\text{\"a\"}),(6\\mapsto\\text{\"aa\"}),(7\\mapsto\\text{\"ab\"}),(8\\mapsto\\text{\"b\"})\\}$"
],
"text/plain": [
- "[\"1\",\"10\",\"11\",\"2\",\"a\",\"aa\",\"ab\",\"b\"]"
+ "{(1↦\"1\"),(2↦\"10\"),(3↦\"11\"),(4↦\"2\"),(5↦\"a\"),(6↦\"aa\"),(7↦\"ab\"),(8↦\"b\")}"
]
},
- "execution_count": 273,
+ "execution_count": 82,
"metadata": {},
"output_type": "execute_result"
}
@@ -2254,19 +2254,19 @@
},
{
"cell_type": "code",
- "execution_count": 274,
+ "execution_count": 83,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[(\\text{\"a\"}\\mapsto 0),(\\text{\"a\"}\\mapsto 1),(\\text{\"b\"}\\mapsto 0)]$"
+ "$\\{(1\\mapsto(\\text{\"a\"}\\mapsto 0)),(2\\mapsto(\\text{\"a\"}\\mapsto 1)),(3\\mapsto(\\text{\"b\"}\\mapsto 0))\\}$"
],
"text/plain": [
- "[(\"a\"↦0),(\"a\"↦1),(\"b\"↦0)]"
+ "{(1↦(\"a\"↦0)),(2↦(\"a\"↦1)),(3↦(\"b\"↦0))}"
]
},
- "execution_count": 274,
+ "execution_count": 83,
"metadata": {},
"output_type": "execute_result"
}
@@ -2294,19 +2294,19 @@
},
{
"cell_type": "code",
- "execution_count": 275,
+ "execution_count": 84,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"a\"},\\text{\"b\"},\\text{\"c\"},\\text{\"c\"},\\text{\"d\"}]$"
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"}),(4\\mapsto\\text{\"c\"}),(5\\mapsto\\text{\"d\"})\\}$"
],
"text/plain": [
- "[\"a\",\"b\",\"c\",\"c\",\"d\"]"
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\"),(4↦\"c\"),(5↦\"d\")}"
]
},
- "execution_count": 275,
+ "execution_count": 84,
"metadata": {},
"output_type": "execute_result"
}
@@ -2336,7 +2336,7 @@
},
{
"cell_type": "code",
- "execution_count": 276,
+ "execution_count": 85,
"metadata": {},
"outputs": [
{
@@ -2345,7 +2345,7 @@
"Loaded machine: Jupyter_SCCS"
]
},
- "execution_count": 276,
+ "execution_count": 85,
"metadata": {},
"output_type": "execute_result"
}
@@ -2359,7 +2359,7 @@
},
{
"cell_type": "code",
- "execution_count": 277,
+ "execution_count": 86,
"metadata": {},
"outputs": [
{
@@ -2371,7 +2371,7 @@
"{{1,2},{3,4}}"
]
},
- "execution_count": 277,
+ "execution_count": 86,
"metadata": {},
"output_type": "execute_result"
}
@@ -2382,7 +2382,7 @@
},
{
"cell_type": "code",
- "execution_count": 278,
+ "execution_count": 87,
"metadata": {},
"outputs": [
{
@@ -2391,63 +2391,72 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
- "<svg width=\"176pt\" height=\"134pt\"\n",
- " viewBox=\"0.00 0.00 176.00 134.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
- "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 130)\">\n",
+ "<svg width=\"176pt\" height=\"131pt\"\n",
+ " viewBox=\"0.00 0.00 176.00 131.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 127)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-130 173,-130 173,5 -4,5\"/>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
"<!-- 4 -->\n",
- "<g id=\"node1\" class=\"node\"><title>4</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-126 0,-126 0,-90 54,-90 54,-126\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-123 0,-123 0,-87 54,-87 54,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"</g>\n",
"<!-- 3 -->\n",
- "<g id=\"node3\" class=\"node\"><title>3</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"73,-36 19,-36 19,-0 73,-0 73,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"46\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"73,-36 19,-36 19,0 73,0 73,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"</g>\n",
"<!-- 4->3 -->\n",
- "<g id=\"edge2\" class=\"edge\"><title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M14.7127,-89.5479C8.92229,-79.0815 4.26329,-65.5953 9.2342,-54 10.7469,-50.4715 12.8093,-47.1304 15.1907,-44.0151\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"18.016,-46.1066 22.0804,-36.3224 12.8016,-41.4365 18.016,-46.1066\"/>\n",
- "<text text-anchor=\"middle\" x=\"17.3829\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M13.9658,-86.8601C8.5525,-77.0267 4.4709,-64.7259 9,-54 10.4817,-50.491 12.4912,-47.1549 14.8124,-44.0309\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"17.6245,-46.1306 21.5364,-36.2844 12.3382,-41.542 17.6245,-46.1306\"/>\n",
+ "<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"</g>\n",
"<!-- 3->4 -->\n",
- "<g id=\"edge4\" class=\"edge\"><title>3->4</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M42.3187,-36.0504C39.6388,-48.4624 35.9542,-65.5279 32.8703,-79.8114\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"29.4432,-79.1006 30.7538,-89.614 36.2855,-80.578 29.4432,-79.1006\"/>\n",
- "<text text-anchor=\"middle\" x=\"46.3829\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M42.0682,-36.0034C39.4963,-47.7801 36.0828,-63.4102 33.1552,-76.8156\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"29.6511,-76.457 30.9368,-86.9735 36.4899,-77.9506 29.6511,-76.457\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"</g>\n",
"<!-- 2 -->\n",
- "<g id=\"node5\" class=\"node\"><title>2</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"149,-126 95,-126 95,-90 149,-90 149,-126\"/>\n",
- "<text text-anchor=\"middle\" x=\"122\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"149,-123 95,-123 95,-87 149,-87 149,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"122\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"</g>\n",
"<!-- 2->3 -->\n",
- "<g id=\"edge6\" class=\"edge\"><title>2->3</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M106.985,-89.614C95.6699,-76.5125 79.9997,-58.3681 67.3773,-43.7526\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"69.9105,-41.331 60.7254,-36.0504 64.6127,-45.9064 69.9105,-41.331\"/>\n",
- "<text text-anchor=\"middle\" x=\"98.3829\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M106.2528,-86.9735C95.3492,-74.4919 80.6716,-57.6899 68.533,-43.7944\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"70.9419,-41.2319 61.7271,-36.0034 65.6701,-45.8371 70.9419,-41.2319\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"</g>\n",
"<!-- 1 -->\n",
- "<g id=\"node8\" class=\"node\"><title>1</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"168,-36 114,-36 114,-0 168,-0 168,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"141\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"168,-36 114,-36 114,0 168,0 168,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"141\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
- "<g id=\"edge8\" class=\"edge\"><title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M120.481,-89.5538C120.042,-79.0894 120.315,-65.6034 123.234,-54 123.951,-51.1501 124.931,-48.2672 126.064,-45.4432\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.318,-46.747 130.352,-36.2028 122.968,-43.8007 129.318,-46.747\"/>\n",
- "<text text-anchor=\"middle\" x=\"131.383\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M120.4276,-86.8094C120.0556,-76.961 120.3724,-64.6623 123,-54 123.7054,-51.1377 124.6671,-48.2411 125.7816,-45.3993\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"129.0662,-46.6305 130.0081,-36.0776 122.6909,-43.7398 129.0662,-46.6305\"/>\n",
+ "<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"</g>\n",
"<!-- 1->2 -->\n",
- "<g id=\"edge10\" class=\"edge\"><title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"firebrick\" d=\"M141.627,-36.427C141.607,-46.8845 140.879,-60.3701 138,-72 137.331,-74.7036 136.455,-77.4548 135.458,-80.1664\"/>\n",
- "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"132.117,-79.0831 131.468,-89.658 138.57,-81.7962 132.117,-79.0831\"/>\n",
- "<text text-anchor=\"middle\" x=\"147.383\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M141.502,-36.171C141.3832,-46.0136 140.5982,-58.3131 138,-69 137.3184,-71.8037 136.4269,-74.6611 135.4132,-77.4782\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"132.1613,-76.1836 131.6235,-86.7648 138.6425,-78.8284 132.1613,-76.1836\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -2456,7 +2465,7 @@
"<Dot visualization: expr_as_graph [(\"rel\",{(1,2),(2,1),(2,3),(3,4),(4,3)})]>"
]
},
- "execution_count": 278,
+ "execution_count": 87,
"metadata": {},
"output_type": "execute_result"
}
@@ -2467,7 +2476,7 @@
},
{
"cell_type": "code",
- "execution_count": 279,
+ "execution_count": 88,
"metadata": {},
"outputs": [
{
@@ -2479,7 +2488,7 @@
"{{2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,54,55,56,57,58,60,62,63,64,65,66,68,69,70,72,74,75,76,77,78,80,81,82,84,85,86,87,88,90,91,92,93,94,95,96,98,99,100},{53},{59},{61},{67},{71},{73},{79},{83},{89},{97}}"
]
},
- "execution_count": 279,
+ "execution_count": 88,
"metadata": {},
"output_type": "execute_result"
}
@@ -2503,7 +2512,7 @@
},
{
"cell_type": "code",
- "execution_count": 280,
+ "execution_count": 89,
"metadata": {},
"outputs": [
{
@@ -2512,7 +2521,7 @@
"Loaded machine: Jupyter_LibraryMeta"
]
},
- "execution_count": 280,
+ "execution_count": 89,
"metadata": {},
"output_type": "execute_result"
}
@@ -2535,19 +2544,19 @@
},
{
"cell_type": "code",
- "execution_count": 281,
+ "execution_count": 90,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\text{\"1.9.0-beta8\"}$"
+ "$\\text{\"1.9.3-nightly\"}$"
],
"text/plain": [
- "\"1.9.0-beta8\""
+ "\"1.9.3-nightly\""
]
},
- "execution_count": 281,
+ "execution_count": 90,
"metadata": {},
"output_type": "execute_result"
}
@@ -2558,19 +2567,19 @@
},
{
"cell_type": "code",
- "execution_count": 282,
+ "execution_count": 91,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\text{\"2a32153ac44523a5f93b0a999f9c42198b9360dc\"}$"
+ "$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
],
"text/plain": [
- "\"2a32153ac44523a5f93b0a999f9c42198b9360dc\""
+ "\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
]
},
- "execution_count": 282,
+ "execution_count": 91,
"metadata": {},
"output_type": "execute_result"
}
@@ -2581,19 +2590,19 @@
},
{
"cell_type": "code",
- "execution_count": 283,
+ "execution_count": 92,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\text{\"Thu Feb 28 13:02:03 2019 +0100\"}$"
+ "$\\text{\"Mon Feb 17 13:18:47 2020 +0100\"}$"
],
"text/plain": [
- "\"Thu Feb 28 13:02:03 2019 +0100\""
+ "\"Mon Feb 17 13:18:47 2020 +0100\""
]
},
- "execution_count": 283,
+ "execution_count": 92,
"metadata": {},
"output_type": "execute_result"
}
@@ -2604,7 +2613,7 @@
},
{
"cell_type": "code",
- "execution_count": 284,
+ "execution_count": 93,
"metadata": {},
"outputs": [
{
@@ -2616,7 +2625,7 @@
"\"1.8.0_202-b08\""
]
},
- "execution_count": 284,
+ "execution_count": 93,
"metadata": {},
"output_type": "execute_result"
}
@@ -2627,19 +2636,19 @@
},
{
"cell_type": "code",
- "execution_count": 285,
+ "execution_count": 94,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\text{\"/usr/bin/java\"}$"
+ "$\\text{\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\"}$"
],
"text/plain": [
- "\"/usr/bin/java\""
+ "\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\""
]
},
- "execution_count": 285,
+ "execution_count": 94,
"metadata": {},
"output_type": "execute_result"
}
@@ -2650,19 +2659,19 @@
},
{
"cell_type": "code",
- "execution_count": 286,
+ "execution_count": 95,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\text{\"5/3/2019 - 13h42 41s\"}$"
+ "$\\text{\"18/2/2020 - 15h12 40s\"}$"
],
"text/plain": [
- "\"5/3/2019 - 13h42 41s\""
+ "\"18/2/2020 - 15h12 40s\""
]
},
- "execution_count": 286,
+ "execution_count": 95,
"metadata": {},
"output_type": "execute_result"
}
@@ -2689,19 +2698,19 @@
},
{
"cell_type": "code",
- "execution_count": 287,
+ "execution_count": 96,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$157096032$"
+ "$151477456$"
],
"text/plain": [
- "157096032"
+ "151477456"
]
},
- "execution_count": 287,
+ "execution_count": 96,
"metadata": {},
"output_type": "execute_result"
}
@@ -2712,7 +2721,7 @@
},
{
"cell_type": "code",
- "execution_count": 288,
+ "execution_count": 97,
"metadata": {},
"outputs": [
{
@@ -2724,7 +2733,7 @@
"1"
]
},
- "execution_count": 288,
+ "execution_count": 97,
"metadata": {},
"output_type": "execute_result"
}
@@ -2735,7 +2744,7 @@
},
{
"cell_type": "code",
- "execution_count": 289,
+ "execution_count": 98,
"metadata": {},
"outputs": [
{
@@ -2747,7 +2756,7 @@
"0"
]
},
- "execution_count": 289,
+ "execution_count": 98,
"metadata": {},
"output_type": "execute_result"
}
@@ -2758,7 +2767,7 @@
},
{
"cell_type": "code",
- "execution_count": 290,
+ "execution_count": 99,
"metadata": {},
"outputs": [
{
@@ -2770,7 +2779,7 @@
"0"
]
},
- "execution_count": 290,
+ "execution_count": 99,
"metadata": {},
"output_type": "execute_result"
}
@@ -2781,7 +2790,7 @@
},
{
"cell_type": "code",
- "execution_count": 291,
+ "execution_count": 100,
"metadata": {},
"outputs": [
{
@@ -2793,7 +2802,7 @@
"−1"
]
},
- "execution_count": 291,
+ "execution_count": 100,
"metadata": {},
"output_type": "execute_result"
}
@@ -2804,19 +2813,19 @@
},
{
"cell_type": "code",
- "execution_count": 292,
+ "execution_count": 101,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$1551789761$"
+ "$1582035160$"
],
"text/plain": [
- "1551789761"
+ "1582035160"
]
},
- "execution_count": 292,
+ "execution_count": 101,
"metadata": {},
"output_type": "execute_result"
}
@@ -2827,19 +2836,19 @@
},
{
"cell_type": "code",
- "execution_count": 293,
+ "execution_count": 102,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$1535$"
+ "$1691$"
],
"text/plain": [
- "1535"
+ "1691"
]
},
- "execution_count": 293,
+ "execution_count": 102,
"metadata": {},
"output_type": "execute_result"
}
@@ -2850,19 +2859,19 @@
},
{
"cell_type": "code",
- "execution_count": 294,
+ "execution_count": 103,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$2519$"
+ "$3040$"
],
"text/plain": [
- "2519"
+ "3040"
]
},
- "execution_count": 294,
+ "execution_count": 103,
"metadata": {},
"output_type": "execute_result"
}
@@ -2899,7 +2908,7 @@
},
{
"cell_type": "code",
- "execution_count": 295,
+ "execution_count": 104,
"metadata": {},
"outputs": [
{
@@ -2911,7 +2920,7 @@
"0"
]
},
- "execution_count": 295,
+ "execution_count": 104,
"metadata": {},
"output_type": "execute_result"
}
@@ -2922,7 +2931,7 @@
},
{
"cell_type": "code",
- "execution_count": 296,
+ "execution_count": 105,
"metadata": {},
"outputs": [
{
@@ -2934,7 +2943,7 @@
"0"
]
},
- "execution_count": 296,
+ "execution_count": 105,
"metadata": {},
"output_type": "execute_result"
}
@@ -2945,7 +2954,7 @@
},
{
"cell_type": "code",
- "execution_count": 297,
+ "execution_count": 106,
"metadata": {},
"outputs": [
{
@@ -2957,7 +2966,7 @@
"0"
]
},
- "execution_count": 297,
+ "execution_count": 106,
"metadata": {},
"output_type": "execute_result"
}
@@ -2968,7 +2977,7 @@
},
{
"cell_type": "code",
- "execution_count": 298,
+ "execution_count": 107,
"metadata": {},
"outputs": [
{
@@ -2980,7 +2989,7 @@
"0"
]
},
- "execution_count": 298,
+ "execution_count": 107,
"metadata": {},
"output_type": "execute_result"
}
@@ -2991,7 +3000,7 @@
},
{
"cell_type": "code",
- "execution_count": 299,
+ "execution_count": 108,
"metadata": {},
"outputs": [
{
@@ -3003,7 +3012,7 @@
"0"
]
},
- "execution_count": 299,
+ "execution_count": 108,
"metadata": {},
"output_type": "execute_result"
}
@@ -3014,7 +3023,7 @@
},
{
"cell_type": "code",
- "execution_count": 300,
+ "execution_count": 109,
"metadata": {},
"outputs": [
{
@@ -3026,7 +3035,7 @@
"0"
]
},
- "execution_count": 300,
+ "execution_count": 109,
"metadata": {},
"output_type": "execute_result"
}
@@ -3037,7 +3046,7 @@
},
{
"cell_type": "code",
- "execution_count": 301,
+ "execution_count": 110,
"metadata": {},
"outputs": [
{
@@ -3049,7 +3058,7 @@
"0"
]
},
- "execution_count": 301,
+ "execution_count": 110,
"metadata": {},
"output_type": "execute_result"
}
@@ -3069,7 +3078,7 @@
},
{
"cell_type": "code",
- "execution_count": 302,
+ "execution_count": 111,
"metadata": {},
"outputs": [
{
@@ -3081,7 +3090,7 @@
"{\"(machine from Jupyter cell).mch\",\"LibraryMeta.def\"}"
]
},
- "execution_count": 302,
+ "execution_count": 111,
"metadata": {},
"output_type": "execute_result"
}
@@ -3092,7 +3101,7 @@
},
{
"cell_type": "code",
- "execution_count": 303,
+ "execution_count": 112,
"metadata": {},
"outputs": [
{
@@ -3104,7 +3113,7 @@
"{\"(machine from Jupyter cell).mch\"}"
]
},
- "execution_count": 303,
+ "execution_count": 112,
"metadata": {},
"output_type": "execute_result"
}
@@ -3115,7 +3124,7 @@
},
{
"cell_type": "code",
- "execution_count": 304,
+ "execution_count": 113,
"metadata": {},
"outputs": [
{
@@ -3127,7 +3136,7 @@
"∅"
]
},
- "execution_count": 304,
+ "execution_count": 113,
"metadata": {},
"output_type": "execute_result"
}
@@ -3138,7 +3147,7 @@
},
{
"cell_type": "code",
- "execution_count": 305,
+ "execution_count": 114,
"metadata": {},
"outputs": [
{
@@ -3150,7 +3159,7 @@
"∅"
]
},
- "execution_count": 305,
+ "execution_count": 114,
"metadata": {},
"output_type": "execute_result"
}
@@ -3161,7 +3170,7 @@
},
{
"cell_type": "code",
- "execution_count": 306,
+ "execution_count": 115,
"metadata": {},
"outputs": [
{
@@ -3173,7 +3182,7 @@
"∅"
]
},
- "execution_count": 306,
+ "execution_count": 115,
"metadata": {},
"output_type": "execute_result"
}
@@ -3184,7 +3193,7 @@
},
{
"cell_type": "code",
- "execution_count": 307,
+ "execution_count": 116,
"metadata": {},
"outputs": [
{
@@ -3196,7 +3205,7 @@
"∅"
]
},
- "execution_count": 307,
+ "execution_count": 116,
"metadata": {},
"output_type": "execute_result"
}
@@ -3207,7 +3216,7 @@
},
{
"cell_type": "code",
- "execution_count": 308,
+ "execution_count": 117,
"metadata": {},
"outputs": [
{
@@ -3219,7 +3228,7 @@
"∅"
]
},
- "execution_count": 308,
+ "execution_count": 117,
"metadata": {},
"output_type": "execute_result"
}
@@ -3230,7 +3239,7 @@
},
{
"cell_type": "code",
- "execution_count": 309,
+ "execution_count": 118,
"metadata": {},
"outputs": [
{
@@ -3242,7 +3251,7 @@
"∅"
]
},
- "execution_count": 309,
+ "execution_count": 118,
"metadata": {},
"output_type": "execute_result"
}
@@ -3253,19 +3262,19 @@
},
{
"cell_type": "code",
- "execution_count": 310,
+ "execution_count": 119,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\{\\text{\"5d45f08d7e5cf22716b8fd3dd54a29b4ba4c443c\"}\\}$"
+ "$\\{\\text{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}\\}$"
],
"text/plain": [
- "{\"5d45f08d7e5cf22716b8fd3dd54a29b4ba4c443c\"}"
+ "{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}"
]
},
- "execution_count": 310,
+ "execution_count": 119,
"metadata": {},
"output_type": "execute_result"
}
@@ -3285,21 +3294,18 @@
},
{
"cell_type": "code",
- "execution_count": 311,
+ "execution_count": 120,
"metadata": {},
"outputs": [
{
- "data": {
- "text/markdown": [
- "$\\text{\"abstract_machine\"}$"
- ],
- "text/plain": [
- "\"abstract_machine\""
- ]
- },
- "execution_count": 311,
- "metadata": {},
- "output_type": "execute_result"
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: ProB returned error messages:\nError: [1,1] expecting: 'generated', 'package', 'DEFINITIONS', 'IMPLEMENTATION', 'MACHINE', 'MODEL', 'SYSTEM', 'REFINEMENT', '#EXPRESSION', '#PREDICATE', '#FORMULA', '#SUBSTITUTION', '#DEFINITION', '#OPPATTERN', '#MACHINECLAUSE' ((machine from Jupyter cell):1:1)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mnull\u001b[0m",
+ "\u001b[1m\u001b[31mError: [1,1] expecting: 'generated', 'package', 'DEFINITIONS', 'IMPLEMENTATION', 'MACHINE', 'MODEL', 'SYSTEM', 'REFINEMENT', '#EXPRESSION', '#PREDICATE', '#FORMULA', '#SUBSTITUTION', '#DEFINITION', '#OPPATTERN', '#MACHINECLAUSE' ((machine from Jupyter cell):1:1)\u001b[0m",
+ "\u001b[1m\u001b[30mM\u001b[0m\u001b[1m\u001b[30m\u001b[41m\u001b[0m\u001b[1m\u001b[30mACHINE_INFO(\"Jupyter_LibraryMeta\",\"TYPE\")\u001b[0m"
+ ]
}
],
"source": [
@@ -3358,7 +3364,7 @@
},
{
"cell_type": "code",
- "execution_count": 312,
+ "execution_count": 121,
"metadata": {},
"outputs": [
{
@@ -3367,7 +3373,7 @@
"Loaded machine: Jupyter_LibraryXML"
]
},
- "execution_count": 312,
+ "execution_count": 121,
"metadata": {},
"output_type": "execute_result"
}
@@ -3390,7 +3396,7 @@
},
{
"cell_type": "code",
- "execution_count": 313,
+ "execution_count": 122,
"metadata": {},
"outputs": [
{
@@ -3402,7 +3408,7 @@
"{(1↦rec(attributes∈{(\"version\"↦\"0.1\")},element∈\"Data\",meta∈{(\"xmlLineNumber\"↦\"3\")},pId∈0,recId∈1)),(2↦rec(attributes∈{(\"attr1\"↦\"value1\"),(\"elemID\"↦\"ID1\")},element∈\"Tag1\",meta∈{(\"xmlLineNumber\"↦\"4\")},pId∈1,recId∈2))}"
]
},
- "execution_count": 313,
+ "execution_count": 122,
"metadata": {},
"output_type": "execute_result"
}
@@ -3448,7 +3454,7 @@
},
{
"cell_type": "code",
- "execution_count": 314,
+ "execution_count": 123,
"metadata": {},
"outputs": [
{
@@ -3457,7 +3463,7 @@
"Loaded machine: Jupyter_LibraryHash"
]
},
- "execution_count": 314,
+ "execution_count": 123,
"metadata": {},
"output_type": "execute_result"
}
@@ -3482,7 +3488,7 @@
},
{
"cell_type": "code",
- "execution_count": 315,
+ "execution_count": 124,
"metadata": {},
"outputs": [
{
@@ -3494,7 +3500,7 @@
"92915201"
]
},
- "execution_count": 315,
+ "execution_count": 124,
"metadata": {},
"output_type": "execute_result"
}
@@ -3505,7 +3511,7 @@
},
{
"cell_type": "code",
- "execution_count": 316,
+ "execution_count": 125,
"metadata": {},
"outputs": [
{
@@ -3517,7 +3523,7 @@
"191034877"
]
},
- "execution_count": 316,
+ "execution_count": 125,
"metadata": {},
"output_type": "execute_result"
}
@@ -3528,7 +3534,7 @@
},
{
"cell_type": "code",
- "execution_count": 317,
+ "execution_count": 126,
"metadata": {},
"outputs": [
{
@@ -3540,7 +3546,7 @@
"FALSE"
]
},
- "execution_count": 317,
+ "execution_count": 126,
"metadata": {},
"output_type": "execute_result"
}
@@ -3562,19 +3568,19 @@
},
{
"cell_type": "code",
- "execution_count": 318,
+ "execution_count": 127,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[37,168,75,91,175,1,8,58,13,207,7,42,222,208,212,29,243,31,27,154]$"
+ "$\\{(1\\mapsto 37),(2\\mapsto 168),(3\\mapsto 75),(4\\mapsto 91),(5\\mapsto 175),(6\\mapsto 1),(7\\mapsto 8),(8\\mapsto 58),(9\\mapsto 13),(10\\mapsto 207),(11\\mapsto 7),(12\\mapsto 42),(13\\mapsto 222),(14\\mapsto 208),(15\\mapsto 212),(16\\mapsto 29),(17\\mapsto 243),(18\\mapsto 31),(19\\mapsto 27),(20\\mapsto 154)\\}$"
],
"text/plain": [
- "[37,168,75,91,175,1,8,58,13,207,7,42,222,208,212,29,243,31,27,154]"
+ "{(1↦37),(2↦168),(3↦75),(4↦91),(5↦175),(6↦1),(7↦8),(8↦58),(9↦13),(10↦207),(11↦7),(12↦42),(13↦222),(14↦208),(15↦212),(16↦29),(17↦243),(18↦31),(19↦27),(20↦154)}"
]
},
- "execution_count": 318,
+ "execution_count": 127,
"metadata": {},
"output_type": "execute_result"
}
@@ -3585,19 +3591,19 @@
},
{
"cell_type": "code",
- "execution_count": 319,
+ "execution_count": 128,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[149,81,45,24,177,25,74,30,204,7,143,202,136,116,148,247,6,221,245,52]$"
+ "$\\{(1\\mapsto 149),(2\\mapsto 81),(3\\mapsto 45),(4\\mapsto 24),(5\\mapsto 177),(6\\mapsto 25),(7\\mapsto 74),(8\\mapsto 30),(9\\mapsto 204),(10\\mapsto 7),(11\\mapsto 143),(12\\mapsto 202),(13\\mapsto 136),(14\\mapsto 116),(15\\mapsto 148),(16\\mapsto 247),(17\\mapsto 6),(18\\mapsto 221),(19\\mapsto 245),(20\\mapsto 52)\\}$"
],
"text/plain": [
- "[149,81,45,24,177,25,74,30,204,7,143,202,136,116,148,247,6,221,245,52]"
+ "{(1↦149),(2↦81),(3↦45),(4↦24),(5↦177),(6↦25),(7↦74),(8↦30),(9↦204),(10↦7),(11↦143),(12↦202),(13↦136),(14↦116),(15↦148),(16↦247),(17↦6),(18↦221),(19↦245),(20↦52)}"
]
},
- "execution_count": 319,
+ "execution_count": 128,
"metadata": {},
"output_type": "execute_result"
}
@@ -3608,7 +3614,7 @@
},
{
"cell_type": "code",
- "execution_count": 320,
+ "execution_count": 129,
"metadata": {},
"outputs": [
{
@@ -3620,7 +3626,7 @@
"FALSE"
]
},
- "execution_count": 320,
+ "execution_count": 129,
"metadata": {},
"output_type": "execute_result"
}
@@ -3642,7 +3648,7 @@
},
{
"cell_type": "code",
- "execution_count": 321,
+ "execution_count": 130,
"metadata": {},
"outputs": [
{
@@ -3654,7 +3660,7 @@
"\"25a84b5baf01083a0dcf072aded0d41df31f1b9a\""
]
},
- "execution_count": 321,
+ "execution_count": 130,
"metadata": {},
"output_type": "execute_result"
}
@@ -3665,7 +3671,7 @@
},
{
"cell_type": "code",
- "execution_count": 322,
+ "execution_count": 131,
"metadata": {},
"outputs": [
{
@@ -3677,7 +3683,7 @@
"\"95512d18b1194a1ecc078fca887494f706ddf534\""
]
},
- "execution_count": 322,
+ "execution_count": 131,
"metadata": {},
"output_type": "execute_result"
}
@@ -3688,7 +3694,7 @@
},
{
"cell_type": "code",
- "execution_count": 323,
+ "execution_count": 132,
"metadata": {},
"outputs": [
{
@@ -3700,7 +3706,7 @@
"\"6bd1d8beefa14ea131285d11bbf8580c5f31fe78\""
]
},
- "execution_count": 323,
+ "execution_count": 132,
"metadata": {},
"output_type": "execute_result"
}
@@ -3711,7 +3717,7 @@
},
{
"cell_type": "code",
- "execution_count": 324,
+ "execution_count": 133,
"metadata": {},
"outputs": [
{
@@ -3723,7 +3729,7 @@
"\"068948b4d423a0db5fd1574edad799005fc456e0\""
]
},
- "execution_count": 324,
+ "execution_count": 133,
"metadata": {},
"output_type": "execute_result"
}
@@ -3734,7 +3740,7 @@
},
{
"cell_type": "code",
- "execution_count": 325,
+ "execution_count": 134,
"metadata": {},
"outputs": [
{
@@ -3746,7 +3752,7 @@
"\"55b9c89f79362578c3641774db978b5455be5bfd\""
]
},
- "execution_count": 325,
+ "execution_count": 134,
"metadata": {},
"output_type": "execute_result"
}
@@ -3771,7 +3777,7 @@
},
{
"cell_type": "code",
- "execution_count": 326,
+ "execution_count": 135,
"metadata": {},
"outputs": [
{
@@ -3780,7 +3786,7 @@
"Loaded machine: Jupyter_LibraryRegex"
]
},
- "execution_count": 326,
+ "execution_count": 135,
"metadata": {},
"output_type": "execute_result"
}
@@ -3965,7 +3971,7 @@
},
{
"cell_type": "code",
- "execution_count": 327,
+ "execution_count": 136,
"metadata": {},
"outputs": [
{
@@ -3977,7 +3983,7 @@
"TRUE"
]
},
- "execution_count": 327,
+ "execution_count": 136,
"metadata": {},
"output_type": "execute_result"
}
@@ -3988,7 +3994,7 @@
},
{
"cell_type": "code",
- "execution_count": 328,
+ "execution_count": 137,
"metadata": {},
"outputs": [
{
@@ -4000,7 +4006,7 @@
"FALSE"
]
},
- "execution_count": 328,
+ "execution_count": 137,
"metadata": {},
"output_type": "execute_result"
}
@@ -4018,7 +4024,7 @@
},
{
"cell_type": "code",
- "execution_count": 329,
+ "execution_count": 138,
"metadata": {},
"outputs": [
{
@@ -4030,7 +4036,7 @@
"TRUE"
]
},
- "execution_count": 329,
+ "execution_count": 138,
"metadata": {},
"output_type": "execute_result"
}
@@ -4041,7 +4047,7 @@
},
{
"cell_type": "code",
- "execution_count": 330,
+ "execution_count": 139,
"metadata": {},
"outputs": [
{
@@ -4053,7 +4059,7 @@
"FALSE"
]
},
- "execution_count": 330,
+ "execution_count": 139,
"metadata": {},
"output_type": "execute_result"
}
@@ -4072,7 +4078,7 @@
},
{
"cell_type": "code",
- "execution_count": 331,
+ "execution_count": 140,
"metadata": {},
"outputs": [
{
@@ -4090,7 +4096,7 @@
"\tstr = \"1.9\""
]
},
- "execution_count": 331,
+ "execution_count": 140,
"metadata": {},
"output_type": "execute_result"
}
@@ -4110,7 +4116,7 @@
},
{
"cell_type": "code",
- "execution_count": 332,
+ "execution_count": 141,
"metadata": {},
"outputs": [
{
@@ -4122,7 +4128,7 @@
"TRUE"
]
},
- "execution_count": 332,
+ "execution_count": 141,
"metadata": {},
"output_type": "execute_result"
}
@@ -4133,7 +4139,7 @@
},
{
"cell_type": "code",
- "execution_count": 333,
+ "execution_count": 142,
"metadata": {},
"outputs": [
{
@@ -4145,7 +4151,7 @@
"FALSE"
]
},
- "execution_count": 333,
+ "execution_count": 142,
"metadata": {},
"output_type": "execute_result"
}
@@ -4167,7 +4173,7 @@
},
{
"cell_type": "code",
- "execution_count": 334,
+ "execution_count": 143,
"metadata": {},
"outputs": [
{
@@ -4179,7 +4185,7 @@
"\"aNUMbNUMcNUMdNUM\""
]
},
- "execution_count": 334,
+ "execution_count": 143,
"metadata": {},
"output_type": "execute_result"
}
@@ -4190,7 +4196,7 @@
},
{
"cell_type": "code",
- "execution_count": 335,
+ "execution_count": 144,
"metadata": {},
"outputs": [
{
@@ -4202,7 +4208,7 @@
"\"X01X23X4X56\""
]
},
- "execution_count": 335,
+ "execution_count": 144,
"metadata": {},
"output_type": "execute_result"
}
@@ -4220,7 +4226,7 @@
},
{
"cell_type": "code",
- "execution_count": 336,
+ "execution_count": 145,
"metadata": {},
"outputs": [
{
@@ -4232,7 +4238,7 @@
"\"1<<abcabd>>2\""
]
},
- "execution_count": 336,
+ "execution_count": 145,
"metadata": {},
"output_type": "execute_result"
}
@@ -4250,7 +4256,7 @@
},
{
"cell_type": "code",
- "execution_count": 337,
+ "execution_count": 146,
"metadata": {},
"outputs": [
{
@@ -4262,7 +4268,7 @@
"\"ab(12)cd(34)\""
]
},
- "execution_count": 337,
+ "execution_count": 146,
"metadata": {},
"output_type": "execute_result"
}
@@ -4283,7 +4289,7 @@
},
{
"cell_type": "code",
- "execution_count": 338,
+ "execution_count": 147,
"metadata": {},
"outputs": [
{
@@ -4295,7 +4301,7 @@
"\"234\""
]
},
- "execution_count": 338,
+ "execution_count": 147,
"metadata": {},
"output_type": "execute_result"
}
@@ -4306,7 +4312,7 @@
},
{
"cell_type": "code",
- "execution_count": 339,
+ "execution_count": 148,
"metadata": {},
"outputs": [
{
@@ -4318,7 +4324,7 @@
"\"abcdef\""
]
},
- "execution_count": 339,
+ "execution_count": 148,
"metadata": {},
"output_type": "execute_result"
}
@@ -4336,7 +4342,7 @@
},
{
"cell_type": "code",
- "execution_count": 340,
+ "execution_count": 149,
"metadata": {},
"outputs": [
{
@@ -4348,7 +4354,7 @@
"\"daf\""
]
},
- "execution_count": 340,
+ "execution_count": 149,
"metadata": {},
"output_type": "execute_result"
}
@@ -4366,7 +4372,7 @@
},
{
"cell_type": "code",
- "execution_count": 341,
+ "execution_count": 150,
"metadata": {},
"outputs": [
{
@@ -4378,7 +4384,7 @@
"\"\""
]
},
- "execution_count": 341,
+ "execution_count": 150,
"metadata": {},
"output_type": "execute_result"
}
@@ -4400,7 +4406,7 @@
},
{
"cell_type": "code",
- "execution_count": 342,
+ "execution_count": 151,
"metadata": {},
"outputs": [
{
@@ -4412,7 +4418,7 @@
"rec(length∈6,position∈1,string∈\"abcdef\",submatches∈∅)"
]
},
- "execution_count": 342,
+ "execution_count": 151,
"metadata": {},
"output_type": "execute_result"
}
@@ -4423,7 +4429,7 @@
},
{
"cell_type": "code",
- "execution_count": 343,
+ "execution_count": 152,
"metadata": {},
"outputs": [
{
@@ -4435,7 +4441,7 @@
"rec(length∈3,position∈13,string∈\"daf\",submatches∈∅)"
]
},
- "execution_count": 343,
+ "execution_count": 152,
"metadata": {},
"output_type": "execute_result"
}
@@ -4446,7 +4452,7 @@
},
{
"cell_type": "code",
- "execution_count": 344,
+ "execution_count": 153,
"metadata": {},
"outputs": [
{
@@ -4458,7 +4464,7 @@
"rec(length∈3,position∈10,string∈\"234\",submatches∈{(1↦\"2\"),(2↦\"34\")})"
]
},
- "execution_count": 344,
+ "execution_count": 153,
"metadata": {},
"output_type": "execute_result"
}
@@ -4476,7 +4482,7 @@
},
{
"cell_type": "code",
- "execution_count": 345,
+ "execution_count": 154,
"metadata": {},
"outputs": [
{
@@ -4488,7 +4494,7 @@
"rec(length∈−1,position∈−1,string∈\"\",submatches∈∅)"
]
},
- "execution_count": 345,
+ "execution_count": 154,
"metadata": {},
"output_type": "execute_result"
}
@@ -4510,7 +4516,7 @@
},
{
"cell_type": "code",
- "execution_count": 346,
+ "execution_count": 155,
"metadata": {},
"outputs": [
{
@@ -4522,7 +4528,7 @@
"{(1↦\"234\"),(2↦\"567\")}"
]
},
- "execution_count": 346,
+ "execution_count": 155,
"metadata": {},
"output_type": "execute_result"
}
@@ -4533,19 +4539,19 @@
},
{
"cell_type": "code",
- "execution_count": 347,
+ "execution_count": 156,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"0\"},\\text{\"0\"},\\text{\"0\"},\\text{\"2\"},\\text{\"3\"},\\text{\"4\"},\\text{\"5\"},\\text{\"6\"},\\text{\"7\"}]$"
+ "$\\{(1\\mapsto\\text{\"0\"}),(2\\mapsto\\text{\"0\"}),(3\\mapsto\\text{\"0\"}),(4\\mapsto\\text{\"2\"}),(5\\mapsto\\text{\"3\"}),(6\\mapsto\\text{\"4\"}),(7\\mapsto\\text{\"5\"}),(8\\mapsto\\text{\"6\"}),(9\\mapsto\\text{\"7\"})\\}$"
],
"text/plain": [
- "[\"0\",\"0\",\"0\",\"2\",\"3\",\"4\",\"5\",\"6\",\"7\"]"
+ "{(1↦\"0\"),(2↦\"0\"),(3↦\"0\"),(4↦\"2\"),(5↦\"3\"),(6↦\"4\"),(7↦\"5\"),(8↦\"6\"),(9↦\"7\")}"
]
},
- "execution_count": 347,
+ "execution_count": 156,
"metadata": {},
"output_type": "execute_result"
}
@@ -4563,7 +4569,7 @@
},
{
"cell_type": "code",
- "execution_count": 348,
+ "execution_count": 157,
"metadata": {},
"outputs": [
{
@@ -4575,7 +4581,7 @@
"∅"
]
},
- "execution_count": 348,
+ "execution_count": 157,
"metadata": {},
"output_type": "execute_result"
}
@@ -4595,19 +4601,19 @@
},
{
"cell_type": "code",
- "execution_count": 349,
+ "execution_count": 158,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"a\"},\\text{\"b\"},\\text{\"c\"},\\text{\"ä\"},\\text{\"é\"},\\text{\"à\"}]$"
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"}),(4\\mapsto\\text{\"ä\"}),(5\\mapsto\\text{\"é\"}),(6\\mapsto\\text{\"à\"})\\}$"
],
"text/plain": [
- "[\"a\",\"b\",\"c\",\"ä\",\"é\",\"à\"]"
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\"),(4↦\"ä\"),(5↦\"é\"),(6↦\"à\")}"
]
},
- "execution_count": 349,
+ "execution_count": 158,
"metadata": {},
"output_type": "execute_result"
}
@@ -4618,7 +4624,7 @@
},
{
"cell_type": "code",
- "execution_count": 350,
+ "execution_count": 159,
"metadata": {},
"outputs": [
{
@@ -4630,7 +4636,7 @@
"\"äéà\""
]
},
- "execution_count": 350,
+ "execution_count": 159,
"metadata": {},
"output_type": "execute_result"
}
@@ -4641,7 +4647,7 @@
},
{
"cell_type": "code",
- "execution_count": 351,
+ "execution_count": 160,
"metadata": {},
"outputs": [
{
@@ -4653,7 +4659,7 @@
"rec(length∈3,position∈5,string∈\"äéà\",submatches∈∅)"
]
},
- "execution_count": 351,
+ "execution_count": 160,
"metadata": {},
"output_type": "execute_result"
}
@@ -4664,7 +4670,7 @@
},
{
"cell_type": "code",
- "execution_count": 352,
+ "execution_count": 161,
"metadata": {},
"outputs": [
{
@@ -4676,7 +4682,7 @@
"\"abc- ça -123\""
]
},
- "execution_count": 352,
+ "execution_count": 161,
"metadata": {},
"output_type": "execute_result"
}
@@ -4687,7 +4693,7 @@
},
{
"cell_type": "code",
- "execution_count": 353,
+ "execution_count": 162,
"metadata": {},
"outputs": [
{
@@ -4699,7 +4705,7 @@
"TRUE"
]
},
- "execution_count": 353,
+ "execution_count": 162,
"metadata": {},
"output_type": "execute_result"
}
@@ -4710,7 +4716,7 @@
},
{
"cell_type": "code",
- "execution_count": 354,
+ "execution_count": 163,
"metadata": {},
"outputs": [
{
@@ -4722,7 +4728,7 @@
"FALSE"
]
},
- "execution_count": 354,
+ "execution_count": 163,
"metadata": {},
"output_type": "execute_result"
}
@@ -4733,7 +4739,7 @@
},
{
"cell_type": "code",
- "execution_count": 355,
+ "execution_count": 164,
"metadata": {},
"outputs": [
{
@@ -4745,7 +4751,7 @@
"TRUE"
]
},
- "execution_count": 355,
+ "execution_count": 164,
"metadata": {},
"output_type": "execute_result"
}
@@ -4772,19 +4778,19 @@
},
{
"cell_type": "code",
- "execution_count": 356,
+ "execution_count": 165,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"The\"},\\text{\"quick\"},\\text{\"fox\"}]$"
+ "$\\{(1\\mapsto\\text{\"The\"}),(2\\mapsto\\text{\"quick\"}),(3\\mapsto\\text{\"fox\"})\\}$"
],
"text/plain": [
- "[\"The\",\"quick\",\"fox\"]"
+ "{(1↦\"The\"),(2↦\"quick\"),(3↦\"fox\")}"
]
},
- "execution_count": 356,
+ "execution_count": 165,
"metadata": {},
"output_type": "execute_result"
}
@@ -4802,19 +4808,19 @@
},
{
"cell_type": "code",
- "execution_count": 357,
+ "execution_count": 166,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in [\\text{\"192\"},\\text{\"69\"},\\text{\"2\"},\\text{\"1\"}])$"
+ "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\})$"
],
"text/plain": [
- "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈[\"192\",\"69\",\"2\",\"1\"])"
+ "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")})"
]
},
- "execution_count": 357,
+ "execution_count": 166,
"metadata": {},
"output_type": "execute_result"
}
@@ -4832,19 +4838,19 @@
},
{
"cell_type": "code",
- "execution_count": 358,
+ "execution_count": 167,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in [\\text{\"192\"},\\text{\"69\"},\\text{\"2\"},\\text{\"1\"}])$"
+ "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\})$"
],
"text/plain": [
- "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈[\"192\",\"69\",\"2\",\"1\"])"
+ "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")})"
]
},
- "execution_count": 358,
+ "execution_count": 167,
"metadata": {},
"output_type": "execute_result"
}
@@ -4862,19 +4868,19 @@
},
{
"cell_type": "code",
- "execution_count": 359,
+ "execution_count": 168,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"192\"},\\text{\"69\"},\\text{\"2\"},\\text{\"1\"}]$"
+ "$\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\}$"
],
"text/plain": [
- "[\"192\",\"69\",\"2\",\"1\"]"
+ "{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")}"
]
},
- "execution_count": 359,
+ "execution_count": 168,
"metadata": {},
"output_type": "execute_result"
}
@@ -4892,7 +4898,7 @@
},
{
"cell_type": "code",
- "execution_count": 360,
+ "execution_count": 169,
"metadata": {},
"outputs": [
{
@@ -4904,7 +4910,7 @@
"{(1↦\"102\"),(2↦\"34\")}"
]
},
- "execution_count": 360,
+ "execution_count": 169,
"metadata": {},
"output_type": "execute_result"
}
@@ -4922,19 +4928,19 @@
},
{
"cell_type": "code",
- "execution_count": 361,
+ "execution_count": 170,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\"weight\"},\\text{\"is\"},\\text{\"50\"},\\text{\"and\"},\\text{\"height\"},\\text{\"is\"},\\text{\"100\"}]$"
+ "$\\{(1\\mapsto\\text{\"weight\"}),(2\\mapsto\\text{\"is\"}),(3\\mapsto\\text{\"50\"}),(4\\mapsto\\text{\"and\"}),(5\\mapsto\\text{\"height\"}),(6\\mapsto\\text{\"is\"}),(7\\mapsto\\text{\"100\"})\\}$"
],
"text/plain": [
- "[\"weight\",\"is\",\"50\",\"and\",\"height\",\"is\",\"100\"]"
+ "{(1↦\"weight\"),(2↦\"is\"),(3↦\"50\"),(4↦\"and\"),(5↦\"height\"),(6↦\"is\"),(7↦\"100\")}"
]
},
- "execution_count": 361,
+ "execution_count": 170,
"metadata": {},
"output_type": "execute_result"
}
@@ -4945,19 +4951,19 @@
},
{
"cell_type": "code",
- "execution_count": 362,
+ "execution_count": 171,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
- "$[\\text{\" is\"},\\text{\" 50\"},\\text{\" and\"},\\text{\" height\"},\\text{\" is\"},\\text{\" 100\"}]$"
+ "$\\{(1\\mapsto\\text{\" is\"}),(2\\mapsto\\text{\" 50\"}),(3\\mapsto\\text{\" and\"}),(4\\mapsto\\text{\" height\"}),(5\\mapsto\\text{\" is\"}),(6\\mapsto\\text{\" 100\"})\\}$"
],
"text/plain": [
- "[\" is\",\" 50\",\" and\",\" height\",\" is\",\" 100\"]"
+ "{(1↦\" is\"),(2↦\" 50\"),(3↦\" and\"),(4↦\" height\"),(5↦\" is\"),(6↦\" 100\")}"
]
},
- "execution_count": 362,
+ "execution_count": 171,
"metadata": {},
"output_type": "execute_result"
}
@@ -4977,7 +4983,7 @@
},
{
"cell_type": "code",
- "execution_count": 363,
+ "execution_count": 172,
"metadata": {},
"outputs": [
{
@@ -4989,7 +4995,7 @@
"\"hi\""
]
},
- "execution_count": 363,
+ "execution_count": 172,
"metadata": {},
"output_type": "execute_result"
}
@@ -5000,7 +5006,7 @@
},
{
"cell_type": "code",
- "execution_count": 364,
+ "execution_count": 173,
"metadata": {},
"outputs": [
{
@@ -5012,7 +5018,7 @@
"\"hi\""
]
},
- "execution_count": 364,
+ "execution_count": 173,
"metadata": {},
"output_type": "execute_result"
}
@@ -5030,17 +5036,17 @@
},
{
"cell_type": "code",
- "execution_count": 365,
+ "execution_count": 174,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":eval: NOT-WELL-DEFINED: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/leuschel/git_root/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 28, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
+ "evalue": ":eval: NOT-WELL-DEFINED: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 28, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
"\u001b[1m\u001b[31m### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\u001b[0m",
- "\u001b[1m\u001b[31m ### File: /Users/leuschel/git_root/prob_prolog/stdlib/LibraryRegex.def\u001b[0m",
+ "\u001b[1m\u001b[31m ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\u001b[0m",
"\u001b[1m\u001b[31m ### Line: 28, Column: 1 until 88\u001b[0m",
"\u001b[1m\u001b[31m ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\u001b[0m"
]
@@ -5059,7 +5065,7 @@
},
{
"cell_type": "code",
- "execution_count": 366,
+ "execution_count": 175,
"metadata": {},
"outputs": [
{
@@ -5071,7 +5077,7 @@
"\"dede\""
]
},
- "execution_count": 366,
+ "execution_count": 175,
"metadata": {},
"output_type": "execute_result"
}
@@ -5109,7 +5115,7 @@
},
{
"cell_type": "code",
- "execution_count": 367,
+ "execution_count": 176,
"metadata": {},
"outputs": [
{
@@ -5121,7 +5127,7 @@
"1"
]
},
- "execution_count": 367,
+ "execution_count": 176,
"metadata": {},
"output_type": "execute_result"
}
@@ -5132,7 +5138,7 @@
},
{
"cell_type": "code",
- "execution_count": 368,
+ "execution_count": 177,
"metadata": {},
"outputs": [
{
@@ -5144,7 +5150,7 @@
"2"
]
},
- "execution_count": 368,
+ "execution_count": 177,
"metadata": {},
"output_type": "execute_result"
}
@@ -5155,7 +5161,7 @@
},
{
"cell_type": "code",
- "execution_count": 369,
+ "execution_count": 178,
"metadata": {},
"outputs": [
{
@@ -5167,7 +5173,7 @@
"2"
]
},
- "execution_count": 369,
+ "execution_count": 178,
"metadata": {},
"output_type": "execute_result"
}
@@ -5178,7 +5184,7 @@
},
{
"cell_type": "code",
- "execution_count": 370,
+ "execution_count": 179,
"metadata": {},
"outputs": [
{
@@ -5190,7 +5196,7 @@
"2"
]
},
- "execution_count": 370,
+ "execution_count": 179,
"metadata": {},
"output_type": "execute_result"
}
@@ -5201,7 +5207,7 @@
},
{
"cell_type": "code",
- "execution_count": 371,
+ "execution_count": 180,
"metadata": {},
"outputs": [
{
@@ -5213,7 +5219,7 @@
"TRUE"
]
},
- "execution_count": 371,
+ "execution_count": 180,
"metadata": {},
"output_type": "execute_result"
}
@@ -5224,7 +5230,7 @@
},
{
"cell_type": "code",
- "execution_count": 372,
+ "execution_count": 181,
"metadata": {},
"outputs": [
{
@@ -5236,7 +5242,7 @@
"FALSE"
]
},
- "execution_count": 372,
+ "execution_count": 181,
"metadata": {},
"output_type": "execute_result"
}
@@ -5247,7 +5253,7 @@
},
{
"cell_type": "code",
- "execution_count": 373,
+ "execution_count": 182,
"metadata": {},
"outputs": [
{
@@ -5259,7 +5265,7 @@
"\"\\\\\\\"\""
]
},
- "execution_count": 373,
+ "execution_count": 182,
"metadata": {},
"output_type": "execute_result"
}
@@ -5277,16 +5283,21 @@
},
{
"cell_type": "code",
- "execution_count": 384,
+ "execution_count": 183,
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: Computation not completed: Unknown identifier \"STRING_CHARS\"",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"STRING_CHARS\"\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"\\\\\"}),(2\\mapsto\\text{\"\\\"\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"\\\\\"),(2↦\"\\\"\")}"
+ ]
+ },
+ "execution_count": 183,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
@@ -5295,7 +5306,7 @@
},
{
"cell_type": "code",
- "execution_count": 374,
+ "execution_count": 184,
"metadata": {},
"outputs": [
{
@@ -5307,7 +5318,7 @@
"\"\\a\""
]
},
- "execution_count": 374,
+ "execution_count": 184,
"metadata": {},
"output_type": "execute_result"
}
@@ -5318,7 +5329,7 @@
},
{
"cell_type": "code",
- "execution_count": 375,
+ "execution_count": 185,
"metadata": {},
"outputs": [
{
@@ -5330,7 +5341,7 @@
"\"\\\\\""
]
},
- "execution_count": 375,
+ "execution_count": 185,
"metadata": {},
"output_type": "execute_result"
}
@@ -5341,7 +5352,7 @@
},
{
"cell_type": "code",
- "execution_count": 376,
+ "execution_count": 186,
"metadata": {},
"outputs": [
{
@@ -5353,7 +5364,7 @@
"\"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)\""
]
},
- "execution_count": 376,
+ "execution_count": 186,
"metadata": {},
"output_type": "execute_result"
}
@@ -5364,7 +5375,7 @@
},
{
"cell_type": "code",
- "execution_count": 377,
+ "execution_count": 187,
"metadata": {},
"outputs": [
{
@@ -5376,7 +5387,7 @@
"\"\\b\""
]
},
- "execution_count": 377,
+ "execution_count": 187,
"metadata": {},
"output_type": "execute_result"
}
@@ -5401,7 +5412,7 @@
},
{
"cell_type": "code",
- "execution_count": 387,
+ "execution_count": 188,
"metadata": {},
"outputs": [
{
@@ -5410,7 +5421,7 @@
"Loaded machine: Jupyter_LibraryStrings"
]
},
- "execution_count": 387,
+ "execution_count": 188,
"metadata": {},
"output_type": "execute_result"
}
@@ -5433,7 +5444,7 @@
},
{
"cell_type": "code",
- "execution_count": 379,
+ "execution_count": 189,
"metadata": {},
"outputs": [
{
@@ -5445,7 +5456,7 @@
"4"
]
},
- "execution_count": 379,
+ "execution_count": 189,
"metadata": {},
"output_type": "execute_result"
}
@@ -5465,7 +5476,7 @@
},
{
"cell_type": "code",
- "execution_count": 380,
+ "execution_count": 190,
"metadata": {},
"outputs": [
{
@@ -5477,7 +5488,7 @@
"TRUE"
]
},
- "execution_count": 380,
+ "execution_count": 190,
"metadata": {},
"output_type": "execute_result"
}
@@ -5488,7 +5499,7 @@
},
{
"cell_type": "code",
- "execution_count": 381,
+ "execution_count": 191,
"metadata": {},
"outputs": [
{
@@ -5515,7 +5526,7 @@
},
{
"cell_type": "code",
- "execution_count": 393,
+ "execution_count": 192,
"metadata": {},
"outputs": [
{
@@ -5527,7 +5538,7 @@
"{2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66,68,70,72,74,76,78,80,82,84,86,88,90,92,94,96,98,100}"
]
},
- "execution_count": 393,
+ "execution_count": 192,
"metadata": {},
"output_type": "execute_result"
}
@@ -5547,7 +5558,7 @@
},
{
"cell_type": "code",
- "execution_count": 390,
+ "execution_count": 193,
"metadata": {},
"outputs": [
{
@@ -5567,7 +5578,7 @@
"\ty = 3"
]
},
- "execution_count": 390,
+ "execution_count": 193,
"metadata": {},
"output_type": "execute_result"
}
@@ -5586,17 +5597,17 @@
},
{
"cell_type": "code",
- "execution_count": 382,
+ "execution_count": 194,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "ProB CLI: 1.9.0-beta8 (2a32153ac44523a5f93b0a999f9c42198b9360dc)\n",
- "ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3)"
+ "ProB CLI: 1.9.3-nightly (50333f1779dcae2a9e6d1b2aa95a23678821f851)\n",
+ "ProB 2: 4.0.0-SNAPSHOT (1d61b6ea7ef1b2e38a6b6045dbb0e81bcb6d8423)"
]
},
- "execution_count": 382,
+ "execution_count": 194,
"metadata": {},
"output_type": "execute_result"
}
@@ -5604,13 +5615,6 @@
"source": [
":version"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/models/Jars_DieHard_Puzzle.ipynb b/notebooks/models/Jars_DieHard_Puzzle.ipynb
index 14fdacc1d51558814e5c45e432a9347fcc23806d..603b0ca48724f083cd4f54f6bc6e9b614576cea8 100644
--- a/notebooks/models/Jars_DieHard_Puzzle.ipynb
+++ b/notebooks/models/Jars_DieHard_Puzzle.ipynb
@@ -25,7 +25,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
@@ -34,7 +34,7 @@
"Loaded machine: Jars"
]
},
- "execution_count": 11,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -80,7 +80,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -89,7 +89,7 @@
"Machine constants set up using operation 0: $setup_constants()"
]
},
- "execution_count": 12,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -100,7 +100,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -109,7 +109,7 @@
"Machine initialised using operation 1: $initialise_machine()"
]
},
- "execution_count": 13,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -127,7 +127,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -139,7 +139,7 @@
"{(j3↦0),(j5↦0)}"
]
},
- "execution_count": 14,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -157,7 +157,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -166,7 +166,7 @@
"Executed operation: FillJar(j5)"
]
},
- "execution_count": 15,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -184,7 +184,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -196,7 +196,7 @@
"{(j3↦0),(j5↦5)}"
]
},
- "execution_count": 16,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -214,7 +214,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -247,7 +247,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 17,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -265,7 +265,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
@@ -274,7 +274,7 @@
"Executed operation: Transfer(j5,3,j3)"
]
},
- "execution_count": 18,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -285,7 +285,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -297,7 +297,7 @@
"{(j3↦3),(j5↦2)}"
]
},
- "execution_count": 20,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -308,7 +308,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
@@ -341,7 +341,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 21,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -359,7 +359,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -368,7 +368,7 @@
"Executed operation: EmptyJar(j3)"
]
},
- "execution_count": 23,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -379,7 +379,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 12,
"metadata": {},
"outputs": [
{
@@ -412,7 +412,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 24,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -423,7 +423,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
@@ -432,7 +432,7 @@
"Executed operation: Transfer(j5,2,j3)"
]
},
- "execution_count": 25,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -443,7 +443,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
@@ -476,7 +476,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 26,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -487,7 +487,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
@@ -496,7 +496,7 @@
"Executed operation: FillJar(j5)"
]
},
- "execution_count": 27,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -507,7 +507,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
@@ -540,7 +540,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 28,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -551,7 +551,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -560,7 +560,7 @@
"Executed operation: Transfer(j5,1,j3)"
]
},
- "execution_count": 29,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -571,7 +571,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -604,7 +604,7 @@
"<Animation function visualisation>"
]
},
- "execution_count": 30,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -622,7 +622,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 19,
"metadata": {},
"outputs": [
{
@@ -634,7 +634,7 @@
"TRUE"
]
},
- "execution_count": 31,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -645,7 +645,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 20,
"metadata": {},
"outputs": [
{
@@ -654,65 +654,60 @@
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
- "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
- "<svg width=\"304pt\" height=\"113pt\"\n",
- " viewBox=\"0.00 0.00 304.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
- "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 109)\">\n",
+ "<svg width=\"304pt\" height=\"110pt\"\n",
+ " viewBox=\"0.00 0.00 304.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 106)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-109 301,-109 301,5 -4,5\"/>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 300,-106 300,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
- "<g id=\"node1\" class=\"node\"><title>Noderoot</title>\n",
- "<polygon fill=\"#b3ee3a\" stroke=\"#b3ee3a\" points=\"42,-76.6019 12,-76.6019 0,-64.6019 0,-47.3981 12,-35.3981 42,-35.3981 54,-47.3981 54,-64.6019 42,-76.6019\"/>\n",
- "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M12,-76.6019C6,-76.6019 0,-70.6019 0,-64.6019\"/>\n",
- "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M0,-47.3981C0,-41.3981 6,-35.3981 12,-35.3981\"/>\n",
- "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M42,-35.3981C48,-35.3981 54,-41.3981 54,-47.3981\"/>\n",
- "<path fill=\"#b3ee3a\" stroke=\"#b3ee3a\" d=\"M54,-64.6019C54,-70.6019 48,-76.6019 42,-76.6019\"/>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"42,-76.6019 12,-76.6019 \"/>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M12,-76.6019C6,-76.6019 0,-70.6019 0,-64.6019\"/>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"0,-64.6019 0,-47.3981 \"/>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M0,-47.3981C0,-41.3981 6,-35.3981 12,-35.3981\"/>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"12,-35.3981 42,-35.3981 \"/>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M42,-35.3981C48,-35.3981 54,-41.3981 54,-47.3981\"/>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"54,-47.3981 54,-64.6019 \"/>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M54,-64.6019C54,-70.6019 48,-76.6019 42,-76.6019\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-60.2\" font-family=\"Times,serif\" font-size=\"14.00\">∈</text>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-43.4\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>Noderoot</title>\n",
+ "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">∈</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
"</g>\n",
"<!-- Node1 -->\n",
- "<g id=\"node2\" class=\"node\"><title>Node1</title>\n",
- "<polygon fill=\"white\" stroke=\"black\" points=\"90,-69 90,-105 144,-105 144,-69 90,-69\"/>\n",
- "<text text-anchor=\"middle\" x=\"117\" y=\"-82.9\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>Node1</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"</g>\n",
"<!-- Node1->Noderoot -->\n",
- "<g id=\"edge2\" class=\"edge\"><title>Node1->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.5971,-77.699C81.4311,-74.8223 72.297,-71.6046 63.6152,-68.5463\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"64.6758,-65.2091 54.081,-65.1876 62.35,-71.8114 64.6758,-65.2091\"/>\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>Node1->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-74.499C81.796,-71.7653 72.6401,-68.7134 63.905,-65.8017\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.8886,-62.4403 54.295,-62.5983 62.675,-69.0811 64.8886,-62.4403\"/>\n",
"</g>\n",
"<!-- Node2 -->\n",
- "<g id=\"node4\" class=\"node\"><title>Node2</title>\n",
- "<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.2 90,-49.8 144,-49.8 144,-0.2 90,-0.2\"/>\n",
- "<text text-anchor=\"middle\" x=\"117\" y=\"-33.2\" font-family=\"Times,serif\" font-size=\"14.00\">ran</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"90,-25 144,-25 \"/>\n",
- "<text text-anchor=\"middle\" x=\"117\" y=\"-8.4\" font-family=\"Times,serif\" font-size=\"14.00\">{3,4}</text>\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>Node2</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-.5 90,-46.5 144,-46.5 144,-.5 90,-.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">ran</text>\n",
+ "<polyline fill=\"none\" stroke=\"#000000\" points=\"90,-23.5 144,-23.5 \"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{3,4}</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\n",
- "<g id=\"edge4\" class=\"edge\"><title>Node2->Noderoot</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M89.5971,-34.301C81.4311,-37.1777 72.297,-40.3954 63.6152,-43.4537\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"62.35,-40.1886 54.081,-46.8124 64.6758,-46.7909 62.35,-40.1886\"/>\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>Node2->Noderoot</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-32.501C81.796,-35.2347 72.6401,-38.2866 63.905,-41.1983\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.675,-37.9189 54.295,-44.4017 64.8886,-44.5597 62.675,-37.9189\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
- "<g id=\"node6\" class=\"node\"><title>Node3</title>\n",
- "<polygon fill=\"white\" stroke=\"black\" points=\"180.32,-0.2 180.32,-49.8 295.68,-49.8 295.68,-0.2 180.32,-0.2\"/>\n",
- "<text text-anchor=\"middle\" x=\"238\" y=\"-33.2\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
- "<polyline fill=\"none\" stroke=\"black\" points=\"180.32,-25 295.68,-25 \"/>\n",
- "<text text-anchor=\"middle\" x=\"238\" y=\"-8.4\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>Node3</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-.5 180,-46.5 296,-46.5 296,-.5 180,-.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"238\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">level</text>\n",
+ "<polyline fill=\"none\" stroke=\"#000000\" points=\"180,-23.5 296,-23.5 \"/>\n",
+ "<text text-anchor=\"middle\" x=\"238\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(j3↦3),(j5↦4)}</text>\n",
"</g>\n",
"<!-- Node3->Node2 -->\n",
- "<g id=\"edge6\" class=\"edge\"><title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M180.288,-25C171.365,-25 162.358,-25 154.072,-25\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"154.023,-21.5001 144.023,-25 154.023,-28.5001 154.023,-21.5001\"/>\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>Node3->Node2</title>\n",
+ "<path fill=\"none\" stroke=\"#000000\" d=\"M179.9808,-23.5C171.2934,-23.5 162.5376,-23.5 154.4316,-23.5\"/>\n",
+ "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.2102,-20.0001 144.2101,-23.5 154.2101,-27.0001 154.2102,-20.0001\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -721,7 +716,7 @@
"<Dot visualization: goal []>"
]
},
- "execution_count": 33,
+ "execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
@@ -729,13 +724,6 @@
"source": [
":dot goal"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/tests/chr_tests.ipynb b/notebooks/tests/chr_tests.ipynb
index 2249959231dac2a197d8cc29c051fd8dfd242d4f..d13d768d22a62cad9d49508979b932a47849f799 100644
--- a/notebooks/tests/chr_tests.ipynb
+++ b/notebooks/tests/chr_tests.ipynb
@@ -111,12 +111,17 @@
},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
- ]
+ "data": {
+ "text/markdown": [
+ "$\\mathit{time\\_out}$"
+ ],
+ "text/plain": [
+ "time_out"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
diff --git a/notebooks/tests/external_functions.ipynb b/notebooks/tests/external_functions.ipynb
index af4fb075bd5161a6308d4a5bcce7b78c6c44a90b..f7dcfb60cfc78a1df011d70392044f710a689ae9 100644
--- a/notebooks/tests/external_functions.ipynb
+++ b/notebooks/tests/external_functions.ipynb
@@ -31,10 +31,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.8.2-beta2\"}$"
+ "$\\text{\"1.9.3-nightly\"}$"
],
"text/plain": [
- "\"1.8.2-beta2\""
+ "\"1.9.3-nightly\""
]
},
"execution_count": 2,
@@ -54,10 +54,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.8.0_172-b11\"}$"
+ "$\\text{\"1.8.0_202-b08\"}$"
],
"text/plain": [
- "\"1.8.0_172-b11\""
+ "\"1.8.0_202-b08\""
]
},
"execution_count": 3,
@@ -77,10 +77,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"ce702ba99f667cb03de8ed41ab58ba72db9112c3\"}$"
+ "$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
],
"text/plain": [
- "\"ce702ba99f667cb03de8ed41ab58ba72db9112c3\""
+ "\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
]
},
"execution_count": 4,
@@ -123,10 +123,10 @@
{
"data": {
"text/markdown": [
- "$150958128$"
+ "$151498512$"
],
"text/plain": [
- "150958128"
+ "151498512"
]
},
"execution_count": 6,
@@ -152,7 +152,7 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":eval: NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.11/\n\n",
+ "evalue": ":eval: NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/Shared/Uni/SHK/ProB2/prob_prolog/\n\n",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
@@ -162,7 +162,7 @@
"\u001b[1m\u001b[31mAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31mJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.11/\u001b[0m"
+ "\u001b[1m\u001b[31mJava B parser (probcliparser.jar) is missing from lib directory in: /Users/Shared/Uni/SHK/ProB2/prob_prolog/\u001b[0m"
]
}
],
diff --git a/notebooks/tests/version.ipynb b/notebooks/tests/version.ipynb
index f2945abcff027eec29185d73af4e0c84bc6fb41f..9a1b887e75626004f59f2c7ee9bf793bbcd12f7f 100644
--- a/notebooks/tests/version.ipynb
+++ b/notebooks/tests/version.ipynb
@@ -36,8 +36,8 @@
{
"data": {
"text/plain": [
- "ProB CLI: 1.8.2-beta2 (ce702ba99f667cb03de8ed41ab58ba72db9112c3)\n",
- "ProB 2: 3.2.11 (f854ed1becc47dd98c4b75d8b1d5c000d6f9e185)"
+ "ProB CLI: 1.9.3-nightly (50333f1779dcae2a9e6d1b2aa95a23678821f851)\n",
+ "ProB 2: 4.0.0-SNAPSHOT (1d61b6ea7ef1b2e38a6b6045dbb0e81bcb6d8423)"
]
},
"execution_count": 2,
diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb
index 4b09952e1ebb7b4914a93cf6551686bde0d01c3d..96c6098a83446524c8a8d833be38f1c9eecc0eae 100644
--- a/notebooks/tutorials/Functional_Programming_in_B.ipynb
+++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb
@@ -68,14 +68,14 @@
"$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $\\mathit{r3} = [4,9,25,49,121]$\n",
+ "* $\\mathit{r3} = \\{(1\\mapsto 4),(2\\mapsto 9),(3\\mapsto 25),(4\\mapsto 49),(5\\mapsto 121)\\}$\n",
"* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
- "\tr3 = [4,9,25,49,121]\n",
+ "\tr3 = {(1↦4),(2↦9),(3↦25),(4↦49),(5↦121)}\n",
"\tf = λx·(x ∈ INTEGER∣x ∗ x)"
]
},
@@ -185,14 +185,14 @@
"$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
- "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
+ "* $\\mathit{f} = /*@symbolic*/ \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
"* $\\mathit{r1} = 317$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
- "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+ "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
"\tr1 = 317"
]
},
@@ -225,10 +225,10 @@
"\n",
"**Solution:**\n",
"* $\\mathit{r2} = \\{1,2,3,4\\}$\n",
- "* $\\mathit{r3} = [2,2,3,3,4]$\n",
+ "* $\\mathit{r3} = \\{(1\\mapsto 2),(2\\mapsto 2),(3\\mapsto 3),(4\\mapsto 3),(5\\mapsto 4)\\}$\n",
"* $\\mathit{r4} = 2$\n",
"* $\\mathit{sqr} = 9802$\n",
- "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
+ "* $\\mathit{f} = /*@symbolic*/ \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$\n",
"* $\\mathit{r1} = 317$"
],
"text/plain": [
@@ -236,10 +236,10 @@
"\n",
"Solution:\n",
"\tr2 = {1,2,3,4}\n",
- "\tr3 = [2,2,3,3,4]\n",
+ "\tr3 = {(1↦2),(2↦2),(3↦3),(4↦3),(5↦4)}\n",
"\tr4 = 2\n",
"\tsqr = 9802\n",
- "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+ "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
"\tr1 = 317"
]
},
@@ -276,14 +276,14 @@
"\n",
"**Solution:**\n",
"* $\\mathit{r5} = \\{2,4,10,100\\}$\n",
- "* $\\mathit{f} = \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$"
+ "* $\\mathit{f} = /*@symbolic*/ \\{\\mathit{x},\\mathit{y}\\mid \\mathit{x} \\in \\mathit{NATURAL} \\land \\mathit{y} \\cprod 2 \\geq \\mathit{x} \\land (\\mathit{y} - 1) \\cprod 2 < \\mathit{x}\\}$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr5 = {2,4,10,100}\n",
- "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}"
+ "\tf = /*@symbolic*/ {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}"
]
},
"execution_count": 7,
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 512fcd47e6f698b480776e8858c6837b7ec7a4ac..9bb75a800034f527152874f71e149bef6cbf7de8 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -288,10 +288,10 @@
{
"data": {
"text/markdown": [
- "$\\{(((((((9\\mapsto 5)\\mapsto 6)\\mapsto 7)\\mapsto 1)\\mapsto 0)\\mapsto 8)\\mapsto 2)\\}$"
+ "$\\{(9\\mapsto 5\\mapsto 6\\mapsto 7\\mapsto 1\\mapsto 0\\mapsto 8\\mapsto 2)\\}$"
],
"text/plain": [
- "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
+ "{(9↦5↦6↦7↦1↦0↦8↦2)}"
]
},
"execution_count": 8,
@@ -547,10 +547,10 @@
{
"data": {
"text/markdown": [
- "$\\{((\\mathit{TRUE}\\mapsto \\mathit{TRUE})\\mapsto \\mathit{FALSE})\\}$"
+ "$\\{(\\mathit{TRUE}\\mapsto \\mathit{TRUE}\\mapsto \\mathit{FALSE})\\}$"
],
"text/plain": [
- "{((TRUE↦TRUE)↦FALSE)}"
+ "{(TRUE↦TRUE↦FALSE)}"
]
},
"execution_count": 14,