From 798ed3f1f84b0004a6a2426d21e8fed03225dac3 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 6 Jan 2022 13:59:56 +0100
Subject: [PATCH] Re-execute all notebooks using current kernel
---
notebooks/experiments/DeliveryExercise.ipynb | 2 +-
.../SMT_Translation_Experiments.ipynb | 12 +-
notebooks/manual/ExternalFunctions.ipynb | 116 ++--
notebooks/models/Jars_DieHard_Puzzle.ipynb | 52 +-
notebooks/models/NFA_to_DFA.ipynb | 497 +++++++++---------
notebooks/models/NQueens_Puzzle.ipynb | 11 +-
notebooks/models/scheduler.ipynb | 8 +-
notebooks/tests/animate.ipynb | 44 +-
notebooks/tests/dot.ipynb | 364 ++++++-------
notebooks/tests/external_functions.ipynb | 21 +-
notebooks/tests/help.ipynb | 6 +-
notebooks/tests/language.ipynb | 6 +-
notebooks/tests/load_cell.ipynb | 30 +-
notebooks/tests/modelcheck.ipynb | 6 +-
notebooks/tests/pref.ipynb | 15 +
notebooks/tests/render.ipynb | 4 +-
notebooks/tests/show.ipynb | 24 +-
notebooks/tests/solve.ipynb | 23 +-
notebooks/tests/table.ipynb | 36 +-
notebooks/tests/time.ipynb | 8 +-
notebooks/tests/trace.ipynb | 2 +-
notebooks/tests/type.ipynb | 16 +-
notebooks/tests/version.ipynb | 12 +-
.../Functional_Programming_in_B.ipynb | 58 +-
notebooks/tutorials/prob_solver_intro.ipynb | 20 +-
25 files changed, 716 insertions(+), 677 deletions(-)
diff --git a/notebooks/experiments/DeliveryExercise.ipynb b/notebooks/experiments/DeliveryExercise.ipynb
index 902fbab..d9ac661 100644
--- a/notebooks/experiments/DeliveryExercise.ipynb
+++ b/notebooks/experiments/DeliveryExercise.ipynb
@@ -83,7 +83,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb
index a953d67..3675139 100644
--- a/notebooks/experiments/SMT_Translation_Experiments.ipynb
+++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb
@@ -104,10 +104,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 0.394252508 seconds"
+ "Execution time: 0.359755436 seconds"
],
"text/plain": [
- "Execution time: 0.394252508 seconds"
+ "Execution time: 0.359755436 seconds"
]
},
"metadata": {},
@@ -211,10 +211,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "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,[])))",
+ "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), 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"
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
@@ -239,10 +239,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "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,[])))",
+ "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), 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"
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist), reason: solver_not_available\u001b[0m"
]
}
],
diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index 9030aec..faa876f 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -1879,7 +1879,7 @@
"text/markdown": [
"|stringify|tostring|\n",
"|---|---|\n",
- "|$\\text{\"\\\"abc\\\"\"}$|$\\text{\"abc\"}$|\n"
+ "|\"\\\"abc\\\"\"|\"abc\"|\n"
],
"text/plain": [
"stringify\ttostring\n",
@@ -2391,78 +2391,78 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\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=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
"<!-- 4 -->\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",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 3 -->\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",
+ "<text text-anchor=\"middle\" x=\"46\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 4->3 -->\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",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M14.23,-86.67C8.69,-76.96 4.4,-64.68 9,-54 10.57,-50.36 12.72,-46.92 15.21,-43.72\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"17.81,-46.06 21.93,-36.3 12.62,-41.36 17.81,-46.06\"/>\n",
+ "<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 3->4 -->\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",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M42.16,-36.18C39.56,-47.81 36.07,-63.42 33.09,-76.73\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"29.61,-76.28 30.84,-86.8 36.44,-77.8 29.61,-76.28\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 2 -->\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",
+ "<text text-anchor=\"middle\" x=\"122\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 2->3 -->\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",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M106.62,-86.8C95.6,-74.47 80.58,-57.68 68.25,-43.89\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.63,-41.3 61.36,-36.18 65.41,-45.96 70.63,-41.3\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1 -->\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",
+ "<text text-anchor=\"middle\" x=\"141\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 2->1 -->\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",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M120.44,-86.62C120.04,-76.88 120.32,-64.61 123,-54 123.72,-51.14 124.71,-48.26 125.86,-45.43\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.12,-46.72 130.2,-36.18 122.78,-43.75 129.12,-46.72\"/>\n",
+ "<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1->2 -->\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",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M141.52,-36.36C141.42,-46.09 140.65,-58.37 138,-69 137.33,-71.7 136.45,-74.45 135.45,-77.16\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"132.11,-76.08 131.46,-86.65 138.56,-78.8 132.11,-76.08\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"</g>\n",
- "</svg>"
+ "</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [(\"rel\",{(1,2),(2,1),(2,3),(3,4),(4,3)})]>"
+ "<Dot visualization: expr_as_graph [(\"rel\",{1|->2,2|->1,2|->3,3|->4,4|->3})]>"
]
},
"execution_count": 87,
@@ -2550,10 +2550,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.9.3-nightly\"}$"
+ "$\\text{\"1.11.1-final\"}$"
],
"text/plain": [
- "\"1.9.3-nightly\""
+ "\"1.11.1-final\""
]
},
"execution_count": 90,
@@ -2573,10 +2573,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
+ "$\\text{\"1125ea39af78125a39093c65a0af783b7636b362\"}$"
],
"text/plain": [
- "\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
+ "\"1125ea39af78125a39093c65a0af783b7636b362\""
]
},
"execution_count": 91,
@@ -2596,10 +2596,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"Mon Feb 17 13:18:47 2020 +0100\"}$"
+ "$\\text{\"Wed Dec 29 13:14:39 2021 +0100\"}$"
],
"text/plain": [
- "\"Mon Feb 17 13:18:47 2020 +0100\""
+ "\"Wed Dec 29 13:14:39 2021 +0100\""
]
},
"execution_count": 92,
@@ -2619,10 +2619,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.8.0_202-b08\"}$"
+ "$\\text{\"1.17.35\\\"\\n\"}$"
],
"text/plain": [
- "\"1.8.0_202-b08\""
+ "\"1.17.35\\\"\\n\""
]
},
"execution_count": 93,
@@ -2642,10 +2642,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\"}$"
+ "$\\text{\"/Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/java\"}$"
],
"text/plain": [
- "\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\""
+ "\"/Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/java\""
]
},
"execution_count": 94,
@@ -2665,10 +2665,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"18/2/2020 - 15h29 52s\"}$"
+ "$\\text{\"6/1/2022 - 13h37 50s\"}$"
],
"text/plain": [
- "\"18/2/2020 - 15h29 52s\""
+ "\"6/1/2022 - 13h37 50s\""
]
},
"execution_count": 95,
@@ -2704,10 +2704,10 @@
{
"data": {
"text/markdown": [
- "$151477456$"
+ "$166651936$"
],
"text/plain": [
- "151477456"
+ "166651936"
]
},
"execution_count": 96,
@@ -2819,10 +2819,10 @@
{
"data": {
"text/markdown": [
- "$1582036192$"
+ "$1641472670$"
],
"text/plain": [
- "1582036192"
+ "1641472670"
]
},
"execution_count": 101,
@@ -2842,10 +2842,10 @@
{
"data": {
"text/markdown": [
- "$1658$"
+ "$2295$"
],
"text/plain": [
- "1658"
+ "2295"
]
},
"execution_count": 102,
@@ -2865,10 +2865,10 @@
{
"data": {
"text/markdown": [
- "$2881$"
+ "$18724$"
],
"text/plain": [
- "2881"
+ "18724"
]
},
"execution_count": 103,
@@ -3268,10 +3268,10 @@
{
"data": {
"text/markdown": [
- "$\\{\\text{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}\\}$"
+ "$\\{\\text{\"9541282a9b1c250d7244201817fbc6f332a22940\"}\\}$"
],
"text/plain": [
- "{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}"
+ "{\"9541282a9b1c250d7244201817fbc6f332a22940\"}"
]
},
"execution_count": 119,
@@ -3405,7 +3405,7 @@
{
"data": {
"text/markdown": [
- "$\\{(1\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"version\"}\\mapsto\\text{\"0.1\"})\\},\\mathit{element}\\in\\text{\"Data\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"3\"})\\},\\mathit{pId}\\in 0,\\mathit{recId}\\in 1)),(2\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"attr1\"}\\mapsto\\text{\"value1\"}),(\\text{\"elemID\"}\\mapsto\\text{\"ID1\"})\\},\\mathit{element}\\in\\text{\"Tag1\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"4\"})\\},\\mathit{pId}\\in 1,\\mathit{recId}\\in 2))\\}$"
+ "$\\{(1\\mapsto\\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"version\"}\\mapsto\\text{\"0.1\"})\\},\\mathit{element}\\in\\text{\"Data\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"3\"})\\},\\mathit{pId}\\in 0,\\mathit{recId}\\in 1)),(2\\mapsto\\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"attr1\"}\\mapsto\\text{\"value1\"}),(\\text{\"elemID\"}\\mapsto\\text{\"ID1\"})\\},\\mathit{element}\\in\\text{\"Tag1\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"4\"})\\},\\mathit{pId}\\in 1,\\mathit{recId}\\in 2))\\}$"
],
"text/plain": [
"{(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))}"
@@ -5044,13 +5044,13 @@
"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/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",
+ "evalue": ":eval: UNKNOWN: \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: 34, 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:eval: UNKNOWN: \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/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 ### Line: 34, 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"
]
}
@@ -5507,10 +5507,13 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
+ "evalue": ":eval: NOT-WELL-DEFINED: \narg not positive x > 0\n ### Line: 1, Column: 27 until 30\n ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\n\n",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
+ "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
+ "\u001b[1m\u001b[31marg not positive x > 0\u001b[0m",
+ "\u001b[1m\u001b[31m ### Line: 1, Column: 27 until 30\u001b[0m",
+ "\u001b[1m\u001b[31m ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\u001b[0m"
]
}
],
@@ -5606,8 +5609,13 @@
{
"data": {
"text/plain": [
- "ProB CLI: 1.9.3-nightly (50333f1779dcae2a9e6d1b2aa95a23678821f851)\n",
- "ProB 2: 4.0.0-SNAPSHOT (1d61b6ea7ef1b2e38a6b6045dbb0e81bcb6d8423)"
+ "ProB 2 Jupyter kernel: 1.2.1-SNAPSHOT (2aaa99bab781d6eca5a2b3388cca76b412fd52f6)\n",
+ "ProB 2: 3.15.0 (6ee6df4eab62d20df40c36cd42108b62962ec41b)\n",
+ "ProB B parser: 2.9.32 (7306d13499ba281a6e336c006d9fb23204624daa)\n",
+ "ProB CLI:\n",
+ "\t1.11.1-final (1125ea39af78125a39093c65a0af783b7636b362)\n",
+ "\tLast changed: Wed Dec 29 13:14:39 2021 +0100\n",
+ "\tProlog: SICStus 4.7.0 (x86_64-darwin-18.7.0): Wed Jul 7 17:07:32 CEST 2021"
]
},
"execution_count": 194,
diff --git a/notebooks/models/Jars_DieHard_Puzzle.ipynb b/notebooks/models/Jars_DieHard_Puzzle.ipynb
index 603b0ca..f2386e6 100644
--- a/notebooks/models/Jars_DieHard_Puzzle.ipynb
+++ b/notebooks/models/Jars_DieHard_Puzzle.ipynb
@@ -86,7 +86,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
@@ -106,7 +106,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
@@ -654,63 +654,63 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\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",
+ "<svg width=\"303pt\" height=\"110pt\"\n",
+ " viewBox=\"0.00 0.00 303.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=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 300,-106 300,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 299,-106 299,4 -4,4\"/>\n",
"<!-- Noderoot -->\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",
+ "<path fill=\"#b3ee3a\" stroke=\"black\" 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\">∈</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
"</g>\n",
"<!-- Node1 -->\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",
+ "<polygon fill=\"white\" stroke=\"black\" 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\">4</text>\n",
"</g>\n",
"<!-- Node1->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
"</g>\n",
"<!-- Node2 -->\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",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">ran</text>\n",
+ "<polyline fill=\"none\" stroke=\"black\" 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\">{3,4}</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
"</g>\n",
"<!-- Node3 -->\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",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"180,-0.5 180,-46.5 295,-46.5 295,-0.5 180,-0.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"237.5\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
+ "<polyline fill=\"none\" stroke=\"black\" points=\"180,-23.5 295,-23.5 \"/>\n",
+ "<text text-anchor=\"middle\" x=\"237.5\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
"</g>\n",
"<!-- Node3->Node2 -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M179.68,-23.5C171.01,-23.5 162.26,-23.5 154.2,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.04,-20 144.04,-23.5 154.04,-27 154.04,-20\"/>\n",
"</g>\n",
"</g>\n",
- "</svg>"
+ "</svg>\n"
],
"text/plain": [
"<Dot visualization: goal []>"
diff --git a/notebooks/models/NFA_to_DFA.ipynb b/notebooks/models/NFA_to_DFA.ipynb
index f6bbcac..f57b2a0 100644
--- a/notebooks/models/NFA_to_DFA.ipynb
+++ b/notebooks/models/NFA_to_DFA.ipynb
@@ -123,7 +123,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 3,
@@ -143,7 +143,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 4,
@@ -204,14 +204,14 @@
"text/markdown": [
"|prj11|prj12|prj2|\n",
"|---|---|---|\n",
- "|$\\mathit{z0}$|$0$|$\\{\\mathit{z0}\\}$|\n",
- "|$\\mathit{z0}$|$1$|$\\{\\mathit{z0},\\mathit{z1}\\}$|\n",
- "|$\\mathit{z1}$|$0$|$\\{\\mathit{z2}\\}$|\n",
- "|$\\mathit{z1}$|$1$|$\\{\\mathit{z2}\\}$|\n",
- "|$\\mathit{z2}$|$0$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\mathit{z2}$|$1$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\mathit{z3}$|$0$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\mathit{z3}$|$1$|$\\{\\mathit{z3}\\}$|\n"
+ "|z0|0|{z0}|\n",
+ "|z0|1|{z0,z1}|\n",
+ "|z1|0|{z2}|\n",
+ "|z1|1|{z2}|\n",
+ "|z2|0|{z3}|\n",
+ "|z2|1|{z3}|\n",
+ "|z3|0|{z3}|\n",
+ "|z3|1|{z3}|\n"
],
"text/plain": [
"prj11\tprj12\tprj2\n",
@@ -252,90 +252,91 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
- "<svg width=\"146pt\" height=\"472pt\"\n",
- " viewBox=\"0.00 0.00 146.00 472.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 468)\">\n",
+ "<svg width=\"144pt\" height=\"358pt\"\n",
+ " viewBox=\"0.00 0.00 144.00 358.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 354)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-468 142,-468 142,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-354 140,-354 140,4 -4,4\"/>\n",
"<g id=\"clust1\" class=\"cluster\">\n",
"<title>cluster_Z</title>\n",
- "<polygon fill=\"#d3d3d3\" stroke=\"#d3d3d3\" points=\"8,-8 8,-456 130,-456 130,-8 8,-8\"/>\n",
- "<text text-anchor=\"middle\" x=\"69\" y=\"-442.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">Z</text>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-342 128,-342 128,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-328.4\" font-family=\"Times,serif\" font-size=\"12.00\">Z</text>\n",
"</g>\n",
"<!-- z0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>z0</title>\n",
- "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-427 16,-427 16,-391 70,-391 70,-427\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z0</text>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-313 16,-313 16,-277 70,-277 70,-313\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">z0</text>\n",
"</g>\n",
"<!-- z0->z0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>z0->z0</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M70.2408,-412.3717C80.0239,-412.4442 88,-411.3203 88,-409 88,-407.5861 85.0382,-406.6164 80.5105,-406.091\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"80.3882,-402.582 70.2408,-405.6283 80.0731,-409.5749 80.3882,-402.582\"/>\n",
- "<text text-anchor=\"middle\" x=\"92\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-298.93C80.02,-299.02 88,-297.71 88,-295 88,-293.35 85.04,-292.22 80.51,-291.61\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.41,-288.1 70.24,-291.07 80.04,-295.09 80.41,-288.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"91.5\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- z0->z0 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>z0->z0</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.1975,-415.1551C88.3402,-416.8876 106,-414.8359 106,-409 106,-404.2583 94.3418,-402.0148 80.2386,-402.2695\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"79.9809,-398.7784 70.1975,-402.8449 80.3814,-405.7669 79.9809,-398.7784\"/>\n",
- "<text text-anchor=\"middle\" x=\"110\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.2,-302.18C88.34,-304.2 106,-301.81 106,-295 106,-289.47 94.34,-286.85 80.24,-287.15\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"79.94,-283.66 70.2,-287.82 80.41,-290.64 79.94,-283.66\"/>\n",
+ "<text text-anchor=\"middle\" x=\"109.5\" y=\"-291.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>z1</title>\n",
- "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-302 16,-302 16,-266 70,-266 70,-302\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-280.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z1</text>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-226 16,-226 16,-190 70,-190 70,-226\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-204.3\" font-family=\"Times,serif\" font-size=\"14.00\">z1</text>\n",
"</g>\n",
"<!-- z0->z1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>z0->z1</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M43,-390.8239C43,-370.2723 43,-336.5472 43,-312.4893\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"46.5001,-312.198 43,-302.198 39.5001,-312.198 46.5001,-312.198\"/>\n",
- "<text text-anchor=\"middle\" x=\"47\" y=\"-342.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-276.8C43,-265.16 43,-249.55 43,-236.24\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5,-236.18 43,-226.18 39.5,-236.18 46.5,-236.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-247.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- z2 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>z2</title>\n",
- "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-177 16,-177 16,-141 70,-141 70,-177\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-155.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z2</text>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">z2</text>\n",
"</g>\n",
"<!-- z1->z2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>z1->z2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-265.8239C43,-245.2723 43,-211.5472 43,-187.4893\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-187.198 43,-177.198 39.5001,-187.198 46.5001,-187.198\"/>\n",
- "<text text-anchor=\"middle\" x=\"47\" y=\"-217.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-189.8C43,-178.16 43,-162.55 43,-149.24\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-149.18 43,-139.18 39.5,-149.18 46.5,-149.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-160.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z3 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>z3</title>\n",
"<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n",
- "<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z3</text>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">z3</text>\n",
"</g>\n",
"<!-- z3->z3 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>z3->z3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.2408,-40.7434C80.0239,-40.8884 88,-38.6406 88,-34 88,-31.1721 85.0382,-29.2328 80.5105,-28.182\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"80.5146,-24.6683 70.2408,-27.2566 79.8863,-31.64 80.5146,-24.6683\"/>\n",
- "<text text-anchor=\"middle\" x=\"92\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.24,-41.87C80.02,-42.04 88,-39.41 88,-34 88,-30.7 85.04,-28.44 80.51,-27.21\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"80.55,-23.7 70.24,-26.13 79.82,-30.66 80.55,-23.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"91.5\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- z2->z3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>z2->z3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-140.8239C43,-120.2723 43,-86.5472 43,-62.4893\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-62.198 43,-52.198 39.5001,-62.198 46.5001,-62.198\"/>\n",
- "<text text-anchor=\"middle\" x=\"47\" y=\"-92.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-102.8C43,-91.16 43,-75.55 43,-62.24\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5,-62.18 43,-52.18 39.5,-62.18 46.5,-62.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"</g>\n",
- "</svg>"
+ "</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:δ(x, 0)})]>"
+ "<Dot visualization: expr_as_graph [(\"0\",{x,y| x∈Z & y:δ(x,0)},\n",
+ " \"1\",{x,y| x∈S & y∈δ(x,1)})]>"
]
},
"execution_count": 7,
@@ -425,10 +426,10 @@
"text/markdown": [
"|x|y|z|\n",
"|---|---|---|\n",
- "|$0$|$1$|$0$|\n",
- "|$0$|$1$|$1$|\n",
- "|$1$|$1$|$0$|\n",
- "|$1$|$1$|$1$|\n"
+ "|0|1|0|\n",
+ "|0|1|1|\n",
+ "|1|1|0|\n",
+ "|1|1|1|\n"
],
"text/plain": [
"x\ty\tz\n",
@@ -464,10 +465,10 @@
"text/markdown": [
"|x|y|z|\n",
"|---|---|---|\n",
- "|$0$|$0$|$0$|\n",
- "|$0$|$0$|$1$|\n",
- "|$1$|$0$|$0$|\n",
- "|$1$|$0$|$1$|\n"
+ "|0|0|0|\n",
+ "|0|0|1|\n",
+ "|1|0|0|\n",
+ "|1|0|1|\n"
],
"text/plain": [
"x\ty\tz\n",
@@ -558,38 +559,38 @@
"text/markdown": [
"|x|a|y|\n",
"|---|---|---|\n",
- "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$|$0$|$\\emptyset$|\n",
- "|$\\emptyset$|$1$|$\\emptyset$|\n",
- "|$\\{\\mathit{z0}\\}$|$0$|$\\{\\mathit{z0}\\}$|\n",
- "|$\\{\\mathit{z0}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1}\\}$|$0$|$\\{\\mathit{z2}\\}$|\n",
- "|$\\{\\mathit{z1}\\}$|$1$|$\\{\\mathit{z2}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z2}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z2}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z3}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
- "|$\\{\\mathit{z3}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n"
+ "|∅|0|∅|\n",
+ "|∅|1|∅|\n",
+ "|{z0}|0|{z0}|\n",
+ "|{z0}|1|{z0,z1}|\n",
+ "|{z0,z1}|0|{z0,z2}|\n",
+ "|{z0,z1}|1|{z0,z1,z2}|\n",
+ "|{z0,z2}|0|{z0,z3}|\n",
+ "|{z0,z2}|1|{z0,z1,z3}|\n",
+ "|{z0,z3}|0|{z0,z3}|\n",
+ "|{z0,z3}|1|{z0,z1,z3}|\n",
+ "|{z1}|0|{z2}|\n",
+ "|{z1}|1|{z2}|\n",
+ "|{z0,z1,z2}|0|{z0,z2,z3}|\n",
+ "|{z0,z1,z2}|1|{z0,z1,z2,z3}|\n",
+ "|{z0,z1,z3}|0|{z0,z2,z3}|\n",
+ "|{z0,z1,z3}|1|{z0,z1,z2,z3}|\n",
+ "|{z1,z2}|0|{z2,z3}|\n",
+ "|{z1,z2}|1|{z2,z3}|\n",
+ "|{z1,z3}|0|{z2,z3}|\n",
+ "|{z1,z3}|1|{z2,z3}|\n",
+ "|{z0,z1,z2,z3}|0|{z0,z2,z3}|\n",
+ "|{z0,z1,z2,z3}|1|{z0,z1,z2,z3}|\n",
+ "|{z2}|0|{z3}|\n",
+ "|{z2}|1|{z3}|\n",
+ "|{z0,z2,z3}|0|{z0,z3}|\n",
+ "|{z0,z2,z3}|1|{z0,z1,z3}|\n",
+ "|{z1,z2,z3}|0|{z2,z3}|\n",
+ "|{z1,z2,z3}|1|{z2,z3}|\n",
+ "|{z2,z3}|0|{z3}|\n",
+ "|{z2,z3}|1|{z3}|\n",
+ "|{z3}|0|{z3}|\n",
+ "|{z3}|1|{z3}|\n"
],
"text/plain": [
"x\ta\ty\n",
@@ -674,402 +675,405 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
- "<svg width=\"662pt\" height=\"566pt\"\n",
- " viewBox=\"0.00 0.00 662.00 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<svg width=\"654pt\" height=\"566pt\"\n",
+ " viewBox=\"0.00 0.00 654.00 566.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 562)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-562 658,-562 658,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-562 650,-562 650,4 -4,4\"/>\n",
"<!-- \\{z2,z3\\} -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>\\{z2,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"226,-471 166,-471 166,-435 226,-435 226,-471\"/>\n",
- "<text text-anchor=\"middle\" x=\"196\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"223.5,-471 164.5,-471 164.5,-435 223.5,-435 223.5,-471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"194\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z2,z3}</text>\n",
"</g>\n",
"<!-- \\{z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M226.4673,-460.8731C236.248,-460.7923 244,-458.168 244,-453 244,-449.8508 241.1214,-447.6461 236.6593,-446.3859\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"236.8209,-442.8794 226.4673,-445.1269 235.9627,-449.8266 236.8209,-442.8794\"/>\n",
- "<text text-anchor=\"middle\" x=\"254.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M223.69,-460.88C233.58,-460.88 241.5,-458.25 241.5,-453 241.5,-449.72 238.41,-447.46 233.67,-446.23\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"234.01,-442.75 223.69,-445.12 233.24,-449.71 234.01,-442.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"251.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z3\\} -->\n",
"<g id=\"node10\" class=\"node\">\n",
"<title>\\{z3\\}</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"185,-384 131,-384 131,-348 185,-348 185,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"158\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z3}</text>\n",
+ "<text text-anchor=\"middle\" x=\"158\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z3}</text>\n",
"</g>\n",
"<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.1924,-434.6451C169.3745,-429.4531 164.8587,-423.4437 162,-417 158.8801,-409.9675 157.4136,-401.8548 156.8388,-394.1981\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.3368,-394.0739 156.5362,-384.1842 153.34,-394.2854 160.3368,-394.0739\"/>\n",
- "<text text-anchor=\"middle\" x=\"166\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.14,-434.79C169.36,-429.57 164.82,-423.49 162,-417 158.98,-410.05 157.55,-402.05 156.98,-394.52\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.47,-394.22 156.67,-384.33 153.47,-394.44 160.47,-394.22\"/>\n",
+ "<text text-anchor=\"middle\" x=\"165.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
"<g id=\"edge27\" class=\"edge\">\n",
"<title>\\{z2,z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M188.1264,-434.9735C182.8784,-422.9585 175.8819,-406.9401 169.9523,-393.3646\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.0737,-391.7664 165.8635,-384.0034 166.6589,-394.5683 173.0737,-391.7664\"/>\n",
- "<text text-anchor=\"middle\" x=\"184\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M186.71,-434.8C181.69,-422.93 174.91,-406.93 169.2,-393.45\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"172.4,-392.02 165.27,-384.18 165.95,-394.75 172.4,-392.02\"/>\n",
+ "<text text-anchor=\"middle\" x=\"182.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\} -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>\\{z1,z2,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"149.5,-558 72.5,-558 72.5,-522 149.5,-522 149.5,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"111\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"148,-558 72,-558 72,-522 148,-522 148,-558\"/>\n",
+ "<text text-anchor=\"middle\" x=\"110\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2,z3}</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M111.9305,-521.819C113.3101,-511.2556 116.546,-498.2486 124,-489 132.3732,-478.611 144.5156,-470.9638 156.4511,-465.4583\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"158.0369,-468.5886 165.9028,-461.4908 155.3275,-462.1342 158.0369,-468.5886\"/>\n",
- "<text text-anchor=\"middle\" x=\"128\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M110.93,-521.63C112.3,-511.19 115.52,-498.18 123,-489 131.29,-478.83 143.27,-471.37 155.04,-466.03\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"156.45,-469.23 164.35,-462.18 153.77,-462.76 156.45,-469.23\"/>\n",
+ "<text text-anchor=\"middle\" x=\"126.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge28\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M128.6121,-521.9735C140.9208,-509.3752 157.5297,-492.3755 171.1785,-478.4055\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.9256,-480.6021 178.4105,-471.0034 168.9186,-475.7103 173.9256,-480.6021\"/>\n",
- "<text text-anchor=\"middle\" x=\"163\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M127,-521.8C139.3,-509.36 156.09,-492.36 169.78,-478.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"172.49,-480.75 177.03,-471.18 167.51,-475.83 172.49,-480.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"161.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2,z3\\}->\\{z1,z2,z3\\} -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>\\{z1,z2,z3\\}->\\{z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M149.5552,-547.8058C159.7662,-547.3597 167.5,-544.7578 167.5,-540 167.5,-537.0264 164.479,-534.8949 159.7203,-533.6055\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"159.9415,-530.1027 149.5552,-532.1942 158.9788,-537.0362 159.9415,-530.1027\"/>\n",
- "<text text-anchor=\"middle\" x=\"178\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M148.21,-547.81C158.33,-547.36 166,-544.76 166,-540 166,-537.03 163.01,-534.89 158.29,-533.61\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"158.6,-530.12 148.21,-532.19 157.63,-537.05 158.6,-530.12\"/>\n",
+ "<text text-anchor=\"middle\" x=\"176\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2,z3\\} -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>\\{z0,z2,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-297 272.5,-297 272.5,-261 349.5,-261 349.5,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"311\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"347,-297 271,-297 271,-261 347,-261 347,-297\"/>\n",
+ "<text text-anchor=\"middle\" x=\"309\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2,z3}</text>\n",
"</g>\n",
"<!-- \\{z0,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-286.8058C359.7662,-286.3597 367.5,-283.7578 367.5,-279 367.5,-276.0264 364.479,-273.8949 359.7203,-272.6055\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-269.1027 349.5552,-271.1942 358.9788,-276.0362 359.9415,-269.1027\"/>\n",
- "<text text-anchor=\"middle\" x=\"378\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.21,-286.81C357.33,-286.36 365,-283.76 365,-279 365,-276.03 362.01,-273.89 357.29,-272.61\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"357.6,-269.12 347.21,-271.19 356.63,-276.05 357.6,-269.12\"/>\n",
+ "<text text-anchor=\"middle\" x=\"375\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\} -->\n",
"<g id=\"node11\" class=\"node\">\n",
"<title>\\{z0,z1,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"393.5,-123 316.5,-123 316.5,-87 393.5,-87 393.5,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"355\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"390,-123 314,-123 314,-87 390,-87 390,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"352\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z3}</text>\n",
"</g>\n",
"<!-- \\{z0,z2,z3\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge13\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.8901,-260.86C313.2776,-239.6836 316.7192,-203.7656 325,-174 328.9228,-159.8994 335.1587,-144.9239 340.9314,-132.5406\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"344.2285,-133.7603 345.4087,-123.2314 337.9202,-130.7263 344.2285,-133.7603\"/>\n",
- "<text text-anchor=\"middle\" x=\"329\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.9,-260.79C311.31,-239.93 314.78,-203.86 323,-174 326.9,-159.84 333.1,-144.76 338.77,-132.4\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"342.04,-133.68 343.16,-123.15 335.71,-130.69 342.04,-133.68\"/>\n",
+ "<text text-anchor=\"middle\" x=\"326.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\} -->\n",
"<g id=\"node14\" class=\"node\">\n",
"<title>\\{z0,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"487,-210 427,-210 427,-174 487,-174 487,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"457\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"481.5,-210 422.5,-210 422.5,-174 481.5,-174 481.5,-210\"/>\n",
+ "<text text-anchor=\"middle\" x=\"452\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z3}</text>\n",
"</g>\n",
"<!-- \\{z0,z2,z3\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge29\" class=\"edge\">\n",
"<title>\\{z0,z2,z3\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M341.2513,-260.9735C363.47,-247.7336 393.8464,-229.6326 417.9059,-215.2958\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"419.9886,-218.1291 426.7875,-210.0034 416.4053,-212.1157 419.9886,-218.1291\"/>\n",
- "<text text-anchor=\"middle\" x=\"396\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M337.94,-260.8C359.94,-247.72 390.39,-229.62 414.29,-215.41\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"416.3,-218.29 423.1,-210.18 412.72,-212.28 416.3,-218.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"392.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z2\\} -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>\\{z2\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"92,-471 38,-471 38,-435 92,-435 92,-471\"/>\n",
- "<text text-anchor=\"middle\" x=\"65\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"91,-471 37,-471 37,-435 91,-435 91,-471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"64\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z2}</text>\n",
"</g>\n",
"<!-- \\{z2\\}->\\{z2\\} -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M92.2408,-460.8673C102.0239,-461.0365 110,-458.4141 110,-453 110,-449.7008 107.0382,-447.4382 102.5105,-446.2123\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"102.5519,-442.6975 92.2408,-445.1327 101.82,-449.6591 102.5519,-442.6975\"/>\n",
- "<text text-anchor=\"middle\" x=\"120.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M91.24,-460.87C101.02,-461.04 109,-458.41 109,-453 109,-449.7 106.04,-447.44 101.51,-446.21\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"101.55,-442.7 91.24,-445.13 100.82,-449.66 101.55,-442.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"119\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z2\\}->\\{z3\\} -->\n",
"<g id=\"edge14\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M70.7229,-434.7868C74.7704,-424.2121 81.0778,-411.2043 90,-402 98.8615,-392.8583 110.5505,-385.5335 121.7332,-379.9399\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"123.3523,-383.0468 130.9344,-375.6466 120.3924,-376.7033 123.3523,-383.0468\"/>\n",
- "<text text-anchor=\"middle\" x=\"94\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M69.95,-434.59C74.22,-424.12 80.85,-411.11 90,-402 98.89,-393.14 110.49,-386.06 121.58,-380.64\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"123.06,-383.81 130.71,-376.48 120.16,-377.44 123.06,-383.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"93.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z2\\}->\\{z3\\} -->\n",
"<g id=\"edge30\" class=\"edge\">\n",
"<title>\\{z2\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M84.2697,-434.9735C97.8615,-422.2586 116.2459,-405.0603 131.2563,-391.0183\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"133.8433,-393.3909 138.755,-384.0034 129.0612,-388.279 133.8433,-393.3909\"/>\n",
- "<text text-anchor=\"middle\" x=\"122\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M83.02,-434.8C96.91,-422.24 115.92,-405.05 131.33,-391.12\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"133.94,-393.48 139.01,-384.18 129.24,-388.29 133.94,-393.48\"/>\n",
+ "<text text-anchor=\"middle\" x=\"120.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\} -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>\\{z0,z1,z2,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"311.5,-36 218.5,-36 218.5,0 311.5,0 311.5,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"265\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"309,-36 217,-36 217,0 309,0 309,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"263\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2,z3}</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge31\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M268.2311,-36.3327C276.1454,-81.2381 296.5441,-196.9783 306.0223,-250.7568\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"302.5827,-251.4063 307.7654,-260.647 309.4765,-250.1912 302.5827,-251.4063\"/>\n",
- "<text text-anchor=\"middle\" x=\"294\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M266.08,-36.32C273.9,-80.38 294.62,-197.01 304.11,-250.49\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"300.72,-251.37 305.91,-260.6 307.61,-250.15 300.72,-251.37\"/>\n",
+ "<text text-anchor=\"middle\" x=\"291.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M311.6737,-21.8315C321.988,-21.4715 329.5,-20.1943 329.5,-18 329.5,-16.6285 326.5656,-15.6153 321.8467,-14.9604\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"321.9152,-11.4553 311.6737,-14.1685 321.3718,-18.4341 321.9152,-11.4553\"/>\n",
- "<text text-anchor=\"middle\" x=\"340\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M309.02,-21.84C319.41,-21.5 327,-20.21 327,-18 327,-16.62 324.03,-15.6 319.27,-14.94\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"319.26,-11.43 309.02,-14.16 318.73,-18.41 319.26,-11.43\"/>\n",
+ "<text text-anchor=\"middle\" x=\"337\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge15\" class=\"edge\">\n",
"<title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.6325,-25.7669C332.4024,-26.4542 350.5,-23.8652 350.5,-18 350.5,-13.1429 338.0889,-10.5326 322.0269,-10.1691\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"321.6107,-6.6715 311.6325,-10.2331 321.6539,-13.6714 321.6107,-6.6715\"/>\n",
- "<text text-anchor=\"middle\" x=\"354.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M309.37,-25.78C329.56,-26.42 347,-23.82 347,-18 347,-13.18 335.04,-10.57 319.46,-10.18\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"319.36,-6.68 309.37,-10.22 319.39,-13.68 319.36,-6.68\"/>\n",
+ "<text text-anchor=\"middle\" x=\"350.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\} -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>\\{z1,z2\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"267,-558 207,-558 207,-522 267,-522 267,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"237\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"263.5,-558 204.5,-558 204.5,-522 263.5,-522 263.5,-558\"/>\n",
+ "<text text-anchor=\"middle\" x=\"234\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2}</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge17\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M212.1632,-521.6958C206.9289,-516.5786 202.0676,-510.5913 199,-504 195.7581,-497.0343 194.3667,-488.9431 193.9447,-481.2858\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"197.4445,-481.239 193.8872,-471.2593 190.4447,-481.2792 197.4445,-481.239\"/>\n",
- "<text text-anchor=\"middle\" x=\"203\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M211.3,-521.81C206.06,-516.67 201.12,-510.63 198,-504 194.78,-497.14 193.28,-489.17 192.71,-481.64\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"196.21,-481.34 192.44,-471.44 189.21,-481.52 196.21,-481.34\"/>\n",
+ "<text text-anchor=\"middle\" x=\"201.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge33\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M228.5048,-521.9735C222.8425,-509.9585 215.2936,-493.9401 208.8959,-480.3646\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"211.9134,-478.5571 204.4843,-471.0034 205.5813,-481.5413 211.9134,-478.5571\"/>\n",
- "<text text-anchor=\"middle\" x=\"223\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M225.91,-521.8C220.32,-509.93 212.79,-493.93 206.45,-480.45\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"209.51,-478.73 202.08,-471.18 203.17,-481.71 209.51,-478.73\"/>\n",
+ "<text text-anchor=\"middle\" x=\"220.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1,z2\\}->\\{z1,z2\\} -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>\\{z1,z2\\}->\\{z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M267.4673,-547.8731C277.248,-547.7923 285,-545.168 285,-540 285,-536.8508 282.1214,-534.6461 277.6593,-533.3859\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"277.8209,-529.8794 267.4673,-532.1269 276.9627,-536.8266 277.8209,-529.8794\"/>\n",
- "<text text-anchor=\"middle\" x=\"295.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.69,-547.88C273.58,-547.88 281.5,-545.25 281.5,-540 281.5,-536.72 278.41,-534.46 273.67,-533.23\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"274.01,-529.75 263.69,-532.12 273.24,-536.71 274.01,-529.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"291.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\} -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>\\{z0,z1,z2\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-384 272.5,-384 272.5,-348 349.5,-348 349.5,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"311\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"347,-384 271,-384 271,-348 347,-348 347,-384\"/>\n",
+ "<text text-anchor=\"middle\" x=\"309\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2}</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge35\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M311,-347.9735C311,-336.1918 311,-320.5607 311,-307.1581\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"314.5001,-307.0033 311,-297.0034 307.5001,-307.0034 314.5001,-307.0033\"/>\n",
- "<text text-anchor=\"middle\" x=\"315\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M309,-347.8C309,-336.16 309,-320.55 309,-307.24\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"312.5,-307.18 309,-297.18 305.5,-307.18 312.5,-307.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"312.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge19\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M276.834,-347.9744C253.5781,-332.9816 227,-309.2335 227,-279 227,-279 227,-279 227,-105 227,-83.4445 236.9173,-61.2074 246.6192,-44.6107\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"249.6526,-46.3596 251.9226,-36.0108 243.6945,-42.6853 249.6526,-46.3596\"/>\n",
- "<text text-anchor=\"middle\" x=\"231\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M275.32,-347.88C251.95,-333.36 225,-310.08 225,-280 225,-280 225,-280 225,-104 225,-82.92 234.86,-61.26 244.54,-45.08\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"247.74,-46.56 250.13,-36.23 241.83,-42.81 247.74,-46.56\"/>\n",
+ "<text text-anchor=\"middle\" x=\"228.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2\\} -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>\\{z0,z1,z2\\}->\\{z0,z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-373.8058C359.7662,-373.3597 367.5,-370.7578 367.5,-366 367.5,-363.0264 364.479,-360.8949 359.7203,-359.6055\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-356.1027 349.5552,-358.1942 358.9788,-363.0362 359.9415,-356.1027\"/>\n",
- "<text text-anchor=\"middle\" x=\"378\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.21,-373.81C357.33,-373.36 365,-370.76 365,-366 365,-363.03 362.01,-360.89 357.29,-359.61\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"357.6,-356.12 347.21,-358.19 356.63,-363.05 357.6,-356.12\"/>\n",
+ "<text text-anchor=\"middle\" x=\"375\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\} -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>\\{z0,z2\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"467,-297 407,-297 407,-261 467,-261 467,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"437\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"462.5,-297 403.5,-297 403.5,-261 462.5,-261 462.5,-297\"/>\n",
+ "<text text-anchor=\"middle\" x=\"433\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2}</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\}->\\{z0,z2\\} -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M467.4673,-286.8731C477.248,-286.7923 485,-284.168 485,-279 485,-275.8508 482.1214,-273.6461 477.6593,-272.3859\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"477.8209,-268.8794 467.4673,-271.1269 476.9627,-275.8266 477.8209,-268.8794\"/>\n",
- "<text text-anchor=\"middle\" x=\"495.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M462.69,-286.88C472.58,-286.88 480.5,-284.25 480.5,-279 480.5,-275.72 477.41,-273.46 472.67,-272.23\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"473.01,-268.75 462.69,-271.12 472.24,-275.71 473.01,-268.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"490.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge22\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M428.3795,-260.7078C413.9466,-230.0818 384.8161,-168.2682 367.9228,-132.4216\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"370.934,-130.6009 363.505,-123.0471 364.6019,-133.585 370.934,-130.6009\"/>\n",
- "<text text-anchor=\"middle\" x=\"408\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M424.94,-260.88C410.75,-230.74 381.22,-168.04 364.41,-132.35\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"367.46,-130.61 360.03,-123.05 361.12,-133.59 367.46,-130.61\"/>\n",
+ "<text text-anchor=\"middle\" x=\"403.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z2\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge38\" class=\"edge\">\n",
"<title>\\{z0,z2\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M441.144,-260.9735C443.8793,-249.0751 447.5171,-233.2508 450.6182,-219.7606\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"454.0318,-220.5333 452.8613,-210.0034 447.2098,-218.965 454.0318,-220.5333\"/>\n",
- "<text text-anchor=\"middle\" x=\"452\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M436.84,-260.8C439.45,-249.16 442.94,-233.55 445.91,-220.24\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"449.39,-220.7 448.16,-210.18 442.56,-219.17 449.39,-220.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"446.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0\\} -->\n",
"<g id=\"node9\" class=\"node\">\n",
"<title>\\{z0\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"461,-558 407,-558 407,-522 461,-522 461,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"434\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"457,-558 403,-558 403,-522 457,-522 457,-558\"/>\n",
+ "<text text-anchor=\"middle\" x=\"430\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0}</text>\n",
"</g>\n",
"<!-- \\{z0\\}->\\{z0\\} -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0\\}</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M461.2408,-543.9337C471.0239,-544.0182 479,-542.707 479,-540 479,-538.3504 476.0382,-537.2191 471.5105,-536.6062\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"471.4107,-533.0962 461.2408,-536.0663 471.0432,-540.0865 471.4107,-533.0962\"/>\n",
- "<text text-anchor=\"middle\" x=\"491.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">start</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M457.24,-543.93C467.02,-544.02 475,-542.71 475,-540 475,-538.35 472.04,-537.22 467.51,-536.61\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"467.41,-533.1 457.24,-536.07 467.04,-540.09 467.41,-533.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"487\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">start</text>\n",
"</g>\n",
"<!-- \\{z0\\}->\\{z0\\} -->\n",
"<g id=\"edge40\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M461.36,-546.9863C482.1371,-549.3424 504,-547.0137 504,-540 504,-534.137 488.7224,-531.5478 471.5725,-532.2324\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"471.0638,-528.761 461.36,-533.0137 471.5979,-535.7406 471.0638,-528.761\"/>\n",
- "<text text-anchor=\"middle\" x=\"508\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M457.1,-546.99C477.58,-549.34 499,-547.01 499,-540 499,-534.14 484.03,-531.55 467.16,-532.23\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"466.8,-528.75 457.1,-533.01 467.34,-535.73 466.8,-528.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"502.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\} -->\n",
"<g id=\"node15\" class=\"node\">\n",
"<title>\\{z0,z1\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"464,-471 404,-471 404,-435 464,-435 464,-471\"/>\n",
- "<text text-anchor=\"middle\" x=\"434\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"459.5,-471 400.5,-471 400.5,-435 459.5,-435 459.5,-471\"/>\n",
+ "<text text-anchor=\"middle\" x=\"430\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1}</text>\n",
"</g>\n",
"<!-- \\{z0\\}->\\{z0,z1\\} -->\n",
"<g id=\"edge24\" class=\"edge\">\n",
"<title>\\{z0\\}->\\{z0,z1\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M434,-521.9735C434,-510.1918 434,-494.5607 434,-481.1581\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"437.5001,-481.0033 434,-471.0034 430.5001,-481.0034 437.5001,-481.0033\"/>\n",
- "<text text-anchor=\"middle\" x=\"438\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M430,-521.8C430,-510.16 430,-494.55 430,-481.24\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"433.5,-481.18 430,-471.18 426.5,-481.18 433.5,-481.18\"/>\n",
+ "<text text-anchor=\"middle\" x=\"433.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z3\\}->\\{z3\\} -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>\\{z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.2408,-369.9337C195.0239,-370.0182 203,-368.707 203,-366 203,-364.3504 200.0382,-363.2191 195.5105,-362.6062\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"195.4107,-359.0962 185.2408,-362.0663 195.0432,-366.0865 195.4107,-359.0962\"/>\n",
- "<text text-anchor=\"middle\" x=\"207\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.24,-369.93C195.02,-370.02 203,-368.71 203,-366 203,-364.35 200.04,-363.22 195.51,-362.61\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"195.41,-359.1 185.24,-362.07 195.04,-366.09 195.41,-359.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"206.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z3\\}->\\{z3\\} -->\n",
"<g id=\"edge26\" class=\"edge\">\n",
"<title>\\{z3\\}->\\{z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M185.1975,-373.1809C203.3402,-375.2022 221,-372.8086 221,-366 221,-360.468 209.3418,-357.8506 195.2386,-358.1477\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"194.9417,-354.6597 185.1975,-358.8191 195.4088,-361.6441 194.9417,-354.6597\"/>\n",
- "<text text-anchor=\"middle\" x=\"225\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M185.2,-373.18C203.34,-375.2 221,-372.81 221,-366 221,-360.47 209.34,-357.85 195.24,-358.15\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"194.94,-354.66 185.2,-358.82 195.41,-361.64 194.94,-354.66\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\}->\\{z0,z2,z3\\} -->\n",
"<g id=\"edge34\" class=\"edge\">\n",
"<title>\\{z0,z1,z3\\}->\\{z0,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M353.1903,-123.2704C350.1723,-150.0824 343.0098,-201.4126 329,-243 328.0589,-245.7937 326.9391,-248.6443 325.7251,-251.4571\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"322.4489,-250.1992 321.3575,-260.7377 328.7826,-253.18 322.4489,-250.1992\"/>\n",
- "<text text-anchor=\"middle\" x=\"350\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M350.49,-123.28C347.83,-149.67 341.17,-201.34 327,-243 326,-245.95 324.78,-248.95 323.46,-251.9\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"320.26,-250.48 319.02,-261 326.55,-253.55 320.26,-250.48\"/>\n",
+ "<text text-anchor=\"middle\" x=\"347.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
"<g id=\"edge18\" class=\"edge\">\n",
"<title>\\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M336.3519,-86.9735C323.1985,-74.2586 305.4072,-57.0603 290.881,-43.0183\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"293.2467,-40.4371 283.6242,-36.0034 288.3815,-45.4701 293.2467,-40.4371\"/>\n",
- "<text text-anchor=\"middle\" x=\"320\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M333.99,-86.8C320.84,-74.24 302.84,-57.05 288.26,-43.12\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"290.63,-40.55 280.98,-36.18 285.8,-45.61 290.63,-40.55\"/>\n",
+ "<text text-anchor=\"middle\" x=\"316.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z3\\} -->\n",
"<g id=\"node12\" class=\"node\">\n",
"<title>\\{z1,z3\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"384,-558 324,-558 324,-522 384,-522 384,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"354\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z3}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"378.5,-558 319.5,-558 319.5,-522 378.5,-522 378.5,-558\"/>\n",
+ "<text text-anchor=\"middle\" x=\"349\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z3}</text>\n",
"</g>\n",
"<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge16\" class=\"edge\">\n",
"<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M323.9095,-523.4312C298.7311,-509.5671 262.6249,-489.6859 235.1903,-474.5795\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"236.6952,-471.4126 226.2471,-469.6551 233.3187,-477.5445 236.6952,-471.4126\"/>\n",
- "<text text-anchor=\"middle\" x=\"289\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M319.48,-522.81C294.78,-509.27 259.36,-489.84 232.45,-475.08\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"234.12,-472.01 223.67,-470.27 230.76,-478.15 234.12,-472.01\"/>\n",
+ "<text text-anchor=\"middle\" x=\"284.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
"<g id=\"edge32\" class=\"edge\">\n",
"<title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M337.4415,-521.9971C326.7521,-511.2333 312.0684,-497.9537 297,-489 278.0574,-477.7442 255.0393,-469.2008 235.7642,-463.2678\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"236.649,-459.8798 226.0671,-460.4027 234.6655,-466.5929 236.649,-459.8798\"/>\n",
- "<text text-anchor=\"middle\" x=\"322\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M332.86,-521.85C322.11,-511.22 307.21,-497.94 292,-489 273.78,-478.29 251.75,-470.06 233.2,-464.28\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"234.15,-460.91 223.57,-461.4 232.15,-467.62 234.15,-460.91\"/>\n",
+ "<text text-anchor=\"middle\" x=\"316.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z1\\} -->\n",
"<g id=\"node13\" class=\"node\">\n",
"<title>\\{z1\\}</title>\n",
"<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-558 0,-558 0,-522 54,-522 54,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1}</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{z1}</text>\n",
"</g>\n",
"<!-- \\{z1\\}->\\{z2\\} -->\n",
"<g id=\"edge20\" class=\"edge\">\n",
"<title>\\{z1\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.0007,-521.8438C27.6026,-511.7804 29.3707,-499.2653 34,-489 35.4686,-485.7435 37.3276,-482.5584 39.4029,-479.5137\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.3516,-481.4212 45.6797,-471.3626 36.8054,-477.1503 42.3516,-481.4212\"/>\n",
- "<text text-anchor=\"middle\" x=\"38\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.04,-521.67C27.64,-511.73 29.39,-499.23 34,-489 35.54,-485.59 37.52,-482.26 39.72,-479.09\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.53,-481.17 45.94,-471.14 37.02,-476.86 42.53,-481.17\"/>\n",
+ "<text text-anchor=\"middle\" x=\"37.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z1\\}->\\{z2\\} -->\n",
"<g id=\"edge36\" class=\"edge\">\n",
"<title>\\{z1\\}->\\{z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M34.8736,-521.9735C40.1216,-509.9585 47.1181,-493.9401 53.0477,-480.3646\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"56.3411,-481.5683 57.1365,-471.0034 49.9263,-478.7664 56.3411,-481.5683\"/>\n",
- "<text text-anchor=\"middle\" x=\"53\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M34.49,-521.8C39.65,-509.93 46.62,-493.93 52.49,-480.45\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"55.74,-481.74 56.52,-471.18 49.32,-478.95 55.74,-481.74\"/>\n",
+ "<text text-anchor=\"middle\" x=\"51.5\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\}->\\{z0,z1,z3\\} -->\n",
"<g id=\"edge21\" class=\"edge\">\n",
"<title>\\{z0,z3\\}->\\{z0,z1,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M444.3424,-173.6871C436.6232,-163.3329 426.1232,-150.5829 415,-141 409.8677,-136.5784 404.1243,-132.3749 398.2795,-128.5043\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"400.0264,-125.468 389.7031,-123.0849 396.2871,-131.3856 400.0264,-125.468\"/>\n",
- "<text text-anchor=\"middle\" x=\"433\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M440.37,-173.97C432.79,-163.65 422.24,-150.66 411,-141 405.84,-136.57 400.05,-132.37 394.16,-128.53\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"395.87,-125.47 385.53,-123.16 392.17,-131.41 395.87,-125.47\"/>\n",
+ "<text text-anchor=\"middle\" x=\"427.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z3\\}->\\{z0,z3\\} -->\n",
"<g id=\"edge37\" class=\"edge\">\n",
"<title>\\{z0,z3\\}->\\{z0,z3\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M487.4673,-199.8731C497.248,-199.7923 505,-197.168 505,-192 505,-188.8508 502.1214,-186.6461 497.6593,-185.3859\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"497.8209,-181.8794 487.4673,-184.1269 496.9627,-188.8266 497.8209,-181.8794\"/>\n",
- "<text text-anchor=\"middle\" x=\"509\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M481.69,-199.88C491.58,-199.88 499.5,-197.25 499.5,-192 499.5,-188.72 496.41,-186.46 491.67,-185.23\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"492.01,-181.75 481.69,-184.12 491.24,-188.71 492.01,-181.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"503\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\}->\\{z0,z1,z2\\} -->\n",
"<g id=\"edge23\" class=\"edge\">\n",
"<title>\\{z0,z1\\}->\\{z0,z1,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M408.5143,-434.9735C390.0432,-421.9086 364.8799,-404.1102 344.7418,-389.8662\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"346.6383,-386.9206 336.453,-384.0034 342.5961,-392.6355 346.6383,-386.9206\"/>\n",
- "<text text-anchor=\"middle\" x=\"383\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M405.51,-434.8C387.15,-421.9 361.81,-404.1 341.71,-389.98\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"343.64,-387.06 333.45,-384.18 339.62,-392.79 343.64,-387.06\"/>\n",
+ "<text text-anchor=\"middle\" x=\"379.5\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{z0,z1\\}->\\{z0,z2\\} -->\n",
"<g id=\"edge39\" class=\"edge\">\n",
"<title>\\{z0,z1\\}->\\{z0,z2\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M434.3154,-434.7078C434.8389,-404.3436 435.891,-343.3226 436.5113,-307.3464\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"440.0158,-307.106 436.6888,-297.0471 433.0169,-306.9852 440.0158,-307.106\"/>\n",
- "<text text-anchor=\"middle\" x=\"439\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M430.3,-434.88C430.82,-405 431.9,-343.11 432.52,-307.27\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"436.03,-307.11 432.7,-297.05 429.03,-306.99 436.03,-307.11\"/>\n",
+ "<text text-anchor=\"middle\" x=\"434.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- \\{\\} -->\n",
"<g id=\"node16\" class=\"node\">\n",
"<title>\\{\\}</title>\n",
- "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"602,-558 548,-558 548,-522 602,-522 602,-558\"/>\n",
- "<text text-anchor=\"middle\" x=\"575\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{}</text>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"596,-558 542,-558 542,-522 596,-522 596,-558\"/>\n",
+ "<text text-anchor=\"middle\" x=\"569\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">{}</text>\n",
"</g>\n",
"<!-- \\{\\}->\\{\\} -->\n",
"<g id=\"edge25\" class=\"edge\">\n",
"<title>\\{\\}->\\{\\}</title>\n",
- "<path fill=\"none\" stroke=\"#473c8b\" d=\"M602.2408,-543.9337C612.0239,-544.0182 620,-542.707 620,-540 620,-538.3504 617.0382,-537.2191 612.5105,-536.6062\"/>\n",
- "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"612.4107,-533.0962 602.2408,-536.0663 612.0432,-540.0865 612.4107,-533.0962\"/>\n",
- "<text text-anchor=\"middle\" x=\"624\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M596.24,-543.93C606.02,-544.02 614,-542.71 614,-540 614,-538.35 611.04,-537.22 606.51,-536.61\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"606.41,-533.1 596.24,-536.07 606.04,-540.09 606.41,-533.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"617.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- \\{\\}->\\{\\} -->\n",
"<g id=\"edge41\" class=\"edge\">\n",
"<title>\\{\\}->\\{\\}</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M602.1975,-547.1809C620.3402,-549.2022 638,-546.8086 638,-540 638,-534.468 626.3418,-531.8506 612.2386,-532.1477\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"611.9417,-528.6597 602.1975,-532.8191 612.4088,-535.6441 611.9417,-528.6597\"/>\n",
- "<text text-anchor=\"middle\" x=\"642\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M596.2,-547.18C614.34,-549.2 632,-546.81 632,-540 632,-534.47 620.34,-531.85 606.24,-532.15\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"605.94,-528.66 596.2,-532.82 606.41,-535.64 605.94,-528.66\"/>\n",
+ "<text text-anchor=\"middle\" x=\"635.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"</g>\n",
- "</svg>"
+ "</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & δs(x, [0])=y})]>"
+ "<Dot visualization: expr_as_graph [(\"0\",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},\n",
+ " \"1\",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},\n",
+ " \"start\", {x,y|x=y & x={z0}},\n",
+ " \"end\", {x,y|x=y & x∩F ≠ ∅})]>"
]
},
"execution_count": 15,
@@ -1083,13 +1087,6 @@
" \"start\", {x,y|x=y & x={z0}},\n",
" \"end\", {x,y|x=y & x∩F ≠ ∅})"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/models/NQueens_Puzzle.ipynb b/notebooks/models/NQueens_Puzzle.ipynb
index 7ffe1c8..7af4b65 100644
--- a/notebooks/models/NQueens_Puzzle.ipynb
+++ b/notebooks/models/NQueens_Puzzle.ipynb
@@ -65,7 +65,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
@@ -85,7 +85,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
@@ -1067,13 +1067,6 @@
"source": [
":show"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/models/scheduler.ipynb b/notebooks/models/scheduler.ipynb
index 7fabf4a..ef4123c 100644
--- a/notebooks/models/scheduler.ipynb
+++ b/notebooks/models/scheduler.ipynb
@@ -96,7 +96,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 5,
@@ -224,7 +224,7 @@
"text/markdown": [
"|waiting|\n",
"|---|\n",
- "|$\\mathit{PID3}$|\n"
+ "|PID3|\n"
],
"text/plain": [
"waiting\n",
@@ -316,8 +316,8 @@
"text/markdown": [
"|waiting|\n",
"|---|\n",
- "|$\\mathit{PID2}$|\n",
- "|$\\mathit{PID3}$|\n"
+ "|PID2|\n",
+ "|PID3|\n"
],
"text/plain": [
"waiting\n",
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 15c0a4c..e147d18 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -261,11 +261,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $setup_constants with additional predicate produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $setup_constants with additional predicate produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate\u001b[0m"
]
}
],
@@ -375,7 +375,9 @@
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
"\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
+ "\u001b[1m\u001b[30mINVARIANT value : min_value..max_value\u001b[0m",
+ "\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mvalue :: min_value..max_value\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[30mOPERATIONS\u001b[0m"
]
}
],
@@ -563,11 +565,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $setup_constants with additional predicate produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $setup_constants with additional predicate produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m"
]
}
],
@@ -581,11 +583,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $initialise_machine with additional predicate produced errors: Machine is already initialised, cannot execute INITIALISATION",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $initialise_machine with additional predicate produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m"
]
}
],
@@ -599,11 +601,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation nope with additional predicate produced errors: Unknown Operation nope",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation nope with additional predicate produced errors: Unknown Operation nope\u001b[0m"
]
}
],
@@ -617,11 +619,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation add with additional predicate produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation add with additional predicate produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)\u001b[0m"
]
}
],
@@ -660,11 +662,11 @@
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root",
+ "ename": "ExecuteOperationException",
+ "evalue": "Executing operation $setup_constants with additional predicate produced errors: Could not execute operation SETUP_CONSTANTS in state root",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root\u001b[0m"
+ "\u001b[1m\u001b[31mde.prob.animator.command.ExecuteOperationException: Executing operation $setup_constants with additional predicate produced errors: Could not execute operation SETUP_CONSTANTS in state root\u001b[0m"
]
}
],
@@ -684,7 +686,9 @@
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
"\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
+ "\u001b[1m\u001b[30mINVARIANT z : MININT..MAXINT\u001b[0m",
+ "\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mz :: {0, 1}\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[30mEND\u001b[0m"
]
}
],
diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb
index 66fd9bc..07c381b 100644
--- a/notebooks/tests/dot.ipynb
+++ b/notebooks/tests/dot.ipynb
@@ -95,19 +95,19 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: visited_states Pages: 1 -->\n",
- "<svg width=\"97pt\" height=\"50pt\"\n",
- " viewBox=\"0.00 0.00 96.64 50.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<svg width=\"94pt\" height=\"50pt\"\n",
+ " viewBox=\"0.00 0.00 94.18 50.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 46)\">\n",
"<title>visited_states</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-46 92.6445,-46 92.6445,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-46 90.18,-46 90.18,4 -4,4\"/>\n",
"<!-- root -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>root</title>\n",
- "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"44.3223,0 88.4675,-31.5 .177,-31.5 44.3223,0\"/>\n",
- "<text text-anchor=\"middle\" x=\"44.3223\" y=\"-17.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"43.09,0 86.27,-31.5 -0.09,-31.5 43.09,0\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43.09\" y=\"-17.9\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -158,32 +158,32 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: visited_states Pages: 1 -->\n",
- "<svg width=\"144pt\" height=\"215pt\"\n",
- " viewBox=\"0.00 0.00 144.32 215.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<svg width=\"143pt\" height=\"215pt\"\n",
+ " viewBox=\"0.00 0.00 143.09 215.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 211)\">\n",
"<title>visited_states</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-211 140.3223,-211 140.3223,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-211 139.09,-211 139.09,4 -4,4\"/>\n",
"<!-- root -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>root</title>\n",
- "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"44.3223,-165 88.4675,-196.5 .177,-196.5 44.3223,-165\"/>\n",
- "<text text-anchor=\"middle\" x=\"44.3223\" y=\"-182.9\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">root</text>\n",
+ "<polygon fill=\"none\" stroke=\"#f4e3c1\" stroke-width=\"2\" points=\"43.09,-165 86.27,-196.5 -0.09,-196.5 43.09,-165\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43.09\" y=\"-182.9\" font-family=\"Times,serif\" font-size=\"12.00\">root</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
- "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"71.3223,-14.5442 71.3223,-29.4558 55.506,-40 33.1385,-40 17.3223,-29.4558 17.3223,-14.5442 33.1385,-4 55.506,-4 71.3223,-14.5442\"/>\n",
- "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"75.3223,-12.4034 75.3223,-31.5966 56.7171,-44 31.9274,-44 13.3223,-31.5966 13.3223,-12.4034 31.9274,0 56.7171,0 75.3223,-12.4034\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"70.09,-14.54 70.09,-29.46 54.27,-40 31.91,-40 16.09,-29.46 16.09,-14.54 31.91,-4 54.27,-4 70.09,-14.54\"/>\n",
+ "<polygon fill=\"none\" stroke=\"#99bf38\" stroke-width=\"2\" points=\"74.09,-12.4 74.09,-31.6 55.49,-44 30.7,-44 12.09,-31.6 12.09,-12.4 30.7,0 55.49,0 74.09,-12.4\"/>\n",
"</g>\n",
"<!-- root->0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>root->0</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" stroke-dasharray=\"1,5\" d=\"M44.3223,-164.8956C44.3223,-136.9146 44.3223,-87.2613 44.3223,-54.4833\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"47.8224,-54.0698 44.3223,-44.0699 40.8224,-54.0699 47.8224,-54.0698\"/>\n",
- "<text text-anchor=\"middle\" x=\"90.3223\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">INITIALISATION</text>\n",
+ "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M43.09,-164.81C43.09,-137.15 43.09,-87.19 43.09,-54.56\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"46.59,-54.22 43.09,-44.22 39.59,-54.22 46.59,-54.22\"/>\n",
+ "<text text-anchor=\"middle\" x=\"89.09\" y=\"-101.4\" font-family=\"Times,serif\" font-size=\"12.00\">INITIALISATION</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -212,20 +212,20 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"62pt\" height=\"46pt\"\n",
" viewBox=\"0.00 0.00 62.00 46.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 42)\">\n",
"<title>g</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-42 58,-42 58,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-42 58,-42 58,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
- "<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-38C42,-38 12,-38 12,-38 6,-38 0,-32 0,-26 0,-26 0,-12 0,-12 0,-6 6,0 12,0 12,0 42,0 42,0 48,0 54,-6 54,-12 54,-12 54,-26 54,-26 54,-32 48,-38 42,-38\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-22.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">⊤</text>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
+ "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M42,-38C42,-38 12,-38 12,-38 6,-38 0,-32 0,-26 0,-26 0,-12 0,-12 0,-6 6,0 12,0 12,0 42,0 42,0 48,0 54,-6 54,-12 54,-12 54,-26 54,-26 54,-32 48,-38 42,-38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-22.8\" font-family=\"Times,serif\" font-size=\"14.00\">⊤</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-7.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
@@ -254,58 +254,58 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
- "<svg width=\"326pt\" height=\"218pt\"\n",
- " viewBox=\"0.00 0.00 326.00 218.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<svg width=\"325pt\" height=\"218pt\"\n",
+ " viewBox=\"0.00 0.00 325.00 218.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 214)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-214 322,-214 322,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-214 321,-214 321,4 -4,4\"/>\n",
"<!-- 3 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>3</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-210 76,-210 76,-174 130,-174 130,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"103\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"129,-210 75,-210 75,-174 129,-174 129,-210\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</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\">1</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 3->1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M75.6408,-186.4668C58.8257,-181.5148 38.5455,-172.4004 28,-156 23.7372,-149.3705 22.3175,-141.1865 22.2793,-133.3301\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"25.7725,-133.5476 22.9019,-123.3491 18.786,-133.1117 25.7725,-133.5476\"/>\n",
- "<text text-anchor=\"middle\" x=\"96.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|->2),(2|->3),(3|->1)}</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M74.65,-185.62C58.14,-180.83 38.35,-171.99 28,-156 23.67,-149.31 22.32,-140.99 22.36,-133.07\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"25.85,-133.29 23.09,-123.06 18.87,-132.77 25.85,-133.29\"/>\n",
+ "<text text-anchor=\"middle\" x=\"96\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"130,-36 76,-36 76,0 130,0 130,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"103\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"129,-36 75,-36 75,0 129,0 129,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 1->2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1->2</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M22.9019,-86.6509C21.6193,-76.2846 21.8693,-63.5346 28,-54 36.5682,-40.6747 51.5628,-32.1592 65.9039,-26.7783\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"67.2605,-30.0155 75.6408,-23.5332 65.0472,-23.3746 67.2605,-30.0155\"/>\n",
- "<text text-anchor=\"middle\" x=\"96.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|->2),(2|->3),(3|->1)}</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M23.09,-86.94C21.7,-76.61 21.77,-63.62 28,-54 36.41,-41.01 51.05,-32.74 65.1,-27.52\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"66.25,-30.83 74.65,-24.38 64.06,-24.18 66.25,-30.83\"/>\n",
+ "<text text-anchor=\"middle\" x=\"96\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"<!-- 2->3 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->3</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M130.2715,-26.586C143.2238,-32.1915 157.4858,-40.9478 165,-54 187.6182,-93.2878 187.6182,-116.7122 165,-156 159.2469,-165.9931 149.5384,-173.468 139.4907,-178.9387\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"137.7391,-175.8983 130.2715,-183.414 140.796,-182.1956 137.7391,-175.8983\"/>\n",
- "<text text-anchor=\"middle\" x=\"249.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(1|->2),(2|->3),(3|->1)}</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.25,-27.16C142.2,-32.56 156.46,-41.08 164,-54 186.86,-93.15 186.86,-116.85 164,-156 158.23,-165.89 148.51,-173.2 138.47,-178.51\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"136.81,-175.42 129.25,-182.84 139.79,-181.76 136.81,-175.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"249\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(1|->2),(2|->3),(3|->1)}</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [{(1,2),(2,3),(3,1)}]>"
+ "<Dot visualization: expr_as_graph [{1|->2, 2|->3, 3|->1}]>"
]
},
"execution_count": 6,
@@ -328,133 +328,133 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"220pt\" height=\"392pt\"\n",
- " viewBox=\"0.00 0.00 220.34 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ " viewBox=\"0.00 0.00 220.11 392.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 388)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-388 216.3366,-388 216.3366,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-388 216.11,-388 216.11,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"126.3366,-297 72.3366,-297 72.3366,-261 126.3366,-261 126.3366,-297\"/>\n",
- "<text text-anchor=\"middle\" x=\"99.3366\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"126.11,-297 72.11,-297 72.11,-261 126.11,-261 126.11,-297\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99.11\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>2</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"60.3366,-123 6.3366,-123 6.3366,-87 60.3366,-87 60.3366,-123\"/>\n",
- "<text text-anchor=\"middle\" x=\"33.3366\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"60.11,-123 6.11,-123 6.11,-87 60.11,-87 60.11,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"33.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M79.0579,-260.9061C66.1479,-248.0804 50.3898,-229.7049 42.3366,-210 32.3296,-185.5146 30.755,-155.197 31.28,-133.4438\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"34.7864,-133.3549 31.6954,-123.221 27.7922,-133.0707 34.7864,-133.3549\"/>\n",
- "<text text-anchor=\"middle\" x=\"53.3366\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M79.4,-260.77C66.39,-248.14 50.29,-229.79 42.11,-210 31.98,-185.5 30.49,-155.04 31.07,-133.43\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"34.57,-133.45 31.51,-123.31 27.58,-133.15 34.57,-133.45\"/>\n",
+ "<text text-anchor=\"middle\" x=\"53.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M72.3052,-265.4238C52.6988,-253.802 27.9955,-234.9838 18.3366,-210 8.649,-184.9421 14.8751,-154.3426 22.0229,-132.6563\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"25.3751,-133.6757 25.4287,-123.081 18.7798,-131.3298 25.3751,-133.6757\"/>\n",
- "<text text-anchor=\"middle\" x=\"23.8366\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M72.04,-264.74C52.42,-253.35 27.71,-234.83 18.11,-210 8.4,-184.88 14.87,-154.15 22.1,-132.63\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"25.41,-133.75 25.52,-123.16 18.83,-131.37 25.41,-133.75\"/>\n",
+ "<text text-anchor=\"middle\" x=\"23.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"131.3366,-36 77.3366,-36 77.3366,0 131.3366,0 131.3366,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"104.3366\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"131.11,-36 77.11,-36 77.11,0 131.11,0 131.11,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"104.11\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 4->1 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M112.2011,-260.991C120.9171,-247.6323 131.6672,-228.5883 136.3366,-210 150.7854,-152.4801 130.3844,-83.5902 116.1253,-45.9526\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"119.2103,-44.2325 112.3004,-36.201 112.6936,-46.7886 119.2103,-44.2325\"/>\n",
- "<text text-anchor=\"middle\" x=\"145.8366\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.6,-260.84C120.38,-247.66 131.37,-228.63 136.11,-210 150.81,-152.22 129.79,-82.84 115.48,-45.66\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"118.61,-44.06 111.66,-36.06 112.11,-46.64 118.61,-44.06\"/>\n",
+ "<text text-anchor=\"middle\" x=\"145.61\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"127.3366,-210 73.3366,-210 73.3366,-174 127.3366,-174 127.3366,-210\"/>\n",
- "<text text-anchor=\"middle\" x=\"100.3366\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"127.11,-210 73.11,-210 73.11,-174 127.11,-174 127.11,-210\"/>\n",
+ "<text text-anchor=\"middle\" x=\"100.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 4->3 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M99.5438,-260.9735C99.6792,-249.1918 99.8589,-233.5607 100.0129,-220.1581\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"103.5144,-220.043 100.1296,-210.0034 96.5148,-219.9624 103.5144,-220.043\"/>\n",
- "<text text-anchor=\"middle\" x=\"104.8366\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M99.31,-260.8C99.45,-249.16 99.63,-233.55 99.79,-220.24\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"103.29,-220.22 99.91,-210.18 96.29,-220.13 103.29,-220.22\"/>\n",
+ "<text text-anchor=\"middle\" x=\"104.61\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M44.556,-86.9526C51.0742,-76.9232 59.6881,-64.4059 68.3366,-54 71.2761,-50.4631 74.5079,-46.8768 77.7917,-43.4073\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"80.4832,-45.6608 84.9702,-36.063 75.4773,-40.7679 80.4832,-45.6608\"/>\n",
- "<text text-anchor=\"middle\" x=\"79.3366\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M44.02,-86.75C50.57,-76.83 59.32,-64.33 68.11,-54 71.11,-50.47 74.42,-46.89 77.78,-43.45\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.48,-45.7 85.11,-36.17 75.55,-40.73 80.48,-45.7\"/>\n",
+ "<text text-anchor=\"middle\" x=\"79.11\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M32.4527,-86.5835C32.8248,-76.1947 34.8248,-63.4447 41.3366,-54 47.9062,-44.4715 57.8746,-37.1455 67.9562,-31.6684\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"69.722,-34.7005 77.1524,-27.1481 66.634,-28.4184 69.722,-34.7005\"/>\n",
- "<text text-anchor=\"middle\" x=\"46.8366\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M32.23,-86.86C32.53,-76.5 34.45,-63.5 41.11,-54 47.7,-44.59 57.68,-37.42 67.76,-32.1\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"69.43,-35.19 76.95,-27.73 66.42,-28.86 69.43,-35.19\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.61\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>5</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"173.3366,-384 119.3366,-384 119.3366,-348 173.3366,-348 173.3366,-384\"/>\n",
- "<text text-anchor=\"middle\" x=\"146.3366\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"173.11,-384 119.11,-384 119.11,-348 173.11,-348 173.11,-384\"/>\n",
+ "<text text-anchor=\"middle\" x=\"146.11\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
"</g>\n",
"<!-- 5->4 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>5->4</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M136.5981,-347.9735C130.0442,-335.8418 121.2854,-319.6287 113.9065,-305.9698\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"116.895,-304.138 109.0625,-297.0034 110.7362,-307.4652 116.895,-304.138\"/>\n",
- "<text text-anchor=\"middle\" x=\"130.8366\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M136.6,-347.8C129.97,-335.82 121.01,-319.62 113.52,-306.06\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"116.51,-304.23 108.61,-297.18 110.38,-307.62 116.51,-304.23\"/>\n",
+ "<text text-anchor=\"middle\" x=\"130.61\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>5->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M119.2819,-350.2868C87.3875,-330.0614 35.8753,-291.6572 13.3366,-243 -5.7213,-201.8576 -2.2595,-184.2556 11.3366,-141 12.2728,-138.0215 13.5071,-135.0369 14.9144,-132.1306\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"18.0667,-133.6627 19.8453,-123.2183 11.9416,-130.2739 18.0667,-133.6627\"/>\n",
- "<text text-anchor=\"middle\" x=\"18.8366\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M119.03,-349.49C87.1,-329.5 35.56,-291.48 13.11,-243 -5.95,-201.86 -1.96,-184.1 12.11,-141 13.09,-138 14.36,-134.98 15.8,-132.04\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"19,-133.5 20.79,-123.06 12.87,-130.1 19,-133.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"18.61\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>5->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M166.5042,-347.7161C182.2012,-331.4029 201.3366,-305.9826 201.3366,-279 201.3366,-279 201.3366,-279 201.3366,-105 201.3366,-71.059 168.0169,-47.0183 140.4342,-32.9318\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"141.8822,-29.7442 131.3565,-28.5363 138.8316,-36.0445 141.8822,-29.7442\"/>\n",
- "<text text-anchor=\"middle\" x=\"206.8366\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M165.65,-347.85C181.46,-332 201.11,-306.89 201.11,-280 201.11,-280 201.11,-280 201.11,-104 201.11,-70.4 167.79,-46.99 140.21,-33.37\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"141.67,-30.19 131.13,-29.12 138.7,-36.53 141.67,-30.19\"/>\n",
+ "<text text-anchor=\"middle\" x=\"206.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>5->3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M146.4197,-347.7778C146.0646,-326.5243 144.0504,-290.5339 135.3366,-261 131.0657,-246.5246 123.8015,-231.4639 116.9944,-219.1202\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"119.9349,-217.2116 111.9351,-210.2651 113.857,-220.6842 119.9349,-217.2116\"/>\n",
- "<text text-anchor=\"middle\" x=\"147.8366\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M146.21,-347.69C145.9,-326.73 143.94,-290.57 135.11,-261 130.75,-246.4 123.26,-231.23 116.33,-218.93\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"119.27,-217.01 111.2,-210.14 113.22,-220.54 119.27,-217.01\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.61\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->2 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M86.4541,-173.9735C76.9316,-161.6085 64.1439,-145.0036 53.5018,-131.1847\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"56.0758,-128.7907 47.2012,-123.0034 50.5298,-133.0618 56.0758,-128.7907\"/>\n",
- "<text text-anchor=\"middle\" x=\"75.8366\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M86.55,-173.8C76.92,-161.59 63.84,-144.99 53.03,-131.28\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"55.59,-128.86 46.65,-123.18 50.09,-133.2 55.59,-128.86\"/>\n",
+ "<text text-anchor=\"middle\" x=\"75.61\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->1 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M100.7571,-173.7078C101.4551,-143.3436 102.8579,-82.3226 103.6849,-46.3464\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"107.1908,-46.1249 103.9217,-36.0471 100.1927,-45.964 107.1908,-46.1249\"/>\n",
- "<text text-anchor=\"middle\" x=\"107.8366\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M100.51,-173.88C101.2,-144 102.64,-82.11 103.47,-46.27\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"106.98,-46.13 103.71,-36.05 99.98,-45.97 106.98,-46.13\"/>\n",
+ "<text text-anchor=\"middle\" x=\"107.61\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y},\"half\",{y,x|x:1..5 & y:1..5 & x+x=y})]>"
]
},
"execution_count": 7,
@@ -497,133 +497,133 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"243pt\" height=\"235pt\"\n",
" viewBox=\"0.00 0.00 243.39 234.72\" 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 230.7203)\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 230.72)\">\n",
"<title>state</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-230.7203 239.3858,-230.7203 239.3858,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-230.72 239.39,-230.72 239.39,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-36 112.1026,-36 112.1026,0 166.1026,0 166.1026,-36\"/>\n",
- "<text text-anchor=\"middle\" x=\"139.1026\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1,-36 112.1,-36 112.1,0 166.1,0 166.1,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.1\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>2</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"235.3858,-131.3602 181.3858,-131.3602 181.3858,-95.3602 235.3858,-95.3602 235.3858,-131.3602\"/>\n",
- "<text text-anchor=\"middle\" x=\"208.3858\" y=\"-109.6602\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"235.39,-131.36 181.39,-131.36 181.39,-95.36 235.39,-95.36 235.39,-131.36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"208.39\" y=\"-109.66\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M146.0962,-36.3277C154.5341,-50.7471 168.707,-70.9379 181.4659,-87.0605\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"178.9494,-89.5137 187.9712,-95.0686 184.3826,-85.1 178.9494,-89.5137\"/>\n",
- "<text text-anchor=\"middle\" x=\"152.781\" y=\"-65.4941\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M146.1,-36.33C154.53,-50.75 168.71,-70.94 181.47,-87.06\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"178.95,-89.51 187.97,-95.07 184.38,-85.1 178.95,-89.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"152.78\" y=\"-65.49\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 4->2 -->\n",
"<g id=\"edge8\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M159.4846,-36.2526C171.3905,-50.4825 185.9022,-70.3727 196.1137,-86.4179\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"193.373,-88.6448 201.577,-95.3489 199.3444,-84.992 193.373,-88.6448\"/>\n",
- "<text text-anchor=\"middle\" x=\"172.2992\" y=\"-65.1352\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M159.48,-36.25C171.39,-50.48 185.9,-70.37 196.11,-86.42\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"193.37,-88.64 201.58,-95.35 199.34,-84.99 193.37,-88.64\"/>\n",
+ "<text text-anchor=\"middle\" x=\"172.3\" y=\"-65.14\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>1</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-190.296 0,-190.296 0,-154.296 54,-154.296 54,-190.296\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-168.596\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-190.3 0,-190.3 0,-154.3 54,-154.3 54,-190.3\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-168.6\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 4->1 -->\n",
"<g id=\"edge9\" class=\"edge\">\n",
"<title>4->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M126.0236,-36.0017C106.3845,-63.0326 69.1556,-114.2737 46.3626,-145.6457\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"43.3895,-143.7832 40.3432,-153.9307 49.0526,-147.8978 43.3895,-143.7832\"/>\n",
- "<text text-anchor=\"middle\" x=\"80.6931\" y=\"-94.6237\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M126.02,-36C106.38,-63.03 69.16,-114.27 46.36,-145.65\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"43.39,-143.78 40.34,-153.93 49.05,-147.9 43.39,-143.78\"/>\n",
+ "<text text-anchor=\"middle\" x=\"80.69\" y=\"-94.62\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>3</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-72.4243 0,-72.4243 0,-36.4243 54,-36.4243 54,-72.4243\"/>\n",
- "<text text-anchor=\"middle\" x=\"27\" y=\"-50.7243\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-72.42 0,-72.42 0,-36.42 54,-36.42 54,-72.42\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-50.72\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 4->3 -->\n",
"<g id=\"edge7\" class=\"edge\">\n",
"<title>4->3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M111.9657,-26.8173C97.6137,-31.4806 79.779,-37.2754 64.1603,-42.3502\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"62.7045,-39.143 54.2756,-45.562 64.8677,-45.8004 62.7045,-39.143\"/>\n",
- "<text text-anchor=\"middle\" x=\"82.563\" y=\"-38.3838\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.97,-26.82C97.61,-31.48 79.78,-37.28 64.16,-42.35\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.7,-39.14 54.28,-45.56 64.87,-45.8 62.7,-39.14\"/>\n",
+ "<text text-anchor=\"middle\" x=\"82.56\" y=\"-38.38\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"#b22222\" d=\"M181.2766,-117.0448C149.9737,-124.8821 98.3616,-141.3877 63.5383,-154.5076\"/>\n",
- "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"62.2655,-151.2472 54.1924,-158.1083 64.7821,-157.7792 62.2655,-151.2472\"/>\n",
- "<text text-anchor=\"middle\" x=\"111.4074\" y=\"-139.5762\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">half</text>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.28,-117.04C149.97,-124.88 98.36,-141.39 63.54,-154.51\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"62.27,-151.25 54.19,-158.11 64.78,-157.78 62.27,-151.25\"/>\n",
+ "<text text-anchor=\"middle\" x=\"111.41\" y=\"-139.58\" font-family=\"Times,serif\" font-size=\"14.00\">half</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge12\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M181.2172,-127.5384C150.0376,-139.8543 98.7636,-156.6493 63.9685,-166.0402\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"62.974,-162.6824 54.1813,-168.5933 64.741,-169.4557 62.974,-162.6824\"/>\n",
- "<text text-anchor=\"middle\" x=\"128.0929\" y=\"-150.5893\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M181.22,-127.54C150.04,-139.85 98.76,-156.65 63.97,-166.04\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"62.97,-162.68 54.18,-168.59 64.74,-169.46 62.97,-162.68\"/>\n",
+ "<text text-anchor=\"middle\" x=\"128.09\" y=\"-150.59\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>5</title>\n",
- "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1026,-226.7203 112.1026,-226.7203 112.1026,-190.7203 166.1026,-190.7203 166.1026,-226.7203\"/>\n",
- "<text text-anchor=\"middle\" x=\"139.1026\" y=\"-205.0203\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">5</text>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"166.1,-226.72 112.1,-226.72 112.1,-190.72 166.1,-190.72 166.1,-226.72\"/>\n",
+ "<text text-anchor=\"middle\" x=\"139.1\" y=\"-205.02\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
"</g>\n",
"<!-- 5->4 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>5->4</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M139.1026,-190.4333C139.1026,-157.0404 139.1026,-85.9864 139.1026,-46.3026\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"142.6027,-46.2317 139.1026,-36.2317 135.6027,-46.2317 142.6027,-46.2317\"/>\n",
- "<text text-anchor=\"middle\" x=\"133.6026\" y=\"-122.1679\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M139.1,-190.43C139.1,-157.04 139.1,-85.99 139.1,-46.3\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"142.6,-46.23 139.1,-36.23 135.6,-46.23 142.6,-46.23\"/>\n",
+ "<text text-anchor=\"middle\" x=\"133.6\" y=\"-122.17\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>5->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M152.4611,-190.3339C162.879,-175.9949 177.4897,-155.885 189.1646,-139.8159\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"192.257,-141.5142 195.3033,-131.3667 186.5938,-137.3997 192.257,-141.5142\"/>\n",
- "<text text-anchor=\"middle\" x=\"165.3128\" y=\"-168.8749\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M152.46,-190.33C162.88,-175.99 177.49,-155.88 189.16,-139.82\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"192.26,-141.51 195.3,-131.37 186.59,-137.4 192.26,-141.51\"/>\n",
+ "<text text-anchor=\"middle\" x=\"165.31\" y=\"-168.87\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>5->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M111.9657,-199.903C97.6137,-195.2398 79.779,-189.4449 64.1603,-184.3701\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"64.8677,-180.9199 54.2756,-181.1584 62.7045,-187.5773 64.8677,-180.9199\"/>\n",
- "<text text-anchor=\"middle\" x=\"82.563\" y=\"-195.9366\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M111.97,-199.9C97.61,-195.24 79.78,-189.44 64.16,-184.37\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"64.87,-180.92 54.28,-181.16 62.7,-187.58 64.87,-180.92\"/>\n",
+ "<text text-anchor=\"middle\" x=\"82.56\" y=\"-195.94\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 5->3 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>5->3</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M126.0236,-190.7187C106.3845,-163.6878 69.1556,-112.4466 46.3626,-81.0746\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"49.0526,-78.8226 40.3432,-72.7896 43.3895,-82.9371 49.0526,-78.8226\"/>\n",
- "<text text-anchor=\"middle\" x=\"80.6931\" y=\"-139.6966\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M126.02,-190.72C106.38,-163.69 69.16,-112.45 46.36,-81.07\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"49.05,-78.82 40.34,-72.79 43.39,-82.94 49.05,-78.82\"/>\n",
+ "<text text-anchor=\"middle\" x=\"80.69\" y=\"-139.7\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->2 -->\n",
"<g id=\"edge10\" class=\"edge\">\n",
"<title>3->2</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M54.1553,-63.2476C85.368,-73.3892 136.7581,-90.0869 171.5567,-101.3937\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"170.7494,-104.8114 181.3415,-104.5729 172.9125,-98.154 170.7494,-104.8114\"/>\n",
- "<text text-anchor=\"middle\" x=\"107.356\" y=\"-86.1207\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M54.16,-63.25C85.37,-73.39 136.76,-90.09 171.56,-101.39\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"170.75,-104.81 181.34,-104.57 172.91,-98.15 170.75,-104.81\"/>\n",
+ "<text text-anchor=\"middle\" x=\"107.36\" y=\"-86.12\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"<!-- 3->1 -->\n",
"<g id=\"edge11\" class=\"edge\">\n",
"<title>3->1</title>\n",
- "<path fill=\"none\" stroke=\"#a0522d\" d=\"M27,-72.5835C27,-91.5634 27,-121.6099 27,-143.7637\"/>\n",
- "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"23.5001,-143.922 27,-153.922 30.5001,-143.9221 23.5001,-143.922\"/>\n",
- "<text text-anchor=\"middle\" x=\"21.5\" y=\"-111.9736\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">gt</text>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M27,-72.58C27,-91.56 27,-121.61 27,-143.76\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"23.5,-143.92 27,-153.92 30.5,-143.92 23.5,-143.92\"/>\n",
+ "<text text-anchor=\"middle\" x=\"21.5\" y=\"-111.97\" font-family=\"Times,serif\" font-size=\"14.00\">gt</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
- "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y})]>"
+ "<Dot visualization: expr_as_graph [(\"gt\",{x,y|x:1..5 & y:1..5 & x>y},\"half\",{y,x|x:1..5 & y:1..5 & x+x=y})]>"
]
},
"execution_count": 9,
@@ -666,64 +666,64 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"242pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 242.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=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
"<!-- Noderoot -->\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",
+ "<path fill=\"#b3ee3a\" stroke=\"black\" 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\">=</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
"</g>\n",
"<!-- Node1 -->\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\">2</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" 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\">2</text>\n",
"</g>\n",
"<!-- Node1->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
"</g>\n",
"<!-- Node2 -->\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\">card</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\">2</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">card</text>\n",
+ "<polyline fill=\"none\" stroke=\"black\" 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\">2</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>Node3</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
- "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\">{1,2}</text>\n",
"</g>\n",
"<!-- Node3->Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-23.5C171.9723,-23.5 163.0335,-23.5 154.4691,-23.5\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M179.6,-23.5C171.61,-23.5 162.69,-23.5 154.18,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.08,-20 144.08,-23.5 154.08,-27 154.08,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
- "<Dot visualization: formula_tree [1*2+3/4=card({1,2})]>"
+ "<Dot visualization: formula_tree [1*2 + 3/4 = card({1, 2})]>"
]
},
"execution_count": 11,
@@ -776,64 +776,66 @@
"<?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.40.1 (20161225.0304)\n",
+ "<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"242pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 242.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=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 238,-106 238,4 -4,4\"/>\n",
"<!-- Noderoot -->\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",
+ "<path fill=\"#b3ee3a\" stroke=\"black\" 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\">=</text>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
"</g>\n",
"<!-- Node1 -->\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\">2</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" 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\">2</text>\n",
"</g>\n",
"<!-- Node1->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
"</g>\n",
"<!-- Node2 -->\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\">card</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\">2</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">card</text>\n",
+ "<polyline fill=\"none\" stroke=\"black\" 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\">2</text>\n",
"</g>\n",
"<!-- Node2->Noderoot -->\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",
+ "<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>Node3</title>\n",
- "<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
- "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{1,2}</text>\n",
+ "<polygon fill=\"white\" stroke=\"black\" points=\"180,-5.5 180,-41.5 234,-41.5 234,-5.5 180,-5.5\"/>\n",
+ "<text text-anchor=\"middle\" x=\"207\" y=\"-19.8\" font-family=\"Times,serif\" font-size=\"14.00\">{1,2}</text>\n",
"</g>\n",
"<!-- Node3->Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3->Node2</title>\n",
- "<path fill=\"none\" stroke=\"#000000\" d=\"M179.997,-23.5C171.9723,-23.5 163.0335,-23.5 154.4691,-23.5\"/>\n",
- "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.295,-20.0001 144.295,-23.5 154.2949,-27.0001 154.295,-20.0001\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M179.6,-23.5C171.61,-23.5 162.69,-23.5 154.18,-23.5\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"154.08,-20 144.08,-23.5 154.08,-27 154.08,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
- "<Dot visualization: formula_tree [thingthing=2thing=card({1,2})]>"
+ "<Dot visualization: formula_tree [LET thing BE thing=2 IN(\n",
+ "thing = card({1, 2})\n",
+ ")END]>"
]
},
"execution_count": 13,
diff --git a/notebooks/tests/external_functions.ipynb b/notebooks/tests/external_functions.ipynb
index f7dcfb6..99c6390 100644
--- a/notebooks/tests/external_functions.ipynb
+++ b/notebooks/tests/external_functions.ipynb
@@ -31,10 +31,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.9.3-nightly\"}$"
+ "$\\text{\"1.11.1-final\"}$"
],
"text/plain": [
- "\"1.9.3-nightly\""
+ "\"1.11.1-final\""
]
},
"execution_count": 2,
@@ -54,10 +54,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"1.8.0_202-b08\"}$"
+ "$\\text{\"1.17.35\\\"\\n\"}$"
],
"text/plain": [
- "\"1.8.0_202-b08\""
+ "\"1.17.35\\\"\\n\""
]
},
"execution_count": 3,
@@ -77,10 +77,10 @@
{
"data": {
"text/markdown": [
- "$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
+ "$\\text{\"1125ea39af78125a39093c65a0af783b7636b362\"}$"
],
"text/plain": [
- "\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
+ "\"1125ea39af78125a39093c65a0af783b7636b362\""
]
},
"execution_count": 4,
@@ -123,10 +123,10 @@
{
"data": {
"text/markdown": [
- "$151498512$"
+ "$164878528$"
],
"text/plain": [
- "151498512"
+ "164878528"
]
},
"execution_count": 6,
@@ -152,14 +152,15 @@
"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/Shared/Uni/SHK/ProB2/prob_prolog/\n\n",
+ "evalue": ":eval: UNKNOWN: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\nUrsache: java.lang.ClassNotFoundException: de.prob.cliparser.CliBParser\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",
+ "\u001b[1m\u001b[31m:eval: UNKNOWN: \u001b[0m",
"\u001b[1m\u001b[31mUnexpected error while parsing machine: \u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
"\u001b[1m\u001b[31mAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m",
+ "\u001b[1m\u001b[31mUrsache: java.lang.ClassNotFoundException: de.prob.cliparser.CliBParser\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/Shared/Uni/SHK/ProB2/prob_prolog/\u001b[0m"
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index fb5e3e3..4cb48eb 100644
--- a/notebooks/tests/help.ipynb
+++ b/notebooks/tests/help.ipynb
@@ -29,6 +29,7 @@
"* `:let` - Evaluate an expression and store it in a local variable.\n",
"* `:unlet` - Remove a local variable.\n",
"* `:assert` - Ensure that the predicate is true, and show an error otherwise.\n",
+ "* `:language` - Change the language used to parse formulas entered by the user.\n",
"\n",
"## Animation\n",
"\n",
@@ -61,7 +62,7 @@
"* `:pref` - View or change the value of one or more preferences.\n",
"* `:stats` - Show statistics about the state space.\n",
"* `:time` - Execute the given command and measure how long it takes to execute.\n",
- "* `:version` - Display version info about the ProB CLI and ProB 2.\n"
+ "* `:version` - Display version info about the ProB 2 Jupyter kernel and its underlying components.\n"
],
"text/plain": [
"Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
@@ -76,6 +77,7 @@
":let - Evaluate an expression and store it in a local variable.\n",
":unlet - Remove a local variable.\n",
":assert - Ensure that the predicate is true, and show an error otherwise.\n",
+ ":language - Change the language used to parse formulas entered by the user.\n",
"\n",
"Animation:\n",
"::load - Load a B machine from the given source code.\n",
@@ -104,7 +106,7 @@
":pref - View or change the value of one or more preferences.\n",
":stats - Show statistics about the state space.\n",
":time - Execute the given command and measure how long it takes to execute.\n",
- ":version - Display version info about the ProB CLI and ProB 2.\n"
+ ":version - Display version info about the ProB 2 Jupyter kernel and its underlying components.\n"
]
},
"execution_count": 1,
diff --git a/notebooks/tests/language.ipynb b/notebooks/tests/language.ipynb
index d28855a..8dcf650 100644
--- a/notebooks/tests/language.ipynb
+++ b/notebooks/tests/language.ipynb
@@ -113,10 +113,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2'",
+ "evalue": ":eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2',Type mismatch: Expected POW(_A), but was INTEGER in '3'",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2'\u001b[0m"
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2',Type mismatch: Expected POW(_A), but was INTEGER in '3'\u001b[0m"
]
}
],
@@ -318,7 +318,7 @@
{
"data": {
"text/markdown": [
- "$\\{(\\mathit{ONE}\\mapsto \\mathit{TWO})\\}$"
+ "$\\{(\\mathit{ONE}\\mapsto\\mathit{TWO})\\}$"
],
"text/plain": [
"{(ONE↦TWO)}"
diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb
index 7d3e416..7865943 100644
--- a/notebooks/tests/load_cell.ipynb
+++ b/notebooks/tests/load_cell.ipynb
@@ -228,13 +228,13 @@
"metadata": {},
"outputs": [
{
- "ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: ProB returned error messages:\nError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES' ((machine from Jupyter cell):1:20)",
+ "ename": "ProBError",
+ "evalue": "ProB returned error messages:\nError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES' ((machine from Jupyter cell).mch:1:19)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mnull\u001b[0m",
- "\u001b[1m\u001b[31mError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES' ((machine from Jupyter cell):1:20)\u001b[0m",
- "\u001b[1m\u001b[31mError start column 20 out of bounds (0..18)\u001b[0m"
+ "\u001b[1m\u001b[31mError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES' ((machine from Jupyter cell).mch:1:19)\u001b[0m",
+ "\u001b[1m\u001b[30mMACHINE syntaxerror\u001b[0m\u001b[1m\u001b[30m\u001b[41m\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
]
}
],
@@ -251,16 +251,20 @@
},
"outputs": [
{
- "ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
+ "ename": "ProBError",
+ "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m2 errors:\u001b[0m",
"\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[30mMACHINE duplicate\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[30m PROPERTIES x : INT\u001b[0m",
"\u001b[1m\u001b[31mError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
- "\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
+ "\u001b[1m\u001b[30mMACHINE duplicate\u001b[0m",
+ "\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[30m PROPERTIES x : INT\u001b[0m"
]
}
],
@@ -278,20 +282,26 @@
"metadata": {},
"outputs": [
{
- "ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)",
+ "ename": "ProBError",
+ "evalue": "Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m3 errors:\u001b[0m",
"\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\u001b[0m",
+ "\u001b[1m\u001b[30mMACHINE typeerrors\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\"string\"\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\u001b[0m",
+ "\u001b[1m\u001b[30m CONSTANTS x\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m",
"\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m",
"\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m\u001b[1m\u001b[30m)\u001b[0m",
+ "\u001b[1m\u001b[30mEND\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)\u001b[0m",
- "\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m\u001b[1m\u001b[30m & 1 = (\"string\"\u001b[0m"
+ "\u001b[1m\u001b[30m CONSTANTS x\u001b[0m",
+ "\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m\u001b[1m\u001b[30m & 1 = (\"string\"\u001b[0m",
+ "\u001b[1m\u001b[30m ^ \"string\"\u001b[0m"
]
}
],
diff --git a/notebooks/tests/modelcheck.ipynb b/notebooks/tests/modelcheck.ipynb
index ebfd01f..6f0e71e 100644
--- a/notebooks/tests/modelcheck.ipynb
+++ b/notebooks/tests/modelcheck.ipynb
@@ -60,7 +60,7 @@
{
"data": {
"text/plain": [
- "0.265 sec, 36 of 36 states processed, 156 transitions"
+ "0.300 sec, 36 of 36 states processed, 156 transitions"
]
},
"metadata": {},
@@ -109,7 +109,7 @@
{
"data": {
"text/plain": [
- "0.519 sec, 84 of 455 states processed, 625 transitions"
+ "0.268 sec, 57 of 316 states processed, 416 transitions"
]
},
"metadata": {},
@@ -166,7 +166,7 @@
{
"data": {
"text/plain": [
- "25.925 sec, 17753 of 17753 states processed, 185145 transitions"
+ "21.538 sec, 17753 of 17753 states processed, 185145 transitions"
]
},
"metadata": {},
diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb
index 01c6e83..416a27b 100644
--- a/notebooks/tests/pref.ipynb
+++ b/notebooks/tests/pref.ipynb
@@ -59,8 +59,10 @@
"ALLOW_INCOMPLETE_SETUP_CONSTANTS = false\n",
"ALLOW_LOCAL_OPERATION_CALLS = false\n",
"ALLOW_NEW_OPERATIONS_IN_REFINEMENT = false\n",
+ "ALLOW_OPERATION_CALLS_FOR_USES = false\n",
"ALLOW_OPERATION_CALLS_IN_EXPRESSIONS = false\n",
"ALLOW_OUTPUT_READING = false\n",
+ "ALLOW_REALS = default\n",
"ALLOW_SIMULTANEOUS_ASSIGNMENTS = false\n",
"ALLOW_UNTYPED_IDENTIFIERS = false\n",
"ALLOY_SCOPELESS_TRANSLATION = false\n",
@@ -72,6 +74,8 @@
"BBRESULTS = false\n",
"BOOL_AS_PREDICATE = false\n",
"BUGLY = false\n",
+ "CACHE_OPERATIONS = true\n",
+ "CBC_PROVIDE_EXPLANATIONS = false\n",
"CHR = false\n",
"CLPFD = true\n",
"COMPILE_WHILE = true\n",
@@ -143,6 +147,7 @@
"EDITOR = /usr/local/bin/bbedit\n",
"EDITOR_GUI = /Applications/BBEdit.app\n",
"ENUMERATE_INFINITE_TYPES = true\n",
+ "ENUMERATION_ORDER_ANALYSIS = true\n",
"EXPAND_FORALL_UPTO = 100\n",
"FILTER_UNUSED = false\n",
"FORGET_STATE_SPACE = false\n",
@@ -153,6 +158,7 @@
"JAVA_PATH = /usr/bin/java\n",
"JVM_PARSER_ARGS = \n",
"JVM_PARSER_HEAP_MB = 0\n",
+ "JVM_PARSER_POSITION_INFOS = true\n",
"KODKOD = false\n",
"KODKOD_MAX_NR_SOLS = 22\n",
"KODKOD_ONLY_FULL = true\n",
@@ -162,6 +168,7 @@
"LATEX_ENCODING = auto\n",
"LATEX_GREEK_IDENTIFIERS = false\n",
"LIFT_EXISTS = false\n",
+ "LTL_SAFETY_MODEL_CHECK = true\n",
"LTSMIN = ./lib/\n",
"MAXINT = 3\n",
"MAX_DISPLAY_SET = 100\n",
@@ -187,6 +194,9 @@
"PP_SEQUENCES = false\n",
"PROB2_TRACE_FILE = \n",
"PROB2_TRACE_FILE_UNIQUE = false\n",
+ "PROB_LASTCHANGED_INFO = Wed Dec 29 13:14:39 2021 +0100\n",
+ "PROB_REVISION_INFO = 1125ea39af78125a39093c65a0af783b7636b362\n",
+ "PROB_VERSION_INFO = 1.11.1-final\n",
"PROOF_INFO = true\n",
"RAISE_ABORT_IMMEDIATELY = false\n",
"RANDOMISED_RESTART_INIT = false\n",
@@ -199,6 +209,9 @@
"SAFETY_MODEL_CHECK = false\n",
"SAT_SUPPORTED_INTERPRETER = false\n",
"SHOW_EVENTB_ANY_VALUES = false\n",
+ "SHOW_FORMULA_EXPLANATIONS = false\n",
+ "SHOW_FORMULA_FUNCTOR = -1\n",
+ "SHOW_FORMULA_PROOF_INFO = false\n",
"SMT = false\n",
"SMTLIB_BOOL_ARRAYS_TO_SETS = false\n",
"SMTLIB_PREPROCESS = false\n",
@@ -231,6 +244,8 @@
"USE_RECORD_CONSTRUCTION = true\n",
"USE_SCOPE_DEFINITION = true\n",
"WARN_IF_DEFINITION_HIDES_VARIABLE = true\n",
+ "WD_ANALYSIS_FOR_ANIMATION = true\n",
+ "WD_IGNORE_EXTERNAL = false\n",
"XML_ENCODING = auto\n"
]
},
diff --git a/notebooks/tests/render.ipynb b/notebooks/tests/render.ipynb
index 308e8d3..b8b1230 100644
--- a/notebooks/tests/render.ipynb
+++ b/notebooks/tests/render.ipynb
@@ -203,10 +203,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": "::render: Missing required body content",
+ "evalue": "::render: Expected at most 1 arguments, got extra argument: This *is* **Markdown!**",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m::render: Missing required body content\u001b[0m"
+ "\u001b[1m\u001b[31m::render: Expected at most 1 arguments, got extra argument: This *is* **Markdown!**\u001b[0m"
]
}
],
diff --git a/notebooks/tests/show.ipynb b/notebooks/tests/show.ipynb
index ddaf7de..b45afcf 100644
--- a/notebooks/tests/show.ipynb
+++ b/notebooks/tests/show.ipynb
@@ -78,7 +78,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 4,
@@ -116,7 +116,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 6,
@@ -426,7 +426,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 15,
@@ -446,7 +446,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 16,
@@ -704,7 +704,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 23,
@@ -724,7 +724,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 1: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 24,
@@ -744,21 +744,21 @@
{
"data": {
"text/markdown": [
- "<table style=\"font-family:monospace\"><tbody>\n",
+ "<table style=\"font-family:\"Arial\" monospace;font-size:18px\"><tbody>\n",
"<tr>\n",
- "<td style=\"padding:10px\">Overview</td>\n",
+ "<td style=\"padding:2px\">Overview</td>\n",
"<td style=\"padding:0px\"></td>\n",
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"<tr>\n",
"<td style=\"padding:0px\"></td>\n",
- "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/small_empty_w.gif\"/></td>\n",
- "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/small_wqueen_w.gif\"/></td>\n",
+ "<td style=\"padding:8px\"><img alt=\"0\" src=\"images/small_empty_w.gif\"/></td>\n",
+ "<td style=\"padding:8px\"><img alt=\"1\" src=\"images/small_wqueen_w.gif\"/></td>\n",
"</tr>\n",
"<tr>\n",
"<td style=\"padding:0px\"></td>\n",
- "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/small_wqueen_w.gif\"/></td>\n",
- "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/small_empty_w.gif\"/></td>\n",
+ "<td style=\"padding:8px\"><img alt=\"1\" src=\"images/small_wqueen_w.gif\"/></td>\n",
+ "<td style=\"padding:8px\"><img alt=\"0\" src=\"images/small_empty_w.gif\"/></td>\n",
"</tr>\n",
"</tbody></table>"
],
diff --git a/notebooks/tests/solve.ipynb b/notebooks/tests/solve.ipynb
index 63f2940..067057b 100644
--- a/notebooks/tests/solve.ipynb
+++ b/notebooks/tests/solve.ipynb
@@ -17,10 +17,13 @@
"The following solvers are currently available:\n",
"\n",
"* `cvc4`\n",
+ "* `dpllt`\n",
"* `kodkod`\n",
"* `prob`\n",
"* `smt_supported_interpreter`\n",
- "* `z3`\n"
+ "* `z3`\n",
+ "* `z3axm`\n",
+ "* `z3cns`\n"
],
"text/plain": [
":solve SOLVER PREDICATE\n",
@@ -29,10 +32,13 @@
"The following solvers are currently available:\n",
"\n",
"* `cvc4`\n",
+ "* `dpllt`\n",
"* `kodkod`\n",
"* `prob`\n",
"* `smt_supported_interpreter`\n",
- "* `z3`\n"
+ "* `z3`\n",
+ "* `z3axm`\n",
+ "* `z3cns`\n"
]
},
"execution_count": 1,
@@ -119,11 +125,12 @@
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4401885196),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
+ "ename": "PrologException",
+ "evalue": "Unhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4427626972),0,procedure,:(z3interface,/(pop_frame,0)),0)))\n",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31m(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4401885196),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUnhandled exception thrown from Prolog: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4427626972),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
+ "\u001b[0m"
]
}
],
@@ -138,11 +145,11 @@
"outputs": [
{
"ename": "ProBError",
- "evalue": "ProB reported Errors\nProB returned error messages:\nInternal error: Call for event start_solving failed. init_interface(z3)",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nInternal error: Call for event start_solving failed. init_smt_supported_interpreter",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
- "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_interface(z3)\u001b[0m"
+ "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_smt_supported_interpreter\u001b[0m"
]
}
],
@@ -208,7 +215,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 0: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 8,
diff --git a/notebooks/tests/table.ipynb b/notebooks/tests/table.ipynb
index 5ad6688..5de8a16 100644
--- a/notebooks/tests/table.ipynb
+++ b/notebooks/tests/table.ipynb
@@ -40,7 +40,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 0: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 2,
@@ -62,10 +62,10 @@
"text/markdown": [
"|Elements|\n",
"|---|\n",
- "|$1$|\n",
- "|$2$|\n",
- "|$3$|\n",
- "|$4$|\n"
+ "|1|\n",
+ "|2|\n",
+ "|3|\n",
+ "|4|\n"
],
"text/plain": [
"Elements\n",
@@ -94,10 +94,10 @@
"text/markdown": [
"|prj1|prj2|\n",
"|---|---|\n",
- "|$1$|$1$|\n",
- "|$2$|$2$|\n",
- "|$3$|$3$|\n",
- "|$4$|$4$|\n"
+ "|1|1|\n",
+ "|2|2|\n",
+ "|3|3|\n",
+ "|4|4|\n"
],
"text/plain": [
"prj1\tprj2\n",
@@ -126,9 +126,9 @@
"text/markdown": [
"|prj11|prj12|prj2|\n",
"|---|---|---|\n",
- "|$1$|$2$|$3$|\n",
- "|$4$|$5$|$6$|\n",
- "|$7$|$8$|$9$|\n"
+ "|1|2|3|\n",
+ "|4|5|6|\n",
+ "|7|8|9|\n"
],
"text/plain": [
"prj11\tprj12\tprj2\n",
@@ -156,7 +156,7 @@
"text/markdown": [
"|prj1|prj2|\n",
"|---|---|\n",
- "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$|$\\emptyset$|\n"
+ "|∅|∅|\n"
],
"text/plain": [
"prj1\tprj2\n",
@@ -182,8 +182,8 @@
"text/markdown": [
"|prj1|prj2|\n",
"|---|---|\n",
- "|$\\{(1\\mapsto 2),(3\\mapsto 4)\\}$|$\\{(5\\mapsto 6),(7\\mapsto 8)\\}$|\n",
- "|$\\{(2\\mapsto 1),(4\\mapsto 3)\\}$|$\\{(6\\mapsto 5),(8\\mapsto 7)\\}$|\n"
+ "|{(1↦2),(3↦4)}|{(5↦6),(7↦8)}|\n",
+ "|{(2↦1),(4↦3)}|{(6↦5),(8↦7)}|\n"
],
"text/plain": [
"prj1\tprj2\n",
@@ -240,9 +240,9 @@
"text/markdown": [
"|prj11|prj12|prj2|\n",
"|---|---|---|\n",
- "|$1$|$2$|$3$|\n",
- "|$4$|$5$|$6$|\n",
- "|$7$|$8$|$9$|\n"
+ "|1|2|3|\n",
+ "|4|5|6|\n",
+ "|7|8|9|\n"
],
"text/plain": [
"prj11\tprj12\tprj2\n",
diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb
index 016287b..be735ee 100644
--- a/notebooks/tests/time.ipynb
+++ b/notebooks/tests/time.ipynb
@@ -51,10 +51,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 1.034897011 seconds"
+ "Execution time: 1.056192286 seconds"
],
"text/plain": [
- "Execution time: 1.034897011 seconds"
+ "Execution time: 1.056192286 seconds"
]
},
"metadata": {},
@@ -90,10 +90,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 1.206485155 seconds"
+ "Execution time: 0.378675290 seconds"
],
"text/plain": [
- "Execution time: 1.206485155 seconds"
+ "Execution time: 0.378675290 seconds"
]
},
"metadata": {},
diff --git a/notebooks/tests/trace.ipynb b/notebooks/tests/trace.ipynb
index b395563..2813104 100644
--- a/notebooks/tests/trace.ipynb
+++ b/notebooks/tests/trace.ipynb
@@ -103,7 +103,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 0: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 4,
diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb
index 9745c40..3684dc1 100644
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -219,18 +219,18 @@
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:18)\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:18)\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mType errors in formula\u001b[0m",
"\u001b[1m\u001b[30m3 errors:\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m",
+ "\u001b[1m\u001b[30m{1, \u001b[0m\u001b[1m\u001b[30m\u001b[41mTRUE\u001b[0m\u001b[1m\u001b[30m, \"string\", {}}\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (:1:10 to 1:18)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m",
+ "\u001b[1m\u001b[30m{1, TRUE, \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m\u001b[1m\u001b[30m, {}}\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
+ "\u001b[1m\u001b[30m{1, TRUE, \"string\", \u001b[0m\u001b[1m\u001b[30m\u001b[41m{}\u001b[0m\u001b[1m\u001b[30m}\u001b[0m"
]
}
],
@@ -244,13 +244,13 @@
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: Type errors in formula\nProB returned error messages:\nError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mType errors in formula\u001b[0m",
"\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
+ "\u001b[1m\u001b[30m1 + \u001b[0m\u001b[1m\u001b[30m\u001b[41m{}\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
]
}
],
diff --git a/notebooks/tests/version.ipynb b/notebooks/tests/version.ipynb
index 25425b1..fc15096 100644
--- a/notebooks/tests/version.ipynb
+++ b/notebooks/tests/version.ipynb
@@ -36,13 +36,13 @@
{
"data": {
"text/plain": [
- "ProB 2 Jupyter kernel: 1.1.1-SNAPSHOT (e5188664ec88fa6c381b5fec7b46ab44deaf9eb7)\n",
- "ProB 2: 4.0.0-SNAPSHOT (489d93856139812923fae9b8e4c1297e9576b460)\n",
- "ProB B parser: 2.9.26-SNAPSHOT (d2cd9ca3dba77bfff8c6eed9799794af899b3230)\n",
+ "ProB 2 Jupyter kernel: 1.2.1-SNAPSHOT (2aaa99bab781d6eca5a2b3388cca76b412fd52f6)\n",
+ "ProB 2: 3.15.0 (6ee6df4eab62d20df40c36cd42108b62962ec41b)\n",
+ "ProB B parser: 2.9.32 (7306d13499ba281a6e336c006d9fb23204624daa)\n",
"ProB CLI:\n",
- "\t1.10.0-nightly (907db892e8fdc604be6a15cea637d74da98bf1cb)\n",
- "\tLast changed: Tue May 12 19:06:34 2020 +0200\n",
- "\tProlog: SICStus 4.5.1 (x86_64-darwin-17.7.0): Tue Apr 2 15:34:32 CEST 2019"
+ "\t1.11.1-final (1125ea39af78125a39093c65a0af783b7636b362)\n",
+ "\tLast changed: Wed Dec 29 13:14:39 2021 +0100\n",
+ "\tProlog: SICStus 4.7.0 (x86_64-darwin-18.7.0): Wed Jul 7 17:07:32 CEST 2021"
]
},
"execution_count": 2,
diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb
index 96c6098..b86c9b0 100644
--- a/notebooks/tutorials/Functional_Programming_in_B.ipynb
+++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb
@@ -27,7 +27,7 @@
"\n",
"**Solution:**\n",
"* $\\mathit{r2} = \\{1,4,9,16,25,36,49,64,81,100\\}$\n",
- "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$\n",
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$\n",
"* $\\mathit{r1} = 10000000000$"
],
"text/plain": [
@@ -35,7 +35,7 @@
"\n",
"Solution:\n",
"\tr2 = {1,4,9,16,25,36,49,64,81,100}\n",
- "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n",
+ "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)\n",
"\tr1 = 10000000000"
]
},
@@ -69,14 +69,14 @@
"\n",
"**Solution:**\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})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr3 = {(1↦4),(2↦9),(3↦25),(4↦49),(5↦121)}\n",
- "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
]
},
"execution_count": 2,
@@ -108,14 +108,14 @@
"\n",
"**Solution:**\n",
"* $\\mathit{r4} = 256$\n",
- "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tr4 = 256\n",
- "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
]
},
"execution_count": 3,
@@ -147,14 +147,14 @@
"\n",
"**Solution:**\n",
"* $\\mathit{sqrt} = 10$\n",
- "* $\\mathit{f} = \\lambda \\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid \\mathit{x} * \\mathit{x})$"
+ "* $\\mathit{f} = /*@\\mathit{symbolic}*/ \\lambda\\mathit{x}\\qdot(\\mathit{x} \\in \\mathit{INTEGER}\\mid\\mathit{x} * \\mathit{x})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tsqrt = 10\n",
- "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+ "\tf = /*@symbolic*/ λx·(x ∈ INTEGER∣x ∗ x)"
]
},
"execution_count": 4,
@@ -185,7 +185,7 @@
"$\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\cprod}{\\mathbin\\times}\\mathit{TRUE}$\n",
"\n",
"**Solution:**\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{f} = /*@\\mathit{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": [
@@ -228,7 +228,7 @@
"* $\\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} = /*@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{f} = /*@\\mathit{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": [
@@ -276,7 +276,7 @@
"\n",
"**Solution:**\n",
"* $\\mathit{r5} = \\{2,4,10,100\\}$\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}\\}$"
+ "* $\\mathit{f} = /*@\\mathit{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",
@@ -313,22 +313,22 @@
"text/markdown": [
"|x|isqrt|\n",
"|---|---|\n",
- "|$1$|$1$|\n",
- "|$2$|$2$|\n",
- "|$3$|$2$|\n",
- "|$4$|$2$|\n",
- "|$5$|$3$|\n",
- "|$6$|$3$|\n",
- "|$7$|$3$|\n",
- "|$8$|$3$|\n",
- "|$9$|$3$|\n",
- "|$10$|$4$|\n",
- "|$11$|$4$|\n",
- "|$12$|$4$|\n",
- "|$13$|$4$|\n",
- "|$14$|$4$|\n",
- "|$15$|$4$|\n",
- "|$16$|$4$|\n"
+ "|1|1|\n",
+ "|2|2|\n",
+ "|3|2|\n",
+ "|4|2|\n",
+ "|5|3|\n",
+ "|6|3|\n",
+ "|7|3|\n",
+ "|8|3|\n",
+ "|9|3|\n",
+ "|10|4|\n",
+ "|11|4|\n",
+ "|12|4|\n",
+ "|13|4|\n",
+ "|14|4|\n",
+ "|15|4|\n",
+ "|16|4|\n"
],
"text/plain": [
"x\tisqrt\n",
@@ -367,10 +367,10 @@
{
"data": {
"text/latex": [
- "$\\mathit{f} = \\lambda \\mathit{x}.(\\mathit{x} \\in \\mathbb Z \\mid \\mathit{x} * \\mathit{x}) \\wedge \\mathit{r1} = \\mathit{f}(100000) \\wedge \\mathit{r2} = \\mathit{f}[1 .. 10]$"
+ "$\\mathit{f} = /*@symbolic*/ \\lambda \\mathit{x}.(\\mathit{x} \\in \\mathbb Z \\mid \\mathit{x} * \\mathit{x}) \\wedge \\mathit{r1} = \\mathit{f}(100000) \\wedge \\mathit{r2} = \\mathit{f}[1 .. 10]$"
],
"text/plain": [
- "f = λx.(x ∈ ℤ|x * x) ∧ r1 = f(100000) ∧ r2 = f[1 ‥ 10]"
+ "f = /*@symbolic*/ λx.(x ∈ ℤ|x * x) ∧ r1 = f(100000) ∧ r2 = f[1 ‥ 10]"
]
},
"execution_count": 9,
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
index 9bb75a8..7b716bf 100644
--- a/notebooks/tutorials/prob_solver_intro.ipynb
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -414,14 +414,14 @@
"text/markdown": [
"|prj1|prj2|\n",
"|---|---|\n",
- "|$1$|$1$|\n",
- "|$2$|$5$|\n",
- "|$3$|$8$|\n",
- "|$4$|$6$|\n",
- "|$5$|$3$|\n",
- "|$6$|$7$|\n",
- "|$7$|$2$|\n",
- "|$8$|$4$|\n"
+ "|1|1|\n",
+ "|2|5|\n",
+ "|3|8|\n",
+ "|4|6|\n",
+ "|5|3|\n",
+ "|6|7|\n",
+ "|7|2|\n",
+ "|8|4|\n"
],
"text/plain": [
"prj1\tprj2\n",
@@ -547,7 +547,7 @@
{
"data": {
"text/markdown": [
- "$\\{(\\mathit{TRUE}\\mapsto \\mathit{TRUE}\\mapsto \\mathit{FALSE})\\}$"
+ "$\\{(\\mathit{TRUE}\\mapsto\\mathit{TRUE}\\mapsto\\mathit{FALSE})\\}$"
],
"text/plain": [
"{(TRUE↦TRUE↦FALSE)}"
@@ -574,7 +574,7 @@
"text/markdown": [
"|A|B|C|\n",
"|---|---|---|\n",
- "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n"
+ "|TRUE|TRUE|FALSE|\n"
],
"text/plain": [
"A\tB\tC\n",
--
GitLab