diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.fasten.assurance.build/models/com.fasten.assurance.build.mps b/code/languages/com.mbeddr.formal.safety/solutions/com.fasten.assurance.build/models/com.fasten.assurance.build.mps
index 20b7cc0e..4a3b3250 100644
--- a/code/languages/com.mbeddr.formal.safety/solutions/com.fasten.assurance.build/models/com.fasten.assurance.build.mps
+++ b/code/languages/com.mbeddr.formal.safety/solutions/com.fasten.assurance.build/models/com.fasten.assurance.build.mps
@@ -605,6 +605,9 @@
+
+
+
@@ -2095,6 +2098,63 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -2195,6 +2255,11 @@
+
+
+
+
+
diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
index a288dc55..20af4617 100644
--- a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
+++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.build/models/com.mbeddr.formal.safety.build.mps
@@ -782,6 +782,9 @@
+
+
+
@@ -2347,6 +2350,63 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -2447,6 +2507,11 @@
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/com.mpsbasics.pdfexporter.mpl b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/com.mpsbasics.pdfexporter.mpl
index 27a5638c..6b2fccf4 100644
--- a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/com.mpsbasics.pdfexporter.mpl
+++ b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/com.mpsbasics.pdfexporter.mpl
@@ -21,6 +21,7 @@
6b84fb9e-5f09-4a61-bf31-3bfdc54820e3(com.mpsbasics.editor.utils)
34e84b8f-afa8-4364-abcd-a279fddddbe7(jetbrains.mps.editor.runtime)
8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)
+ 39983771-4e9b-401b-a1a9-1da6c777c843(MPS.ThirdParty)
@@ -67,6 +68,7 @@
+
diff --git a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.behavior.mps b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.behavior.mps
index e7eb172d..13918f81 100644
--- a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.behavior.mps
+++ b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.behavior.mps
@@ -34,6 +34,12 @@
+
+
+
+
+
+
@@ -191,10 +197,12 @@
+
+
@@ -667,9 +675,7 @@
-
-
-
+
@@ -2442,5 +2448,345 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.editor.mps b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.editor.mps
index 0cdd6b42..1aafa27e 100644
--- a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.editor.mps
+++ b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.editor.mps
@@ -93,6 +93,7 @@
+
@@ -377,5 +378,32 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.structure.mps b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.structure.mps
index b2540024..51749f56 100644
--- a/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.structure.mps
+++ b/code/languages/com.mpsbasics/languages/com.mpsbasics.pdfexporter/models/com.mpsbasics.pdfexporter.structure.mps
@@ -154,5 +154,20 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox.sandbox/models/com.mpsbasics.pdfbox.sandbox._010_smoke.mps b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox.sandbox/models/com.mpsbasics.pdfbox.sandbox._010_smoke.mps
index a0d124b5..890ce569 100644
--- a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox.sandbox/models/com.mpsbasics.pdfbox.sandbox._010_smoke.mps
+++ b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox.sandbox/models/com.mpsbasics.pdfbox.sandbox._010_smoke.mps
@@ -16,6 +16,9 @@
+
+
+
@@ -71,6 +74,270 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/com.mpsbasics.pdfbox.msd b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/com.mpsbasics.pdfbox.msd
index 24f2d9d9..e18fa150 100644
--- a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/com.mpsbasics.pdfbox.msd
+++ b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/com.mpsbasics.pdfbox.msd
@@ -10,10 +10,20 @@
+
+
+
+
+
+
+
+
+
+
diff --git a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-core-1.1.23.jar b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-core-1.1.23.jar
new file mode 100644
index 00000000..364aef30
Binary files /dev/null and b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-core-1.1.23.jar differ
diff --git a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-pdfbox-1.1.23.jar b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-pdfbox-1.1.23.jar
new file mode 100644
index 00000000..be126cb5
Binary files /dev/null and b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/openhtmltopdf-pdfbox-1.1.23.jar differ
diff --git a/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/xmpbox-3.0.1.jar b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/xmpbox-3.0.1.jar
new file mode 100644
index 00000000..ac071766
Binary files /dev/null and b/code/languages/com.mpsbasics/solutions/com.mpsbasics.pdfbox/lib/xmpbox-3.0.1.jar differ
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/_010_uber_atg_safety_case_top.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/_010_uber_atg_safety_case_top.mpsr
index 5c59e650..bce2a1e3 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/_010_uber_atg_safety_case_top.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/_010_uber_atg_safety_case_top.mpsr
@@ -116837,320 +116837,316 @@
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
@@ -117164,10 +117160,6 @@
-
-
-
-
@@ -117187,12 +117179,12 @@
-
-
+
+
-
-
+
+
@@ -117231,12 +117223,12 @@
-
-
+
+
-
-
+
+
@@ -117257,12 +117249,12 @@
-
-
+
+
-
-
+
+
@@ -117270,12 +117262,12 @@
-
-
+
+
-
-
+
+
@@ -117296,12 +117288,12 @@
-
-
+
+
-
-
+
+
@@ -117334,6 +117326,14 @@
+
+
+
+
+
+
+
+
@@ -117370,18 +117370,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -117402,12 +117410,12 @@
-
-
+
+
-
-
+
+
@@ -117428,12 +117436,12 @@
-
-
+
+
-
-
+
+
@@ -117454,12 +117462,12 @@
-
-
+
+
-
-
+
+
@@ -117480,8 +117488,8 @@
-
-
+
+
@@ -117497,8 +117505,8 @@
-
-
+
+
@@ -117518,18 +117526,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -117550,8 +117566,8 @@
-
-
+
+
@@ -117567,8 +117583,8 @@
-
-
+
+
@@ -117588,6 +117604,14 @@
+
+
+
+
+
+
+
+
@@ -117607,12 +117631,12 @@
-
-
+
+
-
-
+
+
@@ -117632,14 +117656,22 @@
+
+
+
+
+
+
+
+
-
-
+
+
@@ -117655,8 +117687,8 @@
-
-
+
+
@@ -117676,14 +117708,22 @@
+
+
+
+
+
+
+
+
-
-
+
+
@@ -117699,8 +117739,8 @@
-
-
+
+
@@ -117720,18 +117760,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -117752,8 +117800,8 @@
-
-
+
+
@@ -117769,8 +117817,8 @@
-
-
+
+
@@ -117778,12 +117826,12 @@
-
-
+
+
-
-
+
+
@@ -117804,12 +117852,12 @@
-
-
+
+
-
-
+
+
@@ -117842,6 +117890,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.1.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.1.mpsr
index de839a5d..e79db6c5 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.1.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.1.mpsr
@@ -75,23 +75,23 @@
-
-
+
+
-
-
+
+
-
+
@@ -99,63 +99,63 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -163,56 +163,56 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -288,180 +288,180 @@
-
+
-
-
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
@@ -469,12 +469,12 @@
-
-
+
+
-
-
+
+
@@ -513,12 +513,12 @@
-
-
+
+
-
-
+
+
@@ -539,12 +539,12 @@
-
-
+
+
-
-
+
+
@@ -565,12 +565,12 @@
-
-
+
+
-
-
+
+
@@ -591,12 +591,12 @@
-
-
+
+
-
-
+
+
@@ -616,14 +616,6 @@
-
-
-
-
-
-
-
-
@@ -655,6 +647,14 @@
+
+
+
+
+
+
+
+
@@ -673,19 +673,19 @@
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
@@ -717,18 +717,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -749,12 +757,12 @@
-
-
+
+
-
-
+
+
@@ -787,18 +795,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -819,12 +835,12 @@
-
-
+
+
-
-
+
+
@@ -845,12 +861,12 @@
-
-
+
+
-
-
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.4.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.4.mpsr
index 830d5602..8bd89fcb 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.4.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.4.mpsr
@@ -14,11 +14,35 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -42,71 +66,71 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -114,48 +138,48 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -215,6 +239,340 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.9.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.9.mpsr
index cc7a5df9..c519adc7 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.9.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.9.mpsr
@@ -14,11 +14,35 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -42,31 +66,31 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -74,31 +98,31 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -106,95 +130,95 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -202,40 +226,40 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -335,6 +359,552 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.mpsr
index 52df974a..0ae12ba8 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.1.mpsr
@@ -78,8 +78,8 @@
-
-
+
+
@@ -88,23 +88,23 @@
-
-
+
+
-
-
+
+
-
+
@@ -112,31 +112,31 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -146,63 +146,63 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -210,7 +210,7 @@
-
+
@@ -218,47 +218,47 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -266,31 +266,31 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -298,39 +298,39 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -338,8 +338,8 @@
-
-
+
+
@@ -348,63 +348,63 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -412,7 +412,7 @@
-
+
@@ -585,149 +585,149 @@
-
+
-
-
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
+
+
+
@@ -735,59 +735,59 @@
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
+
+
+
@@ -795,159 +795,159 @@
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
+
+
+
@@ -955,50 +955,50 @@
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
@@ -1006,11 +1006,11 @@
-
+
-
+
@@ -1044,18 +1044,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1076,12 +1084,12 @@
-
-
+
+
-
-
+
+
@@ -1114,17 +1122,25 @@
+
+
+
+
+
+
+
+
-
+
-
+
@@ -1164,11 +1180,11 @@
-
+
-
+
@@ -1190,11 +1206,11 @@
-
+
-
+
@@ -1228,18 +1244,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1260,11 +1284,11 @@
-
+
-
+
@@ -1286,12 +1310,12 @@
-
-
+
+
-
-
+
+
@@ -1324,18 +1348,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1356,12 +1388,12 @@
-
-
+
+
-
-
+
+
@@ -1382,12 +1414,12 @@
-
-
+
+
-
-
+
+
@@ -1408,11 +1440,11 @@
-
+
-
+
@@ -1434,12 +1466,12 @@
-
-
+
+
-
-
+
+
@@ -1460,12 +1492,12 @@
-
-
+
+
-
-
+
+
@@ -1486,12 +1518,12 @@
-
-
+
+
-
-
+
+
@@ -1524,18 +1556,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1556,12 +1596,12 @@
-
-
+
+
-
-
+
+
@@ -1582,12 +1622,12 @@
-
-
+
+
-
-
+
+
@@ -1608,12 +1648,12 @@
-
-
+
+
-
-
+
+
@@ -1634,11 +1674,11 @@
-
+
-
+
@@ -1672,18 +1712,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1704,12 +1752,12 @@
-
-
+
+
-
-
+
+
@@ -1730,12 +1778,12 @@
-
-
+
+
-
-
+
+
@@ -1756,12 +1804,12 @@
-
-
+
+
-
-
+
+
@@ -1782,11 +1830,11 @@
-
+
-
+
@@ -1808,11 +1856,11 @@
-
+
-
+
@@ -1846,6 +1894,14 @@
+
+
+
+
+
+
+
+
@@ -1864,18 +1920,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1896,12 +1960,12 @@
-
-
+
+
-
-
+
+
@@ -1934,18 +1998,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -1966,12 +2038,12 @@
-
-
+
+
-
-
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.2.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.2.mpsr
index 640a80fd..35af8404 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.2.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.2.mpsr
@@ -75,96 +75,96 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -216,120 +216,120 @@
-
+
-
-
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
@@ -349,18 +349,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -381,12 +389,12 @@
-
-
+
+
-
-
+
+
@@ -419,18 +427,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -451,12 +467,12 @@
-
-
+
+
-
-
+
+
@@ -489,18 +505,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -521,12 +545,12 @@
-
-
+
+
-
-
+
+
@@ -547,12 +571,12 @@
-
-
+
+
-
-
+
+
@@ -573,12 +597,12 @@
-
-
+
+
-
-
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.3.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.3.mpsr
index e9f54e8d..abcf2b04 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.3.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.3.mpsr
@@ -75,15 +75,15 @@
-
-
+
+
-
+
@@ -91,87 +91,87 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
+
@@ -179,56 +179,56 @@
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
-
-
+
+
@@ -312,200 +312,200 @@
-
+
-
-
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
@@ -513,12 +513,12 @@
-
-
+
+
-
-
+
+
@@ -539,12 +539,12 @@
-
-
+
+
-
-
+
+
@@ -565,12 +565,12 @@
-
-
+
+
-
-
+
+
@@ -591,12 +591,12 @@
-
-
+
+
-
-
+
+
@@ -629,18 +629,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -660,14 +668,6 @@
-
-
-
-
-
-
-
-
@@ -687,12 +687,12 @@
-
-
+
+
-
-
+
+
@@ -712,14 +712,6 @@
-
-
-
-
-
-
-
-
@@ -739,12 +731,12 @@
-
-
+
+
-
-
+
+
@@ -777,6 +769,14 @@
+
+
+
+
+
+
+
+
@@ -795,18 +795,26 @@
+
+
+
+
+
+
+
+
-
-
+
+
-
-
+
+
@@ -845,12 +853,12 @@
-
-
+
+
-
-
+
+
@@ -871,12 +879,12 @@
-
-
+
+
-
-
+
+
@@ -897,12 +905,12 @@
-
-
+
+
-
-
+
+
@@ -923,12 +931,12 @@
-
-
+
+
-
-
+
+
@@ -949,12 +957,12 @@
-
-
+
+
-
-
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.mpsr
index b5adecef..b73d2db3 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/extract_from_G1.4.mpsr
@@ -98,10 +98,10 @@
-
+
-
-
+
+
@@ -1412,12 +1412,12 @@
-
-
+
+
-
-
+
+
@@ -4006,12 +4006,12 @@
-
-
+
+
-
-
+
+
@@ -4510,30 +4510,30 @@
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/pdf_export_demo.mpsr b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/pdf_export_demo.mpsr
index 9e583476..cc088e48 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/pdf_export_demo.mpsr
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized/pdf_export_demo.mpsr
@@ -11,6 +11,7 @@
+
@@ -42,6 +43,7 @@
+
@@ -57,11 +59,28 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
diff --git a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized_pdf_export.mps b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized_pdf_export.mps
index 226d2a75..ae4e98f0 100644
--- a/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized_pdf_export.mps
+++ b/code/tutorial-safety/solutions/com.mbeddr.formal.safety.tutorial/models/_500_real_world_examples._010_uber_atg_safety_case_modularized_pdf_export.mps
@@ -15,6 +15,12 @@
+
+
+
+
+
+
@@ -56,10 +62,33 @@
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
@@ -87,6 +116,345 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+