From 718c18ddfd2a5c0f7a7902823a6104a572913fb2 Mon Sep 17 00:00:00 2001 From: danielratiu Date: Thu, 3 Oct 2024 21:21:07 +0200 Subject: [PATCH 1/2] safety: initial support for SPIs --- .../com.mbeddr.formal.safety/.mps/modules.xml | 3 + .../fasten.safety.gsn.runtime.devkit | 9 + .../com.mbeddr.formal.safety.argument.spi.mpl | 95 ++++ ...dr.formal.safety.argument.spi.behavior.mps | 482 ++++++++++++++++++ ...formal.safety.argument.spi.constraints.mps | 19 + ...eddr.formal.safety.argument.spi.editor.mps | 170 ++++++ ...r.formal.safety.argument.spi.structure.mps | 135 +++++ ....formal.safety.argument.spi.typesystem.mps | 11 + ...m.mbeddr.formal.safety.gsn.constraints.mps | 16 + .../com.mbeddr.formal.safety.gsn.editor.mps | 13 + ...com.mbeddr.formal.safety.gsn.structure.mps | 12 + .../models/com.fasten.assurance.build.mps | 306 +++++++++++ ...ddr.formal.safety.argument.spi.sandbox.msd | 43 ++ ...safety.argument.spi.sandbox._010_smoke.mps | 160 ++++++ .../models/com.mbeddr.formal.safety.build.mps | 95 ++++ .../com.mbeddr.formal.safety.gsn.web.rt.msd | 2 + 16 files changed, 1571 insertions(+) create mode 100644 code/languages/com.mbeddr.formal.safety/devkits/fasten.safety.gsn.runtime/fasten.safety.gsn.runtime.devkit create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/com.mbeddr.formal.safety.argument.spi.mpl create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.behavior.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.constraints.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.editor.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.typesystem.mps create mode 100644 code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/com.mbeddr.formal.safety.argument.spi.sandbox.msd create mode 100644 code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/models/com.mbeddr.formal.safety.argument.spi.sandbox._010_smoke.mps diff --git a/code/languages/com.mbeddr.formal.safety/.mps/modules.xml b/code/languages/com.mbeddr.formal.safety/.mps/modules.xml index a59d048c1..7cee74d19 100644 --- a/code/languages/com.mbeddr.formal.safety/.mps/modules.xml +++ b/code/languages/com.mbeddr.formal.safety/.mps/modules.xml @@ -12,6 +12,7 @@ + @@ -31,6 +32,7 @@ + @@ -69,6 +71,7 @@ + diff --git a/code/languages/com.mbeddr.formal.safety/devkits/fasten.safety.gsn.runtime/fasten.safety.gsn.runtime.devkit b/code/languages/com.mbeddr.formal.safety/devkits/fasten.safety.gsn.runtime/fasten.safety.gsn.runtime.devkit new file mode 100644 index 000000000..e96a19cbe --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/devkits/fasten.safety.gsn.runtime/fasten.safety.gsn.runtime.devkit @@ -0,0 +1,9 @@ + + + + + + b64463ba-ae31-4cf7-be7b-afc13cab4daa(fasten.safety.gsn) + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/com.mbeddr.formal.safety.argument.spi.mpl b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/com.mbeddr.formal.safety.argument.spi.mpl new file mode 100644 index 000000000..30f35ef7a --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/com.mbeddr.formal.safety.argument.spi.mpl @@ -0,0 +1,95 @@ + + + + + + + + + + + + + + + + 92d2ea16-5a42-4fdf-a676-c7604efe3504(de.slisson.mps.richtext) + f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage) + 6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK) + 1ed103c3-3aa6-49b7-9c21-6765ee11f224(MPS.Editor) + e8a04d94-4307-4f88-95a2-25f7c4f39437(com.mbeddr.formal.safety.gsn) + 13744753-c81f-424a-9c1b-cf8943bf4e86(jetbrains.mps.lang.sharedConcepts) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base) + f3061a53-9226-4cc5-a443-f952ceaf5816(jetbrains.mps.baseLanguage) + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.behavior.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.behavior.mps new file mode 100644 index 000000000..856473447 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.behavior.mps @@ -0,0 +1,482 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.constraints.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.constraints.mps new file mode 100644 index 000000000..3afd7271f --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.constraints.mps @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.editor.mps new file mode 100644 index 000000000..ee82370cd --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.editor.mps @@ -0,0 +1,170 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps new file mode 100644 index 000000000..573793cbe --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps @@ -0,0 +1,135 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.typesystem.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.typesystem.mps new file mode 100644 index 000000000..6fb5cd500 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.typesystem.mps @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.constraints.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.constraints.mps index fd9e465b4..2a64d845e 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.constraints.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.constraints.mps @@ -75,6 +75,9 @@ + + + @@ -128,6 +131,9 @@ + + + @@ -328,5 +334,15 @@ + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps index b3573fede..39d14b281 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.editor.mps @@ -14889,5 +14889,18 @@ + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps index 496d8b115..d990267d8 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps @@ -468,5 +468,17 @@ + + + + + + + + + + + + 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 79c687e22..1622bf505 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 @@ -6378,6 +6378,312 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/com.mbeddr.formal.safety.argument.spi.sandbox.msd b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/com.mbeddr.formal.safety.argument.spi.sandbox.msd new file mode 100644 index 000000000..43393bffc --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/com.mbeddr.formal.safety.argument.spi.sandbox.msd @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + 8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI) + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/models/com.mbeddr.formal.safety.argument.spi.sandbox._010_smoke.mps b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/models/com.mbeddr.formal.safety.argument.spi.sandbox._010_smoke.mps new file mode 100644 index 000000000..7c7323e87 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.argument.spi.sandbox/models/com.mbeddr.formal.safety.argument.spi.sandbox._010_smoke.mps @@ -0,0 +1,160 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 89a54fc9b..c4c3de6ba 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 @@ -15109,6 +15109,101 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.gsn.web.rt/com.mbeddr.formal.safety.gsn.web.rt.msd b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.gsn.web.rt/com.mbeddr.formal.safety.gsn.web.rt.msd index af19cdb4a..52d2e375d 100644 --- a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.gsn.web.rt/com.mbeddr.formal.safety.gsn.web.rt.msd +++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.gsn.web.rt/com.mbeddr.formal.safety.gsn.web.rt.msd @@ -30,6 +30,7 @@ 31b0df10-2d1f-4744-8de7-461666d7c2d1(com.mbeddr.formal.safety.gsn.web#01) 7124e466-fc92-4803-a656-d7a6b7eb3910(MPS.TextGen) 215c4c45-ba99-49f5-9ab7-4b6901a63cfd(MPS.Generator) + f8e20673-3f65-44e9-84c0-c4a4b6ede37e(jetbrains.mps.make.facets) @@ -82,6 +83,7 @@ + From 18930bd6dec79b992d2f06ad5fe3c2a05db9af23 Mon Sep 17 00:00:00 2001 From: danielratiu Date: Thu, 3 Oct 2024 21:48:19 +0200 Subject: [PATCH 2/2] safety: Force Save All --- .../com.mbeddr.formal.safety.argument.spi.structure.mps | 8 ++++---- .../models/com.mbeddr.formal.safety.gsn.structure.mps | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps index 573793cbe..0fc588cef 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.argument.spi/models/com.mbeddr.formal.safety.argument.spi.structure.mps @@ -50,7 +50,7 @@ - + @@ -67,7 +67,7 @@ - + @@ -100,7 +100,7 @@ - + @@ -126,7 +126,7 @@ - + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps index d990267d8..240c12f23 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.gsn/models/com.mbeddr.formal.safety.gsn.structure.mps @@ -472,7 +472,7 @@ - +