ifm24: Refresh projecs from fm24

README.md

@@ -111,8 +111,8 @@ MoDELS 15
 
 ### Using MMINT
 
-* <a name="paper-fm24"></a> Formal Foundations of Lifted Assurance Cases for Product Lines  
-FM 24 (submitted) | Install: `Examples > MMINT - FM24` | [Readme](examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/README.md)
+* <a name="paper-ifm24"></a> PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases  
+iFM 24 (submitted) | Install: `Examples > MMINT - IFM24` | [Readme](examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/README.md)
 * <a name="paper-sosym22"></a> [The ForeMoSt Approach to Building Valid Model-Based Safety Arguments](https://doi.org/10.1007/s10270-022-01063-4)  
 SoSyM Vol. 22-5 | Install: `Examples > MMINT - SOSYM22` | [Readme](examples/SOSYM22/edu.toronto.cs.se.mmint.examples.sosym22/SOSYM22/README.md)
 * [Validating Safety Arguments with Lean](https://doi.org/10.1007/978-3-030-92124-8_2)  

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/.project → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/.project

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
-	<name>edu.toronto.cs.se.mmint.examples.fm24</name>
+	<name>edu.toronto.cs.se.mmint.examples.ifm24</name>
 	<comment></comment>
 	<projects>
 	</projects>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/.project → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/.project

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
-	<name>FM24</name>
+	<name>IFM24</name>
 	<comment></comment>
 	<projects>
 	</projects>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/META-INF/MANIFEST.MF → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/META-INF/MANIFEST.MF

@@ -1,10 +1,10 @@
 Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
-Bundle-SymbolicName: FM24;singleton:=true
+Bundle-SymbolicName: IFM24;singleton:=true
 Bundle-Version: 2.21.99.qualifier
 Bundle-Vendor: %providerName
-Export-Package: fm24
+Export-Package: ifm24
 Require-Bundle: org.eclipse.emf.ecore,
  org.eclipse.viatra.query.runtime,
  org.eclipse.viatra.query.runtime.rete,
@@ -19,6 +19,6 @@ Require-Bundle: org.eclipse.emf.ecore,
  edu.toronto.cs.se.mmint.types.gsn.productline,
  edu.toronto.cs.se.modelepedia.statemachine
 Bundle-RequiredExecutionEnvironment: JavaSE-22
-Automatic-Module-Name: FM24
+Automatic-Module-Name: IFM24
 Import-Package: org.apache.log4j
 Bundle-ActivationPolicy: lazy

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/README.md → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/README.md

@@ -1,23 +1,23 @@
-## Formal Methods 2024 paper
+## Integrated Formal Methods 2024 paper
 
-Formal Foundations of Lifted Assurance Cases for Product Lines
+PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
 
 ### Instructions to reproduce the examples
 
 1. MMINT
     1. Install Java and Eclipse following the [requirements](/README.md#requirements) and add `https://adisandro.github.io/mmint/develop` to the list of software sites (`Help > Install New Software > Available Software Sites`).
-    2. From the top menu select `Help > Install New Software` and install `Examples > MMINT - FM24 paper`.
-    3. From the top menu select `File > New > Example > MMINT Examples > FM24`.
-    4. Open `/FM24/model/examples.middiag`.
+    2. From the top menu select `Help > Install New Software` and install `Examples > MMINT - IFM24 paper`.
+    3. From the top menu select `File > New > Example > MMINT Examples > IFM24`.
+    4. Open `/IFM24/model/examples.middiag`.
     5. Double-click on the yellow box named `ac : ProductLine` to open the PL AC. During any of the following steps, right-click in the diagram background and select `Layout > All` to automatically arrange all nodes.
 
 2. Querying AC template (Sec. 5.2)
-    1. Right-click in the diagram background, select `MMINT > Import Template`, select the template `/FM24/templates/QueryAnalysis.gsn`, select the analysis class `/FM24/src/fm24/VQLQueryAnalysis.java`.
+    1. Right-click in the diagram background, select `MMINT > Import Template`, select the template `/IFM24/templates/QueryAnalysis.gsn`, select the analysis class `/IFM24/src/ifm24/VQLQueryAnalysis.java`.
     2. Right-click on any of the imported nodes, select `MMINT > Instantiate Template`.
-    3. Insert the safety goal text `the system does not administer a dose`, select the PL model `/FM24/model/R1.productline`, select the query `/FM24/src/fm24/queries.vql`, select `Viatra for Product Lines`. The PL AC is populated with the results of the query analysis.
+    3. Insert the safety goal text `the system does not administer a dose`, select the PL model `/IFM24/model/R1.productline`, select the query `/IFM24/src/ifm24/queries.vql`, select `Viatra for Product Lines`. The PL AC is populated with the results of the query analysis.
 
 3. Model Checking AC template (Sec. 5.2)
-    1. Right-click in the diagram background, select `MMINT > Import Template`, select the template `/FM24/templates/ModelCheckingAnalysis.gsn`, select the analysis class `/FM24/src/fm24/FTS4VMCAnalysis.java`.
+    1. Right-click in the diagram background, select `MMINT > Import Template`, select the template `/IFM24/templates/ModelCheckingAnalysis.gsn`, select the analysis class `/IFM24/src/ifm24/FTS4VMCAnalysis.java`.
     2. (Ids refer to nodes from this template.) Click on the arrow between goal `G0` and strategy `S0`, press delete on your keyboard to delete it, click on the goal `G0`, press delete on your keyboard to delete it, from the palette on the right select `Create supported-by Link`, click on the goal with query result `Alrm_DoseRateHardLimitsViolationS`, click on the strategy `S0` to connect them.
     3. Right-click on any of the imported nodes from this template, select `MMINT > Instantiate Template`.
     4. (This step works only in Linux, requires Python installed, an internet connection, and takes a while to complete. It downloads and uses the FTS4VMC tool at https://github.com/fts4vmc/FTS4VMC.) Insert the property `AG(Alrm_DoseRateHardLimitsViolationS => A[not(Infusion_NormalOperationS) U (E_ClearAlarmS)])`. The check succeeds and the PL AC is populated with the results of the model checking analysis.

examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/model/examples.mid

@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<mid:MID xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:editor="http://se.cs.toronto.edu/mmint/MID/Editor" xmlns:file="http://se.cs.toronto.edu/mmint/File" xmlns:mid="http://se.cs.toronto.edu/mmint/MID">
+  <models uri="/IFM24/model/ac.productline" name="ac" metatypeUri="model://edu.toronto.cs.se.mmint.productline" dynamic="true" fileExtension="productline" editors="//@editors.0"/>
+  <models xsi:type="file:FileModel" uri="/IFM24/model/R1.txt" name="R1.txt" metatypeUri="http://se.cs.toronto.edu/mmint/File" dynamic="true" fileExtension="txt"/>
+  <models uri="/IFM24/model/R1.productline" name="R1" metatypeUri="model://edu.toronto.cs.se.mmint.productline" dynamic="true" origin="CREATED" fileExtension="productline" editors="//@editors.1"/>
+  <editors xsi:type="editor:Diagram" uri="/IFM24/representations.aird#_9lehsPeVEe67baVPhpR8qQ" name="ProductLine Sirius Diagram for model /IFM24/model/ac.productline" metatypeUri="edu.toronto.cs.se.mmint.productline.design" dynamic="true" modelUri="/IFM24/model/ac.productline" id="edu.toronto.cs.se.mmint.productline.design" wizardId="edu.toronto.cs.se.mmint.productline.presentation.ProductLineModelWizardID">
+    <fileExtensions>aird</fileExtensions>
+  </editors>
+  <editors uri="/IFM24/model/R1.productline" name="ProductLine EMF Editor for model /IFM24/model/R1.productline" metatypeUri="edu.toronto.cs.se.mmint.productline.editor" dynamic="true" modelUri="/IFM24/model/R1.productline" id="edu.toronto.cs.se.mmint.productline.presentation.PLEditorID" wizardId="edu.toronto.cs.se.mmint.productline.presentation.PLModelWizardID">
+    <fileExtensions>productline</fileExtensions>
+  </editors>
+  <operators uri="" name="ToProductLine" metatypeUri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine" dynamic="true" workingPath="/IFM24/model" executionTime="179087478">
+    <inputs uri="" name="product" metatypeUri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine/product" dynamic="true" lowerBound="1" upperBound="1" target="//@models.1"/>
+    <outputs uri="" name="productLine" metatypeUri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine/productLine" dynamic="true" lowerBound="1" upperBound="1" target="//@models.2"/>
+  </operators>
+  <extendibleTable key="/IFM24/model/ac.productline" value="//@models.0"/>
+  <extendibleTable key="/IFM24/model/R1.txt" value="//@models.1"/>
+  <extendibleTable key="/IFM24/model/R1.productline" value="//@models.2"/>
+</mid:MID>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/plugin.properties → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/plugin.properties

@@ -10,5 +10,5 @@
 # Contributors:
 #     Alessio Di Sandro - Implementation
 ###############################################################################
-pluginName = FM24 example artifacts
+pluginName = IFM24 example artifacts
 providerName = Software Engineering Group, University of Toronto

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/plugin.xml → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/plugin.xml

@@ -10,9 +10,9 @@
     Contributors:
         Alessio Di Sandro - Implementation
  --><plugin>
-  <extension id="fm24.Queries" point="org.eclipse.viatra.query.runtime.queryspecification">
-    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:fm24.Queries" id="fm24.Queries">
-      <query-specification fqn="fm24.alarmStates"/>
+  <extension id="ifm24.Queries" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ifm24.Queries" id="ifm24.Queries">
+      <query-specification fqn="ifm24.alarmStates"/>
     </group>
   </extension>
 </plugin>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/src-gen/fm24/AlarmStates.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/src-gen/ifm24/AlarmStates.java

@@ -12,7 +12,7 @@
  *       Alessio Di Sandro - Implementation
  *  
  */
-package fm24;
+package ifm24;
 
 import edu.toronto.cs.se.modelepedia.statemachine.State;
 import java.util.Arrays;
@@ -72,7 +72,7 @@
 @SuppressWarnings("all")
 public final class AlarmStates extends BaseGeneratedEMFQuerySpecification<AlarmStates.Matcher> {
   /**
-   * Pattern-specific match representation of the fm24.alarmStates pattern,
+   * Pattern-specific match representation of the ifm24.alarmStates pattern,
    * to be used in conjunction with {@link Matcher}.
    * 
    * <p>Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned.
@@ -129,7 +129,7 @@ public void setState(final State pState) {
 
     @Override
     public String patternName() {
-      return "fm24.alarmStates";
+      return "ifm24.alarmStates";
     }
 
     @Override
@@ -243,7 +243,7 @@ public boolean isMutable() {
   }
 
   /**
-   * Generated pattern matcher API of the fm24.alarmStates pattern,
+   * Generated pattern matcher API of the ifm24.alarmStates pattern,
    * providing pattern-specific query methods.
    * 
    * <p>Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)},
@@ -533,7 +533,7 @@ private GeneratedPQuery() {
 
     @Override
     public String getFullyQualifiedName() {
-      return "fm24.alarmStates";
+      return "ifm24.alarmStates";
     }
 
     @Override

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/src-gen/fm24/Queries.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/src-gen/ifm24/Queries.java

@@ -12,7 +12,7 @@
  *       Alessio Di Sandro - Implementation
  *  
  */
-package fm24;
+package ifm24;
 
 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
 import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedPatternGroup;
@@ -24,7 +24,7 @@
  * a VIATRA Query engine for matching all patterns originally defined in file queries.vql,
  * in order to achieve better performance than one-by-one on-demand matcher initialization.
  * 
- * <p> From package fm24, the group contains the definition of the following patterns: <ul>
+ * <p> From package ifm24, the group contains the definition of the following patterns: <ul>
  * <li>alarmStates</li>
  * </ul>
  * 

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/src/fm24/FTS4VMCAnalysis.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/src/ifm24/FTS4VMCAnalysis.java

@@ -10,7 +10,7 @@
  * Contributors:
  *     Alessio Di Sandro - Implementation
  *******************************************************************************/
-package fm24;
+package ifm24;
 
 import java.nio.file.Files;
 import java.nio.file.Paths;

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/src/fm24/VQLQueryAnalysis.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/src/ifm24/VQLQueryAnalysis.java

@@ -10,7 +10,7 @@
  * Contributors:
  *     Alessio Di Sandro - Implementation
  *******************************************************************************/
-package fm24;
+package ifm24;
 
 import java.util.List;
 import java.util.Set;

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/FM24/src/fm24/queries.vql → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/IFM24/src/ifm24/queries.vql

@@ -10,7 +10,7 @@
  * Contributors:
  *     Alessio Di Sandro - Implementation
  *******************************************************************************/
-package fm24
+package ifm24
 
 import "http://se.cs.toronto.edu/modelepedia/StateMachine"
 

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/META-INF/MANIFEST.MF → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/META-INF/MANIFEST.MF

@@ -1,9 +1,9 @@
 Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: %pluginName
-Bundle-SymbolicName: edu.toronto.cs.se.mmint.examples.fm24;singleton:=true
+Bundle-SymbolicName: edu.toronto.cs.se.mmint.examples.ifm24;singleton:=true
 Bundle-Version: 2.21.99.qualifier
-Automatic-Module-Name: edu.toronto.cs.se.mmint.examples.fm24
+Automatic-Module-Name: edu.toronto.cs.se.mmint.examples.ifm24
 Bundle-RequiredExecutionEnvironment: JavaSE-22
 Bundle-Vendor: %providerName
 Bundle-ActivationPolicy: lazy

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/build.properties → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/build.properties

@@ -15,6 +15,6 @@ output.. = target/classes/
 bin.includes = META-INF/,\
                .,\
                plugin.xml,\
-               FM24/,\
+               IFM24/,\
                plugin.properties
 

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/plugin.properties → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/plugin.properties

@@ -10,6 +10,6 @@
 # Contributors:
 #     Alessio Di Sandro - Implementation
 ###############################################################################
-pluginName = FM24 example
+pluginName = IFM24 example
 providerName = Software Engineering Group, University of Toronto
 

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/plugin.xml → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/plugin.xml

@@ -20,22 +20,22 @@
       <category id="edu.toronto.cs.se.mmint.example"
             name="MMINT Examples"
             parentCategory="org.eclipse.ui.Examples"/>
-      <wizard id="edu.toronto.cs.se.mmint.examples.fm24"
+      <wizard id="edu.toronto.cs.se.mmint.examples.ifm24"
             category="org.eclipse.ui.Examples/edu.toronto.cs.se.mmint.example"
             class="org.eclipse.emf.common.ui.wizard.ExampleInstallerWizard"
             project="true"
-            name="FM24">
-         <description>Creates a project containing the artifacts from the FM24 paper</description>
+            name="IFM24">
+         <description>Creates a project containing the artifacts from the IFM24 paper</description>
       </wizard>
    </extension>
 
    <extension point="org.eclipse.emf.common.ui.examples">
-      <example id="edu.toronto.cs.se.mmint.examples.fm24"
-            wizardID="edu.toronto.cs.se.mmint.examples.fm24">
-         <projectDescriptor name="FM24"
-               contentURI="FM24/"
-               description="Creates a project containing the artifacts from the FM24 paper"/>
-         <fileToOpen location="FM24/README.md"/>
+      <example id="edu.toronto.cs.se.mmint.examples.ifm24"
+            wizardID="edu.toronto.cs.se.mmint.examples.ifm24">
+         <projectDescriptor name="IFM24"
+               contentURI="IFM24/"
+               description="Creates a project containing the artifacts from the IFM24 paper"/>
+         <fileToOpen location="IFM24/README.md"/>
       </example>
    </extension>
 
@@ -44,8 +44,8 @@
       <operatorType>
          <type
                name="ToProductLine"
-               uri="edu.toronto.cs.se.mmint.examples.fm24.operators.TextFileToSMProductLine"
-               class="edu.toronto.cs.se.mmint.examples.fm24.operators.TextFileToSMProductLine">
+               uri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine"
+               class="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine">
             <superType
                   uri="edu.toronto.cs.se.mmint.productline.operators.ToProductLine">
             </superType>
@@ -54,7 +54,7 @@
             <parameter>
                <type
                      name="product"
-                     uri="edu.toronto.cs.se.mmint.examples.fm24.operators.TextFileToSMProductLine/product">
+                     uri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine/product">
                   <superType
                         uri="edu.toronto.cs.se.mmint.productline.operators.ToProductLine/product">
                   </superType>
@@ -68,7 +68,7 @@
             <parameter>
                <type
                      name="productLine"
-                     uri="edu.toronto.cs.se.mmint.examples.fm24.operators.TextFileToSMProductLine/productLine">
+                     uri="edu.toronto.cs.se.mmint.examples.ifm24.operators.TextFileToSMProductLine/productLine">
                   <superType
                         uri="edu.toronto.cs.se.mmint.productline.operators.ToProductLine/productLine">
                   </superType>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/pom.xml → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/pom.xml

@@ -12,7 +12,7 @@
 -->
 <project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/xsd/maven-4.0.0.xsd">
   <modelVersion>4.0.0</modelVersion>
-  <artifactId>edu.toronto.cs.se.mmint.examples.fm24</artifactId>
+  <artifactId>edu.toronto.cs.se.mmint.examples.ifm24</artifactId>
   <packaging>eclipse-plugin</packaging>
   <parent>
   	<groupId>MMINT</groupId>

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/src/edu/toronto/cs/se/mmint/examples/fm24/operators/TextFileToSMProductLine.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/src/edu/toronto/cs/se/mmint/examples/ifm24/operators/TextFileToSMProductLine.java

@@ -10,7 +10,7 @@
  * Contributors:
  *     Alessio Di Sandro - Implementation
  *******************************************************************************/
-package edu.toronto.cs.se.mmint.examples.fm24.operators;
+package edu.toronto.cs.se.mmint.examples.ifm24.operators;
 
 import java.io.IOException;
 import java.nio.file.Files;

examples/FM24/edu.toronto.cs.se.mmint.examples.fm24/src/edu/toronto/cs/se/mmint/examples/fm24/operators/package-info.java → examples/IFM24/edu.toronto.cs.se.mmint.examples.ifm24/src/edu/toronto/cs/se/mmint/examples/ifm24/operators/package-info.java

@@ -11,6 +11,6 @@
  *     Alessio Di Sandro - Implementation
  *******************************************************************************/
 @NonNullByDefault
-package edu.toronto.cs.se.mmint.examples.fm24.operators;
+package edu.toronto.cs.se.mmint.examples.ifm24.operators;
 
 import org.eclipse.jdt.annotation.NonNullByDefault;

features/edu.toronto.cs.se.mmint.examples.fm24.feature/.project → features/edu.toronto.cs.se.mmint.examples.ifm24.feature/.project

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
-	<name>edu.toronto.cs.se.mmint.examples.fm24.feature</name>
+	<name>edu.toronto.cs.se.mmint.examples.ifm24.feature</name>
 	<comment></comment>
 	<projects>
 	</projects>