From 40f6822c178cbaa36222b56b971c666d33cfffc2 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:28:30 +0200
Subject: [PATCH 01/20] #424 CIF to mCRL2 precond chk: add new class. No checks
 for now.

---
 .../META-INF/MANIFEST.MF                      |  3 +-
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java   | 31 +++++++++++++++++++
 2 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF b/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF
index f19987d34c..3672a29105 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/META-INF/MANIFEST.MF
@@ -20,7 +20,8 @@ Require-Bundle: org.eclipse.ui;bundle-version="3.115.0",
  org.eclipse.escet.cif.metamodel.java;bundle-version="5.0.0",
  org.eclipse.escet.cif.common;bundle-version="5.0.0",
  org.apache.commons.lang3;bundle-version="3.1.0",
- org.eclipse.escet.common.box;bundle-version="5.0.0"
+ org.eclipse.escet.common.box;bundle-version="5.0.0",
+ org.eclipse.escet.cif.checkers;bundle-version="5.0.0"
 Import-Package: org.junit.jupiter.api;version="5.9.2"
 Bundle-RequiredExecutionEnvironment: JavaSE-17
 Bundle-ActivationPolicy: lazy
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
new file mode 100644
index 0000000000..968f093926
--- /dev/null
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -0,0 +1,31 @@
+//////////////////////////////////////////////////////////////////////////////
+// Copyright (c) 2010, 2024 Contributors to the Eclipse Foundation
+//
+// See the NOTICE file(s) distributed with this work for additional
+// information regarding copyright ownership.
+//
+// This program and the accompanying materials are made available
+// under the terms of the MIT License which is available at
+// https://opensource.org/licenses/MIT
+//
+// SPDX-License-Identifier: MIT
+//////////////////////////////////////////////////////////////////////////////
+
+package org.eclipse.escet.cif.cif2mcrl2;
+
+import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
+import org.eclipse.escet.common.java.Termination;
+
+/** CIF to mCRL2 transformation precondition checker. */
+public class CifToMcrl2PreChecker extends CifPreconditionChecker {
+    /**
+     * Constructor for the {@link CifToMcrl2PreChecker} class.
+     *
+     * @param termination Cooperative termination query function.
+     */
+    public CifToMcrl2PreChecker(Termination termination) {
+        super(termination
+
+        );
+    }
+}
-- 
GitLab


From 1fe87739162da2d7fb06e9a58760e3b4574d8308 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:41:58 +0200
Subject: [PATCH 02/20] #424 CIF to mCRL2 preconds move: only bool/int/enum
 types.

---
 .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java |  9 ---------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java      | 16 +++++++++++++++-
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 9401ab118e..13d9748eee 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -144,13 +144,6 @@ public class Cif2Mcrl2PreChecker {
         for (Declaration decl: aut.getDeclarations()) {
             if (decl instanceof DiscVariable) {
                 DiscVariable dv = (DiscVariable)decl;
-                CifType tp = CifTypeUtils.normalizeType(dv.getType());
-                if (!(tp instanceof BoolType) && !(tp instanceof IntType) && !(tp instanceof EnumType)) {
-                    msg = fmt("Discrete variable \"%s\" does not have a boolean, integer, or enumeration type.",
-                            CifTextUtils.getAbsName(dv));
-                    problems.add(msg);
-                    continue;
-                }
 
                 if (dv.getValue().getValues().size() != 1) {
                     msg = fmt("Discrete variable \"%s\" does not have a single initial value.",
@@ -362,8 +355,6 @@ public class Cif2Mcrl2PreChecker {
             return fmt("has unsupported enumeration expression \"%s\".", CifTextUtils.exprToStr(e));
         }
 
-        String msg = CifTextUtils.typeToStr(t);
-        return fmt("has an unsupported type \"%s\" in expression \"%s\".", msg, CifTextUtils.exprToStr(e));
     }
 
     /**
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 968f093926..ca251e933b 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -14,6 +14,8 @@
 package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
+import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
+import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.common.java.Termination;
 
 /** CIF to mCRL2 transformation precondition checker. */
@@ -24,7 +26,19 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
      * @param termination Cooperative termination query function.
      */
     public CifToMcrl2PreChecker(Termination termination) {
-        super(termination
+        super(termination,
+
+                // Only boolean, integer and enumeration types are supported.
+                new TypeNoSpecificTypesCheck(
+                        NoSpecificType.COMP_TYPES,
+                        NoSpecificType.DICT_TYPES,
+                        NoSpecificType.DIST_TYPES,
+                        NoSpecificType.FUNC_TYPES,
+                        NoSpecificType.LIST_TYPES,
+                        NoSpecificType.REAL_TYPES,
+                        NoSpecificType.SET_TYPES,
+                        NoSpecificType.STRING_TYPES,
+                        NoSpecificType.TUPLE_TYPES)
 
         );
     }
-- 
GitLab


From d362543c7ea0174c93ec78b7618f57d9cfacb230 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:44:19 +0200
Subject: [PATCH 03/20] #424 CIF to mCRL2 preconds move: disc var at most one
 initial value.

---
 .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java   | 7 -------
 .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java  | 6 +++++-
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 13d9748eee..6756620894 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -145,13 +145,6 @@ public class Cif2Mcrl2PreChecker {
             if (decl instanceof DiscVariable) {
                 DiscVariable dv = (DiscVariable)decl;
 
-                if (dv.getValue().getValues().size() != 1) {
-                    msg = fmt("Discrete variable \"%s\" does not have a single initial value.",
-                            CifTextUtils.getAbsName(dv));
-                    problems.add(msg);
-                    continue;
-                }
-
                 try {
                     CifEvalUtils.eval(dv.getValue().getValues().get(0), true);
                 } catch (CifEvalException err) {
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index ca251e933b..b38d8a7d3e 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
+import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck;
 import org.eclipse.escet.common.java.Termination;
 
 /** CIF to mCRL2 transformation precondition checker. */
@@ -38,7 +39,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                         NoSpecificType.REAL_TYPES,
                         NoSpecificType.SET_TYPES,
                         NoSpecificType.STRING_TYPES,
-                        NoSpecificType.TUPLE_TYPES)
+                        NoSpecificType.TUPLE_TYPES),
+
+                // Discrete variables must not have multiple potential initial values.
+                new VarNoDiscWithMultiInitValuesCheck()
 
         );
     }
-- 
GitLab


From 6bfe3b514401f8b9e57209ee956b16e62d9d6ecb Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:46:41 +0200
Subject: [PATCH 04/20] #424 CIF to mCRL2 preconds move: disc var initial value
 static eval.

---
 .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java | 16 ----------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java      |  6 +++++-
 2 files changed, 5 insertions(+), 17 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 6756620894..c3f15d58c5 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -140,22 +140,6 @@ public class Cif2Mcrl2PreChecker {
 
         checkComponent(aut);
 
-        // Check type of the discrete variables. Only support Boolean, (ranged) integer and enumeration types.
-        for (Declaration decl: aut.getDeclarations()) {
-            if (decl instanceof DiscVariable) {
-                DiscVariable dv = (DiscVariable)decl;
-
-                try {
-                    CifEvalUtils.eval(dv.getValue().getValues().get(0), true);
-                } catch (CifEvalException err) {
-                    msg = fmt("Initial value of discrete variable \"%s\" cannot be evaluated.",
-                            CifTextUtils.getAbsName(dv));
-                    problems.add(msg);
-                    continue;
-                }
-            }
-        }
-
         // Check locations.
         for (Location loc: aut.getLocations()) {
             String locTextMid = CifTextUtils.getLocationText2(loc);
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index b38d8a7d3e..c2451b2c33 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
+import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck;
 import org.eclipse.escet.common.java.Termination;
 
@@ -42,7 +43,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                         NoSpecificType.TUPLE_TYPES),
 
                 // Discrete variables must not have multiple potential initial values.
-                new VarNoDiscWithMultiInitValuesCheck()
+                new VarNoDiscWithMultiInitValuesCheck(),
+
+                // Initial values of discrete variables must be statically evaluable.
+                new VarDiscOnlyStaticEvalInitCheck()
 
         );
     }
-- 
GitLab


From 3c37b062baee1ea02969eeded511e23b7fdd7d99 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:48:07 +0200
Subject: [PATCH 05/20] #424 CIF to mCRL2 preconds move: no continuous
 variables.

---
 .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 6 ------
 .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java   | 6 +++++-
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index c3f15d58c5..1427a9b467 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -40,7 +40,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.cif.metamodel.cif.automata.Update;
 import org.eclipse.escet.cif.metamodel.cif.declarations.AlgVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.Constant;
-import org.eclipse.escet.cif.metamodel.cif.declarations.ContVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration;
 import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl;
@@ -351,11 +350,6 @@ public class Cif2Mcrl2PreChecker {
                 continue;
             } else if (decl instanceof Event) {
                 continue;
-            } else if (decl instanceof ContVariable) {
-                msg = fmt("Continuous variable \"%s\" is unsupported in the transformation.",
-                        CifTextUtils.getAbsName(decl));
-                problems.add(msg);
-                continue;
             } else if (decl instanceof Function) {
                 continue;
             } else if (decl instanceof TypeDecl) {
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index c2451b2c33..10203a762f 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -17,6 +17,7 @@ import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
+import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck;
 import org.eclipse.escet.common.java.Termination;
 
@@ -46,7 +47,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new VarNoDiscWithMultiInitValuesCheck(),
 
                 // Initial values of discrete variables must be statically evaluable.
-                new VarDiscOnlyStaticEvalInitCheck()
+                new VarDiscOnlyStaticEvalInitCheck(),
+
+                // Continuous variables are not supported.
+                new VarNoContinuousCheck()
 
         );
     }
-- 
GitLab


From 15f224ade6a8391bfa52f1adc94798083c3c6713 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:49:46 +0200
Subject: [PATCH 06/20] #424 CIF to mCRL2 preconds move: no input variables.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 36 -------------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java   |  6 +++-
 2 files changed, 5 insertions(+), 37 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 1427a9b467..d500a193d7 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -44,7 +44,6 @@ import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration;
 import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl;
 import org.eclipse.escet.cif.metamodel.cif.declarations.Event;
-import org.eclipse.escet.cif.metamodel.cif.declarations.InputVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.TypeDecl;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression;
@@ -333,39 +332,6 @@ public class Cif2Mcrl2PreChecker {
 
     }
 
-    /**
-     * Check that only supported declarations exist.
-     *
-     * @param decls Declarations to inspect.
-     */
-    private void checkDeclarations(List<Declaration> decls) {
-        String msg;
-
-        for (Declaration decl: decls) {
-            if (decl instanceof AlgVariable) {
-                // Eliminated during preprocessing.
-            } else if (decl instanceof Constant) {
-                // Eliminated during preprocessing.
-            } else if (decl instanceof EnumDecl) {
-                continue;
-            } else if (decl instanceof Event) {
-                continue;
-            } else if (decl instanceof Function) {
-                continue;
-            } else if (decl instanceof TypeDecl) {
-                continue;
-            } else if (decl instanceof DiscVariable) {
-                continue;
-            } else if (decl instanceof InputVariable) {
-                msg = fmt("Input variable \"%s\" is unsupported in the transformation.", CifTextUtils.getAbsName(decl));
-                problems.add(msg);
-                continue;
-            }
-
-            throw new RuntimeException("Unexpected type of CIF declaration.");
-        }
-    }
-
     /**
      * Verify that the given component does not have elements that are not supported in the translation.
      *
@@ -377,8 +343,6 @@ public class Cif2Mcrl2PreChecker {
         // IO declarations should be eliminated already.
         Assert.check(comp.getIoDecls().isEmpty());
 
-        checkDeclarations(comp.getDeclarations());
-
         if (!comp.getEquations().isEmpty()) {
             msg = fmt("Equations are not supported in %s.", CifTextUtils.getComponentText2(comp));
             problems.add(msg);
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 10203a762f..f025cc5452 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -19,6 +19,7 @@ import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecific
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck;
+import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck;
 import org.eclipse.escet.common.java.Termination;
 
 /** CIF to mCRL2 transformation precondition checker. */
@@ -50,7 +51,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new VarDiscOnlyStaticEvalInitCheck(),
 
                 // Continuous variables are not supported.
-                new VarNoContinuousCheck()
+                new VarNoContinuousCheck(),
+
+                // Input variables are not supported.
+                new VarNoInputCheck()
 
         );
     }
-- 
GitLab


From 1ad27018e82e7adf88dd7bb2bf47a54b689664c1 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:50:43 +0200
Subject: [PATCH 07/20] #424 CIF to mCRL2 preconds move: no equations.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java     | 18 ------------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java    |  6 +++++-
 2 files changed, 5 insertions(+), 19 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index d500a193d7..ce87d3e5d0 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -20,8 +20,6 @@ import java.util.Collections;
 import java.util.List;
 
 import org.apache.commons.lang3.StringUtils;
-import org.eclipse.escet.cif.common.CifEvalException;
-import org.eclipse.escet.cif.common.CifEvalUtils;
 import org.eclipse.escet.cif.common.CifTextUtils;
 import org.eclipse.escet.cif.common.CifTypeUtils;
 import org.eclipse.escet.cif.common.CifValueUtils;
@@ -38,13 +36,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.EdgeSend;
 import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate;
 import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.cif.metamodel.cif.automata.Update;
-import org.eclipse.escet.cif.metamodel.cif.declarations.AlgVariable;
-import org.eclipse.escet.cif.metamodel.cif.declarations.Constant;
-import org.eclipse.escet.cif.metamodel.cif.declarations.Declaration;
-import org.eclipse.escet.cif.metamodel.cif.declarations.DiscVariable;
-import org.eclipse.escet.cif.metamodel.cif.declarations.EnumDecl;
-import org.eclipse.escet.cif.metamodel.cif.declarations.Event;
-import org.eclipse.escet.cif.metamodel.cif.declarations.TypeDecl;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression;
@@ -54,7 +45,6 @@ import org.eclipse.escet.cif.metamodel.cif.expressions.Expression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.TauExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression;
-import org.eclipse.escet.cif.metamodel.cif.functions.Function;
 import org.eclipse.escet.cif.metamodel.cif.types.BoolType;
 import org.eclipse.escet.cif.metamodel.cif.types.CifType;
 import org.eclipse.escet.cif.metamodel.cif.types.EnumType;
@@ -147,10 +137,6 @@ public class Cif2Mcrl2PreChecker {
                 msg = locTextStart + " has invariants.";
                 problems.add(msg);
             }
-            if (!loc.getEquations().isEmpty()) {
-                msg = locTextStart + " has equations.";
-                problems.add(msg);
-            }
             for (Edge edge: loc.getEdges()) {
                 for (Update upd: edge.getUpdates()) {
                     if (upd instanceof IfUpdate) {
@@ -343,10 +329,6 @@ public class Cif2Mcrl2PreChecker {
         // IO declarations should be eliminated already.
         Assert.check(comp.getIoDecls().isEmpty());
 
-        if (!comp.getEquations().isEmpty()) {
-            msg = fmt("Equations are not supported in %s.", CifTextUtils.getComponentText2(comp));
-            problems.add(msg);
-        }
         if (!comp.getInitials().isEmpty()) {
             msg = fmt("Initialization predicates are not supported in %s.", CifTextUtils.getComponentText2(comp));
             problems.add(msg);
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index f025cc5452..4dc2c9b71b 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -14,6 +14,7 @@
 package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
+import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
@@ -54,7 +55,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new VarNoContinuousCheck(),
 
                 // Input variables are not supported.
-                new VarNoInputCheck()
+                new VarNoInputCheck(),
+
+                // Equations are not supported.
+                new EqnNotAllowedCheck()
 
         );
     }
-- 
GitLab


From f507877f7ff998aaaf759155273aa1429addd668 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:52:34 +0200
Subject: [PATCH 08/20] #424 CIF to mCRL2 preconds move: no channels.

---
 .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java     | 12 +-----------
 .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java    |  6 +++++-
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index ce87d3e5d0..36ad71f453 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -31,8 +31,6 @@ import org.eclipse.escet.cif.metamodel.cif.automata.Assignment;
 import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
 import org.eclipse.escet.cif.metamodel.cif.automata.Edge;
 import org.eclipse.escet.cif.metamodel.cif.automata.EdgeEvent;
-import org.eclipse.escet.cif.metamodel.cif.automata.EdgeReceive;
-import org.eclipse.escet.cif.metamodel.cif.automata.EdgeSend;
 import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate;
 import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.cif.metamodel.cif.automata.Update;
@@ -173,15 +171,7 @@ public class Cif2Mcrl2PreChecker {
                     continue;
                 }
                 for (EdgeEvent ee: edge.getEvents()) {
-                    if (ee instanceof EdgeSend) {
-                        msg = locTextStart + " has a send edge.";
-                        problems.add(msg);
-                        continue;
-                    } else if (ee instanceof EdgeReceive) {
-                        msg = locTextStart + " has a receive edge.";
-                        problems.add(msg);
-                        continue;
-                    } else if (ee.getEvent() instanceof TauExpression) {
+                    if (ee.getEvent() instanceof TauExpression) {
                         msg = locTextStart + " has a \"tau\" event.";
                         problems.add(msg);
                         continue;
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 4dc2c9b71b..efa873e175 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
+import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
@@ -58,7 +59,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new VarNoInputCheck(),
 
                 // Equations are not supported.
-                new EqnNotAllowedCheck()
+                new EqnNotAllowedCheck(),
+
+                // Channels are not supported.
+                new EventNoChannelsCheck()
 
         );
     }
-- 
GitLab


From f2060f2d6f82a6788b3a1ac1381e9e0b28d7de6c Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:53:34 +0200
Subject: [PATCH 09/20] #424 CIF to mCRL2 preconds move: no tau.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java      | 17 -----------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java     |  6 +++++-
 2 files changed, 5 insertions(+), 18 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 36ad71f453..4c81c30278 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -30,7 +30,6 @@ import org.eclipse.escet.cif.metamodel.cif.Specification;
 import org.eclipse.escet.cif.metamodel.cif.automata.Assignment;
 import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
 import org.eclipse.escet.cif.metamodel.cif.automata.Edge;
-import org.eclipse.escet.cif.metamodel.cif.automata.EdgeEvent;
 import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate;
 import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.cif.metamodel.cif.automata.Update;
@@ -38,10 +37,8 @@ import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.EnumLiteralExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.EventExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.Expression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.TauExpression;
 import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression;
 import org.eclipse.escet.cif.metamodel.cif.types.BoolType;
 import org.eclipse.escet.cif.metamodel.cif.types.CifType;
@@ -164,20 +161,6 @@ public class Cif2Mcrl2PreChecker {
                         problems.add(msg);
                     }
                 }
-
-                if (edge.getEvents().isEmpty()) {
-                    msg = locTextStart + " has a \"tau\" event.";
-                    problems.add(msg);
-                    continue;
-                }
-                for (EdgeEvent ee: edge.getEvents()) {
-                    if (ee.getEvent() instanceof TauExpression) {
-                        msg = locTextStart + " has a \"tau\" event.";
-                        problems.add(msg);
-                        continue;
-                    }
-                    Assert.check(ee.getEvent() instanceof EventExpression);
-                }
             }
         }
 
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index efa873e175..4f5b232149 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -16,6 +16,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
+import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
@@ -62,7 +63,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new EqnNotAllowedCheck(),
 
                 // Channels are not supported.
-                new EventNoChannelsCheck()
+                new EventNoChannelsCheck(),
+
+                // 'Tau' events are not supported.
+                new EventNoTauCheck()
 
         );
     }
-- 
GitLab


From 8528a199f356e0ec7e3e425fdf61100d4305cd34 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:56:13 +0200
Subject: [PATCH 10/20] #424 CIF to mCRL2 preconds move: at least one
 automaton.

---
 .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java     | 12 +++---------
 .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java    |  6 +++++-
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 4c81c30278..d895133836 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -67,9 +67,7 @@ public class Cif2Mcrl2PreChecker {
      */
     public void checkSpec(Specification spec) {
         problems = list();
-        if (!checkGroup(spec)) {
-            problems.add("Specification must have at least one automaton.");
-        }
+        checkGroup(spec);
 
         if (problems.isEmpty()) {
             return;
@@ -87,30 +85,26 @@ public class Cif2Mcrl2PreChecker {
      * Unfold and check a group.
      *
      * @param grp Group to check and unfold.
-     * @return Whether at least one automaton was found in the group.
      */
-    private boolean checkGroup(Group grp) {
+    private void checkGroup(Group grp) {
         // Definitions should be eliminated already.
         Assert.check(grp.getDefinitions().isEmpty());
         checkComponent(grp);
 
-        boolean foundAut = false;
         for (Component c: grp.getComponents()) {
             if (c instanceof Automaton) {
-                foundAut = true;
                 Automaton aut = (Automaton)c;
                 checkAutomaton(aut);
                 continue;
             } else if (c instanceof Group) {
                 Group g = (Group)c;
-                foundAut |= checkGroup(g);
+                checkGroup(g);
                 continue;
             }
 
             // ComponentInst should not happen, as DefInst has been eliminated.
             throw new RuntimeException("Unexpected type of Component.");
         }
-        return foundAut;
     }
 
     /**
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 4f5b232149..c6820f8bcd 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -17,6 +17,7 @@ import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck;
+import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
 import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
@@ -66,7 +67,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new EventNoChannelsCheck(),
 
                 // 'Tau' events are not supported.
-                new EventNoTauCheck()
+                new EventNoTauCheck(),
+
+                // There must be at least one automaton.
+                new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE)
 
         );
     }
-- 
GitLab


From 03c3e86fd49fad439dec9039434e6742b05db33c Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 11:59:09 +0200
Subject: [PATCH 11/20] #424 CIF to mCRL2 preconds move: automata exactly one
 initial location.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 19 -------------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java   |  6 +++++-
 2 files changed, 5 insertions(+), 20 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index d895133836..0dc82136a5 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -22,7 +22,6 @@ import java.util.List;
 import org.apache.commons.lang3.StringUtils;
 import org.eclipse.escet.cif.common.CifTextUtils;
 import org.eclipse.escet.cif.common.CifTypeUtils;
-import org.eclipse.escet.cif.common.CifValueUtils;
 import org.eclipse.escet.cif.metamodel.cif.ComplexComponent;
 import org.eclipse.escet.cif.metamodel.cif.Component;
 import org.eclipse.escet.cif.metamodel.cif.Group;
@@ -157,24 +156,6 @@ public class Cif2Mcrl2PreChecker {
                 }
             }
         }
-
-        // Check the number of initial locations.
-        int initLocCount = 0;
-        for (Location loc: aut.getLocations()) {
-            if (!loc.getInitials().isEmpty() && CifValueUtils.isTriviallyTrue(loc.getInitials(), true, true)) {
-                initLocCount++;
-            }
-        }
-
-        if (initLocCount == 0) {
-            msg = fmt("Automaton \"%s\" has no initial location.", CifTextUtils.getAbsName(aut));
-            problems.add(msg);
-        }
-
-        if (initLocCount > 1) {
-            msg = fmt("Automaton \"%s\" has more than one initial location.", CifTextUtils.getAbsName(aut));
-            problems.add(msg);
-        }
     }
 
     /**
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index c6820f8bcd..803cd602ba 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -14,6 +14,7 @@
 package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
+import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck;
@@ -70,7 +71,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new EventNoTauCheck(),
 
                 // There must be at least one automaton.
-                new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE)
+                new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE),
+
+                // Exactly one initial location per automaton.
+                new AutOnlyWithOneInitLocCheck()
 
         );
     }
-- 
GitLab


From db0f8d5798e69b68e8c5cf24fd6e434f147f4341 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:01:15 +0200
Subject: [PATCH 12/20] #424 CIF to mCRL2 preconds move: only simple
 assignments.

---
 .../escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java   | 14 --------------
 .../escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java  |  6 +++++-
 2 files changed, 5 insertions(+), 15 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 0dc82136a5..5a46919398 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -29,7 +29,6 @@ import org.eclipse.escet.cif.metamodel.cif.Specification;
 import org.eclipse.escet.cif.metamodel.cif.automata.Assignment;
 import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
 import org.eclipse.escet.cif.metamodel.cif.automata.Edge;
-import org.eclipse.escet.cif.metamodel.cif.automata.IfUpdate;
 import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.cif.metamodel.cif.automata.Update;
 import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression;
@@ -127,25 +126,12 @@ public class Cif2Mcrl2PreChecker {
             }
             for (Edge edge: loc.getEdges()) {
                 for (Update upd: edge.getUpdates()) {
-                    if (upd instanceof IfUpdate) {
-                        msg = locTextStart + " has conditional updates.";
-                        problems.add(msg);
-                        continue;
-                    }
-
                     Assignment asg = (Assignment)upd;
                     msg = checkExpression(asg.getValue());
                     if (msg != null) {
                         msg = fmt("A value in %s %s", locTextMid, msg);
                         problems.add(msg);
                     }
-
-                    Expression e = asg.getAddressable();
-                    if (!(e instanceof DiscVariableExpression)) {
-                        msg = fmt("An assignment in %s assigns to unsupported addressable form \"%s\".", locTextMid,
-                                CifTextUtils.exprToStr(e));
-                        problems.add(msg);
-                    }
                 }
                 for (Expression e: edge.getGuards()) {
                     msg = checkExpression(e);
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 803cd602ba..ca318839b8 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck;
+import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck;
@@ -74,7 +75,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new SpecAutomataCountsCheck().setMinMaxAuts(1, SpecAutomataCountsCheck.NO_CHANGE),
 
                 // Exactly one initial location per automaton.
-                new AutOnlyWithOneInitLocCheck()
+                new AutOnlyWithOneInitLocCheck(),
+
+                // No conditional updates and multi-assignments.
+                new EdgeOnlySimpleAssignmentsCheck()
 
         );
     }
-- 
GitLab


From a6278446492c97f17a6ff6f03e42a2a817006d1a Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:37:07 +0200
Subject: [PATCH 13/20] #424 CIF to mCRL2 preconds move: only supported
 expressions.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 140 ------------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java   |  77 +++++++++-
 2 files changed, 76 insertions(+), 141 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 5a46919398..a52e396637 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -21,27 +21,12 @@ import java.util.List;
 
 import org.apache.commons.lang3.StringUtils;
 import org.eclipse.escet.cif.common.CifTextUtils;
-import org.eclipse.escet.cif.common.CifTypeUtils;
 import org.eclipse.escet.cif.metamodel.cif.ComplexComponent;
 import org.eclipse.escet.cif.metamodel.cif.Component;
 import org.eclipse.escet.cif.metamodel.cif.Group;
 import org.eclipse.escet.cif.metamodel.cif.Specification;
-import org.eclipse.escet.cif.metamodel.cif.automata.Assignment;
 import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
-import org.eclipse.escet.cif.metamodel.cif.automata.Edge;
 import org.eclipse.escet.cif.metamodel.cif.automata.Location;
-import org.eclipse.escet.cif.metamodel.cif.automata.Update;
-import org.eclipse.escet.cif.metamodel.cif.expressions.BinaryExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.BoolExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.DiscVariableExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.EnumLiteralExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.Expression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.IntExpression;
-import org.eclipse.escet.cif.metamodel.cif.expressions.UnaryExpression;
-import org.eclipse.escet.cif.metamodel.cif.types.BoolType;
-import org.eclipse.escet.cif.metamodel.cif.types.CifType;
-import org.eclipse.escet.cif.metamodel.cif.types.EnumType;
-import org.eclipse.escet.cif.metamodel.cif.types.IntType;
 import org.eclipse.escet.common.java.Assert;
 import org.eclipse.escet.common.java.Strings;
 import org.eclipse.escet.common.java.exceptions.InvalidInputException;
@@ -124,132 +109,7 @@ public class Cif2Mcrl2PreChecker {
                 msg = locTextStart + " has invariants.";
                 problems.add(msg);
             }
-            for (Edge edge: loc.getEdges()) {
-                for (Update upd: edge.getUpdates()) {
-                    Assignment asg = (Assignment)upd;
-                    msg = checkExpression(asg.getValue());
-                    if (msg != null) {
-                        msg = fmt("A value in %s %s", locTextMid, msg);
-                        problems.add(msg);
-                    }
-                }
-                for (Expression e: edge.getGuards()) {
-                    msg = checkExpression(e);
-                    if (msg != null) {
-                        msg = fmt("A guard in %s %s", locTextMid, msg);
-                        problems.add(msg);
-                    }
-                }
-            }
-        }
-    }
-
-    /**
-     * Check whether the expression supported.
-     *
-     * @param e Expression to check.
-     * @return The last part of an error message if an error was found, else {@code null}.
-     */
-    private String checkExpression(Expression e) {
-        CifType t = CifTypeUtils.normalizeType(e.getType());
-
-        if (t instanceof BoolType) {
-            if (e instanceof BoolExpression) {
-                return null;
-            } else if (e instanceof BinaryExpression) {
-                BinaryExpression be = (BinaryExpression)e;
-                switch (be.getOperator()) {
-                    case CONJUNCTION:
-                    case DISJUNCTION:
-                    case EQUAL:
-                    case GREATER_EQUAL:
-                    case GREATER_THAN:
-                    case LESS_EQUAL:
-                    case LESS_THAN:
-                    case UNEQUAL:
-                    case IMPLICATION:
-                        break;
-                    default: {
-                        String msg = fmt("has unsupported boolean binary operator \"%s\".",
-                                CifTextUtils.operatorToStr(be.getOperator()));
-                        return msg;
-                    }
-                }
-                String msg = checkExpression(be.getLeft());
-                if (msg == null) {
-                    msg = checkExpression(be.getRight());
-                }
-                return msg;
-            } else if (e instanceof UnaryExpression) {
-                UnaryExpression ue = (UnaryExpression)e;
-                switch (ue.getOperator()) {
-                    case INVERSE:
-                        break;
-                    default: {
-                        String msg = fmt("has unsupported boolean unary operator \"%s\".",
-                                CifTextUtils.operatorToStr(ue.getOperator()));
-                        return msg;
-                    }
-                }
-                return checkExpression(ue.getChild());
-            } else if (e instanceof DiscVariableExpression) {
-                return null;
-            }
-
-            return fmt("has unsupported boolean expression \"%s\".", CifTextUtils.exprToStr(e));
         }
-
-        if (t instanceof IntType) {
-            if (e instanceof IntExpression) {
-                return null;
-            } else if (e instanceof BinaryExpression) {
-                BinaryExpression be = (BinaryExpression)e;
-                switch (be.getOperator()) {
-                    case ADDITION:
-                    case MULTIPLICATION:
-                    case SUBTRACTION:
-                        break;
-                    default: {
-                        String msg = fmt("has unsupported integer binary operator \"%s\".",
-                                CifTextUtils.operatorToStr(be.getOperator()));
-                        return msg;
-                    }
-                }
-                String msg = checkExpression(be.getLeft());
-                if (msg == null) {
-                    msg = checkExpression(be.getRight());
-                }
-                return msg;
-            } else if (e instanceof UnaryExpression) {
-                UnaryExpression ue = (UnaryExpression)e;
-                switch (ue.getOperator()) {
-                    case NEGATE:
-                    case PLUS:
-                        break;
-                    default: {
-                        String msg = fmt("has unsupported integer unary operator \"%s\".",
-                                CifTextUtils.operatorToStr(ue.getOperator()));
-                        return msg;
-                    }
-                }
-                return checkExpression(ue.getChild());
-            } else if (e instanceof DiscVariableExpression) {
-                return null;
-            }
-
-            return fmt("has unsupported integer expression \"%s\".", CifTextUtils.exprToStr(e));
-        }
-
-        if (t instanceof EnumType) {
-            if (e instanceof EnumLiteralExpression) {
-                return null;
-            } else if (e instanceof DiscVariableExpression) {
-                return null;
-            }
-
-            return fmt("has unsupported enumeration expression \"%s\".", CifTextUtils.exprToStr(e));
-        }
-
     }
 
     /**
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index ca318839b8..2a962188c1 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -19,6 +19,12 @@ import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoTauCheck;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificBinaryExprsCheck;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificBinaryExprsCheck.NoSpecificBinaryOp;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck;
+import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck.NoSpecificUnaryOp;
 import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
@@ -78,7 +84,76 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new AutOnlyWithOneInitLocCheck(),
 
                 // No conditional updates and multi-assignments.
-                new EdgeOnlySimpleAssignmentsCheck()
+                new EdgeOnlySimpleAssignmentsCheck(),
+
+                // Only certain expression:
+                // - For expressions that produce a boolean value, only boolean literals, constants (eliminated
+                //   already), discrete variables, algebraic variables (eliminated already), binary operators 'and',
+                //   'or', '=>', '=', '!=', '<', '<=', '>' and '>=', and unary operator 'not' are supported.
+                // - For expressions that produce an enumeration value, only enumeration literals, constants (eliminated
+                //   already), discrete variables, and algebraic variables (eliminated already) are supported.
+                // - For expressions that produce an integer value, only integer literals, constants (eliminated
+                //   already), discrete variables, algebraic variables (eliminated already), binary operators '+', '*'
+                //   and '-', and unary operators '-' and '+' are supported.
+                // - Unary and binary expressions are only supported with boolean, integer and enumeration operands.
+                new ExprNoSpecificExprsCheck(
+                        NoSpecificExpr.FUNC_REFS,
+                        NoSpecificExpr.CAST_EXPRS,
+                        NoSpecificExpr.COMP_REFS,
+                        NoSpecificExpr.CONT_VAR_REFS,
+                        NoSpecificExpr.DICT_LITS,
+                        NoSpecificExpr.TUPLE_FIELD_REFS,
+                        NoSpecificExpr.FUNC_CALLS,
+                        NoSpecificExpr.IF_EXPRS,
+                        NoSpecificExpr.INPUT_VAR_REFS,
+                        NoSpecificExpr.LIST_LITS,
+                        NoSpecificExpr.LOC_REFS,
+                        NoSpecificExpr.PROJECTION_EXPRS,
+                        NoSpecificExpr.REAL_LITS,
+                        NoSpecificExpr.RECEIVE_EXPRS,
+                        NoSpecificExpr.SET_LITS,
+                        NoSpecificExpr.SLICE_EXPRS,
+                        NoSpecificExpr.STRING_LITS,
+                        NoSpecificExpr.SWITCH_EXPRS,
+                        NoSpecificExpr.TIME_VAR_REFS,
+                        NoSpecificExpr.TUPLE_LITS),
+                new ExprNoSpecificBinaryExprsCheck(
+                        NoSpecificBinaryOp.ADDITION_REALS,
+                        NoSpecificBinaryOp.ADDITION_LISTS,
+                        NoSpecificBinaryOp.ADDITION_STRINGS,
+                        NoSpecificBinaryOp.ADDITION_DICTS,
+                        NoSpecificBinaryOp.CONJUNCTION_SETS,
+                        NoSpecificBinaryOp.DISJUNCTION_SETS,
+                        NoSpecificBinaryOp.DIVISION,
+                        NoSpecificBinaryOp.ELEMENT_OF,
+                        NoSpecificBinaryOp.EQUAL_DICT,
+                        NoSpecificBinaryOp.EQUAL_LIST,
+                        NoSpecificBinaryOp.EQUAL_REAL,
+                        NoSpecificBinaryOp.EQUAL_SET,
+                        NoSpecificBinaryOp.EQUAL_STRING,
+                        NoSpecificBinaryOp.EQUAL_TUPLE,
+                        NoSpecificBinaryOp.GREATER_EQUAL_REALS,
+                        NoSpecificBinaryOp.GREATER_THAN_REALS,
+                        NoSpecificBinaryOp.INTEGER_DIVISION,
+                        NoSpecificBinaryOp.LESS_EQUAL_REALS,
+                        NoSpecificBinaryOp.LESS_THAN_REALS,
+                        NoSpecificBinaryOp.MODULUS,
+                        NoSpecificBinaryOp.MULTIPLICATION_REALS,
+                        NoSpecificBinaryOp.SUBSET,
+                        NoSpecificBinaryOp.SUBTRACTION_REALS,
+                        NoSpecificBinaryOp.SUBTRACTION_LISTS,
+                        NoSpecificBinaryOp.SUBTRACTION_SETS,
+                        NoSpecificBinaryOp.SUBTRACTION_DICTS,
+                        NoSpecificBinaryOp.UNEQUAL_DICT,
+                        NoSpecificBinaryOp.UNEQUAL_LIST,
+                        NoSpecificBinaryOp.UNEQUAL_REAL,
+                        NoSpecificBinaryOp.UNEQUAL_SET,
+                        NoSpecificBinaryOp.UNEQUAL_STRING,
+                        NoSpecificBinaryOp.UNEQUAL_TUPLE),
+                new ExprNoSpecificUnaryExprsCheck(
+                        NoSpecificUnaryOp.NEGATE_REALS,
+                        NoSpecificUnaryOp.PLUS_REALS,
+                        NoSpecificUnaryOp.SAMPLE)
 
         );
     }
-- 
GitLab


From 0b22c861b95f9493dcc09f41003d4b1327c83efd Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:38:55 +0200
Subject: [PATCH 14/20] #424 CIF to mCRL2 preconds move: no init preds in
 components.

---
 .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 4 ----
 .../eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java   | 6 +++++-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index a52e396637..6a52690f1f 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -123,10 +123,6 @@ public class Cif2Mcrl2PreChecker {
         // IO declarations should be eliminated already.
         Assert.check(comp.getIoDecls().isEmpty());
 
-        if (!comp.getInitials().isEmpty()) {
-            msg = fmt("Initialization predicates are not supported in %s.", CifTextUtils.getComponentText2(comp));
-            problems.add(msg);
-        }
         if (!comp.getInvariants().isEmpty()) {
             msg = fmt("Invariants are not supported in %s.", CifTextUtils.getComponentText2(comp));
             problems.add(msg);
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index 2a962188c1..dd14bea078 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -15,6 +15,7 @@ package org.eclipse.escet.cif.cif2mcrl2;
 
 import org.eclipse.escet.cif.checkers.CifPreconditionChecker;
 import org.eclipse.escet.cif.checkers.checks.AutOnlyWithOneInitLocCheck;
+import org.eclipse.escet.cif.checkers.checks.CompNoInitPredsCheck;
 import org.eclipse.escet.cif.checkers.checks.EdgeOnlySimpleAssignmentsCheck;
 import org.eclipse.escet.cif.checkers.checks.EqnNotAllowedCheck;
 import org.eclipse.escet.cif.checkers.checks.EventNoChannelsCheck;
@@ -153,7 +154,10 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                 new ExprNoSpecificUnaryExprsCheck(
                         NoSpecificUnaryOp.NEGATE_REALS,
                         NoSpecificUnaryOp.PLUS_REALS,
-                        NoSpecificUnaryOp.SAMPLE)
+                        NoSpecificUnaryOp.SAMPLE),
+
+                // No initialization predicates in components.
+                new CompNoInitPredsCheck()
 
         );
     }
-- 
GitLab


From 66eb3a7bf68037554af2d92cf8f5d06fdd3189ce Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:39:22 +0200
Subject: [PATCH 15/20] #424 CIF to mCRL2 preconds move: no invariants.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 24 -------------------
 .../cif/cif2mcrl2/CifToMcrl2PreChecker.java   | 10 +++++++-
 2 files changed, 9 insertions(+), 25 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
index 6a52690f1f..73c8a9dccf 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
@@ -14,19 +14,15 @@
 package org.eclipse.escet.cif.cif2mcrl2;
 
 import static org.eclipse.escet.common.java.Lists.list;
-import static org.eclipse.escet.common.java.Strings.fmt;
 
 import java.util.Collections;
 import java.util.List;
 
-import org.apache.commons.lang3.StringUtils;
-import org.eclipse.escet.cif.common.CifTextUtils;
 import org.eclipse.escet.cif.metamodel.cif.ComplexComponent;
 import org.eclipse.escet.cif.metamodel.cif.Component;
 import org.eclipse.escet.cif.metamodel.cif.Group;
 import org.eclipse.escet.cif.metamodel.cif.Specification;
 import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
-import org.eclipse.escet.cif.metamodel.cif.automata.Location;
 import org.eclipse.escet.common.java.Assert;
 import org.eclipse.escet.common.java.Strings;
 import org.eclipse.escet.common.java.exceptions.InvalidInputException;
@@ -96,20 +92,7 @@ public class Cif2Mcrl2PreChecker {
      * @param aut Automaton to check.
      */
     private void checkAutomaton(Automaton aut) {
-        String msg;
-
         checkComponent(aut);
-
-        // Check locations.
-        for (Location loc: aut.getLocations()) {
-            String locTextMid = CifTextUtils.getLocationText2(loc);
-            String locTextStart = StringUtils.capitalize(locTextMid);
-
-            if (!loc.getInvariants().isEmpty()) {
-                msg = locTextStart + " has invariants.";
-                problems.add(msg);
-            }
-        }
     }
 
     /**
@@ -118,14 +101,7 @@ public class Cif2Mcrl2PreChecker {
      * @param comp Component to check.
      */
     private void checkComponent(ComplexComponent comp) {
-        String msg;
-
         // IO declarations should be eliminated already.
         Assert.check(comp.getIoDecls().isEmpty());
-
-        if (!comp.getInvariants().isEmpty()) {
-            msg = fmt("Invariants are not supported in %s.", CifTextUtils.getComponentText2(comp));
-            problems.add(msg);
-        }
     }
 }
diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
index dd14bea078..854674d7da 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/CifToMcrl2PreChecker.java
@@ -26,6 +26,7 @@ import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck;
 import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificExprsCheck.NoSpecificExpr;
 import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck;
 import org.eclipse.escet.cif.checkers.checks.ExprNoSpecificUnaryExprsCheck.NoSpecificUnaryOp;
+import org.eclipse.escet.cif.checkers.checks.InvNoSpecificInvsCheck;
 import org.eclipse.escet.cif.checkers.checks.SpecAutomataCountsCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck;
 import org.eclipse.escet.cif.checkers.checks.TypeNoSpecificTypesCheck.NoSpecificType;
@@ -33,6 +34,9 @@ import org.eclipse.escet.cif.checkers.checks.VarDiscOnlyStaticEvalInitCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoContinuousCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoDiscWithMultiInitValuesCheck;
 import org.eclipse.escet.cif.checkers.checks.VarNoInputCheck;
+import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantKind;
+import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantPlaceKind;
+import org.eclipse.escet.cif.checkers.checks.invcheck.NoInvariantSupKind;
 import org.eclipse.escet.common.java.Termination;
 
 /** CIF to mCRL2 transformation precondition checker. */
@@ -157,7 +161,11 @@ public class CifToMcrl2PreChecker extends CifPreconditionChecker {
                         NoSpecificUnaryOp.SAMPLE),
 
                 // No initialization predicates in components.
-                new CompNoInitPredsCheck()
+                new CompNoInitPredsCheck(),
+
+                // No invariants.
+                new InvNoSpecificInvsCheck().disallow(
+                        NoInvariantSupKind.ALL_KINDS, NoInvariantKind.ALL_KINDS, NoInvariantPlaceKind.ALL_PLACES)
 
         );
     }
-- 
GitLab


From f04fe1e98e0d9766db15b1c12231e7629cced0dd Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:41:01 +0200
Subject: [PATCH 16/20] #424 Remove old CIF to mCRL2 precondition checker.

---
 .../cif/cif2mcrl2/Cif2Mcrl2PreChecker.java    | 107 ------------------
 1 file changed, 107 deletions(-)
 delete mode 100644 cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
deleted file mode 100644
index 73c8a9dccf..0000000000
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2PreChecker.java
+++ /dev/null
@@ -1,107 +0,0 @@
-//////////////////////////////////////////////////////////////////////////////
-// Copyright (c) 2010, 2024 Contributors to the Eclipse Foundation
-//
-// See the NOTICE file(s) distributed with this work for additional
-// information regarding copyright ownership.
-//
-// This program and the accompanying materials are made available
-// under the terms of the MIT License which is available at
-// https://opensource.org/licenses/MIT
-//
-// SPDX-License-Identifier: MIT
-//////////////////////////////////////////////////////////////////////////////
-
-package org.eclipse.escet.cif.cif2mcrl2;
-
-import static org.eclipse.escet.common.java.Lists.list;
-
-import java.util.Collections;
-import java.util.List;
-
-import org.eclipse.escet.cif.metamodel.cif.ComplexComponent;
-import org.eclipse.escet.cif.metamodel.cif.Component;
-import org.eclipse.escet.cif.metamodel.cif.Group;
-import org.eclipse.escet.cif.metamodel.cif.Specification;
-import org.eclipse.escet.cif.metamodel.cif.automata.Automaton;
-import org.eclipse.escet.common.java.Assert;
-import org.eclipse.escet.common.java.Strings;
-import org.eclipse.escet.common.java.exceptions.InvalidInputException;
-import org.eclipse.escet.common.java.exceptions.UnsupportedException;
-
-/** Class for performing checks whether the specification can be used as input for the CIF to mCRL2 transformation. */
-public class Cif2Mcrl2PreChecker {
-    /** Found problems in the specification. */
-    public List<String> problems = null;
-
-    /** Constructor of the {@link Cif2Mcrl2PreChecker} class. */
-    public Cif2Mcrl2PreChecker() {
-        // Nothing to do.
-    }
-
-    /**
-     * Perform checks whether the specification is usable for performing a CIF to mCRL2 transformation.
-     *
-     * @param spec Specification to check.
-     * @throws InvalidInputException If the specification violates the pre-conditions.
-     */
-    public void checkSpec(Specification spec) {
-        problems = list();
-        checkGroup(spec);
-
-        if (problems.isEmpty()) {
-            return;
-        }
-        // If we have any problems, the specification is unsupported.
-        Collections.sort(problems, Strings.SORTER);
-        if (!problems.isEmpty()) {
-            String msg = "CIF to mCRL2 transformation failed due to unsatisfied preconditions:\n - "
-                    + String.join("\n - ", problems);
-            throw new UnsupportedException(msg);
-        }
-    }
-
-    /**
-     * Unfold and check a group.
-     *
-     * @param grp Group to check and unfold.
-     */
-    private void checkGroup(Group grp) {
-        // Definitions should be eliminated already.
-        Assert.check(grp.getDefinitions().isEmpty());
-        checkComponent(grp);
-
-        for (Component c: grp.getComponents()) {
-            if (c instanceof Automaton) {
-                Automaton aut = (Automaton)c;
-                checkAutomaton(aut);
-                continue;
-            } else if (c instanceof Group) {
-                Group g = (Group)c;
-                checkGroup(g);
-                continue;
-            }
-
-            // ComponentInst should not happen, as DefInst has been eliminated.
-            throw new RuntimeException("Unexpected type of Component.");
-        }
-    }
-
-    /**
-     * Check whether the automaton satisfies all pre-conditions of the CIF to mCRL2 transformation.
-     *
-     * @param aut Automaton to check.
-     */
-    private void checkAutomaton(Automaton aut) {
-        checkComponent(aut);
-    }
-
-    /**
-     * Verify that the given component does not have elements that are not supported in the translation.
-     *
-     * @param comp Component to check.
-     */
-    private void checkComponent(ComplexComponent comp) {
-        // IO declarations should be eliminated already.
-        Assert.check(comp.getIoDecls().isEmpty());
-    }
-}
-- 
GitLab


From 4347eb3abdfd28f95f1aaae02d5b2d76413a3ff9 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:43:07 +0200
Subject: [PATCH 17/20] #424 Update rest of CIF to mCLR2 for removal of old
 precond checker.

---
 .../escet/cif/cif2mcrl2/storage/AutomatonData.java  | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java
index d94692b7c8..4d860e611b 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/storage/AutomatonData.java
@@ -19,7 +19,6 @@ import static org.eclipse.escet.common.java.Sets.set;
 import java.util.Map;
 import java.util.Set;
 
-import org.eclipse.escet.cif.cif2mcrl2.Cif2Mcrl2PreChecker;
 import org.eclipse.escet.cif.common.CifEventUtils;
 import org.eclipse.escet.cif.common.CifTextUtils;
 import org.eclipse.escet.cif.common.CifTypeUtils;
@@ -75,10 +74,6 @@ public class AutomatonData {
     /**
      * Find discrete variables in an automaton.
      *
-     * <p>
-     * Copy of {@link Cif2Mcrl2PreChecker#checkAutomaton}, but without checking on acceptable constructs.
-     * </p>
-     *
      * @param variableMap Mapping of discrete variables in the meta model to their representation in the translation.
      */
     public void addAutomatonVars(Map<DiscVariable, VariableData> variableMap) {
@@ -162,10 +157,6 @@ public class AutomatonData {
     /**
      * Find discrete variables in an expression.
      *
-     * <p>
-     * Copy of {@link Cif2Mcrl2PreChecker#checkExpression}, but without checking on acceptable constructs.
-     * </p>
-     *
      * @param e Expression to inspect.
      * @return Used discrete variables in the expression.
      */
@@ -220,10 +211,6 @@ public class AutomatonData {
     /**
      * Get the events belonging to an edge.
      *
-     * <p>
-     * Copy of part of {@link Cif2Mcrl2PreChecker#checkAutomaton}, but without checking on allowed constructs.
-     * </p>
-     *
      * @param edge Edge to inspect.
      * @return The events of the edge.
      */
-- 
GitLab


From 34e557df7a2620a66f55a8b16af0544cddf75ab3 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:45:05 +0200
Subject: [PATCH 18/20] #424 Adopt new CIF to mCRL2 precondition checker.

---
 .../eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java  | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java
index 7dd967650f..287d6bb526 100644
--- a/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java
+++ b/cif/org.eclipse.escet.cif.cif2mcrl2/src/org/eclipse/escet/cif/cif2mcrl2/Cif2Mcrl2Application.java
@@ -97,6 +97,7 @@ public class Cif2Mcrl2Application extends Application<IOutputComponent> {
         // Read CIF input.
         CifReader cifReader = new CifReader().init();
         Specification spec = cifReader.read();
+        String absSpecPath = Paths.resolve(InputFileOption.getPath());
         if (isTerminationRequested()) {
             return 0;
         }
@@ -123,9 +124,9 @@ public class Cif2Mcrl2Application extends Application<IOutputComponent> {
             return 0;
         }
 
-        // Check pre-conditions of the input.
-        Cif2Mcrl2PreChecker pca = new Cif2Mcrl2PreChecker();
-        pca.checkSpec(spec);
+        // Check preconditions.
+        CifToMcrl2PreChecker checker = new CifToMcrl2PreChecker(() -> isTerminationRequested());
+        checker.reportPreconditionViolations(spec, absSpecPath, "CIF to mCRL2 transformation");
         if (isTerminationRequested()) {
             return 0;
         }
-- 
GitLab


From 3a167675c5ad724bb4ff9416ce064868ce2ba4ea Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:56:18 +0200
Subject: [PATCH 19/20] #424 Update CIF to mCRL2 tests.

---
 .../tests/cif2mcrl2/invalid.cif               |  26 +--
 .../tests/cif2mcrl2/invalid.err               | 167 ++++++++++++++++--
 2 files changed, 163 insertions(+), 30 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif
index ec30f78b66..6961e85ffa 100644
--- a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif
+++ b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.cif
@@ -12,12 +12,12 @@
 //////////////////////////////////////////////////////////////////////////////
 
 group g:
-  event int[0..5] e1, e2;
+  event int[0..5] e1, e2;           // Channels.
 
-  invariant 1 + 1 = 2;
-  invariant 1 = 3;                  // Non-true invariant in group.
+  invariant 1 + 1 = 2;              // Invariant.
+  invariant 1 = 3;                  // Invariant.
 
-  initial 1 = 3;                    // Non-true initialization in group.
+  initial 1 = 3;                    // Initialization predicate in a component.
 
   automaton no_initial:             // No initial location.
     location:
@@ -35,24 +35,24 @@ group g:
   end
 
   plant p:
-    disc int[1..2] x1 in {1,2};     // Non-deterministic variable init.
-    disc int[1..2] x2 in any;       // Non-deterministic variable init.
+    disc int[1..2] x1 in {1,2};     // Multiple potential initial values.
+    disc int[1..2] x2 in any;       // Multiple potential initial values.
     cont cnt der 1.0;               // Continuous variable, real type/value.
     disc list bool lb = [true];     // List type/expr.
 
-    plant invariant 1 + 1 = 2;
-    plant invariant 1 = 3;          // Non-true invariant in automaton.
+    plant invariant 1 + 1 = 2;      // Invariant.
+    plant invariant 1 = 3;          // Invariant.
 
     location:
       initial true;
       edge e1 do if true: x1 := 2 end; // 'if' update.
-      edge e2 do lb := lb + [false];
+      edge e2 do lb := lb + [false];   // List type/expr.
 
-      plant invariant 1+1 = 2;
-      plant invariant 1 = 3;        // Non-true invariant in location.
+      plant invariant 1+1 = 2;      // Invariant.
+      plant invariant 1 = 3;        // Invariant.
   end
 
-  cont x der 1;
-  cont y;
+  cont x der 1;                     // Continuous variable.
+  cont y;                           // Continuous variable.
   equation y' = 2;                  // Equation.
 end
diff --git a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err
index 37699c831f..455faaffa6 100644
--- a/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err
+++ b/cif/org.eclipse.escet.cif.tests/tests/cif2mcrl2/invalid.err
@@ -5,20 +5,153 @@ WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 39, column 20: D
 WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 43, column 11: Duplicate state invariant.
 WARNING: File "cif2mcrl2/invalid.cif": Semantic warning at line 44, column 11: Duplicate state invariant.
 ERROR: CIF to mCRL2 transformation failed due to unsatisfied preconditions:
- - A value in the location of automaton "g.p" has an unsupported type "list bool" in expression "g.p.lb + [false]".
- - Automaton "g.mult_initials" has more than one initial location.
- - Automaton "g.no_initial" has no initial location.
- - Continuous variable "g.p.cnt" is unsupported in the transformation.
- - Continuous variable "g.x" is unsupported in the transformation.
- - Continuous variable "g.y" is unsupported in the transformation.
- - Discrete variable "g.p.lb" does not have a boolean, integer, or enumeration type.
- - Discrete variable "g.p.x1" does not have a single initial value.
- - Discrete variable "g.p.x2" does not have a single initial value.
- - Equations are not supported in group "g".
- - Initialization predicates are not supported in group "g".
- - Invariants are not supported in automaton "g.p".
- - Invariants are not supported in group "g".
- - The location of automaton "g.no_initial" has a "tau" event.
- - The location of automaton "g.no_initial" has a "tau" event.
- - The location of automaton "g.p" has conditional updates.
- - The location of automaton "g.p" has invariants.
+
+  ------------------------------
+  (1/16) A list literal is used.
+  ------------------------------
+   * In automaton "g.p":
+     - edge e2 do lb := lb + [false];
+                             ^
+   * In discrete variable "g.p.lb":
+     - disc list bool lb = [true];
+                           ^
+
+  ---------------------------
+  (2/16) A list type is used.
+  ---------------------------
+   * In automaton "g.p":
+     - edge e2 do lb := lb + [false];
+                  ^     ^  ^ ^
+   * In discrete variable "g.p.lb":
+     - disc list bool lb = [true];
+            ^              ^
+
+  -------------------------------------
+  (3/16) A real number literal is used.
+  -------------------------------------
+   * In group "g":
+     - equation y' = 2.0;
+                     ^
+   * In continuous variable "g.p.cnt":
+     - cont cnt = 0.0 der 1.0;
+                  ^       ^
+   * In continuous variable "g.x":
+     - cont x = 0.0 der 1.0;
+                ^       ^
+   * In continuous variable "g.y":
+     - cont y = 0.0;
+                ^
+
+  ---------------------------
+  (4/16) A real type is used.
+  ---------------------------
+   * In group "g":
+     - equation y' = 2.0;
+                     ^
+   * In continuous variable "g.p.cnt":
+     - cont cnt = 0.0 der 1.0;
+                  ^       ^
+   * In continuous variable "g.x":
+     - cont x = 0.0 der 1.0;
+                ^       ^
+   * In continuous variable "g.y":
+     - cont y = 0.0;
+                ^
+
+  ---------------------------
+  (5/16) An equation is used.
+  ---------------------------
+   * In group "g":
+     - equation y' = 2.0;
+                   ^
+
+  ----------------------------
+  (6/16) An invariant is used.
+  ----------------------------
+   * In group "g":
+     - invariant false;
+       ^
+   * In automaton "g.p":
+     - plant invariant false;
+             ^
+     - plant invariant false;
+             ^
+
+  ------------------------------------------------
+  (7/16) Automaton has multiple initial locations.
+  ------------------------------------------------
+   * In group "g":
+     - automaton mult_initials:
+                 ^
+
+  -----------------------------------------
+  (8/16) Automaton has no initial location.
+  -----------------------------------------
+   * In group "g":
+     - automaton no_initial:
+                 ^
+
+  -----------------------------------------------------------
+  (9/16) Binary operator "+" is used on a list typed operand.
+  -----------------------------------------------------------
+   * In automaton "g.p":
+     - edge e2 do lb := lb + [false];
+                           ^
+
+  --------------------------------------------------
+  (10/16) Component has an initialization predicate.
+  --------------------------------------------------
+   * In group "g":
+     - initial false;
+               ^
+
+  ----------------------------------------------------------------
+  (11/16) Discrete variable has multiple potential initial values.
+  ----------------------------------------------------------------
+   * In automaton "g.p":
+     - disc int[1..2] x1 in {1, 2};
+                      ^
+
+  ------------------------------------------------------------------------------------------
+  (12/16) Discrete variable has multiple potential initial values (any value in its domain).
+  ------------------------------------------------------------------------------------------
+   * In automaton "g.p":
+     - disc int[1..2] x2 in any;
+                      ^
+
+  --------------------------------
+  (13/16) Edge has an 'if' update.
+  --------------------------------
+   * In automaton "g.p":
+     - edge e1 do if true: x1 := 2 end;
+                  ^
+
+  -----------------------------------------
+  (14/16) Edge has an explicit 'tau' event.
+  -----------------------------------------
+   * In automaton "g.no_initial":
+     - edge e1, e2, tau;
+                    ^
+     - edge tau;
+            ^
+
+  ---------------------------
+  (15/16) Event is a channel.
+  ---------------------------
+   * In group "g":
+     - event int[0..5] e1;
+                       ^
+     - event int[0..5] e2;
+                       ^
+
+  ------------------------------------------
+  (16/16) Variable is a continuous variable.
+  ------------------------------------------
+   * In group "g":
+     - cont x = 0.0 der 1.0;
+            ^
+     - cont y = 0.0;
+            ^
+   * In automaton "g.p":
+     - cont cnt = 0.0 der 1.0;
+            ^
-- 
GitLab


From 974a9c3dbf843e73873ab05a33352804d4bffed2 Mon Sep 17 00:00:00 2001
From: Dennis Hendriks <dh_tue@hotmail.com>
Date: Fri, 26 Jul 2024 12:57:35 +0200
Subject: [PATCH 20/20] #424 Fix CIF to mCRL2 documentation.

- Properly escape '=>'.
- Binary operators '=' and '!=' are also supported for enums/ints.
- Binary comparison operators are supported for ints.
- Fixed English mistake.
---
 .../asciidoc/tools/cif2mcrl2.asciidoc                       | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc
index 3922016b73..cfeee748a8 100644
--- a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc
+++ b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/cif2mcrl2.asciidoc
@@ -109,8 +109,10 @@ The latter may have a range.
 *** Boolean-typed constants are supported.
 *** Boolean-typed discrete variables are supported.
 *** Boolean-typed algebraic variables are supported.
-*** Binary operators `and`, `or`, `==`, `!=` and `=>` on boolean-typed arguments are supported.
-*** Unary operator `not` on boolean-typed arguments are supported.
+*** Binary operators `and`, `or` and `+=>+` on boolean-typed arguments are supported.
+*** Binary operators `=` and `!=` on boolean, enum and integer-typed arguments are supported.
+*** Binary operators `<`, `+<=+`, `>` and `>=` on integer-typed arguments are supported.
+*** Unary operator `not` on boolean-typed arguments is supported.
 *** Location references are not supported.
 ** Regarding enumeration-typed expressions (resulting in an enumeration literal as value):
 *** Enumeration literals are supported.
-- 
GitLab